# Learning Branching-Time Properties in CTL and ATL via Constraint Solving

Benjamin Bordais  TU Dortmund University, Dortmund, Germany  Center for
Trustworthy Data Science and Security, University Alliance Ruhr, Dortmund,
Germany  Daniel Neider  TU Dortmund University, Dortmund, Germany  Center for
Trustworthy Data Science and Security, University Alliance Ruhr, Dortmund,
Germany  Rajarshi Roy  Max Planck Institute for Software Systems,
Kaiserslautern, Germany

###### Abstract

We address the problem of learning temporal properties from the branching-time
behavior of systems. Existing research in this field has mostly focused on
learning linear temporal properties specified using popular logics, such as
Linear Temporal Logic (LTL) and Signal Temporal Logic (STL). Branching-time
logics such as Computation Tree Logic (CTL) and Alternating-time Temporal
Logic (ATL), despite being extensively used in specifying and verifying
distributed and multi-agent systems, have not received adequate attention.
Thus, in this paper, we investigate the problem of learning CTL and ATL
formulas from examples of system behavior. As input to the learning problems,
we rely on the typical representations of branching behavior as Kripke
structures and concurrent game structures, respectively. Given a sample of
structures, we learn concise formulas by encoding the learning problem into a
satisfiability problem, most notably by symbolically encoding both the search
for prospective formulas and their fixed-point based model checking
algorithms. We also study the decision problem of checking the existence of
prospective ATL formulas for a given sample. We implement our algorithms in an
Python prototype and have evaluated them to extract several common CTL and ATL
formulas used in practical applications.

##  1 Introduction

Formal verification relies on the fact that formal specifications, which are
precise descriptions of the design requirements, are either readily available
or can be constructed easily. This assumption, however, often proves to be
unrealistic as constructing specifications manually is not only tedious but
also prone to errors. As a result, for years, the availability of precise,
functional, and usable specifications has been one of the biggest bottlenecks
of formal methods [4, 15, 51].

To tackle this serious limitation, recent research has concentrated on
automatically generating specifications, especially in temporal logics. There
is a large body of works targeted towards learning specifications in linear-
time logics such as Linear Temporal Logic (LTL) [42, 20], Metric Temporal
Logic (MTL) [46], Signal Temporal Logic (STL) [16, 40], etc. These approaches
not only generate reliable specifications but can also be used to infer
interpretable descriptions for complex temporal behaviors.

Along with linear-time logics, branching-time logics have had a significant
impact on formal verification. Computation Tree Logic (CTL) [25], which
combines temporal operators such as $\operatorname{\mathbf{X}}$ (next),
$\operatorname{\mathbf{F}}$ (finally), $\operatorname{\mathbf{G}}$ (globally)
with the branching quantifiers $\operatorname{\mathbf{E}\\!}$ (exists) and
$\operatorname{\mathbf{A}\\!}$ (all), is a specification language of choice
for numerous verification tools [12, 31, 23]. Alternating-time Temporal Logic
(ATL) [1], which augments CTL with a “cooperation” quantifier
$\langle\\!\langle\cdot\rangle\\!\rangle$ to reason about interaction of
multiple agents, is popular in specifying properties for distributed and
multi-agent systems [3, 37] and has several applications in AI domains [30,
39].

Despite the significance of branching-time logics, learning such
specifications has received considerably less attention. The few existing
works handle the problem of completing user-defined queries [21], i.e.,
specifications with missing parts, or searching for specifications based on
few restricted templates [55] such as
$\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{F}}?$,
$\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{G}}(?_{1}\rightarrow\operatorname{\mathbf{F}}?_{2})$,
etc. These works are limited in their generality and require one to handcraft
queries/templates suitable for learning.

Towards learning arbitrary branching-time properties, we consider the _passive
learning_ problem for both CTL and ATL. This problem requires, given a sample
$\mathcal{S}$ of positive (or desirable) and negative (or undesirable)
structures, to infer a minimal CTL/ATL formula that is consistent with
$\mathcal{S}$. Passive learning is widely studied in the literature [14, 28,
42] and forms a significant part of many learning frameworks [20, 49] (see
Section 3 for elaboration). In our learning problem, we consider, as input,
structures typical for describing branching behavior: Kripke structures (KSs)
and concurrent game structures (CGSs), which model single and multi-agent
systems, respectively.

To address the passive learning problem, we design algorithms for CTL and ATL
that employ constraint-solving techniques to learn prospective formulas.
Following Neider and Gavran [42], our algorithms search for prospective
formulas of size $n$ for a given sample $\mathcal{S}$, by encoding the problem
into the satisfiability of a propositional formula $\Omega^{\mathcal{S}}_{n}$.
This formula is then solved using an off-the-shelf SAT solver to obtain a
CTL/ATL formula of size $n$ if one exists. The crux of the SAT encoding lies
in symbolically encoding both the structure of the formula and the standard
fixed-point based model-checking for the symbolic formula.

To present the technical details of the encoding, we focus on passive learning
of ATL formulas from CGSs, as ATL and CGSs generalize CTL and KSs for multi-
agent settings, respectively. In particular, restricting the number of agents
to one simply reduces ATL to CTL and CGSs to KSs. Nonetheless, we highlight
aspects of the learning algorithm that improve in the case of CTL passive
learning.

We also initiate the theoretical study of the ATL passive learning problem. We
study the decision problem of whether there is an ATL formula consistent with
$\mathcal{S}$. We extend already existing results for CTL to the case of ATL:
we show that the decision problem for full ATL can be solved in polynomial
time (Thm. 7, extending [18, Thm. 3.2, 3.9]). We also show that, for any
fragment of ATL, the same decision problem can be decided in exponential time
(Thm. 18, extending [35, Thm. 3]). In the same theorem, we exhibit an
exponential bound on the size of the formulae that need to be considered to
find a consistent one, regardless of the fragment considered (parallelizing
[44, Coro. 1]).

We have implemented our learning algorithms in an open-source prototype that
can access an array of SAT solvers. We evaluate the prototype on synthetic
benchmarks consisting of samples of KSs and CGSs that reflect typical
branching-time properties. We observed that our algorithms display the ability
to learn formulas from samples of varying sizes. Further, we demonstrated
improvements to the SAT encoding for enhanced runtime performance.

####  1.0.1 Related Work

As alluded to in the introduction, the majority of works in inferring temporal
logics focus on linear-time logics. For LTL, many works consider learning
based on handcrafted templates or queries, which are incomplete formulas [36,
52, 32]. Few others learn formulas of arbitrary syntactic structure in LTL (or
its important fragments) either by exploiting constraint solving [42, 20, 47]
or efficient enumerative search [45, 53]. Some recent works rely on neuro-
symbolic approaches to learn LTL formulas from noisy data [38, 54]. For STL,
most works focus on learning formulas of particular syntactic structure [16,
17] or searching time intervals for STL formulas of known structure [7, 34,
33]. A handful of works consider learning STL formulas of arbitrary structure
[40, 43]. Apart from LTL and STL, there are works on learning several other
logics such as Metric Temporal Logic [46], Past LTL [6], Property
Specification Language [48], etc.

In contrast to linear-time logics, research on learning branching-time
properties remains relatively sparse. Chan [21] considers the problem of
completing CTL queries—incomplete CTL formulas with missing (Boolean
combinations of) atomic propositions. A related work by Wasylkowski and Zeller
[55] considers inferring operational preconditions for Java methods in CTL.
Both of these works are limited in their ability to search through large
number of CTL formulas of arbitrary syntactic structure. As a result, they
resort to user-defined queries or handcrafted templates to reduce the search
space of specifications.

A recent preprint by Pommellet et al. [44], yet to be published, addresses the
problem of learning CTL formulas from a sample of Kripke structures (KSs).
Their learning algorithm follows a SAT-based paradigm and uses an encoding
similar to ours. Our encoding for CTL was developed independently [50]. In
this paper, we study the more general problem of learning ATL formulas from
CGSs, which conceptually subsumes the problem of learning CTL formulas from
KSs.

Another work that devises a similar encoding is the one by Bertrand et al.
[13]. Their SMT encoding, albeit similar, is tailored towards solving a
different problem of synthesizing small models for probabilistic CTL (PCTL)
formulas.

##  2 Preliminaries

We refer to the set of positive integers by $\mathbb{N}_{1}$. For
$n\in\mathbb{N}_{1}$, we let $\llbracket 1,n\rrbracket\subseteq\mathbb{N}_{1}$
denote the set $\\{1,\ldots,n\\}$. Furthermore, given any non-empty set $Q$,
we let $Q^{*},Q^{+},Q^{\omega}$ denote the set of finite, non-empty finite,
and infinite sequences of elements in $Q$, respectively. For all
$\bullet\in\\{*,+,\omega\\}$, $\rho\in Q^{\bullet}$, and $i\in\mathbb{N}$, if
$\rho$ has at least $i+1$ elements, we let $\rho[i]\in Q$ denote the
$(i+1)$-th element in $\rho$, $\rho[:i]\in Q^{+}$ denote the finite sequence
$\rho_{0}\cdots\rho_{i}\in Q^{+}$, and $\rho[i:]\in Q^{\bullet}$ denote the
sequence $\rho_{i}\cdots\in Q^{\bullet}$.

###  2.1 Concurrent game structure (CGS) and Kripke structure

We model multi-agent systems with concurrent game structures defined below.

######  Definition 1.

A concurrent game structure (CGS for short) is a tuple $C=\langle
Q,I,k,\mathcal{P},\pi,d,\delta\rangle$ where $Q$ is the finite set of states,
$I\subseteq Q$ is the set of initial states, $k\in\mathbb{N}_{1}$ is the
number of agents, we denote by $\mathsf{Ag}:=\llbracket 1,k\rrbracket$ the set
of $k$ agents. Furthermore, $\mathcal{P}$ is the finite set of propositions
(or observations), $\pi:Q\mapsto 2^{\mathcal{P}}$ maps each state $q\in Q$ to
the set of propositions $\pi(q)\subseteq\mathcal{P}$ that hold in $q$.
Finally, $d:Q\times\mathsf{Ag}\rightarrow\mathbb{N}_{1}$ maps each state and
agent to the number of actions available to that agent at that state, and
$\delta:Q_{\mathsf{Act}}\rightarrow Q$ is the function mapping every state and
tuple of one action per agent to the next state, where
$Q_{\mathsf{Act}}:=\cup_{q\in Q}Q_{\mathsf{Act}}(q)$ with
$Q_{\mathsf{Act}}(q):=\\{(q,\alpha_{1},\ldots,\alpha_{k})\mid\forall
a\in\mathsf{Ag},\;\alpha_{a}\in\llbracket 1,d(q,a)\rrbracket\\}$ representing
the set of tuples of actions available to the players at state $q$.

For all $q\in Q$ and $A\subseteq\mathsf{Ag}$, we let
$\mathsf{Act}_{A}(q):=\\{\alpha=(\alpha_{a})_{a\in A}\in\prod_{a\in
A}\\{a\\}\times\llbracket 1,d(q,a)\rrbracket\\}$. Then, for all tuple
$\alpha\in\mathsf{Act}_{A}(q)$ of one action per agent in $A$, we let:

$\mathsf{Succ}(q,\alpha):=\\{q^{\prime}\in
Q\mid\exists\alpha^{\prime}\in\mathsf{Act}_{\mathsf{Ag}\setminus
A}(q),\;\delta(q,(\alpha,\alpha^{\prime}))=q^{\prime}\\}$

When $k=1$, the CGS $C$ is called a _Kripke structure_. In that case, for all
states $q\in Q$, we have the set $\mathsf{Succ}(q)\subseteq Q$ of the
successor states of $Q$.

Finally, we define the size $|C|$ of the structure $C$ by
$|C|=|Q_{\mathsf{Act}}|+|\mathcal{P}|+|\mathsf{Ag}|$.

Unless otherwise stated, a CGS $C$ will always refer to the tuple $C=\langle
Q,I,k,\mathcal{P},\pi,d,\delta\rangle$.

In a CGS, a strategy for an agent is a function that prescribes to the agent
what to do as a function of the history of the game, i.e., the finite sequence
of states seen so far. Moreover, given a coalition of agents and a tuple of
one strategy per agent in the coalition, we define the set of infinite
sequences of states that can occur with this tuple of strategies. Formally, we
define this as follows.

######  Definition 2.

Consider a CGS $C$ and an agent $a\in\mathsf{Ag}$. A _strategy_ for Agent $a$
is a function $s_{a}:Q^{+}\rightarrow\mathbb{N}_{1}$ such that, for all
$\rho=\rho_{0}\dots\rho_{n}\in Q^{+}$, we have $s_{a}(\rho)\leq
d(\rho_{n},a)$. We let $\mathsf{S}_{a}$ denote the set of strategies available
to Agent $a$.

Given a coalition (or subset) of agents $A\subseteq\mathsf{Ag}$, a _strategy
profile_ for the coalition $A$ is a tuple $s=(s_{a})_{a\in A}$ of one strategy
per agent in $A$. We denote by $\mathsf{S}_{A}$ the set of strategy profiles
for the coalition $A$. For all $s\in\mathsf{S}_{A}$ and $q\in Q$, we let
$\mathsf{Out}^{Q}(q,s)\subseteq Q^{\omega}$ denote the set of infinite paths
$\rho$ compatible with $s$ from $q$:

$\mathsf{Out}^{Q}(q,s):=\\{\rho\in Q^{\omega}\mid\rho[0]=q,\;\forall
i\in\mathbb{N},\rho[i+1]\in\mathsf{Succ}(\rho[i],(s_{a}(\rho[:i]))_{a\in
A})\\}$

###  2.2 Alternating-time Temporal Logic

Alternating-time Temporal Logic (ATL) is a temporal logic that takes into
accounts strategic behavior of the agents. It can be seen as a generalization
of Computation Tree Logic (CTL) with more than one agent. There are two
different kinds of ATL formulas: state formulas — where propositions and
strategic operators occur — and path formulas – where temporal operators
occur. To avoid confusion, we denote state formulas and path formulas with
Greek capital letters and Greek lowercase letters, respectively. ATL state
formulas over a set of propositions $\mathcal{P}$ and a set of agents
$\mathsf{Ag}$ are given by the grammar:

$\Phi\Coloneqq p\mid\neg\Phi\mid\Phi\wedge\Phi\mid\langle\\!\langle
A\rangle\\!\rangle\varphi,$

where $p\in\mathcal{P}$ is a proposition, $A\subseteq\mathsf{Ag}$ is a
coalition of agents and $\varphi$ is a path formula. We include the Boolean
constants $\operatorname{\mathit{true}}$ and $\operatorname{\mathit{false}}$
and other operators such as $\Phi\lor\Phi_{2}$ and
$\Phi_{1}\Rightarrow\Phi_{2}$. Next, ATL path formulas are given by the
grammar:

$\varphi\Coloneqq\operatorname{\mathbf{X}}\Phi\mid\Phi\operatorname{\mathbf{U}}\Phi\mid\operatorname{\mathbf{G}}\Phi$

where $\operatorname{\mathbf{X}}$ is the neXt operator,
$\operatorname{\mathbf{U}}$ is the Until operator, and
$\operatorname{\mathbf{G}}$ is the Globally operator. As syntactic sugar, we
allow standard temporal operators $\operatorname{\mathbf{F}}$, the Finally
operator, which is defined in the usual manner: for any coalition of agents
$A\subseteq\mathsf{Ag}$: $\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{F}}\Phi\coloneqq\langle\\!\langle
A\rangle\\!\rangle(\operatorname{\mathit{true}}\operatorname{\mathbf{U}}\Phi)$.

A CTL formula is an ATL formula on a single agent $\mathsf{Ag}=\\{1\\}$. In
particular, the path quantifiers of CTL can be obtained as follows:
$\operatorname{\mathbf{E}\\!}\ \\!\equiv\langle\\!\langle 1\rangle\\!\rangle$
and $\operatorname{\mathbf{A}\\!}\
\\!\equiv\langle\\!\langle\rangle\\!\rangle$.

The size $|\Phi|$ of an ATL formula $\Phi$ is then defined as size of the set
of sub-formulas: $|\Phi|:=|\mathsf{SubF}(\Phi)|$, which is defined inductively
as follows:

  * •

$\mathsf{SubF}(p):=\\{p\\}$ for all $p\in\mathcal{P}$;

  * •

$\mathsf{SubF}(\neg\Phi):=\\{\neg\Phi\\}\cup\mathsf{SubF}(\Phi)$;

  * •

$\mathsf{SubF}(\Phi_{1}\wedge\Phi_{2}):=\\{\Phi_{1}\wedge\Phi_{2}\\}\cup\mathsf{SubF}(\Phi_{1})\cup\mathsf{SubF}(\Phi_{2})$;

  * •

$\mathsf{SubF}(\langle\\!\langle
A\rangle\\!\rangle\\!\bullet\Phi):=\\{\langle\\!\langle
A\rangle\\!\rangle\\!\bullet\Phi\\}\cup\mathsf{SubF}(\Phi)$ for
$\bullet\in\\{\operatorname{\mathbf{X}},\operatorname{\mathbf{G}}\\}$ and
$A\subseteq\mathsf{Ag}$;

  * •

$\mathsf{SubF}(\langle\\!\langle
A\rangle\\!\rangle(\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2})):=\\{\langle\\!\langle
A\rangle\\!\rangle(\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2})\\}\cup\mathsf{SubF}(\Phi_{1})\cup\mathsf{SubF}(\Phi_{2})$
for $A\subseteq\mathsf{Ag}$.

We interpret ATL formulas over CGSs $C$ using the standard definitions [2].
Given a state $q\in Q$, we define when a state formula $\Phi$ holds in state
$q$ — denoted by $q\models\Phi$ — inductively as follows:

$\displaystyle q\models p$ $\displaystyle\text{ iif }p\in\pi(q),$
$\displaystyle q\models\neg\Phi$ $\displaystyle\text{ iif }q\not\models\Phi,$
$\displaystyle q\models\Phi_{1}\wedge\Phi_{2}$ $\displaystyle\text{ iif
}q\models\Phi_{1}\text{ and }q\models\Phi_{2},$ $\displaystyle
q\models\langle\\!\langle A\rangle\\!\rangle\varphi$ $\displaystyle\text{ iif
}\exists
s\in\mathsf{S}_{A},\;\forall\rho\in\mathsf{Out}^{Q}(q,s),\;\rho\models\varphi$

Similarly, given a path $\rho\in Q^{\omega}$ and a path formula $\varphi$, we
define when $\varphi$ holds on path $\rho$, denoted $\rho\models\varphi$ as
above, inductively as follows:

$\displaystyle\rho\models\operatorname{\mathbf{X}}\Phi$ $\displaystyle\text{
iif }\rho[1:]\models\Phi$
$\displaystyle\rho\models\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2}$
$\displaystyle\text{ iif }\exists
j\in\mathbb{N},\;\rho[j]\models\Phi_{2}\text{, and }\forall
k<j,\rho[k:]\models\Phi_{1}$
$\displaystyle\rho\models\operatorname{\mathbf{G}}\Phi$ $\displaystyle\text{
iif }\forall j\in\mathbb{N},\;\rho[j:]\models\Phi$

