The Complexity of Learning LTL, CTL and ATL Formulas

Bordais, Benjamin; Neider, Daniel; Roy, Rajarshi

doi:10.4230/LIPIcs.STACS.2025.19

The Complexity of Learning LTL, CTL and ATL Formulas

Benjamin Bordais

TU Dortmund University, Center for Trustworthy Data Science and Security, University Alliance Ruhr, Dortmund, Germany Daniel Neider

TU Dortmund University, Center for Trustworthy Data Science and Security, University Alliance Ruhr, Dortmund, Germany Rajarshi Roy

Department of Computer Science, University of Oxford, UK

Abstract

We consider the problem of learning temporal logic formulas from examples of system behavior. Learning temporal properties has crystallized as an effective means to explain complex temporal behaviors. Several efficient algorithms have been designed for learning temporal formulas. However, the theoretical understanding of the complexity of the learning decision problems remains largely unexplored. To address this, we study the complexity of the passive learning problems of three prominent temporal logics, Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL) and several of their fragments. We show that learning formulas with unbounded occurrences of binary operators is NP-complete for all of these logics. On the other hand, when investigating the complexity of learning formulas with bounded occurrences of binary operators, we exhibit discrepancies between the complexity of learning LTL, CTL and ATL formulas (with a varying number of agents).

Keywords and phrases:

Temporal logic, passive learning, complexity

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

Related Version:

Full Version: https://arxiv.org/abs/2408.04486 [8]

Funding:

Rajarshi Roy acknowledges partial funding by the ERC under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.834115, FUN2MODEL).

DOI:

10.4230/LIPIcs.STACS.2025.19

Event:

42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Editors:

Olaf Beyersdorff, Michał Pilipczuk, Elaine Pimentel, and Nguyễn Kim Thắng

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Temporal logics are the de-facto standard for expressing temporal properties for software and cyber-physical systems. Originally introduced in the context of program verification [33, 15], temporal logics are now well-established in numerous areas, including reinforcement learning [40, 25, 10], motion planning [17, 12], process mining [13], and countless others. The popularity of temporal logics can be attributed to their unique blend of mathematical rigor and resemblance to natural language.

Until recently, formulating properties in temporal logics has been a manual task, requiring human intuition and expertise [6, 39]. To circumvent this step, in the past ten years, there have been numerous works to automatically learn (i.e., generate) properties in temporal logic. Among them, a substantial number of works [29, 11, 35, 26, 41] target Linear Temporal Logic (LTL) [33]. There is now a growing interest in learning formulas [16, 34, 9] in Computation Tree Logic (CTL) [15] and Alternating-time Temporal Logic (ATL) [1] due to their ability to express branching-time properties, including for multi-agent systems.

While existing approaches for learning temporal properties demonstrate impressive empirical performance, detailed comparisons of computational complexity across different temporal logics remain underexplored. Most related works focus on LTL, either in the verification domain [18, 27] or the database domain [19, 24]. These studies primarily report complexity results, often highlighting $\mathsf{NP}$ -completeness for learning LTL-formulas and their fragments. In contrast, the computational complexity of learning CTL- and ATL-formulas has not yet been thoroughly examined.

In this work, we extend the study of learning temporal properties to include CTL- and ATL-formulas. Additionally, we broaden existing results for LTL to cover a more comprehensive set of operators, specifically addressing all binary operators (temporal or not).

To elaborate on our contributions, let us precisely describe the problem that we consider, the passive learning problem for temporal logic [29, 11]. Its decision version asks the following question: given two sets $\mathcal{P}$ , $\mathcal{N}$ of positive and negative examples of a system’s behavior and a size bound $B$ , does there exist a “separating” formula of size at most $B$ , which is satisfied by the positive examples and violated by the negative ones.

Our instantiation of the above problem depends on the considered logic, following related literature [29, 34, 9]: LTL-formulas express linear-time properties, CTL-formulas express branching-time properties, and ATL-formulas express properties on multi-agent systems. Accordingly, the input examples for learning LTL, CTL and ATL are linear structures (or equivalently infinite words), Kripke structures and concurrent game structures, respectively. We refer to Section 2 for formal definitions and other prerequisites.

We summarize our contributions in Table 1.

Our first result, illustrated in the left column, shows that allowing formulas with unrestricted use of at least one binary operator makes the corresponding learning decision problem $\mathsf{NP}$ -complete for all considered logics. Some of these $\mathsf{NP}$ -hardness results are (closely) inspired by [27], involving reductions from the hitting set problem – one of Karp’s 21 $\mathsf{NP}$ -complete problem; some others require novel proof techniques, e.g. one involves a reduction from an $\mathsf{NP}$ -complete modulo-2 calculus problem. We describe the outline of the proofs in Section 3.

Table 1: The complexity results for learning LTL, CTL and ATL formulas. The notation

\mathsf{ATL}^{k}

refers to

\mathsf{ATL}

-formulas with

k

agents.

\mathsf{U}^{\mathsf{t}}\subseteq\{\neg,\operatorname{\mathbf{X}},\operatorname% {\mathbf{F}},\operatorname{\mathbf{G}}\}

refers to the set of unary temporal operators.

	Unbounded	Bounded use of binary operators
	use of binary	$\operatorname{\mathbf{X}}\in\mathsf{U}^{\mathsf{t}}$	$\operatorname{\mathbf{X}}\notin\mathsf{U}^{\mathsf{t}}$
	operators		$\{\operatorname{\mathbf{F}},\operatorname{\mathbf{G}}\}\subseteq\mathsf{U}^{% \mathsf{t}}$	$\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{F}}\},\{\operatorname{\mathbf{% G}}\}$
$\mathsf{LTL}$	$\mathsf{NP}$ -c	$\mathsf{L}$
$\mathsf{CTL}$		$\mathsf{NP}$ -c	$\mathsf{NL}$ -c
$\mathsf{ATL}^{2}$		$\mathsf{NP}$ -c		$\mathsf{P}$ -c
$\mathsf{ATL}^{k}$		$\mathsf{NP}$ -c

All of the above $\mathsf{NP}$ -hardness proofs rely on separating formulas with linearly many (in the size of the input) occurrences of binary operators. Thus, in the search of expressive temporal logic fragments with lower complexities, we focus on formulas with a bounded occurrences of binary logical operators such as $\land$ (and), $\lor$ (or), etc. and no binary temporal operators such as $\operatorname{\mathbf{U}}$ (until), $\operatorname{\mathbf{R}}$ (release), etc. This choice of formulas is motivated by the fact that such formulas can still express interesting properties (e.g., GR(1) [32] formulas, mode-target formulas [4], etc.) and are used in several practical applications (see Section 4.1 for details). We explore several fragments with different unary temporal operators, $\operatorname{\mathbf{X}}$ (next), $\operatorname{\mathbf{F}}$ (eventually) and $\operatorname{\mathbf{G}}$ (globally), and present the results in the rightmost column of Table 1. We notice that, in this case, the complexity of the learning problems varies considerably between different logics and unary operators. Importantly, we exhibit fragments where the learning problem is below $\mathsf{NP}$ . We prove the three $\mathsf{NP}$ -hardness results using a reduction from the hitting set problem; we give key insights on all of these results in Section 4.

All details can be found in the extended version [8].

Related Works.

The most closely related works are [18] and [27], which operate within a similar framework to ours. Both works consider learning problems in several fragments of LTL, especially involving boolean operators such as $\lor$ and $\land$ , and temporal operators such as $\operatorname{\mathbf{X}}$ , $\operatorname{\mathbf{F}}$ and $\operatorname{\mathbf{G}}$ and prove their $\mathsf{NP}$ -completeness. We extend part of their work by categorizing fragments based on the arity of the operators and studying which type of operators contribute to the hardness. Moreover, there are several differences in the parameters considered for the learning problem. The most important one is the following: the above works consider the size upper bound $B$ to be in binary, while we assume $B$ given in unary. Although, in complexity problems, integers are most often assumed to be written in binary, we believe that considering size bound in unary is justified since one may want to not only decide the existence of a formula but also effectively output one, which will require to explicitly write it. The other differences with the setting of the above works are mostly due to the fact that we do not only consider $\mathsf{LTL}$ learning, but $\mathsf{CTL}$ and $\mathsf{ATL}$ learning as well. A thorough discussion of these differences can be found in the extended version of this paper [8].

In the past, complexity analysis of passive learning has been studied for formalisms other than temporal logics. For instance, [21] and [2] proved $\mathsf{NP}$ -completeness of the passive learning problems of deterministic finite automata (DFAs) and regular expressions (REs).

When it comes to temporal logics, most related works focus on developing efficient algorithms for learning temporal logic formulas. Among these, the emphasis has predominantly been on learning LTL (or its significant fragments), which has been discussed in detail in a recent survey summarizing various learning techniques [30]. Broadly, the techniques can be categorized into three main types: constraint solving [29, 11, 37, 20, 22], enumerative search [35, 41], and neuro-symbolic techniques [26, 42].

For learning CTL, some approaches rely on handcrafted templates [14, 43] for simple enumerative search, while others employ constraint-solving methods to learn formulas with arbitrary structures [34]. The constraint-solving methods are extended to learn ATL-formulas as well [9]. There are also works on learning other logics such as Signal Temporal Logic [7, 28], Metric Temporal Logic [36], Past LTL [3], Property Specification Language [38], etc.

2 Preliminaries and Definitions

We let $\mathbb{N}$ denote the set of all integers and $\mathbb{N}_{1}$ denote the set of all positive integers. For all $i\leq j\in\mathbb{N}$ , we let $[i,\ldots,j]\subseteq\mathbb{N}$ denote the set of integers $\{i,i+1,\ldots,j\}$ .

Given any non-empty set $Q$ , we let $Q^{*},Q^{+}$ and $Q^{\omega}$ denote the sets of finite, non-empty finite and infinite sequences of elements in $Q$ , respectively. For all $\rho\in Q^{+}$ , we denote by $|\rho|\in\mathbb{N}$ the number of elements of $\rho$ . For all $\bullet\in\{+,\omega\}$ , $\rho\in Q^{\bullet}$ and $i\in\mathbb{N}_{1}$ , if $\rho$ has at least $i$ elements, we let: $\rho[i]\in Q$ denote the $i$ -th element in $\rho$ , in particular $\rho[1]\in Q$ is the first element of $\rho$ ; $\rho[:i]\in Q^{+}$ denotes the non-empty finite sequence $\rho_{1}\cdots\rho_{i}\in Q^{+}$ ; $\rho[i:]\in Q^{\bullet}$ denotes the non-empty sequence $\rho_{i}\cdot\rho_{i+1}\cdots\in Q^{\bullet}$ , in particular we have $\rho[1:]=\rho$ .

For the remainder of this section, we fix a non-empty set of propositions $\mathsf{Prop}$ .

2.1 Structures

Usually, ATL-formulas are interpreted on concurrent game structures, i..e. games where, at each state, the concurrent actions of several agents have an impact on the next state reached. A special kind of concurrent game structures are turn-based game structures, where each state belongs to a specific agent who decides what the next state is. Here, we introduce only this special kind of games mainly due to a lack of space, but also because all of our hardness results, presented in Table 1, hold even when only considering turn-based game structures.

Definition 1.

A turn-based game structure (TGS for short) $T=\langle Q,I,\mathsf{Succ},\mathsf{Ag},\alpha,\mathsf{Prop},\pi\rangle$ is a tuple where: $Q$ is a finite set of states; $I\subseteq Q$ is the set of initial states; $\mathsf{Succ}:Q\rightarrow 2^{Q}\setminus\emptyset$ maps each state to its set of successors; $\mathsf{Ag}\subseteq\mathbb{N}$ denotes the set of agents; $\alpha:Q\rightarrow\mathsf{Ag}$ maps each state to the agent owning it; and $\pi:Q\mapsto 2^{\mathsf{Prop}}$ maps each state $q\in Q$ to the set of propositions that hold in $q$ . A state $q$ is said to be self-looping if $q\in\mathsf{Succ}(q)$ . A structure is self-looping if all of its states are self-looping.

For all coalitions of agents $A\subseteq\mathsf{Ag}$ , a strategy $\mathsf{s}_{A}$ for the coalition $A$ is a function $\mathsf{s}_{A}:Q^{+}\rightarrow Q$ such that, for all $\rho=\rho_{1}\cdots\rho_{n}\in Q^{+}$ , if $\alpha(\rho_{n})\in A$ , then $s_{A}(\rho)\in\mathsf{Succ}(\rho_{n})$ . We denote by $\mathsf{S}_{A}$ the set of strategies for the coalition $A$ . Then, from any state $q\in Q$ , we define the set $\mathsf{Out}(q,\mathsf{s}_{A})$ of infinite paths compatible with the strategy $s_{A}$ from $q$ : $\mathsf{Out}(q,\mathsf{s}_{A}):=\{\rho\in q\cdot Q^{\omega}\mid\forall i\in% \mathbb{N}_{1}:\alpha(\rho[i])\in A\implies\rho[i+1]=\mathsf{s}_{A}(\rho[:i])\}$ .

Finally, the size $|T|$ of the turn-based structure $T$ is equal to: $|T|=|Q|+|\mathsf{Ag}|+|\mathsf{Prop}|$ .

Unless otherwise stated, a turn-based structure $T$ will always refer to the tuple $T=\langle Q,I,\mathsf{Succ},A,\alpha,\mathsf{Prop},\pi\rangle$ .

There are also special kinds of turn-based structures of interest for us, introduced below.

Definition 2.

A Kripke structure is a turn-based structure with only one agent. A linear structure is a Kripke structure such that: $|I|=1$ , and for all $q\in Q$ , we have $|\mathsf{Succ}(q)|=1$ . Finally, a turn-based structure is size-1 if $|Q|=1$ .

Unless otherwise stated, a Kripke structure $K$ will always refer to a tuple $\langle Q,I,\mathsf{Succ},\mathsf{Prop},\pi\rangle$ ¹¹1In Kripke structures, there is only one agent, thus $\mathsf{Ag}$ and $\alpha$ are irrelevant..

We have introduced the notion of linear structures as we are going to interpret LTL-formulas on them. In the literature, they are usually interpreted on ultimately periodic words. However, both models are equivalent and can be encoded into each other straightforwardly.

2.2 ATL, CTL and LTL formulas

