Acceleration of affine hybrid transformations

Isabelle Mainz
ULG
Friday, 28 November, 2014 - 16:00
Forum D

In this talk I will speak about 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. I will present 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.