---
_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:
    <i>5th International Conference on Concurrency Theory</i>. Vol 836. Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik; 1994:162-177. doi:<a href="https://doi.org/10.1007/BFb0015008">10.1007/BFb0015008</a>'
  apa: 'Alur, R., Courcoubetis, C., &#38; Henzinger, T. A. (1994). The observational
    power of clocks. In <i>5th International Conference on Concurrency Theory</i>
    (Vol. 836, pp. 162–177). Uppsala, Sweden: Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik. <a href="https://doi.org/10.1007/BFb0015008">https://doi.org/10.1007/BFb0015008</a>'
  chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “The Observational
    Power of Clocks.” In <i>5th International Conference on Concurrency Theory</i>,
    836:162–77. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994. <a href="https://doi.org/10.1007/BFb0015008">https://doi.org/10.1007/BFb0015008</a>.
  ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “The observational power of
    clocks,” in <i>5th International Conference on Concurrency Theory</i>, 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.” <i>5th International
    Conference on Concurrency Theory</i>, vol. 836, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 1994, pp. 162–77, doi:<a href="https://doi.org/10.1007/BFb0015008">10.1007/BFb0015008</a>.
  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'
...
---
_id: '4615'
abstract:
- lang: eng
  text: We introduce the class of event- recording timed automata (ERA). An event-recording
    automaton contains, for every event a, a clock that records the time of the last
    occurrence of a. The class ERA is, on one hand, expressive enough to model (finite)
    timed transition systems and, on the other hand, determinizable and closed under
    all boolean operations. As a result, the language inclusion problem is decidable
    for event-recording automata. We present a translation from timed transition systems
    to event-recording automata, which leads to an algorithm for checking if two timed
    transition systems have the same set of timed behaviors. We also consider event-predicting
    timed automata (EPA), which contain clocks that predict the time of the next occurrence
    of an event. The class of event-clock automata (ECA), which contain both event-recording
    and event-predicting clocks, is a suitable specification language for real-time
    properties. We provide an algorithm for checking if a timed automaton meets a
    specification that is given as an event-clock automaton.
acknowledgement: "Supported in part by the Office of Naval Research under contract
  N00014-91-J-1219, the National Science Foundation under grant CCR-8701103, and by
  DARPA/NSF under grant CCR-9014363.\r\nSupported in part by the National Science
  Foundation under grant CCR-9200794 and by the United States Air Force Office of
  Scientific Research under 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: Limor
  full_name: Fix, Limor
  last_name: Fix
- 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, Fix L, Henzinger TA. A determinizable class of timed automata. In:
    <i>International Conference on Computer Aided Verification</i>. Vol 818. Springer;
    1994:1-13. doi:<a href="https://doi.org/10.1007/3-540-58179-0_39">10.1007/3-540-58179-0_39</a>'
  apa: 'Alur, R., Fix, L., &#38; Henzinger, T. A. (1994). A determinizable class of
    timed automata. In <i>International Conference on Computer Aided Verification</i>
    (Vol. 818, pp. 1–13). Stanford, CA, United States of America: Springer. <a href="https://doi.org/10.1007/3-540-58179-0_39">https://doi.org/10.1007/3-540-58179-0_39</a>'
  chicago: Alur, Rajeev, Limor Fix, and Thomas A Henzinger. “A Determinizable Class
    of Timed Automata.” In <i>International Conference on Computer Aided Verification</i>,
    818:1–13. Springer, 1994. <a href="https://doi.org/10.1007/3-540-58179-0_39">https://doi.org/10.1007/3-540-58179-0_39</a>.
  ieee: R. Alur, L. Fix, and T. A. Henzinger, “A determinizable class of timed automata,”
    in <i>International Conference on Computer Aided Verification</i>, Stanford, CA,
    United States of America, 1994, vol. 818, pp. 1–13.
  ista: 'Alur R, Fix L, Henzinger TA. 1994. A determinizable class of timed automata.
    International Conference on Computer Aided Verification. CAV: Computer Aided Verification,
    LNCS, vol. 818, 1–13.'
  mla: Alur, Rajeev, et al. “A Determinizable Class of Timed Automata.” <i>International
    Conference on Computer Aided Verification</i>, vol. 818, Springer, 1994, pp. 1–13,
    doi:<a href="https://doi.org/10.1007/3-540-58179-0_39">10.1007/3-540-58179-0_39</a>.
  short: R. Alur, L. Fix, T.A. Henzinger, in:, International Conference on Computer
    Aided Verification, Springer, 1994, pp. 1–13.
conference:
  end_date: 1994-06-23
  location: Stanford, CA, United States of America
  name: 'CAV: Computer Aided Verification'
  start_date: 1994-06-21
