CGAAL: A Distributed On-The-Fly ATL Model Checker: The Definitions You Should Know About

Table of Links

Introduction

Definitions

Model Checking

Tool Overview

Evaluation

Conclusion and References

2 Definitions

We recall the definitions of concurrent games and alternating-time temporal logic.

A computation starting in the state q is called a q-computation.

Alternating-time Temporal Logic The alternating-time temporal logic (ATL) [1] is defined with respect to a finite set Π of propositions and a finite set Σ = {1,...,k} of players. An ATL formula is given by the abstract syntax:

where p ∈ Π is a proposition and A ⊆ Σ is a set of players. The operators ⟪⋅⟫ and J⋅K are path quantifiers. We will refer to them as "enforce" and "despite", respectively. The ◯ ("next") and U ("until") are temporal operators. Additional temporal operators like ♢ ("eventually") and □ ("invariant") are derived as usual.

Given a state q of a game structure S, we write q ⊧ φ to indicate that the state q satisfies the property described by φ. The satisfactory relation ⊧ is defined inductively:

This paper is available on Arxiv under CC 4.0 license.