*Rajeev Alur, Costas Courcoubetis, and
Thomas A. Henzinger*

We develop a theory of equivalences for timed systems. Two systems are equivalent iff external observers cannot observe differences in their behavior. The notion of equivalence depends, therefore, on the distinguishing power of the observers. The power of an observer to measure time results in untimed, clock, and timed equivalences: an untimed observer cannot measure the time difference between events; a clock observer uses a clock to measure time differences with finite precision; a timed observer is able to measure time differences with arbitrary precision.

We show that the distinguishing power of clock observers grows with
the number of observers, and approaches, in the limit, the
distinguishing power of a timed observer. More precisely, given any
equivalence for untimed systems, two timed systems are *k*-clock
congruent, for a nonnegative integer *k*, iff their compositions
with every environment that uses *k* clocks are untimed
equivalent. Both *k*-clock bisimulation congruence and
*k*-clock trace congruence form strict decidable hierarchies that
converge towards the corresponding timed equivalences. Moreover,
*k*-clock bisimulation congruence and *k*-clock trace
congruence provide an adequate and abstract semantics for
branching-time and linear-time logics with *k* clocks.

Our results impact on the verification of timed systems in two ways.
First, our decision procedure for *k*-clock bisimulation
congruence leads to a new, symbolic, decision procedure for timed
bisimilarity. Second, timed trace equivalence is known to be
undecidable. If the number of environment clocks is bounded, however,
then our decision procedure for *k*-clock trace congruence allows
the verification of timed systems in a trace model.

*Proceedings of the
Fifth International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 836,
Springer, 1994, pp. 162-177.

Download inofficial, sometimes updated PostScript / PDF document. © 1994 Springer.