Non-Convex Invariants and Urgency Conditions on Linear Hybrid Automata

Abstract. Linear hybrid automata (LHAs) are of particular interest to formal verification because sets of successor states can be computed exactly, which is not the case in general for more complex dynamics. Enhanced with urgency, LHA can be used to model complex systems from a variety of application domains in a modular fashion. Existing algorithms are limited to convex invariants and urgency conditions that consist of a single constraint. Such restrictions can be a major limitation when the LHA is intended to serve as an abstraction of a model with urgent transitions. This includes deterministic modeling languages such as Matlab-Simulink, Modelica, and Ptolemy, since all their transitions are urgent. The goal of this paper is to remove these limitations, making LHA more directly and easily applicable in practice. We propose an algorithm for successor computation with non-convex invariants and closed, linear urgency conditions. The algorithm is implemented in the open-source tool PHAVer, and illustrated with an example.