---
_id: '4614'
abstract:
- lang: eng
text: "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.\r\nWe
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.\r\nOur 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."
acknowledgement: ESPRIT BRA project REACT, National Science Foundation under grant
CCR-9200794, United States Air Force Office of Scientific Research contract F49620-93-1-0056
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Costas
full_name: Courcoubetis, Costas
last_name: Courcoubetis
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Alur R, Courcoubetis C, Henzinger TA. The observational power of clocks. In:
5th International Conference on Concurrency Theory. Vol 836. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 1994:162-177. doi:10.1007/BFb0015008'
apa: 'Alur, R., Courcoubetis, C., & Henzinger, T. A. (1994). The observational
power of clocks. In 5th International Conference on Concurrency Theory
(Vol. 836, pp. 162–177). Uppsala, Sweden: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.1007/BFb0015008'
chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “The Observational
Power of Clocks.” In 5th International Conference on Concurrency Theory,
836:162–77. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994. https://doi.org/10.1007/BFb0015008.
ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “The observational power of
clocks,” in 5th International Conference on Concurrency Theory, Uppsala,
Sweden, 1994, vol. 836, pp. 162–177.
ista: 'Alur R, Courcoubetis C, Henzinger TA. 1994. The observational power of clocks.
5th International Conference on Concurrency Theory. CONCUR: Concurrency Theory,
LNCS, vol. 836, 162–177.'
mla: Alur, Rajeev, et al. “The Observational Power of Clocks.” 5th International
Conference on Concurrency Theory, vol. 836, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 1994, pp. 162–77, doi:10.1007/BFb0015008.
short: R. Alur, C. Courcoubetis, T.A. Henzinger, in:, 5th International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994,
pp. 162–177.
conference:
end_date: 1994-08-25
location: Uppsala, Sweden
name: 'CONCUR: Concurrency Theory'
start_date: 1994-08-22
date_created: 2018-12-11T12:09:46Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T07:41:46Z
day: '01'
doi: 10.1007/BFb0015008
extern: '1'
intvolume: ' 836'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/BFb0015008
month: '01'
oa_version: None
page: 162 - 177
publication: 5th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '3540583297'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '93'
quality_controlled: '1'
status: public
title: The observational power of clocks
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 836
year: '1994'
...