Model Checking via Reachability Testing for Timed Automata

Luca Aceto
Augusto Burgueño
Kim G. Larsen

November 1997


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 logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula tex2html_wrap_inline20, a so-called test automaton tex2html_wrap_inline22 in such a way that checking whether a system S satisfies the property tex2html_wrap_inline20 can be reduced to a reachability question over the system obtained by making tex2html_wrap_inline22 interact with S.

The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in UPPAAL of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version of the ready simulation preorder, for nodes of deterministic, tex2html_wrap_inline32-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.