References of "Herbreteau, Frédéric"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailAcceleration of Affine Hybrid Transformations
Boigelot, Bernard ULg; Herbreteau, Frédéric; Mainz, Isabelle ULg

in Lecture Notes in Computer Science (2014), 8837

This work addresses the computation of the set of reachable configurations of linear hybrid automata. The approach relies on symbolic state-space exploration, using acceleration in order to speed up the ... [more ▼]

This work addresses the computation of the set of reachable configurations of linear hybrid automata. The approach relies on symbolic state-space exploration, using acceleration in order to speed up the computation and to make it terminate for a broad class of systems. Our contribution is an original method for accelerating the control cycles of linear hybrid automata, i.e., to compute their unbounded repeated effect. The idea consists in analyzing the data transformations that label these cycles, by reasoning about the geometrical features of the corresponding system of linear constraints. This approach is complete over Multiple Counters Systems (MCS), and is able to accelerate hybrid transformations that are out of scope of existing techniques. [less ▲]

Detailed reference viewed: 16 (3 ULg)
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: 35 (8 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: 17 (4 ULg)