A new abstraction-refinement based verifier for modular linear hybrid automata and its implementation

A concurrent linear hybrid automaton is composed of a set of linear hybrid automata and is used to model linear hybrid systems. Each component´s behavior exhibits both discrete and continuous dynamics. We have developed LhaVrf, a symbolic verifier for the reachability verification of concurrent linear hybrid automata. The implementation is based on the algorithm proposed in S. Jiang´s papers. In his paper, reachability problem of linear hybrid automata was first reduced to one for linear transition systems, whose reachability analysis was then performed by using counterexample fragment based specification relaxation. S. Jiang proposed in another paper further enhancement in efficiency in context of concurrent systems, where for each counterexample fragment, a minimal conflicting constraints set was identified (that makes the fragment invalid), and used for specification relaxation. We adopted the above key ideas in the implementation of LhaVrf, with added features such as it automatically composes the concurrent subsystem models. Whenever the reachability to an unsafe state is satisfied, the output provides a concrete counterexample with values assigned to the variables. The LhaVrf is illustrated via an application to the Fischer mutual exclusion protocol.