# An improved reachability analysis method for strongly linear hybrid systems (extended abstract)

## 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.

## Keywords

Control Location Hybrid System Reachable State Finite Union Convex Region## References

- [ACD93]R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time.
*Information and Computation*, 104(1):2–34, May 1993.Google Scholar - [ACH+95]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.Google Scholar - [ACHH93]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.Google Scholar - [AD94]R. Alur and D. L. Dill. A theory of timed automata.
*Theoretical Computer Science*, 126(2):183–235, 25 April 1994. Fundamental Study.Google Scholar - [AHH96]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.Google Scholar - [BG96]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.Google Scholar - [BLL+95]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.Google Scholar - [Büc62]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.Google Scholar - [BW94]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.Google Scholar - [DOTY96]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.Google Scholar - [DY95]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.Google Scholar - [Eve79]S. Even.
*Graph Algorithms*. Computer Science Press, 1979.Google Scholar - [Hen96]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.Google Scholar - [HH94]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).Google Scholar
- [HH95]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.Google Scholar - [HHWT95a]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.Google Scholar - [HHWT95b]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.Google Scholar - [HKPV95]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.Google Scholar - [HNSY94]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.Google Scholar - [KPSY92]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.Google Scholar - [LPY95]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.Google Scholar - [MY96]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.Google Scholar - [WB95]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.Google Scholar