Model checking via reachability testing for timed automata

Abstract

In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time property language with clocks. This property language may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every formula φ, a test automaton Tφ, in such a way that checking whether a system S satisfies the property φ can be reduced to a reachability question over the system obtained by making Tφ interact with S.