A decidable class of planar linear hybrid systems

In this paper, we show the decidability of a new subclass of linear hybrid automata. These automata are planar, that is, consist of two state variables, monotonic along some direction in the plane and have identity resets, that is, the values of the continuous variables are not reset to a different value on a discrete transition. Our proof uses a combination of a tree construction capturing the edge-to-edge reachability and a finite bisimulation construction. Our class strictly contains the class of two dimensional piecewise constant derivative systems for which decidability of the reachability problem is known.