Verification of temporal properties on hybrid automata by simulation relations
Alessandro D’Innocenzo, A. Agung Julius, George J. Pappas, Maria Domenica Di Benedetto, S. Di Gennaro · 2007
Model checking can be used to verify temporal properties of hybrid automata. However, model checking is not decidable in general. We overcome this difficulty by considering a durational graph abstraction, for which model checking is decidable. The contribution of this paper is to show that, given a hybrid automaton and the durational graph abstraction, there exists a simulation relation between the two systems. This approach allows checking properties such as safety, but also timing properties of hybrid automata. We apply our framework to a relevant case study in the context of air traffic management (ATM). For an extended version of this paper refer to [A. D'Innocenzo et al., 2007].