The $\mathsf{LTL}$ , $\mathsf{CTL}$ and $\mathsf{ATL}$ -formulas that we consider throughout this paper use the following temporal operators: $\operatorname{\mathbf{X}}$ (neXt), $\operatorname{\mathbf{F}}$ (Future), $\operatorname{\mathbf{G}}$ (Globally), $\operatorname{\mathbf{U}}$ (Until), $\operatorname{\mathbf{R}}$ (Release), $\operatorname{\mathbf{W}}$ (Weak until), $\operatorname{\mathbf{M}}$ (Mighty release). We group these operators into the sets of unary and binary operators: $\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}:=\{\neg,\operatorname{\mathbf{X}},% \operatorname{\mathbf{F}},\operatorname{\mathbf{G}}\}$ and $\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{tp}}:=\{\operatorname{\mathbf{U}},% \operatorname{\mathbf{R}},\operatorname{\mathbf{W}},\operatorname{\mathbf{M}}\}$ . We also let $\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ be the set of all logical binary operators, i.e. classical logical operators, along with their negations: $\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}:=\{\lor,\wedge,\Rightarrow,\Leftarrow% ,\Leftrightarrow,\prescript{\neg}{}{\lor},\prescript{\neg}{}{\wedge},% \prescript{\neg}{}{\Rightarrow},\prescript{\neg}{}{\Leftarrow},\prescript{\neg% }{}{\Leftrightarrow}\}$ (we have $|\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}|=10$ ).

To define ATL-formulas, we consider two types of formulas: state formulas – where strategic operators occur, denoted with the Greek letter $\phi$ – and path formulas – where temporal operators occur, denoted with the Greek letter $\psi$ . Consider some $\mathsf{U}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$ , $\mathsf{B}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{tp}}$ , and $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ . For all $k\in\mathbb{N}_{1}$ , we denote by $\mathsf{ATL}^{k}(\mathsf{Prop},\mathsf{U}^{\mathsf{t}},\mathsf{B}^{\mathsf{t}}% ,\mathsf{B}^{\mathsf{l}})$ the set of $\mathsf{ATL}^{k}$ -state formulas defined by the grammar:

$\phi\Coloneqq p\mid\neg\phi\mid\phi*\phi\mid\langle\!\langle A\rangle\!\rangle\psi$

$\psi\Coloneqq*_{1}\phi\mid\phi*_{2}\phi$

where $\phi$ is a state-formula, $\psi$ is a path formula, $p\in\mathsf{Prop}$ , $*\in\mathsf{B}^{\mathsf{l}}$ , $A\subseteq[1,\ldots,k]$ is a subset of agents, $*_{1}\in\mathsf{U}^{\mathsf{t}}\setminus\{\neg\}$ , and $*_{2}\in\mathsf{B}^{\mathsf{t}}$ . We denote by $\mathsf{ATL}^{k}$ the set of all $\mathsf{ATL}^{k}$ -state formulas $\phi$ . Note that $\mathsf{CTL}$ -formulas are $\mathsf{ATL}^{1}(\mathsf{Prop},\mathsf{U}^{\mathsf{t}},\mathsf{B}^{\mathsf{t}}% ,\mathsf{B}^{\mathsf{l}})$ -formulas. Hence, there are only two possible strategic operator: $\langle\!\langle\emptyset\rangle\!\rangle$ , usually denoted $\forall$ , and $\langle\!\langle\{1\}\rangle\!\rangle$ usually denoted $\exists$ . We define $\mathsf{LTL}$ -formulas as $\mathsf{ATL}^{1}$ -formulas using only the quantifier $\exists$ . Since $\mathsf{LTL}$ -formulas are interpreted on linear structures, where each state has exactly one successor, the strategic operators used have no impact on the satisfaction of the formula. For readability, we will depict $\mathsf{LTL}$ -formulas without the $\exists$ quantifier.

The set of sub-formulas $\mathsf{SubF}(\phi)$ of a formula $\phi$ is then defined inductively as follows: $\mathsf{SubF}(\phi):=\{\phi\}\cup S$ where $S:=\emptyset$ if $\phi=p\in\mathsf{Prop}$ , $S:=\mathsf{SubF}(\phi^{\prime})$ if $\phi\in\{\neg\phi^{\prime},\langle\!\langle A\rangle\!\rangle*_{1}\phi^{\prime}\}$ and $S:=\mathsf{SubF}(\phi_{1})\cup\mathsf{SubF}(\phi_{2})$ if $\phi\in\{\phi_{1}*\phi_{2},\langle\!\langle A\rangle\!\rangle(\phi_{1}*_{2}% \phi_{2})\}$ . The size $|\phi|$ of a formula is then defined as its number of sub-formulas: $|\phi|:=|\mathsf{SubF}(\phi)|$ . We also denote by $|\phi|_{\mathsf{bin}}$ the number of sub-formulas of $\phi$ using a binary operator, $|\phi|_{\mathsf{bin}}:=|\mathsf{SubBin}(\phi)|$ with: $\mathsf{SubBin}(\phi):=\{\phi_{1}*\phi_{2}\in\mathsf{SubF}(\phi)\mid\phi_{1},% \phi_{2}\in\mathsf{SubF}(\phi),*\in\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{tp}}% \cup\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}\}$ .

We interpret $\mathsf{ATL}$ -formulas over TGS using the standard definitions [1]. That is, given a state $q$ and a state formula $\phi$ , the fact $q$ satisfies $\phi$ , denoted $q\models\phi$ , is defined inductively:

	$\displaystyle q$	$\displaystyle\models p$	iff	$\displaystyle p\in\pi(q)$
	$\displaystyle q$	$\displaystyle\models\neg\phi$	iff	$\displaystyle q\not\models\phi$

	$\displaystyle q$	$\displaystyle\models\phi_{1}*\phi_{2}$	iff	$\displaystyle(q\models\phi_{1})*(q\models\phi_{2})=\mathsf{True}$
	$\displaystyle q$	$\displaystyle\models\langle\!\langle A\rangle\!\rangle\psi$	iff	$\displaystyle\exists\mathsf{s}_{A}\in\mathsf{S}_{A},\;\forall\pi\in\mathsf{Out% }(q,s),\;\pi\models\psi$

where $*\in\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ is a binary operator seen as a boolean function $*:\mathbb{B}\times\mathbb{B}\rightarrow\mathbb{B}$ with $\mathbb{B}:=\{\mathsf{True},\mathsf{False}\}$ . Furthermore, given a path $\pi\in Q^{\omega}$ and a path formula $\psi$ , the fact that $\psi$ holds for the path $\pi$ , also denoted $\pi\models\phi$ , is defined inductively as follows:

$\displaystyle\pi$	$\displaystyle\models\operatorname{\mathbf{X}}\phi$	iff	$\displaystyle\pi[2:]\models\phi;$
$\displaystyle\pi$	$\displaystyle\models\operatorname{\mathbf{F}}\phi$	iff	$\displaystyle\exists i\in\mathbb{N}_{1},\;\pi[i:]\models\phi;$
$\displaystyle\pi$	$\displaystyle\models\operatorname{\mathbf{G}}\phi$	iff	$\displaystyle\forall i\in\mathbb{N}_{1},\;\pi[i:]\models\phi$
$\displaystyle\pi$	$\displaystyle\models\phi_{1}\operatorname{\mathbf{W}}\phi_{2}$	iff	$\displaystyle\pi\models(\phi_{1}\operatorname{\mathbf{U}}\phi_{2})\vee% \operatorname{\mathbf{G}}\phi_{1}$

$\displaystyle\pi$	$\displaystyle\models\phi_{1}\operatorname{\mathbf{U}}\phi_{2}$	iff	$\displaystyle\exists i\in\mathbb{N}_{1},\;\pi[i:]\models\phi_{2}\text{ and }$
	$\displaystyle\forall 1\leq j\leq i-1,\;\pi[j:]\models\phi_{1}$
$\displaystyle\pi$	$\displaystyle\models\phi_{1}\operatorname{\mathbf{R}}\phi_{2}$	iff	$\displaystyle\pi\models\neg(\neg\phi_{1}\operatorname{\mathbf{U}}\neg\phi_{2})$
$\displaystyle\pi$	$\displaystyle\models\phi_{1}\operatorname{\mathbf{M}}\phi_{2}$	iff	$\displaystyle\pi\models(\phi_{1}\operatorname{\mathbf{R}}\phi_{2})\wedge% \operatorname{\mathbf{F}}\phi_{1}$

An $\mathsf{ATL}$ -formula $\phi$ accepts a TGS $T$ , denoted by $T\models\phi$ , if $q\models\phi$ for all initial states $q\in I$ , otherwise it rejects it. Given two formulas $\phi,\phi^{\prime}$ , we write $\phi\implies\phi^{\prime}$ if, for all TGS $T$ , if $T\models\phi$ , then $T\models\phi^{\prime}$ . We write $\phi\equiv\phi^{\prime}$ when $\phi\implies\phi^{\prime}$ and $\phi^{\prime}\implies\phi$ .

2.3 Learning decision problem

We define the $\mathsf{LTL}$ , $\mathsf{CTL}$ and $\mathsf{ATL}$ learning problems below, where models for $\mathsf{LTL}$ , $\mathsf{CTL}$ , and $\mathsf{ATL}$ are linear structures, Kripke structures and turn-based game structures, respectively.

Definition 3.

Let $\mathsf{TL}\in\{\mathsf{LTL},\mathsf{CTL},\mathsf{ATL}^{k}\mid k\in\mathbb{N}_% {1}\}$ and consider some sets of operators $\mathsf{U}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$ , $\mathsf{B}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{tp}}$ and $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ . For all $n\in\mathbb{N}\cup\{\infty\}$ , we denote by $\mathsf{TL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\mathsf{B}^{\mathsf{t}},% \mathsf{B}^{\mathsf{l}},n)$ the decision problem:

$\blacksquare$

Input: $(\mathsf{Prop},\mathcal{P},\mathcal{N},B)$ where $\mathsf{Prop}$ is a set of propositions, $\mathcal{P},\mathcal{N}$ are two finite sets of models for $\mathsf{TL}$ , and $B\in\mathbb{N}$ .
$\blacksquare$

Output: yes if and only if there exists a $\mathsf{TL}$ -formula $\varphi\in\mathsf{TL}(\mathsf{Prop},\mathsf{U}^{\mathsf{t}},\mathsf{B}^{% \mathsf{t}},\mathsf{B}^{\mathsf{l}})$ such that $|\varphi|\leq B$ , $|\varphi|_{\mathsf{bin}}\leq n$ , and $\varphi$ is separating, i.e. such that : for all $X\in\mathcal{P}$ (resp. $X\in\mathcal{N}$ ), we have $X\models\varphi$ (resp. $X\not\models\varphi$ ).

The size of the input is equal to $|\mathsf{Prop}|+|\mathcal{P}|+|\mathcal{N}|+B$ (i.e. $B$ is written in unary).

As the model checking problems for $\mathsf{LTL}$ , $\mathsf{CTL}$ , $\mathsf{ATL}$ are in $\mathsf{P}$ [1], it follows that the learning problems for all these logics are in $\mathsf{NP}$ , with a straightforward guess-and-check subroutine.

Proposition 4.

For all $\mathsf{U}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$ , $\mathsf{B}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{tp}}$ , $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ , $n\in\mathbb{N}\cup\{\infty\}$ , and $\mathsf{TL}\in\{\mathsf{LTL},\mathsf{CTL},\mathsf{ATL}^{k}\mid k\in\mathbb{N}_% {1}\}$ , the decision problem $\mathsf{TL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\mathsf{B}^{\mathsf{t}},% \mathsf{B}^{\mathsf{l}},n)$ is in $\mathsf{NP}$ .

2.4 Hitting set problem

We recall below the $\mathsf{NP}$ -complete problem from which we will establish almost all of our ( $\mathsf{NP}$ -hardness) reductions.

Definition 5 (Hitting set problem).

We denote by $\mathsf{Hit}$ the following decision problem:

$\blacksquare$

Input: a triple $(l,C,k)$ where $l\in\mathbb{N}_{1}$ , $C=C_{1},\ldots,C_{n}$ are non-empty subsets of $[1,\dots,l]$
$\blacksquare$

Output: yes iff there is a subset $H\subseteq[1,\ldots,l]$ of size at most $k$ such that, we have $H\cap C_{i}\neq\emptyset$ for all $1\leq i\leq n$ . In such a case, the set $H$ is called a hitting set.

In the following, if $(l,C,k)$ is an instance of the hitting set problem, then $C$ refers to $C_{1},\ldots,C_{n}$ for some $n\in\mathbb{N}_{1}$ .

3 Learning with unbounded use of binary operators

First, we consider the case of learning a formula with arbitrarily many occurrences of binary operators. The main result of this section is stated in Theorem 6 below.

Theorem 6.

Let $\mathsf{B}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{tp}}$ and $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ such that $\mathsf{B}^{\mathsf{t}}\cup\mathsf{B}^{\mathsf{l}}\neq\emptyset$ . Then, for all $\mathsf{U}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$ , the decision problem $\mathsf{LTL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\mathsf{B}^{\mathsf{t}},% \mathsf{B}^{\mathsf{l}},\infty)$ is $\mathsf{NP}$ -hard.

In the passive learning setting that we consider, the size of the formulas is crucial due to the upper bound $B$ . Therefore, although it is possible to express e.g. disjunctions with conjunctions and negations, since doing so affects the size of the formulas involved, if we have proved that a learning problem is $\mathsf{NP}$ -hard with the operators $\lor,\neg$ , it does not imply a priori that it is also $\mathsf{NP}$ -hard with the operator $\wedge$ . Hence, for the sake of completeness, we consider all those fourteen binary operators (ten logical, four temporal), although it seems that some of these binary operators (like $\lor$ or $\wedge$ ) make much more sense to consider than others (like $\Leftrightarrow$ or $\prescript{\neg}{}{\Leftrightarrow}$ ). Since these operators behave differently, we cannot do a single reduction working for all these operators at once. However, we do partition these operators in different groups and exhibit a reduction per group of operators.

Most of the reductions use only size-1 structures, that are (almost) entirely defined by the subset of propositions labeling their only state. In addition, most of the reductions are done from the hitting set problem. In that case, how we extract a hitting set from a (small enough) separating formula relies only on the variables that need to occur in a formula separating the positive and negative structures, regardless of the operators involved.

