Jump to content

Alternating-time temporal logic

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Lucaszeng (talk | contribs) at 20:05, 23 February 2009 (Created a page for Alternating-time Temporal Logic). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

In computer science, Alternating-time Temporal Logic, or ATL, is a branching-time temporal logic that naturally describes computations of multi-agent system and multiplayer games.[1]. It offers selective quantification over program-paths that are possible outcomes of games [2]. ATL uses alternating-time formulas to construct model-checkers in order to address problems such as receptiveness, realizability, and controllability.


See also

Reference

  1. ^ "Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science" by Govert van Drimmelen, IEEE Computer Society Washington, DC, USA
  2. ^ "Alternating-time Temporal Logic" by Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104