Research seminar "Negotiation for Temporal Logic Missions with Time Optimality and Probabilistic Satisfaction Guarantees"

Abstract:

We propose a human-supervised control synthesis method for a stochastic Dubins vehicle such that the expected time to satisfy a temporal logic specification over some environ- mental properties is minimized, while maintaining the satisfaction probability above a given probability threshold. Under some mild assumptions, we construct a finite approximation for the motion of the vehicle in the form of a Markov Decision Process (MDP). We allow for task specifications given as a formula in a fragment of Probabilistic Computation Tree Logic (PCTL). We propose an algorithm for synthesizing an optimal MDP control policy that minimizes the expected completion time with respect to the probability threshold. If the constraint can not be satisfied with the initial specification, for the proposed PCTL fragment, we define specification update rules that guarantee to increase the satisfaction probability. The initial specification can be updated, using the rules, until the supervisor is satisfied with the updated specification and the corresponding satisfaction probability is above the desired threshold. We demonstrate the capabilities of the framework using simulations.

CV:

Igor Cizelj received the B.S. and M.Sc. degrees in mechanical engineering from the Faculty of Mechanical Engineering and Naval Architecture at the University of Zagreb, Zagreb, Croatia, in 2008 and 2009, respectively. He is currently working toward the Ph.D. degree in systems engineering with the Boston University, Boston, MA. His research interest include motion planning and control, formal methods in control synthesis, stochastic processes in probability theory, and robotics.