Skip to main content
SpringerLink
Log in

Model Checking LTL over Controllable Linear Systems Is Decidable

  • Conference paper
  • First Online:
Hybrid Systems: Computation and Control (HSCC 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2623))

Included in the following conference series:

Abstract

The use of algorithmic verification and synthesis tools for hybrid systems is currently limited to systems exhibiting simple continuous dynamics such as timed automata or rectangular hybrid systems. In this paper we enlarge the class of systems amenable to algorithmic analysis and synthesis by showing decidability of model checking Linear Temporal Logic (LTL) formulas over discrete time, controllable, linear systems. This result follows from the construction of a language equivalent, finite abstraction of a control system based on a set of finite observations which correspond to the atomic propositions appearing in a given LTL formula. Furthermore, the size of this abstraction is shown to be polynomial in the dimension of the control system and the number of observations. These results open the doors for verification and synthesis of continuous and hybrid control systems from LTL specifications.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. Hybrid automata: An algorithmic approach to specification and verification of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  2. R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  3. Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere, and George J. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88:971–984, 2000.

    Google Scholar 

  4. E. Asarin, G. Schneider, and S. Yovine. On the decidability of the reachability problem for planar differential inclusions. In M. D. Di Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, volume 2034 of Lecture Notes in Computer Science, pages 89–104. Springer-Verlag, 2001.

    Chapter  Google Scholar 

  5. A. Bemporad and M. Morari. Control of systems integrating logic, dynamics and constraints. Automatica, 35(3):407–427, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  6. Mireille Broucke. A geometric approach to bisimulation and verification of hybrid systems. In Fritz W. Vaandrager and Jan H. van Schuppen, editors, Hybrid Systems: Computation and Control, volume 1569 of Lecture Notes in Computer Science, pages 61–75. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  7. P. Brunovsky. A classification of linear controllable systems. Kybernetika, 6(3):173–188, 1970.

    MathSciNet  MATH  Google Scholar 

  8. Edmund M. M. Clarke, Doron Peled, and Orna Grumberg. Model Checking. MIT Press, 1999.

    Google Scholar 

  9. J.E.R. Cury, B.H. Krogh, and T. Niinomi. Synthesis of supervisory controllers for hybrid systems based on approximating automata. IEEE Transactions on Automatic Control: Special Issue on Hybrid Systems, 43(4):564–568, April 1998.

    Article  MATH  MathSciNet  Google Scholar 

  10. E. A. Emerson. Handbook of Theoretical Computer Science, volume B, chapter Temporal and modal logic, pages 995–1072. Elsevier Science, 1990.

    MathSciNet  Google Scholar 

  11. E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.

    Article  MATH  Google Scholar 

  12. L.C.G.J.M. Habets and J. H. van Schuppen. Control of piecewise-linear hybrid systems on simplices and rectangles. In M. D. Di Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, volume 2034 of Lecture Notes in Computer Sience, pages 261–274. Springer-Verlag, 2001.

    Google Scholar 

  13. T.A. Henzinger and R. Majumdar. Symbolic model checking for rectangular hybrid systems. In S. Graf, editor, TACAS 2000: Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science, New-York, 2000. Springer-Verlag.

    Google Scholar 

  14. Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57:94–124, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  15. R. E. Kalman. Kronecker invariants and feedback. In L. Weiss, editor, Ordinary Differential Equations, pages 459–471. Academic Press, New York, 1972.

    Google Scholar 

  16. Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, and Moshe Y. Vardi. Open systems in reactive environments: Control and synthesis. In Proceedings of the 11th International Conference on Concurency Theory, volume 1877 of Lecture Notes in Computer Science, pages 92–107. Springer-Verlag, 2000.

    Google Scholar 

  17. Gerardo Lafferriere, George J. Pappas, and Shankar Sastry. O-minimal hybrid systems. Mathematics of Control, Signals and Systems, 13(1):1–21, March 2000.

    Article  MATH  MathSciNet  Google Scholar 

  18. P. Madhusudan and P.S. Thiagarajan. Branching time controllers for discrete event systems. Theoretical Computer Science, 274:117–149, March 2002.

    Google Scholar 

  19. Z. Manna and P. Wolper. Synthesis of communication processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6:68–93, 1984.

    Article  MATH  Google Scholar 

  20. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  21. R. Milner. Communication and Concurrency. Prentice Hall, 1989.

    Google Scholar 

  22. T. Moor and J. M. Davoren. Robust controller synthesis for hybrid systems using modal logic. In M. D. Di Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, volume 2034 of Lecture Notes in Computer Science. Springer-Verlag, 2001.

    Chapter  Google Scholar 

  23. eorge J. Pappas. Bisimilar linear systems. Automatica, 2001. To appear.

    Google Scholar 

  24. D.M.R. Park. Concurrency and automata on infinite sequences, volume 104 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

    Google Scholar 

  25. A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular inclusions. In Computer Aided Verification, pages 95–104, 1994.

    Google Scholar 

  26. Eduardo D. Sontag. Mathematical Control Theory, volume 6 of Texts in Applied Mathematics. Springer-Verlag, New-York, 2nd edition, 1998.

    Google Scholar 

  27. Colin Stirling. Handbook of logic in computer science, volume 2, chapter Modal and Temporal Logics, pages 477–563. Oxford University Press, 1992.

    MathSciNet  Google Scholar 

  28. J.A. Stiver, X.D. Koutsoukos, and P.J. Antsaklis. An invariant based approach to the design of hybrid control systems. International Journal of Robust and Nonlinear Control, 11(5):453–478, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  29. Paulo Tabuada and George J. Pappas. Finite bisimulations of controllable linear systems. Theoretical Computer Science, January 2003. Submitted, available at http://www.seas.upenn.edu/~tabuadap.

Download references

Author information

Authors and Affiliations

  1. Department of Electrical and Systems Engineering, University of Pennsylvania, 19104, Philadelphia, PA

    Paulo Tabuada & George J. Pappas

Authors
  1. Paulo Tabuada
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. George J. Pappas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS-VERIMAG, 2 avenue de Vignate, 38610, Gières, France

    Oded Maler

  2. Weizmann Institute of Science, Rehovot, 76100, Israel

    Amir Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tabuada, P., Pappas, G.J. (2003). Model Checking LTL over Controllable Linear Systems Is Decidable. In: Maler, O., Pnueli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2003. Lecture Notes in Computer Science, vol 2623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36580-X_36

Download citation

  • DOI: https://doi.org/10.1007/3-540-36580-X_36

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00913-9

  • Online ISBN: 978-3-540-36580-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation