Verifying Networks of Timed Processes.
Parosh Abdulla and Bengt Jonsson.
Manuscript, 1997.
Abstract:
Over the last years there has been an increasing research effort
directed towards the automatic verification of infinite state
systems, such as timed automata,
hybrid automata, data-independent systems, relational automata, Petri
nets, and lossy channel systems.
We present a method for deciding reachability properties of networks
of timed processes. Such a network consists of an arbitrary set of
identical timed automata, each with a single real-valued clock.
Using a standard reduction from
safety properties to reachability properties, we can use our
algorithm to decide general safety properties of timed networks.
To our knowledge, this is the first decidability result concerning
verification of systems that are infinite-state in ``two dimentions'':
they contain an arbitrary set of (identical) processes, and
they use infinite data-structures, viz.\ real-valued clocks.
We illustrate our method by showing how it can be used to automatically verify
Fischer's protocol,
a timer-based protocol for enforcing mutual exclusion among an
arbitrary number of processes.
Finally, we show the undecidability of temporal logics, such as
PTL and CTL, for timed networks.
To do that we first prove the undecidability of the {\em recurrent
state problem:} given a state in a timed network, check whether there
is a computation of the network visiting the state infinitely often.
The undecidability result follows immediately, since the recurrent
state problem is expressible in these logics.