View source for SURF 2015: Optimal Trajectory Generation under Environmental Uncertainties using Signal Temporal Logic Specifications

'''[[SURF 2015|2015 SURF]] project description'''
Mentor: Richard Murray<br>
Co-mentor: Samira Farahani

The recent planetary decadal survey describes missions that impose tremendously challenging requirements on resilience. The Uninhabited Aerial Vehicles (UAVs) and spacecraft that support these missions will need to be capable of reasoning about their own state and the state of the environment in order to predict and avoid hazardous conditions, to recover from internal failures, and to ultimately meet critical science objectives in the presence of substantial uncertainties. 

This project aims at designing a “correct by construction” controller for a UAV to satisfy its mission under the environmental uncertainties. To this end, we will take advantage of the new tools and techniques for formal specification, design, and verification of embedded control systems [1,2,3,4]. 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. 

Once the model is designed and tested using computer simulation, it is going to be implemented on one of the UAVs that are available in our lab. The idea is to use this UAV as a benchmark to experiment the effect of environmental changes on the controller and to investigate the responsiveness of the controller to these changes. 

[[File:Agent.png]]

''Required Skills:'' The software we will use for the implementation of formal methods is called TuLiP [5] and the programming language underlying TuLiP is Python. The student is expected to know 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 [6]) is desired.

References:

[1] S. Livingston, R. M. Murray, and J. W. Burdick. Backtracking temporal logic synthesis for uncertain environments. In Proc. IEEE International Conference on Robotics and Automation, 2012.
http://scottman.net/pub/Livingston-Murray-Burdick-ICRA2012.pdf

[2] U. Topcu, N. Ozay, J. Liu, , and R. M. Murray. On synthesizing robust discrete controllers under modeling uncertainty. In Hybrid Systems: Computation and Control, 2012.
http://www.cds.caltech.edu/~murray/preprints/tolm12-hscc_s.pdf

[3] E. M. Wolff, U. Topcu, and R. M. Murray. Robust control of uncertain Markov decision processes with temporal logic speci_cations. In Proc. American Control Conference, 2012.
http://www.cds.caltech.edu/~ewolff/wolff_cdc12.pdf

4] T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon temporal logic planning. IEEE Transactions on Automatic Control, 57(11):2817{2830, 2012. http://www.seas.upenn.edu/~utopcu/pubs/WTM-itac12.pdf

[5] 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

[6] EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website
http://www.cds.caltech.edu/~murray/wiki/index.php/HYCON-EECI,_Spring_2013