# CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics††thanks:
Funded by the VILLUM INVESTIGATOR project S4OS.

Falke B. Ø. Carlsen Department of Computer Science,
Aalborg University, Denmark<EMAIL_ADDRESS>Department of Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, Denmark Lars Bo P. Frydenskov Department of Computer
Science,
Aalborg University, Denmark<EMAIL_ADDRESS>Department of Computer
Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, Denmark Nicolaj Ø. Jensen Department of Computer Science,
Aalborg University, Denmark<EMAIL_ADDRESS>Department of Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, Denmark Jener Rasmussen<EMAIL_ADDRESS>Department of
Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, Denmark Mathias M. Sørensen
<EMAIL_ADDRESS>Department of Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, Denmark Asger G. Weirsøe<EMAIL_ADDRESS>Department of
Computer Science,
Aalborg University, DenmarkDepartment of Computer Science,
Aalborg University, Denmark Mathias C. Jensen Department of Computer Science,
Aalborg University, Denmark<EMAIL_ADDRESS>Department of Computer Science,
Aalborg University, Denmark Kim G. Larsen Department of Computer Science,
Aalborg University, Denmark<EMAIL_ADDRESS>
###### Abstract

We present Cgaal, our efficient on-the-fly model checker for alternating-time
temporal logic (ATL) on concurrent game structures (CGS). We present how our
tool encodes ATL as extended dependency graphs with negation edges and employs
the distributed on-the-fly algorithm by Dalsgaard et al. Our tool offers
multiple novel search strategies for the algorithm, including DHS which is
inspired by PageRank and uses the in-degree of configurations as a heuristic,
IHS which estimates instability of assignment values, and LPS which estimates
the distance to a state satisfying the constituent property using linear
programming. CGS are input using our modelling language LCGS, where
composition and synchronisation are easily described. We prove the correctness
of our encoding, and our experiments show that our tool Cgaal is often one to
three orders of magnitude faster than the popular tool Prism-games on case
studies from Prism’s documentation and among case studies we have developed.
In our evaluation, we also compare and evaluate our search strategies, and
find that our custom search strategies are often significantly faster than the
usual breadth-first and depth-first search strategies. #fritfit

##  1 Introduction

Software plays a large role in our everyday lives, making decisions, enabling
efficient communication, ensuring safety, and many more critical tasks.
Furthermore, the complexity of the software and the decisions they have to
make are ever-increasing due the to interconnectivity and reactive nature of
modern systems. These software systems mutually depend on, communicate with,
and guide each other based on their collective and internal states. Even a few
interconnected systems that are not necessarily themselves too complex can
give rise to an extremely complex system as a whole. Safety-critical software
that operates in contexts where errors could lead to human casualties or
significant capital losses requires methods to verify their correctness.
Unfortunately, such methods are difficult to implement due to the sheer state-
space explosion that arises from the inherent parallel composition of systems.

In this paper, we consider systems that can be expressed as discrete
multiplayer games in which the actors can perform actions concurrently. That
is, in each configuration of the game, each player simultaneously chooses an
action they wish to perform and the resulting decision vector then
deterministically results in the next configuration of the game. Such
concurrent games are extremely expressive and can be used to model a variety
of complex systems and lends themselves inherently, by their concurrent
nature, to describing multi-actor systems. The properties that we wish to
verify on these systems are those that can be expressed by Alternating-time
Temporal Logic (ATL) [2], a game theoretic extension of Computation Tree Logic
(CTL) [3, 4], that like CTL can be used to describe safety and liveness
properties. ATL extends CTL by replacing the existential and universal path
quantifiers with so-called coalition quantifiers. These coalition quantifiers
describe properties of the game in which a coalition of players can either
enforce some desired outcome or cannot avoid an outcome. Of course, proof of
satisfaction of such property is done by finding a strategy showing that the
players can indeed enforce said property or by showing that no matter what
strategy the players follow they cannot avoid said property.

One existing tool that can model check concurrent (stochastic) games is Prism-
games [13], an extension of the probabilistic model checker Prism [12]. Prism
excels at stochastic models such as discrete- and continuous-time Markov
chains, Markov decision processes, and (priced) probabilistic timed automata,
for which it can verify various properties described in LTL , CSL, and
probabilistic CTL*. There are multiple verification engines in Prism, both
symbolic and explicit-state. The Prism-games extension focuses on stochastic
games in which game-theoretic approaches are needed. Prism-games can among
other things synthesise strategies and reason about equilibria-based
properties, where players may have distinct, but not necessarily conflicting
objectives. These properties are typically described with probabilistic ATL
with rewards. In version 3.0 [13], Prism-games added support for concurrent
stochastic games.

In [15], Liu and Smolka present a global and a local algorithm to compute
fixed-point boolean vertex assignments in dependency graphs with directed
hyper-edges representing dependencies between vertex values. The global
algorithm has a better worst-case running time of the two, but the on-the-fly
local algorithm only explores the graph as needed to compute the fixed-point
assignment. Many problems have since been encoded as dependency graphs.
Notably, model-checking problems for CTL can be encoded as dependency graphs
and the algorithms by Liu and Smolka can be used to compute the satisfaction
relation enabling model-checking using dependency graphs. J. F. Jensen et al.
[10] show that weighted CTL can be encoded in dependency graphs as well and
introduce symbolic edges to handle weights efficiently. In [11], M. C. Jensen
et al. introduce symbolic dependency graphs, an encoding of probabilistic
weighted CTL, and an implementation of a local and global algorithm. A.
Dalsgaard et al. [5] present a distributed extension to the local algorithm to
boost the performance and show how to model Petri Nets problems using CTL and
dependency graphs. Furthermore, they extend dependency graphs by adding
components and negation edges to solve formulae with negations. An abstract
dependency graph framework is presented by S. Enevoldsen et al. in [7] where
they generalise the various extensions of the dependency graphs with a general
algorithm for any Noetherian partial order domain. In the closely related work
of [6], S. Enevoldsen et at. uses abstract dependency graphs to model check
probabilistic ATL for weighted stochastic games. In multiple works [5, 11] the
local algorithm is found to be faster more often than the global algorithm in
practice.

In this paper, we introduce the tool Cgaal (Concurrent Games AALborg), a model
checker implemented in Rust that allows for the verification of ATL properties
on concurrent games. Cgaal works by encoding the model checking problem as an
extended dependency graph and by implementing the on-the-fly local distributed
algorithm by Dalsgaard et al. [5]. The concurrent games are described and
inputted to the tool using LCGS, our Prism-language inspired model language,
and for specific ATL formulae, we can output a strategy describing how to
ensure satisfaction given a positive result. Furthermore, Cgaal implements a
variety of strategies for searching the problem state space: a heuristic
inspired by PageRank [16] and two heuristic search strategies that exploit the
state vector representation of our model, alongside the usual breadth-first
and depth-first approach. We conduct experiments comparing our different
search strategies with each other on several case studies and show that having
more available compute threads often leads to speed-ups of 1-2 orders of
magnitude. We also perform experiments comparing our tool on a selection of
case studies to the state-of-the-art Prism-games. Though while Prism-games is
a tool specialised for probabilistic games we find that our implementation
often outperforms Prism-games and especially whenever we are not required to
compute the entire fixed point in which case we are often 1-3 orders of
magnitude faster. Again, we emphasise that Prism-games is meant for
probabilistic games and as such this is not a completely fair one-to-one
comparison.

