Abstract
An important case of hybrid systems are the rectangular automata. First, rectangular dynamics can naturally and arbitrarily closely approximate more general, nonlinear dynamics. Second, rectangular automata are the most general type of hybrid systems for which model checking -in particular, Ltl model checking- is decidable. However, on one hand, the original proofs of decidability did not suggest practical algorithms and, on the other hand, practical symbolic model-checking procedures -such as those implemented in HyTech- were not known to terminate on rectangular automata. We remedy this unsatisfactory situation: we present a symbolic method for Ltl model checking which can be performed by HyTech and is guaranteed to terminate on all rectangular automata. We do so by proving that our method for symbolic Ltl model checking terminates on an infinite-state transition system if the trace-equivalence relation of the system has finite index, which is the case for all rectangular automata.
This research was supported in part by the DARPA (NASA) grant NAG2-1214, the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660, the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995. 142, 152
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994. 144, 146, 152
R. Alur and T.A. Henzinger. Real-time system = discrete system + clock variables. Software Tools for Technology Transfer, 1:86–109, 1997. 153
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In Proceedings of the 14th Annual Real-time Systems Symposium, pages 2–11. IEEE Computer Society Press, 1993. 152
G. Bhat and R. Cleaveland. Efficient local model-checking for fragments of the modal μ-calculus. In TACAS96: Tools and Algorithms for Construction and Analysis of Systems, LNCS 1055, pages 107–126. Springer-Verlag, 1996. 148
G. Bhat and R. Cleaveland. Efficient model checking via the equational μ-calculus. In Proceedings of the 11th Annual Symposium on Logic in Computer Science, pages 304–312. IEEE Computer Society Press, 1996. 143, 149
A. Bouajjani, J.-C. Fernandez, and N. Halbwachs. Minimal model generation. In CAV 90: Computer-aided Verification, LNCS 663, pages 197–203. Springer-Verlag, 1990. 145
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992. 147
E.M. Clarke, O. Grumberg, and D.E. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency: Reflections and Perspectives, LNCS 803, pages. Springer-Verlag, 1994. 143, 150
R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for the modal μ-calculus. In CAV 92: Computer-aided Verification, LNCS 663, pages 410–422. Springer-Verlag, 1993. 149
J.C. Corbett. Timing analysis of Ada tasking programs. IEEE Transactions on Software Engineering, 22:461–483, 1996. 142
M. Dam. Ctl* and Ectl* as fragments of the modal μ-calculus. Theoretical Computer Science, 126:77–96, 1994. 143, 149
C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In TACAS98: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1384, pages 313–329. Springer-Verlag, 1998. 143
E.A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier Science Publishers, 1990. 146, 147, 150
E.A. Emerson, C.S. Jutla, and A.P. Sistla. On model checking for fragments of μ-calculus. In CAV 93: Computer-aided Verification, LNCS 697, pages 385–396. Springer-Verlag, 1993. 143, 148, 149
E.A. Emerson and C. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Proceedings of the 1st Annual Symposium on Logic in Computer Science, pages 267–278. IEEE Computer Society Press, 1986. 143
T.A. Henzinger. Hybrid automata with finite bisimulations. In ICALP 95: Automata, Languages, and Programming, LNCS 944, pages 324–335. Springer-Verlag, 1995. 144, 152
T.A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual Symposium on Logic in Computer Science, pages 278–292. IEEE Computer Society Press, 1996. 146, 147
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1:110–122, 1997. 143, 152
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control, 43:540–554, 1998. 142
T.A. Henzinger, B. Horowitz, and R. Majumdar. Rectangular hybrid games. In CONCUR 99: Concurrency Theory, LNCS 1664, pages 320–335, 1999. 153
T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57:94–124, 1998. 142, 143, 151, 152, 153
T.A. Henzinger and R. Majumdar. A classification of symbolic transition systems. In STACS 2000: Theoretical Aspects of Computer Science, LNCS. Springer-Verlag, 2000. 145
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings of the 7th Annual Symposium on Logic in Computer Science, pages 394–406. IEEE Computer Society Press, 1992. 152
T.A. Henzinger and H. Wong-Toi. Using HyTech to synthesize control parameters for a steam boiler. In Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, pages 265–282. Springer-Verlag, 1996. 142
P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In CAV 95: Computer-aided Verification, LNCS 939, pages 381–394. Springer-Verlag, 1995. 142
P.C. Kanellakis and S.A. Smolka. Ccs expressions, finite-state processes, and three problems of equivalence. Information and Computation, 86:43–68, 1990. 144, 145
J. Kosecka, C.J. Tomlin, G. Pappas, and S. Sastry. Generation of conflict resolution manoeuvres for air traffic management. In IROS 97: International Conference on Intelligent Robot and Systems, volume 3, pages 1598–1603. IEEE Press, 1997. 142
S. Nadjm-Tehrani and J.-E. Strömberg. Proving dynamic properties in an aerospace application. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 2–10. IEEE Computer Society Press, 1995. 142
T. Stauner, O. Müller, and M. Fuchs. Using HyTech to verify an automotive control system. In HART 97: Hybrid and Real-time Systems, LNCS 1201, pages 139–153. Springer-Verlag, 1997. 142
W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B, pages 133–191. Elsevier Science Publishers, 1990. 150
T. Villa, H. Wong-Toi, A. Balluchi, J. Preußig, A. Sangiovanni-Vincentelli, and Y. Watanabe. Formal verification of an automotive engine controller in cutoff mode. In Proceedings of the 37th Conference on Decision and Control. IEEE Press, 1998. 142
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Majumdar, R. (2000). Symbolic Model Checking for Rectangular Hybrid Systems. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_11
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive