# Learning temporal formulas from examples is hard††thanks: This article is a
long version of the article presented in the proceedings of the International
Conference on Grammatical Inference (ICGI) in 2021 (?). It includes much
stronger and more general results than the extended abstract.

Corto Mascle<EMAIL_ADDRESS>
LaBRI, University of Bordeaux, France Nathanaël Fijalkow
<EMAIL_ADDRESS>
CNRS, LaBRI, Université de Bordeaux, France Guillaume Lagarde
<EMAIL_ADDRESS>
LaBRI, University of Bordeaux, France

###### Abstract

We study the problem of learning linear temporal logic (LTL) formulas from
examples, as a first step towards expressing a property separating positive
and negative instances in a way that is comprehensible for humans. In this
paper we initiate the study of the computational complexity of the problem.
Our main results are hardness results: we show that the LTL learning problem
is $\NP$-complete, both for the full logic and for almost all of its
fragments. This motivates the search for efficient heuristics, and highlights
the complexity of expressing separating properties in concise natural
language.

##  1 Introduction

We are interested in the complexity of learning formulas of Linear Temporal
Logic (LTL) from examples, in a passive scenario: from a set of positive and
negative words, the objective is to construct a formula, as small as possible,
which satisfies the positive words and does not satisfy the negative words.
Passive learning of languages has a long history paved with negative results.
Learning automata is notoriously difficult from a theoretical perspective, as
witnessed by the original $\NP$-hardness result of learning a Deterministic
Finite Automaton (DFA) from examples (?). This line of hardness results
culminates with the inapproximability result of (?) stating that there is no
polynomial time algorithm for learning a DFA from examples even up to a
polynomial approximation of their size.

One approach to cope with such hardness results is to change representation,
for instance replacing automata by logical formulas; their syntactic
structures make them more amenable to principled search algorithms. There is a
range of potential logical formalisms to choose from depending on the
application domain. Linear Temporal Logic (?), which we abbreviate as LTL, is
a prominent logic for specifying temporal properties over words, it has become
a de facto standard in many fields such as model checking, program analysis,
and motion planning for robotics. Verification of LTL specifications is
routinely employed in industrial settings and marks one of the most successful
applications of formal methods to real-life problems. A key property making
LTL a strong candidate as a concept class is that its syntax does not include
variables, contributing to the fact that LTL formulas are typically easy to
interpret and therefore useful as explanations.

Over the past five to ten years learning temporal logics (of which LTL is the
core) has become an active research area. There are many applications, let us
only mention a few: program specification (?) and fault detections (?). We
refer to (?) for a longer discussion on the potential and actual applications
of learning temporal logics.

Since learning temporal logics is a computationally hard problem, a number of
different approaches have been explored. One of the first and probably most
natural is leveraging SAT solvers (?), which can then accommodate noisy data
(?). Another line of work relies on their connections to automata (?), and a
third completely different idea approaches it from the lens of Bayesian
inference (?). Learning specifically tailored fragments of LTL yields the best
results in practice (?). There are a number of temporal logics, and the ideas
mentioned above have been extended to more expressive logics such as Property
Specification Language (PSL) (?, ?), Computational Tree Logic (CTL) (?), and
Metric Temporal Logic (MTL) (?). Other paradigms have been explored to make
learning temporal logics useful, such as sketching (?).

Despite this growing interest, very little is known about the computational
complexity of the underlying problem; indeed the works cited above focused on
constructing efficient algorithms for practical applications. The goal of this
paper is to initiate the study of the complexity of learning LTL formulas from
examples.

Our contributions. We present a set of results for several fragments of LTL,
showing in almost all cases that the learning problem is $\NP$-complete.
Section 2 gives definitions.

  * •

Our first $\NP$-hardness result is presented in Section 3, it states that the
learning problem for full LTL is $\NP$-hard when the alphabet size is part of
the input.

  * •

To obtain membership in $\NP$ for the learning problem, we show in Section 4
that all fragments of LTL have the short formula property. We then study some
(degenerate) fragments in Section 5 and show that for these fragments the LTL
learning problem is in polynomial time.

  * •

We construct in Section 6 a polynomial-time approximation algorithm for LTL
with only the next operator and conjunctions, and show that assuming
$\P\neq\NP$, the approximation ratio of this algorithm is optimal.

  * •

Our most technical results are presented in Section 7 and Section 8: in the
first section we show that almost all fragments with the next operator are
hard to approximate, and in the next a similar result for almost all fragments
without the next operator.

We conclude in Section 9.

##  2 Preliminaries

Let us fix a (finite) alphabet $\Sigma$. We index words from position $1$ (not
$0$) and the letter at position $i$ in the word $w$ is written $w(i)$, so
$w=w(1)\dots w(\ell)$ where $\ell$ is the length of $w$, written $|w|=\ell$.
We write $w[k\dots]=w(k)\dots w(\ell)$. To avoid unnecessary technical
complications we only consider non-empty words, and let $\Sigma^{+}$ denote
the set of (non-empty) words.

The syntax of Linear Temporal Logic (LTL) includes atomic formulas
$c\in\Sigma$ and their negations, as well as $\top$ and $\bot$, the boolean
operators $\wedge$ and $\vee$, and the temporal operators
$\textbf{X},\textbf{F}$, G, and U. Note that as usually done, we work with LTL
in negation normal form, meaning that negation is only used on atomic
formulas. The semantic of LTL over finite words is defined inductively over
formulas, through the notation $w\models\varphi$ where $w\in\Sigma^{+}$ is a
non-empty word, and $\varphi$ is an LTL formula. The definition is given below
for the atomic formulas and temporal operators
$\textbf{U},\textbf{F},\textbf{G}$, and X, with boolean operators interpreted
as usual.

  * •

We have $w\models\top$ and $w\not\models\bot$.

  * •

$w\models c$ if $w(1)=c$.

  * •

$w\models\textbf{X}\varphi$ if $|w|>1$ and $w[2\dots]\models\varphi$. It is
called the next operator.

  * •

$w\models\textbf{F}\varphi$ if $w[i\dots]\models\varphi$ for some
$i\in[1,|w|]$. It is called the eventually operator.

  * •

$w\models\textbf{G}\varphi$ if $w[i\dots]\models\varphi$ for all
$i\in[1,|w|]$. It is called the globally operator.

  * •

$w\models\varphi\textbf{U}\psi$ if there exists $i\in[1,|w|]$ such that for
$j\in[1,i-1]$ we have $w[j\dots]\models\varphi$, and $w[i\dots]\models\psi$.
It is called the until operator.

Note that $\textbf{F}\varphi$ is syntactic sugar for $\top\textbf{U}\varphi$.
We say that $w$ satisfies $\varphi$ when $w\models\varphi$ is true. It is
sometimes useful to write $w,i\models\varphi$ to mean
$w[i\dots]\models\varphi$. We consider fragments of LTL by specifying which
boolean connectives and temporal operators are allowed. For instance
$\textbf{LTL}(\textbf{X},\wedge)$ is the set of all LTL formulas using only
atomic formulas, conjunctions, and the next operator. The full logic is
$\textbf{LTL}=\textbf{LTL}(\textbf{U},\textbf{F},\textbf{G},\textbf{X},\land,\lor)$.
More generally, for a set of operators
$Op\subseteq\left\\{\textbf{U},\textbf{F},\textbf{G},\textbf{X},\land,\lor\right\\}$,
we write $\textbf{LTL}(Op)$ for the logic using operators from $Op$. The size
of a formula is the size of its syntactic tree. We say that two formulas are
equivalent if they have the same semantics, and we write $\varphi\equiv\psi$
to say that $\varphi$ and $\psi$ are equivalent.

#### The LTL learning problem.

A sample is a pair $(P,N)$ where $P=\left\\{u_{1},\dots,u_{n}\right\\}$ is a
set of positive words and $N=\left\\{v_{1},\dots,v_{m}\right\\}$ a set of
negative words. Without loss of generality we can assume that $n=m$ (adding
duplicate identical words to have an equal number of positive and negative
words). The LTL learning decision problem is:

INPUT: | a sample $(P,N)$ and $k\in\mathbb{N}$,
---|---
QUESTION: | does there exist an LTL formula $\varphi$ of size at most $k$
| such that for all $u\in P$, we have $u\models\varphi$,
| and for all $v\in N$, we have $v\not\models\varphi$?

In that case we say that $\varphi$ separates $P$ from $N$, or simply that
$\varphi$ is a separating formula if the sample is clear from the context. The
LTL learning problem is analogously defined for any fragment of LTL.

#### Parameters for complexity analysis.

The three important parameters for the complexity of the LTL learning problem
are: $n$ the number of words, $\ell$ the maximum length of the words, and $k$
the desired size for the formula. As we will see, another important parameter
is the size of the alphabet. We will consider two settings: either the
alphabet $\Sigma$ is fixed, or it is part of the input. The size of the
alphabet is $|\Sigma|$, the number of letters.

#### Representation.

The words given as input are represented in a natural way: we work with the
RAM model with word size $\log(|\Sigma|+n+\ell)$, which allows us to write a
letter in each cell and to manipulate words and positions in a natural way. We
write $|P|$ for $\sum_{j\in[1,n]}|u_{j}|$ and similarly
$N=\sum_{j\in[1,n]}|v_{j}|$. The size of a sample is $|P|+|N|$.

We emphasise a subtlety on the representation of $k$: it can be given in
binary (a standard assumption) or in unary. In the first case, the input size
is $O(n\cdot\ell+\log(k))$, so the formula $\varphi$ we are looking for may be
exponential in the input size! This means that it is not clear a priori that
the LTL learning problem is in $\NP$. Opting for a unary encoding, the input
size becomes $O(n\cdot\ell+k)$, and in that case an easy argument shows that
the LTL learning problem is in $\NP$. We follow the standard representation:
$k$ is given in binary, and therefore it is not immediate that the LTL
learning problem is in $\NP$.

#### A naive algorithm.

Let us start our complexity analysis of the learning LTL problem by
constructing a naive algorithm for the whole logic.

######  Theorem 1.

There exists an algorithm for solving the LTL learning problem in time and
space $O(|\Sigma|+\text{exp}(k)\cdot n\cdot\ell)$, where $\text{exp}(k)$ is
exponential in $k$.

Notice that the dependence of the algorithm presented in Theorem 1 is linear
in $n$ and $\ell$, and it is exponential only in $k$, but since $k$ is
represented in binary this is a doubly-exponential algorithm.

###### Proof.

For a formula $\varphi\in\textbf{LTL}$, we write $\langle\varphi\rangle:P\cup
N\to\left\\{0,1\right\\}^{\ell}$ for the function defined by

$\langle\varphi\rangle(w)(i)=\begin{cases}1&\text{ if
}w[i\dots]\models\varphi,\\\ 0&\text{ if
}w[i\dots]\not\models\varphi,\end{cases}$

for $w\in P\cup N$.

Note that $\varphi$ is separating if and only if
$\langle\varphi\rangle(u)(1)=1$ and $\langle\varphi\rangle(v)(1)=0$ for all
$u\in P,v\in N$. The algorithm simply consists in enumerating all formulas
$\varphi$ of LTL of size at most $k$ inductively, constructing
$\langle\varphi\rangle$, and checking whether $\varphi$ is separating.
Initially, we construct $\langle a\rangle$ for all $a\in\Sigma$, and then once
we have computed $\langle\varphi\rangle$ and $\langle\psi\rangle$, we can
compute $\langle\varphi\textbf{U}\psi\rangle$,
$\langle\textbf{F}\varphi\rangle$, $\langle\textbf{G}\varphi\rangle$,
$\langle\textbf{X}\varphi\rangle$, $\langle\varphi\wedge\psi\rangle$, and
$\langle\varphi\vee\psi\rangle$ in time $O(n\cdot\ell)$. To conclude, we note
that the number of formulas of LTL of size at most $k$ is exponential in $k$.
∎

### Subwords

Let $u=u(1)\dots u(\ell)$ and $w=w(1)\dots w(\ell^{\prime})$. We say that

  * •

$u$ is a _subword_ of $w$ if there exist $p_{1}<\dots<p_{\ell}$ such that
$u(i)=w(p_{i})$ for all $i\in[1,\ell]$.

  * •

$u$ is a _weak subword_ of $w$ if there exist $p_{1}\leq\dots\leq p_{\ell}$
such that $u(i)=w(p_{i})$ for all $i\in[1,\ell]$.

For instance, $abba$ is a subword of $b\textbf{ab}aaaa\textbf{b}\textbf{a}$,
and $bba$ is a weak subword of $a\textbf{ba}a$ (using the $b$ twice). We say
that a word is non-repeating if every two consecutive letters are different.
If $u$ is non-repeating, then $u$ is a weak subword of $w$ if and only if it
is a subword of $w$.

As a warm-up, let us construct simple LTL formulas related to subwords.

  * •

We consider the word $u=u(1)\dots u(\ell)$ and $p_{1}<p_{2}<\dots<p_{\ell}$.
They induce the following $\textbf{LTL}(\textbf{X},\land)$ formula, called a
pattern:

$\mathcal{P}=\textbf{X}^{p_{1}-1}(u(1)\wedge\textbf{X}^{p_{2}-i_{1}}(\cdots\wedge\textbf{X}^{p_{\ell}-p_{\ell-1}}u(\ell))\cdots).$

It is equivalent to the (larger in size) formula
$\bigwedge_{i\in[1,\ell]}\textbf{X}^{p_{i}-1}u(i)$, which states that for each
$i\in[1,\ell]$, the letter in position $p_{i}$ is $u(i)$.

  * •

We consider the word $u=u(1)\dots u(\ell)$. It induces the following
$\textbf{LTL}(\textbf{F},\land)$ formula, called a fattern (pattern with an
F):

$\mathcal{F}=\textbf{F}(u(1)\wedge\textbf{F}(\cdots\wedge\textbf{F}u(\ell))\cdots).$

A word $w$ satisfies $\mathcal{F}$ if and only if $u$ is a weak subword of
$w$.

##  3 NP-hardness when the alphabet is part of the input

We prove our first hardness result: the learning problem for LTL is $\NP$-hard
for non-constant alphabets for all fragments including F and $\lor$, so in
particular for full LTL.

######  Theorem 2.

For all $\left\\{\textbf{F},\lor\right\\}\subseteq Op$, the $\textbf{LTL}(Op)$
learning problem is $\NP$-hard when the alphabet is part of the input.

Recall that the hitting set problem takes as input $C_{1},\dots,C_{n}$ subsets
of $[1,\ell]$ and $k\in\mathbb{N}$, and asks whether there exists
$H\subseteq[1,\ell]$ of size at most $k$ such that for every $j\in[1,n]$ we
have $H\cap C_{j}\neq\emptyset$. It is known to be -complete.

###### Proof.

We construct a reduction from the hitting set problem. Let
$C_{1},\dots,C_{n}\subseteq[1,\ell]$ and $k\in\mathbb{N}$ an instance of the
hitting set problem. Let us define the alphabet
$\Sigma=\left\\{a_{j},b_{j}:j\in[1,n]\right\\}$, it has size $2n$. For
$j\in[1,n]$, we define $u_{j}$ of length $\ell$ by