#### Outline.

This paper is structured as follows. Section 2 introduces the formal
definitions of concurrent games and alternating-time temporal logic. In
Section 3 we present how model checking of ATL properties in concurrent games
can be encoded in extended dependency graphs. We also give a short explanation
of the CertainZero algorithm and our search strategies. In Section 4 we give a
short example of how to use Cgaal and the LCGS language. An evaluation of our
tool and a comparison with Prism can be found in Section 5, and we conclude on
our findings in Section 6.

##  2 Definitions

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

#### Concurrent Games

A concurrent game structure (CGS) is a tuple $S=\langle
k,Q,\Pi,\pi,d,\delta\rangle$ where:

  * •

$k\geq 1$ is a natural number of players. We identify the players with the
numbers $1,\dotsc,k$.

  * •

$Q$ is a finite set of states.

  * •

$\Pi$ is a finite set of atomic propositions, also called labels.

  * •

A set $\pi(q)\subseteq\Pi$ of propositions are true at $q\in Q$. The function
$\pi$ is called the labelling function.

  * •

For each player $a\in\\{1,\dotsc,k\\}$ and each state $q\in Q$, a natural
number $d_{a}(q)\geq 1$ of moves are available to player $a$ at state $q$. The
moves of player $a$ at state $q$ are identified with the numbers
$1,\dotsc,d_{a}(q)$.

A move vector at $q\in Q$ is a tuple $v=\langle j_{1},\dotsc,j_{k}\rangle$
such that $1\leq j_{a}\leq d_{a}(q)$ for each player $a\in\\{1,\dotsc,k\\}$.
Additionally, given a state $q\in Q$, we write $D(q)$ for the set
$\\{1,\dotsc,d_{1}(q)\\}\times\dotsb\times\\{1,\dotsc,d_{k}(q)\\}$ of all move
vectors possible at $q$. The function $D$ is called the move function.

  * •

For each state $q\in Q$ and each move vector $v=\langle
j_{1},\dotsc,j_{k}\rangle\in D(q)$, we have that $\delta(q,v)\in Q$ is the
resulting state when each player $a\in\\{1,\dotsc,k\\}$ chooses move $j_{a}$
in the state $q$. The function $\delta$ is called the transition function.

A state $q^{\prime}$ is a successor to $q$ if and only if there exists a
transition from $q$ to $q^{\prime}$, i.e. there exists a move vector $v\in
D(q)$ such that $\delta(q,v)=q^{\prime}$. A computation is an infinite
sequence $\lambda=q_{0},q_{1},q_{2},\dotsc$ of states, such that for all
$i\geq 0$, the state $q_{i+1}$ is a successor of $q_{i}$. Given a computation
$\lambda$ and a position $i\geq 0$, we use the following notations:

$\displaystyle\lambda[i]$ The $i$th state of the computation of $\lambda$
$\displaystyle\lambda[0,i]$ The finite prefix $q_{0},q_{1},\dotsc,q_{i}$ of
$\lambda$ $\displaystyle\lambda[i,\infty]$ The infinite suffix
$q_{i},q_{i+1},q_{i+2},\dotsc$ of $\lambda$

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

#### Game strategies

Consider a concurrent game structure $S=\langle k,Q,\Pi,\pi,d,\delta\rangle$
over the set $\Sigma=\\{1,\dotsc,k\\}$ of players. A strategy for a player
$a\in\Sigma$ is a function $z_{a}:Q\to\mathbb{N}$ that maps every state $q\in
Q$ to a natural number, such that $z_{a}(q)\leq d_{a}(q)$. In other words, the
strategy $z_{a}$ describes how player $a$ chooses their move in each state. A
strategy $z_{a}$ for a player $a\in\Sigma$ induces a set of computations that
the player $a$ can enforce. Given a state $q\in Q$, a set $A\subseteq\Sigma$
of players, and a set $Z_{A}=\\{z_{a}\\}_{a\in A}$ of strategies, one strategy
for each player in $A$, we define the outcomes of the strategies $Z_{A}$ from
$q$, denoted $out(q,Z_{A})$, to be the set of $q$-computations that the
players of $A$ enforce following the strategies of $Z_{A}$. That is, a
computation $\lambda=q_{0},q_{1},q_{2},\dotsc$ is in $out(q,Z_{A})$ if
$q_{0}=q$ and for all positions $i\geq 0$, there is a move vector $v=\langle
j_{1},\dotsc,j_{k}\rangle\in D$ such that

  1. 1.

$j_{a}=z_{a}(q_{i})$ for all players $a\in A$, and

  2. 2.

$\delta(q_{i},v)=q_{i+1}$.

The set $\mathcal{Z}^{A}=\\{\\{z_{a}\\}_{a\in A}\mid z_{a}\text{ is a strategy
for the player }a\\}$ contains all sets of strategies, that contain one
strategy for each player in $A\subseteq\Sigma$.

#### Alternating-time Temporal Logic

The alternating-time temporal logic (ATL) [2] is defined with respect to a
finite set $\Pi$ of propositions and a finite set $\Sigma=\\{1,...,k\\}$ of
players. An ATL formula is given by the abstract syntax:

$\phi::=p\mid\neg\phi\mid\phi_{1}\lor\phi_{2}\mid\llangle
A\rrangle\bigcirc\phi\mid\llangle
A\rrangle(\phi_{1}\mathcal{U}\phi_{2})\mid\llbracket
A\rrbracket(\phi_{1}\mathcal{U}\phi_{2})$

where $p\in\Pi$ is a proposition and $A\subseteq\Sigma$ is a set of players.
The operators $\llangle\cdot\rrangle$ and $\llbracket\cdot\rrbracket$ are path
quantifiers. We will refer to them as ”enforce” and ”despite”, respectively.
The $\bigcirc$ (”next”) and $\mathcal{U}$ (”until”) are temporal operators.
Additional temporal operators like $\Diamond$ (”eventually”) and $\Box$
(”invariant”) are derived as usual.

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

  * •

$q\vDash p$ iff $p\in\pi(q)$.

  * •

$q\vDash\neg\phi$ iff $q\not\vDash\phi$.

  * •

$q\vDash\phi_{1}\lor\phi_{2}$ iff $q\vDash\phi_{1}$ or $q\vDash\phi_{2}$.

  * •