We say that an ATL formula $\Phi$ accepts (resp. rejects) a state $q$ if
$q\models\Phi$ (resp. $q\not\models\Phi$). We say that it distinguishes two
states $q,q^{\prime}$ if it accepts one and rejects the other. Finally, we
then say that the ATL formula $\Phi$ accepts a CGS $C$, denoted by
$C\models\Phi$, if $\Phi$ accepts all initial states of $C$.

######  Remark 3.

When evaluated on turn-based game structures (i.e., where, at each state, at
most one player has more than one action available), the formulas
$\langle\\!\langle A\rangle\\!\rangle\varphi$ and
$\neg\langle\\!\langle\mathsf{Ag}\setminus A\rangle\\!\rangle\neg\varphi$ are
equivalent (However, it is not the case when they are evaluated on arbitrary
CGSs.)

##  3 Passive Learning for ATL

In this problem, we are given a sample $\mathcal{S}=(P,N)$ consisting of a set
$P$ of positive structures and a set $N$ of negative structures. The goal is
to find a minimal formula $\Phi$ that is _consistent_ with $\mathcal{S}$,
i.e., $\Phi$ must hold on all positive structures and must not hold on any
negative structure. We are specifically searching for a minimal formula and
the reason for this is two-fold: (1) the prospective formula will be more
interpretable, and (2) it will not overfit the sample [42, 48]. Formally:

######  Problem 4 (Passive learning of ATL).

Given a sample $\mathcal{S}=(P,N)$ consisting of two finite sets $P$ and $N$
of concurrent game structures (CGSs) with the same set $\mathsf{Ag}$ of
agents, find a minimal size ATL formula $\Phi$ on $\mathsf{Ag}$ that is
consistent with $\mathcal{S}$.

The passive learning problem of CTL can be obtained by simplifying Problem 4
by use of a single agent $\mathsf{Ag}=\\{1\\}$, which reduces CGSs to KSs and
ATL to CTL.

Before describing our solution to Problem 4, we briefly discuss the source of
the positive and negative structures. Passive learning, among several
applications, constitutes a critical subroutine of certain learning
frameworks. Active learning [5], which involves learning black-box systems by
interacting with a teacher, often involves repeated passive learning on the
counter-example models, i.e., the feedback, received from the teacher [20].
Furthermore, one-class classification, or learning from positive examples,
leverages passive learning to derive candidate formulas [9, 49]. These
formulas facilitate the generation of negative examples, which help refine the
search for more concise and descriptive formulas.

A concrete application of Problem 4 would be to provide contrastive
explanations [32] in a multi-agent setting. Consider a multi-agent system that
is deemed to have some “good” positions and some “bad” positions. This system
would yield positive and negative CGSs corresponding to the good and bad
positions. To explain the dichotomy between these good and bad positions, one
can learn an ATL formula that accepts the positive CGSs and rejects the
negative ones.

###  3.1 SAT-based Learning Algorithm

Our approach to solving Problem 4 is by reducing it to satisfiability problems
in propositional logic. We thus provide a brief introduction to propositional
logic.

##### Propositional Logic.

Let $\mathsf{Var}$ be a set of propositional variables that can be set to
Boolean values from $\mathbb{B}=\\{0,1\\}$ (0 representing
$\operatorname{\mathit{false}}$ and 1 representing
$\operatorname{\mathit{true}}$). Formulas in Propositional Logic are
inductively constructed as follows:

$\Omega\Coloneqq\operatorname{\mathit{true}}\mid\operatorname{\mathit{false}}\mid
x\in\mathsf{Var}\mid\lnot\Omega\mid\Omega\lor\Omega\mid\Omega\wedge\Omega\mid\Omega\Rightarrow\Omega\mid\Omega\Leftrightarrow\Omega$

To avoid confusion with ATL formulas, we will be exclusively using the letter
$\Omega$ (along with its variants) to denote propositional formulas.

To assign values to propositional variables, we rely on a valuation function
$v:\mathsf{Var}\to\mathbb{B}$. We exploit the valuation function $v$ to define
the satisfaction $v\models\Omega$ of a propositional formula $\Omega$; we use
standard definitions for this. When $v\models\Omega$, we say that $v$
satisfies $\Omega$ and call it a _satisfying valuation_ of $\Omega$. A formula
$\Omega$ is _satisfiable_ if there exists a satisfying valuation $v$ of
$\Phi$. The satisfiability (SAT) problem for propositional logic is a well-
known $\mathsf{NP}$-complete problem, which asks if a propositional formula
given as input is satisfiable. To handle SAT, numerous optimized decision
procedures have been designed in recent years [41, 8, 11].

We now describe a reduction of Problem 4 to SAT, inspired by [42, 20].
Following their work, we design a propositional formula
$\Omega^{\mathcal{S}}_{n}$ that enables the search for an ATL formula of size
at most $n$ that is consistent with a sample $\mathcal{S}$. The formula
$\Omega^{\mathcal{S}}_{n}$ has the following properties:

  1. 1.

$\Omega^{\mathcal{S}}_{n}$ is satisfiable if and only if there exists an ATL
formula of size at most $n$ that is consistent with $\mathcal{S}$; and

  2. 2.

from a satisfying valuation of $\Omega^{\mathcal{S}}_{n}$, one can easily
extract a suitable ATL formula of size at most $n$.

One can then iteratively search for a minimal, consistent formula: for
increasing values of $n$, if $\Omega^{\mathcal{S}}_{n}$ is satisfiable,
extract a consistent ATL formula.

The formula $\Omega^{\mathcal{S}}_{n}$ is defined as a conjunction of
subformulas with distinct roles:
$\Omega^{\mathcal{S}}_{n}\coloneqq\Omega^{\mathsf{str}}_{n}\wedge\Omega^{\mathsf{sem}}_{n}\wedge\Omega^{\mathsf{con}}_{n}$.
The subformula $\Omega^{\mathsf{str}}$ encodes the structure of the
prospective ATL formula $\Phi$. The subformula $\Omega^{\mathsf{sem}}$ encodes
that the correct semantics of ATL is used to interpret the prospective ATL
formula on the given CGSs. Finally, the subformula $\Omega^{\mathsf{con}}$
ensures that the prospective ATL formula holds on the models in $P$ and not in
the models in $N$. The formula used for CTL learning has an identical high-
level structure, with similar subformulas.

We now describe the subformulas of $\Omega^{\mathcal{S}}_{n}$ in detail.

##### Encoding the structure of ATL formulas.

The structure of an ATL formula is symbolically encoded as a _syntax DAG_. A
syntax DAG of an ATL formula is simply a syntax tree in which the common nodes
are merged. Figure 1 depicts an example of a syntax tree and DAG of an ATL
formula.

$\lor$$\langle\\!\langle
1\rangle\\!\rangle\\!\operatorname{\mathbf{U}}$$\langle\\!\langle
2\rangle\\!\rangle\\!\operatorname{\mathbf{X}}$$p$$\langle\\!\langle
1,\\!3\rangle\\!\rangle\\!\operatorname{\mathbf{G}}$$q$645321

Figure 1: Syntax DAG with identifiers (indicated above nodes) of
$\langle\\!\langle
2\rangle\\!\rangle\\!\operatorname{\mathbf{X}}p\lor\langle\\!\langle
1\rangle\\!\rangle(p\operatorname{\mathbf{U}}\langle\\!\langle
1,\\!3\rangle\\!\rangle\\!\operatorname{\mathbf{G}}q)$.

To conveniently encode the syntax DAG of an ATL formula, we first fix a naming
convention for its nodes. For a formula of size at most $n$, we assign to each
of its nodes an identifier in $\llbracket 1,n\rrbracket$ such that the
identifier of each node is larger than those of its children, if applicable.
Note that such a naming convention may not be unique. We then denote the sub-
formula of $\Phi$ rooted at Node $i$ as $\Phi[i]$. Thus, $\Phi[n]$ denotes the
entire formula $\Phi$.

Next, to encode a syntax DAG symbolically, we introduce the following
propositional variables: (i) $x_{i,\lambda}$ for $i\in\llbracket
1,n\rrbracket$ and $\lambda\in\mathcal{P}\cup\Lambda$ with
$\Lambda:=\\{\neg,\wedge,\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{X}},\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{G}},\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{U}}\\}$;
(ii) $A_{i,a}$ for $i\in\llbracket 1,n\rrbracket$ and $a\in\mathsf{Ag}$; and
(iii) $l_{i,j}$ and $r_{i,j}$ for $i\in\llbracket 1,n\rrbracket$ and
$j\in\llbracket 1,i-1\rrbracket$. The variable $x_{i,\lambda}$ tracks the
operator labeled in Node $i$, meaning, $x_{i,\lambda}$ is set to true if and
only if Node $i$ is labeled with $\lambda$. The variable $A_{i,a}$ is relevant
only if $x_{i,\langle\\!\langle\cdot\rangle\\!\rangle\bullet}$ is set to true
for some temporal operator
$\bullet\in\\{\operatorname{\mathbf{X}},\operatorname{\mathbf{G}},\operatorname{\mathbf{U}}\\}$.
In such a case, the variables $(A_{i,a})_{a\in\mathsf{Ag}}$ track which agents
are in the coalition $\langle\\!\langle\cdot\rangle\\!\rangle$ at Node $i$.
The variable $l_{i,j}$ (resp., $r_{i,j}$) tracks the left (resp., right) child
of Node $i$, meaning, $l_{i,j}$ (resp., $r_{i,j}$) is set to true if and only
if the left (resp., right) child of Node $i$ is Node $j$.

To ensure that these variables encode a valid syntax DAG, we impose structural
constraints similar to the ones proposed by Neider and Gavran [42]. For
instance, the constraint below ensures that each node is labeled with a unique
operator:

$\Big{[}\bigwedge_{i\in\llbracket
1,n\rrbracket}\bigvee_{\lambda\in\Lambda}x_{i,\lambda}\Big{]}\land\Big{[}\bigwedge_{i\in\llbracket
1,n\rrbracket}\bigwedge_{\lambda\neq\lambda^{\prime}\in\Lambda}\lnot
x_{i,\lambda}\lor\lnot x_{i,\lambda^{\prime}}\Big{]}$

We impose similar constraints to ensure that each node has a unique left and
right child. We detail all the structural constraints in Appendix A. The
formula $\Omega^{\mathsf{str}}_{n}$ is simply the conjunction of all such
structural constraints.

Based on a satisfying valuation $v$ of $\Omega^{\mathsf{str}}_{n}$, one can
construct a unique ATL formula: label each Node $i$ with the operator
$\lambda$ for which $v(x_{i,\lambda})=1$, include players in a coalition for
which $v(A_{i,a})=1$, and mark the left (resp., right) child with Nodes $j$
(resp., $j^{\prime}$) for which $v(l_{i,j})=1$ (resp.,
$v(r_{i,j^{\prime}})=1$).

For encoding the structure of (the existential fragment of) CTL, the only
difference from that of ATL is that the set of operators is
$\Lambda\coloneqq\\{\neg,\wedge,\operatorname{\mathbf{E}\\!}\operatorname{\mathbf{X}},\operatorname{\mathbf{E}\\!}\operatorname{\mathbf{G}},\operatorname{\mathbf{E}\\!}\operatorname{\mathbf{U}}\\}$.

##### Encoding the semantics of ATL formulas.

To symbolically encode the semantics of the prospective ATL formula $\Phi$ for
a given CGS $C$, we rely on encoding the ATL model-checking procedure
developed in [2, Section 4]. The procedure involves calculating, for each sub-
formula $\Phi^{\prime}$ of $\Phi$, the set
$\mathtt{SAT}_{C}(\Phi^{\prime})=\\{q\in Q\mid q\models\Phi^{\prime}\\}$ of
the states of $C$ where $\Phi^{\prime}$ holds. Since we consider ATL formulas,
we need to handle the strategic operators $\langle\\!\langle
A\rangle\\!\rangle$ for $A\subseteq\mathsf{Ag}$. To do so, given a coalition
of agents $A\subseteq\mathsf{Ag}$ and some subset of states $S\subseteq Q$, we
let $\mathsf{Pre}_{A}(S)\subseteq Q$ denote the set of states from which the
coalition $A$ has a strategy to enforce reaching the set $S$ in one step. That
is: $\mathsf{Pre}_{A}(S):=\\{q\in
Q\mid\exists\alpha\in\mathsf{Act}_{A}(q),\;\mathsf{Succ}(q,\alpha)\subseteq
S\\}$.

We can now describe how to compute the set $\mathtt{SAT}_{C}(\Phi)$. It is
done inductively on the structure of the ATL formula $\Phi$ as follows:

$\displaystyle\mathtt{SAT}_{C}(p)=\\{q\in Q~{}|~{}p\in\pi(q)\\},\text{ for any
}p\in\mathcal{P},$ (1)
$\displaystyle\mathtt{SAT}_{C}(\Phi\wedge\Psi)=\mathtt{SAT}_{C}(\Phi)\cap\mathtt{SAT}_{C}(\Psi),$
(2)
$\displaystyle\mathtt{SAT}_{C}(\neg\Phi)=Q\setminus\mathtt{SAT}_{C}(\Phi),$
(3) $\displaystyle\mathtt{SAT}_{C}(\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi)=\mathsf{Pre}_{A}(\mathtt{SAT}_{C}(\Phi)),$
(4) $\displaystyle\mathtt{SAT}_{C}(\langle\\!\langle
A\rangle\\!\rangle(\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2}))\text{ is the
smallest }T\subseteq Q,\text{ such that }$ $\displaystyle\hskip 28.45274pt(1)\
\mathtt{SAT}_{C}(\Phi_{2})\subseteq T\text{ and }(2)\
\mathtt{SAT}_{C}(\Phi_{1})\cap\mathsf{Pre}_{A}(T)\subseteq T,$ (5)
$\displaystyle\mathtt{SAT}_{C}(\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{G}}\Phi)\text{ is the largest
}T\subseteq Q,\text{ such that }$ $\displaystyle\hskip 28.45274pt(1)\
T\subseteq\mathtt{SAT}_{C}(\Phi)\text{ and }(2)\
T\subseteq\mathsf{Pre}_{A}(T)$ (6)

Our goal is to symbolically encode the above-described computation. To do so,
we introduce the propositional variables $y^{C}_{i,q}$ for each
$i\in\llbracket 1,n\rrbracket$, $q\in Q$ that track whether a state $q\in Q$
belongs to $\mathtt{SAT}_{C}(\Phi[i])$ for a sub-formula $\Phi[i]$ of $\Phi$.
That is, $y^{C}_{i,q}$ is set to true if and only if $\Phi[i]$ holds in state
$q$, i.e. $q\in\mathtt{SAT}_{C}(\Phi[i])$.

Before defining the propositional formulas that ensure the desired meaning of
the variables $y^{C}_{i,q}$, we introduce formulas to keep track of whether a
state belongs to the set $\mathsf{Pre}_{A}(S)$. Formally, for all $q\in Q$ and
$i\in\llbracket 1,n\rrbracket$, given any predicate
$y_{S}:Q\Rightarrow\mathbb{B}$ (encoding a set $S=(y_{S})^{-1}[true]\subseteq
Q$), we define the formula $\Omega_{q,i}^{\mathsf{Pre}}(y_{S})$ that encodes
the fact that $q\in\mathsf{Pre}_{A_{i}}(S)$, where $A_{i}$ is the coalition of
agents defined by the variables $(A_{i,a})_{a\in\mathsf{Ag}}$. This formula is
defined as follows:

$\Omega_{q,i}^{\mathsf{Pre},C}(y_{S}):=\bigvee_{\alpha\in\mathsf{Act}_{\mathsf{Ag}}(q)}\bigwedge_{\alpha^{\prime}\in\mathsf{Act}_{\mathsf{Ag}}(q)}\big{[}(\bigwedge_{a\in\mathsf{Ag}}A_{i,a}\Rightarrow(\alpha_{a}=\alpha^{\prime}_{a}))\Rightarrow
y_{S}(\delta(q,\alpha^{\prime}))\big{]}$

This formula can be informally read as follows: there exists an action tuple
for the coalition $A$ (the disjunction), such that for all action tuples for
the opposing coalition (the conjunction), the corresponding state is in the
set $S$ (indicated by $y_{S}(\delta(q,\alpha^{\prime}))$). Since we do not
know, a priori, what the coalition $A_{i}$ is, we quantify over action tuples
for all the agents both in the disjunction and the conjunction. However, the
rightmost implication of the formula ensures that the only relevant tuples of
actions $\alpha^{\prime}\in\mathsf{Act}_{\mathsf{Ag}}(q)$ are those for which
the action for the agents in the coalition $A_{i}$ are given by the tuple of
actions $\alpha\in\mathsf{Act}_{\mathsf{Ag}}(q)$.

We define the formulas ensuring the intended meaning of the variables
$y_{i,q}$.

$\displaystyle\Omega^{\mathsf{sem}}_{\mathcal{P},C}$
$\displaystyle:=\bigwedge_{p\in\mathcal{P}}\bigwedge_{i\in\llbracket
1,n\rrbracket}\Big{[}x_{i,p}\Rightarrow\bigwedge_{q\in
Q,\;p\in\pi(q)}y^{C}_{i,q}\;\wedge\bigwedge_{q\in Q,\;p\notin\pi(q)}\neg
y^{C}_{i,q}\Big{]}$ $\displaystyle\Omega^{\mathsf{sem}}_{\wedge,C}$
$\displaystyle:=\bigwedge_{\begin{subarray}{c}{i\in\llbracket
1,n\rrbracket}\\\ {j,j^{\prime}\in\llbracket
1,i-1\rrbracket}\end{subarray}}\Big{[}[x_{i,\wedge}\wedge l_{i,j}\wedge
r_{i,j^{\prime}}]\Rightarrow\bigwedge_{q\in
Q}\big{[}y^{C}_{i,q}\Leftrightarrow[y^{C}_{j,q}\wedge
y^{C}_{j^{\prime},q}]\big{]}\Big{]}$
$\displaystyle\Omega^{\mathsf{sem}}_{\neg,C}$
$\displaystyle:=\bigwedge_{\begin{subarray}{c}{i\in\llbracket
1,n\rrbracket}\\\ {j\in\llbracket
1,i-1\rrbracket}\end{subarray}}\Big{[}[x_{i,\neg}\wedge
l_{i,j}]\Rightarrow\bigwedge_{q\in Q}\big{[}y^{C}_{i,q}\Leftrightarrow\neg
y^{C}_{j,q}\big{]}\Big{]}$
$\displaystyle\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{X}},C}$
$\displaystyle:=\bigwedge_{\begin{subarray}{c}{i\in\llbracket
1,n\rrbracket}\\\ {j\in\llbracket
1,i-1\rrbracket}\end{subarray}}\Big{[}[x_{i,\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{X}}}\wedge
l_{i,j}]\Rightarrow\bigwedge_{q\in
Q}\big{[}y^{C}_{i,q}\Leftrightarrow\Omega_{q,i}^{\mathsf{Pre},C}(y^{C}_{j,\cdot})\big{]}\Big{]}$

The above formulas encode, via a straightforward translation, the
$\mathtt{SAT}_{C}$ computation for the propositions, Boolean operators and the
$\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{X}}$
operator.