We start with the operators $\lor,\Rightarrow,\Leftarrow$ , i.e. we assume that $\mathsf{B}^{\mathsf{l}}\cap\{\lor,\Rightarrow,\Leftarrow\}\neq\emptyset$ . The reduction for this case is actually a straightforward adaptation of the proof of [27, Theorem 2]. We describe it here. Given an instance $(l,C,k)$ of the hitting set problem, we let $\mathsf{Prop}:=\{a_{j},b_{j}\mid 1\leq j\leq l\}$ . Furthermore, for all subsets $T\subseteq[1,\ldots,l]$ , we let $\mathcal{L}(T)$ denote a size-1 (linear) structure whose only state is labeled by the set $\{a_{j},b_{j^{\prime}}\mid j\in T,j^{\prime}\notin T\}$ . Then, we let $\mathsf{In}^{\lor,\Rightarrow,\Leftarrow}:=(\mathsf{Prop},\mathcal{P},\mathcal% {N},B)$ for $\mathcal{P}:=\{\mathcal{L}(C_{i})\mid 1\leq i\leq n\}$ , $\mathcal{N}:=\{\mathcal{L}(\emptyset)\}$ , and $B:=2k-1$ . Let us illustrate this reduction on a simple example. Assume that $l=4$ , $C=(\{1,2,3\},\{2,4\},\{1,4\})$ , and $k=2$ . Then, the sets labeling the only state of the positive structures are $\{a_{1},a_{2},a_{3},b_{4}\}$ , $\{b_{1},a_{2},b_{3},a_{4}\}$ , and $\{a_{1},b_{2},b_{3},a_{4}\}$ while the set labeling the only state of the negative structure is $\{b_{1},b_{2},b_{3},b_{4}\}$ . Furthermore, $B=3$ . Then, $H:=\{1,4\}$ is the a hitting set with $|H|\leq 2$ , while $\varphi_{\lor}:=a_{1}\lor a_{4}$ , $\varphi_{\Rightarrow}:=b_{1}\Rightarrow a_{4}$ , and $\varphi_{\Leftarrow}:=a_{1}\Leftarrow b_{4}$ are all separating formulas with $|\varphi_{\lor}|=|\varphi_{\Rightarrow}|=|\varphi_{\Leftarrow}|\leq 3$ .

We claim that $(l,C,k)$ is a positive instance of $\mathsf{Hit}$ iff $\mathsf{In}^{\lor,\Rightarrow,\Leftarrow}$ is a positive instance of $\mathsf{LTL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\mathsf{B}^{\mathsf{t}},% \mathsf{B}^{\mathsf{l}},\infty)$ . Indeed, given a hitting set $H=\{i_{1},\ldots,i_{r}\}$ with $r\leq k$ , one can check that the $\mathsf{LTL}$ -formula $\varphi_{\lor}:=\lor_{1\leq x\leq r}\;a_{i_{x}}$ of size $2r-1\leq B$ accepts $\mathcal{P}$ and rejects $\mathcal{N}$ . Note that, the $\mathsf{LTL}$ -formulas $\varphi_{\Rightarrow}:=b_{j_{1}}\Rightarrow(b_{j_{2}}\Rightarrow(\ldots% \Rightarrow a_{j_{r}}))$ and $\varphi_{\Leftarrow}:=((a_{j_{1}}\Leftarrow b_{j_{2}})\Leftarrow\ldots)% \Leftarrow b_{j_{r}}$ of size $2r+1\leq B$ also accept $\mathcal{P}$ and reject $\mathcal{N}$ . On the other hand, consider an $\mathsf{LTL}$ -formula $\varphi$ of size at most $B$ that accepts $\mathcal{P}$ and rejects $\mathcal{N}$ . We let $H:=\{1\leq j\leq l\mid a_{j}\text{ or }b_{j}\text{ occurs in }\varphi\}$ . Since $|\varphi|\leq B$ , we have $|H|\leq k$ . Furthermore, consider any $1\leq i\leq n$ . Let us consider the set $S_{i}$ (resp. $S$ ) labeling the only state of the structure $\mathcal{L}(C_{i})$ (resp. $\mathcal{L}(\emptyset)$ ). We have $\Delta(S_{i},S):=S_{i}\setminus S\cup S\setminus S_{i}=\{a_{j},b_{j}\mid j\in C% _{i}\}$ . One can then show (rather straightforwardly, by induction on $\mathsf{LTL}$ -formulas) that, since $\varphi$ accepts $\mathcal{L}(C_{i})$ and rejects $\mathcal{L}(\emptyset)$ , at least one variable in $\Delta(S_{i},S)$ occurs in $\varphi$ . That is, $C_{i}\cap H\neq\emptyset$ and $H$ is a hitting set of size at most $k$ .

In fact, the reduction for the operators $\wedge,\prescript{\neg}{}{\Rightarrow},\prescript{\neg}{}{\Leftarrow}$ is obtained from the above one by reversing the positive and negative sets (the arguments are almost identical).

We then handle the operators $\prescript{\neg}{}{\lor},\prescript{\neg}{}{\wedge}$ . The above reductions cannot be used since, when the operator $\prescript{\neg}{}{\wedge}$ (or the operator $\prescript{\neg}{}{\lor}$ ) is used successively, the formula obtained is semantically equivalent to an alternation of conjunctions and disjunctions. For instance, consider six variables $r_{1},r_{2},r_{3},r_{4},x_{1},x_{2}$ to use in a single $\mathsf{LTL}$ -formula using only the $\prescript{\neg}{}{\wedge}$ operator, e.g.: $\varphi:=r_{1}\prescript{\neg}{}{\wedge}\;(x_{1}\prescript{\neg}{}{\wedge}\;(r% _{2}\prescript{\neg}{}{\wedge}\;(x_{2}\prescript{\neg}{}{\wedge}\;(r_{3}% \prescript{\neg}{}{\wedge}\;r_{4}))))$ . It is semantically equivalent to: $\varphi\equiv\neg r_{1}\lor(x_{1}\wedge(\neg r_{2}\lor(x_{2}\wedge(\neg r_{3}% \lor\neg r_{4})))$ . This is in sharp contrast with the above-formulas $\varphi_{\lor},\varphi_{\Leftarrow}$ and $\varphi_{\Rightarrow}$ . To circumvent this difficulty, we change the reduction by adding propositions labeling the only state of all the positive size-1 linear structures (but not the only state of all the negative ones). We can then place these propositions where $x_{2}$ and $x_{4}$ were in the above formula. That way, we semantically obtain a disjunction on relevant variables $r_{1},r_{2},r_{3},r_{4}$ . The obtained reduction is slightly more subtle than the previous ones.

Before considering the last two logical operators $\Leftrightarrow,\prescript{\neg}{}{\Leftrightarrow}$ , we handle the temporal operators $\operatorname{\mathbf{W}},\operatorname{\mathbf{M}}$ . The two previous reductions only use size-1 structures. On such structures, the temporal operators $\operatorname{\mathbf{W}},\operatorname{\mathbf{M}}$ are actually equivalent to $\lor$ and $\wedge$ respectively. Hence, the reductions for $\lor$ and $\wedge$ can also be used as is for the operators $\operatorname{\mathbf{W}}$ and $\operatorname{\mathbf{M}}$ respectively.

We then handle the final two logical operators $\Leftrightarrow,\prescript{\neg}{}{\Leftrightarrow}$ . These operators are unlike the other operators. Let us give an intuition of how the learning problems with these operators behave. Consider an $\mathsf{LTL}$ -formula $\varphi$ using only the operators $\neg,\Rightarrow$ and $\prescript{\neg}{}{\Leftrightarrow}$ and a size-1 structure $\mathcal{L}$ . Let $S$ denote the set of propositions labeling the only state of $\mathcal{L}$ . We let $\mathsf{Neg}(\varphi)$ denote the number of occurrences of the operators $\neg,\prescript{\neg}{}{\Leftrightarrow}$ in $\varphi$ . We also let $\mathsf{NbOc}_{\bar{S}}(\varphi)$ denote the number of occurrences of the propositions not in $S$ in $\varphi$ . Then, one can realize that $\mathcal{L}\models\varphi$ if and only if $\mathsf{Neg}(\varphi)$ and $\mathsf{NbOc}_{\bar{S}}(\varphi)$ have the same parity. This simple observation suggests that the learning problem with the operators $\Leftrightarrow,\prescript{\neg}{}{\Leftrightarrow}$ is linked to modulo-2 calculus. The reduction for these operators is established from an $\mathsf{NP}$ -complete problem dealing with modulo-2 calculus, known as the Coset Weight problem [5].

Finally, we handle the temporal operators $\operatorname{\mathbf{U}}$ and $\operatorname{\mathbf{R}}$ . On size-1 structures, for all $\mathsf{LTL}$ -formulas $\varphi_{1},\varphi_{2}$ , we have the following equivalences: $\varphi_{1}\operatorname{\mathbf{U}}\varphi_{2}\equiv\varphi_{1}\operatorname{% \mathbf{R}}\varphi_{2}\equiv\varphi_{2}$ . That is, contrary to the temporal operators $\operatorname{\mathbf{W}}$ and $\operatorname{\mathbf{M}}$ , on size-1 structures, $\operatorname{\mathbf{U}}$ and $\operatorname{\mathbf{R}}$ are equivalent to unary operators. Hence, the reduction that we consider does not involve only size-1 structures. It is once again established from the hitting set problem, though the construction and the correctness proof are more involved than for the above cases.

On top of that, for all sets of operators, ATL learning is at least as hard as CTL learning, which is itself at least as hard as LTL learning. Thus, from Theorem 6, we obtain that CTL and ATL learning with unbounded use of binary operators are $\mathsf{NP}$ -hard. This justifies the leftmost column of Table 1.

4 Learning with a bounded amount of binary operators

Since, with unbounded use of binary operators, all the learning problems are $\mathsf{NP}$ -hard, we focus on learning formulas where the number of occurrences of binary operators is bounded. Note that the bound $n$ parameterizes the decision problem itself, and therefore is independent of the input. For simplicity, we restrict ourselves to formulas that do not use at all binary temporal operators. Before we dive into the details of our results as summarized in the rightmost column of Table 1, let us first argue why this fragment is interesting to focus on.

4.1 Expressivity

The passive learning problem that we consider in this paper bounds the size of the formulas considered. This is because we want a separating formula not to overfit the input (i.e. not to simply describe the positive and negative models). However, another benefit is that the smaller the formulas, the more understandable they are for users. Similarly, using too many binary operators could make the formulas hard to grasp, regardless of their size.

In addition, there are examples of interesting specifications that can be expressed with a bounded amount of binary operators. We give three examples below with $\mathsf{LTL}$ -formulas.

Consider first so-called “mode-target” formulas of the shape $\bigwedge_{j}\left(\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}M_{j}% \Rightarrow\bigvee_{i}\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}T_{i,j% }\right)$ , where all $M_{j},T_{i,j}$ are propositions. These types of formulas were introduced in [4] and exhibit two interesting features: the corresponding $\mathsf{LTL}$ -synthesis problem is tractable, and these formulas express an interesting property, which can be summarized as follows: if a model eventually settles in a mode $M_{j}$ , then it should eventually settle in one of the target $T_{i,j}$ . Interestingly, when the number of different modes and targets that a system can have is fixed, then the number of binary operators sufficient to express such specification is also bounded.

Similarly, there are also interesting specifications related to “generalized reactivity” (from [32] for $\mathsf{LTL}$ -formulas). Such specifications are of the shape $\bigwedge_{i}\operatorname{\mathbf{G}}\operatorname{\mathbf{F}}\psi_{i}% \Rightarrow\bigwedge_{i}\operatorname{\mathbf{G}}\operatorname{\mathbf{F}}\psi% _{i}^{\prime}$ , where all formulas $\psi_{i}$ and $\psi_{i}^{\prime}$ do not feature at all temporal operators. As such, up to introducing additional propositions, these could be expressible with few binary operators. These formulas can be read as an implication between assumptions and guarantees. As above, when the number of assumptions and guarantees is bounded, then the number of binary operators sufficient to express such formulas also is.

Finally, one of the popular LTL learning tools, Scarlet [35], relies on a fragment of LTL, directed LTL and its dual, which uses unary temporal operators and binary logical operators only. In these fragments, formulas of a fixed length (a search parameter they define) can use several of $\operatorname{\mathbf{F}}$ $\operatorname{\mathbf{G}}$ and $\operatorname{\mathbf{X}}$ operators while using only bounded occurrences of $\land$ and $\lor$ operators.

4.2 Abstract recipes

The six decision problems captured in the rightmost column of Table 1 are of two kinds: three are $\mathsf{NP}$ -complete, while three others are below $\mathsf{NP}$ . In fact, the proofs of all three results of the same kind will follow the same abstract recipes. We present them below.

Recipe for the membership-below-NP proofs.

Let $\mathsf{TL}$ denote either $\mathsf{LTL}$ formulas, or $\mathsf{CTL}$ formulas without the operator $\operatorname{\mathbf{X}}$ , or $\mathsf{ATL}^{2}$ formulas with only one unary operator $\operatorname{\mathbf{F}}$ or $\operatorname{\mathbf{G}}$ (i.e. one of the three logical fragment for which the corresponding decision problem is below $\mathsf{NP}$ ). Then, we follow the two steps below:

A)

First, we show that given the set of propositions $\mathsf{Prop}$ and the bound $B$ , there is a set of relevant $\mathsf{TL}$ -formulas $\mathsf{RelForm}(\mathsf{Prop},B)$ such that: 1) For all $\mathsf{TL}(\mathsf{Prop})$ -formulas $\phi$ of size at most $B$ , there is a formula $\phi^{\prime}\in\mathsf{RelForm}(\mathsf{Prop},B)$ such that $\phi\equiv\phi^{\prime}$ ; and 2) the size of $\mathsf{RelForm}(\mathsf{Prop},B)$ is polynomial in $|\mathsf{Prop}|$ and $B$ .
B)

Second, we show that for all $\mathsf{TL}$ -formulas $\phi\in\mathsf{RelForm}(\mathsf{Prop},B)$ , deciding if $\phi$ satisfies a $\mathsf{TL}$ -model $M$ can be done, depending on $|\mathsf{Prop}|,B,|M|$ , within the resources allowed, i.e. logarithmic space for the $\mathsf{LTL}$ case, non-deterministic logarithmic space for the $\mathsf{CTL}$ case, and polynomial time for the $\mathsf{ATL}^{2}$ case.

Due to a lack of space, in this paper we will only present these two steps in the context of formulas that do not use any binary operator. Since the occurrences of binary operators is bounded in any case, the arguments are essentially the same for the general case. For instance, for the first step, from the result established for formulas without binary operators, we can straightforwardly deduce the result for all formulas, by induction on the bound $n$ . That way, we obtain that $|\mathsf{RelForm}(\mathsf{Prop},B)|$ could be exponential in the bound $n$ , but this does not have an impact complexity-wise, since $n$ is fixed.