$q\vDash\llangle A\rrangle\bigcirc\phi$ iff there exists a set
$Z_{A}\in\mathcal{Z}^{A}$ of strategies, such that for all computations
$\lambda\in out(q,Z_{A})$, we have $\lambda[1]\vDash\phi$.

  * •

$q\vDash\llangle A\rrangle(\phi_{1}\mathcal{U}\phi_{2})$ iff there exists a
set $Z_{A}\in\mathcal{Z}^{A}$ of strategies, such that for all computation
$\lambda\in out(q,Z_{A})$ there exists a position $i\geq 0$, such that
$\lambda[i]\vDash\phi_{2}$ and for all positions $0\leq j<i$, we have
$\lambda[j]\vDash\phi_{1}$.

  * •

$q\vDash\llbracket A\rrbracket(\phi_{1}\mathcal{U}\phi_{2})$ iff for all sets
$Z_{A}\in\mathcal{Z}^{A}$ of strategies, we have that there exists a
computation $\lambda\in out(q,Z_{A})$, such that there exists a position
$i\geq 0$, such that $\lambda[i]\vDash\phi_{2}$ and for all positions $0\leq
j<i$, we have $\lambda[j]\vDash\phi_{1}$.

##  3 Model Checking

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.

#### Extended Dependency Graphs

An extended dependency graph (EDG) is a tuple $G=\langle C,E,N\rangle$ where
$C$ is a finite set of configurations (vertices), $E\subseteq
C\times\mathcal{P}(C)$ is a finite set of hyper-edges, and $N\subseteq C\times
C$ is a finite set of negation edges.

For a hyper-edge $e=\langle c,T\rangle\in E$ we call $c$ the source
configuration and $T\subseteq C$ the set of target configurations. Similarly,
$c$ is called the source configuration of the negation edge $\langle
c,c^{\prime}\rangle\in N$. We write $c\rightarrow c^{\prime}$ if there exists
an edge $\langle c,T\rangle\in E$ such that $c^{\prime}\in T$ and
$c\dashrightarrow c^{\prime}$ if $\langle c,c^{\prime}\rangle\in N$.
Furthermore, we write $c\rightsquigarrow c^{\prime}$ if $c\rightarrow
c^{\prime}$ or $c\dashrightarrow c^{\prime}$. An EDG $G=\langle C,E,N\rangle$
is negation safe if there are no $c,c^{\prime}\in C$ such that
$c\dashrightarrow c^{\prime}$ and $c^{\prime}\rightsquigarrow^{*}c$. In what
follows, we consider only negation-safe EDGs. Let
$dist:C\rightarrow\mathbb{N}_{0}$ be the maximum number of negation edges
throughout all paths starting in a configuration $c\in C$, inductively defined
as:

$\displaystyle dist(c)=\max\\{dist(c^{\prime\prime})+1\mid
c^{\prime},c^{\prime\prime}\in C\text{ and
}c\rightarrow^{*}c^{\prime}\dashrightarrow c^{\prime\prime}\\}$ (1)

By convention $\max\emptyset=0$. We define the $dist(G)$ of an EDG $G$ as
$dist(G)=\max_{c\in C}(dist(c))$. A component $K_{i}$ of an EDG $G$, where
$i\in\mathbb{N}_{0}$, is a subgraph induced on $G$ by the sets

  * •

$C_{i}=\\{c\in C\mid dist(c)\leq i\\}$

  * •

$E_{i}=\\{\langle c,T\rangle\in E\mid dist(c)\leq i\\}$

  * •

$N_{i}=\\{\langle c,c^{\prime}\rangle\in N\mid dist(c)\leq i\\}$

denoting the set of configurations, hyper-edges and negation edges
respectively in each respective component. By definition, the component
$K_{0}$ has no negation edges.

#### Assignments

An assignment $\alpha:C\to\\{0,1\\}$ is a function that assigns boolean values
to configurations of an EDG $G=\langle C,E,N\rangle$, where 0 and 1 represent
false and true, respectively. We define $\alpha_{0}$ as the zero assignment
where $\alpha_{0}(c)=0$ for all $c\in C$. We assume a component-wise ordering
$\sqsubseteq$ on assignments such that we have
$\alpha\sqsubseteq\alpha^{\prime}$ whenever $\alpha(c)\leq\alpha^{\prime}(c)$
for all $c\in C$. The set of all assignments of an EDG $G$ is denoted by
$\mathcal{A}^{G}$ and $\langle\mathcal{A}^{G},\sqsubseteq\rangle$ is a
complete lattice.

By Knaster and Tarski’s theorem, we can find a minimum fixed point on the
complete lattice for any monotonic function. The minimum fixed-point
assignment $\alpha_{\min}$ of an EDG $G$, denoted as
$\alpha^{G}_{\min}=\alpha^{K_{dist(G)}}_{\min}$ is defined inductively on the
components $K_{0},K_{1},\dotsc,K_{dist(G)}$ of $G$. For all $0\leq i\leq
dist(G)$, we define $\alpha^{K_{i}}_{\min}$ to be the minimum fixed-point
assignment of the monotonic function
$F_{i}:\mathcal{A}^{C_{i}}\to\mathcal{A}^{C_{i}}$ where

$\displaystyle
F_{i}(\alpha)(c)=\alpha(c)\lor\Bigg{[}\bigvee_{\begin{subarray}{c}\langle
c,T\rangle\in E_{i}\end{subarray}}\bigwedge_{\begin{subarray}{c}c^{\prime}\in
T\end{subarray}}\alpha(c^{\prime})\Bigg{]}\lor\Bigg{[}\bigvee_{\begin{subarray}{c}\langle
c,c^{\prime}\rangle\in
N_{i}\end{subarray}}\neg\alpha^{K_{i-1}}_{\min}(c^{\prime})\Bigg{]}$ (2)

By convention, the conjunction of $\emptyset$ is true and the disjunction of
$\emptyset$ is false. In the component $K_{0}$ there are no negation edges,
which means the last clause in the disjunction is false for $K_{0}$. We will
refer to the repeated use of the $F_{i}$ as the global algorithm because it
requires building and iterating over the entire EDG. By Equation 2 each
configuration in the EDG is comparable to a boolean formula in disjunctive
normal form where each clause is another configuration or a negation of
another configuration. Clearly, this makes EDGs an expressive structure and we
shall now encode ATL model checking in an EDG.

###  3.1 Encoding of ATL in an EDG

We first establish some definitions related to subsets of move vectors induced
by a coalition of players.

#### Partial Moves.