The case of the
$\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{U}}$ and
$\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{G}}$
operators require some innovation. Indeed, as can be seen in Equations (5) and
(6), the $\mathtt{SAT}_{C}$ involves a least and greatest fixed-point,
respectively. To circumvent this difficulty, we mimic the steps of the fixed-
point computation algorithm [2, Fig. 3] in propositional logic. Let us recall
how they are computed. Given an ATL formula $\Phi=\langle\\!\langle
A\rangle\\!\rangle\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2}$, the way
$\mathtt{SAT}_{C}(\Phi)$ is computed from $\mathtt{SAT}_{C}(\Phi_{1})$ and
$\mathtt{SAT}_{C}(\Phi_{2})$ is described in Algorithm 1. Similarly, given an
ATL formula $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{G}}\Phi^{\prime}$, the way
$\mathtt{SAT}_{C}(\Phi)$ is computed from $\mathtt{SAT}_{C}(\Phi^{\prime})$ is
described in Algorithm 2. Note that, instead of using _while_ loops, as in [2,
Fig. 3], that are necessarily exited after at most $|Q|$ steps, we use _for_
loops.

Algorithm 1 Compute $\mathtt{SAT}_{C}(\Phi)$ for $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\;\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2}$ a

Input: CGS $C$, coalition $A$, $\mathtt{SAT}_{C}(\Phi_{1})$ and
$\mathtt{SAT}_{C}(\Phi_{2})$

1:$S\coloneqq\mathtt{SAT}_{C}(\Phi_{2})$

2:for $1\leq k\leq|Q|$ do

3: $S\leftarrow
S\cup\\{q\in\mathtt{SAT}_{C}(\Phi_{1})\cap\mathsf{Pre}_{A}(S)\\}$

4:end forreturn $S$

Algorithm 2 Compute $\mathtt{SAT}_{C}(\Phi)$ for $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\;\operatorname{\mathbf{G}}\Phi^{\prime}$

Input: CGS $C$, coalition $A$ and $\mathtt{SAT}_{C}(\Phi^{\prime})$

1:$S\coloneqq\mathtt{SAT}_{C}(\Phi^{\prime})$

2:for $1\leq k\leq|Q|$ do

3: $S\leftarrow S\cap\mathsf{Pre}_{A}(S)$

4:end forreturn $S$

As can be seen in both algorithms, the fixed-point computation algorithm
internally maintains an estimate of the $\mathtt{SAT}_{C}$ set and updates it
iteratively. Thus, to encode the fixed-point computation, we introduce
propositional variables that encode whether a state $q$ of a CGS $C$ belongs
to a particular estimate of $\mathtt{SAT}_{C}$. Formally, we introduce
propositional variables $y^{C}_{i,q,k}$ for each $i\in\llbracket
1,n\rrbracket$, $q\in A$, and $k\in\llbracket 0,|Q|\rrbracket$, where the
parameter $k\in\llbracket 0,|Q|\rrbracket$ tracks which iterative step of the
fixed-point computation the variable $y^{C}_{i,q,k}$ encodes. We define the
formulas below to ensure the intended meaning of these introduced variables:

$\displaystyle\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{U}},C}$
$\displaystyle:=\bigwedge_{\begin{subarray}{c}{i\in\llbracket
1,n\rrbracket}\\\ {j,j^{\prime}\in\llbracket
1,n\rrbracket}\end{subarray}}[x_{i,\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{U}}}\wedge
l_{i,j}\wedge r_{i,j^{\prime}}]\Rightarrow\bigwedge_{q\in
Q}\Big{[}\big{[}y^{C}_{i,q,0}\Leftrightarrow
y^{C}_{j^{\prime},q}\big{]}\wedge$ $\displaystyle\hskip
25.60747pt\bigwedge_{0\leq
k\leq|Q|-1}\big{[}y^{C}_{i,q,k+1}\Leftrightarrow[y^{C}_{i,q,k}\vee[y^{C}_{j,q}\wedge\Omega_{q,i}^{\mathsf{Pre}}(y^{C}_{i,\cdot,k})]]\big{]}\wedge\;[y^{C}_{i,q}\Leftrightarrow
y^{C}_{i,q,|Q|}]\Big{]}$
$\displaystyle\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{G}},C}$
$\displaystyle:=\bigwedge_{\begin{subarray}{c}{i\in\llbracket
1,n\rrbracket}\\\ {j\in\llbracket
1,i-1\rrbracket}\end{subarray}}[x_{i,\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{G}}}\wedge
l_{i,j}]\Rightarrow\bigwedge_{q\in
Q}\Big{[}\big{[}y^{C}_{i,q,0}\Leftrightarrow y^{C}_{j,q}\big{]}\wedge$
$\displaystyle\hskip 56.9055pt\bigwedge_{0\leq
k\leq|Q|-1}\big{[}y^{C}_{i,q,k+1}\Leftrightarrow[y^{C}_{i,q,k}\wedge\Omega_{q,i}^{\mathsf{Pre}}(y^{C}_{i,\cdot,k})]\big{]}\wedge\;[y^{C}_{i,q}\Leftrightarrow
y^{C}_{i,q,|Q|}]\Big{]}$

The formula $\Omega^{\mathsf{sem}}_{n}$ is simply defined as the conjunction
of all the formulas above.

For the semantics of CTL, the main difference is that the formula
$\Omega_{q,i}^{\mathsf{Pre}}(y_{S})$ encoding the fact that
$q\in\mathsf{Pre}(S)$ can be greatly simplified (for the quantifier
$\operatorname{\mathbf{E}\\!}$ ):

$\hat{\Omega}_{q,i}^{\mathsf{Pre}}(y_{S}):=\bigvee_{q^{\prime}\in\mathsf{Succ}(q)}y_{S}(q^{\prime})$

##### Encoding the consistency with the models

Finally, to encode that the prospective formula is consistent with
$\mathcal{S}$, we have the following formula:

$\Omega^{\mathsf{con}}_{n}:=\big{[}\bigwedge_{C\in P}\bigwedge_{s\in
I}y^{C}_{n,s}\big{]}\wedge\big{[}\bigwedge_{C\in N}\bigvee_{s\in I}\neg
y^{C}_{n,s}\big{]}$

The size of the formula $\Omega^{\mathcal{S}}_{n}$, and the number of
variables involved in it, is polynomial in $n$ and the size of $\mathcal{S}$,
$|\mathcal{S}|\coloneqq\sum_{C\in P\cup N}|C|$. To express this formally, let
us first introduce notations for various quantities that will occur when
expressing the size of the different formulas involved.

######  Definition 5.

Consider a sample $S=(P,N)$ of CGS. We let: $x:=|\Lambda|=5+|\mathcal{P}|$,
$k:=|\mathsf{Ag}|$, $r=\max_{q\in Q}|Q_{\mathsf{Act}}(q)|$, for all $C\in
P\cup N$, $m_{C}:=|Q_{C}|$ for $Q_{C}$ the of states of the structure $C$ and
$m:=|Q|$ for $Q:=\cup_{C\in P\cup N}Q_{C}$.

Now, by looking how the different formulas are defined, we obtain the
following (asymptotic) bounds:

  * •

$|\Omega_{\Lambda}|=O(n\cdot x^{2})$;

  * •

$|\Omega_{l}|=O(n^{3})$;

  * •

$|\Omega_{r}|=O(n^{3})$;

  * •

$|\Omega_{\mathcal{P}}|=O(x)$.

Hence, we obtain $|\Omega_{n}^{str}|=O(n^{3}+n^{2}\cdot x)$. In addition, for
all $C\in P\cup N$, we have:

  * •

$|\Omega_{\mathcal{P},C}^{\mathsf{sem}}|=O(x\cdot n\cdot m_{C})$;

  * •

$|\Omega_{\wedge,C}^{\mathsf{sem}}|=O(n^{3}\cdot m_{C})$;

  * •

$|\Omega_{\neg,C}^{\mathsf{sem}}|=O(n^{2}\cdot m_{C})$;

  * •

For all states $q\in Q$ and $i\leq n$, we have
$|\Omega_{q,i}^{\mathsf{Pre},C}(y)|=O(r^{2}\cdot k)$;

  * •

$|\Omega_{\operatorname{\mathbf{X}},C}^{\mathsf{sem}}|=O(n^{2}\cdot m_{C}\cdot
r^{2}\cdot k)$;

  * •

$|\Omega_{\operatorname{\mathbf{U}},C}^{\mathsf{sem}}|=O(n^{3}\cdot
m_{C}^{2}\cdot r^{2}\cdot k)$;

  * •

$|\Omega_{\operatorname{\mathbf{G}},C}^{\mathsf{sem}}|=O(n^{2}\cdot
m_{C}^{2}\cdot r^{2}\cdot k)$.

Overall, we obtain $|\Omega_{n}^{\mathsf{sem}}|=O(n^{3}\cdot m^{2}\cdot
r^{2}\cdot k+x\cdot n\cdot m)$. Finally, we have
$|\Omega_{n}^{\mathsf{con}}|=O(m)$. We do obtain that the size of
$\Omega_{n}^{\mathsf{S}}$ is (asymptotically) polynomial in $|S|$ and $n$.

Furthermore, we have the lemma below establishing the correctness of the
encoding. A detailed proof of this proposition can be found in Appendix B.

######  Proposition 6.

Let $\mathcal{S}=(P,N)$ be a sample and $n\in\mathbb{N}\setminus\\{0\\}$ .
Then:

  1. 1.

If an ATL formula of size at most $n$ consistent with $\mathcal{S}$ exists,
then the propositional formula $\Omega^{\mathcal{S}}_{n}$ is satisfiable.

  2. 2.

If a valuation $v$ is such that $v\models\Omega^{\mathcal{S}}_{n}$, then there
is an ATL formula $\Phi^{v}$ of size at most $n$ that is consistent with
$\mathcal{S}$.

###  3.2 Deciding the separability

Given a sample $\mathcal{S}$, by iteratively checking if
$\Omega^{\mathcal{S}}_{0}$ is satisfiable, if $\Omega^{\mathcal{S}}_{1}$ is
satisfiable, etc., we can find a minimal size formula consistent with
$\mathcal{S}$ if one exists. However, if there is no such formula, the above
iteration would not terminate. To circumvent that issue, there are two
possibilities. We may first decide the separability of the sample, i.e. decide
if there exists an ATL formula consistent with it; or we may exhibit a bound
$B$, expressed as a function of $\mathcal{S}$, such that if there is a
separating formula, there is one of size at most $B$. In this subsection, we
tackle both of these issues.

It was shown in [18, Section 3, Thm. 3.2, 3.9] that the separability can be
decided in polynomial time for full CTL (i.e., all operators can be used) with
Kripke structures. Furthermore, in [44, Coro. 1], the results of [18] are used
to exhibit an exponential bound on the size of the CTL formulas to be
considered.

For fragments of CTL (i.e. CTL formulas that can use only some operators), it
was shown in [35, Thm. 3], as a corollary of a “meta theorem” with
applications to various logic, that the separability can be decided in
exponential time.

Here, we extend these results to ATL formulas. We consider two settings: full
ATL and any fragment of ATL. In the first setting, we show that separability
can also be decided in polynomial time. In the second setting, we show that
separability can be decided in exponential time. We deduce an exponential
bound on the size of the formulas that need to be considered, which hold
regardless of the fragment considered (including full ATL).

####  3.2.1 Separability for full ATL.

For full ATL, our goal is to show the theorem below.

######  Theorem 7.

Given a sample $\mathcal{S}=(P,N)$ of CGS, we can decide in time polynomial in
$|\mathcal{S}|$ if the sample $\mathcal{S}$ is separable with (arbitrary) ATL
formulas.

What we are actually going to prove is Lemma 9, that we state below,
establishing the result of Theorem 7 for all fragments of ATL with the
operators $\neg,\wedge$ and $\operatorname{\mathbf{X}}$. Let us first
introduce formally these fragments.

######  Definition 8.

We let
$\mathsf{OP}:=\\{\neg,\wedge,\operatorname{\mathbf{X}},\operatorname{\mathbf{G}},\operatorname{\mathbf{U}}\\}$
denote the set of operators that can be used in (regular) ATL formulas.

For all subsets of operators $\mathsf{O}\subseteq\mathsf{Op}$, we let
$\mathbf{ATL}(\mathsf{O})$ denote the set of ATL formulas using only operators
in $\mathsf{O}$. When $\mathsf{O}=\mathsf{OP}$, $\mathbf{ATL}(\mathsf{O})$ is
simply denoted $\mathbf{ATL}$.

We let $\mathsf{OPn}:=\\{\neg,\wedge,\operatorname{\mathbf{X}}\\}$ and we
refer to formula in the fragment $\mathbf{ATL}(\mathsf{OPn})$ as
ATL-$\operatorname{\mathbf{X}}$ formulas.

For simplicity, in the following, we allow ATL-$\operatorname{\mathbf{X}}$
formulas to use the classical operator $\lor$ since
$\Phi_{1}\lor\Phi_{2}\equiv\neg(\neg\Phi_{1}\wedge\neg\Phi_{2})$ for all ATL
formulas $\Phi_{1}$ and $\Phi_{2}$.

We want to establish of this section the lemma below.

######  Lemma 9.

Consider any subset of operators
$\mathsf{OPn}\subseteq\mathsf{O}\subseteq\mathsf{OP}$, and a sample $S=(P,N)$
of CGS. We can decide in time $O(n^{6}\cdot r^{6}+n^{4}\cdot k+n^{2}\cdot p)$
if the sample $S$ is separable with $\mathbf{ATL}(\mathsf{O})$ formulas.

The proof of this lemma uses ideas similar to what is presented [18] with CTL
formulas. Before we proceed to the proof of this lemma, we introduce some
notations below.

######  Definition 10.

Consider a sample $S=(P,N)$ of CGS. For all CGS $C\in P\cup N$, we let $Q_{C}$
(resp. $I_{C}\subseteq Q_{C}$) denote the set of (resp. initial) states of the
structure $C$. When the sample $S$ is clear from context, we let
$Q:=\cup_{C\in P\cup N}Q_{C}$ denote the set of all the states occurring in
$S$. We also let $\mathsf{Ag}$ denote the set of agents occurring in all CGS
of $S$ and we let $\mathcal{P}$ denote the set of all the propositions
occurring in at least one CGS on $S$.

Whenever a function in $\pi,d,\delta,\mathsf{Act},\mathsf{Succ}$ is applied to
a state $q\in Q$, we always assume that it is the function from the CGS $C$
such that $q\in Q_{C}$.

We also introduce below the notations on samples that we will use in the
following to write complexity bounds.

######  Definition 11.

Consider a sample $S=(P,N)$ of CGS. For all states $q\in Q$, we let:

$||q||:=|Q_{\mathsf{Act}}(q)|$

Note that, for all CGS $C\in P\cup N$, we have
$|(Q_{C})_{\mathsf{Act}}|=\sum_{q\in Q_{C}}||q||$.

We let $r:=\max_{q\in Q}||q||$, $M:=|Q_{\mathsf{Act}}|$, $n:=|Q|$,
$p:=|\mathcal{P}|$ and $k:=|\mathsf{Ag}|$.

Now, the first step that we take is to prove that it is sufficient to consider
only ATL-$\operatorname{\mathbf{X}}$ formulas.This may seem counterintuitive
since given an ATL formula $\Phi$ using the operator
$\operatorname{\mathbf{G}}$ (or the operator $\operatorname{\mathbf{U}}$),
there does not exist ATL-$\operatorname{\mathbf{X}}$ formula equivalent to
$\Phi$ because the number of states of the CGS on which $\Phi$ may be
evaluated is arbitrarily large. However, given a sample $\mathcal{S}$ of
finitely many CGS, there is a bound on the number of states used in all the
CGS of $\mathcal{S}$. Hence, there is an ATL-$\operatorname{\mathbf{X}}$
formula equivalent to $\Phi$ on all the CGS of $\mathcal{S}$.

######  Lemma 12.

Consider a sample $\mathcal{S}=(P,N)$ of CGS and any subset of operators
$\mathsf{OPn}\subseteq\mathsf{O}\subseteq\mathsf{OP}$. If there exists an
$\mathbf{ATL}(\mathsf{O})$ formula consistent with $\mathcal{S}$, then there
is one that is an ATL-$\operatorname{\mathbf{X}}$ formula.

Note that this lemma is known for a long time in the context of CTL formulas
and Kripke structures, see [18, Theorem 3.2, 3.9]. Furthermore, the proof of
this lemma is not complicated, but quite cumbersome as it requires to handle
all the operators $\operatorname{\mathbf{G}},\operatorname{\mathbf{U}}$,etc,
it is therefore postponed to Appendix C.1.

Let us now consider the set $\mathsf{Distinguish}(\mathcal{S})\subseteq Q^{2}$
of pairs of states that we can distinguish with an
ATL-$\operatorname{\mathbf{X}}$ formula.

######  Definition 13.

Consider a sample $\mathcal{S}$ of CGS. We let $Q$ denote the set of all the
states occurring in all CGS of $\mathcal{S}$. We let:

$\mathsf{Distinguish}(\mathcal{S})\coloneqq\\{(q,q^{\prime})\in
Q^{2}~{}|~{}\text{there is ATL-$\operatorname{\mathbf{X}}$ formula }\Phi\text{
s.t. }q\models\Phi\Leftrightarrow q^{\prime}\not\models\Phi\\}$

Given a sample $\mathcal{S}$, we claim the following: 1) it is possible to
compute in time polynomial in $|\mathcal{S}|$ the set
$\mathsf{Distinguish}(\mathcal{S})$, and 2) given
$\mathsf{Distinguish}(\mathcal{S})\subseteq Q^{2}$, we can decide in
polynomial time if there is an ATL-$\operatorname{\mathbf{X}}$ formula
consistent with $\mathcal{S}$.

The second claim is actually a straightforward consequence of the lemma below.

######  Lemma 14.

Consider a sample $S=(P,N)$ of CGS. There is an
ATL-$\operatorname{\mathbf{X}}$ formula consistent with $S$ if and only if for
all $C_{N}\in N$, there some state $q_{C_{N}}\in I_{C_{N}}$ such that, for all
$C_{P}\in P$ and states $q_{C_{P}}\in I_{C_{P}}$, we have
$(q_{C_{P}},q_{C_{N}})\in\mathsf{Distinguish}(S)$.

###### Proof.

Assume that there is an ATL-$\operatorname{\mathbf{X}}$ formula $\Phi$
consistent with $S$. Then, for all $C_{N}\in N$, there is some state
$q_{C_{N}}\in I_{C_{N}}$ such that $q_{C_{N}}\not\models\Phi$. Furthermore,
for all $C_{P}\in P$ and states $q_{C_{P}}\in I_{C_{P}}$, we have
$q_{C_{P}}\models\Phi$. Hence,
$(q_{C_{P}},q_{C_{N}})\in\mathsf{Distinguish}(S)$.

On the other hand, for all $C_{N}\in N$, $C_{P}\in P$ and states $q_{C_{P}}\in
I_{C_{P}}$, we let $\Phi_{q_{C_{P}},q_{C_{N}}}$ be an ATL formula that accepts
$q_{C_{P}}$ and rejects $q_{C_{N}}$. Then, we let $\Phi:=\lor_{C_{P}\in
P}\lor_{q_{C_{P}}\in I_{C_{P}}}(\wedge_{C_{N}\in
N}\Phi_{q_{C_{P}},q_{C_{N}}})$ be an ATL-$\operatorname{\mathbf{X}}$ formula.
By construction, this ATL-$\operatorname{\mathbf{X}}$ formula $\Phi$ is
consistent with $S$.∎