date_created: 2018-12-11T12:09:46Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-01T14:37:25Z
day: '01'
doi: 10.1007/3-540-58179-0_39
extern: '1'
intvolume: '       818'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-58179-0_39
month: '01'
oa_version: None
page: 1 - 13
publication: International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540484691'
publication_status: published
publisher: Springer
publist_id: '92'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A determinizable class of timed automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 818
year: '1994'
...
---
_id: '4617'
abstract:
- lang: eng
  text: 'We extend the timed-automaton model for real-time systems [AD90] to a formal
    model for hybrid systems: while the continuous variables of a timed automaton
    are clocks that measure time, the continuous variables of a hybrid system are
    governed by arbitrary differential equations. We then adopt the verification methodology
    for timed automata [ACD90, ACD+92, HNSY92] to analyze hybrid systems: while the
    verification problem is decidable for timed automata, we obtain semidecision procedures
    for the class of hybrid systems whose continuous variables change in a piecewise
    linear fashion. '
alternative_title:
- LNCIS
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
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
- first_name: Xavier
  full_name: Nicollin, Xavier
  last_name: Nicollin
- first_name: Alfredo
  full_name: Olivero, Alfredo
  last_name: Olivero
- first_name: Joseph
  full_name: Sifakis, Joseph
  last_name: Sifakis
- first_name: Sergio
  full_name: Yovine, Sergio
  last_name: Yovine
citation:
  ama: 'Alur R, Courcoubetis C, Henzinger TA, et al. The algorithmic analysis of hybrid
    systems. In: <i>11th International Conference on Analysis and Optimization of
    Systems Discrete Event Systems</i>. Vol 199. Springer; 1994:331-351. doi:<a href="https://doi.org/10.1007/BFb0033565">10.1007/BFb0033565</a>'
  apa: 'Alur, R., Courcoubetis, C., Henzinger, T. A., Ho, P., Nicollin, X., Olivero,
    A., … Yovine, S. (1994). The algorithmic analysis of hybrid systems. In <i>11th
    International Conference on Analysis and Optimization of Systems Discrete Event
    Systems</i> (Vol. 199, pp. 331–351). Sophia-Antipolis, France: Springer. <a href="https://doi.org/10.1007/BFb0033565">https://doi.org/10.1007/BFb0033565</a>'
  chicago: Alur, Rajeev, Costas Courcoubetis, Thomas A Henzinger, Pei Ho, Xavier Nicollin,
    Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The Algorithmic Analysis
    of Hybrid Systems.” In <i>11th International Conference on Analysis and Optimization
    of Systems Discrete Event Systems</i>, 199:331–51. Springer, 1994. <a href="https://doi.org/10.1007/BFb0033565">https://doi.org/10.1007/BFb0033565</a>.
  ieee: R. Alur <i>et al.</i>, “The algorithmic analysis of hybrid systems,” in <i>11th
    International Conference on Analysis and Optimization of Systems Discrete Event
    Systems</i>, Sophia-Antipolis, France, 1994, vol. 199, pp. 331–351.
  ista: 'Alur R, Courcoubetis C, Henzinger TA, Ho P, Nicollin X, Olivero A, Sifakis
    J, Yovine S. 1994. The algorithmic analysis of hybrid systems. 11th International
    Conference on Analysis and Optimization of Systems Discrete Event Systems. ICAOS:
    Analysis and Optimization of Systems - Discrete-Event Systems, LNCIS, vol. 199,
    331–351.'
  mla: Alur, Rajeev, et al. “The Algorithmic Analysis of Hybrid Systems.” <i>11th
    International Conference on Analysis and Optimization of Systems Discrete Event
    Systems</i>, vol. 199, Springer, 1994, pp. 331–51, doi:<a href="https://doi.org/10.1007/BFb0033565">10.1007/BFb0033565</a>.
  short: R. Alur, C. Courcoubetis, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero,
    J. Sifakis, S. Yovine, in:, 11th International Conference on Analysis and Optimization
    of Systems Discrete Event Systems, Springer, 1994, pp. 331–351.
conference:
  end_date: 1994-06-17
  location: Sophia-Antipolis, France
  name: 'ICAOS: Analysis and Optimization of Systems - Discrete-Event Systems'
  start_date: 1994-06-15
date_created: 2018-12-11T12:09:46Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-01T14:14:31Z
day: '01'
doi: 10.1007/BFb0033565
extern: '1'
intvolume: '       199'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/BFb0033565
month: '01'
oa_version: None
page: 331 - 351
publication: 11th International Conference on Analysis and Optimization of Systems
  Discrete Event Systems
publication_identifier:
  isbn:
  - 978-3-540-19896-3
publication_status: published
publisher: Springer
publist_id: '91'
quality_controlled: '1'
status: public
title: The algorithmic analysis of hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 199
year: '1994'
...