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 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 
, a so-called
test automaton 
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 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, 
-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.