Alur, Rajeev and Henzinger, Thomas A. and Kupferman, Orna , Alternating-Time Temporal Logic
ID: ece237c0-cc23-4868-97ec-6482b253051a ROAM_REFS: https://en.wikipedia.org/wiki/Alternating-time_Temporal_Logic @aluralternatingtime2002 REVIEW_SCORE: 0.0 MTIME: [2024-12-25 Wed 16:03]
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.
1. from wikipedia
CREATED: [2016-11-02 Wed 16:47] ID: f9f80d3c-1149-4fe5-9b81-698999868526 REVIEW_SCORE: 0.0 MTIME: [2025-01-21 Tue 12:25]
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
, less descriptive and touches on the idea of a variant of ATL mediated by dominance.
2. earlier note
An extremely complete model of games, capable of expressing essentially whatever you want it to. Essentially CTL parametrized with actors, coalitions, and enforcements. Forcing (whose relationship with games is touched upon in the logic and game stanford encyclopedia article linked in this same bucket) becomes easy to understand via the sound allegory that this language provides.
In order to nest ATL arbitrarily (which is called ATL*), one needs to jump up in complexity past what's tenable. Instead of nesting it arbitrarily, if we nested it after restricting the possible self-reference to incentivized strategies (thereby needing us to add machinery to discuss player incentives and their compositionality in the first place), this jump up in complexity might not be prohibitive, and could be further heuristically approximated to the point of utility from there.