---
_id: '4438'
abstract:
- lang: eng
  text: "In temporal-logic model checking, we verify the correctness of a program
    with respect to a desired behavior by checking whether a structure that models
    the program satisfies a temporal-logic formula that specifies the behavior. The
    model-checking problem for the branching-time temporal logic CTL can be solved
    in linear running time, and model-checking tools for CTL are used successfully
    in industrial applications. The development of programs that must meet rigid real-time
    constraints has brought with it a need for real-time temporal logics that enable
    quantitative reference to time. Early research on real-time temporal logics uses
    the discrete domain of the integers to model time. Present research on real-time
    temporal logics focuses on continuous time and uses the dense domain of the reals
    to model time. There, model checking becomes significantly more complicated. For
    example, the model-checking problem for TCTL, a continuous-time extension of the
    logic CTL, is PSPACE-complete.\r\nIn this paper we suggest a reduction from TCTL
    model checking to CTL model checking. The contribution of such a reduction is
    twofold. Theoretically, while it has long been known that model-checking methods
    for untimed temporal logics can be extended quite easily to handle discrete time,
    it was not clear whether and how untimed methods can handle the reset quantifier
    of TCTL, which resets a realvalued clock. Practically, our reduction enables anyone
    who has a tool for CTL model checking to use it for TCTL model checking. The TCTL
    model-checking algorithm that follows from our reduction is in PSPACE, matching
    the known bound for this problem. In addition, it enjoys the wide distribution
    of CTL model-checking tools and the extensive and fruitful research efforts and
    heuristics that have been put into these tools."
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
  by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
  contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
  grant NAG2-892, and by the SRC contract 95-DC-324.036.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
citation:
  ama: 'Henzinger TA, Kupferman O. From quantity to quality. In: <i>Proceedings of
    the 5th International Workshop on Hybrid and Real-Time Systems</i>. Vol 1201.
    Springer; 1997:48-62. doi:<a href="https://doi.org/10.1007/BFb0014712">10.1007/BFb0014712</a>'
  apa: 'Henzinger, T. A., &#38; Kupferman, O. (1997). From quantity to quality. In
    <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>
    (Vol. 1201, pp. 48–62). Grenoble, France: Springer. <a href="https://doi.org/10.1007/BFb0014712">https://doi.org/10.1007/BFb0014712</a>'
  chicago: Henzinger, Thomas A, and Orna Kupferman. “From Quantity to Quality.” In
    <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>,
    1201:48–62. Springer, 1997. <a href="https://doi.org/10.1007/BFb0014712">https://doi.org/10.1007/BFb0014712</a>.
  ieee: T. A. Henzinger and O. Kupferman, “From quantity to quality,” in <i>Proceedings
    of the 5th International Workshop on Hybrid and Real-Time Systems</i>, Grenoble,
    France, 1997, vol. 1201, pp. 48–62.
  ista: 'Henzinger TA, Kupferman O. 1997. From quantity to quality. Proceedings of
    the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid and
    Real-Time Systems, LNCS, vol. 1201, 48–62.'
  mla: Henzinger, Thomas A., and Orna Kupferman. “From Quantity to Quality.” <i>Proceedings
    of the 5th International Workshop on Hybrid and Real-Time Systems</i>, vol. 1201,
    Springer, 1997, pp. 48–62, doi:<a href="https://doi.org/10.1007/BFb0014712">10.1007/BFb0014712</a>.
  short: T.A. Henzinger, O. Kupferman, in:, Proceedings of the 5th International Workshop
    on Hybrid and Real-Time Systems, Springer, 1997, pp. 48–62.
conference:
  end_date: 1997-03-28
  location: Grenoble, France
  name: 'HART: Hybrid and Real-Time Systems'
  start_date: 1997-03-26
date_created: 2018-12-11T12:08:51Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T12:29:48Z
day: '01'
doi: 10.1007/BFb0014712
extern: '1'
intvolume: '      1201'
language:
- iso: eng
month: '01'
oa_version: None
page: 48 - 62
publication: Proceedings of the 5th International Workshop on Hybrid and Real-Time
  Systems
