Static Analysis for State-Space Reduction of Polygonal Hybrid Systems

Polygonal hybrid systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as the computation of certain objects of the phase portrait, namely the viability, controllability and invariance kernels, for such systems is decidable. In this paper we show how to compute another object of an SPDI phase portrait, namely semi-separatrix curves and show how the phase portrait can be used for reducing the state-space for optimizing the reachability analysis.

• Type: Conference
• Year: 2006
• Where: FORMATS
• Authors: Gordon J. Pace, Gerardo Schneider
• Keywords: Formal Methods, FORMATS 2006, Phase Portrait, Planar Hybrid Automata, Polygonal Hybrid Systems