Given a CGS $S$ with the set of states $Q$ and $k$ players, we use
$V_{1}\times\dotsb\times V_{k}=\mathcal{V}\subseteq D(q)$ where $q\in Q$ to
denote a partial move in $q$, where zero or more of the players’ moves are
fixed, i.e. their set of possible moves contain a single number. For instance,
if $\mathcal{V}=\\{2\\}\times\\{1,2,3\\}$ in a 2-player game, then player 1
has chosen move 2 while player 2 is still free to choose from 1, 2, or 3.
Furthermore, we use the notation $\mathcal{V}[a\mapsto j]$ for a variant
$\mathcal{V}^{\prime}$ of a partial move $\mathcal{V}=V_{1}\times\dotsb\times
V_{k}$ where player $a$ chooses move $j$. More precisely

$\displaystyle\mathcal{V}[a\mapsto j]=V^{\prime}_{1}\times\dotsb\times
V^{\prime}_{k}\quad\text{where }1\leq i\leq k\text{ and
}V^{\prime}_{i}=\begin{cases}\\{j\\}&\text{if }i=a\\\
V_{i}&\text{otherwise}\end{cases}$ (3)

With this notation in mind, we define the function $pmoves$. The function
$pmoves$ gives the set of all possible partial moves that follow from the
players of the set $A\subseteq\Sigma$ making a combination of moves in the
state $q\in Q$:

$\displaystyle pmoves(q,A)=\\{D(q)[a\mapsto j_{a}][b\mapsto
j_{b}]\dotsb\mid\\{a,b,\dotsc\\}=A\text{ and }\forall i\in A.1\leq j_{i}\leq
d_{i}(q)\\}$ (4)

For instance, if $D(q)=\\{1,2\\}\times\\{1,2\\}$ in a 2-player game and
$A=\\{1\\}$. Then
$pmoves(q,A)=\\{\\{1\\}\times\\{1,2\\},\\{2\\}\times\\{1,2\\}\\}$ contains two
partial moves. One where player 1 chooses action 1, and another where player 1
chooses action 2. In other words, the $pmoves$ function constructs the partial
moves that the set $A$ of players can choose from when working together in the
state $q$. If $A$ chooses $\mathcal{V}\in pmoves(q,A)$, then $\mathcal{V}$
contains all move vectors that result from the remaining players
$\Sigma\backslash A$ also making a choice.

We define a partial transition function $\Delta$ that produces a set of
possible successor states given a state $q\in Q$ and a partial move
$\mathcal{V}$. That is

$\displaystyle\Delta(q,\mathcal{V})=\\{s\mid v\in\mathcal{V}\text{ and
}\delta(q,v)=s\\}\quad\text{where }\mathcal{V}\subseteq D(q)$ (5)

With EDGs, assignments, and partial moves introduced, we can now define how
the satisfaction relation $\vDash$ can be encoded as an EDG.

$\langle q,\textbf{true}\rangle$$\emptyset$

$\langle q,\neg\phi\rangle$$\langle q,\phi\rangle$

$\langle q,p\rangle$$\emptyset$if $p\in\pi(q)$

$\langle q,p\rangle$if $p\notin\pi(q)$

Figure 1: EDG encoding of true, negation, and atomic proposition

$\langle q,\phi_{1}\lor\phi_{2}\rangle$$\langle q,\phi_{1}\rangle$$\langle
q,\phi_{2}\rangle$

Figure 2: EDG encoding of disjunction

$\langle q,\llangle A\rrangle\bigcirc\phi\rangle$$\langle
q_{1},\phi\rangle$$\dotsb$$\langle q_{n},\phi\rangle$$\dotsb$$\langle
s_{1},\phi\rangle$$\dotsb$$\langle s_{m},\phi\rangle$where
$\\{\\{q_{1},\dotsc,q_{n}\\},\dotsc,\\{s_{1},\dotsc,s_{m}\\}\\}=\\{\Delta(q,\mathcal{V})\mid\mathcal{V}\in
pmoves(q,A)\\}$

Figure 3: EDG encoding of next

$\langle q,\llangle A\rrangle(\phi_{1}\mathcal{U}\phi_{2})\rangle$$\langle
q,\phi_{2}\rangle$$\langle q,\phi_{1}\rangle$$\langle q_{1},\llangle
A\rrangle(\phi_{1}\mathcal{U}\phi_{2})\rangle$$\dotsb$$\langle q_{n},\llangle
A\rrangle(\phi_{1}\mathcal{U}\phi_{2})\rangle$$\dotsb$$\langle s_{1},\llangle
A\rrangle(\phi_{1}\mathcal{U}\phi_{2})\rangle$$\dotsb$$\langle s_{m},\llangle
A\rrangle(\phi_{1}\mathcal{U}\phi_{2})\rangle$where
$\\{\\{q_{1},\dotsc,q_{n}\\},\dotsc,\\{s_{1},\dotsc,s_{m}\\}\\}=\\{\Delta(q,\mathcal{V})\mid\mathcal{V}\in
pmoves(q,A)\\}$

Figure 4: EDG encoding of enforce until

$\langle q,\llbracket A\rrbracket(\phi_{1}\mathcal{U}\phi_{2})\rangle$$\langle
q,\phi_{2}\rangle$$\langle q,\phi_{1}\rangle$$\langle
q,\mathcal{V}_{1},\llbracket
A\rrbracket(\phi_{1}\mathcal{U}\phi_{2})\rangle$$\dotsb$$\langle
q,\mathcal{V}_{n},\llbracket
A\rrbracket(\phi_{1}\mathcal{U}\phi_{2})\rangle$where
$\\{\mathcal{V}_{1},\dotsc,\mathcal{V}_{n}\\}=pmoves(q,A)$

Figure 5: EDG encoding of despite until

$\langle q,\mathcal{V},\phi\rangle$$\langle q_{1},\phi\rangle$$\dotsb$$\langle
q_{n},\phi\rangle$where $\\{v_{1},\dotsc,v_{n}\\}=\mathcal{V}$ and
$q_{i}=\delta(q,v_{i})$ for $1\leq i\leq n$

Figure 6: EDG encoding of partially moved despite until

#### Encoding.

Given a CGS $S$, a state $q$ of $S$, and an ATL state formula $\phi$ we now
construct an EDG where every configuration is either a pair of a state and a
formula, or a triple of a state, partial move, and a formula. The triples
represent partially evaluated states, where some players’ moves are already
set. Starting from the initial pair $\langle q,\phi\rangle$, the dependency
graph is constructed according to Figures 6, 6, 6, 6, 6 and 6. The figures
show which outgoing edges each configuration has and the target configurations
of those edges.

######  Theorem 3.1.

Given a CGS $S=\langle k,Q,\Pi,\pi,d,\delta\rangle$, a state $q\in Q$, and an
ATL formula $\phi$, let $G$ be the negation-safe EDG rooted in $\langle
q,\phi\rangle$ constructed following Figures 6, 6, 6, 6, 6 and 6. Then
$\alpha^{G}_{\min}(\langle q,\phi\rangle)=1$ if and only if $q\vDash\phi$.

