Jump to content

Alternating-time temporal logic

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Ott2 (talk | contribs) at 11:55, 4 September 2018 (complete partial citation). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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

References

  1. ^ van Drimmelen, Govert (2003). "Satisfiability in Alternating-time Temporal Logic". Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society. doi:10.1109/LICS.2003.1210060. ISBN 0-7695-1884-2. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help)
  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