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. ATL naturally describes computations of multi-agent systems and multiplayer video 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

In ATL, we can write logical formulas as $\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 $\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* are extended by strategy logic.

See also

• Linear temporal logic