Reference : Hybrid Acceleration using Real Vector Automata
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
Hybrid Acceleration using Real Vector Automata
Boigelot, Bernard mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Herbreteau, Frédéric [> >]
Jodogne, Sébastien mailto [Centre Hospitalier Universitaire de Liège - CHU > > Radiothérapie >]
Lecture Notes in Computer Science
Computer Aided Verification, 15th International Conference
July 2003
Boulder, CO
[en] hybrid systems ; acceleration
[en] This paper addresses the problem of computing an exact and effective representation of the set of reachable configurations of a linear hybrid automaton. Our solution is based on accelerating the state-space exploration by computing symbolically the repeated effect of control cycles. The computed sets of configurations are represented by Real Vector Automata (RVA), the expressive power of which is beyond that of the first-order additive theory of reals and integers. This approach makes it possible to compute in finite time sets of configurations that cannot be expressed as finite unions of convex sets. The main technical contributions of the paper consist in a powerful sufficient criterion for checking whether a hybrid transformation (i.e., with both discrete and continuous features) can be accelerated, as well as an algorithm for applying such an accelerated transformation on RVA. Our results have been implemented and successfully applied to several case studies, including the well-known leaking gas burner, and a simple communication protocol with timers.
This work was partially funded by a grant of the "Communauté française de Belgique - Direction de la recherche scientifique - Actions de recherche concertées", and by the European IST-FET project ADVANCE (IST-1999-29082).
The original publication is available at

File(s) associated to this reference

Fulltext file(s):

Open access
BHJ03.pdfAuthor preprint225.54 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.