Abstract: Current tools for verifying linear hybrid automata require the specification to be given either in terms of reachable states or in a temporal logic. This talk discusses verification in the framework of simulation relations, in which the specification is itself an automaton. That approach allows for checking abstraction or refinement, the compact and intuitive description of properties that might require recursive formulas in temporal logic, and compositional techniques based on preorders.

The simulation of hybrid automata requires a notion of equivalence between continuous states. We present a semi-algorithm for computing the simulation relation of linear hybrid automata with an equivalence relation given by linear constraints. This generality comes at the price of high complexity and requires operations in a continuous space with a dimension three times larger than that of the automata. For practical application, we suggest a strict continuous simulation in which the continuous states of the automaton and the specification are to be identical. While this leads to a loss in expressiveness, it operates on the same state space as the automaton and permits compositional verification. For this purpose, we propose a novel algorithm for solving simulation relations of finite labeled transition systems and extend it to strict simulation of deterministic linear hybrid automata. It is applied to verify linear hybrid automata by quotienting, where the modules of the automaton are successively combined with the specification. Other possible applications of simulation solving include the generation of assumptions for assume-guarantee reasoning and the design of controllers. The approach is demonstrated on a mutual exclusion protocol and a train-gate-controller.

CV: Goran Frehse is a PhD student from the Process Control Laboratory at the Department of Biochemical and Chemical Engineering of Dortmund University, Germany. His research interests are in the compositional verification of hybrid automata and in applying simulation relations in modeling and verification. He is also interested in the optimal control of hybrid systems. He holds a diploma in Electrical Engineering and Information Technology from the University of Karlsruhe, Germany. He can be contacted on goran.frehse@gmx.de.