## The Observational Power of Clocks

*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.

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