Receding horizon control for temporal logic specifications

ABSTRACT

In this paper, we describe a receding horizon framework that satisfies a class of linear temporal logic specifications sufficient to describe a wide range of properties including safety, stability, progress, obligation, response and guarantee. The resulting embedded control software consists of a goal generator, a trajectory planner, and a continuous controller. The goal generator essentially reduces the trajectory generation problem to a sequence of smaller problems of short horizon while preserving the desired system-level temporal properties. Subsequently, in each iteration, the trajectory planner solves the corresponding short-horizon problem with the currently observed state as the initial state and generates a feasible trajectory to be implemented by the continuous controller. Based on the simulation property, we show that the composition of the goal generator, trajectory planner and continuous controller and the corresponding receding horizon framework guarantee the correctness of the system. To handle failures that may occur due to a mismatch between the actual system and its model, we propose a response mechanism and illustrate, through an example, how the system is capable of responding to certain failures and continues to exhibit a correct behavior.

References

1. DARPA Urban Challenge. http://www.darpa.mil/grandchallenge/index.asp, 2007.
2. D. Conner, H. Kress-Gazit, H. Choset, A. Rizzi, and G. Pappas. Valet parking without a valet. In Proc. of IEEE/RSJ International Conference on Intelligent Robots and Systems, pages 572--577, 2007.
3. E. A. Emerson. Temporal and modal logic. In Handbook of theoretical computer science (vol. B): formal models and semantics, pages 995--1072. MIT Press, Cambridge, MA, USA, 1990.
4. A. Girard, A. A. Julius, and G. J. Pappas. Approximate simulation relations for hybrid systems. Discrete Event Dynamic Systems, 18(2):163--179, 2008.
5. A. Girard and G. J. Pappas. Brief paper: Hierarchical control system design using approximate simulation. Automatica, 45(2):566--571, 2009.
6. G. C. Goodwin, M. M. Seron, and J. A. D. Dona. Constrained Control and Estimation: An Optimisation Approach. Springer, 2004.
7. M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2nd edition, 2004.
8. A. Jadbabaie. Nonlinear Receding Horizon Control: A Control Lyapunov Function Approach. PhD thesis, California Institute of Technology, 2000.
9. S. Karaman and E. Frazzoli. Sampling-based motion planning with deterministic µ-calculus specifications. In Proc. of IEEE Conference on Decision and Control, Dec. 2009.
10. M. Kloetzer and C. Belta. A fully automated framework for control of linear systems from temporal logic specifications. IEEE Transaction on Automatic Control, 53(1):287--297, 2008.
11. H. Kress-Gazit, G. Fainekos, and G. Pappas. Where's waldo? Sensor-based temporal logic motion planning. In Proc. of IEEE International Conference on Robotics and Automation, pages 3116--3121, April 2007.
12. H. Kress-Gazit and G. J. Pappas. Automatically synthesizing a planning and control subsystem for the DARPA Urban Challenge. In IEEE International Conference on Automation Science and Engineering, pages 766--771, 2008.
13. Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems. Springer-Verlag, 1992.
14. D. Mayne, J. Rawlings, C. Rao, and P. Scokaert. Constrained model predictive control: Stability and optimality. Automatica, 36:789--814(26), June 2000.
15. M. B. Milam, K. Mushambi, and R. M. Murray. A new computational approach to real-time trajectory generation for constrained mechanical systems. In Proc. of IEEE Conference on Decision and Control, pages 845--851, 2000.
16. R. M. Murray, J. Hauser, A. Jadbabaie, M. B. Milam, N. Petit, W. B. Dunbar, and R. Franz. Online control customization via optimization-based control. In Software-Enabled Control: Information Technology for Dynamical Systems, pages 149--174. Wiley-Interscience, 2002.
17. N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364--380. Springer-Verlag, 2006. Software available at http://jtlv.sourceforge.net/.
18. S. J. Russell and P. Norvig. Artificial Intelligence: A Modern Approach. Pearson Education, 2003.
19. P. Tabuada and G. J. Pappas. Linear time logic control of linear systems. IEEE Transaction on Automatic Control, 51(12):1862--1877, 2006.
20. H. Tanner and G. J. Pappas. Simulation relations for discrete-time linear systems. In Proc. of the IFAC World Congress on Automatic Control, pages 1302--1307, 2002.
21. T. Wongpiromsarn and R. M. Murray. Distributed mission and contingency management for the DARPA urban challenge. In International Workshop on Intelligent Vehicle Control Systems (IVCS), 2008.
22. T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon temporal logic planning for dynamical systems. In Proc. of IEEE Conference on Decision and Control, Dec. 2009.

Index Terms

• Computing methodologies

  • Artificial intelligence

    • Control methods

      • Computational control theory

    • Planning and scheduling

• Software and its engineering

  • Software creation and management

    • Designing software

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods