Alternating-time temporal logic (original) (raw)

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 to construct model-checkers in order to address problems such as receptiveness, realizability, and controllability.