Alternating-time temporal logic

Template:Short description Template:Expert neededIn computer science, alternating-time temporal logic, or ATL, is a branching-time temporal logic that extends computation tree logic (CTL) to multiple players. ATL naturally describes computations of multi-agent systems and concurrent games. Quantification in ATL is 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.

Syntax

Let $\mathrm{\Pi }$ be a set of atomic propositions and $\mathrm{\Sigma }$ a set of agents. A coalition is a finite subset $A\subseteq \mathrm{\Sigma }$ of agents. The formulas of ATL are generated by the grammar$$\phi ::=p\mid \mathrm{\neg }\phi \mid \phi \vee \psi \mid ⟨⟨A⟩⟩X\phi \mid ⟨⟨A⟩⟩G\phi \mid ⟨⟨A⟩⟩(\phi U\psi ),$$

where $p\in \mathrm{\Pi }$ and $A\subseteq \mathrm{\Sigma }$.

Here $X$ is the next operator, $G$ is the globally or always operator, and $U$ is the until operator. The expression $⟨⟨A⟩⟩$ is a strategic quantifier: intuitively, $⟨⟨A⟩⟩X\phi$ states that coalition $A$ has a strategy that guarantees that $\phi$ holds at the next state, regardless of the actions of agents outside the coalition.

The dual strategic quantifier $[[A]]$ is defined by $[[A]]\psi \equiv \mathrm{\neg }⟨⟨A⟩⟩\mathrm{\neg }\psi$. While $⟨⟨A⟩⟩\psi$ states that coalition A can enforce $\psi$, $[[A]]\psi$ states that coalition A cannot avoid $\psi$.

The usual Boolean connectives, such as $\wedge$, $\to$, and $\leftrightarrow$, can be defined in the usual way. The eventually operator $F$ is derived from until; in particular, $⟨⟨A⟩⟩F\phi \equiv ⟨⟨A⟩⟩(\mathrm{\top }U\phi ).$

Unlike in ATL*, temporal operators in ATL cannot be combined arbitrarily: each temporal objective is immediately governed by a strategic quantifier. The syntax is the same as computational tree logic (CTL), but quantifies over coalitional moves rather than branches of executions. The syntactical expressiveness difference between ATL and ATL* is mirrored in CTL and CTL*.

Examples

One can write logical formulas in ATL such as $⟨⟨\{a,b\}⟩⟩Fp$ that expresses the fact that agents a and b have a strategy to ensure that the property p holds in the future, whatever the other agents of the system are performing.

Extensions and variants

ATL* is the extension of ATL, as CTL* extends CTL. ATL* allows to write more complex temporal objectives, for instance $⟨⟨\{a,b\}⟩⟩(Fp\wedge Gq)$. Belardinelli et al. proposes a variant of ATL on finite traces. ATL has been extended with context, in order to store the current strategies played by the agents. ATL* is extended by strategy logic.

ATL has been generalized to include epistemic features. In 2003, van der Hoek and Woodridge proposed ATEL: the logic ATL augmented with an epistemic operator from epistemic logic. In 2004, Pierre-Yves Schobbens proposed variants of ATL with imperfect recall.

One cannot express properties about individual objectives in ATL. That is why, in 2010, Chatterjee, Henzinger and Piterman introduced Strategy Logic, a first-order logic in which strategies are first-order citizens. Strategy logic subsumes both ATL and ATL*.

See also

• Linear temporal logic
• Computational tree logic
• Strategy logic