--- _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' ...