[en] This paper addresses the problem of computing symbolically the set of reachable configurations of a linear hybrid automaton. A solution proposed in earlier work consists in exploring the reachable configurations using an acceleration operator for computing the iterated effect of selected control cycles. Unfortunately, this method imposes a periodicity requirement on the data transformations labeling these cycles, that is not always satisfied in practice. This happens in particular with the important subclass of timed automata, even though it is known that the paths of such automata have a periodic behavior. The goal of this paper is to broaden substantially the applicability of hybrid acceleration. This is done by introducing powerful reduction rules, aimed at translating hybrid data transformations into equivalent ones that satisfy the periodicity criterion. In particular, we show that these rules always succeed in the case of timed automata. This makes it possible to compute an exact symbolic representation of the set of reachable configurations of a linear hybrid automaton, with a guarantee of termination over the subclass of timed automata. Compared to other known solutions to this problem, our method is simpler, and applicable to a much larger class of systems.
Disciplines :
Computer science
Author, co-author :
Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Herbreteau, Frédéric; Laboratoire Bordelais de Recherche en Informatique (LaBRI)
Language :
English
Title :
The power of hybrid acceleration
Publication date :
2006
Event name :
18th International Conferencence on Computer-Aided Verification
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
[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, 1995.
[BBR97] B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In Proceedings of the 9th Int. Conf. on Computer-Aided Verification (CAV'97), volume 1254 of Lecture Notes in Computer Science, pages 167-177. Springer-Verlag, 1997.
[BHJ03] B. Boigelot, F. Herbreteau, and S. Jodogne. Hybrid acceleration using real vector automata. In Proc. of the 15th Int. Conf. on Computer-Aided Verification (CAV'03), volume 2725 of Lecture Notes in Computer Science, pages 193-205. Springer-Verlag, 2003.
[BJW05] B. Boigelot, S. Jodogne, and P. Wolper. An effective decision procedure for linear arithmetic with integer and real variables. ACM Transactions on Computational Logic (TOCL), 6(3):614-633, 2005.
[BLFP03] S. Bardin, J. Leroux, A. Finkel, and L. Petrucci. FAST: Fast accelereation of symbolic transition systems. In Proc. 15th Int. Conf. on Computer-Aided Verification, volume 2725 of Lect. Notes in Comp. Sc., pages 118-121, 2003.
[BLR05] P. Bouyer, F. Laroussinie, and P.-A. Reynier. Diagonal constraints in timed automata: Forward analysis of timed systems. In Proc. of the 3rd Int. Conf. on Formal Modelling and Analysis of Timed Systems, volume 3829 of Lecture Notes in Computer Science, pages 112-126. Springer-Verlag, 2005.
[Boi98] B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Université de Liège, 1998.
[Bou03] P. Bouyer. Untameable timed automata! In Proc. of 20th Ann. Symp. Theoretical Aspects of Computer Science (STACS'03), Lecture Notes in Computer Science, Berlin, Germany, 2003. Springer-Verlag.
[BY03] J. Bengtsson and W. Yi. On clock difference constraints and termination in reachability analysis of timed automata. In Proc. of 5th Int. Conf. on Formal Engineering Methods (ICFEM'03), volume 2885 of Lecture Notes in Computer Science, pages 491-503, 2003.
[CJ98] H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In Proc. of 10th Int. Conf. on Computer-Aided Verification (CAV'98), volume 1427 of Lecture Notes in Computer Science, pages 268-279. Springer-Verlag, 1998.
[CJ99] H. Comon and Y. Jurski. Timed automata and the theory of real numbers. In Proc. 10th Int. Conf. Concurrency Theory (CONCUR'99), volume 1664 of Lecture Notes in Computer Science, pages 242-257. Springer-Verlag, 1999.
[Fri98] L. Fribourg. A closed-form evaluation for extended timed automata. Research Report LSV-98-2, LSV, March 1998.
[Hen96] T. A. Henzinger. The theory of hybrid automata. In Proc. 11th Annual Symp. on Logic in Computer Science (LICS), pages 278-292. IEEE Computer Society Press, 1996.
[LASH] The Liège Automata-based Symbolic Handler (LASH). Available at : http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.
[Rev93] P. Z. Revesz. A closed-form evaluation for datalog queries with integer (gap)-order constraints. Theor. Comp. Sc., 116(1&2):117-149, 1993.
[Wei99] V. Weispfenning. Mixed real-integer linear quantifier elimination. In ISSAC: Proceedings of the ACM SIGSAM Int. Symp. on Symbolic and Algebraic Computation, pages 129-136, Vancouver, 1999. ACM Press.
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.