$u_{j}(i)=\begin{cases}a_{j}\text{ if }i\in C_{j},\\\ b_{j}\text{
otherwise}.\end{cases}$

Let $v=b_{1}\cdots b_{n}$. We claim that there exists a hitting set $H$ of
size at most $k$ if and only if there exists a separating formula of LTL of
size at most $2k$.

Given a hitting set $H$ of size $k$, we construct the formula
$\textbf{F}(\bigvee_{j\in H}a_{j})$, it is separating by definition of $H$
being a hitting set, and it has size $2k$. Conversely, let us consider a
separating formula $\varphi$ of size $2k$. Since all operators have arity one
or two, the syntactic tree of $\varphi$ contains at most $k$ leaves, so the
set $H=\left\\{j\in[1,\ell]:a_{j}\text{ appears in }\varphi\right\\}$ has size
at most $k$. Suppose $H$ is not a hitting set of $C_{1},\ldots,C_{n}$, there
exists $j\in[1,n]$ such that $H\cap C_{j}=\emptyset$. We prove that for all
subformulas $\psi$ of $\varphi$ and for all $i\in[1,\ell]$, if
$u_{j}[i\dots]\vDash\psi$ then $v[j\dots]\vDash\psi$. We proceed by induction.

  * •

If $\psi$ is a letter. If $u_{j}[i\dots]\vDash\psi$, this implies that
$u_{j}(i)=b_{j}$ because $a_{j}$ cannot appear in both $\psi$ and $u_{j}$
since $H\cap C_{j}=\emptyset$. Remark that $v(i)=b_{i}$, so
$v[i\dots]\vDash\psi$.

  * •

The other cases are easily proved by applying directly the induction
hypothesis.

In particular, since $u_{j}$ satisfies $\varphi$, then so does $v$, a
contradiction with $\varphi$ being separating. ∎

This could be the end of our study! However the assumption that the alphabet
is part of the input is very unusual, and in the rest of the paper we will
therefore fix the alphabet size. In the remainder of the paper, we will
consider only fragments of LTL without the until operator. In other words,
when consider $Op$ a set of operators, we assume that
$Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X},\land,\lor\right\\}$.

##  4 Membership in NP: the short formula property

######  Definition 1.

Let $Op$ a set of operator, we say that $Op$ has the _short formula property_
if there exists a polynomial P such that for all samples $(P,N)$, if there
exists an LTL(Op) separating formula, then there exists one of size at most
$\textbf{P}(|P|+|N|)$.

Note that if $Op$ has the short formula property then the $\textbf{LTL}(Op)$
learning problem is in $\NP$.

######  Theorem 3.

All $Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X},\land,\lor\right\\}$
have the short formula property, and therefore the $\textbf{LTL}(Op)$ learning
problem is in $\NP$.

This theorem is the consequence of the following propositions, which establish
it for various subsets of operators. We start with some technical lemmas. The
following lemma is easily proved by induction, it shows that LTL cannot detect
repetitions in the last letter of a word.

######  Lemma 1.

Let $u$ whose last letter is $a$. For all formulas $\varphi\in\textbf{LTL}$,
for all $k\in\mathbb{N}$, if $u$ satisfies $\varphi$ then $ua^{k}$ satisfies
$\varphi$.

######  Lemma 2.

If a formula of the form
$\varphi=\textbf{F}(\psi_{1}\land\textbf{F}(\psi_{2}\land\left(\dots\land\textbf{F}\psi_{r}\right)\dots)$
is not satisfied by some word $v$ then there exist $i_{1}<\dots<i_{k}$ with
$k\leq|v|+1$ such that $v$ does not satisfy
$\psi=\textbf{F}(\psi_{i_{1}}\land\textbf{F}(\psi_{i_{2}}\land\left(\dots\land\textbf{F}\psi_{i_{k}}\right)\dots)$
but all words satisfying $\varphi$ also satisfy $\psi$.

###### Proof.

We set $v_{1}=v$. For all $i\in[2,r]$ we set $v_{i}$ as the largest suffix of
$v_{i-1}$ satisfying $\psi_{i}$. If this suffix does not exist, we set
$v_{i}=\varepsilon$. As $v$ does not satisfy $\varphi$, we easily obtain that
for all $i<r$ $v_{i}$ does not satisfy
$\textbf{F}(\psi_{i}\land\textbf{F}(\psi_{i+1}\land\dots\land\textbf{F}\psi_{r})\dots)$.
Hence $v_{r-1}$ does not satisfy $\textbf{F}\psi_{r}$ and thus
$v_{r}=\varepsilon$. We can now extract a decreasing subsequence of suffixes
$v_{i_{1}},\ldots,v_{i_{k}}$ with $i_{1}=1$ and for all $j>1$, $i_{j}$ is the
smallest index larger than $i_{j-1}$ such that $v_{i_{j}}\neq v_{i_{j-1}}$ if
it exists. Note that as this sequence is decreasing $k$ cannot be larger than
$|v|+1$. We set
$\psi=\textbf{F}(\psi_{i_{1}}\land\textbf{F}(\psi_{i_{2}}\land\dots\land\textbf{F}\psi_{i_{k}})\dots)$.
We have that for all $j>1$, $v_{i_{j}}$ is the largest suffix of $v_{i_{j-1}}$
satisfying $\psi_{i_{j}}$, and $v_{i_{k}}=\varepsilon$. It is then easy to
infer by reverse induction on $j$ that for all $j$, $v_{i_{j}}$ does not
satisfy
$\textbf{F}(\psi_{i_{j}}\land\textbf{F}(\psi_{i_{j+1}}\land\dots\land\textbf{F}\psi_{i_{k}})\dots)$
and thus that in particular $v_{i_{1}}=v$ does not satisfy $\psi$.

Let $u$ be a word satisfying $\varphi$, there is a non-increasing sequence of
suffixes $u_{i}$ of $u$ such that $u_{1}=u$ and each $u_{i}$ satisfies
$\textbf{F}(\psi_{i}\land\textbf{F}(\psi_{i+1}\land\dots\land\textbf{F}\psi_{r})\dots)$.
It is then easy to see, by reverse induction on $j$, that for each $j\in[1,k]$
$u_{i_{j}}$ satisfies
$\textbf{F}(\psi_{i_{j}}\land\textbf{F}(\psi_{i_{j+1}}\land\dots\land\textbf{F}\psi_{i_{k}})\dots)$.
In particular $u_{1}=u$ satisfies $\psi$. ∎

We state and prove a dual version.

######  Lemma 3.

If a formula of the form
$\varphi=\textbf{G}(\psi_{1}\lor\textbf{G}(\psi_{2}\lor\dots\lor\textbf{G}\psi_{r})\dots)$
is satisfied by some word $u$ then there exist $i_{1}<\dots<i_{k}$ with
$k\leq|u|+1$ such that $u$ satisfies
$\psi=\textbf{G}(\psi_{i_{1}}\lor\textbf{G}(\psi_{i_{2}}\lor\dots\lor\textbf{G}\psi_{i_{k}})\dots)$
and all words satisfying $\psi$ also satisfy $\varphi$.

###### Proof.

Let us momentarily use negation. Note that the proof of Lemma 2 still holds
when we allow negations. The word $u$ does not satisfy
$\varphi^{\prime}=\textbf{F}(\neg\psi_{1}\land\textbf{F}(\neg\psi_{2}\lor\dots\land\textbf{F}\neg\psi_{r})\dots)$
as it is equivalent to the negation of $\varphi$, thus there exist
$i_{1}<\ldots<i_{k}$ with $k\leq|u|+1$ such that $u$ does not satisfy
$\psi^{\prime}=\textbf{F}(\psi_{i_{1}}\land\textbf{F}(\psi_{i_{2}}\land\dots\land\textbf{F}\psi_{i_{k}})\dots)$
but all words satisfying $\varphi^{\prime}$ satisfy $\psi^{\prime}$. The
formula
$\psi=\textbf{G}(\psi_{i_{1}}\lor\textbf{G}(\psi_{i_{2}}\lor\dots\lor\textbf{G}\psi_{i_{k}})\dots)$
is equivalent to the negation of $\psi^{\prime}$, thus it is satisfied by $u$,
and all words satisfying $\psi$ satisfy $\varphi$. ∎

The following fact will be useful for obtaining weak normal forms.

######  Fact 1.

For all formulas $\varphi,\psi,\varphi_{1},\ldots,\varphi_{n}\in\textbf{LTL}$,
the following equivalences hold:

  1. 1.

$\textbf{G}\textbf{G}\varphi\equiv\textbf{G}\varphi$ and
$\textbf{F}\textbf{F}\varphi\equiv\textbf{F}\varphi$.

  2. 2.

$\textbf{X}(\varphi\land\psi)\equiv\textbf{X}\varphi\land\textbf{X}\psi$ and
$\textbf{X}(\varphi\lor\psi)\equiv\textbf{X}\varphi\lor\textbf{X}\psi$.

  3. 3.

$\textbf{G}\textbf{X}\varphi\equiv\bot$ and
$\textbf{F}\textbf{X}\varphi\equiv\textbf{X}\textbf{F}\varphi$.

  4. 4.

$\textbf{G}\textbf{F}\varphi\equiv\textbf{F}\textbf{G}\varphi$ (both state
that $\psi$ is satisfied on the last position)

  5. 5.

$\textbf{G}(\varphi\land\psi)\equiv\textbf{G}\varphi\land\textbf{G}\psi$ and
$\textbf{F}(\varphi\lor\psi)\equiv\textbf{F}\varphi\lor\textbf{F}\psi$.

  6. 6.

$\textbf{F}(\psi\land\bigwedge_{i=1}^{n}\textbf{F}\varphi_{i})\equiv\bigwedge_{i=1}^{n}\textbf{F}(\psi\land\textbf{F}\varphi_{i})$
and
$\textbf{G}(\psi\lor\bigvee_{i=1}^{n}\textbf{G}\varphi_{i})\equiv\bigvee_{i=1}^{n}\textbf{G}(\psi\lor\textbf{G}\varphi_{i})$.

######  Proposition 1.

All $Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X},\land\right\\}$ have
the short formula property.

###### Proof.

Let us consider a formula $\varphi$ separating $P$ from $N$ in
$\textbf{LTL}(Op)$, we apply a series of transformations to $\varphi$ to
construct another separating formula of polynomial size.

First of all we push the G in front of the letters, which is possible by using
repeatedly the equivalences 1, 3, 4 and 5 of Fact 1. Then we push the X to the
bottom of the formula as well, as they commute with F and $\land$. We obtain a
$\textbf{LTL}(\textbf{F},\land)$ formula with atoms of the form either
$\textbf{X}^{k}\textbf{G}a$ or $\textbf{X}^{k}a$. Once that is done, we make
the formula follow a normal form by repeatedly using equivalence 6 of Fact 1.
While $\varphi$ has a subformula of the form
$\textbf{F}(\psi\land\bigwedge_{i=1}^{p}\textbf{F}\varphi_{i})$, we turn it
into $\bigwedge_{i=1}^{p}\textbf{F}(\psi\land\textbf{F}\varphi_{i})$. In the
end $\varphi$ is of the form $\psi\land\bigwedge_{i=1}^{p}\varphi_{i}$ with
each $\varphi_{i}$ of the form
$\textbf{F}(\psi_{1}\land\textbf{F}(\psi_{2}\land\dots\land\textbf{F}\psi_{r})\dots)$
where $\psi$ and the $\psi_{i}$ are conjunctions of formulas of the form
$\textbf{X}^{k}\textbf{G}a$ or $\textbf{X}^{k}a$. Note that $p$ may be
exponential in $|\varphi|$.

Observe that given two formulas $\alpha$ and $\beta$ of the form either $a$ or
$\textbf{G}a$ for some $a\in\Sigma$,
$\textbf{X}^{k}\alpha\land\textbf{X}^{k}\beta$ is equivalent to either
$\textbf{X}^{k}\alpha$, $\textbf{X}^{k}\beta$, or $\bot$. It is then easy to
see that every conjunction of formulas of the form $\textbf{X}^{k}\textbf{G}a$
or $\textbf{X}^{k}a$ is equivalent over non-empty words of length at most
$\ell$ to either $\bot$ or a conjunction of at most $\ell$ formulas of the
form $\textbf{X}^{k}a$ or $\textbf{X}^{k}\textbf{G}a$ with $k<\ell$. We can
thus assume $\psi$ and all $\psi_{i}$ to be of that form, and thus to be of
size polynomial in $\ell$.

This formula being equivalent to $\varphi$, all $u_{i}$ satisfy all
$\varphi_{r}$ and $\psi$, and for all $v_{j}$ either $v_{j}$ does not satisfy
$\psi$ or it does not satisfy some $\varphi_{r}$. We focus on the second case.
Say $v_{j}$ does not satisfy
$\varphi_{r}=\textbf{F}(\psi_{1}\land\textbf{F}(\psi_{2}\land\dots\land\textbf{F}\psi_{s})\dots)$,
by Lemma 2 we can turn $\varphi_{\ell}$ into a short formula
$\varphi^{\prime}_{j}$ that is still satisfied by all $u_{i}$ but not by
$v_{j}$. We set $\varphi^{\prime}_{j}$ to be as described above for all
$v_{j}$ that satisfy $\psi$ and to be $\psi$ for the others. As a result, the
formula $\bigwedge_{i=1}^{m}\varphi^{\prime}_{j}$ is a formula of polynomial
size in $m$ and $\ell$ separating the $u_{i}$ and $v_{j}$.

Furthermore, we did not add any operators to the formula, hence the final
formula uses the same set of operators as $\varphi$. ∎

######  Proposition 2.

All $Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X},\lor\right\\}$ have
the short formula property.

###### Proof.

The proof is nearly identical to the one of Proposition 1. We start by pushing
the F and X to the bottom of the formula to obtain a formula of
$\textbf{LTL}(\textbf{G},\lor)$ with atoms of the form $\textbf{X}^{k}a$ or
$\textbf{X}^{k}\textbf{F}a$. We also use repeatedly equivalence 6 of Fact 1 to
obtain a formula of the form $\psi\lor\bigvee_{i=1}^{p}\varphi_{i}$ with each
$\varphi_{i}$ of the form
$\textbf{G}(\psi_{1}\lor\textbf{G}(\psi_{2}\lor\dots\lor\textbf{G}\psi_{r})\dots)$
where $\psi$ and the $\psi_{i}$ are disjunctions of formulas of the form
$\textbf{X}^{k}\textbf{F}a$ or $\textbf{X}^{k}a$. Then we note that every
disjunction of formulas of the form $\textbf{X}^{k}a$ and
$\textbf{X}^{k}\textbf{F}a$ can be replaced by a disjunction of at most
$\ell|\Sigma|$ such formulas, equivalent on non-empty words of length at most
$\ell$ (as $\textbf{X}^{k}\textbf{F}a\lor\textbf{X}^{k}a$ is equivalent to
$\textbf{X}^{k}\textbf{F}a$). We can thus assume that all $\psi_{i}$ and
$\psi$ mentioned above are of polynomial size in $\ell$ and $|\Sigma|$. No
$v_{j}$ satisfies either $\psi$ or any $\psi_{r}$. For each $u_{i}$ either
there exists $\varphi_{r}$ that is satisfied by $u_{i}$ or $u_{i}$ satisfies
$\psi$. In the first case we use Lemma 3 to turn that $\varphi_{r}$ into a
formula $\varphi^{\prime}_{i}$ of polynomial size in $\ell$ and $|\Sigma|$
satisfied by $u_{i}$ but not by any $v_{j}$. If $u_{i}$ does not satisfy any
$\varphi_{r}$ we set $\varphi^{\prime}_{i}=\psi$. In the end the formula
$\bigvee_{i=1}^{n}\varphi^{\prime}_{i}$ is satisfied by all $u_{i}$ but no
$v_{j}$, and is of polynomial size in $\ell$, $n$ and $|\Sigma|$. ∎

