Misplaced Pages

Alternating-time temporal logic

Article snapshot taken from[REDACTED] with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Type of temporal logic
This article needs attention from an expert in computer science. The specific problem is: contains buzzwords that should be explained in a less technical manner. WikiProject Computer science may be able to help recruit an expert. (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. 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.

Examples

One can write logical formulas in ATL such as ⟨ ⟨ { a , b } ⟩ ⟩ F p {\displaystyle \langle \langle \{a,b\}\rangle \rangle 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 } ⟩ ⟩ ( F p ∧ G q ) {\displaystyle \langle \langle \{a,b\}\rangle \rangle (Fp\land 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

References

  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.
  3. 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.
  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.
Categories:
Alternating-time temporal logic Add topic