Alternating-time 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. (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.[1] ATL naturally describes computations of multi-agent systems and multiplayer video 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
In ATL, we can write logical formulas 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 . ATL has been extended with context, in order to store the current strategies played by the agents. ATL* are extended by strategy logic.
See also
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.
{{cite conference}}: Unknown parameter|booktitle=ignored (|book-title=suggested) (help) - ^ 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.
{{cite conference}}: Unknown parameter|booktitle=ignored (|book-title=suggested) (help) - ^ 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.