Abstract
This paper addresses the exact computation of the set of reachable states of a strongly linear hybrid system. It proposes an approach that is an extension of classical state-space exploration. This approach uses a new operation, based on a cycle analysis in the control graph of the system, for generating sets of reachable states, as well as a powerful representation system for sets of values. The method broadens the range of hybrid systems for which a finite and exact representation of the set of reachable states can be computed. In particular, the state-space exploration may be performed even if the set of variable values reachable at a given control location cannot be expressed as a finite union of convex regions. The technique is illustrated on a very simple example.
“Aspirants” (Research Assistants) for the National Fund for Scientific Research (Belgium)
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, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.
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(1):3–34, 6 February 1995.
R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I, volume 736 of Lecture Notes in Computer Science, pages 209–229. Springer-Verlag, 1993.
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 25 April 1994. Fundamental Study.
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181–201, 1996.
B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Proc. Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1–12, New-Brunswick, NJ, USA, July 1996. Springer-Verlag.
J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL — a tool suite for automatic verification of real-time systems. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, October 1995.
J. R. Büchi. On a decision method in restricted second order arithmetic. In Logic, Methodology and Philosophy of Science, Proceedings of the 1960 International Congress, Stanford, California, 1962. Stanford Univ. Press.
B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Computer Aided Verification, Proc. 6th Int. Conference, Stanford, California, June 1994. Lecture Notes in Computer Science, Springer-Verlag.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In Hybrid Systems HI, Verification and Control, volume 1066 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proceedings of the 1995 IEEE Real-Time Systems Symposium, Pisa, Italy, 1995. IEEE Computer Society Press.
S. Even. Graph Algorithms. Computer Science Press, 1979.
T. A. Henzinger. The theory of hybrid automata. In Proceedings, 11 th Annual IEEE Symposium on Logic in Computer Science, pages 278–292, New Brunswick, New Jersey, 27–30 July 1996. IEEE Computer Society Press.
T.A. Henzinger and P.-H. Ho. Model-checking strategies for linear hybrid systems. Technical Report CSD-TR-94-1437, Cornell University, 1994. Presented at the Seventh International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Austin, TX).
T.A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. In P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, editors, Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 265–293. Springer-Verlag, 1995.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: the next generation. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 56–65. IEEE Computer Society Press, 1995.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HyTech. In E. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, and B. Steffen, editors, TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 41–71. Springer-Verlag, 1995.
T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proceedings of the 27th Annual Symposium on Theory of Computing, pages 373–382. ACM Press, 1995.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994. Special issue for LICS 92.
Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In Proceedings of Workshop on Theory of Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 179–208, Lyngby, Denmark, 1992. Springer-Verlag.
K. G. Larsen, P. Pettersson, and W. Yi. Model-checking for real-time systems. In Horst Reichel, editor, Proceedings of the 10th International Conference on Fundamentals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 62–88, Dresden, Germany, August 1995. Springer-Verlag.
O. Maler and S. Yovine. Hardware timing verification using Kronos. In Proceedings of the IEEE 7th Israeli Conference on Computer Systems and Software Engineering, ICCBSSE'96. IEEE Computer Society Press, 1996.
P. Wolper and B. Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. Static Analysis Symposium, Lecture Notes in Computer Science, Glasgow, September 1995. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boigelot, B., Bronne, L., Rassart, S. (1997). An improved reachability analysis method for strongly linear hybrid systems (extended abstract). In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_18
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive