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.
Examples
One can write logical formulas in ATL such as [math]\displaystyle{ \langle \langle \{a, b\}\rangle \rangle F p }[/math] 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 [math]\displaystyle{ \langle \langle \{a, b\}\rangle \rangle (F p \land G q) }[/math]. 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
References
- ↑ Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (1997). "Alternating-time temporal logic". 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". IEEE Computer Society. doi:10.1109/LICS.2003.1210060. ISBN 0-7695-1884-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. https://repository.upenn.edu/cis_reports/102.
- ↑ Belardinelli, Francesco; Lomuscio, Alessio; Murano, Aniello; Rubin, Sasha (2018). Alternating-time Temporal Logic on Finite Traces. pp. 77–83. https://www.ijcai.org/proceedings/2018/11.
- ↑ van der Hoek, Wiebe; Wooldridge, Michael (2003-10-01). "Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications" (in en). Studia Logica 75 (1): 125–157. doi:10.1023/A:1026185103185. ISSN 1572-8730.
- ↑ 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". 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. https://repository.ist.ac.at/56/1/Strategy_logic.pdf.
 |  |
