Abstract
Hybrid systems are systems that exhibit both discrete and continuous behavior. Reachability, the question of whether a system in one state can reach some other state, is undecidable for hybrid systems in general. The Generalized Polygonal Hybrid System (GSPDI) is a restricted form of hybrid automaton where reachability is decidable. It is limited to two continuous variables that uniquely determine which location the automaton is in, and restricted in that the discrete transitions does not allow changes in the state, only the location, of the automaton. One application of GSPDIs is for approximating control systems and verifying the safety of such systems.
In this paper we present the following two contributions: i) An optimized algorithm that answers reachability questions for GSPDIs, where all cycles in the reachability graph are accelerated. ii) An algorithm by which more complex planar hybrid systems are over-approximated by GSPDIs subject to two measures of precision. We prove soundness, completeness, and termination of both algorithms, and discuss their implementation.