Let us now consider the first claim. Our goal is to compute the set
$\mathsf{Distinguish}(S)$ in polynomial tine. To do so, we are going to
iteratively add to the empty set pairs of states that can be distinguished by
ATL-$\operatorname{\mathbf{X}}$ formulas.

Before we define what sets of states we add at each state, let us define the
notion of relevant agents, given any pair of states.

######  Definition 15.

Consider a sample $S=(P,N)$ of CGS. For all pairs of states $(q,q^{\prime})\in
Q^{2}$, we let $\mathsf{RelAg}(q,q^{\prime})\subseteq\mathsf{Ag}$ be equal to:

$\mathsf{RelAg}(q,q^{\prime}):=\\{a\in\mathsf{Ag}\mid d(q,a)\cdot
d(q^{\prime},a)\geq 2\\}$

Note that, for convenience, for the empty coalition $\emptyset$, we let
$\mathsf{Act}_{\emptyset}(q):=\\{\epsilon\\}$, for all states $q\in Q$, where
$\epsilon$ is an empty tuple of actions.

The way we add states at every step is now defined below.

######  Definition 16.

Consider a sample $S=(P,N)$ of CGS. Consider some subset $R\subseteq Q^{2}$.
We let $\mathsf{Upd}(R)\subseteq Q^{2}$ be equal to:

$\displaystyle\mathsf{Upd}(R):=\\{$
$\displaystyle(q,q^{\prime}),(q^{\prime},q)\in Q^{2}\mid\exists
A\subseteq\mathsf{RelAg}(q,q^{\prime}),\;\exists\alpha\in\mathsf{Act}_{A}(q),\;$
$\displaystyle\forall\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime}),\exists
t^{\prime}\in\mathsf{Succ}(q^{\prime},\alpha^{\prime}),\forall
t\in\mathsf{Succ}(q,\alpha),\;(t,t^{\prime})\in R\\}$

We can now iteratively compute the set $\mathsf{Distinguish}(S)$ with
approximations until we reach a fixed point. Note that this is similar to what
is done [18, Secion 3] with CTL formulas and Kripke structures, except that we
additionally have to handle the coalitions of agents.

######  Lemma 17.

Consider a sample $S=(P,N)$ of CGS. We let $n:=|Q|^{2}$. We define
$(R_{i})_{0\leq i\leq n^{2}}\subseteq(Q^{2})^{n^{2}+1}$ as follows:

  * •

$R_{0}:=\\{(q,q^{\prime}),(q^{\prime},q)\in
Q^{2}\mid\pi(q)\neq\pi(q^{\prime})\\}$;

  * •

for all $0\leq i\leq n^{2}-1$, $R_{i+1}:=R_{i}\cup\mathsf{Upd}(R_{i})$.

We let $R:=R_{n^{2}}$. Then, we have:

$R=\mathsf{Distinguish}(S)$

###### Proof.

First of all, let us show that $\mathsf{Upd}(R)\subseteq R$. Clearly, for all
$0\leq i\leq n^{2}-1$, we have $R_{i}\subseteq R_{i+1}$. Therefore, since
$|Q^{2}|=n^{2}$, if $R_{n^{2}}\neq Q^{2}$, then there is some $0\leq k\leq
n^{2}-1$ such that $R_{k}=R_{k+1}$ and $\mathsf{Upd}(R_{k})\subseteq R_{k}$.
In such a case, for all $k\leq i\leq n^{2}$, we have $R_{i}=R_{k}$ and
$\mathsf{Upd}(R_{i})\subseteq R_{i}$. Hence, we do have
$\mathsf{Upd}(R)\subseteq R$.

By definition, for all $(q,q^{\prime})\in\mathsf{Distinguish}(S)$, we also
have $(q^{\prime},q)\in\mathsf{Distinguish}(S)$. This is also the case for
$R$. Indeed, for all $(q,q^{\prime})\in R_{0}$, $(q^{\prime},q)\in R_{0}$.
Furthermore, for all subsets $T\subseteq Q^{2}$, we have that for all
$(q,q^{\prime})\in\mathsf{Upd}(T)$, $(q^{\prime},q)\in\mathsf{Upd}(T)$.

For all pairs $(t,t^{\prime})\in\mathsf{Distinguish}(S)$, we let
$\Phi_{(t,t^{\prime})}$ be an ATL-$\operatorname{\mathbf{X}}$ formula such
that $t\models\Phi_{(t,t^{\prime})}$ and
$t^{\prime}\not\models\Phi_{(t,t^{\prime})}$, which exists since we can use
the negation in ATL-$\operatorname{\mathbf{X}}$ formulas.

Now, let us show that $R\subseteq\mathsf{Distinguish}(S)$. We show by
induction on $0\leq i\leq n^{2}$ that $R_{i}\subseteq\mathsf{Distinguish}(S)$.
Consider any $(q,q^{\prime})\in R_{0}$. Consider a proposition
$p\in\mathcal{P}$ such that $p\in\pi(q)$ iff $p\notin\pi(q^{\prime})$, which
exists by definition of $R_{0}$. Then, the ATL-$\operatorname{\mathbf{X}}$
formula $\Phi:=p$ distinguishes the states $q$ and $q^{\prime}$. Hence,
$R_{0}\subseteq\mathsf{Distinguish}(S)$.

Assume now that $R_{i}\subseteq\mathsf{Distinguish}(S)$ for some $0\leq i\leq
n^{2}-1$. Consider some $(q,q^{\prime})\in\mathsf{Upd}(R_{i})$ for which there
is a coalition of agents $A\subseteq\mathsf{RelAg}(q,q^{\prime})$ and a tuple
of actions $\alpha\in\mathsf{Act}_{A}(q)$ such that for all tuples of actions
$\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$, there exists
$t^{\prime}\in\mathsf{Succ}(q^{\prime},\alpha^{\prime})$ such that for all
$t\in\mathsf{Succ}(q,\alpha)$, we have $(t,t^{\prime})\in R_{i}$. For all
tuples of actions $\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$, we let
$t_{\alpha^{\prime}}\in\mathsf{Succ}(q^{\prime},\alpha^{\prime})$ be such that
for all $t\in\mathsf{Succ}(q,\alpha)$, we have $(t,t^{\prime})\in
R_{i}\subseteq\mathsf{Distinguish}(S)$. For all tuples of actions
$\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$, we let:

$\Phi_{\alpha^{\prime}}:=\bigvee_{t\in\mathsf{Succ}(q,\alpha)}\Phi_{(t,t_{\alpha^{\prime}})}$

We also let:

$\Phi_{\alpha}:=\bigwedge_{\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})}\Phi_{\alpha^{\prime}}$

Finally, we let $\Phi:=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi_{\alpha}$. Note that $\Phi$
is an ATL-$\operatorname{\mathbf{X}}$ formula since, for all
$(t,t^{\prime})\in\mathsf{Distinguish}(S)$, $\Phi_{(t,t^{\prime})}$ is an
ATL-$\operatorname{\mathbf{X}}$ formula. We claim that $q\models\Phi$ and
$q^{\prime}\not\models\Phi$. Indeed:

  * •

Let $t\in\mathsf{Succ}(q,\alpha)$. Consider any
$\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$. We have
$t\models\Phi_{(t,t_{\alpha^{\prime}})}$. Hence,
$t\models\Phi_{\alpha^{\prime}}$. Since this holds for all
$\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$, it follows that
$t\models\Phi_{\alpha}$. This holds for all $t\in\mathsf{Succ}(q,\alpha)$.
Thus, $q\models\Phi$.

  * •

Consider any $\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$. For all
$t\in\mathsf{Succ}(q,\alpha)$, we have
$t_{\alpha^{\prime}}\not\models\Phi_{(t,t_{\alpha^{\prime}})}$. Therefore,
$t_{\alpha^{\prime}}\not\models\Phi_{\alpha^{\prime}}$. Thus,
$t_{\alpha^{\prime}}\not\models\Phi_{\alpha}$. That is, for all
$\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$, there is some
$t_{\alpha^{\prime}}\in\mathsf{Succ}(q^{\prime},\alpha^{\prime})$ such that
$t_{\alpha^{\prime}}\not\models\Phi_{\alpha}$. Thus,
$q^{\prime}\not\models\Phi$.

Therefore, $(q,q^{\prime}),(q^{\prime},q)\in\mathsf{Distinguish}(S)$. It
follows that $R_{i+1}\subseteq\mathsf{Distinguish}(S)$. In fact,
$R_{i}\subseteq\mathsf{Distinguish}(S)$ for all $0\leq i\leq n^{2}$. Hence,
$R\subseteq\mathsf{Distinguish}(S)$.

Let us now show that $\mathsf{Distinguish}(S)\subseteq R$. We show by
induction on ATL-$\operatorname{\mathbf{X}}$ formulas $\Phi$ the property
$\mathcal{P}(\Phi)$: for all $(q,q^{\prime})\in Q^{2}$, if $q\models\Phi$ and
$q^{\prime}\not\models\Phi$, then $(q,q^{\prime})\in R$.

Consider an ATL-$\operatorname{\mathbf{X}}$ formula $\Phi=p\in\mathcal{P}$.
Let $(q,q^{\prime})\in Q^{2}$, such that $q\models\Phi$ and
$q^{\prime}\not\models\Phi$. Then, $p\in\pi(q)$ and $p\notin\pi(q^{\prime})$.
Therefore, $\pi(q)\neq\pi(q^{\prime})$. Thus, $(q,q^{\prime})\in
R_{0}\subseteq S$. Hence, $\mathcal{P}(\Phi)$ holds. Then:

  * •

Consider an ATL-$\operatorname{\mathbf{X}}$ formula $\Phi=\neg\Phi^{\prime}$.
Assume that $\mathcal{P}(\Phi^{\prime})$ holds. Consider any
$(q,q^{\prime})\in Q^{2}$, such that $q\models\Phi$ and
$q^{\prime}\not\models\Phi$. Then, $q^{\prime}\models\Phi^{\prime}$ and
$q\not\models\Phi^{\prime}$. By $\mathcal{P}(\Phi^{\prime})$, it follows that
$(q^{\prime},q)\in S$, and therefore we also have $(q,q^{\prime})\in S$.
Hence, $\mathcal{P}(\Phi)$ holds.

  * •

Consider an ATL-$\operatorname{\mathbf{X}}$ formula
$\Phi=\Phi_{1}\wedge\Phi_{2}$. Assume that $\mathcal{P}(\Phi_{1})$ and
$\mathcal{P}(\Phi_{2})$ hold. Consider any $(q,q^{\prime})\in Q^{2}$, such
that $q\models\Phi$ and $q^{\prime}\not\models\Phi$. Then, let
$\Phi^{\prime}\in\\{\Phi_{1},\Phi_{2}\\}$ be such that
$q^{\prime}\not\models\Phi^{\prime}$. We have $q\models\Phi^{\prime}$. Hence,
by $\mathcal{P}(\Phi^{\prime})$, we have $(q,q^{\prime})\in S$. Hence,
$\mathcal{P}(\Phi)$ holds.

  * •

Consider an ATL-$\operatorname{\mathbf{X}}$ formula
$\Phi=\Phi_{1}\lor\Phi_{2}$. Assume that $\mathcal{P}(\Phi_{1})$ and
$\mathcal{P}(\Phi_{2})$ hold. Consider any $(q,q^{\prime})\in Q^{2}$, such
that $q\models\Phi$ and $q^{\prime}\not\models\Phi$. Then, let
$\Phi^{\prime}\in\\{\Phi_{1},\Phi_{2}\\}$ be such that
$q\models\Phi^{\prime}$. We have $q^{\prime}\not\models\Phi^{\prime}$. Hence,
by $\mathcal{P}(\Phi^{\prime})$, we have $(q,q^{\prime})\in S$. Hence,
$\mathcal{P}(\Phi)$ holds.

  * •

Consider an ATL-$\operatorname{\mathbf{X}}$ formula $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi^{\prime}$ for a coalition
of agents $A\subseteq\mathsf{Ag}$. Assume that $\mathcal{P}(\Phi^{\prime})$
holds. Consider any $(q,q^{\prime})\in Q^{2}$, such that $q\models\Phi$ and
$q^{\prime}\not\models\Phi$. Then:

    * –

there is a tuple of actions $\alpha\in\mathsf{Act}_{A}(q)$ such that, for all
$t\in\mathsf{Succ}(q,\alpha)$, we have $t\models\Phi^{\prime}$;

    * –

for all tuples of actions $\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$,
there is some
$t_{\alpha^{\prime}}\in\mathsf{Succ}(q^{\prime},\alpha^{\prime})$, such that
$t_{\alpha^{\prime}}\not\models\Phi^{\prime}$.

We let $\bar{A}:=A\cap(\mathsf{RelAg}(q,q^{\prime}))$ and for all
$u\in\\{q,q^{\prime}\\}$, for all tuples of actions
$\alpha\in\mathsf{Act}_{A}(u)$, we let
$\bar{\alpha}\in\mathsf{Act}_{\bar{A}}(u)$ be such that, for all
$a\in\bar{A}$, we have $\bar{\alpha}_{a}=\alpha_{a}$. Then, by definition of
the set $\mathsf{RelAg}(q,q^{\prime})$, we have
$\mathsf{Succ}(q,\alpha)=\mathsf{Succ}(q,\bar{\alpha})$. Hence, the two above
points are equivalent to:

    * –

there is a tuple of actions $\alpha\in\mathsf{Act}_{\bar{A}}(q)$ such that,
for all $t\in\mathsf{Succ}(q,\alpha)$, we have $t\models\Phi^{\prime}$;

    * –

for all tuples of actions
$\alpha^{\prime}\in\mathsf{Act}_{\bar{A}}(q^{\prime})$, there is some
$t_{\alpha^{\prime}}\in\mathsf{Succ}(q^{\prime},\alpha^{\prime})$, such that
$t_{\alpha^{\prime}}\not\models\Phi^{\prime}$.

Therefore, by $\mathcal{P}(\Phi^{\prime})$, for all
$t\in\mathsf{Succ}(q,\alpha)$ and
$\alpha^{\prime}\in\mathsf{Act}_{A}(q^{\prime})$, we have
$(t,t_{\alpha^{\prime}})\in R$. Overall, we have: for the coalition of agents
$\bar{A}\subseteq\mathsf{RelAg}(q,q^{\prime})$ and for the tuple of actions
$\alpha\in\mathsf{Act}_{\bar{A}}(q)$, for all tuples of actions
$\alpha^{\prime}\in\mathsf{Act}_{\bar{A}}(q^{\prime})$, the state
$t_{\alpha^{\prime}}\in\mathsf{Succ}(q^{\prime},\alpha^{\prime})$ is such
that, for all $t\in\mathsf{Succ}(q,\alpha)$, we have
$(t,t_{\alpha^{\prime}})\in R$. Therefore,
$(q,q^{\prime})\in\mathsf{Upd}(R)\subseteq R$. Hence, $\mathcal{P}(\Phi)$
holds.

Overall, $\mathcal{P}(\Phi)$ holds for ATL-$\operatorname{\mathbf{X}}$
formulas $\Phi$. Therefore, $\mathsf{Distinguish}(S)\subseteq R$. ∎

There now only remains to note that, given a set $R$, we can compute in
polynomial time the set $\mathsf{Dist}_{\operatorname{\mathbf{X}}}(R)$. It
then follows, from Lemma 17 that we can compute in polynomial time the set
$\mathsf{Distinguish}(\mathcal{S})$. We provide explicit algorithms in
Appendix C.2, with explicit bounds. This allows to establish Lemma 9, from
which directly follows Theorem 7.

####  3.2.2 Separability for any fragment of ATL

Let us now consider the case of an arbitrary fragment of ATL. Now, the above-
described algorithm a priori does not work. Among other things, one of the
issues is that, possibly, we may not be able to use the operator
$\operatorname{\mathbf{X}}$. Therefore, given a sample $\mathcal{S}$, instead
of iteratively constructing a subset of
$\mathsf{Distinguish}(\mathcal{S})\subseteq Q^{2}$ of distinguishable pairs of
states, we iteratively compute a subset $\mathsf{Acc}(\mathcal{S})\subseteq
2^{Q}$ of sets of states that can be accepted with a formula in the fragment
considered, while the complement set is rejected. We can then prove a
definition and lemma similar to Definition 16 and Lemma 17 except that we
additionally have to be able to handle the operators
$\operatorname{\mathbf{G}}$ and $\operatorname{\mathbf{U}}$, which is done by
using Algorithms 1, 2.

The goal of subsection is to show the theorem below.

######  Theorem 18.

Consider a sample $\mathcal{S}$ and a fragment ATL’ of ATL. We can decide in
time exponential in $|\mathcal{S}|$ if the sample $\mathcal{S}$ is separable
with ATL’ formulas. If it is, then there exists an ATL’ formula consistent
with $\mathcal{S}$ of size at most $2^{|Q|}$.

To establish this theorem, we are actually to prove the lemma below.

######  Lemma 19.

Consider any subset of operators $\mathsf{O}\subseteq\mathsf{OP}$. and a
sample $S=(P,N)$ of CGS. We can decide in time $O(2^{k+2n}\cdot n^{2}\cdot
M\cdot r)$ if there is an $\mathbf{ATL}(\mathsf{O})$-formula consistent with
$S$. Furthermore, if it is the case, then there is an
$\mathbf{ATL}(\mathsf{O})$-formula of size at most $2^{n}$ that is consistent
with $S$.

The complexity result extends [35, Theorem 3] to the case of ATL formulas and
CGS. For the bound on the size of the formulas, this extends [44, Corollary 1]
to any fragment of ATL, although it is not clear whether our bound and the one
from [44, Corollary 1] are comparable or not.

First of all, for any subset of operators $\mathsf{O}\subseteq\mathsf{OP}$,
let us define formally the set $\mathsf{Acc}(S,\mathsf{O})\subseteq 2^{Q}$ of
accepted sets of states by $\mathbf{ATL}(\mathsf{O})$-formulas.

######  Definition 20.

Given any sample $S=(P,N)$ of CGS and ATL formula $\Phi$, we let
$\mathsf{SAT}(\Phi)\subseteq Q$ denote the set of states that satisfy the
formula $\Phi$: $\mathsf{SAT}(\Phi):=\\{q\in Q\mid q\models\Phi\\}$. Then, for
any subset of operators $\mathsf{O}\subseteq\mathsf{OP}$, we define the set
$\mathsf{Acc}(S,\mathsf{O})\subseteq 2^{Q}$ as follows:

$\mathsf{Acc}(S,\mathsf{O}):=\\{\mathsf{SAT}(\Phi)\mid\Phi\in\mathbf{ATL}(\mathsf{O})\\}\subseteq
2^{Q}$

Our goal is to able to compute the set $\mathsf{Acc}(S,\mathsf{O})$, To do so,
as in the previous subsection, we are going to iteratively compute an
approximation of that set until we reach a fixed point. We define below the
update function that we will consider.

######  Definition 21.

Consider a sample $S=(P,N)$ of CGS and a coalition of agents
$A\subseteq\mathsf{Ag}$. For all subsets $T\subseteq Q$, we let:

  * •

