real-vector automata; linear hybrid systems; infinite-state systems
Abstract :
[en] This paper addresses the exact computation of the set of reachable
states of a 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.
Disciplines :
Computer science
Author, co-author :
Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Bronne, Louis
Rassart, Stéphane
Language :
English
Title :
An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems
Publication date :
1997
Event name :
Computer Aided Verification, 9th International Conference (CAV'97)
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Bibliography
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2-34, May 1993.
R. Atur, 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, N J, USA, July 1996. Springer-Verlag.
J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL-_9 tool suite for automatic verification of real-time systems. In Proceedings of the 4th DIMA CS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, October 1995.
J. R. Biichi. 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 Ill, Verification and Control, volume 1066 of Lecture Notes in Computer Science. Springer-Vedag, 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, CorneU 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 CorneU Hybrid Technology Tool. In P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, editors, Hybrid Systems 1I, 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. Purl, 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 lOth 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, 1CCBSSE'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.
Similar publications
Sorry the service is unavailable at the moment. Please try again later.
This website uses cookies to improve user experience. Read more
Save & Close
Accept all
Decline all
Show detailsHide details
Cookie declaration
About cookies
Strictly necessary
Performance
Strictly necessary cookies allow core website functionality such as user login and account management. The website cannot be used properly without strictly necessary cookies.
This cookie is used by Cookie-Script.com service to remember visitor cookie consent preferences. It is necessary for Cookie-Script.com cookie banner to work properly.
Performance cookies are used to see how visitors use the website, eg. analytics cookies. Those cookies cannot be used to directly identify a certain visitor.
Used to store the attribution information, the referrer initially used to visit the website
Cookies are small text files that are placed on your computer by websites that you visit. Websites use cookies to help users navigate efficiently and perform certain functions. Cookies that are required for the website to operate properly are allowed to be set without your permission. All other cookies need to be approved before they can be set in the browser.
You can change your consent to cookie usage at any time on our Privacy Policy page.