######  Proposition 3.

All $\left\\{\textbf{G},\textbf{X},\land,\lor\right\\}\subseteq Op$ have the
short formula property.

###### Proof.

Let $(P,N)$ a sample. Consider the formula
$\varphi=\bigvee_{i=1}^{n}\varphi_{u_{i}}$ where
$\varphi_{u_{i}}=\bigwedge_{j=1}^{m-1}\textbf{X}^{j-1}a_{j}\land\textbf{X}^{m-1}\textbf{G}a_{m}$
with $u_{i}=a_{1}\cdots a_{m}$. If there exist $u_{i},v_{j}$ such that
$v_{j}\in u_{i}a^{*}$ with $a$ the last letter of $u_{i}$, then there is no
separating formula: By Lemma 1 every formula satisfied by $u_{i}$ is also
satisfied by $v_{j}$. Otherwise, every $u_{i}$ satisfies the associated
formula $\varphi_{u_{i}}$ while no $v_{j}$ satisfies any of them. Hence
$\varphi$ is a separating formula of polynomial size. ∎

######  Proposition 4.

All $Op$ such that $\left\\{\textbf{X},\land,\lor\right\\}\subseteq
Op\subseteq\left\\{\textbf{F},\textbf{X},\land,\lor\right\\}$ have the short
formula property.

###### Proof.

Let $(P,N)$ a sample. Consider the formula
$\varphi=\bigvee_{i=1}^{n}\varphi_{u_{i}}$ where
$\varphi_{u_{i}}=\bigwedge_{j=1}^{m}\textbf{X}^{j-1}a_{j}$ with
$u_{i}=a_{1}\cdots a_{m}$. We distinguish two cases.

  * •

If there exist $u_{i},v_{j}$ such that $u_{i}$ is a prefix of $v_{j}$, then
there is no separating formula: An easy induction shows that every formula
satisfied by $u_{i}$ is also satisfied by $v_{j}$.

  * •

Otherwise, every $u_{i}$ satisfies the associated formula $\varphi_{u_{i}}$
while no $v_{j}$ satisfies any of them. Hence $\varphi$ is a separating
formula of polynomial size.

∎

######  Fact 2.

For all
$\varphi,\varphi_{1},\varphi_{2}\in\textbf{LTL}(\textbf{F},\textbf{G},\land,\lor,\neg)$,
the following equivalences hold:

  * •

$\neg(\varphi_{1}\land\varphi_{2})\equiv\neg\varphi_{1}\lor\neg\varphi_{2}$

  * •

$\neg(\varphi_{1}\lor\varphi_{2})\equiv\neg\varphi_{1}\land\neg\varphi_{2}$

  * •

$\neg\textbf{F}\varphi\equiv\textbf{G}\neg\varphi$

  * •

$\neg\textbf{G}\varphi\equiv\textbf{F}\neg\varphi$

######  Proposition 5.

$\left\\{\textbf{F},\land,\lor\right\\}$ and
$\left\\{\textbf{G},\land,\lor\right\\}$ have the short formula property.

###### Proof.

Let $(P,N)$ a sample. Let $j\in[1,n]$, if there exists $w_{j}$ a weak subword
of all $u_{i}$ that is not a weak subword of $v_{j}$ then we set
$\psi(w_{j})=\textbf{F}(a_{1}\land\textbf{F}(a_{2}\land\cdots\textbf{F}a_{k}))$
with $w_{j}=a_{1}\cdots a_{k}$. This formula is satisfied by exactly the words
which have $w_{j}$ as a weak subword, hence by all $u_{i}$ but not $v_{j}$. We
set $\varphi_{j}$ as $\psi(w_{j})$ if it exists and $a$ if all $u_{i}$ start
with an $a$ and $v_{j}$ does not for some $a\in\Sigma$.

If $\varphi_{j}$ is defined for all $j$ then the formula
$\bigwedge_{j}\varphi_{j}$ is a separating formula. Otherwise there exists a
$v_{j}$ such that there are no weak subwords of all the $u_{i}$ that are not
weak subwords of $v_{j}$ and either the $u_{i}$ do not start with the same
letter or $v_{j}$ also starts with that letter. In that case we can easily
prove by induction that all $\textbf{LTL}(\textbf{F},\land,\lor)$ formulas of
the form $\textbf{F}\psi$ that are satisfied by all $u_{i}$ are also satisfied
by $v_{j}$, and as all formulas of the form $a$ with $a\in\Sigma$ satisfied by
all $u_{i}$ are also satisfied by $v_{j}$, the same can be said about boolean
combinations of those two types of formulas, and thus there are no separating
formulas in $\textbf{LTL}(\textbf{F},\land,\lor)$.

Concerning $\left\\{\textbf{G},\land,\lor\right\\}$, one can easily infer from
Fact 2 that we can turn any formula of $\textbf{LTL}(\textbf{F},\land,\lor)$
into one of $\textbf{LTL}(\textbf{G},\land,\lor)$ equivalent to its negation,
and vice-versa. Hence the short formula property of
$\left\\{\textbf{G},\land,\lor\right\\}$ is a consequence of the one of
$\left\\{\textbf{F},\land,\lor\right\\}$. ∎

######  Proposition 6.

$\left\\{\textbf{F},\textbf{G},\land,\lor\right\\}$ has the short formula
property.

###### Proof.

Let $(P,N)$ a sample. For all $u_{i}$ we set
$\varphi(u_{i})=\textbf{F}(a_{1}\land\textbf{F}(a_{2}\land\cdots\textbf{F}a_{k}))$
with $u_{i}=a_{1}\cdots a_{k}$. This formula is satisfied by exactly the words
with $u_{i}$ as a weak subword. For all $v_{j}$ we set
$\varphi(v_{j})=\textbf{G}(\bar{a_{1}}\lor\textbf{G}(\bar{a_{2}}\lor\cdots\textbf{G}\bar{a_{k}}))$
with $v_{j}=a_{1}\cdots a_{k}$ and
$\bar{a}=\bigvee_{b\in\Sigma\setminus\left\\{a\right\\}}b$ for all
$a\in\Sigma$. This formula is satisfied by exactly the words which do not have
$v_{j}$ as a weak subword. For all pairs $(u_{i},v_{j})$ we set $\psi_{i,j}$
as $\varphi(u_{i})\land\varphi(v_{j})$, and finally we define $\psi$ as
$\bigvee_{i}\bigwedge_{j}\psi_{i,j}$. If this formula does not separate the
$u_{i}$ and $v_{j}$ then there must exist $u_{i}$ and $v_{j}$ which are weak
subwords of each other. An easy induction on the formula then shows that
$u_{i}$ and $v_{j}$ satisfy the same formulas in
$\textbf{LTL}(\textbf{F},\textbf{G},\land,\lor)$, and thus there does not
exist any separating formula. ∎

##  5 Degenerate cases: the shortest formula property

######  Definition 2.

Let $Op$ a set of operators, we say that $Op$ has the _shortest formula
property_ if there is a polynomial time algorithm solving the
$\textbf{LTL}(Op)$ learning problem and outputting the minimal separating
formula if it exists.

######  Theorem 4.

Let $Op$ such that either
$Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X}\right\\}$,
$Op\subseteq\left\\{\lor,\land\right\\}$,
$Op=\left\\{\textbf{G},\land\right\\}$. Then $Op$ has the shortest formula
property, and therefore the $\textbf{LTL}(Op)$ learning problem is in $\P$.
The same holds for $Op=\left\\{\textbf{F},\lor\right\\}$ if the size of the
alphabet is fixed.

This theorem is the consequence of the following propositions, which establish
it for various subsets $Op$ of operators.

######  Proposition 7.

All $Op\subseteq\left\\{\lor,\land\right\\}$ have the shortest formula
property.

###### Proof.

Let $(P,N)$ a sample. Let $A\subseteq\Sigma$ be the set of first letters of
the $u_{i}$. Consider the formula $\psi=\bigvee_{a\in A}a$. We distinguish two
cases.

  * •

Either $\psi$ does not separate the $u_{i}$ and $v_{i}$, meaning that some
$u_{i}$ and $v_{j}$ share the same first letter. In that case $u_{i}$ and
$v_{j}$ satisfy the same formulas of $\textbf{LTL}(\lor,\land)$ and thus there
is no separating formula.

  * •

Or $\psi$ does separate the $u_{i}$ and $v_{j}$. In that case it is also of
minimal size: say some element $a$ of $A$ does not appear in a formula
$\varphi\in\textbf{LTL}(\lor,\land)$, then as it is satisfied by some $u_{i}$
starting with $a$, $\psi$ is a tautology and is also satisfied by the $v_{j}$.
Hence a separating formula has to contain all letters of $A$, and thus also at
least $|A|-1$ boolean operators. As a result, $\psi$ is of minimal size.

∎

######  Proposition 8.

All $Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X}\right\\}$ have the
shortest formula property.

###### Proof.

Let $\ell\in\mathbb{N}$, every formula
$\varphi\in\textbf{LTL}(\textbf{F},\textbf{G},\textbf{X})$ is equivalent over
words of length at most $\ell$ to a formula of smaller or equal size in

$\left\\{\top,\bot,\textbf{X}^{k}a,\textbf{X}^{k}\textbf{F}a,\textbf{X}^{k}\textbf{G}a,\textbf{X}^{k}\textbf{F}\textbf{G}a\mid
a\in\Sigma,0\leq k<\ell\right\\}.$

This can be shown by observing that over those words, for all $\psi$,
$\textbf{F}\textbf{X}\psi$ and $\textbf{X}\textbf{F}\psi$ are equivalent, as
well as $\textbf{G}\textbf{X}\psi$ and $\bot$. This allows to push all X
operators at the top of the formula. Finally, every formula of the form
$\textbf{X}^{k}\psi$ with $k\geq N$ is equivalent to $\bot$.

As a result we can compute a minimal separating formula by enumerating
formulas from this set (of polynomial size) and checking which ones separate
the positive and negative words. ∎

######  Proposition 9.

$\left\\{\textbf{G},\land\right\\}$ has the shortest formula property.

###### Proof.

An easy induction on $\psi$ shows that all $\textbf{LTL}(\textbf{G},\land)$
formulas are equivalent over finite words to a formula of the form $\top$,
$\bot$, $a$ or $\textbf{G}a$ with $a\in\Sigma$, i.e., to a formula of size at
most 2. As those can be enumerated in polynomial time, we can compute a
separating formula of minimal size or conclude that it does not exist in
polynomial time. ∎

A corollary of our results is that the classification between ¶ and mostly
does not depend upon whether we consider the alphabet as part of the input or
not. The only affected subcase is $Op=\left\\{\textbf{F},\lor\right\\}$, which
is -hard when the alphabet is not fixed (Theorem 2).

######  Proposition 10.

$\left\\{\textbf{F},\lor\right\\}$ has the shortest formula property when the
alphabet is fixed.

###### Proof.

Since F commutes with $\lor$, every formula can be turned into an equivalent
disjunction of formulas of the form $a$ or $\textbf{F}a$ with $a\in\Sigma$, of
polynomial size. There are only $2^{2|\Sigma|}$ such formulas, hence when
given a sample $(P,N)$ one can simply select the formulas that are not
satisfied by any $v_{j}$, take their disjunction, and check that all $u_{i}$
satisfy the resulting formula. If they do we have a separating formula,
otherwise there cannot exist any. ∎

##  6 An approximation algorithm for $\textbf{LTL}(\textbf{X},\land)$

An $\alpha$-approximation algorithm for learning a fragment of LTL does the
following: the algorithm either determines that there are no separating
formulas, or constructs a separating formula $\varphi$ which has size at most
$\alpha\cdot m$ with $m$ the size of a minimal separating formula.

######  Theorem 5.

There exists a $O(n\cdot\ell^{2})$ time $\log(n)$-approximation algorithm for
learning $\textbf{LTL}(\textbf{X},\land)$.

Recall the definition of patterns: a word $u=u(1)\dots u(\ell)$ and
$p_{1}<p_{2}<\dots<p_{\ell}$ induce the following
$\textbf{LTL}(\textbf{X},\land)$ formula, called a pattern:

$\mathcal{P}=\textbf{X}^{p_{1}-1}(u(1)\wedge\textbf{X}^{p_{2}-i_{1}}(\cdots\wedge\textbf{X}^{p_{\ell}-p_{\ell-1}}u(\ell))\cdots).$

It is equivalent to the (larger in size) formula
$\bigwedge_{i\in[1,\ell]}\textbf{X}^{p_{i}-1}u(i)$, which states that for each
$i\in[1,\ell]$, the letter in position $p_{i}$ is $u(i)$. To determine the
size of a pattern $\mathcal{P}$ we look at two parameters: its last position
$\textbf{last}(\mathcal{P})=i_{p}$ and its width $0pt(\mathcal{P})=p$. The
size of $\mathcal{P}$ is $\textbf{last}(P)+2(0pt(P)-1)$. The two parameters of
a pattern, last position and width, hint at the key trade-off we will have to
face in learning $\textbf{LTL}(\textbf{X},\wedge)$ formulas: do we increase
the last position, to reach further letters in the words, or the width, to
further restrict the set of satisfying words?

######  Lemma 4.

For every formula $\varphi\in\textbf{LTL}(\textbf{X},\wedge)$ there exists an
equivalent pattern of size smaller than or equal to $\varphi$.

###### Proof.

We proceed by induction on $\varphi$.

  * •

Atomic formulas are already a special case of patterns.

  * •

If $\varphi=\textbf{X}\varphi^{\prime}$, by induction hypothesis we get a
pattern $\mathcal{P}$ equivalent to $\varphi^{\prime}$, then
$\textbf{X}\mathcal{P}$ is a pattern and equivalent to $\varphi$.

  * •

If $\varphi=\varphi_{1}\wedge\varphi_{2}$, by induction hypothesis we get two
patterns $\mathcal{P}_{1}$ and $\mathcal{P}_{2}$ equivalent to $\varphi_{1}$
and $\varphi_{2}$. We use the inductive definition for patterns to show that
$\mathcal{P}_{1}\wedge\mathcal{P}_{2}$ is equivalent to another pattern. We
focus on the case
$\mathcal{P}_{1}=\textbf{X}^{i_{1}}(c_{1}\wedge\mathcal{P}^{\prime}_{1})$ and
$\mathcal{P}_{2}=\textbf{X}^{i_{2}}(c_{2}\wedge\mathcal{P}^{\prime}_{2})$, the
other cases are simpler instances of this one.

There are two cases: $i_{1}=i_{2}$ or $i_{1}\neq i_{2}$.

