Automata-based Representations for the Verification of Hybrid Systems
Sébastien Jodogne, Summer School Modelling and Verification of Parallel Processes (MOVEP) · ORBi (University of Liège) · 2002
This paper addresses the reachability problem for linear hybrid systems. We show that this problem can be solved using automata-based symbolic representations for the configurations of such systems, leading to a simple analysis technique. We then argue that those representations can be used for verifying linear hybrid systems whose set of reachable configurations cannot be expressed as a finite union of convex polyhedra.