The power of reachability testing for timed automata

The computational engine of the verification tool U consists of a collection of efficient algorithms for the analysis of reachability properties of systems. Model-checking of properties other than plain reachability ones may currently be carried out in such a tool as follows. Given a property φ to model-check, the user must provide a test automaton T_φ for it. This test automaton must be such that the original system S has the property expressed by φ precisely when none of the distinguished reject states of T_φ can be reached in the synchronized parallel composition of S with T_φ. This raises the question of which properties may be analysed by U in such a way. This paper gives an answer to this question by providing a complete characterization of the class of properties for which model-checking can be reduced to reachability testing in the sense outlined above. This result is obtained as a corollary of a stronger statement pertaining to the compositionality of the property language considered in this study. In particular, it is shown that our language is the least expressive compositional language that can express a simple safety property stating that no reject state can ever be reached.

Finally, the property language characterizing the power of reachability testing is used to provide a definition of characteristic properties with respect to a timed version of the ready simulation preorder, for nodes of τ-free, deterministic timed automata.