Recipe for the NP-hardness proofs.

The formulas that we consider only use a bounded amount of binary operators. Thus, contrary to the $\mathsf{NP}$ -hardness reductions of Section 3, here, our $\mathsf{NP}$ -hardness proofs do not rely on binary operators. In fact, these binary operators make it harder to argue about how the permitted unary operators interact. For this reason, our proof of $\mathsf{NP}$ -hardness is decomposed into two steps. We first exhibit reductions for the learning problems without binary operators. Then, from these reductions, we devise reductions for the learning problems with bounded occurrences of binary operators. We present in details the former reductions in this paper and give intuition behind the later reductions below.

Let $n\in\mathbb{N}$ and $*\in\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ be a binary (non-temporal) operator. We consider $n$ propositions $\{p_{1},\ldots,p_{n}\}$ and we define multiple size-1 structures using the propositions $\{p_{1},\ldots,p_{n}\}$ forming two sets $\mathcal{A}_{n,*}$ and $\mathcal{B}_{n,*}$ . The idea is that to distinguish these two sets, a separating formula will necessarily feature all the propositions $\{p_{1},\ldots,p_{n}\}$ . In fact, from a positive and a negative sets of structures $\mathcal{P}$ and $\mathcal{N}$ on the set of proposition $\{p\}$ ²²2In fact, for technical reason, in [8], we use two propositions $\{p,\bar{p}\}$ . (which is the only proposition that unary formulas can use in our reductions), we can show the following: if a formula of size at most $B+2n$ , with at most $n$ occurrences of binary operators, separates both $\mathcal{P}$ and $\mathcal{N}$ , and $\mathcal{A}_{n,*}$ and $\mathcal{B}_{n,*}$ , then there is a unary formula of size at most $B$ that separates $\mathcal{P}$ and $\mathcal{N}$ .³³3Actually, we can also show the converse (which is important for us to prove that the reduction is correct). That way, a reduction for the learning problem without binary operators can be translated (in logspace) into a reduction for the learning with bounded occurrences of binary operators. Note that the arguments presented in this paragraph are not straightforward to formally state and prove (this is handled in Theorem “Proving $\mathsf{NP}$ -hardness without binary operators is sufficient” in the extended version [8]).

Let us now consider how we handle the reduction without binary operators. From an instance $(l,C,k)$ of the hitting problem, we proceed as follows. We define a sample of structures (and a bound $B$ ) such that all separating formulas have a specific shape, and there is a bijection between subsets $H\subseteq[1,\ldots,l]$ and formulas $\varphi(l,H)$ of that specific shape. This correspondence allows us to extract a hitting set. More specifically, we follow the abstract recipe below:

(a)

We define the bound $B$ and positive and negative structures that “eliminate” certain operators or pattern of operators from any potential separating formula. This way we ensure that any separating formula will be of the form $\varphi(l,H)$ , for some $H\subseteq[1,\ldots,l]$ .
(b)

We define a negative structure satisfied by a formula $\varphi(l,H)$ if and only if $|H|\geq k+1$ .
(c)

For all $1\leq i\leq n$ , we define a positive structure that a formula $\varphi(l,H)$ accepts if and only if $H\cap C_{i}\neq\emptyset$ .

By construction, the instance of the learning decision problem that we obtain is a positive instance if and only if the hitting set instance $(l,C,k)$ also is. Furthermore, note that in all three cases, this reduction can be computed in logspace.

4.3 LTL learning

We start with LTL learning. We have the proposition below.

Proposition 7.

For all sets of unary operators $\mathsf{U}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$ , sets of binary (non-temporal) operators $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ , and $n\in\mathbb{N}$ , the decision problem $\mathsf{LTL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},n)$ is in $\mathsf{L}$ .

We present Steps A and B of Section 4.2 in the case $n=0$ . Toward Step A, we have the equivalences below (see e.g. [27, Prop. 8]), which imply the corollary that follows.

Observation 8.

For all $\mathsf{LTL}$ -formulas $\varphi$ and $k\in\mathbb{N}$ , we have: 1) $\operatorname{\mathbf{F}}\operatorname{\mathbf{X}}^{k}\varphi\equiv% \operatorname{\mathbf{X}}^{k}\operatorname{\mathbf{F}}\varphi$ , $\operatorname{\mathbf{G}}\operatorname{\mathbf{X}}^{k}\varphi\equiv% \operatorname{\mathbf{X}}^{k}\operatorname{\mathbf{G}}\varphi$ ; 2) $\operatorname{\mathbf{F}}\operatorname{\mathbf{F}}\varphi\equiv\operatorname{% \mathbf{F}}\varphi$ , $\operatorname{\mathbf{G}}\operatorname{\mathbf{G}}\varphi\equiv\operatorname{% \mathbf{G}}\varphi$ ; 3) $\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}\operatorname{\mathbf{F}}% \varphi\equiv\operatorname{\mathbf{G}}\operatorname{\mathbf{F}}\varphi$ , $\operatorname{\mathbf{G}}\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}% \varphi\equiv\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}\varphi$ .

Corollary 9.

Consider a set of propositions $\mathsf{Prop}$ . We let $\mathsf{Lit}(\mathsf{Prop}):=\{x,\neg x\mid x\in\mathsf{Prop}\}$ and $\mathsf{LTL}_{\mathsf{Un}}(\mathsf{Prop}):=\{\operatorname{\mathbf{X}}^{k}x,% \operatorname{\mathbf{X}}^{k}\operatorname{\mathbf{F}}x,\operatorname{\mathbf{% X}}^{k}\operatorname{\mathbf{G}}x,\operatorname{\mathbf{X}}^{k}\operatorname{% \mathbf{F}}\operatorname{\mathbf{G}}x,\operatorname{\mathbf{X}}^{k}% \operatorname{\mathbf{G}}\operatorname{\mathbf{F}}x\mid k\in\mathbb{N},\;x\in% \mathsf{Lit}(\mathsf{Prop})\}$ .

Then, for any $\mathsf{LTL}$ -formula $\varphi\in\mathsf{LTL}(\mathsf{Prop},\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}},% \emptyset,\mathsf{B}^{\mathsf{l}},0)$ , there is an $\mathsf{LTL}$ -formula $\varphi^{\prime}\in\mathsf{LTL}_{\mathsf{Un}}(\mathsf{Prop})\cap\mathsf{LTL}(% \mathsf{Prop},\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ such that $\varphi\equiv\varphi^{\prime}$ and $|\varphi^{\prime}|\leq|\varphi|$ .

Proof sketch.

With the equivalences 1) from Observation 8, we can push the $\operatorname{\mathbf{X}}$ operators in $\varphi$ at the beginning of the formula. The equivalences 2) and 3) from Observation 8 ensure that it is possible to have at most two nested $\operatorname{\mathbf{F}},\operatorname{\mathbf{G}}$ operators in the resulting formula $\varphi^{\prime}$ . $\hfill\blacktriangleleft$

The set of relevant formulas $\mathsf{RelForm}(\mathsf{Prop},B)$ is then obtained directly from the set of formulas $\mathsf{LTL}_{\mathsf{Un}}(\mathsf{Prop})$ . Note that however, how it is obtained depends on the exact operators in $\mathsf{U}^{\mathsf{t}}$ . For instance, if $\operatorname{\mathbf{G}}\notin\mathsf{U}^{\mathsf{t}}$ while $\neg,\operatorname{\mathbf{F}}\in\mathsf{U}^{\mathsf{t}}$ , we should replace the occurrences of $\operatorname{\mathbf{G}}$ in formulas in $\mathsf{RelForm}(\mathsf{Prop},B)$ by $\neg\operatorname{\mathbf{F}}\neg$ . Nonetheless, in any case, we obtain a set $\mathsf{RelForm}(\mathsf{Prop},B)$ of relevant formulas whose number of elements is linear in $|\mathsf{Prop}|\cdot B$ . This concludes the arguments for Step A. As for Step B, one can realize that since there are at most two nested $\operatorname{\mathbf{F}},\operatorname{\mathbf{G}}$ operators in formulas in $\mathsf{RelForm}(\mathsf{Prop},B)$ , then checking that they hold on a linear structure can be done in logarithmic space (because it suffices to have a constant number of pointers browsing the structure).

4.4 CTL learning

Consider now the more involved case of CTL learning. As can be seen in Table 1, we distinguish two cases: with and without the operator $\operatorname{\mathbf{X}}$ .

Assume that $\operatorname{\mathbf{X}}\in\mathsf{U}^{\mathsf{t}}$ .

The goal is to show the theorem below.

Theorem 10.

For all sets $\mathsf{U}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$ , $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ , and bound $n\in\mathbb{N}$ , if $\operatorname{\mathbf{X}}\in\mathsf{U}^{\mathsf{t}}$ , then the decision problem $\mathsf{CTL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},n)$ is $\mathsf{NP}$ -hard.

As stated in Section 4.2, we argue the theorem in the case $n=0$ . Recall that in that case we consider a single proposition $\{p\}$ . Consider an instance $(l,C,k)$ of the hitting set problem $\mathsf{Hit}$ . We follow the three Steps a, b, and c. Toward Step a, we define Kripke structures that prevent the use of the operators $\operatorname{\mathbf{F}},\operatorname{\mathbf{G}},\neg$ . To do so, we let $B:=l+1$ and for two sets $S_{1},S_{2}\subseteq\{p\}$ , we consider the Kripke structure $K_{l,S_{1},S_{2}}$ that is depicted in Figure 1. These structures satisfy the lemma below.

Figure 1: The structure

K_{l,S_{1},S_{2}}

where

S_{1}\subseteq\{p\}

(resp.

S_{2}\subseteq\{p\}

) labels

q_{l+1}

(resp.

q_{l+2}

).

Lemma 11.

