An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems

This paper addresses the exact computation of the set of reachable
states of a linear hybrid system. It proposes an approach that is an
extension of classical state-space exploration. This approach uses a
new operation, based on a cycle analysis in the control graph of the
system, for generating sets of reachable states, as well as a powerful
representation system for sets of values. The method broadens the
range of hybrid systems for which a finite and exact representation of
the set of reachable states can be computed. In particular, the
state-space exploration may be performed even if the set of variable
values reachable at a given control location cannot be expressed as a
finite union of convex regions. The technique is illustrated on a
very simple example.