Alternating-time temporal logic

In computer science, alternating-time temporal logic, or ATL, is a branching-time temporal logic that extends computation tree logic (CTL) to multiple players.^[1] ATL naturally describes computations of multi-agent systems and concurrent games.^[2] Quantification in ATL is over program-paths that are possible outcomes of games.^[3] ATL uses alternating-time formulas to construct model-checkers in order to address problems such as receptiveness, realizability, and controllability.

Syntax

Let $Π$ be a set of atomic propositions and $Σ$ a set of agents. A coalition is a finite subset $A \subseteq Σ$ of agents. The formulas of ATL are generated by the grammar $φ : := p ∣ \neg φ ∣ φ \lor ψ ∣ ⟨ ⟨ A ⟩ ⟩ X φ ∣ ⟨ ⟨ A ⟩ ⟩ G φ ∣ ⟨ ⟨ A ⟩ ⟩ (φ U ψ),$

where $p \in Π$ and $A \subseteq Σ$ .^[3]

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 φ$ states that coalition $A$ has a strategy that guarantees that $φ$ holds at the next state, regardless of the actions of agents outside the coalition.

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

The usual Boolean connectives, such as $\land$ , $\to$ , and $\leftrightarrow$ , can be defined in the usual way. The eventually operator $F$ is derived from until; in particular, $⟨ ⟨ A ⟩ ⟩ F φ \equiv ⟨ ⟨ A ⟩ ⟩ (⊤ U φ) .$

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} ⟩ ⟩ F p$ 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} ⟩ ⟩ (F p \land G q)$ . Belardinelli et al. proposes a variant of ATL on finite traces.^[4] 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.^[5] In 2004, Pierre-Yves Schobbens proposed variants of ATL with imperfect recall.^[6]

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.^[7] Strategy logic subsumes both ATL and ATL*.

References

↑ Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (1997). "Alternating-time temporal logic". Proceedings of the 38th Annual Symposium on Foundations of Computer Science. IEEE Computer Society. pp. 100–109. doi:10.1109/SFCS.1997.646098. ISBN 0-8186-8197-7.
↑ 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.
1 2 Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (2002). "Alternating-Time Temporal Logic". Journal of the ACM. 49 (5): 672–713. doi:10.1145/585265.585270. S2CID 15984608. Archived from the original on July 11, 2010.
↑ Belardinelli, Francesco; Lomuscio, Alessio; Murano, Aniello; Rubin, Sasha (2018). "Alternating-time Temporal Logic on Finite Traces": 77–83. {{cite journal}}: Cite journal requires |journal= (help)
↑ van der Hoek, Wiebe; Wooldridge, Michael (2003-10-01). "Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications". Studia Logica. 75 (1): 125–157. doi:10.1023/A:1026185103185. ISSN 1572-8730. S2CID 10913405.
↑ Schobbens, Pierre-Yves (2004-04-01). "Alternating-time logic with imperfect recall". Electronic Notes in Theoretical Computer Science. LCMAS 2003, Logic and Communication in Multi-Agent Systems. 85 (2): 82–93. doi:10.1016/S1571-0661(05)82604-0. ISSN 1571-0661.
↑ Chatterjee, Krishnendu; Henzinger, Thomas A.; Piterman, Nir (2010-06-01). "Strategy logic" (PDF). Information and Computation. Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007). 208 (6): 677–693. doi:10.1016/j.ic.2009.07.004. ISSN 0890-5401.

[1] Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (1997). "Alternating-time temporal logic". Proceedings of the 38th Annual Symposium on Foundations of Computer Science. IEEE Computer Society. pp. 100–109. doi:10.1109/SFCS.1997.646098. ISBN 0-8186-8197-7.

[2] 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.

[AlurHenzingerKupferman2002-3] 1 2 Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (2002). "Alternating-Time Temporal Logic". Journal of the ACM. 49 (5): 672–713. doi:10.1145/585265.585270. S2CID 15984608. Archived from the original on July 11, 2010.

[4] Belardinelli, Francesco; Lomuscio, Alessio; Murano, Aniello; Rubin, Sasha (2018). "Alternating-time Temporal Logic on Finite Traces": 77–83. {{cite journal}}: Cite journal requires |journal= (help)

[5] van der Hoek, Wiebe; Wooldridge, Michael (2003-10-01). "Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications". Studia Logica. 75 (1): 125–157. doi:10.1023/A:1026185103185. ISSN 1572-8730. S2CID 10913405.

[6] Schobbens, Pierre-Yves (2004-04-01). "Alternating-time logic with imperfect recall". Electronic Notes in Theoretical Computer Science. LCMAS 2003, Logic and Communication in Multi-Agent Systems. 85 (2): 82–93. doi:10.1016/S1571-0661(05)82604-0. ISSN 1571-0661.

[7] Chatterjee, Krishnendu; Henzinger, Thomas A.; Piterman, Nir (2010-06-01). "Strategy logic" (PDF). Information and Computation. Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007). 208 (6): 677–693. doi:10.1016/j.ic.2009.07.004. ISSN 0890-5401.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

Syntax

Examples

Extensions and variants

See also

References