Hybrid Acceleration using Real Vector Automata
Abstract:
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 cycles in the automaton control graph. 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.
Keywords:
hybrid systems, acceleration, symbolic representations, real and integer arithmetic, real vector automata.
Download:
Available soon
BibTeX entry:
Available soon