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