Control Strategy Synthesis under Infeasible Goals: a Maximally-Satisfying Approach

The application of temporal logic-based control strategy synthesis to autonomous robot action and motion planning combines two benefits: First, temporal logic formulas can capture rich, high-level goal specifications, including safety, sequencing, persistent surveillance, or request-response properties. Second, using formal methods, a correct-by-design plan can be automatically generated that guarantees the satisfaction of the temporal logic goal. However, such a plan often does not exist, e.g., due to logical conflicts in the goal specifications or environmental constraints. In this talk, we introduce the concept of maximally-satisfying planning, where we aim to synthesize as good plan/control strategy as possible instead of reporting the failure to meet the goal specification. Two specific use cases are discussed: reactive control of a NAO robot, whose attempt to execute an action primitive may succeed as well as fail, and motion planning for an autonomous golf cart that cannot achieve its goal destination without a partial violation of the prescribed road rules. The latter case involves the integration of maximally-satisfying planning with the RRT* motion planning algorithm. 

Speaker Biography

Jana Tumova is a postdoctoral researcher at the Automatic Control Department at KTH Royal Institute of Technology in Stockholm, Sweden. She received the PhD degree in computer science from Masaryk University in Brno, Czech Republic in 2013 and she was also a visiting researcher at Boston University and MIT. Her research interests include formal verification, control synthesis, and temporal logics in general, as well as formal methods applied in robot motion planning, control and analysis of dynamical and hybrid systems and multi-agent control.