A formula $\phi\in\mathsf{CTL}(\{p\},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ of size at most $l+1$ accepting $K_{l,\{p\},\emptyset}$ and rejecting $K_{l,\emptyset,\{p\}}$ and $K_{l,\emptyset,\emptyset}$ cannot use the operators $\operatorname{\mathbf{F}},\operatorname{\mathbf{G}},\neg$ .

Proof sketch.

Consider an equivalent CTL-formula $\phi^{\prime}$ with $|\phi^{\prime}|\leq|\phi|$ where negations, if any, occur right before the proposition $p$ . Then, if $\phi^{\prime}$ uses the operator $\operatorname{\mathbf{G}}$ , it cannot distinguish the structures $K_{l,\{p\},\emptyset}$ and $K_{l,\emptyset,\emptyset}$ . Otherwise, if it uses the operator $\operatorname{\mathbf{F}}$ , it cannot distinguish the structures $K_{l,\{p\},\emptyset}$ and $K_{l,\emptyset,\{p\}}$ . Otherwise, since $K_{l,\{p\},\emptyset},K_{l,\emptyset,\{p\}}$ , and $K_{l,\emptyset,\emptyset}$ coincide on the first $l$ states, $\phi^{\prime}$ has to use at least $l$ operators $\operatorname{\mathbf{X}}$ . Since $|\phi^{\prime}|\leq l+1$ , it cannot use a negation. Thus $\phi^{\prime}$ does not use $\operatorname{\mathbf{F}},\operatorname{\mathbf{G}},\neg$ , and neither does $\phi$ . $\hfill\blacktriangleleft$

In fact, a $\mathsf{CTL}$ -formula $\phi\in\mathsf{CTL}(\{p\},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ of size at most $l+1$ accepting $K_{l,\{p\},\emptyset}$ and rejecting $K_{l,\emptyset,\{p\}},K_{l,\emptyset,\emptyset}$ necessarily uses exactly $l$ operators $\operatorname{\mathbf{X}}$ followed by the proposition $p$ . Such a formula is therefore entirely defined by the $\operatorname{\mathbf{X}}$ operators before which it uses the $\exists$ quantifier. This suggests the definition below of the CTL-formula $\phi(l,H)$ induced by a subset $H\subseteq[1,\ldots,l]$ .

Definition 12.

For all $H\subseteq[1,\ldots,l]$ , we let $\phi(l,H)\in\mathsf{CTL}(\{p\},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ denote the $\mathsf{CTL}$ -formula defined by $\phi(l,H):=Q_{1}\operatorname{\mathbf{X}}\cdots Q_{l}\operatorname{\mathbf{X}}p$ where, for all $1\leq i\leq l$ , we have $Q_{i}\in\{\exists,\forall\}$ and $Q_{i}=\exists$ if and only if $i\in H$ .

For $1\leq i\leq l+1$ , we let $\phi_{i}(l,H):=Q_{i}\operatorname{\mathbf{X}}\ldots Q_{l}\operatorname{\mathbf% {X}}p$ (with $\phi_{l+1}(l,H):=p$ ).

Let us now turn toward Step b. We define a structure $K^{l}_{\exists>k}$ with $k+2$ different levels, where: the single starting state $q_{0,1}$ is at the bottommost level; the proposition $p$ only labels the state $q^{\mathsf{win}}$ at the topmost level; and every state of the bottom $k+1$ levels has a successor at the same level and one level higher. That way, going from $q_{0,1}$ to $q^{\mathsf{win}}$ is equivalent to leveling up $k+1$ times. Furthermore, the top most level can be reached in at most $l$ . An example is depicted in Figure 2. This structure satisfies the lemma below.

Figure 2: The Kripke structure

K^{5}_{\exists>2}

.

Figure 3: The Kripke structure

K_{5,\{2,5\}}

.

Lemma 13.

For all $H\subseteq[1,\ldots,l]$ , we have $K^{l}_{\exists>k}\models\phi(l,H)$ if and only if $|H|>k$ .

Consider now Step c. For $C\subseteq[1,\ldots,l]$ , we define the Kripke structure $K(l,C)$ with $\{q_{1},\ldots,q_{l},q_{l+1},q^{\mathsf{win}}\}$ as set of states where $q^{\mathsf{win}}$ is the only state labeled with $p$ ; and for all $1\leq j\leq l$ , $q_{j}$ branches to $q_{j+1}$ and, if (and only if) $j\in C$ , $q_{j}$ also branches to $q^{\mathsf{win}}$ , as exemplified in Figure 3. Such structures satisfy the lemma below.

Lemma 14.

For all $C,H\subseteq[1,\ldots,l]$ , we have $K_{(l,C)}\models\phi(l,H)$ if and only if $C\cap H\neq\emptyset$ .

Proof sketch.

We can show by induction on $l+1\geq j\geq 1$ the property $\mathcal{P}(j)$ : $q_{j}\models\phi_{j}(l,H)$ if and only if $H\cap[j,\ldots,l]\cap C\neq\emptyset$ . The lemma is then given by $\mathcal{P}(1)$ . $\hfill\blacktriangleleft$

We can finally define the reduction that we consider. We let $\mathsf{In}^{\mathsf{CTL}}:=(\{p\},\mathcal{P},\mathcal{N},B)$ , with $B:=l+1$ , $\mathcal{P}:=\{K_{l,\{p\},\emptyset},K_{i}\mid 1\leq i\leq n\}$ and $\mathcal{N}:=\{K_{l,\emptyset,\emptyset},K_{l,\emptyset,\{p\}},K^{l}_{\exists>% k}\}$ , be an input of the decision problem $\mathsf{CTL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ . By Lemmas 11, 13, 14, $\mathsf{In}^{\mathsf{CTL}}$ is a positive instance of the decision problem $\mathsf{CTL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ if and only if $(l,C,k)$ is a positive instance of the decision problem $\mathsf{Hit}$ . Theorem 10 follows (in the case $n=0$ ).

Assume that $\operatorname{\mathbf{X}}\notin\mathsf{U}^{\mathsf{t}}$ .

In that case, the CTL learning problem is now in $\mathsf{NL}$ .

Theorem 15.

For all sets of operators $\mathsf{U}^{\mathsf{t}}\subseteq\{\operatorname{\mathbf{F}},\operatorname{% \mathbf{G}},\neg\}$ , $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ , and bounds $n\in\mathbb{N}$ , the decision problem $\mathsf{CTL}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},n)$ is in $\mathsf{NL}$ .

Toward Step A, a crucial observation is that using the operators $\operatorname{\mathbf{F}}$ or $\operatorname{\mathbf{G}}$ twice in a row is useless. This is stated in the lemma below in the context of $\mathsf{ATL}$ -formula because this lemma will be used again in the next subsection.

Lemma 16.

Let $I\subseteq J\subseteq\mathbb{N}$ , and $\phi$ be an $\mathsf{ATL}$ -formula. We have:
$\displaystyle\langle\!\langle J\rangle\!\rangle\operatorname{\mathbf{F}}\phi$ $\displaystyle\equiv\langle\!\langle I\rangle\!\rangle\operatorname{\mathbf{F}}% \langle\!\langle J\rangle\!\rangle\operatorname{\mathbf{F}}\phi\equiv\langle\!% \langle J\rangle\!\rangle\operatorname{\mathbf{F}}\langle\!\langle I\rangle\!% \rangle\operatorname{\mathbf{F}}\phi$ $\displaystyle\langle\!\langle I\rangle\!\rangle\operatorname{\mathbf{G}}\phi$ $\displaystyle\equiv\langle\!\langle I\rangle\!\rangle\operatorname{\mathbf{G}}% \langle\!\langle J\rangle\!\rangle\operatorname{\mathbf{G}}\phi\equiv\langle\!% \langle J\rangle\!\rangle\operatorname{\mathbf{G}}\langle\!\langle I\rangle\!% \rangle\operatorname{\mathbf{G}}\phi$

Proof sketch.

We argue the result for $\operatorname{\mathbf{F}}$ , the case of $\operatorname{\mathbf{G}}$ is dual. We have $\langle\!\langle J\rangle\!\rangle\operatorname{\mathbf{F}}\phi\implies\langle% \!\langle I\rangle\!\rangle\operatorname{\mathbf{F}}\langle\!\langle J\rangle% \!\rangle\operatorname{\mathbf{F}}$ by definition of $\operatorname{\mathbf{F}}$ . Furthermore, if a state $q$ satisfies $\langle\!\langle I\rangle\!\rangle\operatorname{\mathbf{F}}\langle\!\langle J% \rangle\!\rangle\operatorname{\mathbf{F}}\phi$ then there is a strategy $\mathsf{s}_{I}$ for the coalition $I$ such that eventually a state satisfying $\langle\!\langle J\rangle\!\rangle\operatorname{\mathbf{F}}\phi$ is surely reached. For all such states $q$ , we consider a strategy $\mathsf{s}_{J}^{q}$ for the coalition $J$ ensuring to eventually visit a state satisfying $\phi$ . Then, consider a strategy $\mathsf{s}_{J}^{\prime}$ for the coalition $J$ that: mimics $\mathsf{s}_{I}$ (which is possible since $I\subseteq J$ ) until a state $q$ satisfying $\langle\!\langle J\rangle\!\rangle\operatorname{\mathbf{F}}\phi$ is reached, and then switches to the strategy $\mathsf{s}_{J}^{q}$ . That strategy ensures eventually reaching a state satisfying $\phi$ . Therefore, $\langle\!\langle I\rangle\!\rangle\operatorname{\mathbf{F}}\langle\!\langle J% \rangle\!\rangle\operatorname{\mathbf{F}}\phi\implies\langle\!\langle J\rangle% \!\rangle\operatorname{\mathbf{F}}\phi$ . This is similar for $\langle\!\langle J\rangle\!\rangle\operatorname{\mathbf{F}}\langle\!\langle I% \rangle\!\rangle\operatorname{\mathbf{F}}\phi$ . $\hfill\blacktriangleleft$

From this, we can actually deduce (this is not direct) that there is a bound $M\in\mathbb{N}$ such that, for any set of propositions $\mathsf{Prop}$ and for all $\mathsf{U}^{\mathsf{t}}\subseteq\{\operatorname{\mathbf{F}},\operatorname{% \mathbf{G}},\neg\}$ , given any $\mathsf{CTL}(\mathsf{Prop},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ -formula $\phi$ , there is an equivalent $\mathsf{CTL}(\mathsf{Prop},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ -formula $\phi^{\prime}$ , with $|\phi^{\prime}|\leq M$ . Thus, the number of $\mathsf{CTL}$ -formulas to consider is linear in $|\mathsf{Prop}|$ . As for Step B, consider any such formula $\phi$ . Since the number of quantifiers it uses is bounded by $M$ and $\mathsf{NL}=\mathsf{coNL}$ , we deduce that checking that it satisfies a Kripke structure can be done in $\mathsf{NL}$ .

Proof of NL-hardness.

In Table 1, we do not state only that CTL learning without the operator $\operatorname{\mathbf{X}}$ is in $\mathsf{NL}$ , but also that it is $\mathsf{NL}$ -hard. Proving this result is actually straightforward. We exhibit a reduction from the problem of reachability in a graph (which is $\mathsf{NL}$ -complete [23]). Given an input $(\mathcal{G},s,t)$ of that problem, with $\mathcal{G}$ a graph, $s$ the source state and $t$ the target state, we define a positive Kripke structure $K$ that is obtained from $\mathcal{G}$ by making $s$ its only initial state, and $t$ the only state labeled by the proposition $p$ . Additionally, we consider $B:=2$ as the bound, and with an additional structure, we ensure that if there is a separating formula, then the formula $\phi:=\exists\operatorname{\mathbf{F}}p$ is separating.

4.5 ATL learning

We have seen that CTL learning with the operator $\operatorname{\mathbf{X}}$ is $\mathsf{NP}$ -hard, which implies that it is also the case for ATL learning. Here, we consider the case of ATL learning without the operator $\operatorname{\mathbf{X}}$ . First, let us informally explain why the $\mathsf{NP}$ -hardness reduction that we have described above for CTL cannot possibly work without the operator $\operatorname{\mathbf{X}}$ . A central aspect of the proof of Lemma 14 is to be able to associate a specific operator in a prospective formula with a specific state in a Kripke structure. That is intrinsically not possible with the operator $\operatorname{\mathbf{F}}$ since this operator looks at arbitrarily distant horizons. At least, this is true with CTL-formulas interpreted on Kripke structures. However, with $\mathsf{ATL}$ -formulas interpreted on turn-based structures, it is possible to “block the horizon” of $\operatorname{\mathbf{F}}$ operators. Indeed, consider the structure of Figure 5, where blue lozenge-shaped states are Agent-1 states, and red square-shaped states are Agent-2’s. Here, one can see that $q_{2}^{1,2}\not\models\langle\!\langle 1\rangle\!\rangle\operatorname{\mathbf{% F}}p$ because Agent 2 can enforce to loop on the Agent-2 state $q_{1}^{1,2}$ and not see the state $q^{\mathsf{win}}$ , labeled by $p$ .

Figure 4: The turn-based structure

T_{4:1,2}

.

Figure 5: On the left

T_{p}

, on the right

T_{\mathsf{no}\;2\operatorname{\mathbf{G}}}

.

These kinds of turn-based games will be extensively used in the following. In all generality, there are defined as follows: given a pair of agents $i\neq j$ and $l\in\mathbb{N}$ , in the turn-based structure $T_{l:i,j}$ , there are $l+1$ self-looping states, alternatively belonging to Agents $i$ and $j$ , that can get closer and closer to the self-looping sink $q^{\mathsf{win}}$ , the only state labeled by $p$ . In fact, such structures are linked to alternating-formulas, defined below.

Definition 17.

An $\mathsf{ATL}$ -formula is positive if it does not use any negation. For a pair of agents $i\neq j$ and $l\in\mathbb{N}$ , a positive $\mathsf{ATL}$ -formula $\phi$ is $(i,j)$ -free if it does not use an operator $\langle\!\langle A\rangle\!\rangle\operatorname{\mathbf{F}}$ with $i,j\in A$ . It is $(i,j,l)$ -alternating if it is $(i,j)$ -free and if there are at least $l$ alternating occurrences of operators $\langle\!\langle A_{i}\rangle\!\rangle\operatorname{\mathbf{F}}$ with $i\in A_{i}$ and $\langle\!\langle A_{j}\rangle\!\rangle\operatorname{\mathbf{F}}$ with $j\in A_{j}$ .

Lemma 18.

Consider two agents $i\neq j$ , $l\in\mathbb{N}$ , and a positive $\mathsf{ATL}$ -formula $\phi$ that is $(i,j)$ -free. The formula $\phi$ accepts the structure $T_{l:i,j}$ if and only if it is $(i,j,l)$ -alternating.

$\mathsf{ATL}^{2}$ learning with $\{\operatorname{\mathbf{F}},\operatorname{\mathbf{G}}\}\subseteq\mathsf{U}^{% \mathsf{t}}$ .

Here, all the turn-based structures that we consider use the set of agents $\mathsf{Ag}=\{1,2\}$ . The goal is to show the theorem below.

Theorem 19.

For all sets $\mathsf{U}^{\mathsf{t}}\subseteq\mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$ , $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ , and bound $n\in\mathbb{N}$ , if $\{\operatorname{\mathbf{F}},\operatorname{\mathbf{G}}\}\subseteq\mathsf{U}^{% \mathsf{t}}$ and $\operatorname{\mathbf{X}}\notin\mathsf{U}^{\mathsf{t}}$ , then the decision problem $\mathsf{ATL}^{2}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}% ^{\mathsf{l}},n)$ is $\mathsf{NP}$ -hard.

In the following, to ease the notations, the strategic operators $\langle\!\langle\emptyset\rangle\!\rangle,\langle\!\langle\{1\}\rangle\!% \rangle,\langle\!\langle\{2\}\rangle\!\rangle,\langle\!\langle\{1,2\}\rangle\!\rangle$ will simply be denoted $\emptyset$ , $1$ , $2$ and $1,2$ respectively. Consider an instance $(l,C,k)$ of the hitting set problem. We follow the recipe of Subsection 4.2. Here, we want separating formulas to be promising, i.e. to only use the operators $1\operatorname{\mathbf{F}},2\operatorname{\mathbf{F}}$ and $1\operatorname{\mathbf{G}}$ . To this end, all the structures we use are self-looping, thus making the operators $\emptyset\operatorname{\mathbf{F}}$ and $1,2\operatorname{\mathbf{G}}$ useless.

Lemma 20.

For all $\mathsf{ATL}$ -formulas $\phi$ and self-looping states $q$ , we have: $q\models\phi\text{ if and only if }q\models\emptyset\operatorname{\mathbf{F}}% \phi\text{ if and only if }q\models 1,2\operatorname{\mathbf{G}}\phi$

Proof.

Since $q$ is self-looping the coalition of agents $\{1,2\}$ has a strategy $\mathsf{s}$ such that $\mathsf{Out}(q,\mathsf{s})=\{q^{\omega}\}$ . The lemma follows from the definition of the operators $\operatorname{\mathbf{F}}$ and $\operatorname{\mathbf{G}}$ . $\hfill\blacktriangleleft$

We also consider the two structures $T_{p},T_{\mathsf{no}\;2\operatorname{\mathbf{G}}}$ , of Figure 5 satisfying the lemma below.

Lemma 21.

For all $\mathsf{ATL}$ -formulas $\phi\in\mathsf{ATL}(\{p\},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}^{% \mathsf{l}},0)$ accepting $T_{p},T_{\mathsf{no}\;2\operatorname{\mathbf{G}}}$ and rejecting $T_{2l+1:1,2}$ , there is a promising formula $\phi^{\prime}\in\mathsf{ATL}(\{p\},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B% }^{\mathsf{l}},0)$ with $|\phi^{\prime}|\leq|\phi|$ that is equivalent to $\phi$ on self-looping structures.

Proof sketch.

Consider an $\mathsf{ATL}$ -formula $\phi^{\prime}$ equivalent to $\phi$ with $|\phi^{\prime}|\leq|\phi|$ and with at most one negation occurring before the proposition $p$ . Since $\phi^{\prime}$ accepts $T_{p}$ , it follows that it is positive. By Lemma 20, we can remove the operators $1,2\operatorname{\mathbf{G}}$ and $\emptyset\operatorname{\mathbf{F}}$ from $\phi^{\prime}$ . Furthermore: $\phi^{\prime}$ cannot use $\emptyset\operatorname{\mathbf{G}},2\operatorname{\mathbf{G}}$ , since it accepts $T_{\mathsf{no}\;2\operatorname{\mathbf{G}}}$ , and it cannot use $1,2\operatorname{\mathbf{F}}$ since it rejects $T_{2l+1:1,2}$ . It is therefore promising. $\hfill\blacktriangleleft$

Figure 6: The structure

T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq 2}

.

Figure 7: The structure

T_{2,\{1\},2}

.