$\mathsf{Upd}_{\neg}(S,T):=Q\setminus T$;

  * •

$\mathsf{Upd}_{\operatorname{\mathbf{X}}}(S,A,T):=\mathsf{Pre}_{A}(T)$;

  * •

$\mathsf{Upd}_{\operatorname{\mathbf{G}}}(S,A,T):=\mathsf{ComputeSAT}_{\operatorname{\mathbf{G}}}(S,A,T)$
which refers to the output of Algorithm 2 on $(S,A,T)$;

For all pairs of subsets $T,T^{\prime}\subseteq Q$, we let:

  * •

$\mathsf{Upd}_{\wedge}(S,T,T^{\prime}):=T\cap T^{\prime}$;

  * •

$\mathsf{Upd}_{\operatorname{\mathbf{U}}}(S,A,T,T^{\prime}):=\mathsf{ComputeSAT}_{\operatorname{\mathbf{U}}}(S,A,T,T^{\prime})$,
which refers to the output of Algorithm 1 on $(S,A,T,T^{\prime})$;

Then, for any subset of operators $\mathsf{O}\subseteq\mathsf{OP}$ and for all
$R\subseteq 2^{Q}$, we let $\mathsf{Upd}_{\mathsf{O}}(R)\subseteq 2^{Q}$ be
equal to:

$\mathsf{Upd}_{\mathsf{O}}(R):=\bigcup_{A\subseteq\mathsf{Ag}}\left(\bigcup_{T\in
R}\bigcup_{o\in\mathsf{O}\cap\\{\neg,\operatorname{\mathbf{X}},\operatorname{\mathbf{G}}\\}}\mathsf{Upd}_{o}(S,A,T)\cup\bigcup_{T,T^{\prime}\in
R}\bigcup_{o\in\mathsf{O}\cap\\{\wedge,\operatorname{\mathbf{U}}\\}}\mathsf{Upd}_{o}(S,A,T,T^{\prime})\right)$

As intended, this definition matches the semantics of the operators
$\neg,\wedge,\operatorname{\mathbf{X}},\operatorname{\mathbf{G}},\operatorname{\mathbf{U}}$.

######  Lemma 22.

Consider a sample $S=(P,N)$ of CGS and any ATL formula $\Phi$.

  * •

If $\Phi=\neg\Phi^{\prime}$, then
$\mathsf{SAT}(\Phi)=\mathsf{Upd}_{\neg}(S,\mathsf{SAT}(\Phi^{\prime}))$.

  * •

If $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi^{\prime}$, then
$\mathsf{SAT}(\Phi)=\mathsf{Upd}_{\operatorname{\mathbf{X}}}(S,A,\mathsf{SAT}(\Phi^{\prime}))$.

  * •

If $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{G}}\Phi^{\prime}$, then
$\mathsf{SAT}(\Phi)=\mathsf{Upd}_{\operatorname{\mathbf{G}}}(S,A,\mathsf{SAT}(\Phi^{\prime}))$.

  * •

If $\Phi=\Phi_{1}\wedge\Phi_{2}$, then
$\mathsf{SAT}(\Phi)=\mathsf{Upd}_{\wedge}(S,\mathsf{SAT}(\Phi_{1}),\mathsf{SAT}(\Phi_{2}))$.

  * •

If $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2}$, then
$\mathsf{SAT}(\Phi)=\mathsf{Upd}_{\operatorname{\mathbf{U}}}(S,A,\mathsf{SAT}(\Phi_{1},\mathsf{SAT}(\Phi_{2}))$.

###### Proof.

The case of the operators $\neg,\wedge$ and $\operatorname{\mathbf{X}}$ comes
directly from the definition of the semantics of these operators. The case of
the operators $\operatorname{\mathbf{G}}$ and $\operatorname{\mathbf{U}}$
comes from the fixed point computation algorithm [2, Fig. 3] (as mentioned in
the main part of the paper). ∎

We can now define the iterative approximations of the set
$\mathsf{Acc}(S,\mathsf{O})$.

######  Definition 23.

Consider a sample $S=(P,N)$ of CGS. We let $n:=|Q|$. For any subset of
operators $\mathsf{O}\subseteq\mathsf{OP}$, we define
$(\mathsf{Apr}_{i}(S,\mathsf{O}))_{1\leq i\leq 2^{n}}\subseteq(2^{Q})^{2^{n}}$
as follows:

  * •

$\mathsf{Apr}_{1}(S,\mathsf{O}):=\cup_{b\in\mathcal{P}}\\{q\in Q\mid
b\in\pi(q)\\}=\cup_{b\in\mathcal{P}}\mathsf{SAT}(b)$;

  * •

for all $1\leq i\leq 2^{n}-1$,
$\mathsf{Apr}_{i+1}(S,\mathsf{O}):=\mathsf{Apr}_{i}(S,\mathsf{O})\cup\mathsf{Upd}_{\mathsf{O}}(\mathsf{Apr}_{i}(S,\mathsf{O}))$.

We let $\mathsf{Apr}(S,\mathsf{O}):=\mathsf{Apr}_{2^{n}}(S,\mathsf{O})$.

Our goal is now to show that
$\mathsf{Apr}(S,\mathsf{O})=\mathsf{Acc}(S,\mathsf{O})$. This will be done in
two different lemmas. We start with the easy inclusion.

######  Lemma 24.

Given any sample $S=(P,N)$ of CGS and any subset of operators
$\mathsf{O}\subseteq\mathsf{OP}$, we have:

$\mathsf{Acc}(S,\mathsf{O})\subseteq\mathsf{Apr}(S,\mathsf{O})$

We proceed similarly than for the proof of Lemma 17.

###### Proof.

Let us first show that
$\mathsf{Upd}_{\mathsf{O}}(\mathsf{Apr}(S,\mathsf{O}))\subseteq\mathsf{Apr}(S,\mathsf{O})$.
Clearly, for all $1\leq i\leq 2^{n}-1$, we have
$\mathsf{Apr}_{i}(S,\mathsf{O})\subseteq\mathsf{Apr}_{i+1}(S,\mathsf{O})$.
Therefore, since $|2^{Q}|=2^{n}$, if $\mathsf{Apr}_{2^{n}}(S,\mathsf{O})\neq
2^{Q}$, then there is some $1\leq k\leq 2^{n}-1$ such that
$\mathsf{Apr}_{k}(S,\mathsf{O})=\mathsf{Apr}_{k+1}(S,\mathsf{O})$ and
$\mathsf{Upd}_{\mathsf{O}}(\mathsf{Apr}_{k}(S,\mathsf{O}))\subseteq\mathsf{Apr}_{k}(S,\mathsf{O})$.
In such a case, for all $k\leq i\leq 2^{n}$, we have
$\mathsf{Apr}_{i}(S,\mathsf{O})=\mathsf{Apr}_{k}(S,\mathsf{O})$ and
$\mathsf{Upd}_{\mathsf{O}}(\mathsf{Apr}_{i}(S,\mathsf{O}))\subseteq\mathsf{Apr}_{i}(S,\mathsf{O})$.
Hence, we do have
$\mathsf{Upd}_{\mathsf{O}}(\mathsf{Apr}(S,\mathsf{O}))\subseteq\mathsf{Apr}(S,\mathsf{O})$.

We now show by induction on $\mathbf{ATL}(\mathsf{O})$-formulas $\Phi$ the
property $\mathcal{P}(\Phi)$:
$\mathsf{SAT}(\Phi)\in\mathsf{Apr}(S,\mathsf{O})$.

Consider an $\mathbf{ATL}(\mathsf{O})$-formula $\Phi\in\mathcal{P}$. By
definition, we have
$\mathsf{SAT}(\Phi)\in\mathsf{Apr}_{1}(S,\mathsf{O})\subseteq\mathsf{Apr}(S,\mathsf{O})$.
Hence, $\mathcal{P}(\Phi)$ holds.

Consider any unary operator
$u\in\\{\neg,\operatorname{\mathbf{X}},\operatorname{\mathbf{G}}\\}$. If
$u\in\mathsf{O}$, then for any $\mathbf{ATL}(\mathsf{O})$-formula
$\Phi=(\langle\\!\langle A\rangle\\!\rangle\\!)\;u\;\Phi^{\prime}$ (where
$\langle\\!\langle A\rangle\\!\rangle\\!$ appears, for some coalition of
agents $A\subseteq\mathsf{Ag}$, iff $u\neq\neg$), if
$\mathsf{SAT}(\Phi^{\prime})\in\mathsf{Apr}(S,\mathsf{O})$, then by Lemma 22,
we have
$\mathsf{SAT}(\Phi)\in\mathsf{Upd}_{\mathsf{O}}(\mathsf{Apr}(S,\mathsf{O}))\subseteq\mathsf{Apr}(S,\mathsf{O})$.
That is, $\mathcal{P}(\Phi^{\prime})$ implies $\mathcal{P}(\Phi)$.

Similarly, consider any binary operator
$b\in\\{\wedge,\operatorname{\mathbf{U}}\\}$. If $b\in\mathsf{O}$, then for
any $\mathbf{ATL}(\mathsf{O})$-formula $\Phi=(\langle\\!\langle
A\rangle\\!\rangle\\!)\Phi_{1}\;b\;\Phi_{2}$ (where $\langle\\!\langle
A\rangle\\!\rangle\\!$ appears, for some coalition of agents
$A\subseteq\mathsf{Ag}$, iff $b\neq\wedge$), if
$\mathsf{SAT}(\Phi_{1}),\mathsf{SAT}(\Phi_{2})\in\mathsf{Apr}(S,\mathsf{O})$,
then by Lemma 22, we have
$\mathsf{SAT}(\Phi)\in\mathsf{Upd}_{\mathsf{O}}(\mathsf{Apr}(S,\mathsf{O}))\subseteq\mathsf{Apr}(S,\mathsf{O})$.
That is, $\mathcal{P}(\Phi_{1})$ and $\mathcal{P}(\Phi_{2})$ imply
$\mathcal{P}(\Phi)$.

Therefore, $\mathcal{P}(\Phi)$ holds for all
$\mathbf{ATL}(\mathsf{O})$-formulas $\Phi$. Therefore,
$\mathsf{Acc}(S,\mathsf{O})\subseteq\mathsf{Apr}(S,\mathsf{O})$. ∎

We now state and prove a lemma establishing the reverse inclusion. We
additionally establish in this lemma a bound on the size of the
$\mathbf{ATL}(\mathsf{O})$-formulas that are sufficient to consider.

######  Lemma 25.

Consider a sample $S=(P,N)$ of CGS and a subset of operators
$\mathsf{O}\subseteq\mathsf{OP}$. For all $T\in\mathsf{Apr}(S,\mathsf{O})$,
there is an $\mathbf{ATL}(\mathsf{O})$-formula $\Phi$ of size at most $2^{n}$
such that $\mathsf{SAT}(\Phi)=T$.

In particular, this implies
$\mathsf{Apr}(S,\mathsf{O})\subseteq\mathsf{Acc}(S,\mathsf{O})$.

###### Proof.

We define a function
$f:\mathsf{Apr}(S,\mathsf{O})\rightarrow\mathbf{ATL}(\mathsf{O})$ such that,
for all $T\in\mathsf{Apr}(S,\mathsf{O})$, we have $\mathsf{SAT}(f(T))=T$. We
define this function inductively on $1\leq i\leq 2^{n}$ such that it satisfies
the property $\mathcal{P}(i)$: for all $T\in\mathsf{Apr}_{i}(S,\mathsf{O})$,
$\mathsf{SubF}(f(T))\subseteq f(\mathsf{Apr}_{i}(S,\mathsf{O}))$.

Consider any set $T\in\mathsf{Apr}_{1}(S,\mathsf{O})$. By definition, there is
some proposition $p\in\mathcal{P}$ such that $T=\mathsf{SAT}(p)$. We let
$f(T):=p$, which ensures that the property $\mathcal{P}(1)$ holds.

Assume now that the function $f$ is defined on
$\mathsf{Apr}_{i}(S,\mathsf{O})$ for some $1\leq i\leq 2^{n}-1$ and that
$\mathcal{P}(i)$ holds. Let us define $f$ on
$\mathsf{Apr}_{i+1}(S,\mathsf{O})$. Let
$T\in\mathsf{Apr}_{i+1}(S,\mathsf{O})\setminus\mathsf{Apr}_{i}(S,\mathsf{O})$.
There are several (quite similar) cases:

  * •

Assume that $\neg\in\mathsf{O}$ and that $T=\mathsf{Upd}_{\neg}(S,T^{\prime})$
for some $T^{\prime}\in\mathsf{Apr}_{i}(S,\mathsf{O})$. Then, we let
$f(T):=\neg f(T^{\prime})\in\mathbf{ATL}(\mathsf{O})$. By Lemma 22 and
$\mathcal{P}(i)$, we have
$\mathsf{SAT}(f(T))=\mathsf{Upd}_{\neg}(S,\mathsf{SAT}(f(T^{\prime})))=\mathsf{Upd}_{\neg}(S,T^{\prime})=T$.
Furthermore,
$\mathsf{SubF}(f(T))=\\{f(T)\\}\cup\mathsf{SubF}(f(T^{\prime}))\subseteq
f(\mathsf{Apr}_{i+1}(S,\mathsf{O}))$.

  * •

Let $\bullet\in\\{\operatorname{\mathbf{X}},\operatorname{\mathbf{G}}\\}$.
Assume that $\bullet\in\mathsf{O}$ and that
$T=\mathsf{Upd}_{\bullet}(S,A,T^{\prime})$ for some
$T^{\prime}\in\mathsf{Apr}_{i}(S,\mathsf{O})$ and $A\subseteq\mathsf{Ag}$.
Then, we let $f(T):=\langle\\!\langle A\rangle\\!\rangle\\!\bullet
f(T^{\prime})\in\mathbf{ATL}(\mathsf{O})$. By Lemma 22 and $\mathcal{P}(i)$,
we have
$\mathsf{SAT}(f(T))=\mathsf{Upd}_{\bullet}(S,A,\mathsf{SAT}(f(T^{\prime})))=\mathsf{Upd}_{\bullet}(S,A,T^{\prime})=T$.
Furthermore,
$\mathsf{SubF}(f(T))=\\{f(T)\\}\cup\mathsf{SubF}(f(T^{\prime}))\subseteq
f(\mathsf{Apr}_{i+1}(S,\mathsf{O}))$.

  * •

Assume that $\wedge\in\mathsf{O}$ and that
$T=\mathsf{Upd}_{\wedge}(S,T_{1},T_{2})$ for some
$T_{1},T_{2}\in\mathsf{Apr}_{i}(S,\mathsf{O})$. Then, we let
$f(T):=f(T_{1})\wedge f(T_{2})\in\mathbf{ATL}(\mathsf{O})$. By Lemma 22 and
$\mathcal{P}(i)$, we have
$\mathsf{SAT}(f(T))=\mathsf{Upd}_{\wedge}(S,\mathsf{SAT}(f(T_{1})),\mathsf{SAT}(f(T_{2})))=\mathsf{Upd}_{\wedge}(S,T_{1},T_{2})=T$.
Furthermore,
$\mathsf{SubF}(f(T))=\\{f(T)\\}\cup\mathsf{SubF}(f(T_{1}))\cup\mathsf{SubF}(f(T_{2}))\subseteq
f(\mathsf{Apr}_{i+1}(S,\mathsf{O}))$.

  * •

Assume that $\operatorname{\mathbf{U}}\in\mathsf{O}$ and that
$T=\mathsf{Upd}_{\operatorname{\mathbf{U}}}(S,A,T_{1},T_{2})$ for some
$T_{1},T_{2}\in\mathsf{Apr}_{i}(S,\mathsf{O})$ and $A\subseteq\mathsf{Ag}$.
Then, we let $f(T):=\langle\\!\langle
A\rangle\\!\rangle\\!f(T_{1})\operatorname{\mathbf{U}}f(T_{2})\in\mathbf{ATL}(\mathsf{O})$.
By Lemma 22 and $\mathcal{P}(i)$, we have
$\mathsf{SAT}(f(T))=\mathsf{Upd}_{\operatorname{\mathbf{U}}}(S,A,\mathsf{SAT}(f(T_{1})),\mathsf{SAT}(f(T_{2})))=\mathsf{Upd}_{\operatorname{\mathbf{U}}}(S,A,T_{1},T_{2})=T$.
Furthermore,
$\mathsf{SubF}(f(T))=\\{f(T)\\}\cup\mathsf{SubF}(f(T_{1}))\cup\mathsf{SubF}(f(T_{2}))\subseteq
f(\mathsf{Apr}_{i+1}(S,\mathsf{O}))$.

Therefore, $\mathcal{P}(i+1)$ holds. In fact, $\mathcal{P}(i)$ holds for all
$1\leq i\leq 2^{n}$.

Hence, for all
$T\in\mathsf{Apr}(S,\mathsf{O})=\mathsf{Apr}_{2^{n}}(S,\mathsf{O})$, there is
an $\mathbf{ATL}(\mathsf{O})$-formula $\Phi$ such that $\mathsf{SAT}(\Phi)=T$
and $\mathsf{SubF}(\Phi)\subseteq f(\mathsf{Apr}_{2^{n}}(S,\mathsf{O}))$.
Therefore,
$|\Phi|=|\mathsf{SubF}(\Phi)|\leq|\mathsf{Apr}_{2^{n}}(S,\mathsf{O})|\leq|2^{Q}|=2^{n}$.
∎

The exponential bound on the size of formulas is established in Lemma 25. We
can then deduce Lemma 19 by carefully looking at the complexity of computing
the set $\mathsf{Apr}_{i}(S,\mathsf{O})$. This is done in Appendix C.3. Then,
Theorem 18 follows directly from Lemma 19.

##  4 Experimental Evaluation

$20$$40$$60$$80$$100$$120$01K2KNumber of examplesRuntime (in secs)CTL
learningCTL
formulas$\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{G}}(\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{F}}(p))$$\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{G}}(\neg
p\\!\lor\\!\neg
q)$$\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{G}}(p\\!\rightarrow\\!\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{F}}(q))$$\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{G}}(\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{F}}(p)\\!\land\\!\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{F}}(q))$$10$$20$$30$$40$$50$$60$Number
of examplesATL learningATL formulas$\langle\\!\langle
0\rangle\\!\rangle\\!\operatorname{\mathbf{F}}(q)$$\langle\\!\langle\rangle\\!\rangle\\!\operatorname{\mathbf{G}}(p\\!\rightarrow\\!\langle\\!\langle
1\rangle\\!\rangle\\!\operatorname{\mathbf{G}}(p))$$\langle\\!\langle\rangle\\!\rangle\\!\operatorname{\mathbf{G}}(p\rightarrow\langle\\!\langle
0,\\!1\rangle\\!\rangle\\!\operatorname{\mathbf{F}}(q))$$\langle\\!\langle\rangle\\!\rangle\\!\operatorname{\mathbf{G}}((p\\!\wedge\\!\neg
q)\\!\rightarrow\\!\langle\\!\langle
1\rangle\\!\rangle\\!\operatorname{\mathbf{G}}(p))$ Figure 2: Runtime of CTL
and ATL learning algorithms on samples with varying number of examples
(considering structures of size $\leq 20$).