If $i_{1}=i_{2}$, either $c_{1}\neq c_{2}$ and then
$\mathcal{P}_{1}\wedge\mathcal{P}_{2}$ is equivalent to false, which is the
pattern $c_{1}\wedge c_{2}$, or $c_{1}=c_{2}$, and then
$\mathcal{P}_{1}\wedge\mathcal{P}_{2}$ is equivalent to
$\textbf{X}^{i_{1}}(c_{1}\wedge\mathcal{P}^{\prime}_{1}\wedge\mathcal{P}^{\prime}_{2})$.
By induction hypothesis
$\mathcal{P}^{\prime}_{1}\wedge\mathcal{P}^{\prime}_{2}$ is equivalent to a
pattern $\mathcal{P}^{\prime}$, so the pattern
$\textbf{X}^{i_{1}}(c_{1}\wedge\mathcal{P}^{\prime})$ is equivalent to
$\mathcal{P}_{1}\wedge\mathcal{P}_{2}$, hence to $\varphi$.

If $i_{1}\neq i_{2}$, without loss of generality $i_{1}<i_{2}$, then
$\mathcal{P}_{1}\wedge\mathcal{P}_{2}$ is equivalent to
$\textbf{X}^{i_{1}}(c_{1}\wedge\mathcal{P}^{\prime}_{1}\wedge\textbf{X}^{i_{2}-i_{1}}(c_{2}\wedge\mathcal{P}^{\prime}_{2}))$.
By induction hypothesis
$\mathcal{P}^{\prime}_{1}\wedge\textbf{X}^{i_{2}-i_{1}}(c_{2}\wedge\mathcal{P}^{\prime}_{2})$
is equivalent to a pattern $\mathcal{P}^{\prime}$, so the pattern
$\textbf{X}^{i_{1}}(c_{1}\wedge\mathcal{P}^{\prime})$. is equivalent to
$\mathcal{P}_{1}\wedge\mathcal{P}_{2}$, hence to $\varphi$.

∎

###### Proof.

Let $u_{1},\dots,u_{n},v_{1},\dots,v_{n}$ a set of $2n$ words of length at
most $\ell$. Thanks to Lemma 4 we are looking for a pattern. For a pattern
$\mathcal{P}$ we define
$I(\mathcal{P})=\left\\{i_{q}\in[1,\ell]:q\in[1,p]\right\\}$. Note that
$\textbf{last}(\mathcal{P})=\max I(\mathcal{P})$ and
$0pt(\mathcal{P})=\text{Card}(I(\mathcal{P}))$.

We define the set $X=\left\\{i\in[1,\ell]:\exists c\in\Sigma,\forall
j\in[1,n],u_{j}(i)=c\right\\}$. Note that $\mathcal{P}$ satisfies
$u_{1},\dots,u_{n}$ if and only if $I(\mathcal{P})\subseteq X$. Further, given
$I\subseteq X$, we can construct a pattern $\mathcal{P}$ such that
$I(\mathcal{P})=I$ and $\mathcal{P}$ satisfies $u_{1},\dots,u_{n}$: we simply
choose $c_{q}=u_{1}(i_{q})=\dots=u_{n}(i_{q})$ for $q\in[1,p]$. We call
$\mathcal{P}$ the pattern corresponding to $I$.

Recall that the size of the pattern $\mathcal{P}$ is
$\textbf{last}(\mathcal{P})+2(0pt(\mathcal{P})-1)$. This makes the task of
minimising it difficult: there is a trade-off between minimising the last
position $\textbf{last}(\mathcal{P})$ and the width $0pt(\mathcal{P})$.

Let us consider the following easier problem: construct a
$\log(n)$-approximation of a minimal separating pattern with fixed last
position. Assuming we have such an algorithm, we obtain a
$\log(n)$-approximation of a minimal separating pattern by running the
previous algorithm on prefixes of length $\ell^{\prime}$ for each
$\ell^{\prime}\in[1,\ell]$.

We now focus on the question of constructing a $\log(n)$-approximation of a
minimal separating pattern with fixed last position. For a set $I$, we write
$C_{I}=\bigcup\left\\{Y_{i}:i\in I\right\\}$: the pattern corresponding to $I$
does not satisfy $v_{j}$ if and only if $j\in C_{I}$. In particular, the
pattern corresponding to $I$ is separating if and only if $C_{I}=[1,n]$.

The algorithm constructs a set $I$ incrementally through the sequence
$(I_{x})_{x\geq 0}$, with the following easy invariant: for $x\geq 0$, we have
$C_{x}=C_{I_{x}}$. The algorithm is greedy: $I_{x}$ is augmented with $i\in
X\setminus I_{x}$ maximising the number of words added to $C_{x}$ by adding
$i$, which is the cardinality of $Y_{i}\setminus C_{x}$.

We now prove that this yields a $\log(n)$-approximation algorithm. Let
$\mathcal{P}_{\text{opt}}$ a minimal separating pattern with last position
$\ell$, inducing $I_{\text{opt}}=I(\mathcal{P}_{\text{opt}})\subseteq[1,\ell]$
of cardinal $m$. Note that $C_{I_{\text{opt}}}=[1,n]$.

We let $n_{x}=n-|C_{x}|$ and show the following by induction on $x\geq 0$:

$n_{x+1}\leq n_{x}\cdot\left(1-\frac{1}{m}\right)=n_{x}\cdot\frac{m-1}{m}.$

We claim that there exists $i\in X\setminus I_{x}$ such that
$\text{Card}(Y_{i}\setminus C_{x})\geq\frac{n_{x}}{m}$. Indeed, assume towards
contradiction that for all $i\in X\setminus I_{x}$ we have
$\text{Card}(Y_{i}\setminus C_{x})<\frac{n_{x}}{m}$, then there are no sets
$I$ of cardinal $m$ such that $C_{I}\supseteq[1,n]\setminus C_{x}$,
contradicting the existence of $I_{\text{opt}}$. Thus there exists $i\in
X\setminus I_{x}$ such that $\text{Card}(Y_{i}\setminus
C_{x})\geq\frac{n_{x}}{m}$, implying that the algorithm chooses such an $i$
and $n_{x+1}\leq n_{x}-\frac{n_{x}}{m}=n_{x}\cdot\left(1-\frac{1}{m}\right)$.

The proved inequality implies $n_{x}\leq
n\cdot\left(1-\frac{1}{m}\right)^{x}$. This quantity is less than $1$ for
$x\geq\log(n)\cdot m$, implying that the algorithm stops after at most
$\log(n)\cdot m$ steps. Consequently, the pattern corresponding to $I$ has
size at most $\log(n)\cdot|\mathcal{P}_{\text{opt}}|$, completing the claim on
approximation.

A naive complexity analysis yields an implementation of the greedy algorithm
running in time $O(n\cdot\ell)$, leading to an overall complexity of
$O(n\cdot\ell^{2})$ by running the greedy algorithm on the prefixes of length
$\ell^{\prime}$ of $u_{1},\dots,u_{n},v_{1},\dots,v_{n}$ for each
$\ell^{\prime}\in[1,\ell]$. ∎

##  7 Almost all fragments with the next operator are hard to approximate

######  Theorem 6.

The $\textbf{LTL}(\textbf{X},\wedge)$ learning problem is -hard, and there are
no $(1-o(1))\cdot\log(n)$ polynomial time approximation algorithms unless
$\P=\NP$, even for a single positive word.

Note that Theorem 5 and Theorem 6 yield matching upper and lower bounds on
approximation algorithms for learning $\textbf{LTL}(\textbf{X},\land)$.

The hardness result stated in Theorem 6 follows from a reduction to the set
cover problem, that we define now. The set cover decision problem is: given
$S_{1},\dots,S_{\ell}$ subsets of $[1,n]$ and $k\in\mathbb{N}$, does there
exists $I\subseteq[1,\ell]$ of size at most $k$ such that $\bigcup_{i\in
I}S_{i}=[1,n]$? In that case we say that $I$ is a cover. An
$\alpha$-approximation algorithm returns a cover of size at most $\alpha\cdot
k$ where $k$ is the size of a minimal cover. The following results form the
state of the art for solving exact and approximate variants of the set cover
problem.

######  Theorem 7 ((?)).

The set cover problem is -complete, and there are no $(1-o(1))\cdot\log(n)$
polynomial time approximation algorithms unless $\P=\NP$.

###### Proof.

We construct a reduction from set cover. Let $S_{1},\dots,S_{\ell}$ subsets of
$[1,n]$ and $k\in\mathbb{N}$.

Let us consider the word $u=a^{\ell+1}$, and for each $j\in[1,n]$ and
$i\in[1,\ell]$, writing $v_{j}(i)$ for the $i$th letter of $v_{j}$:

$v_{j}(i)=\begin{cases}b\text{ if }j\in S_{i},\\\ a\text{ if }j\notin
S_{i},\\\ \end{cases}$

and we set $v_{j}(\ell+1)=a$ for any $j\in[1,n]$. We also add
$v_{n+1}=a^{\ell}b$.

We claim that there is a cover of size $k$ if and only if there is a formula
of size $\ell+2k-1$ separating $u$ from $v_{1},\dots,v_{n+1}$.

Thanks to Lemma 4 we can restrict our attention to patterns, i.e formulas of
the form (we adjust the indexing for technical convenience)

$\varphi=\textbf{X}^{i_{1}-1}(c_{1}\wedge\textbf{X}^{i_{2}-i_{1}}(\cdots\wedge\textbf{X}^{i_{p+1}-i_{p}}c_{p+1})\cdots),$

for some positions $i_{1}\leq\dots\leq i_{p+1}$ and letters
$c_{1},\dots,c_{p+1}\in\Sigma$. If $\varphi$ satisfies $u$, then necessarily
$c_{1}=\dots=c_{p+1}=a$. This implies that if $\varphi$ does not satisfy
$v_{n+1}$, then necessarily $i_{p+1}=\ell+1$.

We associate to $\varphi$ the set $I=\left\\{i_{1}\leq\dots\leq
i_{p}\right\\}$. It is easy to see that $\varphi$ is equivalent to
$\bigwedge_{q\in[1,p]}\textbf{X}^{i_{q}-1}a\wedge\textbf{X}^{\ell}a$, and the
size of $\varphi$ is $\ell+1+2(|I|-1)$.

By construction, $\varphi$ separates $u$ from $v_{1},\dots,v_{n+1}$ if and
only if $I$ is a cover. Indeed, $I$ is a cover if and only if for every
$j\in[1,n]$ there exists $i\in I$ such that $j\in S_{i}$, which is equivalent
to for every $j\in[1,n]$ we have $v_{j}\not\models\varphi$. ∎

We can extend the previous hardness result to all sets of operators $Op$ such
that $\left\\{\textbf{X},\land\right\\}\subseteq
Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X},\land,\lor\right\\}$, by
reducing their learning problems to the previous one. The reduction consists
in transforming the input words so that the F and G operators are essentially
useless. The $\lor$ operator is also useless since we only have one positive
word, implying that the minimal separating formulas in $\textbf{LTL}(Op)$ and
$\textbf{LTL}(\textbf{X},\land)$ are in fact the same.

The first step is a reduction lemma for disjunctions.

######  Lemma 5.

For all $\varphi\in\textbf{LTL}(\textbf{X},\land,\lor)$, for all
$u,v_{1},\dots,v_{n}$, if $\varphi$ separates $u$ from $v_{1},\dots,v_{n}$,
then there exists $\psi\in\textbf{LTL}(\textbf{X},\land)$ such that
$|\psi|\leq|\varphi|$ which separates $u$ from $v_{1},\dots,v_{n}$.

###### Proof.

We define $D(\varphi)\subseteq\textbf{LTL}(\textbf{X},\land)$ by induction:

  * •

If $\varphi=c$ then $D(\varphi)=\left\\{c\right\\}$.

  * •

If $\varphi=\varphi_{1}\wedge\varphi_{2}$ then
$D(\varphi)=\left\\{\psi_{1}\wedge\psi_{2}:\psi_{1}\in
D(\varphi_{1}),\psi_{2}\in D(\varphi_{2})\right\\}$.

  * •

If $\varphi=\varphi_{1}\vee\varphi_{2}$ then $D(\varphi)=D(\varphi_{1})\cup
D(\varphi_{2})$.

  * •

If $\varphi=\textbf{X}\varphi^{\prime}$ then
$D(\varphi)=\left\\{\textbf{X}\psi:\psi\in D(\varphi^{\prime})\right\\}$.

  * •

If $\varphi=\textbf{F}\varphi^{\prime}$ then
$D(\varphi)=\left\\{\textbf{F}\psi:\psi\in D(\varphi^{\prime})\right\\}$.

Observe that all formulas of $D(\varphi)$ are of size at most $|\varphi|$, and
are in $\textbf{LTL}(\textbf{X},\land)$. We now show that for all $\varphi$,
for all $u,v_{1},\dots,v_{n}$, if $\varphi$ separates $u$ from
$v_{1},\dots,v_{n}$ then there exists $\psi\in D(\varphi)$ separating them,
which proves the lemma.

We proceed by induction on $\varphi$.

  * •

If $\varphi=c$ this is clear.

  * •

If $\varphi=\varphi_{1}\wedge\varphi_{2}$ then
$D(\varphi)=\left\\{\psi_{1}\wedge\psi_{2}:\psi_{1}\in
D(\varphi_{1}),\psi_{2}\in D(\varphi_{2})\right\\}$. Since $\varphi$ separates
$u$ from $v_{1},\dots,v_{n}$, there exists $I_{1},I_{2}\subseteq[1,n]$ such
that $I_{1}\cup I_{2}=[1,n]$, $\varphi_{1}$ separates $u$ from
$\left\\{v_{i}:i\in I_{1}\right\\}$, and $\varphi_{2}$ separates $u$ from
$\left\\{v_{i}:i\in I_{2}\right\\}$. By induction hypothesis applied to both
$\varphi_{1}$ and $\varphi_{2}$ there exists $\psi_{1}\in D(\varphi_{1})$
separating $u$ from $\left\\{v_{i}:i\in I_{1}\right\\}$ and $\psi_{2}\in
D(\varphi_{2})$ separating $u$ from $\left\\{v_{i}:i\in I_{2}\right\\}$. It
follows that $\psi_{1}\wedge\psi_{2}$ separates $u$ from $v_{1},\dots,v_{n}$,
and $\psi_{1}\wedge\psi_{2}\in D(\varphi)$.

  * •

If $\varphi=\varphi_{1}\vee\varphi_{2}$ then $D(\varphi)=D(\varphi_{1})\cup
D(\varphi_{2})$. Since $\varphi$ separates $u$ from $v_{1},\dots,v_{n}$,
either $\varphi_{1}$ or $\varphi_{2}$ does as well; without loss of generality
let us say that $\varphi_{1}$ separates $u$ from $v_{1},\dots,v_{n}$. The
induction hypothesis implies that $\psi_{1}\in D(\varphi_{1})$ separates $u$
from $v_{1},\dots,v_{n}$, and $\psi_{1}\in D(\varphi)$.

  * •

The case $\varphi=\textbf{X}\varphi^{\prime}$ follows directly by induction
hypothesis.

∎

######  Proposition 11.