We will also consider $T_{2l:1,2}$ as a positive structure, thus allowing us to focus on $(1,2,2l)$ -alternating formulas (recall Lemma 18). Then, we want to associate to a subset $H\subseteq[1,\ldots,l]$ a promising $(1,2,2l)$ -alternating $\mathsf{ATL}$ -formula. To get an intuition, let us consider the turn-based structure $T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq t}$ for $t=2$ of Figure 6. This structure $T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq t}$ is analogous to the structure $T_{2t:1,2}$ except that all Agent-2 states have an additional successor: the state $q^{\mathsf{lose}}$ that does not satisfy any positive formula. Back to the structure of Figure 6, because Agent 2 owns the states $q_{3}^{\operatorname{\mathbf{G}}},q_{1}^{\operatorname{\mathbf{G}}}$ , these states do not accept any positive $\mathsf{ATL}$ -formula of the shape $1\operatorname{\mathbf{G}}\phi$ . Therefore, for all $q\in\{q_{4}^{\operatorname{\mathbf{G}}},q_{2}^{\operatorname{\mathbf{G}}}\}$ and positive $\mathsf{ATL}$ -formulas $\phi$ , we have $q\models 1\operatorname{\mathbf{F}}1\operatorname{\mathbf{G}}2\operatorname{% \mathbf{F}}\phi$ if and only if $q\models\phi$ . This actually implies that a $(1,2,2l)$ -alternating formula $\phi$ accepts $T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq 2}$ if and only if the sequence of operators $1\operatorname{\mathbf{F}}2\operatorname{\mathbf{F}}$ (without $1\operatorname{\mathbf{G}}$ in between) occurs at least twice in $\phi$ (to go from $q_{4}^{\operatorname{\mathbf{G}}}$ to $q_{2}^{\operatorname{\mathbf{G}}}$ and then from $q_{2}^{\operatorname{\mathbf{G}}}$ to $q^{\mathsf{win}}$ ). In fact, we consider formulas that only use $1\operatorname{\mathbf{G}}$ operators after $1\operatorname{\mathbf{F}}$ and before $2\operatorname{\mathbf{F}}$ , as defined below. Such formulas satisfy the lemma that follows.

Definition 22.

For all $H\subseteq[1,\ldots,l]$ , we let $\phi(l,H,2)\in\mathsf{ATL}^{2}(\{p\},\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf% {B}^{\mathsf{l}},0)$ denote the $\mathsf{ATL}$ -formula defined by: $\phi(l,H,2):=1\operatorname{\mathbf{F}}Q_{1}2\operatorname{\mathbf{F}}\cdots 1% \operatorname{\mathbf{F}}Q_{l}2\operatorname{\mathbf{F}}p$ where, for all $1\leq i\leq l$ , we have $Q_{i}\in\{\epsilon,1\operatorname{\mathbf{G}}\}$ and $Q_{i}=1\operatorname{\mathbf{G}}$ iff $i\notin H$ .

For all $1\leq i\leq l+1$ , we let $\phi_{i}(l,H,2):=1\operatorname{\mathbf{F}}Q_{i}2\operatorname{\mathbf{F}}% \cdots 1\operatorname{\mathbf{F}}Q_{l}2\operatorname{\mathbf{F}}p$ (with $\phi_{l+1}(l,H,2):=p$ ).

Lemma 23.

A promising $(1,2,2l)$ -alternating formula $\phi$ with $|\phi|\leq 3l+1-k$ rejects $T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq k+1}$ if and only if $\phi=\phi(l,H,2)$ for some $H\subseteq[1,\ldots,l]$ such that $|H|=k$ .

Proof sketch.

Since $\phi$ is $(1,2,2l)$ -alternating, it uses at least $l$ operators $1\operatorname{\mathbf{F}}$ and $2\operatorname{\mathbf{F}}$ . Thus, it can use at most $l-k$ operators $1\operatorname{\mathbf{G}}$ . In addition, $\phi$ accepts $T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq k+1}$ iff there are at least $k+1$ occurrences of the sequence $1\operatorname{\mathbf{F}}2\operatorname{\mathbf{F}}$ in $\phi$ . Thus, $\phi$ uses each $l-k$ remaining operators $1\operatorname{\mathbf{G}}$ between a different pair of successive $1\operatorname{\mathbf{F}},2\operatorname{\mathbf{F}}$ iff it rejects $T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq k+1}$ . $\hfill\blacktriangleleft$

With $T_{p},T_{\mathsf{no}\;2\operatorname{\mathbf{G}}},T_{2l:1,2}$ as positive structures and $T_{2l+1:1,2},T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq k+1}$ as negative structures, we have achieved both Steps a and b. Let us turn to Step c. For all $C\subseteq[1,\ldots,l]$ , we define a turn-based structure $T_{l,C,2}$ . An example is depicted in Figure 7 for $l=2$ . The structure $T_{l,C,2}$ features a sequence of states $q_{1}^{1},q_{1}^{2},\ldots,q_{l}^{1},q_{l}^{2}$ alternating between Agent-1 and Agent-2 states ending in a self-looping sink $q^{\mathsf{lose}}$ not labeled by $p$ . However, the Agent-1 states $q_{i}^{1}$ for which $i\in C$ have a “testing state” $q_{i}^{\mathsf{Test}}$ as successor. That state is self-looping, and may branch to the self-looping sink $q^{\mathsf{lose}}$ or to the structure $T_{2(l-i):1,2}$ . That state is such that $q_{i}^{\mathsf{Test}}\models Q_{i}2\operatorname{\mathbf{F}}\phi_{i+1}(l,H,2)$ iff $Q_{i}=\epsilon$ (iff $i\in H$ ). Furthermore, note that it is useless to “wait” at the state $q_{i}^{1}$ before branching to $q_{i}^{\mathsf{Test}}$ . Indeed, if for instance $Q_{i}=1\operatorname{\mathbf{G}}$ but $Q_{i+1}=\epsilon$ , then it may seem that $q_{1}^{\mathsf{Test}}\models\varphi^{\prime}$ , for $\varphi^{\prime}:=Q_{i+1}2\operatorname{\mathbf{F}}\phi_{i+2}(l,H,2)$ and therefore $q_{i}^{1}\models\phi_{i}(l,H,2)=1\operatorname{\mathbf{F}}Q_{i}2\operatorname{% \mathbf{F}}1\operatorname{\mathbf{F}}\varphi^{\prime}$ . However, it is not the case because we do not have $q_{i}^{\mathsf{Test}}\models\varphi^{\prime}$ , since $\phi_{i+2}(l,H,2)$ is not $(1,2,2(l-i))$ -alternating, and thus it does not satisfy the structure $T_{2(l-i):1,2}$ . Overall, we have the lemma below.

Lemma 24.

For all $C,H\subseteq[1,\ldots,l]$ , we have $T_{(l,C)}\models\phi(l,H,2)$ if and only if $C\cap H\neq\emptyset$ .

We have achieved Step c. Then, we let $\mathsf{In}^{\mathsf{ATL}(2)}:=(\{p\},\mathcal{P},\mathcal{N},B)$ be an input of the decision problem $\mathsf{ATL}^{2}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}% ^{\mathsf{l}},0)$ where $\mathcal{P}:=\{T_{p},T_{\mathsf{no}\;2\operatorname{\mathbf{G}}},T_{2l:1,2},T_% {(l,C_{i},2)}\mid 1\leq i\leq n\}$ , $\mathcal{N}:=\{T_{2l+1:1,2},T_{\mathsf{no}\;1\operatorname{\mathbf{G}}\geq k+1}\}$ , and $B:=3l+1-k$ . By Lemmas 21, 23 and 24, $\mathsf{In}^{\mathsf{ATL}(2)}$ is a positive instance of $\mathsf{ATL}^{2}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}% ^{\mathsf{l}},0)$ iff $(l,C,k)$ is a positive instance of $\mathsf{Hit}$ .

$\mathsf{ATL}^{2}$ learning with $\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{F}}\}$ or $\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{G}}\}$ .

The $\mathsf{ATL}^{2}$ learning problem is now in $\mathsf{P}$ .

Theorem 25.

For all sets of operators $\mathsf{U}^{\mathsf{t}}\in\{\{\operatorname{\mathbf{F}}\},\{\operatorname{% \mathbf{G}}\}\}$ , $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ , and bounds $n\in\mathbb{N}$ , the decision problem $\mathsf{ATL}^{2}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}% ^{\mathsf{l}},n)$ is in $\mathsf{P}$ .

We focus on the case $\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{F}}\}$ , the other is analogous. Towards Step A, consider a formula $\phi\in\mathsf{ATL}^{2}(\mathsf{Prop},\{\operatorname{\mathbf{F}}\},\emptyset,% \mathsf{B}^{\mathsf{l}},0)$ and the only proposition $p\in\mathsf{Prop}$ occurring in $\phi$ . By Lemma 16, we can make the following observations: 1) If the operator $1,2\operatorname{\mathbf{F}}$ occurs in $\phi$ , then $\phi\equiv 1,2\operatorname{\mathbf{F}}p$ ; 2) Otherwise, if the only operator occurring in $\phi$ is $\emptyset\operatorname{\mathbf{F}}$ then $\phi\equiv\emptyset\operatorname{\mathbf{F}}p$ ; 3) Otherwise, $\phi$ is equivalent to a formula $\phi^{\prime}$ alternating between the operators $1\operatorname{\mathbf{F}}$ and $2\operatorname{\mathbf{F}}$ , with $|\phi^{\prime}|\leq|\phi|$ . These observations suggest the definition below, which satisfies the lemma that follows.

Definition 26.

For a set of propositions $\mathsf{Prop}$ , we define the set $\mathsf{ATL}^{2}_{\operatorname{\mathbf{F}}}(\mathsf{Prop}):=\{\mathsf{Qt}% \cdot p\mid p\in\mathsf{Prop},\;\mathsf{Qt}\in\mathsf{Quant}_{\mathsf{Alt}}^{% \operatorname{\mathbf{F}}}\}$ where $\mathsf{Quant}_{\mathsf{Alt}}^{\operatorname{\mathbf{F}}}:=\{\epsilon,% \emptyset\operatorname{\mathbf{F}},1,2\operatorname{\mathbf{F}},(1% \operatorname{\mathbf{F}}\cdot 2\operatorname{\mathbf{F}})^{*},(1\operatorname% {\mathbf{F}}\cdot 2\operatorname{\mathbf{F}})^{*}\cdot 1\operatorname{\mathbf{% F}},(2\operatorname{\mathbf{F}}\cdot 1\operatorname{\mathbf{F}})^{*},(2% \operatorname{\mathbf{F}}\cdot 1\operatorname{\mathbf{F}})^{*}\cdot 2% \operatorname{\mathbf{F}}\}$ .

Lemma 27.

For a set of propositions $\mathsf{Prop}$ , and $\phi\in\mathsf{ATL}^{2}(\mathsf{Prop},\{\operatorname{\mathbf{F}}\},\emptyset,% \mathsf{B}^{\mathsf{l}},0)$ , there is an $\mathsf{ATL}$ -formula $\phi^{\prime}\in\mathsf{ATL}^{2}_{\operatorname{\mathbf{F}}}(\mathsf{Prop})$ such that $\phi\equiv\phi^{\prime}$ and $|\phi^{\prime}|\leq|\phi|$ .

This concludes Step A since the number of formulas of size at most $B$ in $\mathsf{ATL}^{2}_{\operatorname{\mathbf{F}}}(\mathsf{Prop})$ is polynomial in $B$ and $|\mathsf{Prop}|$ . As for Step B, in this case it is trivial since checking that an $\mathsf{ATL}$ -formula satisfies a structure can always be done in polynomial time.

Proof of P-hardness.

In Table 1, we additionally state only that $\mathsf{ATL}^{2}$ learning with $\mathsf{U}^{\mathsf{t}}\in\{\{\operatorname{\mathbf{F}}\},\{\operatorname{% \mathbf{G}}\}\}$ is $\mathsf{P}$ -hard. The proof of this fact is actually very similar to the proof that $\mathsf{CTL}$ learning without the operator $\operatorname{\mathbf{X}}$ is $\mathsf{NL}$ -hard, except that the reduction is made from the problem of reachability in a turn-based game (which is $\mathsf{P}$ -complete [31]).

$\mathsf{ATL}^{3}$ learning with $\mathsf{U}^{\mathsf{t}}\in\{\{\operatorname{\mathbf{F}}\},\{\operatorname{% \mathbf{G}}\}\}$ .

Let us consider $\mathsf{ATL}$ learning with one more agent, i.e. $\mathsf{ATL}^{3}$ learning, still with $\mathsf{U}^{\mathsf{t}}\in\{\{\operatorname{\mathbf{F}}\},\{\operatorname{% \mathbf{G}}\}\}$ . The turn-based structures that we consider now use the set of agents $\mathsf{Ag}=\{1,2,3\}$ . The goal is to show the theorem below.

Theorem 28.

For all sets $\mathsf{U}^{\mathsf{t}}\in\{\{\operatorname{\mathbf{F}}\},\{\operatorname{% \mathbf{G}}\}\}$ , $\mathsf{B}^{\mathsf{l}}\subseteq\mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ , and bound $n\in\mathbb{N}$ , the decision problem $\mathsf{ATL}^{3}_{\mathsf{Learn}}(\mathsf{U}^{\mathsf{t}},\emptyset,\mathsf{B}% ^{\mathsf{l}},n)$ is $\mathsf{NP}$ -hard.

We focus on the case $\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{F}}\}$ (the case $\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{G}}\}$ is analogous since the operators $\operatorname{\mathbf{F}}$ and $\operatorname{\mathbf{G}}$ have a dual behavior). Once again, let us consider an instance $(l,C,k)$ of the problem $\mathsf{Hit}$ . We start right away by defining the $\mathsf{ATL}^{3}$ -formula associated to a subset $H\subseteq[1,\ldots,l]$ .

Definition 29.

For $H\subseteq[1,\ldots,l]$ , we let $\phi(l,H,3)$ denote the $\mathsf{ATL}^{3}$ -formula defined by $\phi(l,H,3):=1\operatorname{\mathbf{F}}\langle\!\langle A_{1}\rangle\!\rangle% \operatorname{\mathbf{F}}\cdots 1\operatorname{\mathbf{F}}\langle\!\langle A_{% l}\rangle\!\rangle\operatorname{\mathbf{F}}p$ where, for all $1\leq i\leq l$ , we have $A_{i}\in\{\{2\},\{2,3\}\}$ and $A_{i}=\{2,3\}\operatorname{\mathbf{F}}$ if and only if $i\in H$ .