To test the ability of our learning algorithms (from Section 3.1), we
implement them in an open-source
prototype111https://github.com/rajarshi008/learning-branching-time. The
prototype is developed in Python3 and utilizes the PySMT library [27],
providing us access to an array of SAT solvers. Moreover, it offers
configurable parameters for learning, including options to specify the model
type (KS or CGS) and the formula type (CTL or ATL).

To test various aspects of our algorithms, we rely on synthetic benchmarks
generated from a set of chosen formulas as is common in the literature [42,
20]. We first identified some common CTL and ATL formulas from standard
sources: the book on model-checking by Baier and Katoen [10, Example 6.3] for
CTL and the seminal work by Alur et al. [1, Examples 3.1,3.2] for ATL. Fig.
(2) displays a selection of formulas (see Appendix D.1 for the full list); we
used abstract propositions and players in the formulas to maintain uniformity.
The CTL formulas reflect properties occurring in distributed systems, such as
mutual exclusion, request-response progress, etc. The ATL formulas describe
various properties of a train-controller (multi-agent) system.

We generated samples following a random generation technique. To construct a
structure $C$ for a sample, we iteratively added states to $C$ ensuring its
connectedness; assigned random propositions to each state of $C$; and added
random edges, labeled with action tuples if generating a CGS. For CGSs, we
focussed on generating turn-based games, i.e., games where only one player has
actions in each state, due to their prevalence in verification and synthesis.
We split the randomly generated structures into $P$ and $N$ based on the
selected formula.

Overall, from six CTL formulas and six ATL formulas, we generated two
benchmark suites, the first one consisting of 144 samples of KSs and the
second one consisting of 144 samples of CGSs, respectively. The number of
examples in the suites ranges from 20 to 120 and 10 to 60, respectively.
Moreover, the sizes of the KSs range from 1 to 40, while the size of the CGSs
range from 1 to 20.

All tests were run on Intel Xeon Gold 6142 CPU (at 2.6 GHz) using up to 10 GB
of RAM using MathSAT solver [24]222MathSAT [24] performed better than Z3 [41]
and Boolector [19] in our experiments., with a timeout of 2400 seconds.

How effective are the algorithms in learning CTL/ATL formulas? To answer this,
we ran the CTL and ATL learning algorithms on the first and second benchmark
suites, respectively. Fig. 2 depicts runtimes of both algorithms for samples
generated from a selection of formulas (full results are available in Appendix
D.2). Both algorithms exhibit reasonable runtime performance for small
samples. As the samples size increases, the runtime also increases, more
prominently for the larger formulas in our selection. For the smaller
formulas, however, the runtime of the algorithms remains reasonable even when
the samples size increases.

$10^{-1}$$10^{0}$$10^{1}$$10^{2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$TOTORuntime
with $\operatorname{\mathbf{U}}$Runtime without $\operatorname{\mathbf{U}}$CTL
learning (a) Improvement by dropping $\operatorname{\mathbf{U}}$

$10^{-1}$$10^{0}$$10^{1}$$10^{2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$TOTORuntime
with $\Omega_{q,i}^{\mathsf{Pre}}$Runtime with
$\bar{\Omega}_{q,i}^{\mathsf{Pre}}$ATL learning (b) Turn-based games
improvement

Figure 3: Runtime improvement with optimized encodings for CTL and ATL
learning on first and second benchmark suites, respectively. The runtimes are
in seconds and “TO” represents timeout.

Which parts of the SAT encoding contribute significantly towards the runtime?
To understand this, we profiled both algorithms to identify the constraints
responsible for significant runtime increases. Notably, generating constraints
for the $\operatorname{\mathbf{U}}$ operators (i.e.,
$\operatorname{\mathbf{E}\\!}\operatorname{\mathbf{U}}$,
$\operatorname{\mathbf{A}\\!}\operatorname{\mathbf{U}}$ for CTL and
$\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{U}}$ for ATL)
turned out to be the most time-consuming among all operators. Consequently, we
compared runtime performance with and without these operators. (Note that we
included $\operatorname{\mathbf{F}}$ and $\operatorname{\mathbf{G}}$ operators
in both cases.) Learning without the $\operatorname{\mathbf{U}}$ operator is
often justified, since several properties do not require the
$\operatorname{\mathbf{U}}$ operator [45]. Fig. 3(a) depicts this comparison
for CTL learning; the average runtime improvement is 46%.

Moreover, computing the constraints for $\Omega_{q,i}^{\mathsf{Pre}}(y)$
happens to be expensive due to the nesting of conjunction and disjunction of
propositional formulas. As a result, we noticed an improvement when we used
the following optimized encoding designed specifically for turn-based games:

$\bar{\Omega}_{q,i}^{\mathsf{Pre}}(y_{S})\coloneqq[A_{i,\sigma(q)}\Rightarrow\bigvee_{\alpha\in\mathsf{Act}_{\mathsf{Ag}}(q)}y_{S}(\delta(q,\alpha)]\wedge[\neg
A_{i,\sigma(q)}\Rightarrow\bigwedge_{\alpha\in\mathsf{Act}_{\mathsf{Ag}}(q)}y_{S}(\delta(q,\alpha)],$

where $\sigma(q)$ denotes the Agent owning the state $q$. Fig. 3(b)
illustrates this improvement; the average runtime improvement is 52%.

Overall, we demonstrated that our learning algorithms can successfully infer
several CTL and ATL formulas from samples of varying sizes.

##  5 Conclusion

In this work, we address the passive learning problem for CTL and ATL,
proposing a constraint-solving technique that encodes search and model-
checking of formulas in propositional logic. We additionally investigate the
separability of ATL formulas and develop decision procedures for it. Our
experimental evaluations validate the efficacy of our algorithms in inferring
useful CTL/ATL formulas.

As future work, we like to explore the computational hardness of the passive
learning problems for CTL/ATL, similar to [26]. We also plan to improve our
prototype by adding heuristics, such as the ones discussed in [44]. Finally,
we like to lift our techniques to probabilistic logics such as PCTL [29] and
PATL [22].

## References

  * [1] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (sep 2002). https://doi.org/10.1145/585265.585270, https://doi.org/10.1145/585265.585270
  * [2] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002). https://doi.org/10.1145/585265.585270, https://doi.org/10.1145/585265.585270
  * [3] Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: CAV. Lecture Notes in Computer Science, vol. 1427, pp. 521–525. Springer (1998)
  * [4] Ammons, G., Bodík, R., Larus, J.R.: Mining specifications. In: Launchbury, J., Mitchell, J.C. (eds.) Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002. pp. 4–16. ACM (2002). https://doi.org/10.1145/503272.503275, https://doi.org/10.1145/503272.503275
  * [5] Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
  * [6] Arif, M.F., Larraz, D., Echeverria, M., Reynolds, A., Chowdhury, O., Tinelli, C.: SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In: FMCAD. pp. 93–103. IEEE (2020)
  * [7] Asarin, E., Donzé, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Proceedings of the Second International Conference on Runtime Verification. p. 147–160. RV’11, Springer-Verlag, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-29860-8_12, https://doi.org/10.1007/978-3-642-29860-8_12
  * [8] Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(1), 1840001:1–1840001:25 (2018)
  * [9] Avellaneda, F., Petrenko, A.: Inferring DFA without negative examples. In: Unold, O., Dyrka, W., Wieczorek, W. (eds.) Proceedings of the 14th International Conference on Grammatical Inference, ICGI 2018, Wrocław, Poland, September 5-7, 2018. Proceedings of Machine Learning Research, vol. 93, pp. 17–29. PMLR (2018), http://proceedings.mlr.press/v93/avellaneda19a.html
  * [10] Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)
  * [11] Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: TACAS (1). Lecture Notes in Computer Science, vol. 13243, pp. 415–442. Springer (2022)
  * [12] Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Hybrid Systems. Lecture Notes in Computer Science, vol. 1066, pp. 232–243. Springer (1995)
  * [13] Bertrand, N., Fearnley, J., Schewe, S.: Bounded satisfiability for PCTL. In: Cégielski, P., Durand, A. (eds.) Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France. LIPIcs, vol. 16, pp. 92–106. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012). https://doi.org/10.4230/LIPIcs.CSL.2012.92, https://doi.org/10.4230/LIPIcs.CSL.2012.92
  * [14] Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behavior. IEEE Trans. Computers 21(6), 592–597 (1972)
  * [15] Bjørner, D., Havelund, K.: 40 years of formal methods - some obstacles and some possibilities? In: FM. Lecture Notes in Computer Science, vol. 8442, pp. 42–61. Springer (2014)
  * [16] Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. p. 1–10. HSCC ’16, Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/2883817.2883843, https://doi.org/10.1145/2883817.2883843
  * [17] Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. p. 1–10. HSCC ’16, Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/2883817.2883843, https://doi.org/10.1145/2883817.2883843
  * [18] Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115–131 (1988). https://doi.org/10.1016/0304-3975(88)90098-9, https://doi.org/10.1016/0304-3975(88)90098-9
  * [19] Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: TACAS. Lecture Notes in Computer Science, vol. 5505, pp. 174–177. Springer (2009)
  * [20] Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: ICAPS. pp. 621–630. AAAI Press (2019)
  * [21] Chan, W.: Temporal-logic queries. In: CAV. Lecture Notes in Computer Science, vol. 1855, pp. 450–463. Springer (2000)
  * [22] Chen, T., Lu, J.: Probabilistic alternating-time temporal logic and model checking algorithm. In: FSKD (2). pp. 35–39. IEEE Computer Society (2007)
  * [23] Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) Computer Aided Verification, 11th International Conference, CAV ’99, Trento, Italy, July 6-10, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1633, pp. 495–499. Springer (1999). https://doi.org/10.1007/3-540-48683-6_44, https://doi.org/10.1007/3-540-48683-6_44
  * [24] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: TACAS. Lecture Notes in Computer Science, vol. 7795, pp. 93–107. Springer (2013)
  * [25] Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs. Lecture Notes in Computer Science, vol. 131, pp. 52–71. Springer (1981)
  * [26] Fijalkow, N., Lagarde, G.: The complexity of learning linear temporal formulas from examples. In: ICGI. Proceedings of Machine Learning Research, vol. 153, pp. 237–250. PMLR (2021)
  * [27] Gario, M., Micheli, A.: Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In: SMT Workshop 2015 (2015)
  * [28] Gold, E.M.: Complexity of automaton identification from given data. Inf. Control. 37(3), 302–320 (1978)
  * [29] Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)
  * [30] van der Hoek, W., Wooldridge, M.J.: Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Stud Logica 75(1), 125–157 (2003)
  * [31] Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)
  * [32] Kim, J., Muise, C., Shah, A., Agarwal, S., Shah, J.: Bayesian inference of linear temporal logic specifications for contrastive explanations. In: IJCAI. pp. 5591–5598. ijcai.org (2019)
  * [33] Kong, Z., Jones, A., Belta, C.: Temporal logics for learning and detection of anomalous behavior. IEEE Transactions on Automatic Control 62(3), 1210–1222 (2017). https://doi.org/10.1109/TAC.2016.2585083
  * [34] Kong, Z., Jones, A., Medina Ayala, A., Aydin Gol, E., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control. p. 273–282. HSCC ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2562059.2562146, https://doi.org/10.1145/2562059.2562146
  * [35] Krogmeier, P., Madhusudan, P.: Languages with decidable learning: A meta-theorem. Proc. ACM Program. Lang. 7(OOPSLA1), 143–171 (2023). https://doi.org/10.1145/3586032, https://doi.org/10.1145/3586032
  * [36] Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: MEMOCODE. pp. 43–50. IEEE (2011)
  * [37] Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings. Lecture Notes in Computer Science, vol. 3920, pp. 450–454. Springer (2006). https://doi.org/10.1007/11691372_31, https://doi.org/10.1007/11691372_31
  * [38] Luo, W., Liang, P., Du, J., Wan, H., Peng, B., Zhang, D.: Bridging ltlf inference to GNN inference for learning ltlf formulae. In: AAAI. pp. 9849–9857. AAAI Press (2022)
  * [39] Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15(4), 34:1–34:47 (2014). https://doi.org/10.1145/2631917, https://doi.org/10.1145/2631917
  * [40] Mohammadinejad, S., Deshmukh, J.V., Puranic, A.G., Vazquez-Chanlatte, M., Donzé, A.: Interpretable classification of time-series data using efficient enumerative techniques. In: HSCC ’20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020. pp. 9:1–9:10. ACM (2020). https://doi.org/10.1145/3365365.3382218
  * [41] de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)
  * [42] Neider, D., Gavran, I.: Learning linear temporal properties. In: Bjørner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp. 1–10. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8603016, https://doi.org/10.23919/FMCAD.2018.8603016
  * [43] Nenzi, L., Silvetti, S., Bartocci, E., Bortolussi, L.: A robust genetic algorithm for learning temporal specifications from data. In: McIver, A., Horvath, A. (eds.) Quantitative Evaluation of Systems. pp. 323–338. Springer International Publishing, Cham (2018)
  * [44] Pommellet, A., Stan, D., Scatton, S.: Sat-based learning of computation tree logic. CoRR abs/2402.06366 (2024). https://doi.org/10.48550/ARXIV.2402.06366, https://doi.org/10.48550/arXiv.2402.06366
  * [45] Raha, R., Roy, R., Fijalkow, N., Neider, D.: Scalable anytime algorithms for learning fragments of linear temporal logic. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 263–280. Springer International Publishing, Cham (2022)
  * [46] Raha, R., Roy, R., Fijalkow, N., Neider, D., Pérez, G.A.: Synthesizing efficiently monitorable formulas in metric temporal logic. In: VMCAI (2). Lecture Notes in Computer Science, vol. 14500, pp. 264–288. Springer (2024)
  * [47] Riener, H.: Exact synthesis of LTL properties from traces. In: FDL. pp. 1–6. IEEE (2019)
  * [48] Roy, R., Fisman, D., Neider, D.: Learning interpretable models in the property specification language. In: IJCAI. pp. 2213–2219. ijcai.org (2020)
  * [49] Roy, R., Gaglione, J., Baharisangari, N., Neider, D., Xu, Z., Topcu, U.: Learning interpretable temporal properties from positive examples only. CoRR abs/2209.02650 (2022)
  * [50] Roy, R., Neider, D.: Inferring properties in computation tree logic. CoRR abs/2310.13778 (2023)
  * [51] Rozier, K.Y.: Specification: The biggest bottleneck in formal methods and autonomy. In: VSTTE. Lecture Notes in Computer Science, vol. 9971, pp. 8–26 (2016)
  * [52] Shah, A., Kamath, P., Shah, J.A., Li, S.: Bayesian inference of temporal task specifications from demonstrations. In: NeurIPS. pp. 3808–3817 (2018)
  * [53] Valizadeh, M., Fijalkow, N., Berger, M.: LTL learning on gpus. CoRR abs/2402.12373 (2024). https://doi.org/10.48550/ARXIV.2402.12373, https://doi.org/10.48550/arXiv.2402.12373
  * [54] Wan, H., Liang, P., Du, J., Luo, W., Ye, R., Peng, B.: End-to-end learning of ltlf formulae by faithful ltlf encoding. In: AAAI. pp. 9071–9079. AAAI Press (2024)
  * [55] Wasylkowski, A., Zeller, A.: Mining temporal specifications from object usage. Autom. Softw. Eng. 18(3-4), 263–292 (2011)

##  Appendix A Structural conditions

As mentioned in the main part of the paper, we impose structural constraints
on the introduced variables to ensure that they do encode an ATL formula. The
constraints are similar to the ones proposed by Neider and Gavran [42]. We
define:

$\displaystyle\Omega_{\Lambda}$ $\displaystyle:=\Big{[}\bigwedge_{1\leq i\leq
n}\bigvee_{\lambda\in\Lambda}x_{i,\lambda}\Big{]}\land\Big{[}\bigwedge_{1\leq
i\leq n}\bigwedge_{\lambda\neq\lambda^{\prime}\in\Lambda}\lnot
x_{i,\lambda}\lor\lnot x_{i,\lambda^{\prime}}\Big{]},$
$\displaystyle\Omega_{l}$ $\displaystyle:=\Big{[}\bigwedge_{2\leq i\leq
n}\bigvee_{1\leq j\leq i}l_{i,j}\Big{]}\land\Big{[}\bigwedge_{2\leq i\leq
n}\bigwedge_{1\leq j<j^{\prime}<i}\lnot l_{i,j}\lor\lnot
l_{i,j^{\prime}}\Big{]},$ $\displaystyle\Omega_{r}$
$\displaystyle:=\Big{[}\bigwedge_{2\leq i\leq n}\bigvee_{1\leq j\leq
i}r_{i,j}\Big{]}\land\Big{[}\bigwedge_{2\leq i\leq n}\bigwedge_{1\leq
j<j^{\prime}<i}\lnot r_{i,j}\lor\lnot r_{i,j^{\prime}}\Big{]},$
$\displaystyle\Omega_{\mathcal{P}}$
$\displaystyle:=\bigvee_{p\in\mathcal{P}}x_{1,p}$

The formula $\Omega_{\Lambda}$ ensures that each node is labeled by exactly
one operator or one proposition. The formulas $\Omega_{l}$ and $\Omega_{r}$
enforce that each node (except for Node 1) has exactly one left and exactly
one right child, respectively. Finally, the formula $\Omega_{\mathcal{P}}$
ensures that Node $1$ is labeled by a proposition.

Based on a satisfying valuation $v$ of $\Omega^{\mathsf{str}}$, one can
straightforwardly construct a unique ATL formula as follows: label each Node
$i$ with the unique operator $\lambda$ for which $v(x_{i,\lambda})=1$, taking
into account the variables $(A_{i,a})_{a\in\mathsf{Ag}}$ if
$\lambda\in\\{\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{X}},\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{G}},\langle\\!\langle\cdot\rangle\\!\rangle\\!\operatorname{\mathbf{U}}\\}$,
and mark the left and right children of the node with the unique Nodes $j$ and
$j^{\prime}$ for which $v(l_{i,j})=1$ and $v(r_{i,j^{\prime}})=1$,
respectively.

##  Appendix B Correctness of the encoding

Consider a concurrent game structure $C=\langle
Q,I,k,\mathcal{P},\pi,\sigma,d,\delta\rangle$ and some integer
$n\in\mathbb{N}^{+}$. We consider the formulas $\Omega^{\mathsf{str}}_{n}$ and
$\Omega^{\mathsf{sem}}_{n}$. We let $X_{n}(C)$ denote the variables occurring
in these formulas. We have:

$\displaystyle X_{n}(C)=$ $\displaystyle X^{\mathsf{Var}}_{n}\cup
X^{\mathsf{Struct}}_{C}$

with

$\displaystyle X^{\mathsf{Var}}_{n}:=\;$ $\displaystyle\\{x_{i,\lambda}\mid
1\leq i\leq n,\;\lambda\in\Lambda\\}\cup\\{A_{i,a}\mid 1\leq i\leq
n,\;a\in\mathsf{Ag}\\}\cup$ $\displaystyle\\{l_{i,j},r_{i,j}\mid 1\leq i\leq
n,\;1\leq j\leq i-1\\}$

and

