Alternating-time temporal logic explained

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.

Examples

One can write logical formulas in ATL such as

\langle \langle \{a, b\}\rangle \rangle 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

\langle \langle \{a, b\}\rangle \rangle (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*.

See also

• Linear temporal logic

Notes and References

1. Alternating-time temporal logic. Rajeev. Alur. Rajeev Alur. Thomas A.. Henzinger. Thomas Henzinger. Orna. Kupferman. Orna Kupferman. Proceedings of the 38th Annual Symposium on Foundations of Computer Science. 1997. 100–109. IEEE Computer Society. 10.1109/SFCS.1997.646098. 0-8186-8197-7.
2. Satisfiability in Alternating-time Temporal Logic. Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science. Govert. van Drimmelen. IEEE Computer Society. 0-7695-1884-2. 2003. 10.1109/LICS.2003.1210060.
3. Alternating-Time Temporal Logic. Rajeev. Alur. Thomas A.. Henzinger. Orna. Kupferman. Journal of the ACM. 49. 5. 672–713. 2002. 10.1145/585265.585270. 15984608.
4. Belardinelli. Francesco. Lomuscio. Alessio. Murano. Aniello. Rubin. Sasha. 2018. Alternating-time Temporal Logic on Finite Traces. 77–83.
5. van der Hoek. Wiebe. Wooldridge. Michael. 2003-10-01. Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications. Studia Logica. en. 75. 1. 125–157. 10.1023/A:1026185103185. 10913405. 1572-8730.
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. 10.1016/S1571-0661(05)82604-0. 1571-0661. free.
7. Chatterjee. Krishnendu Chatterjee. Krishnendu. Henzinger. Thomas A.. Piterman. Nir. 2010-06-01. Strategy logic. Information and Computation. Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007). 208. 6. 677–693. 10.1016/j.ic.2009.07.004. 0890-5401.