SURF 2017: Scalable Robust Synthesis from Temporal Logic Specifications

2017 SURF project description

• Mentor: Richard M. Murray
• Co-mentors: Sumanth Dathathri

Several interesting problems are presented below and it is desirable that the SURF identifies one or more of the following problems in addition to the experimental task to develop some experience with working on theoretical problems. The primary task would be to develop an experimental test-bed for demonstration/evaluation of recent results and future work with regard to the optimality and robustness of controllers synthesized from temporal logic specifications.

The test bed would be a platform that allows for noise/failures to manifest in the form of sensing noise/actuation failures/unexpected behavior from the environment. The precise form of the test-bed is to be determined (after some preliminary research/exploring literature) -- it could consist of a swarm of quad rotors, RC cars or turtle bots for example. A good starting point would be the experimental set up proposed for the Formal Methods for Robotics Challenge at ICRA 2016. In addition to the design of the experimental facility, other interesting areas of work for the SURF to contribute towards are:

1. Scalable Synthesis A current direction of research in the group is exploring the parallelizability of GR(1) synthesis [3]. The complexity of the algorithm scales as cube of the length of the formula (number of liveness formulas to be satisfied). For large problems, algorithms that are linear or quasi-linear algorithms are desirable. Parallelizing the synthesis algorithm could reduce the complexity, enabling synthesis for systems where the formulas are complex and large. Identifying scenarios in which the synthesis can be efficiently parallelized is an interesting topic. Once proofs are developed for the theory, the SURF would help with writing code to develop a tool that incorporates the parallelization into the synthesis algorithm. Additionally, coming up with heuristics for instances where parallelization cannot be done in a complete manner (completeness here refers to the guarantee that a solution is found whenever the problem is feasible) to parallelize the algorithm is an area to explore for the motivated SURF . Heuristics could potentially involve learning-based algorithms for decomposition or other algorithmic approaches (eg. greedy).

2. Robust Synthesis using Reinforcement Learning to augment robustness There has been recent work on employing reinforcement learning for enforcing temporal logic specifications [1,2]. In [4], the authors construct a product MDP that combines a Rabin automata generated from a LTL spec to synthesize reactive optimal controllers that satisfy LTL specifications. In general, for strategies synthesized from logic specifications, the guarantees fail to hold in case of modeling uncertainty or deviation in behavior of the environment from its assumed behavior. They observe from experiments that the controllers generated do reasonably well even for scenarios when the formula cannot be satisfied. Exploring this line of work, developing theoretical guarantees regarding robustness for such a synthesis approach would be useful.

Though not necessary, it would be useful for the student to have some knowledge of the following:

• Mathematical Logic, Formal Methods
• Some background in Algorithms (CS 2, Ma 5, CS21 at Caltech, CS38 at Caltech) -- not essential but would be useful for exploring research directions
• Programming Skills (Preferably Python, if not some experience with C or Java or other languages would be good)
• Familiarity with Linear Temporal Logic and Formal Verification (CS118) (useful, but not necessary)
• Familiarity with Reinforcement Learning (would be useful but not necessary)
• Familiarity with Robot Operating System (ROS) platform (useful not necessary, can be picked up during the course of the summer)

References

[1] D. Aksaray, A. Jones, Z. Kong, M. Schwager, and C. Belta. Q-learning for robust satisfaction of signal temporal logic specifications. CoRR, abs/1609.07409, 2016.

[2] A. Jones, D. Aksaray, Z. Kong, M. Schwager, and C. Belta. Enforcing temporal logic specifications via reinforcement learning. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC ’15, pages 279–280, New York, NY, USA, 2015. ACM

[3] Y. Kesten, N. Piterman, and A. Pnueli. Bridging the gap between fair simulation and trace inclusion. Information and Computation, 200:35– 61, 2005.

[4] D. Sadigh, E. S. Kim, S. Coogan, S. S. Sastry, and S. A. Seshia. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. CoRR, abs/1409.5486, 2014.