---
_id: '4601'
abstract:
- lang: eng
  text: "Temporal logic comes in two varieties: linear-time temporal logic assumes
    implicit universal quantification over all paths that are generated by system
    moves; branching-time temporal logic allows explicit existential and universal
    quantification over all paths. We introduce a third, more general variety of temporal
    logic: alternating-time temporal logic offers selective quantification over those
    paths that are possible outcomes of games, such as the game in which the system
    and the environment alternate moves. While linear-time and branching-time logics
    are natural specification languages for closed systems, alternating-time logics
    are natural specification languages for open systems. For example, by preceding
    the temporal operator “eventually” with a selective path quantifier, we can specify
    that in the game between the system and the environment, the system has a strategy
    to reach a certain state. Also the problems of receptiveness, realizability, and
    controllability can be formulated as model-checking problems for alternating-time
    formulas.\r\nDepending on whether we admit arbitrary nesting of selective path
    quantifiers and temporal operators, we obtain the two alternating-time temporal
    logics ATL and ATL. We interpret the formulas of ATL and ATL over alternating
    transition systems. While in ordinary transition systems, each transition corresponds
    to a possible step of the system, in alternating transition systems, each transition
    corresponds to a possible move in the game between the system and the environment.
    Fair alternating transition systems can capture both synchronous and asynchronous
    compositions of open systems. For synchronous systems, the expressive power of
    ATL beyond CTL comes at no cost: the model-checking complexity of synchronous
    ATL is linear in the size of the system and the length of the formula. The symbolic
    model-checking algorithm for CTL extends with few modifications to synchronous
    ATL, and with some work, also to asynchronous ATL, whose model-checking complexity
    is quadratic. This makes ATL an obvious candidate for the automatic verification
    of open systems. In the case of ATL, the model-checking problem is closely related
    to the synthesis problem for linear-time formulas, and requires doubly exponential
    time for both synchronous and asynchronous systems.\r\nA preliminary version of
    this paper appeared in the Proceedings of the 38th IEEE Symposium on Foundations
    of Computer Science (FOCS 1997), pp. 100–109."
acknowledgement: This work 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 97-DC-324.041.
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
citation:
  ama: 'Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. In: <i>Proceedings
    of the International Symposium on Compositionality</i>. Vol 1536. Springer; 1999:23-60.
    doi:<a href="https://doi.org/10.1007/3-540-49213-5_2">10.1007/3-540-49213-5_2</a>'
  apa: 'Alur, R., Henzinger, T. A., &#38; Kupferman, O. (1999). Alternating-time temporal
    logic. In <i>Proceedings of the International Symposium on Compositionality</i>
    (Vol. 1536, pp. 23–60). Bad Malente, Germany: Springer. <a href="https://doi.org/10.1007/3-540-49213-5_2">https://doi.org/10.1007/3-540-49213-5_2</a>'
  chicago: Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time
    Temporal Logic.” In <i>Proceedings of the International Symposium on Compositionality</i>,
    1536:23–60. Springer, 1999. <a href="https://doi.org/10.1007/3-540-49213-5_2">https://doi.org/10.1007/3-540-49213-5_2</a>.
  ieee: R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,”
    in <i>Proceedings of the International Symposium on Compositionality</i>, Bad
    Malente, Germany, 1999, vol. 1536, pp. 23–60.
  ista: 'Alur R, Henzinger TA, Kupferman O. 1999. Alternating-time temporal logic.
    Proceedings of the International Symposium on Compositionality. COMPOS: Compositionality,
    LNCS, vol. 1536, 23–60.'
  mla: Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” <i>Proceedings of the
    International Symposium on Compositionality</i>, vol. 1536, Springer, 1999, pp.
    23–60, doi:<a href="https://doi.org/10.1007/3-540-49213-5_2">10.1007/3-540-49213-5_2</a>.
  short: R. Alur, T.A. Henzinger, O. Kupferman, in:, Proceedings of the International
    Symposium on Compositionality, Springer, 1999, pp. 23–60.
conference:
  end_date: 1997-09-12
  location: Bad Malente, Germany
  name: 'COMPOS: Compositionality'
  start_date: 1997-09-08
date_created: 2018-12-11T12:09:41Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-01T14:23:41Z
day: '01'
doi: 10.1007/3-540-49213-5_2
extern: '1'
intvolume: '      1536'
language:
- iso: eng
month: '01'
oa_version: None
page: 23 - 60
publication: Proceedings of the International Symposium on Compositionality
publication_identifier:
  isbn:
  - '9783540654933'
publication_status: published
publisher: Springer
publist_id: '106'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating-time temporal logic
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1536
year: '1999'
...