Alur, Rajeev and Henzinger, Thomas A. and Kupferman, Orna :: Alternating-Time Temporal Logic
- authors
- Alur, Rajeev and Henzinger, Thomas A. and Kupferman, Orna
- url
- http://dl.acm.org/citation.cfm?id=585270
Paper that describes alternating-time temporal logic.
Alternating-time temporal logic is a logic which can express whether the coordinated action of a coalition of agents can enforce a given property of play. This is expressed as players navigating a state space to reach a state from which no futures that violate the property can be reached.
A sentence in alternating-time temporal logic is structured as follows:
<coalition c> can force <LTL claim L>
Which plays out semantically as
there exists a partial strategy σ consisting only of moves by members of c, such that for every state s' that σ potentially reaches from the current state s, all histories beginning from s' obey L.
ATL is modeled by concurrent game systems. It is satisfiable in PTIME. There exist variants, notably ATL*, which are only satisfiable in 2EXPTIME.
The "alternation" desrcibes the proof strategy, which shows that given a specific coalition and a specific outcome they are trying to force, if there exists a coalitional strategy to force that outcome it can be found by treating the game as a 2-player game between the coalition and its complement and using more typical BIR from there.
from wikipedia
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. It offers selective quantification over program-paths that are possible outcomes of games. ATL uses alternating-time formulas to construct model-checkers in order to address problems such as receptiveness, realizability, and controllability.
"Alternating-time Temporal Logic" by Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104
description in ruledynamics.org, less descriptive and touches on the idea of a variant of ATL mediated by dominance.