For $1\leq i\leq l+1$ , we let $\phi_{i}(l,H,3):=1\operatorname{\mathbf{F}}\langle\!\langle A_{i}\rangle\!% \rangle\operatorname{\mathbf{F}}\cdots 1\operatorname{\mathbf{F}}\langle\!% \langle A_{l}\rangle\!\rangle\operatorname{\mathbf{F}}p$ (with $\phi_{l+1}(l,H,3)=p$ ).

Toward Step a, we define $T_{2l+1:1,2},T_{2(k+1):1,3}$ as negative structures, thus ensuring that a separating formula does not use an operator $\langle\!\langle A\rangle\!\rangle\operatorname{\mathbf{F}}$ with $1,2\in A$ , or $1,3\in A$ . We also define $T_{2l:1,2}$ as a positive structure with the bound $B:=2l+1$ . That way, a separating formula is necessarily $(1,2,2l)$ -alternating and only uses the operators $1\operatorname{\mathbf{F}},2\operatorname{\mathbf{F}}$ , and $2,3\operatorname{\mathbf{F}}$ .

Lemma 30.

If a formula $\phi\in\mathsf{ATL}^{3}(\{\{p\},\{\operatorname{\mathbf{F}}\},\emptyset,% \mathsf{B}^{\mathsf{l}},n)$ with $|\phi|\leq 2l+1$ accepts $T_{2l:1,2}$ and rejects $T_{2l+1:1,2},T_{2(k+1):1,3}$ , then there is some $H\subseteq[1,\ldots,l]$ such that $\phi=\phi(l,H,3)$ .

Note that, if $|H|\geq k+1$ , then $\phi(l,H,3)$ is $(1,3,2(k+1))$ -alternating. Therefore, since $T_{2(k+1):1,3}$ is a negative structure, if $\phi(l,H,3)$ is separating, then $|H|\leq k$ , i.e. we have also achieved Step b. Let us now turn to Step c. For all $C\subseteq[1,\ldots,l]$ , we define the structure $T_{l,C,3}$ . An example is given in Figure 8 with $l=3$ . This structure $T_{l,C,3}$ features a sequence of states $q_{1}^{1},q_{1}^{2},\ldots,q_{l}^{1},q_{l}^{2}$ alternating between Agent-1 and Agent-2 states ending in a self-looping sink $q^{\mathsf{lose}}$ . However, the Agent-1 states $q_{i}^{1}$ for which $i\in C$ have an Agent-3 “testing state” $q_{i}^{\mathsf{Test}}$ as successor. That state is self-looping and also branches to the structure $T_{(l-i):1,2}$ . Note that, given $r\geq i+1$ , the sub-formula $\phi_{r}(l,H,3)$ is $(1,2,l-r+1)$ -alternating, and therefore satisfies the structure $T_{(l-i):1,2}$ , iff $r=i+1$ . Thus, since $q_{i}^{\mathsf{Test}}$ is an Agent-3 state, $q_{i}^{\mathsf{Test}}\models\langle\!\langle A_{i}\rangle\!\rangle% \operatorname{\mathbf{F}}\phi_{i+1}(l,H,3)$ iff $3\in A_{i}$ iff $i\in H$ . Thus, we have the following lemma.

Figure 8: The turn-based structure

T_{3,\{2\},3}

.

Lemma 31.

For all $C,H\subseteq[1,\ldots,l]$ , we have $T_{(l,C,3)}\models\phi(l,H,3)$ if and only if $C\cap H\neq\emptyset$ .

This concludes Step c. Overall, we let $\mathsf{In}^{\mathsf{ATL}(3),\operatorname{\mathbf{F}}}:=(\{p\},\mathcal{P},% \mathcal{N},B)$ be an input of the decision problem $\mathsf{ATL}^{3}_{\mathsf{Learn}}(\{\operatorname{\mathbf{F}}\},\emptyset,% \mathsf{B}^{\mathsf{l}},0)$ where $\mathcal{P}:=\{T_{2l:1,2},T_{(l,C_{i},3)}\mid 1\leq i\leq n\}$ , $\mathcal{N}:=\{T_{2l+1:1,2},T_{2(k+1):1,3}\}$ , and $B:=2l+1$ . We have that $\mathsf{In}^{\mathsf{ATL}(3),\operatorname{\mathbf{F}}}$ is a positive instance of $\mathsf{ATL}_{\mathsf{Learn}}^{3}(\{\operatorname{\mathbf{F}}\},\emptyset,% \mathsf{B}^{\mathsf{l}},0)$ if and only if $(l,C,k)$ is a positive instance of $\mathsf{Hit}$ .

5 Future Work

Within our setting, we have covered many cases, as can be seen in Table 1. That is why the complete version of this work [8] is already quite long. However, there are still some cases that we have not tackled. First, there is the case of $\mathsf{ATL}^{2}$ learning with $\mathsf{U}^{\mathsf{t}}\in\{\{\operatorname{\mathbf{F}},\neg\},\{\operatorname% {\mathbf{G}},\neg\}\}$ . We believe that it behaves like the case $\operatorname{\mathbf{F}},\operatorname{\mathbf{G}}\in\mathsf{U}^{\mathsf{t}}$ , but the proofs would entail many additional technical details, since replacing $\operatorname{\mathbf{F}}$ with $\neg\operatorname{\mathbf{G}}\neg$ increases the size of the formulas.

More importantly, when considering a bounded amount of binary operators, we have not allowed binary temporal operators ( $\operatorname{\mathbf{U}},\operatorname{\mathbf{R}},\operatorname{\mathbf{W}},% \operatorname{\mathbf{M}}$ ). Doing so would enhance the expressivity of the fragment that we consider, and we conjecture that we would obtain the same result as in this paper, with proofs that should be only moderately more involved.

On a more high level perspective, in this paper we have focused solely on solving exactly the learning problems and although we have found some relevant tractable cases, many are untractable. A promising research direction would be to look for tractable approximation algorithms, similarly to what is done in [27].

References

[1] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672–713, September 2002. doi:10.1145/585265.585270.
[2] Dana Angluin. On the complexity of minimum inference of regular sets. Inf. Control., 39(3):337–350, 1978. doi:10.1016/S0019-9958(78)90683-6.
[3] M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli. SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In FMCAD, pages 93–103. IEEE, 2020. doi:10.34727/2020/ISBN.978-3-85448-042-6_16.
[4] Ayca Balkan, Moshe Y. Vardi, and Paulo Tabuada. Mode-target games: Reactive synthesis for control applications. IEEE Trans. Autom. Control., 63(1):196–202, 2018. doi:10.1109/TAC.2017.2722960.
[5] Elwyn R. Berlekamp, Robert J. McEliece, and Henk C. A. van Tilborg. On the inherent intractability of certain coding problems (corresp.). IEEE Trans. Inf. Theory, 24(3):384–386, 1978. doi:10.1109/TIT.1978.1055873.
[6] Dines Bjørner and Klaus Havelund. 40 years of formal methods - some obstacles and some possibilities? In FM, volume 8442 of Lecture Notes in Computer Science, pages 42–61. Springer, 2014. doi:10.1007/978-3-319-06410-9_4.
[7] Giuseppe Bombara, Cristian-Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka, and Calin Belta. A decision tree approach to data classification using signal temporal logic. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC ’16, pages 1–10, New York, NY, USA, 2016. Association for Computing Machinery. doi:10.1145/2883817.2883843.
[8] Benjamin Bordais, Daniel Neider, and Rajarshi Roy. The complexity of learning temporal properties. CoRR, abs/2408.04486, 2024. doi:10.48550/arXiv.2408.04486.
[9] Benjamin Bordais, Daniel Neider, and Rajarshi Roy. Learning branching-time properties in CTL and ATL via constraint solving. In André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I, volume 14933 of Lecture Notes in Computer Science, pages 304–323. Springer, 2024. doi:10.1007/978-3-031-71162-6_16.
[10] Alberto Camacho, Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIlraith. LTL and beyond: Formal languages for reward function specification in reinforcement learning. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 6065–6073. ijcai.org, 2019. doi:10.24963/IJCAI.2019/840.
[11] Alberto Camacho and Sheila A. McIlraith. Learning interpretable models expressed in linear temporal logic. In ICAPS, pages 621–630. AAAI Press, 2019. URL: https://ojs.aaai.org/index.php/ICAPS/article/view/3529.
[12] Alberto Camacho, Eleni Triantafillou, Christian J. Muise, Jorge A. Baier, and Sheila A. McIlraith. Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces. In AAAI, pages 3716–3724. AAAI Press, 2017. doi:10.1609/AAAI.V31I1.11058.
[13] Alessio Cecconi, Giuseppe De Giacomo, Claudio Di Ciccio, Fabrizio Maria Maggi, and Jan Mendling. Measuring the interestingness of temporal logic behavioral specifications in process mining. Inf. Syst., 107:101920, 2022. doi:10.1016/J.IS.2021.101920.
[14] William Chan. Temporal-logic queries. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 450–463. Springer, 2000.
[15] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer, 1981. doi:10.1007/BFB0025774.
[16] Rüdiger Ehlers, Ivan Gavran, and Daniel Neider. Learning properties in LTL $\cap$ ACTL from positive examples only. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 104–112. IEEE, 2020. doi:10.34727/2020/ISBN.978-3-85448-042-6_17.
[17] Georgios E. Fainekos, Hadas Kress-Gazit, and George J. Pappas. Temporal logic motion planning for mobile robots. In ICRA, pages 2020–2025. IEEE, 2005. doi:10.1109/ROBOT.2005.1570410.
[18] Nathanaël Fijalkow and Guillaume Lagarde. The complexity of learning linear temporal formulas from examples. In Jane Chandlee, Rémi Eyraud, Jeff Heinz, Adam Jardine, and Menno van Zaanen, editors, Proceedings of the 15th International Conference on Grammatical Inference, 23-27 August 2021, Virtual Event, volume 153 of Proceedings of Machine Learning Research, pages 237–250. PMLR, 2021. URL: https://proceedings.mlr.press/v153/fijalkow21a.html.
[19] Marie Fortin, Boris Konev, Vladislav Ryzhikov, Yury Savateev, Frank Wolter, and Michael Zakharyaschev. Reverse engineering of temporal queries mediated by LTL ontologies. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 3230–3238. ijcai.org, 2023. doi:10.24963/IJCAI.2023/360.
[20] Jean-Raphaël Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu, and Zhe Xu. Maxsat-based temporal logic inference from noisy data. Innov. Syst. Softw. Eng., 18(3):427–442, 2022. doi:10.1007/S11334-022-00444-8.
[21] E. Mark Gold. Complexity of automaton identification from given data. Inf. Control., 37(3):302–320, 1978. doi:10.1016/S0019-9958(78)90562-4.
[22] Antonio Ielo, Mark Law, Valeria Fionda, Francesco Ricca, Giuseppe De Giacomo, and Alessandra Russo. Towards ilp-based ltlf passive learning. In Inductive Logic Programming: 32nd International Conference, ILP 2023, Bari, Italy, November 13–15, 2023, Proceedings, pages 30–45, Berlin, Heidelberg, 2023. Springer-Verlag. doi:10.1007/978-3-031-49299-0_3.
[23] Neil Immerman. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci., 22(3):384–406, 1981. doi:10.1016/0022-0000(81)90039-8.
[24] Jean Christoph Jung, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Extremal separation problems for temporal instance queries. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, pages 3448–3456. ijcai.org, 2024. URL: https://www.ijcai.org/proceedings/2024/382.
[25] Xiao Li, Cristian Ioan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC, Canada, September 24-28, 2017, pages 3834–3839. IEEE, 2017. doi:10.1109/IROS.2017.8206234.
[26] Weilin Luo, Pingjia Liang, Jianfeng Du, Hai Wan, Bo Peng, and Delong Zhang. Bridging ltlf inference to GNN inference for learning ltlf formulae. In AAAI, pages 9849–9857. AAAI Press, 2022. doi:10.1609/AAAI.V36I9.21221.
[27] Corto Mascle, Nathanaël Fijalkow, and Guillaume Lagarde. Learning temporal formulas from examples is hard. CoRR, abs/2312.16336, 2023. doi:10.48550/arXiv.2312.16336.
[28] Sara Mohammadinejad, Jyotirmoy V. Deshmukh, Aniruddh Gopinath Puranic, Marcell Vazquez-Chanlatte, and Alexandre Donzé. 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, pages 9:1–9:10. ACM, 2020. doi:10.1145/3365365.3382218.
[29] Daniel Neider and Ivan Gavran. Learning linear temporal properties. In Nikolaj S. Bjørner and Arie Gurfinkel, editors, 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pages 1–10. IEEE, 2018. doi:10.23919/FMCAD.2018.8603016.
[30] Daniel Neider and Rajarshi Roy. What Is Formal Verification Without Specifications? A Survey on Mining LTL Specifications, pages 109–125. Springer Nature Switzerland, Cham, 2025. doi:10.1007/978-3-031-75778-5_6.
[31] C.H. Papadimitriou. Computational Complexity. Theoretical computer science. Addison-Wesley, 1994. URL: https://books.google.de/books?id=JogZAQAAIAAJ.
[32] Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. Synthesis of reactive(1) designs. In E. Allen Emerson and Kedar S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pages 364–380. Springer, 2006. doi:10.1007/11609773_24.
[33] Amir Pnueli. The temporal logic of programs. In Proc. 18th Annu. Symp. Found. Computer Sci., pages 46–57, 1977. doi:10.1109/SFCS.1977.32.
[34] Adrien Pommellet, Daniel Stan, and Simon Scatton. Sat-based learning of computation tree logic. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 366–385. Springer, 2024. doi:10.1007/978-3-031-63498-7_22.
[35] Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, and Daniel Neider. Scalable anytime algorithms for learning fragments of linear temporal logic. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 263–280, Cham, 2022. Springer International Publishing. doi:10.1007/978-3-030-99524-9_14.
[36] Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, Daniel Neider, and Guillermo A. Pérez. Synthesizing efficiently monitorable formulas in metric temporal logic. In VMCAI (2), volume 14500 of Lecture Notes in Computer Science, pages 264–288. Springer, 2024. doi:10.1007/978-3-031-50521-8_13.
[37] Heinz Riener. Exact synthesis of LTL properties from traces. In FDL, pages 1–6. IEEE, 2019. doi:10.1109/FDL.2019.8876900.
[38] Rajarshi Roy, Dana Fisman, and Daniel Neider. Learning interpretable models in the property specification language. In IJCAI, pages 2213–2219. ijcai.org, 2020. doi:10.24963/IJCAI.2020/306.
[39] Kristin Yvonne Rozier. Specification: The biggest bottleneck in formal methods and autonomy. In VSTTE, volume 9971 of Lecture Notes in Computer Science, pages 8–26, 2016. doi:10.1007/978-3-319-48869-1_2.
[40] Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, and Sanjit A. Seshia. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pages 1091–1096. IEEE, 2014. doi:10.1109/CDC.2014.7039527.
[41] Mojtaba Valizadeh, Nathanaël Fijalkow, and Martin Berger. LTL learning on gpus. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, volume 14683 of Lecture Notes in Computer Science, pages 209–231. Springer, 2024. doi:10.1007/978-3-031-65633-0_10.
[42] Hai Wan, Pingjia Liang, Jianfeng Du, Weilin Luo, Rongzhen Ye, and Bo Peng. End-to-end learning of ltlf formulae by faithful ltlf encoding. In AAAI, pages 9071–9079. AAAI Press, 2024. doi:10.1609/AAAI.V38I8.28757.
[43] Andrzej Wasylkowski and Andreas Zeller. Mining temporal specifications from object usage. Autom. Softw. Eng., 18(3-4):263–292, 2011. doi:10.1007/S10515-011-0084-1.

[bib.bib1] [1] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672–713, September 2002. doi:10.1145/585265.585270.

[bib.bib2] [2] Dana Angluin. On the complexity of minimum inference of regular sets. Inf. Control., 39(3):337–350, 1978. doi:10.1016/S0019-9958(78)90683-6.

[bib.bib3] [3] M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli. SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In FMCAD, pages 93–103. IEEE, 2020. doi:10.34727/2020/ISBN.978-3-85448-042-6_16.

[bib.bib4] [4] Ayca Balkan, Moshe Y. Vardi, and Paulo Tabuada. Mode-target games: Reactive synthesis for control applications. IEEE Trans. Autom. Control., 63(1):196–202, 2018. doi:10.1109/TAC.2017.2722960.

[bib.bib5] [5] Elwyn R. Berlekamp, Robert J. McEliece, and Henk C. A. van Tilborg. On the inherent intractability of certain coding problems (corresp.). IEEE Trans. Inf. Theory, 24(3):384–386, 1978. doi:10.1109/TIT.1978.1055873.

[bib.bib6] [6] Dines Bjørner and Klaus Havelund. 40 years of formal methods - some obstacles and some possibilities? In FM, volume 8442 of Lecture Notes in Computer Science, pages 42–61. Springer, 2014. doi:10.1007/978-3-319-06410-9_4.

[bib.bib7] [7] Giuseppe Bombara, Cristian-Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka, and Calin Belta. A decision tree approach to data classification using signal temporal logic. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC ’16, pages 1–10, New York, NY, USA, 2016. Association for Computing Machinery. doi:10.1145/2883817.2883843.

[bib.bib8] [8] Benjamin Bordais, Daniel Neider, and Rajarshi Roy. The complexity of learning temporal properties. CoRR, abs/2408.04486, 2024. doi:10.48550/arXiv.2408.04486.

[bib.bib9] [9] Benjamin Bordais, Daniel Neider, and Rajarshi Roy. Learning branching-time properties in CTL and ATL via constraint solving. In André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I, volume 14933 of Lecture Notes in Computer Science, pages 304–323. Springer, 2024. doi:10.1007/978-3-031-71162-6_16.

[bib.bib10] [10] Alberto Camacho, Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIlraith. LTL and beyond: Formal languages for reward function specification in reinforcement learning. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 6065–6073. ijcai.org, 2019. doi:10.24963/IJCAI.2019/840.

[bib.bib11] [11] Alberto Camacho and Sheila A. McIlraith. Learning interpretable models expressed in linear temporal logic. In ICAPS, pages 621–630. AAAI Press, 2019. URL: https://ojs.aaai.org/index.php/ICAPS/article/view/3529.

[bib.bib12] [12] Alberto Camacho, Eleni Triantafillou, Christian J. Muise, Jorge A. Baier, and Sheila A. McIlraith. Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces. In AAAI, pages 3716–3724. AAAI Press, 2017. doi:10.1609/AAAI.V31I1.11058.

[bib.bib13] [13] Alessio Cecconi, Giuseppe De Giacomo, Claudio Di Ciccio, Fabrizio Maria Maggi, and Jan Mendling. Measuring the interestingness of temporal logic behavioral specifications in process mining. Inf. Syst., 107:101920, 2022. doi:10.1016/J.IS.2021.101920.

[bib.bib14] [14] William Chan. Temporal-logic queries. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 450–463. Springer, 2000.

[bib.bib15] [15] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer, 1981. doi:10.1007/BFB0025774.

[bib.bib16] [16] Rüdiger Ehlers, Ivan Gavran, and Daniel Neider. Learning properties in LTL $\cap$ ACTL from positive examples only. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 104–112. IEEE, 2020. doi:10.34727/2020/ISBN.978-3-85448-042-6_17.

[bib.bib17] [17] Georgios E. Fainekos, Hadas Kress-Gazit, and George J. Pappas. Temporal logic motion planning for mobile robots. In ICRA, pages 2020–2025. IEEE, 2005. doi:10.1109/ROBOT.2005.1570410.

[bib.bib18] [18] Nathanaël Fijalkow and Guillaume Lagarde. The complexity of learning linear temporal formulas from examples. In Jane Chandlee, Rémi Eyraud, Jeff Heinz, Adam Jardine, and Menno van Zaanen, editors, Proceedings of the 15th International Conference on Grammatical Inference, 23-27 August 2021, Virtual Event, volume 153 of Proceedings of Machine Learning Research, pages 237–250. PMLR, 2021. URL: https://proceedings.mlr.press/v153/fijalkow21a.html.

[bib.bib19] [19] Marie Fortin, Boris Konev, Vladislav Ryzhikov, Yury Savateev, Frank Wolter, and Michael Zakharyaschev. Reverse engineering of temporal queries mediated by LTL ontologies. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 3230–3238. ijcai.org, 2023. doi:10.24963/IJCAI.2023/360.

[bib.bib20] [20] Jean-Raphaël Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu, and Zhe Xu. Maxsat-based temporal logic inference from noisy data. Innov. Syst. Softw. Eng., 18(3):427–442, 2022. doi:10.1007/S11334-022-00444-8.

[bib.bib21] [21] E. Mark Gold. Complexity of automaton identification from given data. Inf. Control., 37(3):302–320, 1978. doi:10.1016/S0019-9958(78)90562-4.

[bib.bib22] [22] Antonio Ielo, Mark Law, Valeria Fionda, Francesco Ricca, Giuseppe De Giacomo, and Alessandra Russo. Towards ilp-based ltlf passive learning. In Inductive Logic Programming: 32nd International Conference, ILP 2023, Bari, Italy, November 13–15, 2023, Proceedings, pages 30–45, Berlin, Heidelberg, 2023. Springer-Verlag. doi:10.1007/978-3-031-49299-0_3.

[bib.bib23] [23] Neil Immerman. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci., 22(3):384–406, 1981. doi:10.1016/0022-0000(81)90039-8.

[bib.bib24] [24] Jean Christoph Jung, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Extremal separation problems for temporal instance queries. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, pages 3448–3456. ijcai.org, 2024. URL: https://www.ijcai.org/proceedings/2024/382.

[bib.bib25] [25] Xiao Li, Cristian Ioan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC, Canada, September 24-28, 2017, pages 3834–3839. IEEE, 2017. doi:10.1109/IROS.2017.8206234.

[bib.bib26] [26] Weilin Luo, Pingjia Liang, Jianfeng Du, Hai Wan, Bo Peng, and Delong Zhang. Bridging ltlf inference to GNN inference for learning ltlf formulae. In AAAI, pages 9849–9857. AAAI Press, 2022. doi:10.1609/AAAI.V36I9.21221.

[bib.bib27] [27] Corto Mascle, Nathanaël Fijalkow, and Guillaume Lagarde. Learning temporal formulas from examples is hard. CoRR, abs/2312.16336, 2023. doi:10.48550/arXiv.2312.16336.

[bib.bib28] [28] Sara Mohammadinejad, Jyotirmoy V. Deshmukh, Aniruddh Gopinath Puranic, Marcell Vazquez-Chanlatte, and Alexandre Donzé. 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, pages 9:1–9:10. ACM, 2020. doi:10.1145/3365365.3382218.

[bib.bib29] [29] Daniel Neider and Ivan Gavran. Learning linear temporal properties. In Nikolaj S. Bjørner and Arie Gurfinkel, editors, 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pages 1–10. IEEE, 2018. doi:10.23919/FMCAD.2018.8603016.

[bib.bib30] [30] Daniel Neider and Rajarshi Roy. What Is Formal Verification Without Specifications? A Survey on Mining LTL Specifications, pages 109–125. Springer Nature Switzerland, Cham, 2025. doi:10.1007/978-3-031-75778-5_6.

[bib.bib31] [31] C.H. Papadimitriou. Computational Complexity. Theoretical computer science. Addison-Wesley, 1994. URL: https://books.google.de/books?id=JogZAQAAIAAJ.

[bib.bib32] [32] Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. Synthesis of reactive(1) designs. In E. Allen Emerson and Kedar S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pages 364–380. Springer, 2006. doi:10.1007/11609773_24.

[bib.bib33] [33] Amir Pnueli. The temporal logic of programs. In Proc. 18th Annu. Symp. Found. Computer Sci., pages 46–57, 1977. doi:10.1109/SFCS.1977.32.

[bib.bib34] [34] Adrien Pommellet, Daniel Stan, and Simon Scatton. Sat-based learning of computation tree logic. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 366–385. Springer, 2024. doi:10.1007/978-3-031-63498-7_22.

[bib.bib35] [35] Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, and Daniel Neider. Scalable anytime algorithms for learning fragments of linear temporal logic. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 263–280, Cham, 2022. Springer International Publishing. doi:10.1007/978-3-030-99524-9_14.

[bib.bib36] [36] Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, Daniel Neider, and Guillermo A. Pérez. Synthesizing efficiently monitorable formulas in metric temporal logic. In VMCAI (2), volume 14500 of Lecture Notes in Computer Science, pages 264–288. Springer, 2024. doi:10.1007/978-3-031-50521-8_13.

[bib.bib37] [37] Heinz Riener. Exact synthesis of LTL properties from traces. In FDL, pages 1–6. IEEE, 2019. doi:10.1109/FDL.2019.8876900.

[bib.bib38] [38] Rajarshi Roy, Dana Fisman, and Daniel Neider. Learning interpretable models in the property specification language. In IJCAI, pages 2213–2219. ijcai.org, 2020. doi:10.24963/IJCAI.2020/306.

[bib.bib39] [39] Kristin Yvonne Rozier. Specification: The biggest bottleneck in formal methods and autonomy. In VSTTE, volume 9971 of Lecture Notes in Computer Science, pages 8–26, 2016. doi:10.1007/978-3-319-48869-1_2.

[bib.bib40] [40] Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, and Sanjit A. Seshia. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pages 1091–1096. IEEE, 2014. doi:10.1109/CDC.2014.7039527.

[bib.bib41] [41] Mojtaba Valizadeh, Nathanaël Fijalkow, and Martin Berger. LTL learning on gpus. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, volume 14683 of Lecture Notes in Computer Science, pages 209–231. Springer, 2024. doi:10.1007/978-3-031-65633-0_10.

[bib.bib42] [42] Hai Wan, Pingjia Liang, Jianfeng Du, Weilin Luo, Rongzhen Ye, and Bo Peng. End-to-end learning of ltlf formulae by faithful ltlf encoding. In AAAI, pages 9071–9079. AAAI Press, 2024. doi:10.1609/AAAI.V38I8.28757.

[bib.bib43] [43] Andrzej Wasylkowski and Andreas Zeller. Mining temporal specifications from object usage. Autom. Softw. Eng., 18(3-4):263–292, 2011. doi:10.1007/S10515-011-0084-1.

The Complexity of Learning LTL, CTL and ATL Formulas

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

We summarize our contributions in Table 1.

Related Works.

2 Preliminaries and Definitions

2.1 Structures

Definition 1.

Definition 2.

2.2 ATL, CTL and LTL formulas

2.3 Learning decision problem

Definition 3.

Proposition 4.

2.4 Hitting set problem

Definition 5 (Hitting set problem).

3 Learning with unbounded use of binary operators

Theorem 6.

4 Learning with a bounded amount of binary operators

4.1 Expressivity

4.2 Abstract recipes

Recipe for the membership-below-NP proofs.

Recipe for the NP-hardness proofs.

4.3 LTL learning

Proposition 7.

Observation 8.

Corollary 9.

Proof sketch.

4.4 CTL learning

Assume that 𝐗∈𝗨𝘁.

Theorem 10.

Lemma 11.

Proof sketch.

Definition 12.

Lemma 13.

Lemma 14.

Proof sketch.

Assume that 𝐗∉𝗨𝘁.

Theorem 15.

Lemma 16.

Proof sketch.

Proof of NL-hardness.

4.5 ATL learning

Definition 17.

Lemma 18.

𝗔𝗧𝗟𝟐 learning with {𝐅,𝐆}⊆𝗨𝘁.

Theorem 19.

Lemma 20.

Proof.

Lemma 21.

Proof sketch.

Definition 22.

Lemma 23.

Proof sketch.

Lemma 24.

𝗔𝗧𝗟𝟐 learning with 𝗨𝘁={𝐅} or 𝗨𝘁={𝐆}.

Theorem 25.

Definition 26.

Lemma 27.

Proof of P-hardness.

𝗔𝗧𝗟𝟑 learning with 𝗨𝘁∈{{𝐅},{𝐆}}.

Theorem 28.

Definition 29.

Lemma 30.

Lemma 31.

5 Future Work

References

Assume that $\operatorname{\mathbf{X}}\in\mathsf{U}^{\mathsf{t}}$ .

Assume that $\operatorname{\mathbf{X}}\notin\mathsf{U}^{\mathsf{t}}$ .

$\mathsf{ATL}^{2}$ learning with $\{\operatorname{\mathbf{F}},\operatorname{\mathbf{G}}\}\subseteq\mathsf{U}^{% \mathsf{t}}$ .

$\mathsf{ATL}^{2}$ learning with $\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{F}}\}$ or $\mathsf{U}^{\mathsf{t}}=\{\operatorname{\mathbf{G}}\}$ .

$\mathsf{ATL}^{3}$ learning with $\mathsf{U}^{\mathsf{t}}\in\{\{\operatorname{\mathbf{F}}\},\{\operatorname{% \mathbf{G}}\}\}$ .