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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere, and George J. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88:971–984, 2000.
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.
A. Bemporad and M. Morari. Control of systems integrating logic, dynamics and constraints. Automatica, 35(3):407–427, 1999.
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.
P. Brunovsky. A classification of linear controllable systems. Kybernetika, 6(3):173–188, 1970.
Edmund M. M. Clarke, Doron Peled, and Orna Grumberg. Model Checking. MIT Press, 1999.
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.
E. A. Emerson. Handbook of Theoretical Computer Science, volume B, chapter Temporal and modal logic, pages 995–1072. Elsevier Science, 1990.
E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.
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.
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.
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.
R. E. Kalman. Kronecker invariants and feedback. In L. Weiss, editor, Ordinary Differential Equations, pages 459–471. Academic Press, New York, 1972.
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.
Gerardo Lafferriere, George J. Pappas, and Shankar Sastry. O-minimal hybrid systems. Mathematics of Control, Signals and Systems, 13(1):1–21, March 2000.
P. Madhusudan and P.S. Thiagarajan. Branching time controllers for discrete event systems. Theoretical Computer Science, 274:117–149, March 2002.
Z. Manna and P. Wolper. Synthesis of communication processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6:68–93, 1984.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
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.
eorge J. Pappas. Bisimilar linear systems. Automatica, 2001. To appear.
D.M.R. Park. Concurrency and automata on infinite sequences, volume 104 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular inclusions. In Computer Aided Verification, pages 95–104, 1994.
Eduardo D. Sontag. Mathematical Control Theory, volume 6 of Texts in Applied Mathematics. Springer-Verlag, New-York, 2nd edition, 1998.
Colin Stirling. Handbook of logic in computer science, volume 2, chapter Modal and Temporal Logics, pages 477–563. Oxford University Press, 1992.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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