SURF 2015: Optimal Trajectory Generation under Environmental Uncertainties using Signal Temporal Logic Specifications
2015 SURF project description
- Mentor: Richard Murray
- Co-mentor: Samira Farahani
In safety-critical robotics applications in which autonomous air, ground, and space vehicles carry out complex tasks, it is important to concisely and unambiguously specify the desired system behavior to be able to automatically synthesize a controller that implements this behavior. Controller synthesis is complicated by the fact that autonomous systems often have high-dimensional, nonlinear dynamics and require efficient (not just feasible) controllers.
This project aims at designing a “correct by construction” controller for an autonomous vehicle that is capable of responding to a dynamic environment, visiting goals, periodically monitoring areas, staying safe, and remaining stable. To this end, we will take advantage of the new tools and techniques for formal specification, design, and verification of embedded control systems [3]. In these approaches, we either verify that a given design satisfies the specification or synthesize a controller that satisfies the specification, as summarized in the following figure.
The formal language that we use in this project is Signal Temporal Logic (STL), which allows the specification of properties of dense-time, real-valued signals. For an efficient implementation, we will directly encode an STL formula as mixed-integer linear constraints on the original dynamical system [2]. Of particular interest are mixed logical dynamical (MLD) systems and certain differentially flat systems, whose dynamics can be encoded with mixed-integer linear constraints. MLD systems include constrained linear systems, linear hybrid automata, and piecewise affine systems. Differentially flat systems include quadrotors and car-like robots.
After the successful design the controller, we are going to perform a detailed comparison of mixed-integer linear programming solvers and Boolean satisfiability solvers that have been extended to support linear operations, e.g., [1]. Moreover, depending on the progress lever, we can also implement the controller on of the available robots in the lab for experimental purposes.
Required Skills: The software we will use for the implementation of formal methods is called TuLiP [4] and the programming language underlying TuLiP is Python. The student is expected to know Matlab and Python or to have enough programming experience to learn it in a short time. Some familiarity with or willingness to learn automata theory, formal languages, and model checking (see for instance to the extent of the first 5 lectures in [5]) is desired.
References:
[1] M. Fränzle and C. Herde. Efficient proof engines for bounded model checking of hybrid systems. Electronic Notes in Theoretical Computer Science, 133:119–137, 2005. http://homepage.divms.uiowa.edu/~tinelli/classes/AR-group/readingsF04/FMICS04_Fraenzle_Herde.pdf
[2] V. Raman, A. Donzé, M. Maasoumy, R. M. Murray, A. Sangiovanni-Vincentelli, S. A. Seshia, Model Predictive Control with Signal Temporal Logic Specifications, CDC 2014. http://users.cms.caltech.edu/~vasu/papers/vraman_cdc_14.pdf
[3] E. M. Wolff, U. Topcu, and R. M. Murray, Optimization-based trajectory generation with linear temporal logic specifications, International Conference on Robotics and Automation (ICRA), 2014. http://www.cds.caltech.edu/~ewolff/wolff_icra14.pdf
[4] Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R.~M. Murray, TuLiP: a software toolbox for receding horizon temporal logic planning, International Conference on Hybrid Systems: Computation and Control, 2011 (software available at http://tulip-control.sourceforge.net). http://www.aero.umd.edu/~mumu/files/wtoxm_HSCC2011.pdf
[5] EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website http://www.cds.caltech.edu/~murray/wiki/index.php/HYCON-EECI,_Spring_2013