The proof of Theorem 3.1 can be found in the extended version of this paper.

#### Certain Zero

In addition to the global algorithm (repeated application of $F_{i}$ from
Equation 2), Cgaal also implements a local algorithm heavily inspired by the
distributed CertainZero algorithm by Dalsgaard et al. [5]. A local algorithm
specialises in finding the assignment $\alpha_{\min}^{G}(\langle
q,\phi\rangle)$ of a specific configuration $\langle q,\phi\rangle$ and not
necessarily the assignment of the whole EDG. This allows the algorithm to
terminate early in many cases. For the CertainZero algorithm, Dalsgaard et al.
also introduce a symbolic assignment with new assignment values. The value
$\bot$ indicates that the configuration is unexplored. The value $?$ (unknown)
indicates that the configuration is explored, but its final value has yet to
be determined. Lastly, 0 and 1 indicate the final values in the minimum fixed-
point assignment $\alpha_{\min}^{G}$. This induces an ordering as seen in the
lattice in Figure 7. During the algorithm, the assignments of the
configurations will rise to more and more certain values, and if the
assignment of a configuration ever becomes 0 or 1, we can be certain that its
final value is 0 or 1, respectively. This is one of the properties that lead
to improved performance, since in contrast to the global algorithm where all
configurations are initially assigned 0, we can distinguish an initial 0 and a
certain 0. Hence, the CertainZero algorithm can terminate early if the root
configuration is ever assigned either 0 or 1. Otherwise, it terminates when it
can no longer raise any assignment values.

$\bot$$?$01

Figure 7: Ordering of assignment values for fixed-point computation in the
CertainZero algorithm. The top values are more certain.

###  3.2 Search Strategies

The CertainZero algorithm is controlled by a search strategy, which determines
in which order the edges are explored and evaluated. Our search strategies for
Cgaal include the common breadth-first search (BFS) and depth-first search
(DFS) strategies, as well as multiple search strategies based on heuristics.
Some of these are discussed in the following subsections. Which strategy is
best depends heavily on the shape of the EDG which is determined by the CGS
and the ATL formula in question. An evaluation of the strategies can be found
in Section 5. The BFS strategy is the default strategy.

#### Dependency Heuristic Search (DHS)

PageRank [16] is an algorithm that was created to estimate the importance of a
website based on how many other websites have links to it. The idea has since
been used in other areas, such as graph recommendation systems [14] or
measuring structural-context similarity with SimRank [8]. Our dependency
heuristic search (DHS) uses a similar idea by assuming that configurations
with many ingoing edges are important. Finding the assignments of these,
results in more back-propagation, bringing us closer to termination. In other
words, the heuristic focuses on the trunk of the EDG where certain assignments
are of high value. Specifically, DHS prioritise edges where the source
configuration has a high number of ingoing edges. That is, if $e$ is an edge
with source configuration $c$ then:

$\displaystyle
priority(e)=indegree(source(e))=|\\{e^{\prime}\mid(e^{\prime}=\langle
c^{\prime},T\rangle\in E\land c\in T)\lor e^{\prime}=\langle
c^{\prime},c\rangle\in N\\}|$ (6)

Edges with the same priority are subject to FIFO ordering. However, since we
do not know the whole graph in advance, we must continuously update the
priority of edges when we explore successors of new configurations. This is
only a small overhead with a priority queue data structure.

#### Linear Programming Heuristic Search (LPS)

In this search strategy, we take advantage of how LCGS states can be
represented as vectors, i.e. $Q$ is a vector space. Given an edge with source
configuration $\langle q,\phi\rangle$, we transform $\phi$ into a set
$\mathcal{L}_{\phi}$ of linear constraints, each defined as a pair
$\langle\textbf{C},b\rangle$, where C is a matrix and $b$ is a vector. We
prioritise edge $e$ if its source configuration $\langle q,\phi\rangle$ has a
low estimated distance to satisfaction as given by:

$\displaystyle dist_{LPS}(\langle
q,\phi\rangle)=\min||s-q||_{1}\quad\text{subject to }\textbf{C}s\geq
b\quad\text{ where }s\in Q,\;\langle\textbf{C},b\rangle\in\mathcal{L}_{\phi}$
(7)

where $||\cdot||_{1}$ is the 1-norm, i.e. taxicap distance. The following
equation is an equivalent linear programming problem:

$\displaystyle\min\sum_{i}x_{i}\quad\text{subject to }\textbf{C}s\geq b\text{
and }-x_{i}\leq s_{i}-q_{i}\leq x_{i}\quad\forall i\quad\text{ where }s\in
Q,\;\langle\textbf{C},b\rangle\in\mathcal{L}_{\phi}$ (8)

$2$$4$$6$$8$$2$$4$$6$$8$$q$$s$$dist_{LPS}(\langle q,\phi\rangle)$ $-x+y\geq 1$
$\frac{1}{2}x+y\geq 7$

Figure 8: The distance $dist_{LPS}(\langle q,\phi\rangle)=7$ when $q=\langle
7,1\rangle\in Q=\mathbb{R}^{2}$ and $\mathcal{L_{\phi}}$ corresponds to the
constraints $-x+y\geq 1$ and $\frac{1}{2}x+y\geq 7$. The state $s$ minimises
$||s-q||_{1}$ while adhering to the constraints.

A visualisation of the distance $dist_{LPS}$ can be seen on Figure 8, where
$Q=\mathbb{R}^{2}$, $q=\langle 7,1\rangle\in Q$ and

$\mathcal{L}_{\phi}=\\{\langle\begin{bmatrix}-1&1\\\
\frac{1}{2}&1\end{bmatrix},\begin{bmatrix}1\\\ 7\end{bmatrix}\rangle\\}$

Many methods exist for solving linear programming problems. We use a library
called minilp111minilp crate: https://crates.io/crates/minilp. The LPS
strategy assumes value-wise close states are structurally close and works best
when the constituent variables of states represent non-categorical data. The
drawback of this method is the computational overhead of linear programming
amplified by the potential need to solve multiple linear programming problems
for each configuration based on the structure of $\phi$. We reduce some of
this overhead by caching the set $\mathcal{L}_{\phi}$ for each $\phi$.

We also support an alternative search strategy involving linear programming.
It is called Linear Representative Search (LRS) and it computes the distance
described above for the root configuration only. The closest satisfying state
$s$ is then saved and edges are prioritised based on the 1-norm distance
between $s$ and the state in their source configuration. In other words, we
assume that the state $s$ found for the root represents all satisfied states.
As a result this search strategy is cheaper than LPS but risks being
inaccurate.

#### Instability Heuristic Search (IHS)