$\displaystyle X^{\mathsf{Struct}}_{C}:=$ $\displaystyle\;\\{y^{C}_{i,q}\mid
1\leq i\leq n,\;q\in Q\\}\cup$ $\displaystyle\;\\{y^{C}_{i,q,k}\mid 1\leq
i\leq n,\;q\in Q,\;1\leq k\leq|Q|+1\\}$

The proof of Proposition 6 is rather long and somewhat tedious. However, note
that there is not much difficulty involved. The length of the proof is due to
the several cases of all the operators to handle.

First of all, we define formally the ATL formula that a valuation
$v:X^{\mathsf{Var}}_{n}\rightarrow\mathbb{B}$ satisfying the
$\Omega^{\mathsf{str}}_{n}$ encodes.

######  Definition 26.

Consider a valuation $v:X^{\mathsf{Var}}_{n}\rightarrow\mathbb{B}$ satisfying
the formula $\Omega^{\mathsf{str}}_{n}$. We define $\mathsf{Op}:\llbracket
1,n\rrbracket\rightarrow\mathcal{P}\cup\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Un}}\cup\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Bin}}$
with
$\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Un}}:=\\{\neg,\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}},\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{G}}\mid A\subseteq\mathsf{Ag}\\}$
and
$\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Bin}}:=\\{\wedge,\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{U}}\mid A\subseteq\mathsf{Ag}\\}$.
Let $i\in\llbracket 1,n\rrbracket$. Since $v\models\Omega^{\mathsf{str}}_{n}$,
there is a unique $\lambda\in\Lambda$ such that $v(x_{i,\lambda})=1$. Then:

  * •

If $\lambda\in\mathcal{P}\cup\\{\neg,\wedge\\}$, we let
$\mathsf{Op}(i):=\lambda$;

  * •

If $\lambda=\langle\\!\langle\cdot\rangle\\!\rangle\\!\bullet$ for some
$\bullet\in\\{\operatorname{\mathbf{X}},\operatorname{\mathbf{G}},\operatorname{\mathbf{U}}\\}$,
we let $\mathsf{Op}(i):=\langle\\!\langle A_{i}\rangle\\!\rangle\\!\bullet$
with $A_{i}\subseteq\mathsf{Ag}$ such that for all $a\in\mathsf{Ag}$, we have
$a\in A_{i}$ if and only if $v(A_{i,a})=1$.

We also let $r:\llbracket 2,n\rrbracket\rightarrow\llbracket 1,n\rrbracket$ be
such that, for all $i\in\llbracket 2,n\rrbracket$, $r(i)\in\llbracket
1,i-1\rrbracket$ is such that $v(r_{i,r(i)})=1$. Note that there is exactly
one such $r(i)\in\llbracket 1,n\rrbracket$ because
$v\models\Omega^{\mathsf{str}}_{n}$. We define similarly $l:\llbracket
2,n\rrbracket\rightarrow\llbracket 1,n\rrbracket$.

Finally, we define the function $\Phi^{v}_{n}:\llbracket
1,n\rrbracket\rightarrow ATL$ as follows. For all $i\in\llbracket
1,n\rrbracket$:

  * •

If $\mathsf{Op}(i)\in\mathcal{P}$, then $\Phi^{v}_{n}(i):=\mathsf{Op}(i)$;

  * •

If $\mathsf{Op}(i)\in\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Un}}$, then
$\Phi^{v}_{n}(i):=\mathsf{Op}(i)\;\Phi^{v}_{n}(l(i))$;

  * •

If $\mathsf{Op}(i)\in\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Bin}}$,
then
$\Phi^{v}_{n}(i):=\Phi^{v}_{n}(l(i))\;\mathsf{Op}(i)\;\Phi^{v}_{n}(r(i))$.

One can show by induction (on the tree structure induced by the children
relations given by the functions $l$ and $r$) that we do have that for all
$i\in\llbracket 1,n\rrbracket$, $\Phi^{v}_{n}(i)$ is an ATL formula.

We can finally define the ATL formula $\Phi^{v}$ that $v$ encodes:
$\Phi^{v}:=\Phi^{v}_{n}(n)$.

######  Remark 27.

A valuation satisfying the formula $\Omega^{\mathsf{str}}_{n}$ encodes a
single ATL formula. On the other hand, given an ATL formula $\Phi$, there
exist (several) valuations satisfying the formula $\Omega^{\mathsf{str}}_{n}$
that encode the formula $\Phi$. We do not give a proof of this statement here,
a similar statement is proved in [42, Lemma 1]. We define such a valuation by
considering a syntax DAG of $\Phi$.

Let us now show the formula $\Omega^{\mathsf{sem}}_{n}$ does capture the
semantics of ATL formula.

######  Lemma 28.

Consider a valuation $v:X^{\mathsf{Var}}_{n}\rightarrow\mathbb{B}$ satisfying
the formula $\Omega^{\mathsf{str}}_{n}$. For all $q\in Q$, we have:

$q\models\Phi^{v}\text{ iff }v(y_{n,q}^{C})=1$

We are going to prove this lemma by induction on the tree structure of the set
$\llbracket 1,n\rrbracket$. Before we proceed to the proof of this lemma, we
state and prove intermediate lemmas handling the temporal and strategic ATL
operators on their own.

First of all, we tackle the formula $\Omega_{q,i}^{\mathsf{Pre}}(y)$ in the
lemma below.

######  Lemma 29.

Consider a valuation $v:X_{n}(C)\rightarrow\mathbb{B}$ satisfying the formula
$\Omega^{\mathsf{str}}_{n}\wedge\Omega^{\mathsf{sem}}_{n}$. Let $q\in Q$ and
$i\in\llbracket 1,n\rrbracket$. For all predicates $Y\subseteq Q$, defined
with $(v(y_{q}))_{q\in Q}$, we have (recall that $A_{i}$ is defined in
Definition 26):

$v\models\Omega_{q,i}^{\mathsf{Pre}}(y)\text{ iff
}q\in\mathsf{Pre}_{A_{i}}(Y)$

###### Proof.

Let $\alpha\in\mathsf{Act}_{\mathsf{Ag}}(q)$. Let $\Omega_{\alpha}$ denote the
conjunction in $\Omega_{q,i}^{\mathsf{Pre}}(y)$ evaluated with the tuple of
actions $\alpha\in\mathsf{Act}_{\mathsf{Ag}}(q)$. We let
$\alpha_{i}\in\mathsf{Act}_{A_{i}}$ be such that, for all $a\in A_{i}$, we
have $\alpha_{i}(a):=\alpha(a)$. We claim that $v\models\Omega_{\alpha}$ if
and only if for all $q^{\prime}\in\mathsf{Succ}(q,\alpha_{i})$, we have
$q^{\prime}\in Y$ (i.e. $v(y_{q^{\prime}})=1$). We denote by
$\mathsf{Act}_{\mathsf{Ag}}(\alpha_{i})$ the set of tuples of actions that
coincide with $\alpha_{i}$ on $A_{i}$. Then, $v\models\Omega_{\alpha}$ iff for
all $\alpha^{\prime}\in\mathsf{Act}_{\mathsf{Ag}}$ such that, for all
$a\in\mathsf{Ag}$, if $v(A_{i,a})=1$, then $\alpha(a)=\alpha^{\prime}(a)$, we
have $v(y_{\delta(q,\alpha^{\prime})})=1$. By definition of $A_{i}$, this is
equivalent to for all
$\alpha^{\prime}\in\mathsf{Act}_{\mathsf{Ag}}(\alpha_{i})$, we have
$v(y_{\delta(q,\alpha^{\prime})})=1$. This is equivalent to, for all tuple of
actions $\alpha_{i}^{\prime}\in\mathsf{Act}_{\mathsf{Ag}\setminus A_{i}}$, we
have $v(y_{\delta(q,(\alpha_{i},\alpha_{i}^{\prime}))})=1$. That is, for all
$q^{\prime}\in\mathsf{Succ}(q,\alpha_{i})$, we have $q^{\prime}\in Y$. We have
established that $v\models\Omega_{\alpha}$ if and only if
$\mathsf{Succ}(q,\alpha_{i})\subseteq Y$ for all tuples of actions
$\alpha\in\mathsf{Act}_{\mathsf{Ag}}(q)$. The lemma follows. ∎

This will allow us to formally tackle the case of the operator
$\operatorname{\mathbf{X}}$ in the proof of Lemma 28. Let us consider the
slightly more involved case of the operator $\operatorname{\mathbf{U}}$.

######  Lemma 30.

Consider a valuation $v:X_{n}(C)\rightarrow\mathbb{B}$ satisfying the formula
$\Omega^{\mathsf{str}}_{n}\wedge\Omega^{\mathsf{sem}}_{n}$. Let
$i\in\mathsf{Defined}^{v}$. Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{U}}$ and that, for all $q\in
Q$, we have $v(y_{q,l(i)}^{C})=1$ if and only if $q\models\Phi^{v}(l(i))$ and
$v(y_{q,r(i)}^{C})=1$ if and only if $q\models\Phi^{v}(r(i))$. Then, for all
$q\in Q$, we have:

$q\models\Phi^{v}(i)\text{ if and only if }v(y_{i,q}^{C})=1$

###### Proof.

Recall that we have:

$\Phi^{v}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\;\Phi^{v}(l(i))\;\operatorname{\mathbf{U}}\;\Phi^{v}(r(i))$

Consider Algorithm 1. For all $0\leq j\leq|Q|$, we let $S_{j}\subseteq Q$
denote the set $S$ when exiting the _for_ loop when $k=j$. When $j=0$, this
corresponds to initialization of the set $S$ before the _for_ loop is ever
entered. We show by induction on $0\leq k\leq|Q|$ the property
$\mathcal{P}(k)$: for all states $q\in Q$, we have $v(y^{C}_{i,q,k})=1$ if and
only if $q\in S_{k}$.

  * •

Let $q\in Q$. We have $S_{0}=\mathsf{SAT}_{C}(\Phi^{v}(r(i)))$, i.e. $q\in
S_{0}$ iff $q\models\Phi^{v}(r(i))$. Since
$v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{U}}}$, we have
$v(y_{i,q,0}^{C})=v(y_{r(i),q}^{C})$. Furthermore, by assumption,
$v(y_{q,r(i)}^{C})=1$ if and only if $q\models\Phi^{v}(r(i))$. Therefore,
$q\in S_{0}$ if and only if $v(y_{i,q,0}^{C})=1$. Hence, $\mathcal{P}(0)$
holds.

  * •

Assume now that $\mathcal{P}(k)$ holds for some $0\leq k\leq|Q|-1$. Let $q\in
Q$. Assume that $q\in S_{k+1}$. If $q\in S_{k}$, then by $\mathcal{P}(k)$, we
have $v(y^{C}_{i,q,k})=1$. Since
$v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{U}}}$, this implies
$v(y^{C}_{i,q,k+1})=1$. Assume now that $q\in S_{k+1}\setminus S_{k}$. In that
case, we have $q\in\mathsf{SAT}_{C}(\Phi^{v}(l(i)))$, i.e.
$q\models\Phi^{v}(l(i))$. Therefore, by assumption, $v(y_{q,l(i)}^{C})=1$. In
addition, we also have $q\in\mathsf{Pre}_{A_{i}}(S_{k})$. Therefore, by Lemma
29, this implies $v\models\Omega_{q,i}^{\mathsf{Pre}}(y)$ for a collection of
variables $(y_{q})_{q\in Q}$ such that, for all $q^{\prime}\in Q$, we have
$v(y_{q^{\prime}})=1$ if and only if $q^{\prime}\in S_{k}$. By
$\mathcal{P}(k)$, this is verified by the collection $(y_{i,q,k}^{C})_{q\in
Q}$. Therefore, $v\models\Omega_{q,i}^{\mathsf{Pre}}(y_{i,\cdot,k}^{C})$ and
since $v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{U}}}$, we have
$v(y^{C}_{i,q,k+1})=1$.

Assume now $v(y^{C}_{i,q,k+1})=1$. Since
$v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{U}}}$, we have
$v(y^{C}_{i,q,k})=1$ or $v\models
y_{q,l(i)}^{C}\wedge\Omega_{q,i}^{\mathsf{Pre}}(y_{i,\cdot,k}^{C})$. In the
first case, this implies $q\in S_{k}$, by $\mathcal{P}(k)$. In the second
case, this implies both $v(y_{q,l(i)}^{C})=1$, i.e.
$q\in\mathsf{SAT}_{C}(\Phi^{v}(l(i)))$, and by Lemma 29 and $\mathcal{P}(k)$,
$q\in\mathsf{Pre}_{A_{i}}(S_{k})$. Therefore, in both cases, we have $q\in
S_{k+1}$. Thus, $\mathcal{P}(k+1)$ holds.

In fact, $\mathcal{P}(k)$ holds for all $0\leq k\leq|Q|$. Therefore, by
$\mathcal{P}(|Q|)$ and since
$v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{U}}}$, for all $q\in Q$,
we have $q\in S_{|Q|}=\mathsf{SAT}_{C}(\Phi^{v}(i))$, i.e.
$q\models\Phi^{v}(i)$, if and only if $v(y^{C}_{i,q})=v(y^{C}_{i,q,|Q|})=1$. ∎

Let us now tackle the similar case of the operator
$\operatorname{\mathbf{G}}$.

######  Lemma 31.

Consider a valuation $v:X_{n}(C)\rightarrow\mathbb{B}$ satisfying the formula
$\Omega^{\mathsf{str}}_{n}\wedge\Omega^{\mathsf{sem}}_{n}$. Let
$i\in\mathsf{Defined}^{v}$. Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{G}}$ and that, for all $q\in
Q$, we have $v(y_{q,l(i)}^{C})=1$ if and only if $q\models\Phi^{v}(l(i))$.
Then, for all $q\in Q$, we have:

$q\models\Phi^{v}(i)\text{ if and only if }v(y_{i,q}^{C})=1$

The proof of this lemma is very close to the proof of Lemma 30.

###### Proof.

Recall that we have:

$\Phi^{v}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\;\operatorname{\mathbf{G}}\;\Phi^{v}(l(i))$

Consider Algorithm 2. For all $0\leq j\leq|Q|$, we let $S_{j}\subseteq Q$
denote the set $S$ when exiting the _for_ loop when $k=j$. When $j=0$, this
corresponds to initialization of the set $S$ before the _for_ loop is ever
entered. We show by induction on $0\leq k\leq|Q|$ the property
$\mathcal{P}(k)$: for all states $q\in Q$, we have $v(y^{C}_{i,q,k})=1$ if and
only if $q\in S_{k}$.

  * •

Let $q\in Q$. We have $S_{0}=\mathsf{SAT}_{C}(\Phi^{v}(l(i)))$, i.e. $q\in
S_{0}$ iff $q\models\Phi^{v}(l(i))$. Since
$v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{G}}}$, we have
$v(y_{i,q,0}^{C})=v(y_{l(i),q}^{C})$. Furthermore, by assumption,
$v(y_{q,l(i)}^{C})=1$ if and only if $q\models\Phi^{v}(l(i))$. Therefore,
$q\in S_{0}$ if and only if $v(y_{i,q,0}^{C})=1$. Hence, $\mathcal{P}(0)$
holds.

  * •

Assume now that $\mathcal{P}(k)$ holds for some $0\leq k\leq|Q|-1$. Let $q\in
Q$. Assume that $q\in S_{k+1}$. In that case, we have $q\in S_{k}$, and hence
by $\mathcal{P}(k)$, we have $v(y^{C}_{i,q,k})=1$. In addition, we also have
$q\in\mathsf{Pre}_{A_{i}}(S_{k})$. Therefore, by Lemma 29, this implies
$v\models\Omega_{q,i}^{\mathsf{Pre}}(y)$ for a collection of variables
$(y_{q})_{q\in Q}$ such that, for all $q^{\prime}\in Q$, we have
$v(y_{q^{\prime}})=1$ if and only if $q^{\prime}\in S_{k}$. By
$\mathcal{P}(k)$, this is verified by the collection $(y_{i,q,k}^{C})_{q\in
Q}$. Therefore, $v\models\Omega_{q,i}^{\mathsf{Pre}}(y_{i,\cdot,k}^{C})$.
Since $v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{G}}}$, it follows
that $v(y^{C}_{i,q,k+1})=1$.

Assume now $v(y^{C}_{i,q,k+1})=1$. Since
$v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{G}}}$, we have
$v(y^{C}_{i,q,k})=1$ and
$v\models\Omega_{q,i}^{\mathsf{Pre}}(y_{i,\cdot,k}^{C})$. Hence, by
$\mathcal{P}(k)$, we have $q\in S_{k}$. In addition, by Lemma 29 and
$\mathcal{P}(k)$, we have $q\in\mathsf{Pre}_{A_{i}}(S_{k})$. Therefore, $q\in
S_{k+1}$. Thus, $\mathcal{P}(k+1)$ holds.

In fact, $\mathcal{P}(k)$ holds for all $0\leq k\leq|Q|$. By
$\mathcal{P}(|Q|)$ and since
$v\models\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{G}}}$, for all $q\in Q$,
we have $q\in S_{|Q|}=\mathsf{SAT}_{C}(\Phi^{v}(i))$, i.e.
$q\models\Phi^{v}(i)$, if and only if $v(y^{C}_{i,q})=v(y^{C}_{i,q,|Q|})=1$. ∎

We can now proceed to the proof of Lemma 28.

###### Proof.

Let us define a tree structure (with possibly muiltiple roots) on $\llbracket
1,n\rrbracket$ has a tree structure. For all $i\in\llbracket 1,n\rrbracket$:

  * •

If $\mathsf{Op}(i)\in\mathcal{P}$, then $i$ is a leaf;

  * •

If $\mathsf{Op}(i)\in\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Un}}$, then
$i$ has one child $l(i)$;

  * •

If $\mathsf{Op}(i)\in\mathsf{Op}(\mathcal{P},\mathsf{Ag})_{\mathsf{Bin}}$,
then $i$ has two children $l(i),r(i)$.

On this tree structure, let us prove by induction the property
$\mathcal{P}(i)$ for $i\in\llbracket 1,n\rrbracket$: for all $q\in Q$, we have
$q\models\Phi^{v}(i)\text{ iff }v(y_{i,q}^{C})=1$.

  * •

Let $i\in\llbracket 1,n\rrbracket$ be a leaf. In that case, we have
$\Phi^{v}(i)=\mathsf{Op}(i)\in\mathcal{P}$. Since
$v\models\Omega_{\mathcal{P}}^{\mathsf{sem}}$, for all $q\in Q$, we have
$v(y_{i,q}^{C})=1$ if and only if $\Phi^{v}(i)\in\pi(q)$, i.e.
$q\models\Phi^{v}(i)$. Hence, $\mathcal{P}(i)$ holds.

  * •

Let $i\in\llbracket 1,n\rrbracket$ be with a single child $l(i)\in\llbracket
1,n\rrbracket$. Assume that $\mathcal{P}(l(i))$ holds. There are three cases:

    * –