For all $\left\\{\textbf{X},\land\right\\}\subseteq
Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X},\land,\lor\right\\}$,
there is a polynomial-time reduction from the $\textbf{LTL}(X,\land)$ learning
problem for a single positive word to the $\textbf{LTL}(Op)$ one over the same
alphabet.

We recall two (folklore) facts about LTL. They can easily be proven by
induction on the formula.

######  Fact 3.

For all $w_{1}\in\Sigma^{*},w_{2}\in\Sigma^{+},N\in\mathbb{N}$, and
$\varphi\in\textbf{LTL}$ with $|\varphi|\leq N$, then
$w_{1}w_{2}^{N}\vDash\varphi$ if and only if $w_{1}w_{2}^{N+1}\vDash\varphi$.

######  Fact 4.

For all $w_{1}\in\Sigma^{*},N\in\mathbb{N}$, and
$\varphi\in\textbf{LTL}(\textbf{X},\land,\lor)$ with at most $N+1$ operators X
in $\varphi$, then $w_{1}\vDash\varphi$ if and only if $w_{1}^{\leq
N}\vDash\varphi$.

We now proceed to the proof of Proposition 11.

###### Proof.

Let $u,v_{1},\ldots,v_{n}\in\Sigma^{*}$ be words, all of length $\ell$. Let
$a\in\Sigma$, we set $M$ as the size of the formula

$\psi_{u}=\bigwedge_{i=0}^{|u|-1}X^{i}u_{i},$

$u^{\prime}=ua^{M}$, for all $i$, we define $v^{\prime}_{i}=v_{i}a^{M}$,

$\textbf{u}=(u^{\prime}v^{\prime}_{1}\cdots
v^{\prime}_{n})^{M+1}\quad;\quad\textbf{v}_{i}=v^{\prime}_{i}\cdots
v^{\prime}_{n}(u^{\prime}v^{\prime}_{1}\cdots v^{\prime}_{n})^{M}.$

The formula $\psi_{u}$ separates $u$ from $\left\\{v_{1},\dots,v_{n}\right\\}$
unless one of the $v_{i}$ is equal to $u$. This can be checked in polynomial
time, and in that case we can answer no to the learning problem immediately.
In all that follows we assume that $\psi_{u}$ separates $u$ from the $v_{i}$.

Let $\varphi\in\textbf{LTL}(Op)$ be a formula of minimal size separating u
from the $(\textbf{v}_{i})_{1\leq i\leq n}$. Note that $\psi_{u}$ is satisfied
by u but not by any $\textbf{v}_{i}$, thus since $Op$ contains X and $\land$,
$\varphi$ exists and $|\varphi|\leq|\varphi_{u}|=M$.

We first show that $\varphi$ contains no F or G. Let
$C\in\textbf{LTL}(\textbf{X},\land,\lor)$ be a context with free variables
$x_{1},\ldots,x_{m}$ (each appearing exactly once in $C$) such that
$\varphi=C[\psi_{1}\to x_{1},\ldots,\psi_{m}\to x_{m}]$ for some
$\psi_{i}\in\textbf{LTL}(Op)$ of the form either $\textbf{F}\psi^{\prime}$ or
$\textbf{G}\psi^{\prime}$.

As the X operator commutes with all the others, we can push the X to the
variables in $C$. Hence there exist a boolean context $B$ with free variables
$y_{1},\ldots,y_{m}$ (each appearing exactly once in $B$) and
$j_{1},\ldots,j_{m}\in\mathbb{N}$ such that $B[X^{j_{1}}x_{1}\to
y_{1},\ldots,X^{j_{m}}x_{m}\to y_{m}]$ is equivalent to $C$. Furthermore, the
formulas $B$ and $C$ have the same depth, thus as $C$ is of size at most $M$,
we have $j_{p}\leq M$ for all $p$.

Note that $B$ does not contain any negation, thus if u did not satisfy some
$X^{j_{p}}\psi_{p}$, we would have that u satisfies $B[X^{j_{1}}\psi_{1}\to
y_{1},\ldots,X^{j_{m}}\bot\to y_{p},\ldots X^{j_{m}}\psi_{m}\to y_{m}]$, while
no $\textbf{v}_{i}$ satisfies it, since they do not satisfy
$B[X^{j_{1}}\psi_{1}\to y_{1},\ldots,X^{j_{m}}\psi_{m}\to y_{m}]$. As a
result, $C[\psi_{1}\to x_{1},\ldots,\bot\to x_{p},\ldots,\psi_{m}\to x_{m}]$
would be satisfied by u but no $\textbf{v}_{i}$, contradicting the minimality
of $\varphi$. Hence u satisfies all $X^{j_{p}}\psi_{p}$.

Let $1\leq p\leq m$, let $1\leq i\leq n$, we show that $\textbf{v}_{i}$
satisfies $\textbf{X}^{j_{p}}\psi_{p}$. We distinguish two cases:

  * •

$\psi_{p}=\textbf{G}\psi^{\prime}$. Since $\textbf{v}_{i}$ is a suffix of u of
length greater than $M$, $\textbf{v}_{i}[j_{p}\dots]$ is not empty and is a
suffix of $\textbf{u}[j_{p}\dots]$. As the latter satisfies
$\textbf{G}\psi^{\prime}$, so does the former. Hence
$\textbf{v}_{i}\vDash\textbf{X}^{j_{p}}\psi_{p}$.

  * •

$\psi_{p}=\textbf{F}\psi^{\prime}$. We have that
$\textbf{u}[j_{p}\dots]=(u^{\prime}[j_{p}\dots]v^{\prime}_{1}\cdots
v^{\prime}_{n})(u^{\prime}v^{\prime}_{1}\cdots v^{\prime}_{n})^{M}$ satisfies
$\psi_{p}$. By Fact 3, as $\psi_{p}$ is of size at most $|\psi|\leq M$,
$(u^{\prime}[j_{p}\dots]v^{\prime}_{1}\cdots v^{\prime}_{n})(u^{M}v_{1}\cdots
u^{M}v_{n})^{M-1}$ satisfies $\psi_{p}$ as well. As the latter is a suffix of
$\textbf{v}_{i}[j_{p}\dots]$, $\textbf{v}_{i}[j_{p}\dots]$ also satisfies the
formula. Hence $\textbf{v}_{i}\vDash\textbf{X}^{j_{p}}\psi_{p}$.

Now consider the formula $\varphi^{\prime}=C[\top\to x_{1},\ldots,\top\to
x_{m}]$, which is equivalent to $B[\textbf{X}^{j_{1}}\top\to
y_{1},\ldots,\textbf{X}^{j_{m}}\top\to y_{m}]$. As all $\textbf{v}_{i}$
satisfy all $\psi_{p}$ but not $\varphi$, no $\textbf{v}_{i}$ satisfies
$\varphi^{\prime}$. Further, as u satisfies $\varphi$ and all $\psi_{p}$, it
also satisfies $\varphi^{\prime}$. This contradicts the minimality of
$\varphi$, unless $m=0$. As a result, $\varphi$ does not contain any F or G.
Thus the minimal $\textbf{LTL}(Op)$ formula separating u and the
$\textbf{v}_{i}$ is the same as the minimal
$\textbf{LTL}(Op\cap\left\\{\textbf{X},\land,\lor\right\\})$ separating them.

By Fact 4, we have that this formula is also the minimal formula separating
$u^{\prime}$ and the $v^{\prime}_{i}$. Clearly any
$\textbf{LTL}(Op\cap\left\\{\textbf{X},\land,\lor\right\\})$ formula
separating $u$ and the $v_{i}$ also separates those. By Lemma 5, there exists
$\varphi^{\prime}\in\textbf{LTL}(\textbf{X},\land)$ with
$|\varphi^{\prime}|\leq|\varphi|$ separating $u^{\prime}$ and the
$v_{i}u^{M-1}$, of the form
$X^{i_{1}-1}(c_{1}\land\textbf{X}^{i_{2}-i_{1}}(\cdots\land\textbf{X}^{i_{p}-i_{p-1}}c_{p})\cdots)$
with $0<i_{1}<\ldots<i_{p}$ and $c-1,\ldots,c_{p}\in\Sigma$. As $u^{\prime}$
and the $v^{\prime}_{i}$ are equal after the first $|u|$ letters, by
minimality of $|\varphi|$, we have $i_{p}<|u|$. As a result, by Fact 4,
$\varphi^{\prime}$ separates $u$ and the $v_{i}$.

We conclude that the minimal size of a formula of $\textbf{LTL}(Op)$
separating u and the $\textbf{v}_{i}$ is the same as the minimal size of a
formula of $\textbf{LTL}(\textbf{X},\land)$ separating $u$ and the $v_{i}$.
This completes the reduction. ∎

######  Proposition 12.

For all $\left\\{\textbf{X},\lor\right\\}\subseteq
Op\subseteq\left\\{\textbf{F},\textbf{G},\textbf{X},\land,\lor\right\\}$,
there is a polynomial-time reduction from the $\textbf{LTL}(\textbf{X},\vee)$
learning problem for a single negative word to the $\textbf{LTL}(Op)$ one over
the same alphabet.

###### Proof.

The proof is identical to the one of Proposition 11, with the roles of
positive and negative words reversed and disjunctions and conjunctions
reversed. ∎

##  8 Almost all fragments without the next operator are hard to approximate

### A study of $\textbf{LTL}(\textbf{F},\wedge)$

As we will see, $\textbf{LTL}(\textbf{F},\wedge)$ over an alphabet of size $2$
is very weak. This degeneracy vanishes when considering alphabets of size at
least $3$. Instead of defining a normal form as we did for
$\textbf{LTL}(\textbf{X},\wedge)$ we characterise the expressive power of
$\textbf{LTL}(\textbf{F},\wedge)$ and construct for each property expressible
in this logic a minimal formula.

######  Lemma 6.

For every formula $\varphi\in\textbf{LTL}(\textbf{F},\wedge)$, either it is
equivalent to false or there exists a finite set of non-repeating words
$w_{1},\dots,w_{p}$ and $c\in\Sigma\cup\left\\{\varepsilon\right\\}$ such that
for every word $z$,

$z\models\varphi\text{ if and only if }\begin{cases}\text{for all
$q\in[1,p],w_{q}$ is a subword of $z$},\\\ \text{and $z$ starts with
$c$}.\end{cases}$

###### Proof.

We proceed by induction over $\varphi$.

  * •

For the atomic formula $c\in\Sigma$, the property is satisfied using the empty
set of words and $c$.

  * •

If $\varphi=\textbf{F}\varphi^{\prime}$, by induction hypothesis we get
$w_{1},\dots,w_{p}$ and $c$ for $\varphi^{\prime}$. We let
$w^{\prime}_{i}=cw_{i}$ if $w_{i}(1)\neq c$ and $w^{\prime}_{i}=w_{i}$
otherwise, then $z\models\varphi$ if and only if for all $q\in[1,p]$,
$w^{\prime}_{q}$ is a subword of $z$ and $z$ starts with $\varepsilon$ (the
latter condition is always satisfied).

  * •

If $\varphi=\varphi_{1}\wedge\varphi_{2}$, by induction hypothesis we get
$w^{1}_{1},\dots,w^{1}_{p_{1}},c_{1}$ for $\varphi_{1}$ and
$w^{2}_{1},\dots,w^{2}_{p_{2}},c_{2}$ for $\varphi_{2}$. There are two cases.
If $c_{1}$ and $c_{2}$ are non-empty and $c_{1}\neq c_{2}$ then $\varphi$ is
equivalent to false. Otherwise, either both are non-empty and equal or at
least one is $\varepsilon$, say $c_{2}$. In both cases, $u\models\varphi$ if
and only if for all $(e,q)\in(1,[1,p_{1}])\cup(2,[1,p_{2}])$, $w^{e}_{q}$ is a
subword of $u$ and $u$ starts with $c_{1}$.

∎

Lemma 6 gives a characterisation of the properties expressible in
$\textbf{LTL}(\textbf{F},\wedge)$. It implies that over an alphabet of size
$2$ the fragment $\textbf{LTL}(\textbf{F},\wedge)$ is very weak. Indeed, there
are very few non-repeating words over the alphabet
$\Sigma=\left\\{a,b\right\\}$: only prefixes of $abab\dots$ and $baba\dots$.
This implies that formulas in $\textbf{LTL}(\textbf{F},\wedge)$ over
$\Sigma=\left\\{a,b\right\\}$ can only place lower bounds on the number of
alternations between $a$ and $b$ (starting from $a$ or from $b$) and check
whether the word starts with $a$ or $b$. In particular, the
$\textbf{LTL}(\textbf{F},\wedge)$ learning problem over this alphabet is
(almost) trivial and thus not interesting. Hence we now assume that $\Sigma$
has size at least $3$.

We move back from semantics to syntax, and show how to construct minimal
formulas. Let $w_{1},\dots,w_{p}$ a finite set of non-repeating words and
$c\in\Sigma\cup\left\\{\varepsilon\right\\}$, we define a formula $\varphi$ as
follows.

The set of prefixes of $w_{1},\dots,w_{p}$ are organised in a forest (set of
trees): a node is labelled by a prefix $w$ of some $w_{1},\dots,w_{p}$, and
its children are the words $wc$ which are prefixes of some
$w_{1},\dots,w_{p}$. The leaves are labelled by $w_{1},\dots,w_{p}$. We
interpret each tree $t$ as a formula $\varphi_{t}$ in
$\textbf{LTL}(\textbf{F},\wedge)$ as follows, in an inductive fashion: for
$c\in\Sigma$, if $t$ is labelled $wa$ with subtrees $t_{1},\dots,t_{q}$, then

$\varphi_{t}=\textbf{F}(c\wedge\bigwedge_{i}\varphi_{t_{i}}).$

If $c=\varepsilon$, the formula associated to $w_{1},\dots,w_{p}$ and $c$ is
the conjunction of the formulas for each tree of the forest, and if
$c\in\Sigma$, then the formula additionally has a conjunct $c$.

As an example, consider the set of words $ab,ac,bab$, and the letter $a$. The
forest corresponding to $ab,ac,bab$ contains two trees: one contains the nodes
$b,ba,bab$, and the other one the nodes $a,ab,ac$. The two corresponding
formulas are

$\textbf{F}(b\wedge\textbf{F}(a\wedge\textbf{F}b))\qquad;\qquad\textbf{F}(a\wedge\textbf{F}b\wedge\textbf{F}c).$

And the formula corresponding to the set of words $ab,ac,bab$, and the letter
$a$ is

$a\ \wedge\ \textbf{F}(b\wedge\textbf{F}(a\wedge\textbf{F}b))\ \wedge\
\textbf{F}(a\wedge\textbf{F}b\wedge\textbf{F}c).$

######  Lemma 7.

For every non-repeating words $w_{1},\dots,w_{p}$ and
$c\in\Sigma\cup\left\\{\varepsilon\right\\}$, the formula $\varphi$
constructed above is minimal, meaning there are no smaller equivalent
formulas.

Applying the construction above to a single non-repeating word $w=c_{1}\dots
c_{p}$ we obtain what we call a “fattern” (pattern with an F):

$F=\textbf{F}(c_{1}\wedge\textbf{F}(\cdots\wedge\textbf{F}c_{p})\cdots),$

