References of "Herbreteau, Frédéric"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailThe power of hybrid acceleration
Boigelot, Bernard ULg; Herbreteau, Frédéric

in Lecture Notes in Computer Science (2006), 4144

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 29 (5 ULg)
Full Text
Peer Reviewed
See detailHybrid Acceleration using Real Vector Automata
Boigelot, Bernard ULg; Herbreteau, Frédéric; Jodogne, Sébastien ULg

in Lecture Notes in Computer Science (2003, July), 2725

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 15 (3 ULg)