---
_id: '4603'
abstract:
- lang: eng
  text: Alternating transition systems are a general model for composite systems which
    allow the study of collaborative as well as adversarial relationships between
    individual system components. Unlike in labeled transition systems, where each
    transition corresponds to a possible step of the system (which may involve some
    or all components), in alternating transition systems, each transition corresponds
    to a possible move in a game between the components. In this paper, we study refinement
    relations between alternating transition systems, such as “Does the implementation
    refine the set A of specification components without constraining the components
    not in A?” In particular, we generalize the definitions of the simulation and
    trace containment preorders from labeled transition systems to alternating transition
    systems. The generalizations are called alternating simulation and alternating
    trace containment. Unlike existing refinement relations, they allow the refinement
    of individual components within the context of a composite system description.
    We show that, like ordinary simulation, alternating simulation can be checked
    in polynomial time using a fixpoint computation algorithm. While ordinary trace
    containment is PSPACE-complete, we establish alternating trace containment to
    be EXPTIME-complete. Finally, we present logical characterizations for the two
    preorders in terms of ATL, a temporal logic capable of referring to games between
    system components.
acknowledgement: This work is supported in part by the ONR YIP award N00014-95-1-0520,
  by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9504469, CCR-9628400,
  and CCR-9700061, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341,
  by the SRC contract 97-DC-324.041, and by a grant from the Intel Corporation.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- 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
- first_name: Moshe
  full_name: Vardi, Moshe
  last_name: Vardi
citation:
  ama: 'Alur R, Henzinger TA, Kupferman O, Vardi M. Alternating refinement relations.
    In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>.
    Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:163-178. doi:<a
    href="https://doi.org/10.1007/BFb0055622">10.1007/BFb0055622</a>'
  apa: 'Alur, R., Henzinger, T. A., Kupferman, O., &#38; Vardi, M. (1998). Alternating
    refinement relations. In <i>Proceedings of the 9th Interantional Conference on
    Concurrency Theory</i> (Vol. 1466, pp. 163–178). Nice, France: Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/BFb0055622">https://doi.org/10.1007/BFb0055622</a>'
  chicago: Alur, Rajeev, Thomas A Henzinger, Orna Kupferman, and Moshe Vardi. “Alternating
    Refinement Relations.” In <i>Proceedings of the 9th Interantional Conference on
    Concurrency Theory</i>, 1466:163–78. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    1998. <a href="https://doi.org/10.1007/BFb0055622">https://doi.org/10.1007/BFb0055622</a>.
  ieee: R. Alur, T. A. Henzinger, O. Kupferman, and M. Vardi, “Alternating refinement
    relations,” in <i>Proceedings of the 9th Interantional Conference on Concurrency
    Theory</i>, Nice, France, 1998, vol. 1466, pp. 163–178.
  ista: 'Alur R, Henzinger TA, Kupferman O, Vardi M. 1998. Alternating refinement
    relations. Proceedings of the 9th Interantional Conference on Concurrency Theory.
    CONCUR: Concurrency Theory, LNCS, vol. 1466, 163–178.'
  mla: Alur, Rajeev, et al. “Alternating Refinement Relations.” <i>Proceedings of
    the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–78, doi:<a href="https://doi.org/10.1007/BFb0055622">10.1007/BFb0055622</a>.
  short: R. Alur, T.A. Henzinger, O. Kupferman, M. Vardi, in:, Proceedings of the
    9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 1998, pp. 163–178.
conference:
  end_date: 1998-09-11
  location: Nice, France
  name: 'CONCUR: Concurrency Theory'
  start_date: 1998-09-08
date_created: 2018-12-11T12:09:42Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T09:50:34Z
day: '01'
doi: 10.1007/BFb0055622
extern: '1'
intvolume: '      1466'
language:
- iso: eng
month: '01'
oa_version: None
page: 163 - 178
publication: Proceedings of the 9th Interantional Conference on Concurrency Theory
publication_identifier:
  isbn:
  - 978-3-540-64896-3
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '104'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating refinement relations
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1466
year: '1998'
...
---
_id: '4515'
abstract:
- lang: eng
  text: We summarize and reorganize some of the last decade's research on real-time
    extensions of temporal logic. Our main focus is on tableau constructions for model
    checking linear temporal formulas with timing constraints. In particular, we find
    that a great deal of real-time verification can be performed in polynomial space,
    but also that considerable care must be exercised in order to keep the real-time
    verification problem in polynomial space, or even decidable.
acknowledgement: This research was supported in part by the Office of Naval Research
  Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER
  award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the
  Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research
  Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation
  contract 97-DC-324.041.
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
citation:
  ama: 'Henzinger TA. It’s about time: Real-time logics reviewed. In: <i>Proceedings
    of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik; 1998:439-454. doi:<a href="https://doi.org/10.1007/BFb0055640">10.1007/BFb0055640</a>'
  apa: 'Henzinger, T. A. (1998). It’s about time: Real-time logics reviewed. In <i>Proceedings
    of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp.
    439–454). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a
    href="https://doi.org/10.1007/BFb0055640">https://doi.org/10.1007/BFb0055640</a>'
  chicago: 'Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” In
    <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>,
    1466:439–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href="https://doi.org/10.1007/BFb0055640">https://doi.org/10.1007/BFb0055640</a>.'
  ieee: 'T. A. Henzinger, “It’s about time: Real-time logics reviewed,” in <i>Proceedings
    of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998,
    vol. 1466, pp. 439–454.'
  ista: 'Henzinger TA. 1998. It’s about time: Real-time logics reviewed. Proceedings
    of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency
    Theory, LNCS, vol. 1466, 439–454.'
  mla: 'Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” <i>Proceedings
    of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–54, doi:<a href="https://doi.org/10.1007/BFb0055640">10.1007/BFb0055640</a>.'
  short: T.A. Henzinger, in:, Proceedings of the 9th Interantional Conference on Concurrency
    Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–454.
conference:
  end_date: 1998-09-11
  location: Nice, France
  name: 'CONCUR: Concurrency Theory'
  start_date: 1998-09-08
date_created: 2018-12-11T12:09:15Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T14:24:08Z
day: '01'
doi: 10.1007/BFb0055640
extern: '1'
intvolume: '      1466'
language:
- iso: eng
month: '01'
oa_version: None
page: 439 - 454
publication: Proceedings of the 9th Interantional Conference on Concurrency Theory
publication_identifier:
  isbn:
  - 978-3-540-64896-3
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '214'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'It''s about time: Real-time logics reviewed'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1466
year: '1998'
...