The Petri Net model checker Tapaal [9] implements the CertainZero algorithm as
well. Their configurations consist of a marking (a state) and a property, and
their default search strategy uses a heuristic that estimates the distance
between the marking of the configuration and a marking that satisfies the
formula of the configuration. Our novel instability heuristic is inspired by
their heuristic, but we differ by acknowledging that since there are negation
edges in the EDG, we may not always be looking for a state that satisfies the
formula. That is, if the state already satisfies the associated formula, we
estimate the distance to a state that does not instead. This guides the search
towards configurations where the assignment is unstable and thus may have a
high influence. Algorithms 1 and 2 find the $dist_{IHS}$ described above for
an edge. The algorithms use an abstract metric $BiDist$ which for state-
property pairs finds $\langle\hat{t},\hat{f}\rangle$ where $\hat{t}$ is the
distance to the property being true and $\hat{f}$ is the distance to the
property being false.

Input : An edge $e\in E$

Output : An estimated distance to a different assignment

1

2if  _$e=\langle c,T\rangle\in E$_ then

3 $\langle\hat{t},\hat{f}\rangle:=\bigsqcap_{\langle q,\phi\rangle\in
T}BiDist(q,\phi)$;

4 return _$\hat{t}$ if $\hat{t}>0$, otherwise $\hat{f}$_

5else if  _$e=\langle c,\langle q,\phi\rangle\rangle\in N$_ then

6 $\langle\hat{t},\hat{f}\rangle:=BiDist(q,\phi)$;

7 return _$\hat{f}$ if $\hat{f}<0$, otherwise $\hat{t}$_

Algorithm 1 $dist_{IHS}$

Input : A state $q$ and formula $\phi$

Output : A bi-distance $\langle\hat{t},\hat{f}\rangle$ describing the
instability of $\phi$ in $q$

1

2if  _$\phi=expr_{1}\lhd expr_{2}$ _and_
$v=eval(q,expr_{1})-eval(q,expr_{2})$_ then

3 return _$\langle v,0\rangle$ if $v>0$, otherwise $\langle 0,v\rangle$_

4else if  _$\phi=expr_{1}\rhd expr_{2}$ _and_
$v=eval(q,expr_{2})-eval(q,expr_{1})$_ then

5 return _$\langle v,0\rangle$ if $v>0$, otherwise $\langle 0,v\rangle$_

6else if  _$\phi=\neg\phi^{\prime}$ _and_
$\langle\hat{t},\hat{f}\rangle=BiDist(q,\phi^{\prime})$_ then

7 return _$\langle\hat{f},\hat{t}\rangle$_

8else if  _$\phi=\phi_{1}\land\phi_{2}$_ then

9 return _$BiDist(q,\phi_{1})\sqcap BiDist(q,\phi_{2})$_

10else if  _$\phi=\phi_{1}\lor\phi_{2}$_ then

11 return _$BiDist(q,\phi_{1})\sqcup BiDist(q,\phi_{2})$_

12else if  _$\phi=\llangle A\rrangle\bigcirc\phi^{\prime}$_ then

13 return _$BiDist(q,\phi^{\prime})$_

14else if  _$\phi=\llangle A\rrangle(\phi_{1}\;\mathcal{U}\;\phi_{2})$_ then

15 return _$BiDist(q,\phi_{1})\sqcup BiDist(q,\phi_{2})$_

16else if  _$\phi=\llbracket A\rrbracket(\phi_{1}\;\mathcal{U}\;\phi_{2})$_
then

17 return _$BiDist(q,\phi_{1})\sqcup BiDist(q,\phi_{2})$_

18// where
$\lhd\in\\{<,\leq\\},\langle\hat{t}_{1},\hat{f}_{1}\rangle\sqcap\langle\hat{t}_{2},\hat{f}_{2}\rangle=\langle\hat{t}_{1}+\hat{t}_{2},\min\\{\hat{f}_{1},\hat{f}_{2}\\}\rangle$

19//
$\quad\quad\quad\rhd\in\\{>,\geq\\},\langle\hat{t}_{1},\hat{f}_{1}\rangle\sqcup\langle\hat{t}_{2},\hat{f}_{2}\rangle=\langle\min\\{\hat{t}_{1},\hat{t}_{2}\\},\hat{f}_{1}+\hat{f}_{2}\rangle$

Algorithm 2 $BiDist$

##  4 Tool Overview

