Model-checking for hybrid systems by quotienting and constraints solving

Abstract

In this paper we present a semi-algorithm to do compositional model-checking for hybrid systems. We first define a modal logic Lhν which is expressively complete for linear hybrid automata. We then show that it is possible to extend the result on compositional model- checking for parallel compositions of finite automata and networks of timed automata to linear hybrid automata. Finally we present some results obtained with an extension of the tool CMC to handle a subclass of hybrid automata (the stopwatch automata).