alternating-time temporal logic
{{Short description|Type of temporal logic}}
{{Expert needed|computer science|reason=contains buzzwords that should be explained in a less technical manner|date=July 2017}}
In computer science, alternating-time temporal logic, or ATL, is a branching-time temporal logic that extends computation tree logic (CTL) to multiple players.{{cite conference|title=Alternating-time temporal logic|first1=Rajeev|last1=Alur|author1-link = Rajeev Alur|first2=Thomas A.|last2=Henzinger|author2-link = Thomas Henzinger|first3=Orna|last3=Kupferman|author3-link = Orna Kupferman|book-title=Proceedings of the 38th Annual Symposium on Foundations of Computer Science|year=1997|pages=100–109|publisher=IEEE Computer Society|doi=10.1109/SFCS.1997.646098|isbn=0-8186-8197-7}} ATL naturally describes computations of multi-agent systems and concurrent games.{{cite conference|title=Satisfiability in Alternating-time Temporal Logic|book-title=Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science|first=Govert|last=van Drimmelen|publisher=IEEE Computer Society|isbn=0-7695-1884-2|year=2003|doi=10.1109/LICS.2003.1210060}} Quantification in ATL is over program-paths that are possible outcomes of games.{{cite journal|title=Alternating-Time Temporal Logic|first1=Rajeev|last1=Alur|first2=Thomas A.|last2=Henzinger|first3=Orna|last3=Kupferman|journal=Journal of the ACM|volume=49|issue=5|pages=672–713|year=2002|doi=10.1145/585265.585270|s2cid=15984608|url=https://repository.upenn.edu/cis_reports/102}} 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 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 . Belardinelli et al. proposes a variant of ATL on finite traces.{{Cite journal|last1=Belardinelli|first1=Francesco|last2=Lomuscio|first2=Alessio|last3=Murano|first3=Aniello|last4=Rubin|first4=Sasha|date=2018|title=Alternating-time Temporal Logic on Finite Traces|url=https://www.ijcai.org/proceedings/2018/11|pages=77–83}} 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.{{Cite journal|last1=van der Hoek|first1=Wiebe|last2=Wooldridge|first2=Michael|date=2003-10-01|title=Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications|journal=Studia Logica|language=en|volume=75|issue=1|pages=125–157|doi=10.1023/A:1026185103185|s2cid=10913405|issn=1572-8730}} In 2004, Pierre-Yves Schobbens proposed variants of ATL with imperfect recall.{{Cite journal|last=Schobbens|first=Pierre-Yves|date=2004-04-01|title=Alternating-time logic with imperfect recall|journal=Electronic Notes in Theoretical Computer Science|series=LCMAS 2003, Logic and Communication in Multi-Agent Systems|volume=85|issue=2|pages=82–93|doi=10.1016/S1571-0661(05)82604-0|issn=1571-0661|doi-access=free}}
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.{{Cite journal|last1=Chatterjee|author1-link = Krishnendu Chatterjee|first1=Krishnendu|last2=Henzinger|first2=Thomas A.|last3=Piterman|first3=Nir|date=2010-06-01|title=Strategy logic|journal=Information and Computation|series=Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007)|volume=208|issue=6|pages=677–693|doi=10.1016/j.ic.2009.07.004|issn=0890-5401|url=https://repository.ist.ac.at/56/1/Strategy_logic.pdf}} Strategy logic subsumes both ATL and ATL*.