We say that the non-repeating word $w$ induces the fattern $F$ above, and
conversely that the fattern $F$ induces the word $w$. The size of a fattern
$F$ is $3|w|-1$. Adding the initial letter we obtain a grounded fattern
$c\wedge F$, in that case the letter $c$ is added at the beginning of $w$ and
the size is $3|w|-2$.

######  Lemma 8.

Let $u_{1},\dots,u_{n},v_{1},\dots,v_{n}$. If there exists
$\varphi\in\textbf{LTL}(\textbf{F},\wedge)$ separating $u_{1},\dots,u_{n}$
from $v_{1},\dots,v_{n}$, then there exists a conjunction of at most $n$
fatterns separating $u_{1},\dots,u_{n}$ from $v_{1},\dots,v_{n}$.

###### Proof.

Thanks to Lemma 6, to the separating formula $\varphi$ we can associate a
finite set of non-repeating words $w_{1},\dots,w_{p}$ and
$c\in\Sigma\cup\left\\{\varepsilon\right\\}$ such that for every word $z$,

$z\models\varphi\text{ if and only if }\begin{cases}\text{for all
$q\in[1,p],w_{q}$ is a subword of $z$},\\\ \text{and $z$ starts with
$c$}.\end{cases}$

Let $j\in[1,n]$, since $v_{j}$ does not satisfy $\varphi$ either $v_{j}$ does
not start with $c$ or for some $q\in[1,p]$ the word $w_{q}$ is not a subword
of $u$. For each $j\in[1,n]$ such that $v_{j}$ starts with $c$, we pick one
$q_{j}\in[1,p]$ for which $w_{q_{j}}$ is not a subword of $v_{j}$, and
consider the set $\left\\{w_{q_{j}}:j\in[1,n]\right\\}$ together with
$c\in\Sigma\cup\left\\{\varepsilon\right\\}$. The formula induced by the
construction above is a conjunction of at most $n$ fatterns and it separates
$u_{1},\dots,u_{n}$ from $v_{1},\dots,v_{n}$. ∎

### Hardness result when the alphabet is part of the input

######  Theorem 8.

The $\textbf{LTL}(\textbf{F},\wedge)$ learning problem is $\NP$-hard when the
alphabet is part of the input, and there are no $(1-o(1))\cdot\log(n)$
polynomial time approximation algorithms unless $\P=\NP$, even with a single
positive word.

The result follows from a reduction from the hitting set problem. For proving
the correctness of the reduction we will need a normalisation lemma
specialised to the case of a single positive word.

######  Lemma 9.

Let $u,v_{1},\dots,v_{n}$. If there exists
$\varphi\in\textbf{LTL}(\textbf{F},\wedge)$ separating $u$ from
$v_{1},\dots,v_{n}$, then there exists a fattern of size smaller than or equal
to $\varphi$ separating $u$ from $v_{1},\dots,v_{n}$.

###### Proof.

Thanks to Lemma 6, to the separating formula $\varphi$ we can associate a
finite set of non-repeating words $w_{1},\dots,w_{p}$ and
$c\in\Sigma\cup\left\\{\varepsilon\right\\}$ such that for every word $z$,

$z\models\varphi\text{ if and only if }\begin{cases}\text{for all
$q\in[1,p],w_{q}$ is a subword of $z$},\\\ \text{and $z$ starts with
$c$}.\end{cases}$

Since $u$ satisfies $\varphi$, it starts with $c$ and for all $q\in[1,p]$,
$w_{q}$ is a subword of $u$. For each $q\in[1,p]$ there exists $\varphi_{q}$
mapping the positions of $w_{q}$ to $u$. Let us write $w$ for the word
obtained by considering all positions mapped by $\varphi_{q}$ for $q\in[1,p]$.
By definition $w$ is a subword of $u$, and for all $q\in[1,p]$ $w_{q}$ is a
subword of $w$. It follows that the fattern induced by $w$ separates $u$ from
$v_{1},\dots,v_{n}$. The size of $w$ is at most the sum of the sizes of the
$w_{q}$ for $q\in[1,p]$, hence the fattern induced by $w$ is smaller than the
original formula $\varphi$. ∎

We can now prove Theorem 8.

###### Proof.

We construct a reduction from the hitting set problem. Let $C_{1},\dots,C_{n}$
subsets of $[1,m]$ and $k\in\mathbb{N}$. Let us consider the alphabet $[0,m]$,
we define the word $u=012\dots m$. For each $j\in[1,n]$ we let $[1,m]\setminus
C_{j}=\left\\{a_{j,1}<\dots<a_{j,m_{j}}\right\\}$, and define
$v_{j}=0a_{j,1}\dots a_{j,m_{j}}$.

We claim that there exists a hitting set of size at most $k$ if and only if
there exists a formula in $\textbf{LTL}(\textbf{F},\wedge)$ of size at most
$3k-1$ separating $u$ from $v_{1},\dots,v_{n}$.

Let $H=\left\\{c_{1},\dots,c_{k}\right\\}$ a hitting set of size $k$ with
$c_{1}<c_{2}<\dots<c_{k}$, we construct the (non-grounded) fattern induced by
$w=c_{1}\dots c_{k}$, it separates $u$ from $v_{1},\dots,v_{n}$ and has size
$3k-1$.

Conversely, let $\varphi$ a formula in $\textbf{LTL}(\textbf{F},\wedge)$ of
size $3k-1$ separating $u$ from $v_{1},\dots,v_{n}$. Thanks to Lemma 9 we can
assume that $\varphi$ is a fattern, let $w=c_{1}\dots c_{k}$ the non-repeating
word it induces. Necessarily $c_{1}<c_{2}<\dots<c_{k}$. If $\varphi$ is
grounded then $c_{1}=0$, but then the (non-grounded) fattern induced by
$c_{2}\dots c_{k}$ is also separating, so we can assume that $\varphi$ is not
grounded. We let $H=\left\\{c_{1},\dots,c_{k}\right\\}$, and argue that $H$ is
a hitting set. Indeed, $H$ is a hitting set if and only if for every
$j\in[1,n]$ we have $H\cap C_{j}\neq\emptyset$, which is equivalent to for
every $j\in[1,n]$ we have $v_{j}\not\models\varphi$; indeed for $c_{i}\in
H\cap C_{j}$ by definition $c_{i}$ does not appear in $v_{j}$ so
$v_{j}\not\models\textbf{F}c_{i}$. ∎

### Hardness result for fixed alphabet

The most technical result in this paper is the following theorem, which
strengthens Theorem 8 by restricting to an alphabet of size $3$.

######  Theorem 9.

For all $\left\\{\textbf{F},\land\right\\}\subseteq
Op\subseteq\left\\{\textbf{F},\textbf{G},\land,\lor,\neg\right\\}$, the
learning problem for $\textbf{LTL}(Op)$ is -hard even for an alphabet of size
$3$.

Its main difficulty stems from the use of a fixed alphabet, combined with the
absence of X, which forbids us from pointing at a specific position. To
circumvent this problem we will adapt the previous reductions from hitting
set: we again use a single positive example $u$ against several negative ones
$v_{1},\ldots,v_{n}$. Each of those words is a sequence of factors
$abab\cdots$ (one for each subset) separated by a letter $c$. We introduce
small differences between the factors in the $v_{i}$ and in $u$. We ensure
that detecting those differences is costly in terms or operators, and thus
that a minimal formula has to “talk about” as few of them as possible. The
main difficulty in the proof is showing that we do not have more efficient
ways to separate the words. Much like in the previous hardness proofs, the
minimal formula has to select a minimal amount of positions (here factors) in
the words that are enough to distinguish $u$ from the $v_{i}$. Those positions
answer the hitting set problem. We temporarily allow the negation operator as
it does not make the proof more difficult and allows us to obtain a dual
version of Theorem 9 easily.

We consider the alphabet $\Sigma=\left\\{a,b,c\right\\}$. Let
$S=\left\\{1,\ldots,m\right\\}$, let $T_{1},\ldots,T_{n}\subseteq S$, let
$k^{\prime}\in\mathbb{N}$. We set $M=3m+2$, $u=((ab)^{M+1}c)^{m}$ and for all
$i$, $v_{i}=cw_{i,1}cw_{i,2}c\cdots w_{i,m}c$ with

$w_{i,j}=\begin{cases}(ab)^{M}&\text{ if }j\in T_{i},\\\ (ab)^{M+1}&\text{
otherwise.}\end{cases}$

Let $k$ be size of a minimal hitting set.

######  Claim 1.

There exists a separating formula in $\textbf{LTL}(\textbf{F},\land)$ of size
at most $6kM+9m+2$.

###### Proof.

Let $H$ be a hitting set of size $k$. We define for $i\in[1,m]$,

$z_{j}=\begin{cases}(ab)^{M+1}&\text{ if }i\in H,\\\ ab&\text{
otherwise.}\end{cases}$

and $w=c\ z_{1}\ c\ z_{2}\ c\ \cdots z_{m}\ c$. Let us write $w=x_{1}\cdots
x_{p}$ where $x_{1},\dots,x_{p}$ are letters, and define the formula

$\psi=\textbf{F}(x_{1}\land\textbf{F}(x_{2}\land\textbf{F}(x_{3}\land\textbf{F}(\dots\land\textbf{F}x_{p})))).$

This formula has size $3p-1=3(2kM+3m+1)-1\leq 6kM+9m+2$. We claim that
$\varphi$ is a separating formula. First, note that since all letters in $w$
are non-repeating, $\psi$ is satisfied by exactly the words which have $w$ as
a subword.

  * •

Since $w$ is a subword of $u$, we have that $u$ satisfies $w$.

  * •

Let $j\in[1,n]$. Since $v_{j}$ and $w$ contain the same number of $c$’s, for
$w$ to be a subword of $v_{j}$, $z_{i}$ needs to be a subword of $w_{i,j}$ for
all $i$, i.e., we need to have $y_{i,j}=(ab)^{M+1}$ for all $j\in H$. However,
as $H$ is a hitting set of $(C_{j})_{1\leq j\leq n}$, there exists $j\in H$
such that $i\in C_{j}$ and thus $w_{i,j}=(ab)^{M}$.

∎

The rest of the proof is about proving the converse implication:

######  Proposition 13.

Let $\varphi$ be an $\textbf{LTL}(\textbf{F},\textbf{G},\land,\lor,\neg)$
formula separating $u$ and the $v_{i}$, then we have $k(6M-3)\leq||\varphi||$,
and thus, as $||\varphi||\leq|\varphi|$, this implies $k(6M-3)\leq|\varphi|$.

We define a _separation tree_ of $\varphi$ as a finite tree with each node $x$
labelled by a subformula $\psi^{x}$ of $\varphi$, a set of indices
$I^{x}\subseteq\left\\{1,\ldots,n\right\\}$, a family of numbers
$(J^{x}_{i})_{i\in I^{x}}$ with $J^{x}_{i}\in\left\\{0,\ldots,m\right\\}$ and
two families of words $(P^{x}_{i})_{i\in I},(V^{x}_{i})_{i\in I}$ with
$P^{x}_{i}\in\left\\{\varepsilon,a,b,ab,ba\right\\}$ and $V^{x}_{i}$ a suffix
of $w_{i,J^{x}_{i}}$ for all $i$ (with $w_{i,0}=\varepsilon$ for all $i$).

This tree and labelling must respect the following rules. Those rules should
be understood as follows: imagine two players, one trying to prove that $u$
satisfies the formula $\varphi$ but the $v_{i}$ do not and the other trying to
prove the contrary. The game is defined by induction on the formula. For
instance, if $\varphi$ is of the form $\textbf{F}\psi$, then the first player
will choose a suffix of $u$ on which she claims $\psi$ to be satisfied, and
the second player will do the same for each $v_{i}$. A separation tree
describes a play of this game in which the second player follows a specific
strategy: he tries to copy everything the first player does, and to take a
suffix that is as similar as possible to the current one of the first player.

Here are the rules:

  * •

If $\psi^{x}=\psi_{1}\lor\psi_{2}$ or $\psi=\psi_{1}\land\psi_{2}$ then $x$
has two children $x_{1}$ and $x_{2}$ and $\psi^{x_{1}}=\psi_{1}$,
$\psi^{x_{2}}=\psi_{2}$ and $I^{x}$ is the disjoint union of $I^{x_{1}}$ and
$I^{x_{2}}$, and
$(J_{i}^{x_{1}},P_{i}^{x_{1}},V_{i}^{x_{1}})=(J_{i}^{x},P_{i}^{x},V_{i}^{x})$
for all $i\in I^{x_{1}}$ and
$(J_{i}^{x_{2}},P_{i}^{x_{2}},V_{i}^{x_{2}})=(J_{i}^{x},P_{i}^{x},V_{i}^{x})$
for all $i\in I^{x_{2}}$.

  * •

If $\psi_{x}=\textbf{G}\psi$ then $x$ has one child $y$, $\psi^{y}=\psi$,
$I^{y}=I^{x}$ and either $J_{i}^{y}=J_{i}^{x}$ and $V_{i}^{y}$ is a suffix of
$V_{i}^{x}$ or $0\leq J_{i}^{y}<J_{i}^{x}$ and $V_{i}^{y}$ is a suffix of
$w_{i,J_{i}^{y}}$. In both cases $P_{i}^{y}=\varepsilon$.

  * •

If $\psi_{x}$ is a letter then $x$ is a leaf and all $P_{i}^{x}V_{i}^{x}c$
start with that letter but none of the $V_{i}^{x}c$ do.

  * •

If $\psi_{x}$ is the negation of a letter then $x$ is a leaf and all
$V_{i}^{x}c$ start with that letter but none of the $P_{i}^{x}V_{i}^{x}c$ do.

  * •

If $\psi_{x}=\textbf{F}\psi$ with $\psi$ a boolean combination of formulas all
of the form $\textbf{F}\psi^{\prime}$ or $\textbf{G}\psi^{\prime}$ then $x$
has one child $y$, $\psi^{y}=\psi$ and $I^{y}=I^{x}$. Furthermore, there
exists $(J,U)$ such that for all $i\in I^{x}$ either $J^{x}_{i}=J$ and $U$ is
a suffix of $P^{x}_{i}V^{x}_{i}$ or $J^{x}_{i}<J$ and $U$ is a suffix of
$(ab)^{M+1}$. For all $i$ we have $J^{y}_{i}=J$.

We have $V^{y}_{i}$ equal to the shortest of $U$ and $V^{x}_{i}$ if
$J^{x}_{i}=J^{y}_{i}$ and to the shortest of $U$ and $w_{i,C^{y}_{i}}$
otherwise. In the first case $U$ is a suffix of $P^{x}_{i}V^{x}_{i}$ and in
the second it is a suffix of $abw_{i,J}$. Thus in all cases we can select
$P^{y}_{i}\in\left\\{\varepsilon,a,b,ab,ba\right\\}$ such that
$U=P^{x}_{i}V^{x}_{i}$.

  * •