Assume that $\mathsf{Op}(i)=\neg$. Since
$v\models\Omega_{\neg}^{\mathsf{sem}}$, we have
$v(y_{i,q}^{C})=1-v(y_{l(i),q}^{C})$. Therefore, by $\mathcal{P}(l(i))$, for
all $q\in Q$, we have $q\models\Phi^{v}(i)=\neg\Phi^{v}(l(i))$ iff
$v(y_{l(i),q}^{C})=0$ iff $v(y_{i,q}^{C})=1$.

    * –

Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{X}}$. Since
$v\models\Omega_{\operatorname{\mathbf{X}}}^{\mathsf{sem}}$, for all $q\in Q$,
we have $v(y_{i,q}^{C})=1$ iff
$v\models\Omega_{q,i}^{\mathsf{Pre}}(y_{l(i)}^{C})$ iff (by Lemma 29 and
$\mathcal{P}(l(i))$)
$q\in\mathsf{Pre}_{A_{i}}(\mathsf{SAT}_{C}(\Phi^{v}(l(i))))$ iff
$q\models\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi^{v}(l(i))=\Phi^{v}(i)$.

    * –

Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{G}}$. By Lemma 31 and
$\mathcal{P}(l(i))$, for all $q\in Q$, we have $q\models\Phi^{v}(i)$ iff
$v(y_{i,q}^{C})=1$.

Hence, $\mathcal{P}(i)$ holds.

  * •

Let $i\in\llbracket 1,n\rrbracket$ be with two children
$l(i),r(i)\in\llbracket 1,n\rrbracket$. Assume that $\mathcal{P}(l(i))$ and
$\mathcal{P}(r(i))$ hold. There are two cases:

    * –

Assume that $\mathsf{Op}(i)=\wedge$. Since
$v\models\Omega_{\wedge}^{\mathsf{sem}}$, it follows that
$v(y_{i,q}^{C})=\min(v(y_{l(i),q}^{C}),v(y_{r(i),q}^{C}))$. Therefore, by
$\mathcal{P}(l(i))$ and $\mathcal{P}(r(i))$, for all $q\in Q$, we have
$q\models\Phi^{v}(i)=\Phi^{v}(l(i))\wedge\Phi^{v}(r(i))$ iff
$v(y_{l(i),q}^{C})=1$ and $v(y_{r(i),q}^{C})=1$ iff $v(y_{i,q}^{C})=1$.

    * –

Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{U}}$. By Lemma 30 and
$\mathcal{P}(l(i))$ and $\mathcal{P}(r(i))$, for all $q\in Q$, we have
$q\models\Phi^{v}(i)$ iff $v(y_{i,q}^{C})=1$.

Hence, $\mathcal{P}(i)$ holds.

Therefore, $\mathcal{P}(i)$ holds for all $i\in\llbracket 1,n\rrbracket$. The
lemma is then given by $\mathcal{P}(n)$ since $\Phi^{v}=\Phi^{v}(n)$. ∎

We can finally prove Proposition 6.

###### Proof.

Assume that there is an ATL formula $\Phi$ of size $n$ consistent with
$\mathcal{S}$. Consider a valuation
$v:X^{\mathsf{Var}}_{n}\rightarrow\mathbb{B}$ such that $\Phi=\Phi^{v}$. Let
$C\in P\cup N$. Let us show that we can define $v$ on
$X_{C}^{\mathsf{Struct}}$ such that $v\models\Omega_{n,C}^{\mathsf{sem}}$. As
for the proof of Lemma 28, we define $v$ by induction on the tree structure of
the set $\llbracket 1,n\rrbracket$.

  * •

Let $i\in\llbracket 1,n\rrbracket$ be a leaf. For all $q\in Q$, we set
$v(y_{i,q}^{C}):=1$ if and only if $p\in\pi(q)$. That way, the formula
$\Omega^{\mathsf{sem}}_{\mathcal{P}}$ is satisfied by $v$ for the index $i$.
For all $0\leq k\leq|Q|$, $v(y_{i,q,k}^{C})$ is defined arbitrarily.

  * •

Let $i\in\llbracket 1,n\rrbracket$ be with a single child $l(i)\in\llbracket
1,i-1\rrbracket$. Assume that $v$ is defined on
$X_{C,l(i)}^{\mathsf{Struct}}$. There are three cases:

    * –

Assume that $\mathsf{Op}(i)=\neg$. For all $q\in Q$, we let
$v(y_{i,q}^{C}):=1-v(y_{l(i),q}^{C})$. That way, the formula
$\Omega^{\mathsf{sem}}_{\neg}$ is satisfied by $v$ for the index $i$. For all
$0\leq k\leq|Q|$, $v(y_{i,q,k}^{C})$ is defined arbitrarily.

    * –

Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{X}}$. For all $q\in Q$, we set
$v(y_{i,q}^{C})=1$ iff $v\models\Omega_{q,i}^{\mathsf{Pre}}(y_{l(i)}^{C})$.
That way, the formula $\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{X}}}$ is
satisfied by $v$ for the index $i$. For all $0\leq k\leq|Q|$,
$v(y_{i,q,k}^{C})$ is defined arbitrarily.

    * –

Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{G}}$. Let $q\in Q$. We set
$v(y^{C}_{i,q,0}):=v(y^{C}_{l(i),q})$. Furthermore, for all $0\leq
k\leq|Q|-1$, if $v\models\Omega_{q,i}^{\mathsf{Pre}}(y^{C}_{i,\cdot,k})$, we
set $v(y^{C}_{i,q,k+1}):=v(y^{C}_{i,q,k})$, otherwise $v(y^{C}_{i,q,k+1}):=0$.
Finally, we set $v(y^{C}_{i,q}):=v(y^{C}_{i,q,|Q|})$. That way, the formula
$\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{G}}}$ is satisfied by $v$ for
the index $i$.

  * •

Let $i\in\llbracket 1,n\rrbracket$ be with two children
$l(i),r(i)\in\llbracket 1,i-1\rrbracket$. Assume that $v$ is defined on
$X_{C,l(i)}^{\mathsf{Struct}}$ and $X_{C,r(i)}^{\mathsf{Struct}}$. There are
two cases:

    * –

Assume that $\mathsf{Op}(i)=\wedge$. For all $q\in Q$, we set
$v(y_{i,q}^{C}):=\min(v(y_{l(i),q}^{C}),v(y_{r(i),q}^{C}))$. That way, the
formula $\Omega^{\mathsf{sem}}_{\wedge}$ is satisfied by $v$ for the index
$i$. For all $0\leq k\leq|Q|$, $v(y_{i,q,k}^{C})$ is defined arbitrarily.

    * –

Assume that $\mathsf{Op}(i)=\langle\\!\langle
A_{i}\rangle\\!\rangle\\!\operatorname{\mathbf{U}}$. We set
$v(y^{C}_{i,q,0}):=v(y^{C}_{r(i),q})$. Furthermore, for all $0\leq
k\leq|Q|-1$, if $v\not\models\Omega_{q,i}^{\mathsf{Pre}}(y^{C}_{i,\cdot,k})$,
we set $v(y^{C}_{i,q,k+1}):=v(y^{C}_{i,q,k})$, otherwise
$v(y^{C}_{i,q,k+1}):=\max(v(y^{C}_{i,q,k}),v(y^{C}_{l(i),q}))$. Finally, we
set $v(y^{C}_{i,q}):=v(y^{C}_{i,q,|Q|})$. That way, the formula
$\Omega^{\mathsf{sem}}_{\operatorname{\mathbf{U}}}$ is satisfied by $v$ for
the index $i$.

We have shown that we can define the valuation $v$ on
$X_{C}^{\mathsf{Struct}}$ such that $v\models\Omega_{n,C}^{\mathsf{sem}}$. For
all $C\in P\cup N$, we define on $X_{C}^{\mathsf{Struct}}$ such that
$v\models\Omega_{n,C}^{\mathsf{sem}}$. Then, since $\Phi$ is consistent with
$S$, for all positive structures $C\in P$ and initial states $q\in I$, we have
$s\models\Phi$. Therefore, by Lemma 28, $v(y^{C}_{n,s})=1$. On the other hand,
for all negative structures $C\in N$, there is an initial state $q\in I$ such
that we have $s\not\models\Phi$. Therefore, by Lemma 28, $v(y^{C}_{n,s})=0$.
Hence, we have $v\models\Omega^{\mathsf{con}}_{n}$. That is,
$v\models\Omega^{\S}_{n}$.

Now, let us assume that $\Omega^{\S}_{n}$ is satisfiable. Consider a valuation
$v$ such that $v\models\Omega^{\S}_{n}$. Since
$v\models\Omega_{n}^{\mathsf{str}}$, there is an ATL formula $\Phi^{v}$ of
size at most $n$ that this valuation encodes. Consider a positive (resp.
negative) structure $C\in P$. Since $v\models\Omega^{\mathsf{con}}_{n}$ and by
Lemma 28 (since $v\models\Omega_{n}^{\mathsf{sem}}$), we have $C\models\Phi$
(resp. $C\not\models\Phi$). Hence the valuation $v$ is consistent with $S$. ∎

##  Appendix C Deciding separability

###  C.1 Proof of Lemma 12

The proof of this lemma is not complicated, but is a little long due the need
to handle all operators, and especially the operators
$\operatorname{\mathbf{G}}$ and $\operatorname{\mathbf{U}}$.

######  Lemma 32.

Let $n\in\mathbb{N}$. Consider a set of agents $\mathsf{Ag}$, a coalition of
agents $A\subseteq\mathsf{Ag}$ and an ATL formula $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\Phi_{1}\operatorname{\mathbf{U}}\Phi_{2}$.

For all $k\in\mathbb{N}$, we define the ATL formula
$\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})$. We set:

  * •

$\Phi_{\operatorname{\mathbf{X}},0}(A,\Phi_{1},\Phi_{2}):=\Phi_{2}$;

  * •

for all $k\in\mathbb{N}$,
$\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2}):=\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})\lor(\Phi_{1}\wedge\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2}))$.

Let $n\in\mathbb{N}$. For all CGS $C$ with $n$ states, for all states $q\in C$
and for all $k\geq n$, we have $q\models\Phi$ if and only if
$q\models\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})$.

###### Proof.

Consider a CGS $C$ with $n$ states. As for the proof of Lemma 30, let us
consider Algorithm 1. For all $0\leq j\leq|Q|$, we let $S_{j}\subseteq Q$
denote the set $S$ when exiting the _for_ loop when $k=j$. When $j=0$, this
corresponds to initialization of the set $S$ before the _for_ loop is ever
entered. We show by induction on $0\leq k\leq n$ the property
$\mathcal{P}(k)$:
$S_{k}=\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2}))$.

For $k=0$, we have
$\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})=\Phi_{2}$, hence
$\mathcal{P}(0)$ straightforwardly holds. Assume now that $\mathcal{P}(k)$
holds for some $k\in\mathbb{N}$. Let $q\in Q$. We have:

$\displaystyle q\in S_{k+1}$ $\displaystyle\text{ iff }q\in S_{k}\text{ or
}q\in\mathsf{SAT}_{C}(\Phi_{1})\cap\mathsf{Pre}_{A}(S_{k})$
$\displaystyle\text{ iff
}q\models\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})\text{ or
}q\models\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})\text{ and
}q\models\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})$
$\displaystyle\text{ iff
}q\models\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2})$

Thus, $\mathcal{P}(k+1)$ follows. In fact, $\mathcal{P}(k)$ holds for all
$0\leq k\leq n$. Since $S_{n}=\mathsf{SAT}_{C}(\Phi)$, it follows that we have
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},n}(A,\Phi_{1},\Phi_{2}))=\mathsf{SAT}_{C}(\Phi)$.

Let us show that
$\mathsf{SAT}_{C}(\Phi_{1})\cap\mathsf{Pre}_{A}(S_{n})\subseteq
S_{n}=\mathsf{SAT}_{C}(\Phi)$. There are two cases:

  * •

Either $S_{n}=Q$, and in that case the inclusion is obvious.

  * •

Or $S_{n}\neq Q$, and in that case, since for all $0\leq k\leq n-1$, we have
$S_{k}\subseteq S_{k+1}$, and $|Q|=n$, it follows that there is some $k\leq
n-1$ such that $S_{k}=S_{k+1}$. That is,
$\mathsf{SAT}_{C}(\Phi_{1})\cap\mathsf{Pre}_{A}(S_{k})\subseteq S_{k}$. This
straightforwardly implies that, for all $k\leq i\leq n$, we have $S_{k}=S_{i}$
and $\mathsf{SAT}_{C}(\Phi_{1})\cap\mathsf{Pre}_{A}(S_{i})\subseteq S_{i}$.

Now, consider any $k\in\mathbb{N}$ and assume that
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2}))=\mathsf{SAT}_{C}(\Phi)$.
Let us show that
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2}))=\mathsf{SAT}_{C}(\Phi)$.
Clearly,
$\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2})\implies\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2})$,
hence
$\mathsf{SAT}_{C}(\Phi)\subseteq\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2}))$.
On the other hand, consider any
$q\in\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2}))$.
If $q\notin\mathsf{SAT}_{C}(\Phi)$, then
$q\in\mathsf{SAT}_{C}(\Phi_{1})\cap\mathsf{Pre}_{A}(\mathsf{SAT}_{C}(\Phi))$.

Hence, we do have:
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2}))=\mathsf{SAT}_{C}(\Phi)$.
Therefore, for all $k\geq n$, we have
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi_{1},\Phi_{2}))=\mathsf{SAT}_{C}(\Phi)$.
The lemma follows. ∎

We state a lemma analogous to Lemma 32 for the operator
$\operatorname{\mathbf{G}}$.

######  Lemma 33.

Consider a set of agents $\mathsf{Ag}$, a coalition of agents
$A\subseteq\mathsf{Ag}$ and an ATL formula $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{G}}\Phi^{\prime}$.

For all $k\in\mathbb{N}$, we define the ATL formula
$\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})$. We set:

  * •

$\Phi_{\operatorname{\mathbf{X}},0}(A,\Phi^{\prime}):=\Phi^{\prime}$;

  * •

for all $k\in\mathbb{N}$,
$\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi^{\prime}):=\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})\wedge\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})$.

Let $n\in\mathbb{N}$. For all CGS $C$ with $n$ states, for all states $q\in C$
and for all $k\geq n$, we have $q\models\Phi$ if and only if
$q\models\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})$.

We proceed very similarly than the proof of Lemma 32.

###### Proof.

Consider a CGS $C$ with $n$ states. As for the proof of Lemma 31, let us
consider Algorithm 2. For all $0\leq j\leq|Q|$, we let $S_{j}\subseteq Q$
denote the set $S$ when exiting the _for_ loop when $k=j$. When $j=0$, this
corresponds to initialization of the set $S$ before the _for_ loop is ever
entered. We show by induction on $0\leq k\leq n$ the property
$\mathcal{P}(k)$:
$S_{k}=\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime}))$.

For $k=0$, we have
$\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})=\Phi^{\prime}$, hence
$\mathcal{P}(0)$ straightforwardly holds. Assume now that $\mathcal{P}(k)$
holds for some $k\in\mathbb{N}$. Let $q\in Q$. We have:

$\displaystyle q\in S_{k+1}$ $\displaystyle\text{ iff }q\in S_{k}\text{ and
}q\in\mathsf{Pre}_{A}(S_{k})$ $\displaystyle\text{ iff
}q\models\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})\text{ and
}q\models\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})$
$\displaystyle\text{ iff
}q\models\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi^{\prime})$

Thus, $\mathcal{P}(k+1)$ follows. In fact, $\mathcal{P}(k)$ holds for all
$0\leq k\leq n$. Since $S_{n}=\mathsf{SAT}_{C}(\Phi)$, it follows that we have
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},n}(A,\Phi^{\prime}))=\mathsf{SAT}_{C}(\Phi)$.

Let us show that
$\mathsf{SAT}_{C}(\Phi)\subseteq\mathsf{Pre}_{A}(\mathsf{SAT}_{C}(\Phi))$. We
have $S_{n}=\mathsf{SAT}_{C}(\Phi)$. There are two cases:

  * •

Either $S_{n}=\emptyset$, and in that case the inclusion is obvious.

  * •

Or $S_{n}\neq\emptyset$, and in that case, since for all $0\leq k\leq n-1$, we
have $S_{k}\supseteq S_{k+1}$, and $|Q|=n$, it follows that there is some
$k\leq n-1$ such that $S_{k}=S_{k+1}$ and
$S_{k}\subseteq\mathsf{Pre}_{A}(S_{k})$. This straightforwardly implies that,
for all $k\leq i\leq n$, we have $S_{k}=S_{i}$ and
$S_{i}\subseteq\mathsf{Pre}_{A}(S_{i})$.

Now, consider any $k\in\mathbb{N}$ and assume that
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime}))=\mathsf{SAT}_{C}(\Phi)$.
Let us show that
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi^{\prime}))=\mathsf{SAT}_{C}(\Phi)$.
Clearly,
$\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi^{\prime})\implies\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})$,
hence
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi_{1},\Phi_{2}))\subseteq\mathsf{SAT}_{C}(\Phi)$.
On the other hand, consider any
$q\in\mathsf{SAT}_{C}(\Phi)\subseteq\mathsf{Pre}_{A}(\mathsf{SAT}_{C}(\Phi))=\mathsf{Pre}_{A}(\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})))$.
Therefore, we have
$q\in\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime}))\cap\mathsf{Pre}_{A}(\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime})))=\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi^{\prime}))$.

Hence, we do have:
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k+1}(A,\Phi^{\prime}))=\mathsf{SAT}_{C}(\Phi)$.
Therefore, for all $k\geq n$, we have
$\mathsf{SAT}_{C}(\Phi_{\operatorname{\mathbf{X}},k}(A,\Phi^{\prime}))=\mathsf{SAT}_{C}(\Phi)$.
The lemma follows. ∎

We can now proceed to the proof of Lemma 12.

###### Proof.

Let $n\in\mathbb{N}$. Let us prove by induction on ATL formulas $\Phi$ the
property $\mathcal{P}(\Phi)$: there exists an ATL-$\operatorname{\mathbf{X}}$
formula $\Phi^{\prime}$ that is equivalent $\Phi$ on CGS with at most $n$
states.

This straightforwardly holds for ATL formulas $\Phi\in\mathcal{P}$ since such
formulas are also ATL-$\operatorname{\mathbf{X}}$ formulas. Then:

  * •

Let $\Phi=\neg\Phi_{1}$ be an ATL formula and assume that
$\mathcal{P}(\Phi_{1})$ holds. Consider an ATL-$\operatorname{\mathbf{X}}$
formulas $\Phi_{1}^{\prime}$ equivalent to $\Phi_{1}$ on CGS with at most $n$
states. Then, $\Phi^{\prime}:=\neg\Phi_{1}^{\prime}$ is an
ATL-$\operatorname{\mathbf{X}}$ formula equivalent to $\Phi$ on CGS with at
most $n$ states. Hence, $\mathcal{P}(\Phi)$ holds.

  * •

Let $\Phi=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi_{1}$ be an ATL formula for
a coalition of agents $A\subseteq\mathsf{Ag}$ and assume that
$\mathcal{P}(\Phi_{1})$ holds. Consider an ATL-$\operatorname{\mathbf{X}}$
formulas $\Phi_{1}^{\prime}$ equivalent to $\Phi_{1}$ on CGS with at most $n$
states. Then, $\Phi^{\prime}:=\langle\\!\langle
A\rangle\\!\rangle\\!\operatorname{\mathbf{X}}\Phi_{1}^{\prime}$ is an
ATL-$\operatorname{\mathbf{X}}$ formula equivalent to $\Phi$ on CGS with at