CGAAL: A Distributed On-The-Fly ATL Model Checker: The Definitions You Should Know About
Too Long; Didn't Read
This paper is available on arxiv under CC 4.0 license. We recall the definitions of concurrent games and alternating-time temporal logic. A computation starting in the state *q* is called a *q-computation. We will refer to them as "enforce" and "despite", respectively.