If $\psi_{x}=\textbf{F}\psi$ with $\psi$ a boolean combination of formulas all
of the form $\textbf{F}\psi^{\prime}$ or $\textbf{G}\psi^{\prime}$ then $x$
has one child $y$, $\psi^{y}=\psi$ and $I^{y}=I^{x}$. Furthermore, there
exists $(J,U)$ such that for all $i\in I^{x}$ either $J^{x}_{i}=J$ and $U$ is
a suffix of $P^{x}_{i}V^{x}_{i}$ or $J^{x}_{i}<J$ and $U$ is a suffix of
$(ab)^{M+1}$. For all $i$ we have $J^{y}_{i}=J$.

For the values of $P^{y}_{i}$ and $V^{y}_{i}$ we have several cases:

    * $\to$

if $J^{y}_{i}>J_{i}^{x}$ then $V^{y}_{i}=U$ and $P^{y}_{i}=\varepsilon$ if $U$
is a suffix of $w_{i,J}$. Otherwise we have $w_{i,J}=(ab)^{M}$ and either
$U=(ab)^{M+1}$, in which case $P_{i}^{y}=ab$ and $V_{i}^{y}=(ab)^{M}$, or
$U=b(ab)^{M}$, and then $P_{i}^{y}=ba$ and $V_{i}^{y}=b(ab)^{M-1}$.

    * $\to$

if $J^{y}_{i}=J_{i}^{x}$ and $U$ is a suffix of $V_{i}^{x}$ then $V^{y}_{i}=U$
and $P^{y}_{i}=\varepsilon$.

    * $\to$

if $J^{y}_{i}=J_{i}^{x}$ and $U=P^{x}_{i}V^{x}_{i}$ then $P_{i}^{y}=P_{i}^{x}$
and $V_{i}^{y}=V^{x}_{i}$.

    * $\to$

if $J^{y}_{i}=J_{i}^{x}$ and $U=aV^{x}_{i}$ and $|V^{x}_{i}|>1$ then
$P_{i}^{y}=ab$. Similarly if $U=bV^{x}_{i}$ and $|V^{x}_{i}|>0$ then
$P_{i}^{y}=ba$. In both cases $V_{i}^{y}$ is such that $U=P^{y}_{i}V^{y}_{i}$.

    * $\to$

if $J^{y}_{i}=J_{i}^{x}$ and $U=aV^{x}_{i}$ and $|V^{x}_{i}|\leq 1$ or if
$U=bV^{x}_{i}$ and $|V^{x}_{i}|=0$ then $i\notin I^{y}$.

This also defines $I^{y}$.

######  Lemma 10.

If $\varphi$ is satisfied by $u$ but none of the $v_{i}$ then there exists a
separation proof tree for $\varphi$ with a root $r$ such that
$I^{r}=\left\\{1,\ldots,n\right\\}$ and for all $i\in I^{r}$, $J^{r}_{i}=0$
and $P^{r}_{i}=V^{r}_{i}=\varepsilon$.

###### Proof.

We prove the following statement:

> Let $\psi\in\textbf{LTL}(\textbf{F},\textbf{G},\land,\lor,\neg)$, let
> $I\subseteq\left\\{1,\ldots,n\right\\}$, let $(J_{i})_{i\in I}$ be a family
> of indices in $\left\\{0,\ldots,m\right\\}$, and let $(P_{i})_{i\in I}$ and
> $(V_{i})_{i\in I}$ be families of words such that for all $i\in I$, we have
> $P_{i}\in\left\\{\varepsilon,a,b,ab,ba\right\\}$, $V_{i}$ is a suffix of
> $w_{i,J_{i}}$ and $P_{i}V_{i}$ is a suffix of $(ab)^{M+1}$. If $\psi$ is
> satisfied by all $u_{i}=P_{i}V_{i}c((ab)^{M+1}c)^{m-J_{i}}$ but none of the
> $v_{i}=V_{i}cw_{i,J_{i}+1}c\cdots w_{i,m}c$, then there exists a separation
> tree with a root $r$ labelled by $I^{r}=I$, $\psi^{r}=\psi$ and
> $(J_{i},P_{i},V_{i})_{i\in I}$.

This implies the lemma.

We proceed by induction on $\psi$.

#### Case 1:

If $\psi$ is a letter then all $u_{i}$ start with that letter but none of the
$v_{i}$ do, thus the same can be said of the $P_{i}V_{i}c$ and $V_{i}c$.

#### Case 2:

Similarly if $\psi$ is the negation of a letter then all $v_{i}$ start with
that letter but none of the $u_{i}$ do, thus the same can be said of the
$V_{i}c$ and $P_{i}V_{i}c$.

#### Case 3:

If $\psi=\psi_{1}\lor\psi_{2}$ then we set $I_{1}=\left\\{i\in I\mid
u_{i}\vDash\psi_{1}\right\\}$ and $I_{2}=I\setminus I_{1}$. As all $u_{i}$
satisfy $\psi$, all $u_{i}$ with $i\in I_{2}$ satisfy $\psi_{2}$. As no
$v_{i}$ satisfies $\psi$, they satisfy neither $\psi_{1}$ nor $\psi_{2}$. By
induction hypothesis there exists a separation tree with a root $r_{1}$ (resp.
$r_{2}$) labelled by $I_{1}$ (resp. $I_{2}$), $\psi_{1}$ (resp. $\psi_{2}$)
and $(J_{i},P_{i},V_{i})_{i\in I_{1}}$ (resp. $(J_{i},P_{i},V_{i})_{i\in
I_{2}}$). The tree with a root $r$ labelled by $I$, $\psi$ and
$(J_{i},P_{i},V_{i})_{i\in I}$ and with those two subtrees as children is a
separation tree. We can proceed similarly when
$\psi^{x}=\psi_{1}\land\psi_{2}$ by setting $I_{1}=\left\\{i\in I\mid
v_{i}\nvDash\psi_{1}\right\\}$.

#### Case 4:

If $\psi=\textbf{G}\psi^{\prime}$ then for all $i$ there exists a suffix
$v^{\prime}_{i}$ of $v_{i}$ not respecting $\psi^{\prime}$. We set
$J^{\prime}_{i}=m-C^{\prime}_{i}$ with $C^{\prime}_{i}$ the number of $c$ in
$v^{\prime}$ and $V^{\prime}_{i}$ the largest prefix of $v^{\prime}_{i}$
without $c$. We also set $P^{\prime}_{i}=\varepsilon$. As $u_{i}$ satisfies
$\textbf{G}\psi^{\prime}$ and as
$u^{\prime}_{i}=V_{i}c((ab)^{M+1}c)^{m-J_{i}}$ is a suffix of $u_{i}$,
$u^{\prime}_{i}$ satisfies $\psi^{\prime}$ By induction hypothesis, there
exists a separation tree $t$ with a root labelled by $I$, $\psi^{\prime}$ and
$(J^{\prime}_{i},P^{\prime}_{i},V^{\prime}_{i})_{i\in I}$. As a result, there
exists a separation tree for $\psi$, obtained by taking a root labelled by
$I$, $\psi^{\prime}$ and $(J^{\prime}_{i},P^{\prime}_{i},V^{\prime}_{i})_{i\in
I}$ and giving it one child whose subtree is $t$.

#### Case 5:

If $\psi=\textbf{F}\psi^{\prime}$ then let $u^{\prime}$ be the shortest suffix
of $u$ satisfying $\psi^{\prime}$. As all $u_{i}$ are suffixes of $u$
satisfying $\psi$, $u^{\prime}$ is a suffix of all $u_{i}$. Let
$J^{\prime}=m-C^{\prime}$ with $C^{\prime}$ the number of $c$ in $u^{\prime}$
and $U^{\prime}$ the largest prefix of $u^{\prime}$ without $c$. For all $i\in
I$ we set $J^{\prime}_{i}=J^{\prime}$. We will define a set
$I^{\prime}\subseteq I$ along the way. For all $i\in I$, if $J^{\prime}=J_{i}$
and $U^{\prime}$ is a suffix of $V_{i}$, or if $J^{\prime}>J_{i}$ and
$U^{\prime}$ is a suffix of $w_{i,J^{\prime}}$, then we can set
$V^{\prime}_{i}=U^{\prime}$ and $P^{\prime}_{i}=\varepsilon$. Then
$v^{\prime}_{i}=V^{\prime}_{i}cw_{i,J^{\prime}+1}\cdots cw_{i,m}c$ is a suffix
of $v_{i}$ and thus does not satisfy $\psi^{\prime}$ (as $v_{i}$ does not
satisfy $\textbf{F}\psi^{\prime}$). Otherwise, we have to distinguish cases
according to the shape of $\psi^{\prime}$.

##### Case 5.1:

Suppose $\psi^{\prime}$ is a boolean combination of formulas of the form
$\textbf{F}\psi^{\prime\prime}$ or $\textbf{G}\psi^{\prime\prime}$.

If $J_{i}=J^{\prime}$ then we set $V^{\prime}_{i}=V_{i}$. In that case
$U^{\prime}$ is a suffix of $P_{i}V_{i}$ and $V_{i}$ is a suffix of $U_{i}$,
hence there exists $P^{\prime}_{i}\in\left\\{\varepsilon,a,b,ab,ba\right\\}$
such that $U^{\prime}=P^{\prime}_{i}V^{\prime}_{i}$. As $v_{i}=v^{\prime}_{i}$
does not satisfy $\textbf{F}\psi^{\prime}$, it does not satisfy
$\psi^{\prime}$ either.

If $J_{i}>J^{\prime}$ then we set $V^{\prime}_{i}=w_{i,J^{\prime}}$. In that
case $U^{\prime}$ is a suffix of $(ab)^{M+1}$ but not of $w_{i,J^{\prime}}$,
hence there exists $P^{\prime}_{i}\in\left\\{\varepsilon,a,b,ab,ba\right\\}$
such that $U^{\prime}=P^{\prime}_{i}V^{\prime}_{i}$. As $v_{i}$ does not
satisfy $\textbf{F}\psi^{\prime}$, and as
$v^{\prime}_{i}=V^{\prime}_{i}cw_{i,J^{\prime}+1}\cdots cw_{i,m}c$ is a suffix
of $v_{i}$, $v^{\prime}_{i}$ does not satisfy $\psi^{\prime}$.

##### Case 5.2:

Now suppose $\psi^{\prime}$ is a boolean combination of formulas of which at
least one is a letter or its negation.

If $J_{i}=J^{\prime}$ and $U^{\prime}$ starts with $aba$ then we set
$P^{\prime}_{i}=ab$ and $V^{\prime}_{i}$ such that
$U^{\prime}=abV^{\prime}_{i}$. As $U^{\prime}$ is a suffix of $P_{i}V_{i}$ and
$|P_{i}|\leq 2$, $V^{\prime}_{i}$ is a suffix of $V_{i}$. As a result,
$v^{\prime}_{i}=V^{\prime}_{i}cw_{i,J^{\prime}+1}\cdots cw_{i,m}c$ is a suffix
of $v_{i}$, hence it does not satisfy $\psi^{\prime}$.

Similarly, if $J_{i}=J^{\prime}$ and $U^{\prime}$ starts with $bab$ then we
set $P^{\prime}_{i}=ba$ and $V^{\prime}_{i}$ such that
$U^{\prime}=baV^{\prime}_{i}$. Again, as $U^{\prime}$ is a suffix of
$P_{i}V_{i}$ and $|P_{i}|\leq 2$, $V^{\prime}_{i}$ is a suffix of $V_{i}$. As
a result, $v^{\prime}_{i}=V^{\prime}_{i}cw_{i,J^{\prime}+1}\cdots cw_{i,m}c$
is a suffix of $v_{i}$, hence it does not satisfy $\psi^{\prime}$.

If $J_{i}=J^{\prime}$ and $|U^{\prime}|\leq 2$ then $i\notin I^{\prime}$.

If $J_{i}<J^{\prime}$ then as $U^{\prime}$ is not a suffix of
$w_{i,J^{\prime}}$ we must have $w_{i,J^{\prime}}=(ab)^{M}$ and $U^{\prime}$
is either $(ab)^{M+1}$ or $b(ab)^{M}$. If $U^{\prime}=(ab)^{M+1}$ then we set
$P^{\prime}_{i}=ab$ and $V^{\prime}_{i}=(ab)^{M}$. As
$v^{\prime}_{i}=V^{\prime}_{i}cw_{i,J^{\prime}+1}\cdots cw_{i,m}c$ is a suffix
of $v_{i}$, it does not satisfy $\psi^{\prime}$.

Similarly if $U^{\prime}=b(ab)^{M}$ then we set $P^{\prime}_{i}=ba$ and
$V^{\prime}_{i}=b(ab)^{M-1}$. Since
$v^{\prime}_{i}=V^{\prime}_{i}cw_{i,J^{\prime}+1}\cdots cw_{i,m}c$ is a suffix
of $v_{i}$, it does not satisfy $\psi^{\prime}$. We can then apply the
induction hypothesis to obtain a separation tree $t$ whose root is labelled by
$I^{\prime}$, $\psi^{\prime}$ and
$(J^{\prime}_{i},P^{\prime}_{i},V^{\prime}_{i})_{i\in I^{\prime}}$. We obtain
the result by taking a tree whose root is labelled by $I$, $\psi$ and
$(J_{i},P_{i},V_{i})_{i\in I}$ and giving it one child whose subtree is $t$.

This concludes our induction. ∎

######  Lemma 11.

If there exists a separation proof tree for $\varphi$ then $||\varphi||\geq
6k(M-1)$.

###### Proof.

We make some key observations. Let $x$ be a node labelled by some letter or
its negation. Then:

  * •

either $x$ only has ancestors labelled by formulas of the form
$\varphi_{1}\lor\varphi_{2}$ or $\varphi_{1}\land\varphi_{2}$, in which case
$P_{i}^{x}V_{i}^{x}c$ and $V_{i}^{x}c$ both start with $c$.

  * •

or $x$ has an ancestor labelled by a formula of the form $\textbf{F}\varphi$
or $\textbf{G}\varphi$. Let $y$ be its closest such ancestor, and $z$ the only
child of $y$. Then $\psi^{y}$ is of the form $\textbf{F}\psi^{z}$ or
$\textbf{G}\psi^{z}$ with $\psi^{z}$ a boolean combination of formulas
including $\psi^{x}$ (which is a letter or its negation).

Hence for all $i\in I^{z}$ we have that $P^{z}_{i}V^{z}_{i}c$ and $V^{z}_{i}c$
start with the same letter. Moreover as all nodes from $z$ to $x$ are labelled
by formulas of the form $\psi_{1}\lor\psi_{2}$ or $\psi_{1}\land\psi_{2}$, we
have $I^{x}\subseteq I^{z}$ and $P^{x}_{i}V^{x}_{i}c=P^{x}_{i}V^{x}_{i}c$ and
$V^{z}_{i}c=V^{x}_{i}c$ for all $i\in I^{x}$. As a result, by definition of a
separation tree, we must have $I^{x}=\emptyset$.

Thus for all node $x$, if $x$ is a leaf then $I^{x}=\emptyset$. Furthermore,
if $x$ has two children $y$ and $z$ then $I^{x}$ is the disjoint union of
$I^{y}$ and $I^{z}$, and if $x$ has a single child $y$ then $I^{y}\subseteq
I^{x}$. Those facts are direct consequences of the definition of separation
tree.

