SURF 2014: Invariant Refinement for Receding Horizon Temporal Logic Planning

2014 SURF project description

• Mentor: Richard Murray
• Co-mentor: Vasu Raman

Fig. 1. Illustration of state space partitioning for receding horizon framework, c.f. Fig. 2 of [1].

Fig. 2. Road network and autonomous vehicle example from Fig. 5 of [1]. Solid black lines indicate the discrete states considered for the full planning problem, red dotted lines demarcate subsets used in the receding horizon framework.

Overview: Linear Temporal Logic (LTL) synthesis has been successfully applied to the construction of control policies for autonomous systems such as robots and embedded systems software. LTL synthesis frameworks allow non-expert users to easily specify tasks and have the relevant systems automatically synthesize and execute implementing controllers. One limitation of synthesis from LTL specifications is the combinatorial blow up of the state-space, or the “state explosion problem”. To address this, recent work proposed a receding horizon framework for synthesizing and executing finite state automata while ensuring system correctness with respect to a given LTL specification [1]. The key idea is to reduce the synthesis problem into a set of smaller problems of shorter horizon, effectively shrinking the domain.

Receding horizon approaches rely on two key factors: the existence of a collection of subsets of the discrete states, partially ordered based on their distance to the goal, and an invariant formula that, when fulfilled by all initial states, ensures that there exists a path between the aforementioned subsets. These approaches are incomplete: there may exist a control strategy that satisfies the original specification, but no suitable invariant or collection of subsets to allow a receding horizon strategy to be applied

Goals: This project will investigate rigorous methods for determining a sufficient invariant formula for a receding horizon approach to LTL synthesis. This invariant is currently determined by iteratively refining an initial guess, based on the infeasible initial states returned by the synthesis algorithm. However, additional information can be extracted from an infeasible specification that could accelerate convergence to a feasible invariant [2]. Open research questions include:

1. What information can be extracted from unsynthesizable receding horizon control specifications about the reason for failure?
2. How can this information be used to
   • refine the invariant
   • refine the set of partially ordered subsets of discrete states

All software produced as a result of this project will be integrated with the Temporal Logic Planning Toolbox (TuLiP)[3].

Required Skills: This project requires programming experience, ideally in Python and Java. Familiarity with and an interest in applied automata theory and formal methods such as model checking and logic synthesis is desired.

References

[1] T. Wongpiromsarn, U. Topcu, and R. Murray. Receding horizon temporal logic planning, IEEE Transactions on Automatic Control, 57(11):2817-2830, 2012.

[2] V.Raman and H. Kress-Gazit. Explaining impossible high-level robot behaviors, IEEE Transactions on Robotics, 29(1): 94-104, 2013.

[3] 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: https://github.com/tulip-control/tulip-control).