Cgaal (https://github.com/d702e20/CGAAL) is written in Rust and consists of a
command-line interface and a verification engine. The primary feature of Cgaal
is the verification of ATL properties for CGSs. Verification is either done
with a global algorithm or local algorithm, both of which are described in
Section 3. If requested, a partial strategy witness can also be computed,
which instructs how the given players must play to satisfy the given property.
Another feature converts the model into dot graph format such that it can be
visually rendered with Graphviz.222Graphviz: https://graphviz.org/

To model concurrent game structures for Cgaal, we designed a declarative
Language for Concurrent Game Structure, called LCGS. In LCGS a CGS is defined
with a series of declarations such that it is possible to find the successors
of any state from the declarations alone. The language acts as an abstract
representation of the CGS and allows us to save memory at the small cost of
having to evaluate the expressions of declarations whenever successors are
explored. The syntax of the language is inspired by Prism-lang [12] used by
the Prism model checker to model stochastic multi-player games with rewards.
However, LCGS differs in multiple ways. For instance, LCGS has player
templates instead of modules, and templates have no effect unless there exists
an instance of it. Additionally, synchronisations affecting the internal state
of a player are much easier to declare.

#### Example Use

As an example, we want to check if a cowboy can guarantee to stay alive in a
three-way Mexican standoff. The standoff is simulated in rounds and in each
round a cowboy can choose to wait, shoot the cowboy to the right, or shoot the
cowboy to the left. If a cowboy is hit by two bullets, he dies.

⬇

1const max_health = 2;

2

3template cowboy

4

5 // How many bullets a cowboy can be hit by before dying

6 health : [0 .. max_health] init max_health;

7 health’ = max(health - opp_right.shoot_left - opp_left.shoot_right, 0);

8

9 // A proposition used by ATL formulae

10 label alive = health > 0;

11

12 // The actions available to each cowboy

13 [wait] 1;

14 [shoot_right] health > 0 && opp_right.health > 0;

15 [shoot_left] health > 0 && opp_left.health > 0;

16

17endtemplate

18

19// The three cowboys in the Mexican standoff

20player billy = cowboy [opp_right=clayton, opp_left=jesse];

21player clayton = cowboy [opp_right=jesse, opp_left=billy];

22player jesse = cowboy [opp_right=billy, opp_left=clayton];

Listing 1: LCGS implementation of a Mexican standoff

We model this scenario in LABEL:code:mexican_standoff_lcgs. The cowboy
template is declared on lines 3-17. Herein, on line 6, we define that each
cowboy can be hit by two bullets before being incapacitated, but we make this
number a constant on line 1 so it is easy to change. Each cowboy has their own
health variable and the combination of the values of these variables makes up
a state. Line 7 defines how the health of a cowboy is updated in each
transition. The value of opp_right.shoot_left and opp_left.shoot_right are 1
if this cowboy was shot by the given opponent to the right or left,
respectively, otherwise 0. On line 10 we define a label called alive, which is
a proposition that is true if the cowboy has more than zero health. Lines
13-15 define the actions of the cowboy template, and the expression to the
right of the name is a condition defining in which states the action is
available. As can be seen, a cowboy can always wait, but only shoot if they
and their target are alive. Lastly, we declare three instances of the cowboy
template on lines 20-22. We define the right and left opponent in the
relabelling function after the name of the template. Any identifier in a
template can be relabelled to another expression as long as the result is
syntactically and semantically correct.

The ATL formula $\llangle\texttt{billy}\rrangle\Box\texttt{billy.alive}$ is
satisfied if the cowboy billy has a strategy to stay alive. We can now run
Cgaal with the following command: ./cgaal solver -m standoff.lcgs -f billy-
can-stay-alive.atl, and Cgaal will tell us that the property is not satisfied.
Billy has no strategy that can guarantee his survival.

##  5 Evaluation

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 Cgaal. We make the
Prism-lang and LCGS implementations of models as identical as possible, such
that the state spaces are comparable. Some of the concurrent games and related
ATL formulae used in the experiments are presented below. Queries marked with
$\top$ (resp. $\bot$) are satisfied (resp. not satisfied), and queries marked
with $\dagger$ may terminate early as we are not required to compute the
entire fixed-point:

  * •

Mexican-Standoff: In this model $N$ cowboys stand in a circle, each with a
revolver. At each moment they can choose to shoot another cowboy or do
nothing. If a cowboy is hit by $B$ bullets, they are incapacitated. We run the
following queries:

$\displaystyle MS_{N}^{B}\phi^{\bot\dagger}_{1}=\llangle p_{1}\rrangle\Box
p_{1}\\_alive$ $\displaystyle MS_{N}^{B}\phi^{\bot}_{2}=\llangle
p_{1}\rrangle\Diamond\neg p_{1}\\_alive$ $\displaystyle
MS_{N}^{B}\phi^{\top}_{3}=\llangle\\{p_{i}\in\Sigma\mid 1\equiv i\mod
2\\}\rrangle\Box p_{1}\\_alive$

  * •

Gossiping Girls: In this model, $N$ nodes each know a piece of information.
The nodes can exchange information by calling each other. Our experiments
include both a fully connected network of nodes and a circular network of
nodes. We run the following queries:

$\displaystyle GG_{N}\phi^{\top\dagger}_{1}=\llangle\Sigma\rrangle(calls\leq
10\;\mathcal{U}\;all\\_girls\\_know\\_all)$ $\displaystyle
GG_{N}\phi^{\top\dagger}_{2}=\llangle\Sigma\rrangle(calls\leq
10\;\mathcal{U}\;only\\_p_{1}\\_knows\\_all)$ $\displaystyle
GG_{N}\phi^{\top\dagger}_{3}=\llangle\Sigma\rrangle(calls\leq
10\;\mathcal{U}\;p_{1}\\_knows\\_all)$ $\displaystyle
GG_{N}\phi^{\top\dagger}_{4}=\llangle\Sigma\rrangle\Diamond calls>10\land
all\\_girls\\_know\\_all$ $\displaystyle
GG_{N}\phi^{\top\dagger}_{5}=\llangle\emptyset\rrangle\Diamond calls>10$
$\displaystyle GG_{N}\phi^{\bot\dagger}_{6}=\llangle p_{1}\rrangle(calls\leq
10\;\mathcal{U}\;p_{1}\\_knows\\_all)$ $\displaystyle
GG_{N}\phi^{\top\dagger}_{7}=\llangle\Sigma\setminus\\{p_{1}\\}\rrangle\Diamond
everyone\\_except\\_p_{1}\\_knows\\_all$

  * •

Robot Coordination: In this model, four robots move orthogonally on a $N$ by
$N$ grid. Each robot needs to reach the opposite corner of where they start,
but crashing into each other is fatal. We run the following queries:

$\displaystyle RC_{N}\phi^{\bot}_{1}=\llangle
p_{1},p_{2},p_{3}\rrangle\Diamond p_{1}\\_at\\_target\land
p_{2}\\_at\\_target$ $\displaystyle
RC_{N}\phi^{\top}_{2}=all\\_robots\\_at\\_home$ $\displaystyle
RC_{N}\phi^{\top\dagger}_{3}=\llangle p_{1},p_{2},p_{3},p_{4}\rrangle\Diamond
all\\_robots\\_at\\_targets$ $\displaystyle RC_{N}\phi^{\bot}_{4}=\llangle
p_{1},p_{3},p_{4}\rrangle\Diamond p_{1}\\_at\\_target\land\neg
p_{1}\\_crashed$

Each experiment is run with a time limit of two hours, allocated 128 GB of
memory, and has 32 cores available regardless of how many worker threads Cgaal
may spawn. All experiments are run on several identical AMD EPYC 7642 based
servers, allowing only one experiment per node at a time to reduce noise in
the results.

#### Results

(a) Mexican-standoff: horizontal axis is $(N,B)$ tuples with $N$ being the
number of cowboys in the model and $B$ the number of bullets the cowboys can
be hit by.

(b) Robot Coordination: horizontal axis is the size of the grid the robots are
to manoeuvre on.

(c) Gossiping girls in a circular topology: horizontal axis being the number
of girls in the circle.

(d) Gossiping girls with six girls in a circular topology: horizontal axis
being the number of compute threads used in our distributed algorithm. Note
that Prism was always run with just one thread.

Figure 9: Select experimental results. Cgaal-results in Figures 9(a), 9(b) and
9(c) show the best result for each search strategy when varying between 1 and
32 threads.

Here we provide a select set of experimental results that roughly exemplify
our findings in general. For a more thorough set of results along with all of
our experimental data and the Python script processing it, see the git
repository https://github.com/d702e20/evaluation-results/.

We find that the local on-the-fly algorithm is often one order of magnitude
faster than the global algorithm regardless of the search strategy. However,
the global algorithm can compete with and sometimes outperforms the local
algorithm in cases where the local algorithm cannot terminate early. This
matches observations made by A. Dalsgaard et al. [5] and M. C. Jensen et al.
[11].

Prism-games is a stochastic model checker and checks queries involving both
probability and rewards, capabilities which are irrelevant in our test cases.
Therefore, in many cases, Cgaal’s local algorithm is two orders of magnitude
faster than Prism-games, typically when the model has many synchronisations
that affect internal states of modules such as in Mexican Standoff and
Gossiping Girls as seen in Figures 9(a) and 9(c). Such synchronisations also
require a high amount of Prism-lang code, while being easily expressed in
LCGS. However, there are a few cases where Prism-games is faster than Cgaal,
e.g. $RC_{N}\phi^{\bot}_{1}$ and $RC_{N}\phi^{\bot}_{4}$ as seen in Figure
9(b). Here the local algorithm cannot terminate early.

The choice of search strategy sometimes has a discernible impact on the
performance of the local algorithm. Which search strategy is best varies from
case to case and no definitive best strategy. The BFS strategy does not work
well when the local algorithm can terminate early based on information found
multiple moves into the model, but its low overhead is beneficial when early
termination is not possible. The IHS strategy is often a good choice when
early termination is possible. The LPS strategy is often significantly slower
than the others, which is unsurprising given its overhead of solving linear
programming problems. In models where differences in the states correspond to
a distance in space, such as in robot coordination, the LPS strategy performs
notably better and is even faster than both BFS and DFS on
$RC_{4}\phi^{\top\dagger}_{3}$. The lightweight version, LRS, which only
solves the linear problem once, matches LPS in these cases but is also
generally better due to its lower overhead.

A general trend in our experiments is that we see an increase in the execution
speed of our distributed implementation as we increase the number of compute
threads available. The only times we do not see a speed-up with an increased
number of compute threads are when the models are small enough such that the
overhead of managing the additional threads is significant. Similarly, a
single thread performs better than a few threads in many cases, since there is
no communication overhead with only one compute thread. In general, depending
on the search strategy employed, we see an improvement on a scale of one to
two orders of magnitude when increasing the number of compute threads as
exemplified in Figure 9(d).

##  6 Conclusion

In this paper, we present Cgaal, 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 and then computes the
satisfaction relation using the distributed local on-the-fly CertainZero
algorithm by Dalsgaard et al. [5]. We provide multiple novel search strategies
for the algorithm and allow concurrent games to be expressed in our language
LCGS. Our experiments show that the local on-the-fly algorithm outperforms the
global algorithm in the majority of cases. We also find that Cgaal outperforms
the state-of-the-art tool Prism-games by being up to two orders of magnitude
faster, especially in models where synchronisations affect the internal state
of modules and whenever we are not required to compute the entire fixed point.
However, this comparison is unfair, since our test only uses a fraction of
Prism-games feature set.

Cgaal is still in early development and much work is needed before it competes
with Prism in terms of capabilities. However, dependency graphs have been used
for encoding various model-checking problems, and we intend to incorporate
these techniques into Cgaal.

## References

  * [1]
  * [2] Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002): _Alternating-Time Temporal Logic_.  J. ACM 49(5), p. 672–713, 10.1145/585265.585270.
  * [3] Edmund M. Clarke & E. Allen Emerson (1982): _Design and synthesis of synchronization skeletons using branching time temporal logic_.  In Dexter Kozen, editor: Logics of Programs, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 52–71, 10.1007/BFb0025774.
  * [4] Edmund M Clarke, Thomas A Henzinger, Helmut Veith, Roderick Bloem et al. (2018): _Handbook of model checking_.  10, Springer, 10.1007/978-3-319-10575-8.
  * [5] Dalsgaard, Andreas E. and Enevoldsen, Søren and Fogh, Peter and Jensen, Lasse S. and Jepsen, Tobias S. and Kaufmann, Isabella and Larsen, Kim G. and Nielsen, Søren M. and Olesen, Mads Chr. and Pastva, Samuel and Srba, Jiří (2017): _Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation_.  In Wil van der Aalst & Eike Best, editors: Application and Theory of Petri Nets and Concurrency, Springer International Publishing, Cham, pp. 139–158, 10.1007/978-3-319-57861-3_10.
  * [6] Søren Enevoldsen, Mathias Claus Jensen, Kim Guldstrand Larsen, Anders Mariegaard & Jiří Srba (2020): _Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs_.  LOPSTR2020, 10.1007/978-3-030-68446-4_13.
  * [7] Søren Enevoldsen, Kim Guldstrand Larsen & Jirí Srba (2022): _Extended abstract dependency graphs_.  Int. J. Softw. Tools Technol. Transf. 24(1), pp. 49–65, 10.1007/s10009-021-00638-8.
  * [8] Glen Jeh & Jennifer Widom (2002): _SimRank: a measure of structural-context similarity_.  In: Proceedings of the Eighth ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, July 23-26, 2002, Edmonton, Alberta, Canada, ACM, pp. 538–543, 10.1145/775047.775126.
  * [9] Jonas F. Jensen, Thomas Nielsen, Lars K. Oestergaard & Jiří Srba (2016): _TAPAAL and Reachability Analysis of P/T Nets_ , pp. 307–318.  Springer Berlin Heidelberg, Berlin, Heidelberg, 10.1007/978-3-662-53401-4_16.
  * [10] Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba & Lars Kaerlund Østergaard (2016): _Efficient model-checking of weighted CTL with upper-bound constraints_.  International Journal on Software Tools for Technology Transfer 18(4), pp. 409–426, 10.1007/s10009-014-0359-5.
  * [11] Mathias Claus Jensen, Anders Mariegaard & Kim Guldstrand Larsen (2019): _Symbolic model checking of weighted PCTL using dependency graphs_.  NASA Formal Methods Symposium, pp. 298–315, 10.1007/978-3-030-20652-9_20.
  * [12] M. Kwiatkowska, G. Norman & D. Parker (2011): _PRISM 4.0: Verification of Probabilistic Real-time Systems_.  In G. Gopalakrishnan & S. Qadeer, editors: Proc. 23rd International Conference on Computer Aided Verification (CAV’11), LNCS 6806, Springer, pp. 585–591, 10.1007/978-3-642-22110-1_47.
  * [13] M. Kwiatkowska, G. Norman, D. Parker & G. Santos (2020): _PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time_.  In: Proc. 32nd International Conference on Computer Aided Verification (CAV’20), LNCS 12225, Springer, pp. 475–487, 10.1007/978-3-030-53291-8_25.
  * [14] Sangkeun Lee, Minsuk Kahng & Sang goo Lee (2015): _Constructing compact and effective graphs for recommender systems via node and edge aggregations_.  Expert Systems with Applications 42(7), pp. 3396–3409, 10.1016/j.eswa.2014.11.062.
  * [15] Xinxin Liu & Scott A. Smolka (1998): _Simple Linear-Time Algorithms for Minimal Fixed Points (Extended Abstract)_.  In Kim Guldstrand Larsen, Sven Skyum & Glynn Winskel, editors: Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, Lecture Notes in Computer Science 1443, Springer, pp. 53–66, 10.1007/BFb0055040.
  * [16] Lawrence Page, Sergey Brin, Rajeev Motwani & Terry Winograd (1998): _The PageRank Citation Ranking: Bringing Order to the Web_.  Technical Report, Stanford Digital Library Technologies Project.  Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.1768.