Static analysis of SPDIs for state-space reduction

摘要

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