Browse ORBi by ORBi project

- Background
- Content
- Benefits and challenges
- Legal aspects
- Functions and services
- Team
- Help and tutorials

Acceleration of Affine Hybrid Transformations Boigelot, Bernard ; ; Mainz, Isabelle 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: 54 (14 ULg)The power of hybrid acceleration Boigelot, Bernard ; 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: 40 (8 ULg)Hybrid Acceleration using Real Vector Automata Boigelot, Bernard ; ; Jodogne, Sébastien 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: 24 (4 ULg) |
||