publication_identifier:
  isbn:
  - '9783540626008'
publication_status: published
publisher: Springer
publist_id: '291'
quality_controlled: '1'
scopus_import: '1'
status: public
title: From quantity to quality
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1201
year: '1997'
...
---
_id: '4520'
abstract:
- lang: eng
  text: 'We define robust timed automata, which are timed automata that accept all
    trajectories robustly: if a robust timed automaton accepts a trajectory, then
    it must accept neighboring trajectories also; and if a robust timed automaton
    rejects a trajectory, then it must reject neighboring trajectories also. We show
    that the emptiness problem for robust timed automata is still decidable, by modifying
    the region construction for timed automata. We then show that, like timed automata,
    robust timed automata cannot be determinized. This result is somewhat unexpected,
    given that in temporal logic, the removal of realtime equality constraints is
    known to lead to a decidable theory that is closed under all boolean operations.'
acknowledgement: The first and third author were supported in part by grants from
  ARPA and ONR. The second author was supported in part by the ONR YIP award N00014-95-1-0520,
  by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
  contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
  grant NAG2-892, and by the SRC contract 95-DC-324.036. The third author was also
  supported by the NSF.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Vineet
  full_name: Gupta, Vineet
  last_name: Gupta
- 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: Radha
  full_name: Jagadeesan, Radha
  last_name: Jagadeesan
citation:
  ama: 'Gupta V, Henzinger TA, Jagadeesan R. Robust timed automata. In: <i>Proceedings
    of the 5th International Workshop on Hybrid and Real-Time Systems</i>. Vol 1201.
    Springer; 1997:331-345. doi:<a href="https://doi.org/10.1007/BFb0014736">10.1007/BFb0014736</a>'
  apa: 'Gupta, V., Henzinger, T. A., &#38; Jagadeesan, R. (1997). Robust timed automata.
    In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>
    (Vol. 1201, pp. 331–345). Grenoble, France: Springer. <a href="https://doi.org/10.1007/BFb0014736">https://doi.org/10.1007/BFb0014736</a>'
  chicago: Gupta, Vineet, Thomas A Henzinger, and Radha Jagadeesan. “Robust Timed
    Automata.” In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time
    Systems</i>, 1201:331–45. Springer, 1997. <a href="https://doi.org/10.1007/BFb0014736">https://doi.org/10.1007/BFb0014736</a>.
  ieee: V. Gupta, T. A. Henzinger, and R. Jagadeesan, “Robust timed automata,” in
    <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>,
    Grenoble, France, 1997, vol. 1201, pp. 331–345.
  ista: 'Gupta V, Henzinger TA, Jagadeesan R. 1997. Robust timed automata. Proceedings
    of the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid
    and Real-Time Systems, LNCS, vol. 1201, 331–345.'
  mla: Gupta, Vineet, et al. “Robust Timed Automata.” <i>Proceedings of the 5th International
    Workshop on Hybrid and Real-Time Systems</i>, vol. 1201, Springer, 1997, pp. 331–45,
    doi:<a href="https://doi.org/10.1007/BFb0014736">10.1007/BFb0014736</a>.
  short: V. Gupta, T.A. Henzinger, R. Jagadeesan, in:, Proceedings of the 5th International
    Workshop on Hybrid and Real-Time Systems, Springer, 1997, pp. 331–345.
conference:
  end_date: 1997-03-28
  location: Grenoble, France
  name: 'HART: Hybrid and Real-Time Systems'
  start_date: 1997-03-26
date_created: 2018-12-11T12:09:17Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T09:04:39Z
day: '01'
doi: 10.1007/BFb0014736
extern: '1'
intvolume: '      1201'
language:
- iso: eng
month: '01'
oa_version: None
page: 331 - 345
publication: Proceedings of the 5th International Workshop on Hybrid and Real-Time
  Systems
publication_identifier:
  isbn:
  - '9783540626008'
publication_status: published
publisher: Springer
publist_id: '207'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Robust timed automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1201
year: '1997'
...