Explore

CGAAL is our model checker of alternating-time temporal logic properties in concurrent games. CGAAL checks such properties by encoding the problem as an extended dependency graph. It then computes the satisfaction relation using the distributed local on-the-fly CERTAINZERO algorithm by Dalsgaard et al. We provide multiple novel search strategies for the algorithm and allow concurrent games to be expressed in our language LCGS.

To evaluate our tool, we run several experiments. In our experiments we compare our global algorithm, our local algorithm using our various search strategies, and the established tool PRISM-games. We use several different concurrent game case studies. Some of these are PRISM-games case studies adapted to LCGS for CGAAL and determinised if needed. Others are well-known algorithms and games constructed during the development of...

This paper is available on arxiv under CC 4.0 license. The syntax of the language is inspired by PRISM-lang used by the PRISM model checker to model stochastic multi-player games with rewards. The primary feature of CGAAL is the verification of ATL properties for CGSs.

In order to check if a CGS satisfies an ATL property, CGAAL encodes the problem as an extended dependency graph and finds a fixed-point assignment describing the satisfaction relation.