The second key observation is that if $y$ is a child of $x$ and
$J^{x}_{i}=J^{y}_{i}$ and $P^{y}_{i}\neq\varepsilon$ for some $i$ then
$P^{x}_{i}\neq\varepsilon$ and $|V_{i}^{y}|\geq|V_{i}^{x}|-1$. If furthermore
$|V_{i}^{y}|=|V_{i}^{x}|-1$ then $\psi^{x}$ is of the form
$\textbf{F}\psi^{y}$ with $\psi^{y}$ a boolean combination of formulas
including at least one letter or its negation.

The third observation is that if $y$ is a child of $x$ and
$J^{x}_{i}<J^{y}_{i}$ and $P^{y}_{i}\neq\varepsilon$ for some $i$ then
$|V_{i}^{y}|\geq 2M-1$ and $w_{i,J_{i}^{y}}=(ab)^{M}$.

Let $i\in\left\\{1,\ldots,n\right\\}$. In light of the previous observations,
there is a branch of the tree $x_{1},\ldots,x_{k+1}$ ($x_{j+1}$ being a child
of $x_{j}$ for all $j$) such that $i$ is in $I^{x_{j}}$ for all $j\leq k$ but
not in $I^{x_{k+1}}$. As $i\in I^{x_{k}}$ but $i\notin I^{x_{k+1}}$, we have
$J_{i}^{x_{k+1}}=J_{i}^{x_{k}}$ and $|V_{i}^{x_{k}}|\leq 1$ and
$P_{i}^{x_{k}}\neq\varepsilon$. Let $j$ be the minimal index such that
$J_{i}^{x_{j}}=J_{i}^{x_{k+1}}$. As the sequence of $J_{i}^{x_{\ell}}$ is non-
increasing, all $J_{i}^{x_{\ell}}$ are equal for $j\leq\ell\leq k+1$. Thanks
to the previous remarks, we infer that $P_{i}^{x_{\ell}}\neq\varepsilon$ for
all $j\leq\ell\leq k+1$. Therefore $x_{j}$ cannot be the root, hence $j>1$. As
a consequence, by our third remark, we have $|V_{i}^{x_{j}}|\geq 2M-1$ and
$w_{i,J_{i}^{x_{j}}}=(ab)^{M}$. Furthermore $|V_{i}^{x_{k}}|\leq 1$. Our
second remark allows us to conclude that there exist at least $2M-2$ nodes
$x_{\ell}$ such that $\psi^{x_{\ell}}$ is of the form
$\textbf{F}\psi^{x_{\ell+1}}$ with $\psi^{x_{\ell+1}}$ a boolean combination
of formulas including at least one letter or its negation. For each such
$\ell$, $x_{\ell+1}$ and the leaf corresponding to that letter (or its
negation) are all labelled by $J_{i}^{x_{\ell}}$. Hence for all $i$ there
exists $J_{i}$ such that $w_{i,J_{i}}=(ab)^{M}$ and $J_{i}^{x}=J_{i}$ for at
least $6M-6$ distinct nodes in the separation tree. As $w_{i,J_{i}}=(ab)^{M}$,
we have $i\in T_{J_{i}}$ for all $i$, hence the set of $J_{i}$ is a solution
to the set cover problem. As a result, there are at least $k$ distinct
$J_{i}$, and thus there are at least $6k(M-1)$ nodes in the separation tree.
As the size of the separation tree is exactly $||\varphi||$, we obtain the
result. ∎

We may now finish the proof of Theorem 9. Recall that we considered an input
$S=\left\\{1,\ldots,m\right\\}$, $T_{1},\ldots,T_{n}\subseteq S$ and
$k^{\prime}\in\mathbb{N}$ (the encoding is irrelevant). We set $k$ to be the
size of a minimal hitting set of $H\subseteq S$ hitting all $T_{i}$, and
$M=3m+2$.

Let $\varphi$ be a formula of minimal size satisfied by $u$ but not by any
$v_{i}$. By Proposition 13 and Claim 1, we have $6kM-3k\leq|\varphi|\leq
6kM+9m+2$. We set $K=6k^{\prime}M+9m+2$ and show that $k^{\prime}\geq k$ if
and only if $|\varphi|\leq K$.

  * •

Suppose $k^{\prime}\geq k$, then $K\geq 6kM+9m+2\geq|\varphi|$.

  * •

Suppose $k^{\prime}\leq k-1$, then $K\leq
6(k-1)M+9m+2=18km-9m+12k-10\leq(6kM-3k)-9m+3k-10<6kM-3k\leq|\varphi|$ as
$k\leq m$.

As a result, the hitting set problem has a positive answer on instance
$S,T_{1},\ldots,T_{n},k^{\prime}$ if and only if so does the
$\textbf{LTL}(Op)$ learning problem on instance $u,v_{1},\ldots,v_{n},K$. As
the latter instance is constructible in polynomial time from the former,
Theorem 9 is proven.

### Dual hardness result

We now show hardness for fragments with operators G and $\lor$. As we allowed
negation in the previous result, we can infer that one almost directly.

######  Theorem 10.

For all $\left\\{\textbf{G},\lor\right\\}\subseteq
Op\subseteq\left\\{\textbf{F},\textbf{G},\land,\lor,\neg\right\\}$, the
learning problem for $\textbf{LTL}(Op)$ is -hard even for an alphabet of size
$3$.

We take the same instance of the hitting problem, but this time we consider
the $\textbf{LTL}(Op)$ learning problem with the $v_{i}$ as positive words and
$u$ as the only negative one.

######  Corollary 1.

Let $\varphi$ be an $\textbf{LTL}(\land,\lor,\neg,F,G)$ formula separating the
$u_{i}$ and $v$, then we have: $k(6M-3)\leq|\varphi|$.

###### Proof.

Let $\varphi$ be such a formula, and let $\overline{\varphi}$ be its negation,
with the negations pushed to the bottom. Formally, $\overline{\varphi}$ is
defined by induction on $\varphi$:

  * •

$\overline{a}=\neg a$

  * •

$\overline{\varphi_{1}\land\varphi_{2}}=\overline{\varphi_{1}}\lor\overline{\varphi_{2}}$

  * •

$\overline{\varphi_{1}\lor\varphi_{2}}=\overline{\varphi_{1}}\land\overline{\varphi_{2}}$

  * •

$\overline{\textbf{F}\varphi_{1}}=\textbf{G}\overline{\varphi_{1}}$

  * •

$\overline{\textbf{G}\varphi_{1}}=\textbf{F}\overline{\varphi_{1}}$

A clear induction shows that a word satisfies one if and only if it does not
satisfy the other (note that this would not be true if we allowed the operator
X). Hence $\overline{\varphi}$ is satisfied by $u$ but not by the $v_{i}$, so
by Theorem 9 we have $k(6M-3)\leq||\overline{\varphi}||=|\varphi|$. ∎

######  Lemma 12.

There exists a formula $\varphi$ of $\textbf{LTL}(\textbf{G},\lor)$ separating
the $u_{i}$ and $v$ with $|\varphi|\leq 6kM+11m+4$.

###### Proof.

Let $J$ be a cover of $S$ of size $k$. We set, for all $1\leq i\leq n$,

$z_{j}=\begin{cases}(ab)^{M+1}&\text{ if }j\in J,\\\ ab&\text{
otherwise.}\end{cases}$

and we set $w=cz_{1}cz_{2}c\cdots z_{m}c$. We use the formula
$\psi=\textbf{G}(\bar{x_{1}}\lor\textbf{G}(\bar{x_{2}}\lor\textbf{G}(\bar{x_{3}}\lor\textbf{G}(...\lor\textbf{G}\bar{x_{p}}))))$,
where $x_{1},\ldots,x_{p}$ are letters such that $x_{1}\cdots x_{p}=w$,
$\bar{a}=b$, $\bar{b}=a$ and $\bar{c}=a\lor b$. This formula has size
$3p-1+2m+2=3(2kM+3m+1)+2m+1\leq 6kM+11m+4$.

Observe that $\psi$ is satisfied by exactly the words which do not have any
$w^{\prime}$ as a weak subword, with $w^{\prime}\in(2^{\Sigma})^{*}$ obtained
by replacing each $c$ by $\left\\{c\right\\}$, $a$ by $\left\\{a,c\right\\}$
and $b$ by $\left\\{b,c\right\\}$. As $w$ is a weak subword of $v$, so is
$w^{\prime}$, hence $v$ does not satisfy $\varphi$. Let $i\in S$, as $u_{i}$
and $w$ contain the same number of $c$, for $u_{i}$ to not satisfy the
formula, $z_{j}$ needs to be a subword of $y_{i,j}$ for all $j$, i.e., we need
to have $y_{i,j}=(ab)^{M+1}$ for all $j\in J$. However, as $J$ is a cover of
$S$, there exists $j\in J$ such that $i\in C_{j}$ and thus $y_{i,j}=(ab)^{M}$.
Therefore all $u_{i}$ satisfy the formula. ∎

Let $\varphi$ be a formula of minimal size satisfied by all $v_{i}$ but not by
$u$. By Proposition 1 and Lemma 12, we have $6kM-3k\leq|\varphi|\leq
6kM+11m+4$.

We set $K=6k^{\prime}M+11m+4$ and show that $k^{\prime}\geq k$ if and only if
$|\varphi|\leq K$.

  * •

Suppose $k^{\prime}\geq k$, then $K\geq 6kM+11m+4\geq|\varphi|$.

  * •

Suppose $k^{\prime}\leq k-1$, then $K\leq
6(k-1)M+11m+4=18km-7m+12k-8\leq(6kM-3k)-7m+3k-8<6kM-3k\leq|\varphi|$ as $k\leq
m$.

As a result, the hitting set problem has a positive answer on instance
$S,T_{1},\ldots,T_{n},k^{\prime}$ if and only if so does the
$\textbf{LTL}(Op)$ learning problem on instance $u,v_{1},\ldots,v_{n},K$. As
the latter instance is constructible in polynomial time from the former,
Theorem 10 is proven.

##  9 Perspectives and open problems

In this paper, we showed $\NP$-completeness of the LTL learning problem for
all fragments which do not include the until operator. The same holds adding
until for non-constant size alphabets. Hence the main open question is the
following:

######  Open problem 1.

Is the learning problem $\NP$-complete for full LTL with constant size
alphabet?

We consider LTL over finite traces; some of the related works we discussed in
the introduction actually considered infinite traces as common in the
verification research community. All our hardness results easily transfer to
the infinite trace case, simply by extending finite traces into infinite ones
with a new symbol. In particular, we obtain as corollary that the LTL learning
problem is $\NP$-hard for infinite traces when the alphabet is part of the
input.

The negative results in this paper suggest looking for approximation
algorithms. Beyond $\textbf{LTL}(\textbf{X},\land)$, nothing is known in terms
of upper and lower bounds on polynomial time approximation algorithms, leaving
an open field of exciting research directions. In the same vein, one could
wonder about the parameterized complexity of the LTL learning problem, in
particular when fixing the number of words. We leave this question open and
hope to inspire further studies!

## References

  * Baharisangari, Gaglione, Neider, Topcu, & Xu Baharisangari, N., Gaglione, J., Neider, D., Topcu, U., & Xu, Z. (2021).  Uncertainty-aware signal temporal logic inference.  In Bloem, R., Dimitrova, R., Fan, C., & Sharygina, N. (Eds.), International Conference on Software Verification, VSTTE, Vol. 13124 of Lecture Notes in Computer Science, pp. 61–85. Springer.
  * Bombara, Vasile, Penedo Alvarez, Yasuoka, & Belta Bombara, G., Vasile, C. I., Penedo Alvarez, F., Yasuoka, H., & Belta, C. (2016).  A Decision Tree Approach to Data Classification using Signal Temporal Logic.  In Hybrid Systems: Computation and Control, HSCC.
  * Camacho & McIlraith Camacho, A., & McIlraith, S. A. (2019).  Learning interpretable models expressed in linear temporal logic.  International Conference on Automated Planning and Scheduling, ICAPS, 29.
  * Dinur & Steurer Dinur, I., & Steurer, D. (2014).  Analytical approach to parallel repetition.  In Symposium on Theory of Computing, STOC, pp. 624–633.
  * Ehlers, Gavran, & Neider Ehlers, R., Gavran, I., & Neider, D. (2020).  Learning properties in LTL $\cap$ ACTL from positive examples only.  In Formal Methods in Computer Aided Design, FMCAD.
  * Fijalkow & Lagarde Fijalkow, N., & Lagarde, G. (2021).  The complexity of learning linear temporal formulas from examples.  In Chandlee, J., Eyraud, R., Heinz, J., Jardine, A., & van Zaanen, M. (Eds.), International Conference on Grammatical Inference, ICGI, Vol. 153 of Proceedings of Machine Learning Research, pp. 237–250. PMLR.
  * Gaglione, Neider, Roy, Topcu, & Xu Gaglione, J., Neider, D., Roy, R., Topcu, U., & Xu, Z. (2022).  Maxsat-based temporal logic inference from noisy data.  Innovations in Systems and Software Engineering, 18(3), 427–442.
  * Gold Gold, E. M. (1978).  Complexity of automaton identification from given data.  Information and Control, 37(3), 302–320.
  * Kim, Muise, Shah, Agarwal, & Shah Kim, J., Muise, C., Shah, A., Agarwal, S., & Shah, J. (2019).  Bayesian inference of linear temporal logic specifications for contrastive explanations.  In International Joint Conference on Artificial Intelligence, IJCAI.
  * Lemieux, Park, & Beschastnikh Lemieux, C., Park, D., & Beschastnikh, I. (2015).  General LTL specification mining.  In International Conference on Automated Software Engineering, (ASE).
  * Lutz, Neider, & Roy Lutz, S., Neider, D., & Roy, R. (2023).  Specification sketching for linear temporal logic.  In André, É., & Sun, J. (Eds.), International Symposium on Automated Technology for Verification and Analysis, ATVA, Vol. 14216 of Lecture Notes in Computer Science, pp. 26–48. Springer.
  * Neider & Gavran Neider, D., & Gavran, I. (2018).  Learning linear temporal properties.  In Formal Methods in Computer Aided Design, FMCAD, pp. 1–10.
  * Pitt & Warmuth Pitt, L., & Warmuth, M. K. (1993).  The minimum consistent DFA problem cannot be approximated within any polynomial.  Journal of the ACM, 40(1), 95–142.
  * Pnueli Pnueli, A. (1977).  The temporal logic of programs.  In Symposium on Foundations of Computer Science, SFCS.
  * Raha, Roy, Fijalkow, & Neider Raha, R., Roy, R., Fijalkow, N., & Neider, D. (2022).  Scalable anytime algorithms for learning fragments of linear temporal logic.  In Fisman, D., & Rosu, G. (Eds.), International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Vol. 13243 of Lecture Notes in Computer Science, pp. 263–280. Springer.
  * Raha, Roy, Fijalkow, Neider, & Pérez Raha, R., Roy, R., Fijalkow, N., Neider, D., & Pérez, G. A. (2024).  Synthesizing efficiently monitorable formulas in metric temporal logic.  In International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI.
  * Roy, Fisman, & Neider Roy, R., Fisman, D., & Neider, D. (2020).  Learning interpretable models in the property specification language.  In International Joint Conference on Artificial Intelligence, IJCAI.