Algorithmic analysis of polygonal hybrid systems, part I: Reachability

In this work we are concerned with the formal verification of two-dimensional non-deterministic hybrid systems, namely polygonal differential inclusion systems (SPDIs). SPDIs are a class of non-deterministic systems that correspond to piecewise constant differential inclusions on the plane, for which we study the reachability problem.Our contribution is the development of an algorithm for solving exactly the reachability problem of SPDIs. We extend the geometric approach due to Maler and Pnueli [O. Maler, A. Pnueli. Reachability analysis of planar multi-linear systems. in: C. Courcoubetis (Ed.), CAV’93, in: LNCS, vol. 697, Springer-Verlag, 1993, pp. 194–209] to non-deterministic systems, based on the combination of three techniques: the representation of the two-dimensional continuous-time dynamics as a one-dimensional discrete-time system (using Poincaré maps), the characterization of the set of qualitative behaviors of the latter as a finite set of types of signatures, and acceleration used to explore reachability according to each of these types.