---
OA_type: closed access
_id: '4432'
abstract:
- lang: eng
  text: We add freeze quantifiers to the game logic ATL in order to specify real-time
    objectives for games played on timed structures. We define the semantics of the
    resulting logic TATL by restricting the players to physically meaningful strategies,
    which do not prevent time from diverging. We show that TATL can be model checked
    over timed automaton games. We also specify timed optimization problems for physically
    meaningful strategies, and we show that for timed automaton games, the optimal
    answers can be approximated to within any degree of precision.
acknowledgement: This research was supported in part by the NSF grants CCR-0208875,
  CCR-0225610, and CCR-0234690.
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: Vinayak
  full_name: Prabhu, Vinayak
  last_name: Prabhu
citation:
  ama: 'Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: <i>Proceedings
    of the 4th International Conference on Formal Modeling and Analysis of Timed Systems</i>.
    Vol 4202. Springer Nature; 2006:1-17. doi:<a href="https://doi.org/10.1007/11867340_1">10.1007/11867340_1</a>'
  apa: 'Henzinger, T. A., &#38; Prabhu, V. (2006). Timed alternating-time temporal
    logic. In <i>Proceedings of the 4th international conference on Formal Modeling
    and Analysis of Timed Systems</i> (Vol. 4202, pp. 1–17). Paris, France: Springer
    Nature. <a href="https://doi.org/10.1007/11867340_1">https://doi.org/10.1007/11867340_1</a>'
  chicago: Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal
    Logic.” In <i>Proceedings of the 4th International Conference on Formal Modeling
    and Analysis of Timed Systems</i>, 4202:1–17. Springer Nature, 2006. <a href="https://doi.org/10.1007/11867340_1">https://doi.org/10.1007/11867340_1</a>.
  ieee: T. A. Henzinger and V. Prabhu, “Timed alternating-time temporal logic,” in
    <i>Proceedings of the 4th international conference on Formal Modeling and Analysis
    of Timed Systems</i>, Paris, France, 2006, vol. 4202, pp. 1–17.
  ista: 'Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. Proceedings
    of the 4th international conference on Formal Modeling and Analysis of Timed Systems.
    FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.'
  mla: Henzinger, Thomas A., and Vinayak Prabhu. “Timed Alternating-Time Temporal
    Logic.” <i>Proceedings of the 4th International Conference on Formal Modeling
    and Analysis of Timed Systems</i>, vol. 4202, Springer Nature, 2006, pp. 1–17,
    doi:<a href="https://doi.org/10.1007/11867340_1">10.1007/11867340_1</a>.
  short: T.A. Henzinger, V. Prabhu, in:, Proceedings of the 4th International Conference
    on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2006, pp. 1–17.
conference:
  end_date: 2006-09-27
  location: Paris, France
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
  start_date: 2006-09-25
date_created: 2018-12-11T12:08:49Z
date_published: 2006-09-19T00:00:00Z
date_updated: 2026-08-21T11:39:08Z
day: '19'
doi: 10.1007/11867340_1
extern: '1'
intvolume: '      4202'
language:
- iso: eng
month: '09'
oa_version: None
page: 1 - 17
publication: Proceedings of the 4th international conference on Formal Modeling and
  Analysis of Timed Systems
publication_identifier:
  eisbn:
  - '9783540450313'
  eissn:
  - 1611-3349
  isbn:
  - '9783540450269'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
publist_id: '296'
status: public
title: Timed alternating-time temporal logic
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4202
year: '2006'
...