View source for SURF 2012: Evaluation and benchmarking for robot motion planning problems using TuLiP

'''[[SURF 2012|2012 SURF]] project description'''
* Mentor: Richard Murray
* Co-mentor: Ufuk Topcu, Necmiye Ozay and Pavithra Prabhakar

The Temporal Logic Planning Toolbox, TuLiP, is a collection of Python-based routines for automatic synthesis of correct-by-construction embedded control software as discussed in [1].  This project aims at (i) expanding the available synthesis tools (i.e. solvers) in TuLiP by using off-the-shelf model checkers and temporal logic game solvers and (ii) empirically analyzing the performance of these solvers on robot motion planning problems.

In particular, symbolic model checkers (e.g. NuSMV [2]) are known to work better for hardware (e.g. digital circuit) verification, whereas automaton-based
model checkers (e.g. SPIN [3]) are considered to be more suitable for software verification. Both of these model checkers can be used to do synthesis when there is no dynamic environment (for example, robotic motion planning tasks with fixed floor map). The goal of this project is to develop a benchmark to compare the performance of standard symbolic vs. automaton-based model checkers in the context of 2D motion planning with LTL specifications (maybe for a few simple dynamic robot models). This benchmark will be used to empirically evaluate the performance of the solvers implemented in TuLiP. 

Along with this study, the following improvements to TuLiP will be required:
* Adding new solvers to TuLiP by developing wrappers to model checkers (NuSMV and SPIN) for synthesis problems without adversarial environment. Additionally and if time allows, interfacing to additional temporal logic game solvers (in particular to those that solve either strict subsets, e.g., safety games, or supersets, e.g., whole LTL, of GR[1] specifications) for the problems with adversarial environment.
* Standardization of input, output and automaton formats for different solvers Developing error handling routines for the syntax of the input LTL specification (e.g. checking parentheses, etc. using regular expressions) 

''Required Skills:'' This project requires programming experience. 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 \cite{eeci}) is desired.

'''References'''
# T. 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). 
# NuSMV, http://nusmv.fbk.eu/
# Spin Model Checker, http://spinroot.com/spin/whatispin.html.
# EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website, http://www.cds.caltech.edu/~utopcu/index.php/HYCON-EECI,_Spring_2011.