# Inferring Symbolic Automata

Dana Fisman  Ben-Gurion University, Be’er Sheva, Israel  ,  Hadar Frenkel
CISPA Helmholtz Center for Information Security, Saarbrücken, Germany  and
Sandra Zilles  University of Regina, Regina, Canada

###### Abstract.

We study the learnability of _symbolic finite state automata_ (SFA), a model
shown useful in many applications in software verification. The state-of-the-
art literature on this topic follows the _query learning_ paradigm, and so far
all obtained results are positive. We provide a necessary condition for
efficient learnability of SFAs in this paradigm, from which we obtain the
first negative result.

The main focus of our work lies in the learnability of SFAs under the paradigm
of _identification in the limit using polynomial time and data_ , and its
strengthening _efficient identifiability_ , which are concerned with the
existence of a systematic set of _characteristic samples_ from which a learner
can correctly infer the target language. We provide a necessary condition for
identification of SFAs in the limit using polynomial time and data, and a
sufficient condition for efficient learnability of SFAs. From these conditions
we derive a positive and a negative result.

Since the performance of a learning algorithm is bounded as a function of the
size of the representation of the target language and since SFAs, in general,
do not have a canonical form, and there are trade-offs between the complexity
of the predicates on the transitions and the number of transitions, we start
by defining size measures for SFAs. We revisit the complexity of procedures on
SFAs and analyze them according to these measures, paying attention to the
special forms of SFAs: _normalized SFAs_ and _neat SFAs_ , as well as to SFAs
over a _monotonic_ effective Boolean algebra.

This is an extended version of the paper with the same title published in
CSL’22 [FFZ22].

##  1\. Introduction

_Symbolic finite state automata_ , SFAs for short, are an automata model in
which transitions between states correspond to predicates over a domain of
concrete alphabet letters. Their purpose is to cope with situations where the
domain of concrete alphabet letters is large or infinite. As an example for
automata over finite large alphabets consider automata over the alphabet
$2^{AP}$ where ${AP}$ is a set of atomic propositions; these are used in model
checking [CGP01, BK08]. Another example, used in string sanitizer algorithms
[HLM+11], are automata over predicates on the Unicode alphabet which consists
of over a million symbols. An infinite alphabet is used for example in _event
recording automata_ , a determinizable class of timed automata [AFH99] in
which an alphabet letter consists of both a symbol from a finite alphabet, and
a non-negative real number. Formally, the transition predicates in an SFA are
defined with respect to an effective Boolean algebra as defined in section 2.

SFAs have proven useful in many applications [DVLM14, PGLM15, ASJ+16, HD17,
SV17, MRA+17] and consequently have been studied as a theoretical model of
automata. Many algorithms for natural questions over these automata already
exist in the literature, in particular, Boolean operations, determinization,
and emptiness [VdHT10]; minimization [DV16]; and language inclusion [KT14].
Recently the subject of learning automata in verification has also attracted
attention, as it has been shown useful in many applications, see Vaandrager’s
survey [Vaa17].

There already exists substantial literature on learning restricted forms of
SFAs [GJL10, MM14, ASKK16, MM17, CDYS17], as well as general SFAs [DD17,
AD18], and even non-deterministic residual SFAs [CHYS19]. For other types of
automata over infinite alphabets, [HSM11] suggests learning abstractions, and
[She19] presents a learning algorithm for deterministic variable automata. All
these works consider the query learning paradigm, and provide extensions to
Angluin’s ${{\textbf{L}}}^{*}$ algorithm for learning DFAs using membership
and equivalence queries [Ang87]. Unique to these works is the work [AD18]
which studies the learnability of SFAs taking as a parameter the learnability
of the underlying algebras, providing positive results regarding specific
Boolean algebras.

One of our contributions is to demonstrate that these positive learnability
results are far from trivial. In particular, we show that there are
limitations to the power of membership and equivalence queries when it comes
to learning SFAs. To do so, we provide a necessary condition for efficient
learnability of SFAs in the query learning paradigm, from which we obtain a
negative result regarding query learning of SFAs over the propositional
algebra. This is, to the best of our knowledge, the first negative result on
learning SFAs with membership and equivalence queries and thus gives useful
insights into the limitations of the ${{\textbf{L}}}^{*}$ framework in this
context.

The main focus of our work lies on the learning paradigm of _identification in
the limit using polynomial time and data_. We are interested in providing
sufficient or necessary conditions for a class of SFAs to be learnable under
this paradigm. To this end, we show that the type of the algebra, in
particular whether it is monotonic or not, largely influences the learnability
of the class.

Learnability of a class of languages in a certain paradigm greatly depends on
the representation chosen for the language. For instance, regular languages
are efficiently learnable (both in the paradigm of identification in the limit
using polynomial time and data, and in the query learning paradigm using
membership and equivalence queries) when represented as DFAs but not when
represented as NFAs. While we are interested in SFAs as the representations,
there are various types of SFAs (with the same expressive power), and the
learnabilty results for them may vary.

The literature on SFAs has mainly focused on a special type of SFA, termed
_normalized_ , in which there is at most one transition between every pair of
states. This minimization of the number of transitions comes at the cost of
obtaining more complex predicates. We consider also another special type of
SFAs, that we term a _neat SFAs_ , which by contrast, allows several
transitions between the same pair of states, but restricts the predicates to
be _basic_ , as formally defined in subsection 2.1.

To get on the right track, we first take a global look at the complexity of
the standard operations on SFAs, and how they vary according to the special
form. We revisit the results in the literature and analyze them along the
measures we find adequate for a size of an SFA: the number of states ($n$),
the number of transitions ($m$) and the size of the most complex predicate
($l$).111 Previous results have concentrated mainly on the number of states.
The results show that most procedures are more efficient on neat SFAs.

We then turn to study identification of SFAs in the limit using polynomial
time and data. We provide a necessary condition a class of SFAs ${\mathbb{M}}$
should meet in order to be identified in the limit using polynomial time and
data, and a sufficient condition a class of SFAs ${\mathbb{M}}$ should meet in
order to be efficiently identifiable. These conditions are expressed in terms
of the existence of certain efficiently computable functions, which we call
${\textsf{Generalize}}_{\mathbb{M}}$, ${\textsf{Concretize}}_{\mathbb{M}}$,
and ${\textsf{Decontaminate}}_{\mathbb{M}}$. We then provide positive and
negative results regarding the learnability of specific classes of SFAs in
this paradigm. In particular, we show the class of SFAs over _any_ monotonic
algebra is efficiently identifiable.

##### Comparison to the conference version

Preliminary results of this work appear in [FFZ22]. This paper extends the
results of [FFZ22] by adding a thorough discussion of the different SFA types
and their effect on the complexity on different automata procedures; as well
as a new theorem regarding efficient learnability, and additional examples for
learning SFAs. In particular, sections 3, 4, and 5, are all new, as well as
Theorem 9 and Examples 10 and 10.

##### Outline

The rest of the paper is organized as follows. In section 2 we provide the
necessary definitions on effective Boolean algebras and SFAs. Section 3
introduces the special forms of SFAs. In section 4 we discuss transformations
between the special forms. Section 5 then reviews the complexity of standard
automata procedures along the mentioned parameters.

We then turn to discuss the learnability of symbolic automata. Section 6
provides a short overview and definitions regarding learnability of SFAs. In
section 7 we discuss the paradigm of learnability in the limit using
polynomial time and data, and provide an overview of learning DFAs in this
paradigm. Sections 8 and 9 present a necessary condition and a sufficient
condition for the efficient learnability of SFAs, and sections 10 and 11 use
these conditions to prove a positive result on the learnability of SFAs over
monotonic algebras, and a negative result on the learnability of SFAs over the
propositional algebra. Section 12 discusses query learning of SFAs and
provides a negative result. We conclude in section Acknowledgments with a
short discussion.

##  2\. Preliminaries

###  2.1. Effective Boolean Algebra

_A Boolean Algebra_ $\mathpzc{A}$ can be represented as a tuple
$(\mathbb{D},{\mathbb{P}},\llbracket{\cdot}\rrbracket,\bot,\top,\vee,$
$\wedge,\neg)$ where $\mathbb{D}$ is a set of domain elements; ${\mathbb{P}}$
is a set of predicates closed under the Boolean connectives, where
$\bot,\top\in{\mathbb{P}}$; the component
$\llbracket{\cdot}\rrbracket:{\mathbb{P}}\rightarrow 2^{\mathbb{D}}$ is the
so-called _semantics function_. It satisfies the following three requirements:
(i) $\llbracket{\bot}\rrbracket=\emptyset$, (ii)
$\llbracket{\top}\rrbracket=\mathbb{D}$, and (iii) for all
$\varphi,\psi\in{\mathbb{P}}$,
$~{}\llbracket{\varphi\vee\psi}\rrbracket=\llbracket{\varphi}\rrbracket\cup\llbracket{\psi}\rrbracket$,
$~{}\llbracket{\varphi\wedge\psi}\rrbracket=\llbracket{\varphi}\rrbracket\cap\llbracket{\psi}\rrbracket$,
and
$\llbracket{\neg\varphi}\rrbracket=\mathbb{D}\setminus\llbracket{\psi}\rrbracket$.
A Boolean Algebra is _effective_ if all the operations above, as well as
satisfiability, are decidable. Henceforth, we implicitly assume Boolean
algebras to be effective.

One way to define a Boolean algebra is by defining a set ${\mathbb{P}}_{0}$ of
_atomic formulas_ that includes $\top$ and $\bot$ and obtaining ${\mathbb{P}}$
by closing ${\mathbb{P}}_{0}$ for conjunction, disjunction and negation. For a
predicate $\psi\in{\mathbb{P}}$ we say that $\psi$ is _atomic_ if
$\psi\in{\mathbb{P}}_{0}$. We say that $\psi$ is _basic_ if $\psi$ is a
conjunction of atomic formulas.

We now introduce two Boolean algebras that are discussed extensively in the
paper.

##### The Interval Algebra

is the Boolean algebra in which the domain $\mathbb{D}$ is the set
$\mathbb{Z}\cup\\{-\infty,\infty\\}$ of integers augmented with two special
symbols with their standard semantics, and the set of atomic formulas
${\mathbb{P}}_{0}$ consists of intervals of the form $[a,b)$ where
$a,b\in\mathbb{D}$. The semantics associated with intervals is the natural
one: $\llbracket{[a,b)}\rrbracket=\\{z\in\mathbb{D}~{}|~{}a\leq z\mbox{ and
}z<b\\}$. If $a>b$ then $\llbracket{[a,b)}\rrbracket=\emptyset$ and we have
that $[a,b)$ is semantically equivalent to $\bot$.

##### The Propositional Algebra

is defined with respect to a set $AP=\\{p_{1},p_{2},\ldots,p_{k}\\}$ of atomic
propositions. The set of _atomic predicates_ $\mathbb{P}_{0}$ consists of the
atomic propositions and their negations as well as $\top$ and $\bot$. The
domain $\mathbb{D}$ consists of all the possible valuations for these
propositions, thus it is $\mathbb{B}^{k}$ where $\mathbb{B}\\!=\\!\\{0,1\\}$.
The semantics of an atomic predicate $p$ is given by
$\llbracket{p_{i}}\rrbracket=\\{v\in\mathbb{B}^{k}~{}|~{}v[i]=1\\}$, and
similarly $\llbracket{\neg
p_{i}}\rrbracket=\\{v\in\mathbb{B}^{k}~{}|~{}v[i]=0\\}$.222In this case a
basic formula is a _monomial_.

####  2.1.1. Predicate Size

In order to reason about the complexity of operations over the Boolean algebra
(and later, the efficient learnability of SFAs using such Boolean algebras),
we need some measure of the size of predicates. We assume the algebra is
associated with a function
$\mathit{size}^{{\mathbb{P}}}:\mathbb{P}\rightarrow\mathbb{N}$ returning for
each predicate its size. If the algebra is defined via a set of atomic
propositions, one can assume the existence of functions
$\mathit{size}^{{\mathbb{P}}}:\mathbb{P}_{0}\rightarrow\mathbb{N}$,
$\mathit{size}^{{\mathbb{P}}}_{\wedge}:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$,
$\mathit{size}^{{\mathbb{P}}}_{\vee}:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$,
$\mathit{size}^{{\mathbb{P}}}_{\neg}:\mathbb{N}\rightarrow\mathbb{N}$
according to which the size of predicates can inductively be computed. Note
that the size is a property of the predicate, not the set of concrete elements
it represents.

For the interval algebra, we define the size of one interval to be $1$, and
the size of a general predicate as the size of its parse tree, where leaves
are single intervals (whose size is $1$). Thus for example
$\mathit{size}^{{\mathbb{P}}}(([0,50)\vee[100,200))\wedge[20,60))$ is $5$
whereas the size of the semantically equivalent predicate $[20,50)$ is $1$.

Similarly, for the propositional algebra we define the size of a predicate to
be the size of its parse tree. Note that Boolean functions from
$\mathbb{B}^{k}$ to $\mathbb{B}$ can be represented in other ways as well,
e.g., using Binary Decision Diagrams (BDDs) [Bry86]. This would result in a
different Boolean algebra (where predicated are BDDs) with a different size
measure for predicates.

###  2.2. Symbolic Automata

A _symbolic finite automaton_ (SFA) is a tuple
$\mathcal{M}=(\mathpzc{A},Q,q_{\iota},F,\Delta)$ where $\mathpzc{A}$ is a
Boolean algebra, $Q$ is a finite set of states, $q_{\iota}\in Q$ is the
initial state, $F\subseteq Q$ is the set of final states, and $\Delta\subseteq
Q\times{\mathbb{P}}{A}\times Q$ is a finite set of transitions, where
${\mathbb{P}}{A}$ is the set of predicates of $\mathpzc{A}$.

We use the term _letters_ for elements of $\mathbb{D}$ where $\mathbb{D}$ is
the domain of $\mathpzc{A}$, and the term _words_ for elements of
$\mathbb{D}^{*}$. A run of $\mathcal{M}$ on a word $a_{1}a_{2}\ldots a_{n}$ is
a sequence of transitions $\langle q_{0},\psi_{1},q_{1}\rangle\langle
q_{1},\psi_{2},q_{2}\rangle\ldots\langle q_{n-1},\psi_{n},q_{n}\rangle$
satisfying that $a_{i}\in\llbracket{\psi_{i}}\rrbracket$, that $\langle
q_{i},\psi_{i+1},q_{i+1}\rangle\in\Delta$ and that $q_{0}=q_{\iota}$. Such a
run is said to be _accepting_ if $q_{n}\in F$. A word $w=a_{1}a_{2}\ldots
a_{n}$ is said to be _accepted_ by $\mathcal{M}$ if there exists an accepting
run of $\mathcal{M}$ on $w$. The set of words accepted by an SFA $\mathcal{M}$
is denoted $\mathcal{L}({\mathcal{M}})$. We use
$\hat{\mathcal{L}}({\mathcal{M}})$ for the set of labeled words
$\hat{\mathcal{L}}({\mathcal{M}})=\\{(w,1)~{}|~{}w\in\mathcal{L}({\mathcal{M}})\\}\cup\\{(w,0)~{}|~{}w\notin\mathcal{L}({\mathcal{M}})\\}$.

An SFA is said to be _deterministic_ if for every state $q\in Q$ and every
letter $a\in\mathbb{D}$ we have that $|\\{\langle
q,\psi,q^{\prime}\rangle\in\Delta~{}|~{}a\in\llbracket{\psi}\rrbracket\\}|\leq
1$, namely from every state and every concrete letter there exists at most one
transition. It is said to be _complete_ if $|\\{\langle
q,\psi,q^{\prime}\rangle\in\Delta~{}|~{}a\in\llbracket{\psi}\rrbracket\\}|\geq
1$ for every $q\in Q$ and $a\in\mathbb{D}$, namely from every state and every
concrete letter there exists at least one transition. It is not hard to see
that, as is the case for finite

$q_{0}$$q_{1}$$[0,100)$$[0,200)$$[100,\infty)$$[200,\infty)$

Figure 1. The SFA $\mathcal{M}$ over ${\mathpzc{A_{\mathbb{N}}}}$

automata (over concrete alphabets), non-determinism does not add expressive
power but does add succinctness. When $\mathcal{A}$ is deterministic we use
$\Delta(q,w)$ to denote the state $\mathcal{A}$ reaches on reading the word
$w$ from state $q$. If $\Delta(q_{\iota},w)=q$ then $w$ is termed an _access
word to state_ $q$. If $w$ is the smallest access word according to
lexicographic order we say that $w$ is the _lex-access_ word to state $q$.

Consider the SFA $\mathcal{M}$ given in Figure 1. It is defined over the
algebra ${\mathpzc{A_{\mathbb{N}}}}$ which is the interval algebra restricted
to the domain $\mathbb{D}=\mathbb{N}\cup\\{\infty\\}$. The language of
$\mathcal{M}$ is the set of all words over $\mathbb{D}$ of the form
$w_{1}\cdot d\cdot w_{2}$ where $w_{1}$ is some word over the domain
$\mathbb{D}$, the letter $d$ satisfies $0\leq d<100$ and all letters of the
word $w_{2}$ are numbers smaller than 200.

##  3\. Types of Symbolic Automata

Since the complexity of a learning algorithm for a class of languages
${\mathbb{L}}$ using some representation ${\mathbb{R}}$ is measured with
respect to the size of the smallest representation $R\in{\mathbb{R}}$ for the
unknown language $L\in{\mathbb{L}}$, we first need to agree how to measure the
size of an SFA. Subsection 3.1 explains why the number of states is not a
sufficient measure, and proposes an alternative using three parameters.
Optimizing different parameters leads to different special forms which are
discussed in subsection 3.2.

###  3.1. Size of an SFA

We note that there is a trade-off between the number of transitions and the
complexity of the transition predicates. The size of an automaton (not a
symbolic one) is typically measured by its number of states. This is since for
DFAs, the size of the alphabet is assumed to be a given constant, and the rest
of the parameters, in particular the transition relation, are at most
quadratic in the number of states. In the case of SFAs the situation is
different, as the size of the predicates labeling the transitions can vary
greatly. In fact, if we measure the size of a predicate by the number of nodes
in its parse dag, then the size of a formula can grow unboundedly (and the
same is true for other reasonable size measures for predicates). The size and
structure of the predicates influence the complexity of their satisfiability
check, and thus the complexity of the corresponding algorithms. On the other
hand there might be a trade-off between the size of the transition predicates
and the number of transitions; e.g., a predicate of the form
$\psi_{1}\vee\psi_{2}\ldots\vee\psi_{k}$ can be replaced by $k$ transitions,
each one labeled by $\psi_{i}$ for $1\leq i\leq k$.

Therefore, we measure the size of an SFA by three parameters: the number of
states ($n$), the maximal out-degree of a state ($m$) and the largest size of
a predicate ($l$).

In addition, in order to analyze the complexity of automata algorithms
discussed in subsection 5.1 and subsection 5.2, for a class ${\mathbb{P}}$ of
predicates over a Boolean algebra $\mathpzc{A}$, we use the complexity measure
$\mathit{sat}^{{\mathbb{P}}}(l)$, which is the complexity of satisfiability
check for a predicate of size $l$ in ${\mathbb{P}}$. We also use
$\mathit{sat}^{{\mathbb{P}}_{0}}(l)$ for the respective complexities when
restricted to atomic predicates.

###  3.2. Special Form SFAs

We turn to define special types of SFAs, which affect the complexity of
related procedures.

##### Neat and Normalized SFAs

The literature defines an SFA as _normalized_ if for every two states $q$ and
$q^{\prime}$ there exists at most one transition from $q$ to $q^{\prime}$.
This definition prefers fewer transitions at the cost of potentially
complicated predicates. By contrast, preferring simple transitions at the cost
of increasing the number of transitions, leads to  _neat_ SFAs. We define an
SFA to be _neat_ if all transition predicates are basic predicates.

##### Feasibility

The second distinction concerns the fact that an SFA can have transitions with
unsatisfiable predicates. A symbolic automaton is said to be _feasible_ if for
every $\langle q,\psi,q^{\prime}\rangle\in\Delta$ we have that
$\llbracket{\psi}\rrbracket\neq\emptyset$. Feasibility is an orthogonal
property to being neat or normalized.

##### Monotonicity

The third distinction we make concerning the nature of a given SFA regards its
underlying algebra. A Boolean algebra $\mathpzc{A}$ over domain $\mathbb{D}$
is said to be _monotonic_ if the following hold.

  1. (1)

There exists a total order $<$ on the elements of $\mathbb{D}$; and

  2. (2)

There exist two elements $d_{-\infty}$ and $d_{\infty}$ such that
$d_{-\infty}\leq d$ and $d\leq d_{\infty}$ for all $d\in\mathbb{D}$; and

  3. (3)

An atomic predicate $\psi\in\mathbb{P}_{0}$ can be associated with two
concrete values $a$ and $b$ such that
$\llbracket{\psi}\rrbracket=\\{d\in\mathbb{D}~{}:~{}a\leq d<b\\}$. Henceforth,
we denote an atomic predicate $\psi$ over a monotonic algebra as $\psi=[a,b)$
where $\llbracket{\psi}\rrbracket=\\{d\in\mathbb{D}~{}:~{}a\leq d<b\\}$. If
$b\leq a$ then we have that $\llbracket{\psi}\rrbracket=\emptyset$ and thus
the predicate is equivalent to $\bot$.

The interval algebra is clearly monotonic, as is the similar algebra obtained
using $\mathbb{R}$ (the real numbers) instead of $\mathbb{Z}$ (the integers).
On the other hand, the propositional algebra is clearly non-monotonic.

The SFA $\mathcal{M}$ from Example 2.2 (Figure 1) is defined over a monotonic
algebra, and is neat, normalized, deterministic and complete.

##  4\. Transformations to Special Forms

We now address the task of transforming SFAs into their special forms as
presented in section 3. We discuss transformations to the special forms _neat_
, _normalized_ and _feasible_ automata, measured as suggested using $\langle
n,m,l\rangle$ — the number of states, the maximal out-degree of a state, and
the largest size of a predicate.

###  4.1. Neat Automata

Since each predicate in a neat SFA is a conjunction of atomic predicates, neat
automata are intuitive, and the number of transitions in the SFA reflects the
complexity of the different operations, as opposed to the situation with
normalized SFAs. For the class ${\mathbb{P}}_{0}$ of basic formulas,
$\mathit{sat}^{{\mathbb{P}}_{0}}(l)$ is usually more efficient than
$\mathit{sat}^{{\mathbb{P}}}(l)$, and in particular is polynomial for the
algebras we consider here. This is since satisfiability testing can be reduced
to checking that for a basic predicate $\varphi$ that is a conjunction of $l$
atomic predicates, there are no two atomic predicates that contradict each
other. Since satisfiability checking directly affects the complexity of
various algorithms discussed in subsection 5.1, neat SFAs allow for efficient
automata operations, as we show in subsection 5.2.

####  4.1.1. Transforming to Neat

Given a general SFA $\mathcal{M}$ of size $\langle n,m,l\rangle$, we can
construct a neat SFA $\mathcal{M}^{\prime}$ of size $\langle n,m\cdot
2^{l},l\rangle$, by transforming each transition predicate to a DNF formula,
and turning each disjunct into an individual transition. The number of states,
$n$, remains the same. However, the number of transitions can grow
exponentially due to the transformation to DNF. In the worst case, the size of
the most complex predicate can remain the same after the transformation,
resulting in the same $l$ parameter for both automata.

Note that there is not necessarily a unique minimal neat SFA. For instance, a
predicate $\psi$ over the propositional algebra with
$AP=\\{p_{1},p_{2},p_{3}\\}$, satisfying
$\llbracket{\psi}\rrbracket=\\{[100],[101],[111]\\}$ can be represented using
the two basic transitions $(p_{1}\wedge\neg p_{2})$ and $(p_{1}\wedge
p_{2}\wedge p_{3})$; or alternatively using the two basic transitions
$(p_{1}\wedge p_{3})$ and $(p_{1}\wedge\neg p_{2}\wedge\neg p_{3})$, though it
cannot be represented using one basic transition.333This is related to the
fact that there is no unique DNF formula – a neat automaton “breaks” the DNF
to transitions according to the disjunctions in the formula. If there is no
unique DNF formula, then there is no unique neat SFA.

Although in the general case, the transformation from normalized to neat SFAs
is exponential, for monotonic algebras we have the following lemma, which
follows directly from the definition of monotonic algebras and basic
predicates.

######  Lemma 1.

Over a monotonic algebra, the conjunction of two atomic predicates is also an
atomic predicate; inductively, any basic formula that does not contain
negations, over a monotonic algebra, is an atomic predicate. In addition, the
negation of an atomic predicate is a disjunction of at most 2 atomic
predicates.

######  Lemma 2.

Let $\mathcal{M}$ be a normalized SFA over a monotonic algebra
$\mathpzc{A}_{\mathit{mon}}$. Then, transforming $\mathcal{M}$ into a neat SFA
$\mathcal{M}^{\prime}$ is linear in the size of $\mathcal{M}$.

Since a DNF formula with $m$ disjunctions is a natural representation of $m$
basic transitions, Lemma 2 follows from the following property of monotonic
algebras.

######  Lemma 3.

Let $\psi$ be a general formula over a monotonic algebra
$\mathpzc{A}_{\mathit{mon}}$. Then, there exists an equivalent DNF formula
$\psi_{\mathit{d}}$ of size linear in $|\psi|$.

######  Proof 4.1.

First, we transform $\psi$ into a Negation Normal Form formula
$\psi_{\mathit{NNF}}$, pushing negations inside the formula. When transforming
to NNF, the number of atomic predicates (possibly under negation) remains the
same, and so is the number of conjunctions and disjunctions. Since, by Lemma
1, a negation of an atomic predicate over a monotonic algebra, namely a
negation of an interval, results in at most two intervals, we get that
$|\psi_{\mathit{NNF}}|\leq 2\cdot|\psi|$. Note that $\psi_{\mathit{NNF}}$ does
not contain any negations, as they were applied to the intervals. We now
transform $\psi_{\mathit{NNF}}$ into a DNF formula $\psi_{d}$ recursively,
operating on sub-formulas of $\psi_{\mathit{NNF}}$, distributing conjunctions
over disjunctions.

We inductively prove that
$\llbracket{\psi_{d}}\rrbracket=\llbracket{\psi_{\mathit{NNF}}}\rrbracket$ and
$|\psi_{d}|\leq|\psi_{\mathit{NNF}}|$. For the base case, if
$\psi_{\mathit{NNF}}$ is a single interval $[a,b)$, then $[a,b)$ is in DNF and
we are done.

For the induction step, consider the following two cases.

  1. (1)

Assume $\psi_{\mathit{NNF}}=\psi_{1}\vee\psi_{2}$. By the induction
hypothesis, there exists DNF formulas $\psi_{1d}$ and $\psi_{2d}$ such that
$\llbracket{\psi_{id}}\rrbracket=\llbracket{\psi_{i}}\rrbracket$ and
$|\psi_{id}|\leq|\psi_{i}|$ for $i=1,2$. Then,
$\psi_{d}=\psi_{1d}\vee\psi_{2d}$ is equivalent to $\psi_{\mathit{NNF}}$ and
of the same size.

  2. (2)

Assume $\psi_{\mathit{NNF}}=\psi_{1}\wedge\psi_{2}$. Again, by the induction
hypothesis, instead of $\psi_{1}\wedge\psi_{2}$ we can consider
$\psi_{1d}\wedge\psi_{2d}$ where $\psi_{1d}$ and $\psi_{2d}$ are in DNF. That
is $\psi_{1d}=\bigvee_{i=1}^{k}[a_{i},b_{i})$ and
$\psi_{2d}=\bigvee_{j=1}^{l}[c_{j},d_{j})$. Now,

$\psi_{1d}\wedge\psi_{2d}=\left(\bigvee_{i=1}^{k}[a_{i},b_{i})\right)\wedge\left(\bigvee_{j=1}^{l}[c_{j},d_{j})\right)=\bigvee_{i=1}^{k}\bigvee_{j=1}^{l}\Big{(}[a_{i},b_{i})\wedge[c_{j},d_{j})\Big{)}$

From properties of intervals, each conjunction
$[a_{i},b_{i})\wedge[c_{j},d_{j})$ is of the form
$[\max\\{a_{i},c_{j}\\},\allowbreak\min\\{b_{i},d_{j}\\})$. The intervals in
$\\{[a_{i},b_{i})~{}:~{}1\leq i\leq k\\}$ do not intersect (otherwise it would
have resulted in a longer single interval), and the same for
$\\{[c_{j},d_{j})~{}:~{}1\leq j\leq l\\}$. Thus, every element $a_{i}$ or
$c_{j}$ can define at most one interval of the form
$[\max\\{a_{i},c_{j}\\},\min\\{b_{i},d_{j}\\})$. That is, the DNF formula
$\psi_{d}=\bigvee_{i=1}^{k}\bigvee_{j=1}^{l}\Big{(}[a_{i},b_{i})\wedge[c_{j},d_{j})\Big{)}$
contains at most $k+l$ intervals, as the others are empty intervals. Since the
size of the original $\psi_{NNF}$ is $k+l$, we have that
$|\psi_{d}|\leq|\psi_{NNF}|$.

To conclude, since $\psi_{NNF}$ is linear in the size of $\psi$ and $\psi_{d}$
is of the same size as $\psi_{NNF}$, we have that the translation of $\psi$
into the DNF formula $\psi_{d}$ is linear.

###  4.2. Normalized Automata

Neat automata stand in contrast to normalized ones. In a normalized SFA, there
is at most one transition between every pair of states, which allows for a
succinct formulation of the condition to transit from one state to another. On
the other hand, this makes the predicates on the transitions structurally more
complicated. Given a general SFA $\mathcal{M}$ with parameters $\langle
n,m,l\rangle$, we can easily construct a normalized SFA $\mathcal{M}^{\prime}$
as follows. For every pair of states $q$ and $q^{\prime}$, construct a single
edge labeled with the predicate $\bigvee_{\langle
q,\varphi,q^{\prime}\rangle\in\delta}\varphi$. Then, $\mathcal{M}^{\prime}$
has size $\langle
n,\min(n^{2},m),\mathit{size}^{{\mathbb{P}}}_{\vee^{m}}(l)\rangle$, where we
use $\mathit{size}^{{\mathbb{P}}}_{\vee^{m}}(l)$ to denote the size of $m$
disjunctions of predicates of size at most $l$.

Note that there is no unique minimal normalized automaton either, since in
general a Boolean formula can have two semantically equivalent, yet
syntactically different expressions in the underlying representation system,
e.g., two distinct BDDs can represent the same formula. However, in subsection
5.2 we show that over monotonic algebras there is a canonical minimal
normalized SFA.

The complexity of $\mathit{sat}^{{\mathbb{P}}}(l)$ for general formulas
(corresponding to normalized SFAs) is usually exponentially higher than for
basic predicates (and thus for neat SFAs). In addition, as we show above,
generating a normalized automaton is an easy operation. This motivates working
with neat automata, and generating normalized automata as a last step, if
desired (e.g., for presenting a graphical depiction of the automaton).

###  4.3. Feasible Automata

The motivation for feasible automata is clear; if the automaton contains
unsatisfiable transitions, then its size is larger than necessary, and the
redundancy of transitions makes it less interpretable. Thus, infeasible SFAs
add complexity both algorithmically and for the user, as they are more
difficult to understand. In order to generate a feasible SFA from a given SFA
$\mathcal{M}$, we need to traverse the transitions of $\mathcal{M}$ and test
the satisfiability of each transition. The parameters $\langle n,m,l\rangle$
of the SFA remain the same since there is no change in the set of states, and
there might be no change in transitions as well (if they are all satisfiable).

In the following, we usually assume that the automata are feasible, and when
applying algorithms, we require the output to be feasible as well.

##  5\. Complexity of standard automata procedures on SFAs

In this section we analyze the complexity of automata procedures on SFAs, in
terms of their effect on the parameters $\langle n,m,l\rangle$. We start in
subsection 5.1 with examining general SFAs, and then in subsection 5.2 discuss
the effects on special SFAs.

###  5.1. Complexity of Automata Procedures for General SFAs

We turn to discuss Boolean operations, determinization and minimization, and
decision procedures (such as emptiness and equivalence) for the different
types of SFAs. For intersection and union, the product construction of SFAs
was studied in [VdHT10, HV11]. There, the authors assume a normalized SFAs as
input, and do not delve into the effect of the construction on the number of
transitions and the complexity of the resulting predicates. Determinization of
SFAs was studied in [VdHT10], and [DV14] study minimization of SFAs, assuming
the given SFA is normalized.

Table 1 shows the sizes of the SFAs resulting from the mentioned operations,
in terms of $\langle n,m,l\rangle$. The analysis applies to all types of SFAs,
not just normalized ones. The time complexity for each operation is given in
terms of the parameters $\langle n,m,l\rangle$ and the complexity of
feasibility tests for the resulting SFA, as discussed in subsection 4.3. Table
2 summarizes the time complexity of decision procedures for SFAs: emptiness,
inclusion, and membership. Again, the analysis applies to all types of SFAs.
We note that in many applications of learning in verification, the challenging
part is implementing the teacher, for example in [PGGB+08, CKKS20, FGPS20]. In
such cases the complexity of membership and equivalence queries as well as
standard automata operations plays a major role.

In both tables we consider two SFAs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$
with parameters $\langle n_{i},m_{i},l_{i}\rangle$ for $i=1,2$, over algebra
$\mathpzc{A}$ with predicates ${\mathbb{P}}$. We use
$\mathit{size}^{{\mathbb{P}}}_{\wedge^{m}}(l)$ for an upper bound on the size
of $m$ conjunctions of predicates of size at most $l$. All SFAs are assumed to
be deterministic, except of course for the input for determinization.

Operation | $\mathbf{\langle n,m,l\rangle}$
---|---
product construction $\mathcal{M}_{1}$, $\mathcal{M}_{2}$ | $\langle n_{1}\times n_{2},\ m_{1}\times m_{2},\ \mathit{size}^{{\mathbb{P}}}_{\wedge}(l_{1},l_{2})\rangle$
complementation of deterministic $\mathcal{M}_{1}$444For complementation, no feasibility check is needed, since we assume a feasible input. | $\langle n_{1}+1,\ m_{1}+1,\ \mathit{size}^{{\mathbb{P}}}_{\neg}(\mathit{size}^{{\mathbb{P}}}_{\vee^{m_{1}}}(l_{1}))\rangle$
determinization of $\mathcal{M}_{1}$ |  $\langle 2^{n_{1}},\ 2^{m_{1}},\ \mathit{size}^{{\mathbb{P}}}_{\wedge^{n_{1}\times m_{1}}}(l_{1})\rangle$ 555To determinize transitions, conjunction may be applied $n_{1}\times m_{1}$ times, according to the number of states that correspond to a new deterministic state.
minimization of $\mathcal{M}_{1}$ | $\langle n_{1},m_{1},\ \mathit{size}^{{\mathbb{P}}}_{\wedge^{m_{1}}}(l_{1})\rangle$
Table 1. Analysis of standard automata procedures on SFAs.  Decision Procedures | Time Complexity
---|---
emptiness | linear in $n,m$
emptiness + feasibility | $n\times m\times\mathit{sat}^{{\mathbb{P}}}(l)$
membership of $\gamma_{1}\cdots\gamma_{t}\in\mathbb{D}^{*}$ |  $\sum_{i=1}^{t}\mathit{sat}^{{\mathbb{P}}}(\mathit{size}^{{\mathbb{P}}}_{\wedge}(l,|\psi_{\gamma_{i}}|))$ 666Where $\psi_{\gamma_{i}}$ is a predicate describing $\gamma_{i}$.
inclusion $\mathcal{M}_{1}\subseteq\mathcal{M}_{2}$ |  $(n_{1}\times n_{2})\times(m_{1}\times m_{2})\times\mathit{sat}^{{\mathbb{P}}}(\mathit{size}^{{\mathbb{P}}}_{\wedge}(l_{1},l_{2}))$
Table 2. Analysis of time complexity of decision procedures for SFAs.

We now briefly describe the algorithms we analyze in both tables.

##### Product Construction [VdHT10, HV11]

The product construction for SFAs is similar to the product of DFAs — the set
of states is the product of the states of $\mathcal{M}_{1}$ and
$\mathcal{M}_{2}$; and a transition is a synchronization of transitions of
$\mathcal{M}_{1}$ and $\mathcal{M}_{2}$. That is, a transition from $\langle
q_{1},q_{2}\rangle$ to $\langle p_{1},p_{2}\rangle$ can be made while reading
a concrete letter $\gamma$, iff $\langle
q_{1},\psi_{1},p_{1}\rangle\in\Delta_{1}$ and $\langle
q_{2},\psi_{2},p_{2}\rangle\in\Delta_{2}$ and $\gamma$ satisfies both
$\psi_{1}$ and $\psi_{2}$. Therefore, the predicates labeling transitions in
the product construction are conjunctions of predicates from the two SFAs
$\mathcal{M}_{1}$ and $\mathcal{M}_{2}$.

##### Complementation

In order to complement a deterministic SFA $\mathcal{M}_{1}$, we first need to
make $\mathcal{M}_{1}$ complete. In order to do so, we add one state which is
a non-accepting sink, and from each state we add at most one transition which
is the negation of all other transitions from that state. If $\mathcal{M}_{1}$
is complete, then complementation simply switches accepting and non-accepting
states, resulting in the same parameters $\langle n_{1},m_{1},l_{1}\rangle$.

##### Determinization [VdHT10]

In order to make an SFA deterministic, the algorithm of [VdHT10] uses the
subset construction for DFAs, resulting in an exponential blowup in the number
of states. However, in the case of SFAs this is not enough, and the predicates
require special care. Let $P=\\{q_{1},\cdots,q_{t}\\}$ be a state in the
deterministic SFA, where $q_{1},\ldots,q_{t}$ are states of the original SFA
$\mathcal{M}_{1}$, and let $\psi_{1},\ldots,\psi_{t}$ be some predicates
labelling outgoing transitions from $q_{1},\ldots q_{t}$, correspondingly.
Then, in order to determinize transitions, the algorithm of [VdHT10] computes
the conjunction $\bigwedge_{i=1}^{t}\psi_{i}$, which labels a single
transition from the state $P$.

##### Minimization [DV14]

Given a deterministic SFA $\mathcal{M}_{1}$, the output of minimization is an
equivalent deterministic SFA with a minimal number of states. When
constructing such an SFA, the number of states and transitions cannot grow.
However, as in determinization, if two states of $\mathcal{M}_{1}$ are
replaced with one state, then outgoing transitions might overlap, resulting in
a non-deterministic SFA. D’Antoni and Veanes [DV14] suggest several algorithms
to cope with this difficulty. One of their approaches is to compute _minterms_
, which are the smallest conjunctions of outgoing transitions. Minterms then
do not intersect, and thus the output is deterministic. Their other approaches
avoid computing minterms, but are able to achieve the same goal.

##### Emptiness

If we assume a feasible SFA $\mathcal{M}$ as an input, then in order to check
for emptiness we need to find an accepting state which is reachable from the
initial state (as in DFAs). If we do not assume a feasible input, we need to
test the satisfiability of each transition, thus the complexity depends on the
complexity measure $\mathit{sat}^{{\mathbb{P}}}(l)$.

##### Membership

Similarly to emptiness, in order to check if a concrete word
$\gamma_{1}\cdots\gamma_{n}$ is in $\mathcal{L}(\mathcal{M})$, we need not
only check if it reaches an accepting state but also locally consider the
satisfiability of each transition. In the case of membership, we need to check
whether the letter $\gamma_{i}$ satisfies the predicate on the corresponding
transition.

##### Inclusion

Deciding inclusion amounts to checking emptiness and feasibility of
$\mathcal{M}_{1}\cap\overline{\mathcal{M}_{2}}$. We assume here that both
$\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ are deterministic and complete.

###  5.2. Complexity of Automata Procedures for Special SFAs

We now discuss the advantages of neat SFAs and of monotonic algebras, in the
context of the algorithms presented in the tables, and show that, in general,
they are more efficient to handle compared to other SFAs.

####  5.2.1. Neat SFAs

As can be observed from Table 2, almost all decision procedures regarding SFAs
depend on $\mathit{sat}^{{\mathbb{P}}}(l)$. For neat SFAs it is more precise
to say that they depend on $\mathit{sat}^{{\mathbb{P}}_{0}}(l)$, namely on the
satisfiability of atomic predicates rather than arbitrary predicated. Since
$\mathit{sat}^{{\mathbb{P}}_{0}}(l)$ is usually less costly than
$\mathit{sat}^{{\mathbb{P}}}(l)$, most decision procedures are more efficient
on neat automata. Here, we claim that applying automata algorithms on neat
SFAs preserves their neatness, thus suggesting that neat SFAs may be
preferable in many applications.

######  Lemma 4.

Let $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ be neat SFAs. Then the algorithms
for their product construction, complementation, determinization and
minimization discussed in subsection 5.1 result in a neat SFA.

######  Proof 5.1.

Observing the procedures for product construction [VdHT10, HV11],
determinization [VdHT10] and minimization [DV14] constructions, one can see
that they use only conjunctions in order to construct the predicates on the
output SFAs. Thus, if the predicates on the input SFAs are basic, then so are
the output predicates.

####  5.2.2. Monotonic Algebras

We now consider the class ${\mathbb{M}}_{\mathpzc{A}_{mon}}$ of SFAs over a
monotonic algebra $\mathpzc{A}_{mon}$ with predicates ${\mathbb{P}}$. We first
discuss $\mathit{size}^{{\mathbb{P}}}_{\wedge}(l_{1},l_{2})$ and
$\mathit{sat}^{{\mathbb{P}}}(l)$, as they are essential measures in automata
operations. Then we show that for $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ in
the class ${\mathbb{M}}_{\mathpzc{A}_{mon}}$, the product construction is
linear in the number of transitions, adding to the efficiency of SFAs over
monotonic algebras.

######  Lemma 5.

Let $\psi_{1}$ and $\psi_{2}$ be formulas over a monotonic algebra
$\mathpzc{A}_{mon}$. Then $\mathit{size}^{{\mathbb{P}}}_{\wedge}(|\psi_{1}|,$
$|\psi_{2}|)$ is linear in $|\psi_{1}|+|\psi_{2}|$ and
$\mathit{sat}^{{\mathbb{P}}}(|\psi_{1}|)$ is linear in $|\psi_{1}|$.

######  Proof 5.2.

Transforming to DNF is linear, as we saw in Lemma 3. There, we saw that the
conjunction of two DNF formulas of sizes $k$ and $l$ has size $k+l$, which
implies that the conjunction of general formulas has linear size. In addition,
$\mathit{sat}^{{\mathbb{P}}}(l)$ is trivial for a single interval, and
following Lemma 3, is linear for general formulas. For an interval $[a,b)$,
satisfiability check amounts to the question “is $a<b$?”.

######  Lemma 6.

Let $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ be deterministic SFAs over a
monotonic algebra $\mathpzc{A}_{mon}$. Then the out-degree of their product
SFA $\mathcal{M}$ is at most $m=2\cdot(m_{1}+m_{2})$.

######  Proof 5.3.

From Lemma 2 and Lemma 3, we can construct neat SFAs
$\mathcal{M}^{\prime}_{1}$ and $\mathcal{M}^{\prime}_{2}$ of sizes $\langle
n_{i},2m_{i},$ $l_{i}\rangle$ for $i\in\\{1,2\\}$. Similarly to the proof of
Lemma 3, each transition $\langle\langle
q_{1},q_{2}\rangle,[a,b)\wedge[c,d),\langle p_{1},p_{2}\rangle\rangle$ in the
product SFA results in a formula $[\max\\{a,c\\},\allowbreak\min\\{b,d\\})$.
Then, for $q_{1}\in Q_{1}$, every minimal element in the set of $q_{1}$’s
outgoing transitions can define at most one transition in $\mathcal{M}$, and
the same for a state $q_{2}\in Q_{2}$, and so the number of transitions from
$\langle q_{1},q_{2}\rangle$ is at most $m_{1}+m_{2}$, as required.

######  Lemma 7.

Let $\mathcal{M}$ be a neat SFA over a monotonic algebra. Then, transforming
$\mathcal{M}$ into a complete SFA $\mathcal{M^{\prime}}$ is polynomial in the
size of $\mathcal{M}$.

######  Proof 5.4.

In order to complete $\mathcal{M}$, we add a non-accepting sink $r$ in case it
does not already exist, and at most $m+1$ transitions from each state $q$ to
$r$, when $m$ is the out-degree of the SFA. We now prove this. Let $[a,b)$ and
$[c,d)$ be two predicates labeling outgoing transitions of $q$, where $c$ is
the minimal left end-point of a predicate such that $b<c$. Then, in order to
complete $\mathcal{M}$, we need to add a transition to the sink, labeled by
the predicate $[b,c)$. In addition, for the predicate $[a,b)$ where there is
no $c>b$ that defines another predicate, if $b\neq d_{\infty}$ then we add
$[b,d_{\infty})$, and similarly we add $[d_{-\infty},a)$. Then, for each state
we add at most $m+1$ new transitions, resulting in at most $|Q|\times(m+1)$
new transitions.

For predicates over a monotonic algebra, we define a _canonical
representation_ of a predicate $\psi$ as the simplified DNF formula which is
the disjunction of all maximal disjoint intervals satisfying $\psi$.

Note that every predicate $\psi$ over a monotonic algebra defines a unique
partition of the domain into maximal disjoint intervals. This unique partition
corresponds to a simplified DNF formula, which is exactly the canonical
representation of $\psi$.

The canonical representation of $\psi=[0,100)\wedge([50,150)\vee[20,40))$ is
$[20,40)\vee[50,100)$.

######  Lemma 8.

Let $\mathcal{M}$ be an SFA over a monotonic algebra. Then:

  1. (1)

There is a unique minimal-state neat SFA $\mathcal{M^{\prime}}$ such that
$\mathcal{L}(\mathcal{M})=\mathcal{L}(\mathcal{M^{\prime}})$.

  2. (2)

There is a canonical minimal-state normalized SFA $\mathcal{M^{\prime\prime}}$
such that $\mathcal{L}(\mathcal{M})=\mathcal{L}(\mathcal{M^{\prime\prime}})$.

######  Proof 5.5.

For a language $\mathcal{L}=\mathcal{L}(\mathcal{M})$ for some SFA
$\mathcal{M}$, the minimal number of states in an SFA corresponds, similarly
to DFAs, to the number of equivalence classes in the equivalence relation $N$
defined by $(u,v)\in N\Longleftrightarrow\forall
z\in\mathbb{D}^{*}:(uz\in\mathcal{L}\Leftrightarrow vz\in\mathcal{L})$ [Myh57,
Ner58]. Indeed if $(u,v)\in N$ then there is no reason that reading them (from
the initial state) should end up in different states, and if $(u,v)\notin N$
then reading them (from the initial state) must lead to different states.

As for transitions, we have the following.

  1. (1)

Let $\psi$ be a general predicate labeling a transition in $\mathcal{M}$. Then
$\psi$ defines a unique partition of the domain into maximal disjoint
intervals, which are exactly the transitions in a neat SFA. Then, the minimal
state neat SFA is unique, where its transitions correspond exactly to these
maximal disjoint intervals.

  2. (2)

For normalized transitions, we can use Lemma 3 to transform a general
predicate labeling a transition to a DNF predicate in linear time. A DNF
predicate over a monotonic algebra is in-fact a disjunction of disjoint
intervals, where the construction of Lemma 3 obtains the maximal disjoint
intervals. Then, to obtain a canonical representation, we order these
intervals by order of their minimal elements.

##  6\. Learning SFAs

We turn to discuss the learnability of symbolic automata. In grammatical
inference, loosely speaking, we are interested in learning a class of
languages ${\mathbb{L}}$ over an alphabet $\Sigma$, from examples which are
words over $\Sigma$. Examples for classes of languages can be the set of
regular languages, the set of context-free languages, etc. A learning
algorithm, aka a _learner_ , is expected to output some concise representation
of the language from a class of representations ${\mathbb{R}}$ for the class
${\mathbb{L}}$. For instance, in learning the class ${\mathbb{L}}_{reg}$ of
regular languages one might consider the class ${\mathbb{R}}_{\textsc{dfa}}$
of DFAs, or the class ${\mathbb{R}}_{\textsc{lin}}$ of right linear grammars,
since both are capable of expressing all regular languages.777The class of
regular languages was shown learnable via various representations including
DFAs [Ang87], NFAs [BHKL09], and AFAs (alternating finite automata) [AEF15].
We often say that a class of representations ${\mathbb{R}}$ is learnable (or
not) when we mean that class of languages ${\mathbb{L}}$ is learnable (or not)
via the class of representations ${\mathbb{R}}$. The complexity of learning an
unknown language $L\in{\mathbb{L}}$ via ${\mathbb{R}}$ is typically measured
with respect to the size of the smallest representation $R_{L}\in{\mathbb{R}}$
for $L$. For instance, when learning ${\mathbb{L}}_{reg}$ via
${\mathbb{R}}_{\textsc{dfa}}$ a learner is expected to output a DFA for an
unknown language in time that is polynomial in the number of states of the
minimal DFA for $L$.

In our setting we are interested in learning regular languages using as a
representation a class of SFAs over a certain algebra. To measure complexity
we must agree on how to measure the size of an SFA. Thus, as discussed in
subsection 3.1 we represent the size of an SFA using the parameters $\langle
n,m,l\rangle$ of the number of states of the SFA, the number of transitions,
and the size of the largest predicate. Another important factor regarding size
and canonical forms of SFAs, is the underlying algebra, specifically, whether
it is monotonic or not.

##### Learning Paradigms

The exact definition regarding learnability of a class depends on the
_learning paradigm_. In this work we consider two widely studied paradigms:
_learning with membership and equivalence queries_ , and _identification in
the limit using polynomial time and data_. Their definitions are provided in
the respective sections. Note that in general, a positive or negative result
in one paradigm, does not derive the same result in another paradigm. We
discuss this further in Acknowledgments.

##### Basic SFAs

To provide results regarding the learnability of SFAs, we study classes of
SFAs that contain all basic SFAs, defined as follows.

An SFA $\mathcal{M}$ over a Boolean Algebra $\mathpzc{A}$ with a set of
predicates ${\mathbb{P}}$ is termed _basic_ if it is of the form
$\mathcal{M}_{\varphi}=(\mathpzc{A},\\{q_{\iota},q_{ac},q_{rj}\\},q_{\iota},\\{q_{ac}\\},\Delta)$
where $\varphi\in{\mathbb{P}}$ and $\Delta=\\{\langle
q_{\iota},\varphi,q_{ac}\rangle,\langle
q_{\iota},\neg\varphi,q_{rj}\rangle,\langle q_{rj},\top,q_{rj}\rangle,\langle
q_{ac},\top,q_{rj}\rangle\\}$. Note that $\mathcal{M}_{\varphi}$ accepts only
words of length one consisting of a concrete letter satisfying $\varphi$, and
it is minimal among all complete deterministic SFAs accepting this language
(minimal in both number of states and number of transitions).

In the sequel, our results are regarding classes of SFAs that contain all
basic SFAs $\mathcal{M}_{\varphi}$ for all $\varphi\in{\mathbb{P}}$.

##  7\. Efficient Identifiability

While in _active learning_ (namely, query learning with mqs and eqs) the
learner can select any word and query about its membership in the unknown
language, in _passive learning_ the learner is given a set of words, and for
each word $w$ in the set, a label $b_{w}$ indicating whether $w$ is in the
unknown language or not. Formally, a _sample_ for a language $L$ is a finite
set $\mathcal{S}$ consisting of labeled examples, that is, pairs of the form
$\langle w,b_{w}\rangle$ where $w$ is a word and $b_{w}\in\\{0,1\\}$ is its
label, satisfying that $b_{w}=1$ if and only if $w\in L$. The words that are
labeled $1$ are termed _positive_ words, and those that are labeled $0$ are
termed _negative_ words. Note that if $L$ is recognized by an automaton
$\mathcal{M}$, we have that
$\mathcal{S}\subseteq\hat{\mathcal{L}}({\mathcal{M}})$ (as defined in
subsection 2.2). If $\mathcal{S}$ is a sample for $L$ we often say that
$\mathcal{S}$ _agrees with_ $L$. Given two words $w,w^{\prime}$, we say that
$w$ and $w^{\prime}$ are not equivalent with respect to $\mathcal{S}$, denoted
$w\not\sim_{\mathcal{S}}w^{\prime}$, iff there exists $z$ such that $\langle
wz,b\rangle,\langle w^{\prime}z,b^{\prime}\rangle\in\mathcal{S}$ and $b\neq
b^{\prime}$. Otherwise we say that $w$ and $w^{\prime}$ are equivalent with
respect to $\mathcal{S}$, and denote $w\sim_{\mathcal{S}}w^{\prime}$.

Given a sample $\mathcal{S}$ for a language $L$ over a concrete domain
$\mathbb{D}$, it is possible to construct a DFA that agrees with $\mathcal{S}$
in polynomial time. Indeed one can create the _prefix-tree automaton_ , a
simple automaton that accepts all and only the positively labeled words in the
sample. Clearly the constructed automaton may not be the minimal automaton
that agrees with $\mathcal{S}$. There are several algorithms, in particular
the popular RPNI [OG92], that merges the states of the prefix-tree automaton
and results in an automaton that may accept an infinite language. Obviously
though, this procedure is not guaranteed to return an automaton for the
unknown language, as the sample may not provide sufficient information. For
instance if $L=aL_{1}\cup bL_{2}$ and the sample contains only words starting
with $a$, there is no way for the learner to infer $L_{2}$ and hence also $L$
correctly. One may thus ask, given a language $L$, what should a sample
contain in order for a passive learning algorithm to infer $L$ correctly, and
can such sample be of polynomial size with respect to a minimal representation
(e.g., a DFA) for the language.

One approach to answer these questions is captured in the paradigm of
_identification in the limit using polynomial time and data_. This model was
proposed by Gold [Gol78], who also showed that it admits learning of regular
languages represented by DFAs. We follow de la Higuera’s more general
definition [dlH97].888This paradigm may seem related to conformance testing.
The relation between conformance testing for Mealy machines and automata
learning of DFAs has been explored in [BGJ+05]. This definition requires that
for any language $L$ in a class of languages ${\mathbb{L}}$ represented by
${\mathbb{R}}$, there exists a sample $\mathcal{S}_{L}$ of size polynomial in
the size of the smallest representation $R\in{\mathbb{R}}$ of $L$ (e.g., the
smallest DFA for $L$), such that a valid learner can infer the unknown
language $L$ from the information contained in $\mathcal{S}_{L}$. The set
$\mathcal{S}_{L}$ is then termed a _characteristic sample_.999De la Higuera’s
notion of characteristic sample is a core concept in grammatical inference,
for various reasons. Firstly, it addresses shortcomings of several other
attempts to formulate polynomial-time learning in the limit [Ang88, Pit89].
Secondly, this notion has inspired the design of popular algorithms for
learning formal languages such as, for example, the RPNI algorithm [OG92].
Thirdly, it was shown to bear strong relations to a classical notion of
machine teaching [GM96]; models of the latter kind are currently experiencing
increased attention in the machine learning community [ZSZR18]. Here, a valid
learner is an algorithm that learns the target language exactly and
efficiently. In particular, a valid learner produces in polynomial time a
representation that agrees with the provided sample. The learner also has to
correctly learn the unknown language $L$ when given the characteristic sample
$\mathcal{S}_{L}$ as input. Moreover, if the input sample $\mathcal{S}$
subsumes $\mathcal{S}_{L}$ yet is still consistent with $L$, the additional
information in the sample should not “confuse” the learner; the latter still
has to output a correct representation for $L$. (Intuitively, this requirement
precludes situations in which the sample consists of some smart encoding of
the representation that the learner simply deciphers. In particular, the
learner will not be confused if an adversary “contaminates” the characteristic
sample by adding labeled examples for the target language.) We provide the
formal definition after the following informal example.

For the class of DFAs, let us consider the regular language $L=a^{*}$ over the
alphabet $\\{a,b\\}$. Further, consider a sample set
$\mathcal{S}=\\{\langle\epsilon,1\rangle,\langle a,1\rangle,\langle
b,0\rangle,\langle bb,0\rangle,\langle ba,0\rangle\\}$ for $L$. There is a
valid learner for the class of all DFAs that uses the sample $\mathcal{S}$ as
a characteristic sample for $L$. By definition, such a learner has to output a
DFA for $L$ when fed with $\mathcal{S}$, but also has to output equivalent
DFAs whenever given any superset of $\mathcal{S}$ as input, as long as this
superset agrees with $L$. Naturally, the sample $\mathcal{S}$ is also
consistent with the regular language $L^{\prime}=\\{\epsilon,a\\}$. However,
this does not pose any problem, since the same learner can use a
characteristic sample for $L^{\prime}$ that disagrees with $L$, for example,
$\mathcal{S}^{\prime}=\\{\langle\epsilon,1\rangle,\langle a,1\rangle,\langle
aa,0\rangle\\}$. When defining a system of characteristic samples like that,
the core requirement is that the size of a sample be bounded from above by a
function that is polynomial in the size of the smallest DFA for the respective
target language.

[identification in the limit using polynomial time and data [dlH97]] A class
of languages ${\mathbb{L}}$ is said to be _identified in the limit using
polynomial time and data_ via representations in a class ${\mathbb{R}}$ if
there exists a learning algorithm A such that the following two requirements
are met.

  1. (1)

Given a finite sample $\mathcal{S}$ of labeled examples, A returns a
hypothesis $\mathcal{R}\in{\mathbb{R}}$ that agrees with $\mathcal{S}$ in
polynomial time.

  2. (2)

For every language $L\in{\mathbb{L}}$, there exists a sample
$\mathcal{S}_{L}$, termed _a characteristic sample_ , of size polynomial in
the minimal representation $\mathcal{R}\in{\mathbb{R}}$ for $L$ such that the
algorithm A returns a correct hypothesis when run on any sample $\mathcal{S}$
for $L$ that subsumes $\mathcal{S}_{L}$.

Note that the first condition ensures polynomial time and the second
polynomial data. However, the latter is not a worst-case measure; the
algorithm may fail to return a correct hypothesis on arbitrarily large finite
samples (if they do not subsume a characteristic set).

Note also that the definition does not require the existence of an efficient
algorithm that constructs a characteristic sample for each language in the
underlying class. When such an algorithm is also available we say that the
class is _efficiently identifiable_. The following result shows that efficient
identifiability does not trivially follow from identifiability; in fact it
makes the much stronger statement that not even _computability_ of
characteristic sets follows from their existence.

######  Theorem 9.

There exists a class of languages that possesses polynomial-size
characteristic sets, yet without the ability to construct such sets
effectively.

We first prove Theorem 9 and then provide a definition for efficient
identification.

######  Proof 7.1.

We present a class of recursive languages that is identifiable in the limit
from polynomial time and data, while there is no (polynomial-time or other)
algorithm that constructs a characteristic sample for every language in the
class, using a specific underlying representation of the languages in the
class.

For the purpose of defining such class, let $\varphi$ be a Gödel numbering of
all partial computable functions over the natural numbers, and let $\Phi$ be a
corresponding Blum complexity measure. Here $\varphi_{i}$ refers to the $i$th
partial computable function in the numbering $\varphi$. Intuitively,
$\Phi_{i}(j)$ is undefined if $\varphi_{i}(j)$ is undefined (i.e., the
computation of $\varphi_{i}(j)$ does not terminate); otherwise $\Phi_{i}(j)$
is the number of computational steps required until the termination of the
computation of $\varphi_{i}(j)$. The set $K=\\{k\mid\varphi_{k}(k)\mbox{ is
defined}\\}$ is called the halting set for $\varphi$; this set is recursively
enumerable but membership in $K$ is not decidable.

We now define two languages for each natural number $k$:

$\displaystyle L_{k,1}$ $\displaystyle=$ $\displaystyle a^{*}\cup\\{b^{k}\\}$
$\displaystyle L_{k,2}$ $\displaystyle=$
$\displaystyle\begin{cases}\\{a^{i}\mid
i\leq\Phi_{k}(k)\\}\cup\\{b^{k}\\}\,,&\mbox{if }k\in K\,,\\\
a^{*}\cup\\{b^{k}\\}\,,&\mbox{otherwise}\,.\end{cases}$

Note that $L_{k,1}=L_{k,2}$ if and only if $k\notin K$. Now let $\mathbb{L}$
consist of all languages $L_{k,q}$ for $k\in\mathbb{N}$ and $q\in\\{1,2\\}$.

There is an effective algorithm that decides membership in $L_{k,q}$, given
$k\in\mathbb{N}$ and $q\in\\{1,2\\}$. To see that, note that, given $k$, $q$,
and a word $w$, membership is trivial to decide when $q=1$ or when $w$ is not
of the form $a^{i}$. If $w=a^{i}$, then $w$ belongs to $L_{k,2}$ if and only
if the computation of $\varphi_{k}(k)$ does not terminate within fewer than
$i$ steps, which can be checked effectively.

Moreover, every language in $\mathbb{L}$ is regular and has a characteristic
sample of size at most 2. In particular, $\\{\langle b^{k},1\rangle\\}$ serves
as a characteristic sample for $L_{k,1}$ (and thus also for $L_{k,2}$ in case
$k\notin K$), while $\\{\langle b^{k},1\rangle,\langle
a^{\Phi_{k}(k)+1},0\rangle\\}$ is a characteristic sample for $L_{k,2}$ in
case $k\in K$. Thus, using the above representation, the class $\mathbb{L}$
has polynomial-size (even constant-size) characteristic samples. However,
there is no algorithm to construct such characteristic samples effectively,
since otherwise such an algorithm could be used to decide membership in $K$.
(The latter can be verified by noting that $L_{k,2}\subseteq L_{k,1}$ for all
$k$. Therefore, a system of characteristic samples would need to distinguish
$L_{k,2}$ from $L_{k,1}$ (when $k\in K$) by either (i) a negative example of
the form $\langle a^{i},0\rangle$ for $L_{k,2}$, or (ii) a positive example of
the form $\langle a^{i},1\rangle$ for $L_{k,1}$, where $a^{i}\notin L_{k,2}$.
Thus, the presence or absence of such example in the characteristic samples
for $L_{k,1}$, $L_{k,2}$ can be used to decide whether or not $k\in K$.)

Since we are concerned with learning classes of automata, we now formulate the
definition of _efficient identification_ directly over classes of automata.

[efficient identification] A class of automata ${\mathbb{M}}$ over an alphabet
$\Sigma$ is said to be _efficiently identified_ if the following two
requirements are met.

  1. (1)

There exists a polynomial time learning algorithm
${{\textbf{{Infer}}}}:2^{(\Sigma^{*}\times\\{0,1\\})}\rightarrow{\mathbb{M}}$
such that, for any sample $\mathcal{S}$, we have
$\mathcal{S}\subseteq\hat{\mathcal{L}}({{{\textbf{{Infer}}}}(\mathcal{S})})$.

  2. (2)

There exists a polynomial time algorithm
${{\textbf{Char}}}:{\mathbb{M}}\rightarrow 2^{(\Sigma^{*}\times\\{0,1\\})}$
such that, for every $\mathcal{M}\in{\mathbb{M}}$ and every sample
$\mathcal{S}$ satisfying
${{\textbf{Char}}}(\mathcal{M})\subseteq\mathcal{S}\subseteq\hat{\mathcal{L}}({\mathcal{M}})$,
the automaton ${{\textbf{{Infer}}}}(\mathcal{S})$ recognizes the same language
as $\mathcal{M}$.

When we apply this definition for a class of SFAs over a Boolean algebra
$\mathpzc{A}$ with domain $\mathbb{D}$ and predicates ${\mathbb{P}}$, the
characteristic sample is defined over the concrete set of letters $\mathbb{D}$
rather than the set of predicates ${\mathbb{P}}$ as this is the alphabet of
the words accepted by an SFA. (Inferring an SFA from a set of words labeled by
predicates can be done using the methods for inferring DFAs, by considering
the alphabet to be the set of predicates.)

Throughout this section we study whether a class of SFAs ${\mathbb{M}}$ is
efficiently identifiable. That is, we are interested in the existence of
algorithms ${{\textbf{{Infer}}}}_{{\mathbb{M}}}$ and
${{\textbf{Char}}}_{{\mathbb{M}}}$ satisfying the requirements of Definition
7.1. In section 8 we provide a necessary condition for a class of SFAs to be
identified in the limit using polynomial time and data. In section 9 we
provide a sufficient condition for a class of SFAs to be efficiently
identifiable. On the positive side, we show in section 10 that the class of
SFAs over the interval algebra is efficiently identifiable. On the negative
side, we show in section 11 that SFAs over the general propositional algebra
cannot be identified in the limit using polynomial time and data. All classes
of SFAs that we study are assumed to contain all basic SFAs (as per Definition
6).

###  7.1. Efficient Identification of DFAs

Before investigating efficient identification of SFAs, it is worth noting that
DFAs are efficiently identifiable. We state a result that provides more
details about the nature of these algorithms, since we need it later, in
section 10, to provide our positive result. Intuitively, it says that there
exists a valid learner such that if $\mathcal{D}$ is a minimal DFA recognizing
a certain language $L$ then the learner can infer $L$ from a characteristic
sample consisting of access words to each state of $\mathcal{D}$ and their
extensions with distinguishing words (words showing each pair of states cannot
be merged) as well as one letter extensions of the access words that are
required to retrieve the transition relation. For completeness we give a proof
of this theorem in Appendix A.

######  Theorem 10 ([OG92]).

The class of DFAs is efficiently identifiable via procedures CharDFA and
InferDFA. Furthermore, these procedures satisfy that if $\mathcal{D}$ is a
minimal and complete DFA and
${{\textbf{{CharDFA}}}}(\mathcal{D})=\mathcal{S}_{\mathcal{D}}$ then the
following hold:

  1. (1)

$\mathcal{S}_{\mathcal{D}}$ contains a prefix-closed set $A$ of access words.
Moreover, $A$ can be chosen to contain only lex-access words, i.e., only the
lexicographically smallest access word for each state.

  2. (2)

For every $u_{1},u_{2}\in A$ it holds that
$u_{1}\not\sim_{\mathcal{S}_{\mathcal{D}}}u_{2}$.

  3. (3)

For every $u,v\in A$ and $\sigma\in\Sigma$, if
$\Delta(q_{\iota},u\sigma)\neq\Delta(q_{\iota},v)$ then
$u\sigma\not\sim_{\mathcal{S}_{\mathcal{D}}}v$.

We briefly describe CharDFA and InferDFA.

The algorithm CharDFA works as follows. It first creates a prefix-closed set
of access words to states. This can be done by considering the graph of the
automaton and running an algorithm for finding a spanning tree from the
initial state. Choosing one of the letters on each edge, the access word for a
state is obtained by concatenating the labels on the unique path of the
obtained tree that reaches that state. If we wish to work with lex-access
words, we can use a depth-first search algorithm that spans branches according
to the order of letters in $\Sigma$, starting from the smallest. The labels on
the paths of the spanning tree constructed this way will form the set of lex-
access words.

Let $S$ be the set of access words (or lex-access words). Next the algorithm
turns to find a distinguishing word $v_{i,j}$ for every pair of states
$s_{i},s_{j}\in S$ (where $s_{i}\neq s_{j}$). It holds that any pair of states
of the minimal DFA has a distinguishing word of size quadratic in the size of
the DFA. Let $E$ be the set of all such distinguishing words. Then the
algorithm returns the set $\mathcal{S}_{\mathcal{D}}=\\{\langle
w,\mathcal{D}(w)\rangle~{}|~{}w\in(S\cdot E)\cup(S\cdot\Sigma\cdot E)\\}$
where $\mathcal{D}(w)$ is the label $\mathcal{D}$ gives $w$ (i.e., $1$ if it
is accepted, and $0$ otherwise). It is easy to see that
$\mathcal{S}_{\mathcal{D}}$ satisfies the properties of Theorem 10.

The algorithm InferDFA, given a sample of words $\mathcal{S}$, infers from it
in polynomial time a DFA that agrees with $\mathcal{S}$. Moreover, if
$\mathcal{S}$ subsumes the characteristic set $\mathcal{S}_{\mathcal{D}}$ of a
DFA $\mathcal{D}$ then InferDFA returns a DFA that recognizes $\mathcal{D}$.
Let $W$ be the set of words in the given sample $\mathcal{S}$ (without their
labels). Let $R$ be the set of prefixes of $W$ and $C$ the set of suffixes of
$W$. Note that $\epsilon\in R$ and $\epsilon\in C$. Let $r_{0},r_{1},\ldots$
be some enumeration of $R$ and $c_{0},c_{1},\ldots$ some enumeration of $C$
where $r_{0}=c_{0}=\epsilon$. The algorithm builds a matrix $M$ of size
$|R|\times|C|$ whose entries take values in $\\{0,1,?\\}$, and sets the value
of entry $(i,j)$ as follows. If $r_{i}c_{j}$ is not in $W$, it is set to $?$.
Otherwise it is set to $1$ iff the word $r_{i}c_{j}$ is labeled $1$ in
$\mathcal{S}$. We get that $r_{i}\sim_{\mathcal{S}}r_{j}$ iff for every $k$
such that both $M(i,k)$ and $M(j,k)$ are different than $?$ we have that
$M(i,k)=M(j,k)$. The algorithm sets $R_{0}=\\{\epsilon\\}$. Once $R_{i}$ is
constructed, the algorithm tries to establish whether for $r\in R_{i}$ and
$\sigma\in\Sigma$, $r\sigma$ is distinguished from all words in $R_{i}$. It
does so by considering all other words $r^{\prime}\in R_{i}$ and checking
whether $r\sim_{\mathcal{S}}r^{\prime}$. If $r\sigma$ is found to be distinct
from all words in $R_{i}$, then $R_{i+1}$ is set to $R_{i}\cup\\{r\sigma\\}$.
The algorithm proceeds until no new words are distinguished.101010There is
some resemblance between the partial matrix and the apartness relation of
[VGRW22], used in query learning of DFAs.

Let $k$ be the minimal iteration such that $R_{k}=R_{k^{\prime}}$ for all
$k^{\prime}>k$. If not all words in $R_{k}$ are in $W$ (that is $M(i,0)=?$ for
some $r_{i}\in R_{k}$), the algorithm returns the prefix-tree automaton.
Otherwise, the states of the constructed DFA are set to be the words in
$R_{k}$. The initial state is $\epsilon$ and a state $r_{i}$ is classified as
accepting iff $M(i,0)=1$ (recall that the entry $M(i,0)$ stands for the value
of $r_{i}\cdot\epsilon$ in $\mathcal{S}$). To determine the transitions, for
every $r\in R_{k}$ and $\sigma\in\Sigma$, recall that there exists at least
one state $r^{\prime}\in R$ that cannot be distinguished from $r\sigma$. The
algorithm then adds a transition from $r$ on $\sigma$ to $r^{\prime}$.

##  8\. Necessary Condition

We make use of the following definitions. A sequence
$\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle$ consisting of finite sets of
concrete letters $\Gamma_{i}\subseteq{\mathbb{D}}$ is termed a _concrete
partition_ of $\mathbb{D}$ if the sets are pairwise disjoint (namely
$\Gamma_{i}\cap\Gamma_{j}=\emptyset$ for every $i\neq j$). Note that we do not
require that in addition $\bigcup_{1\leq i\leq k}\Gamma_{i}=\mathbb{D}$. We
use $\Pi_{\textsf{conc}}({\mathbb{D}})$ to define the set of all concrete
partitions over $\mathbb{D}$. A sequence of predicates
$\langle\psi_{1},\ldots,\psi_{k}\rangle$ over a Boolean algebra $\mathpzc{A}$
on a domain $\mathbb{D}$ is termed a _predicate partition_ if
$\llbracket{\psi_{i}}\rrbracket\cap\llbracket{\psi_{j}}\rrbracket=\emptyset$
for every $i\neq j$, and in addition $\bigcup_{1\leq i\leq
k}\llbracket{\psi_{i}}\rrbracket=\mathbb{D}$. That is, here we do require the
assignments to the predicates cover the domain. We use
$\Pi_{\textsf{pred}}({{\mathbb{P}}})$ to define the set of all predicate
partitions over ${\mathbb{P}}$. For both concrete partition and predicate
partition, we do not require that the sets $\Gamma_{i}$ or
$\llbracket{\psi_{i}}\rrbracket$ are non-empty.

  * •

A function
$f_{c}:\Pi_{\textsf{pred}}({{\mathbb{P}}})\rightarrow\Pi_{\textsf{conc}}({\mathbb{D}})$
is termed _concretizing_ if
$f_{c}(\langle\psi_{1},\ldots,\psi_{m}\rangle)=\langle\Gamma_{1},\ldots,\Gamma_{k}\rangle$
implies $k=m$ and $\Gamma_{i}\subseteq\llbracket{\psi_{i}}\rrbracket$ for all
$1\leq i\leq m$.

  * •

A function
$f_{g}:\Pi_{\textsf{conc}}({\mathbb{D}})\rightarrow\Pi_{\textsf{pred}}({{\mathbb{P}}})$
is termed _generalizing_ if
$f_{g}(\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle)=\langle\psi_{1},\ldots,\psi_{k}\rangle$
implies $k=m$ and $\llbracket{\psi_{i}}\rrbracket\supseteq\Gamma_{i}$ for all
$1\leq i\leq m$.

Note that $f_{g}$ and $f_{c}$ are defined over partitions of any size. In
Theorem 11 we use their _dyadic_ restriction, that is, a concretizing and a
generalizing function that are defined only over partitions of size two.

We say that $f_{g}$ (resp. $f_{c}$) is _efficient_ if it can be computed in
polynomial time. Note that if $f_{c}$ is efficient then the sets $\Gamma_{i}$
in the constructed concrete partition are of polynomial size.

We are now ready to provide a necessary condition for identifiability in the
limit using polynomial time and data.

######  Theorem 11.

Let ${\mathbb{M}}{A}$ be a class of SFAs over a Boolean algebra $\mathpzc{A}$,
that contain all basic SFAs over $\mathpzc{A}$. If ${\mathbb{M}}{A}$ is
identified in the limit using polynomial time and data, then there exist
efficient dyadic concretizing and generalizing functions
${\textsf{Concretize}}{A}:\Pi_{\textsf{pred}}({{\mathbb{P}}})\rightarrow\Pi_{\textsf{conc}}({\mathbb{D}})$
and
${\textsf{Generalize}}{A}:\Pi_{\textsf{conc}}({\mathbb{D}})\rightarrow\Pi_{\textsf{pred}}({{\mathbb{P}}})$
satisfying that

if
${\textsf{Concretize}}{A}(\langle\psi_{1},\psi_{2}\rangle)=\langle\Gamma_{1},\Gamma_{2}\rangle$

and
${\textsf{Generalize}}{A}(\langle\Gamma^{\prime}_{1},\Gamma^{\prime}_{2}\rangle)=\langle\varphi_{1},\varphi_{2}\rangle$

where $\Gamma_{i}\subseteq\Gamma^{\prime}_{i}$ for every $1\leq i\leq 2$

then $\llbracket{\varphi_{i}}\rrbracket=\llbracket{\psi_{i}}\rrbracket$ for
every $1\leq i\leq 2$.

######  Proof 8.1.

Assume that ${\mathbb{M}}{A}$ is identified in the limit using polynomial time
and data. That is, there exist two algorithms
$\textsf{CharSFA}:{\mathbb{M}}{A}\rightarrow
2^{\mathbb{D}^{*}\times\\{0,1\\}}$ and
$\textsf{InferSFA}:2^{\mathbb{D}^{*}\times\\{0,1\\}}\rightarrow{\mathbb{M}}{A}$
satisfying the requirements of Definition 7. We show that efficient dyadic
concretizing and generalizing functions do exist.

We start with the definition of ${\textsf{Concretize}}{A}$. Let
$\langle\varphi_{1},\varphi_{2}\rangle$ be the argument of
${\textsf{Concretize}}{A}$. Note that $\varphi_{2}=\neg\varphi_{1}$ by the
definition of a predicate partition. The implementation of
${\textsf{Concretize}}{A}$ invokes CharSFA on the SFA
$\mathcal{M}_{\varphi_{1}}$ accepting all words of length one consisting of a
concrete letter satisfying $\varphi_{1}$, as defined in Definition 6. Let
$\mathcal{S}$ be the returned sample. Let $\Gamma_{1}$ be the set of
positively labeled words in the sample. Note that all such words are of size
one, namely they are letters. Let $\Gamma_{2}$ be the set of letters that are
first letters in a negative word in the sample. Then
${\textsf{Concretize}}{A}$ returns $\langle\Gamma_{1},\Gamma_{2}\rangle$.

We turn to the definition of ${\textsf{Generalize}}{A}$. Given
$\langle\Gamma_{1},\Gamma_{2}\rangle$ the implementation of
${\textsf{Generalize}}{A}$ invokes InferSFA on sample
$\mathcal{S}=\\{(\gamma,1)~{}|~{}\gamma\in\Gamma_{1}\\}\cup\\{(\gamma,0)~{}|~{}\gamma\in\Gamma_{2}\\}\cup\\{(\gamma\gamma^{\prime},0)~{}|~{}\gamma,\gamma^{\prime}\in\Gamma_{1}\cup\Gamma_{2}\\}$.
That is, all one-letter words satisfying $\Gamma_{1}$ are positively labeled,
all one-letter words satisfying $\Gamma_{2}$ are negatively labeled, and all
words of length $2$ using some of the given concrete letters are negatively
labeled. Let $\mathcal{M}$ be the returned SFA when given
$\mathcal{S}^{\prime}$, such that $\mathcal{S}^{\prime}\supseteq\mathcal{S}$,
as an input. Let $\Psi_{1}$ be the set of all predicates labeling some edge
from the initial state to an accepting state, and let $\Psi_{2}$ be the set of
all predicates labeling some edge from the initial state to a rejecting state.
Let
$\varphi=(\bigvee_{\psi\in\Psi_{1}}\psi)\wedge(\bigwedge_{\psi\in\Psi_{2}}\neg\psi)$.
Then ${\textsf{Generalize}}{A}$ returns $\langle\varphi,\neg\varphi\rangle$.

It is not hard to verify that the constructed methods
${\textsf{Concretize}}{A}$ and ${\textsf{Generalize}}{A}$ satisfy the
requirements of the theorem.

The following example shows the existence of functions Concretize and
Generalize for the interval algebra.

Consider the class ${\mathbb{M}}_{{\mathpzc{A_{\mathbb{N}}}}}$ of SFAs over
the algebra ${\mathpzc{A_{\mathbb{N}}}}$ of Example 2.2 and consider the
functions
${\textsf{Concretize}}_{{{\mathpzc{A_{\mathbb{N}}}}}}(\langle[d_{1},d^{\prime}_{1}),[d_{2},d^{\prime}_{2}),\ldots,[d_{m},d^{\prime}_{m})\rangle)=\langle\\{d_{1}\\},\ldots,\\{d_{m}\\}\rangle$
and ${\textsf{Generalize}}_{{{\mathpzc{A_{\mathbb{N}}}}}}$
$(\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle)=\langle[\min{\Gamma_{1}},\min{\hat{\Gamma_{1}}}),[\min{\Gamma_{2}},\min{\hat{\Gamma_{2}}}),$
$\ldots,[\min{\Gamma_{m}},\infty)\rangle$ where
$\hat{\Gamma_{i}}=\bigcup_{j\neq i}\Gamma_{j}$ for every $1\leq i<m$. Then,
${\textsf{Concretize}}_{{{\mathpzc{A_{\mathbb{N}}}}}}$ and
${\textsf{Generalize}}_{{{\mathpzc{A_{\mathbb{N}}}}}}$ satisfy the variadic
generalization of the conditions of Theorem 11.

We would like to relate the necessary condition on the learnability of a class
of SFAs over a Boolean algebra $\mathpzc{A}$ to the learnability of the
Boolean algebra $\mathpzc{A}$ itself. For this we need to first define
efficient identifiability of a Boolean algebra $\mathpzc{A}$. Since to learn
an unknown predicate we need to supply two sets, one of negative examples and
one of positive examples, it makes sense to say that a Boolean algebra
$\mathpzc{A}$ with predicates ${\mathbb{P}}$ over domain $\mathbb{D}$ is
_efficiently identifiable_ if there exist efficient dyadic concretizing and
generalizing functions,
${\textsf{Concretize}}{A}:\Pi_{\textsf{pred}}({{\mathbb{P}}})\rightarrow\Pi_{\textsf{conc}}({\mathbb{D}})$
and
${\textsf{Generalize}}{A}:\Pi_{\textsf{conc}}({\mathbb{D}})\rightarrow\Pi_{\textsf{pred}}({{\mathbb{P}}})$
satisfying the criteria of Theorem 11. Using this terminology we can state the
following corollary.

######  Corollary 12.

Efficient identifiability of the Boolean algebra $\mathpzc{A}$ is a necessary
condition for identification in the limit using polynomial time and data of
any class of SFAs over $\mathpzc{A}$, that contains all basic SFAs over
$\mathpzc{A}$.

##  9\. Sufficient Condition

We turn to discuss a sufficient condition for the efficient identifaibility of
a class of SFAs ${\mathbb{M}}{A}$ over a Boolean algebra $\mathpzc{A}$. To
prove that ${\mathbb{M}}{A}$ is efficiently identifiable, we need to supply
two algorithms ${{\textbf{CharSFA}}}_{{\mathbb{M}}{A}}$ and
${{\textbf{{InferSFA}}}}_{{\mathbb{M}}{A}}$ as required in Definition 7.1. The
idea is to reduce the problem to efficient identifiablity of DFAs, namely to
use the algorithms CharDFA and InferDFA provided in Theorem 10. The
implementation of CharSFA, given an SFA $\mathcal{M}$ will transform it into a
DFA $\mathcal{D}_{\mathcal{M}}$ by applying ${\textsf{Concretize}}{A}$ on the
partitions induced by the states of the DFA. The resulting DFA
$\mathcal{D}_{\mathcal{M}}$ will not be equivalent to the given SFA
$\mathcal{M}$, but it may be used to create a sample of words
$\mathcal{S}_{\mathcal{M}}$ that is a characteristic set for $\mathcal{M}$,
see Figure 2.

To implement InferSFA we would like to use InferDFA to obtain, as a first
step, a DFA from the given sample, then at the second step, apply
${\textsf{Generalize}}{A}$ on the concrete-partitions induced by the DFA
states. A subtle issue that we need to cope with is that inference should
succeed also on samples subsuming the characteristic sample. The fact that
this holds for inference of the DFA does not suffice, since we are guaranteed
that the inference of the DFA will not be confused if the sample contains more
labeled words, as long as the new words are over the same alphabet. In our
case the alphabet of the sample can be a strict subset of the concrete letters
$\mathbb{D}$ (and if $\mathbb{D}$ is infinite, this surely will be the case).
Example 10 in section 10 illustrates this problem for the class of SFAs over a
monotonic algebra $\mathpzc{A_{m}}$, for which the respective methods
${\textsf{Concretize}}{A_{m}}$ and ${\textsf{Generalize}}{A_{m}}$ exist. So we
need an additional step to remove words from the given sample if they are not
over the alphabet of the characteristic sample. We call a method implementing
this ${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$.

Figure 2. A schematic description of algorithms CharSFA and InferSFA

Formally, we first define the extension of ${\textsf{Concretize}}{A}$ and
${\textsf{Generalize}}{A}$ to automata instead of partitions, which we term
${\textsf{Concretize}}_{{\mathbb{M}}{A}}$ and
${\textsf{Generalize}}_{{\mathbb{M}}{A}}$ (with ${\mathbb{M}}$ in the
subscript).

Algorithm 1 ${\textsf{Concretize}}_{{\mathbb{M}}{A}}(\mathcal{M})$

Algorithm 2 ${\textsf{Generalize}}_{{\mathbb{M}}{A}}(\mathcal{M})$

  * •

The formal definition of ${\textsf{Concretize}}_{{\mathbb{M}}{A}}$ is given in
Algorithm 1. Let $\mathcal{M}=(\mathpzc{A},Q,q_{\iota},F,\Delta)$ be an SFA.
Then ${\textsf{Concretize}}_{{\mathbb{M}}{A}}(\mathcal{M})$ is the DFA
$\mathcal{D}_{\mathcal{M}}=(\Sigma,Q,q_{\iota},F,\Delta_{\mathcal{D}})$ where
$\Delta_{\mathcal{D}}$ is defined as follows. For each state $q\in Q$ let
$\pi_{q}=\langle\psi_{1},\ldots,\psi_{m}\rangle$ be the predicate partition
consisting of all predicates labeling a transition exiting $q$ in
$\mathcal{M}$. Intuitively, in $\mathcal{D}$, the outgoing transitions of each
state $q$ correspond to ${\textsf{Concretize}}{A}(\pi_{q})$. That is, let
${\textsf{Concretize}}{A}(\pi_{q})=\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle$.
Then, if $\langle q,\psi_{i},q^{\prime}\rangle\in\Delta$, then $\langle
q,\gamma,q^{\prime}\rangle\in\Delta_{\mathcal{D}}$ for every
$\gamma\in\Gamma_{i}$.

  * •

The formal definition of ${\textsf{Generalize}}_{{\mathbb{M}}{A}}$ is given in
Algorithm 2. Let $\mathcal{D}=(\Sigma,Q,q_{\iota},F,\Delta_{\mathcal{D}})$ be
a DFA. We define ${\textsf{Generalize}}_{{\mathbb{M}}{A}}(\mathcal{D})$ with
respect to an algebra $\mathpzc{A}$ as follows. Let
$\mathcal{M}=(\mathpzc{A},Q,q_{\iota},F,\Delta_{\mathcal{M}})$ where
$\Delta_{\mathcal{M}}$ is defined as follows. For each state $q\in Q$ let
$\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle$ be the concrete partition
consisting of letters labeling outgoing transitions from $q$. Note that
$\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle$ is a concrete partition, since
$\mathcal{D}$ is a DFA. Let
${\textsf{Generalize}}{A}(\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle)=\langle\psi_{1},\ldots,\psi_{m}\rangle$.
Then, $\langle q,\psi_{i},q^{\prime}\rangle\in\Delta_{\mathcal{M}}$ if
$\Gamma_{i}$ is the set of letters labeling transitions from $q$ to
$q^{\prime}$ in $\mathcal{D}$.

We are now ready to define the conditions the _decontaminating_ function has
to satisfy. We recall that the role of the decontaminating function is to
identify words in the sample that are not over the alphabet
$\Gamma_{\mathcal{D}}$ of the characteristic sample (note that
$\Gamma_{\mathcal{D}}$ is not known to the decontaminating function).

A function $f_{d}:2^{(\mathbb{D}^{*}\times\\{0,1\\})}\rightarrow
2^{(\mathbb{D}^{*}\times\\{0,1\\})}$ is called _decontaminating_ for a class
of SFAs ${\mathbb{M}}$ and a respective ${\textsf{Concretize}}_{\mathbb{M}}$
function if the following holds. Let $\mathcal{M}\in{\mathbb{M}}$ be an SFA,
and $\mathcal{D}={\textsf{Concretize}}_{\mathbb{M}}(\mathcal{M})$. Let
$\mathcal{S_{\mathcal{D}}}={{\textbf{{CharDFA}}}}(\mathcal{D})$. Then, for
every $\mathcal{S}^{\prime}\supseteq\mathcal{S}_{\mathcal{D}}$ such that
$\mathcal{S}^{\prime}$ agrees with $\mathcal{M}$, it holds that
$\mathcal{S}_{\mathcal{D}}\subseteq
f_{d}(\mathcal{S}^{\prime})\subseteq(\mathcal{S}^{\prime}\cap\Gamma_{\mathcal{D}})$,
where $\Gamma_{\mathcal{D}}$ is the alphabet of $\mathcal{S}_{\mathcal{D}}$.

As before we say that $f_{d}$ is _efficient_ if it can be computed in
polynomial time.

Intuitively, InferDFA is only promised to be correct if it is applied on a
sample set $\mathcal{S}^{\prime}$ over the alphabet of the original DFA. For
DFAs, this is always the case. However for SFAs, the concrete alphabet
$\mathbb{D}$ usually contains more letters than appear in the characteristic
set $\mathcal{S}$. If $\Gamma_{D}$ is the set of letters in $\mathcal{S}$ then
$\mathcal{S}^{\prime}$ might contain letters in
$\mathbb{D}\setminus\Gamma_{D}$, i.e. letters that are not from the alphabet
of the characteristic set. Consider, for example, the characteristic set
$\mathcal{S}$ over the interval algebra

$\mathcal{S}=\\{\langle\epsilon,0\rangle,\langle 0,1\rangle,\langle
100,0\rangle,\langle 200,0\rangle,\langle 0\cdot 0,1\rangle,\langle 0\cdot
100,1\rangle,\langle 0\cdot 200,0\rangle\\}$

And consider the set $\mathcal{S}^{\prime}\supseteq\mathcal{S}$ that contains,
in addition to the words in $\mathcal{S}$, also the word $150\cdot 100$. Since
the letter $150$ is not part of any word in the original set $\mathcal{S}$, we
cannot apply InferDFA as it is, but we first need to remove it from
$\mathcal{S}^{\prime}$. Note that words that are not in $\mathcal{S}$ but are
over the alphabet $\\{0,100,200\\}$ do not pose a problem, as InferDFA can
handle supersets over the same alphabet as the set $\mathcal{S}$. See Examples
10 and 10 in section 10 for more details.

We now provide the sufficient condition for efficient identifiability.

######  Theorem 13.

Let ${\mathbb{M}}{A}$ be a class of SFAs over a Boolean algebra $\mathpzc{A}$.
If there exist an efficient decontaminating function
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$ and efficient functions
${\textsf{Concretize}}{A}$ and ${\textsf{Generalize}}{A}$ satisfying that

if
${\textsf{Concretize}}{A}(\langle\psi_{1},\ldots,\psi_{m}\rangle)=\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle$

and
${\textsf{Generalize}}{A}(\langle\Gamma^{\prime}_{1},\ldots,\Gamma^{\prime}_{m}\rangle)=\langle\varphi_{1},\ldots,\varphi_{m}\rangle$

where $\Gamma_{i}\subseteq\Gamma^{\prime}_{i}$ for every $1\leq i\leq m$

then $\llbracket{\varphi_{i}}\rrbracket=\llbracket{\psi_{i}}\rrbracket$ for
every $1\leq i\leq m$

then the class ${\mathbb{M}}{A}$ is efficiently identifiable.

Given functions ${\textsf{Concretize}}_{\mathpzc{A}}$,
${\textsf{Generalize}}_{\mathpzc{A}}$ and
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$ for a class ${\mathbb{M}}{A}$ of
SFAs over a Boolean algebra $\mathpzc{A}$ meeting the criteria of Theorem 13,
we show that ${\mathbb{M}}{A}$ can be efficiently identified by providing two
algorithms CharSFA and InferSFA, described below. These algorithms make use of
the respective algorithms CharDFA and InferDFA guaranteed in Theorem 10.I., as
well as the methods provided by the theorem.

We briefly describe these two algorithms, and then turn to prove Theorem 13.
The algorithm CharSFA receives an SFA ${\mathcal{M}\in{\mathbb{M}}}$, and
returns a characteristic sample for it. It does so by applying
${\textsf{Concretize}}_{{\mathbb{M}}{A}}(\mathcal{M})$ (Algorithm 1) to
construct a DFA $\mathcal{D}_{\mathcal{M}}$ and generating the sample
$\mathcal{S}_{\mathcal{M}}$ using the algorithm CharDFA applied on the DFA
$\mathcal{D}_{\mathcal{M}}$.

Algorithm InferSFA, given a sample set $\mathcal{S}$, if $\mathcal{S}$
subsumes a characteristic set of an SFA $\mathcal{M}$, returns an equivalent
SFA. Otherwise InferSFA returns an SFA that agrees with the sample
$\mathcal{S}$. First, it applies ${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$
to find a subset $\mathcal{S^{\prime}}\subseteq\mathcal{S}$ over the alphabet
of the subsumed characteristic sample, if such a subsumed sample exists. Then
it uses $\mathcal{S^{\prime}}$ to construct a DFA by applying the inference
algorithm InferDFA on $\mathcal{S^{\prime}}$. From this DFA it constructs an
SFA, $\mathcal{M}_{\mathcal{S}}$, by applying
${\textsf{Generalize}}_{{\mathbb{M}}{A}}$ (Algorithm 2). If the resulting
automaton disagrees with the given sample it resorts to returning the prefix-
tree automaton. In order to construct the symbolic prefix-tree automaton we
first construct the prefix-tree DFA $\mathcal{A}$ for the set $\mathcal{S}$,
and then apply ${\textsf{Generalize}}_{{\mathbb{M}}{A}}(\mathcal{A})$ to get
an SFA that agrees with $\mathcal{S}$.

In brief, we define:

  * •

${{\textbf{CharSFA}}}(\mathcal{M})={{\textbf{{CharDFA}}}}({\textsf{Concretize}}_{{\mathbb{M}}{A}}(\mathcal{M}))$

  * •

${{\textbf{{InferSFA}}}}(\mathcal{S})=\begin{cases}\mathcal{M}_{\mathcal{S}}:={\textsf{Generalize}}_{{\mathbb{M}}{A}}({{\textbf{{InferDFA}}}}({\textsf{Decontaminate}}_{{\mathbb{M}}{A}}(\mathcal{S})))&\text{if
$\mathcal{S}\subseteq\hat{\mathcal{L}}({\mathcal{M}_{\mathcal{S}}})$ }\\\
\text{The symbolic prefix-tree automaton of
$\mathcal{S}$}&\text{otherwise}\end{cases}$

In section 10 we provide methods ${\textsf{Concretize}}_{\mathpzc{A}}$,
${\textsf{Generalize}}_{\mathpzc{A}}$ and
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$ for SFAs over monotonic algebras,
deriving their identification in the limit result. We now prove Theorem 13.

######  Proof 9.1 (Proof of Theorem 13).

Given functions ${\textsf{Concretize}}{A}$, ${\textsf{Generalize}}{A}$, and
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$, we show that the algorithms
CharSFA and InferSFA satisfy the requirements of Definition 7.1.

For the first condition, given that CharDFA,
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$ and ${\textsf{Generalize}}{A}$
run in polynomial time, and that the prefix-tree automaton can be constructed
in polynomial time, it is clear that so does InferSFA. In addition, the test
performed in the definition of InferSFA ensures the output agrees with the
sample.

For the second condition, note that the sample generated by CharSFA is
polynomial in the size of $\mathcal{D}_{\mathcal{M}}$, from the correctness of
CharDFA. In addition, since ${\textsf{Concretize}}{A}$ is efficient,
$\mathcal{D}_{\mathcal{M}}$ is polynomial in the size of $\mathcal{M}$, and
thus $\mathcal{S}_{\mathcal{M}}$ generated by CharSFA is polynomial in
$\mathcal{M}$ as well. It is left to show that given
$\mathcal{S}_{\mathcal{M}}$ is the concrete sample produced by CharSFA when
running on an SFA $\mathcal{M}$, then when InferSFA runs on any sample
$\mathcal{S}\supseteq\mathcal{S}_{\mathcal{M}}$ it returns an SFA for
$\mathcal{L}({\mathcal{M}})$. Since
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$ is a decontaminating function,
and $\mathcal{S}\supseteq\mathcal{S}_{\mathcal{M}}$, it holds that the set
$\mathcal{S^{\prime}}={\textsf{Decontaminate}}_{{\mathbb{M}}{A}}(\mathcal{S})$
is such that $\mathcal{S^{\prime}}\supseteq\mathcal{S}_{\mathcal{M}}$ and is
only over the alphabet $\Gamma_{\mathcal{M}}$, which is the alphabet of the
DFA $\mathcal{D}_{\mathcal{M}}$ generated in Algorithm 1.

From the correctness of InferDFA, given
$\mathcal{S^{\prime}}\supseteq\mathcal{S}_{\mathcal{M}}$, applying InferDFA on
the output $\mathcal{S}^{\prime}$ of
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$ results in a DFA $\mathcal{D}$
that is equivalent to $\mathcal{D}_{\mathcal{M}}$ constructed in Algorithm 1.
Since $\mathcal{D}_{\mathcal{M}}$ is complete with respect to its alphabet
$\Gamma_{\mathcal{M}}$, for state $q$ of $\mathcal{D}$, the concrete partition
$\langle\Gamma_{1},\ldots,\Gamma_{n}\rangle$ generated in Algorithm 2, line 4,
covers $\Gamma_{\mathcal{M}}$ and subsumes the output of
${\textsf{Concretize}}_{{\mathbb{M}}{A}}$ on $\pi_{q}$ (Algorithm 1, line 2).
Thus, since ${\textsf{Generalize}}{A}$ and ${\textsf{Concretize}}{A}$ satisfy
the criteria of Theorem 13, it holds that the constructed predicates agree
with the original predicates. In addition, since $\mathcal{S}$, and therefore
$\mathcal{S^{\prime}}$, agrees with $\mathcal{M}$, the test performed in the
definition of InferSFA succeeds and the returned SFA is equivalent to
$\mathcal{M}$.

##  10\. Positive Result

We present the following positive result regarding monotonic algebras.

######  Theorem 14.

Let ${\mathbb{M}}_{\mathpzc{A_{m}}}$ be the set of SFAs over a monotonic
Boolean algebra $\mathpzc{A_{m}}$. Then ${\mathbb{M}}_{\mathpzc{A_{m}}}$ is
efficiently identifiable.

In order to prove Theorem 14, we show that the sufficient condition holds for
the case of monotonic algebras. Example 10 demonstrates how to apply CharSFA
and InferSFA in order to learn an SFA over the algebra
$\mathpzc{A_{\mathbb{N}}}$.

######  Proposition 15.

There exist functions ${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ and
${\textsf{Generalize}}_{\mathpzc{A_{m}}}$ for a monotonic Boolean algebra
$\mathpzc{A_{m}}$, satisfying the criteria of Theorem 13.

######  Proof 10.1.

Let $\mathbb{D}$ be the domain of $\mathpzc{A_{m}}$. We provide the functions
${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ and
${\textsf{Generalize}}_{\mathpzc{A_{m}}}$ and prove that the criteria of
Theorem 13 hold for them. For ease of presentation, for the function
${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ we consider basic predicates. Note
that for monotonic algebras, basic predicates are in fact intervals, as a
conjunction of intervals is an interval. We can assume all predicates are
basic since, as we show in Lemma 3, for monotonic algebras the transformation
from a general formula to a DNF formula of basic predicates is linear. Then,
each basic predicate in the formula corresponds to a different predicate in
the predicate partition. The definitions of
${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ and
${\textsf{Generalize}}_{\mathpzc{A_{m}}}$ are generalizations of the functions
${\textsf{Concretize}}_{\mathpzc{A_{\mathbb{N}}}}$ and
${\textsf{Generalize}}_{\mathpzc{A_{\mathbb{N}}}}$ given in Example 8. We
define
${\textsf{Concretize}}_{\mathpzc{A_{m}}}(\langle\psi_{1},\ldots\psi_{m}\rangle)=\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle$
where we set $\Gamma_{i}=\\{\
\min\\{{d\in\mathbb{D}}\,|\,{d\in\llbracket{\psi_{i}}\rrbracket}\\}\ \\}$ for
$1\leq i\leq m$. Since $\mathpzc{A_{m}}$ is monotonic, $\Gamma_{i}$ is well-
defined and contains a single element, thus
${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ is an efficient concretizing
function.

We define
${\textsf{Generalize}}_{\mathpzc{A_{m}}}(\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle)=\langle\psi_{1},\ldots,\psi_{m}\rangle$,
where $\psi_{i}$ is defined as follows. Let $\Gamma=\bigcup_{1\leq i\leq
m}\Gamma_{i}$. First, for all $1\leq i\leq m$ we set $\psi_{i}=\bot$. Then, we
iteratively look for the minimal element $\gamma\in\Gamma$. Let $i$ be such
that $\gamma\in\Gamma_{i}$, and let $\gamma^{\prime}$ be the minimal element
in $\Gamma$ satisfying $\gamma^{\prime}\notin\Gamma_{i}$. We then set
$\psi_{i}=\psi_{i}\vee[\gamma,\gamma^{\prime})$, and remove all elements
$\gamma\leq\gamma^{\prime\prime}<\gamma^{\prime}$ from $\Gamma$. We repeat the
process until for the found $\gamma\in\Gamma_{j}$, there is no
$\gamma^{\prime}>\gamma$ such that $\gamma^{\prime}\notin\Gamma_{j}$. In that
case, we define $\psi_{j}=\psi_{j}\vee[\gamma,d_{\infty})$. Then,
$\Gamma_{i}\subseteq\llbracket{\psi_{i}}\rrbracket$ and the predicates are
disjoint, thus ${\textsf{Generalize}}_{\mathpzc{A_{m}}}$ is an efficient
generalizing function. See Example 10 and Figure 3.

Now, let $\langle\Gamma_{1},\ldots,\Gamma_{m}\rangle$ be the concrete
partition obtained from ${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ when applied
on the predicate partition $\langle\psi_{1},\ldots,\psi_{m}\rangle$. Assume
further that the predicate partition
$\langle\Gamma^{\prime}_{1},\ldots,\Gamma^{\prime}_{m}\rangle$ satisfies
$\Gamma_{i}\subseteq\Gamma^{\prime}_{i}\subseteq\llbracket{\psi_{i}}\rrbracket$
for $1\leq i\leq m$. In particular,
$\min(\Gamma^{\prime}_{i})=\min(\Gamma_{i})$, since $\Gamma_{i}$ contains the
minimal elements in $\llbracket{\psi_{i}}\rrbracket$, and
$\Gamma_{i}\subseteq\Gamma^{\prime}_{i}\subseteq\llbracket{\psi_{i}}\rrbracket$.
Thus applying ${\textsf{Generalize}}_{\mathpzc{A_{m}}}$ will result in the
same interval, satisfying the criterion of Theorem 13.

(a)

(b)

Figure 3. Visualisation of Example 10

Let $\Gamma_{1}=\\{0,100,400,500\\}$ and $\Gamma_{2}=\\{150,200\\}$ over the
algebra ${{\mathpzc{A_{\mathbb{N}}}}}$ with domain
$\mathbb{N}\cup\\{\infty\\}$, see Figure 3a. Then,
${\textsf{Generalize}}{A_{\mathbb{N}}}$ sets
$\Gamma=\\{0,100,150,200,400,500\\}$, and finds the minimal element in
$\Gamma$, which is $0$. Since $0\in\Gamma_{1}$, it then looks for the minimal
element $\gamma\in\Gamma$ such that $\gamma\notin\Gamma_{1}$, and finds
$150\in\Gamma_{2}$. Therefore $\psi_{1}=[0,150)$ and we remove from $\Gamma$
all elements in $[0,150)$, that is, we remove $0$ and $100$, and we have
$\Gamma=\\{150,200,400,500\\}$. Next, it finds the minimal element in the
updated $\Gamma$, which is $150$ and is in $\Gamma_{2}$. The minimal element
in $\Gamma\setminus\Gamma_{2}$ is $400$. Then, $\psi_{2}$ is set to be
$\psi_{2}=[150,400)$ and $\Gamma=\\{400,500\\}$. Now,
$\psi_{1}=[0,150)\vee[400,\infty)$ since $400\in\Gamma_{1}$ and there is no
greater element that is not in $\Gamma_{1}$ (Figure 3b).

To show that any class of SFAs ${\mathbb{M}}{A_{m}}$ over a monotonic algebra
$\mathpzc{A_{m}}$ is efficiently identifiable, we define in Algorithm 3 an
algorithm that implements a decontaminating function
${\textsf{Decontaminate}}_{{\mathbb{M}}{A_{m}}}$, that fulfills the
requirements of Theorem 13. Loosely speaking, the idea of the algorithm is to
simultaneously collect elements into two sets $A_{w}$ and $\Sigma^{\prime}$
such that $A_{w}$ will consist of the minimal representative according to the
lexicographic order of each equivalence class in $\sim_{\mathcal{S}}$ and
$\Sigma^{\prime}$ will consist of minimal letters aiding to distinguishing
these words. When this process terminates the algorithm returns the subset of
words in the sample that consist of only letters in $\Sigma^{\prime}$.

Algorithm 3 ${\textsf{Decontaminate}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}$ –
finding the necessary letters for a characteristic sample

######  Lemma 16.

Assume the input to
${\textsf{Decontaminate}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}$ is $\mathcal{S}$,
where $\mathcal{S}\supseteq\mathcal{S}_{\mathcal{M}}$ for some
$\mathcal{M}\in{\mathbb{M}}_{\mathpzc{A_{m}}}$ such that
$\mathcal{S}_{\mathcal{M}}={{\textbf{{CharDFA}}}}({\textsf{Concretize}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}(\mathcal{M}))$,
and
$\mathcal{D}_{\mathcal{M}}={\textsf{Concretize}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}(\mathcal{M})$
is over the alphabet $\Gamma_{\mathcal{M}}$. Then for $\Sigma^{\prime}$
constructed by ${\textsf{Decontaminate}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}$
(Algorithm 3) it holds that $\Sigma^{\prime}\\!=\\!\Gamma_{\mathcal{M}}$.

######  Proof 10.2.

Let $\mathcal{M}=(\mathpzc{A},Q,q_{\iota},F,\Delta_{\mathcal{M}})$,
$\mathcal{D}_{\mathcal{M}}={\textsf{Concretize}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}(\mathcal{M})$
and
$\mathcal{S}_{\mathcal{M}}={{\textbf{{CharDFA}}}}(\mathcal{D}_{\mathcal{M}})$.
Assume
$\mathcal{D}_{\mathcal{M}}=(\Gamma_{\mathcal{M}},Q,q_{\iota},F,\Delta_{\mathcal{D}})$.
We inductively show that for
${\textsf{Decontaminate}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}$ given in Algorithm
3, if its input $\mathcal{S}$ satisfies
$\mathcal{S}\supseteq\mathcal{S}_{\mathcal{M}}$ then the set $A_{w}$ is
exactly the set of all lex-access words (lexicographically smallest access
words) of states in $\mathcal{D}_{\mathcal{M}}$ and that
$\Sigma^{\prime}=\Gamma_{\mathcal{M}}$ (where $\Gamma_{\mathcal{M}}$ is the
alphabet of $\mathcal{D}_{\mathcal{M}}$).

First, we show that every $u\in A_{w}$ is a lex-access word and that
$\Sigma^{\prime}\subseteq\Gamma_{\mathcal{M}}$.

For the base case, we consider $A_{w}=\\{\epsilon\\}$ and
$\Sigma^{\prime}=\\{d_{-\infty}\\}$. From item 1 of Theorem 10, we can assume
access words are minimal according to the lexicographic order. Thus,
$\epsilon\in A_{w}$ is indeed a lex-access word (of the state $q_{\iota}$).
For $d_{-\infty}\in\Sigma^{\prime}$, it holds that $\Gamma_{\mathcal{M}}$
contains the minimal element of $\mathbb{D}$ since it contains all
concretizations of intervals, the SFA is complete and
${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ returns the minimal element of each
interval. Therefore $d_{-\infty}\in\Gamma_{\mathcal{M}}$.

For the induction step, assume that $A_{w}$ contains only lex-access words and
that the current $\Sigma^{\prime}$ is a subset of $\Gamma_{\mathcal{M}}$.
Then, when considering $u\in A_{w}$ in line 4, it holds that $u$ is a lex-
access word of some state $q$. Then, $\sigma$ is added to $\Sigma^{\prime}$
only if $u\sigma\not\sim_{\mathcal{S}}ud_{-\infty}$. Since $\mathcal{S}$
agrees with $\mathcal{M}$, it holds that
$\Delta_{\mathcal{M}}(q_{\iota},u\sigma)\neq\Delta_{\mathcal{M}}(q_{\iota},ud_{-\infty})$
and $\sigma$ is a minimal element with that property. Then, $\sigma$ must be a
minimal element of an interval labeling an outgoing transition from $q$,
therefore is in $\Gamma_{\mathcal{M}}$. Inductively this holds for all
elements added to $\Sigma^{\prime}$ in the current iteration. This proves that
$\Sigma^{\prime}\subseteq\Gamma_{\mathcal{M}}$. Assume now that $A_{w}$
contains only lex-access words and let $u\sigma$ be a word added to $A_{w}$ in
line 9. Thus, for all $u^{\prime}\in A_{w}$ it holds that
$u\sigma\not\sim_{\mathcal{S}}u^{\prime}$.

  * Claim. In this setting, $u\sigma\not\sim_{\mathcal{S}}u^{\prime}$ implies $u\sigma\not\sim_{\mathcal{S}_{\mathcal{M}}}u^{\prime}$.

  * Proof. Since we assume all words already in $A_{w}$ are lex-access words, then in particular $u$ is a lex-access word. In addition, $\sigma\in\Sigma^{\prime}$ and thus $\sigma\in\Gamma_{\mathcal{M}}$. Since $u\sigma\not\sim_{\mathcal{S}}u^{\prime}$ there is $z\in\Sigma^{*}$ such that $\langle u\sigma z,b_{1}\rangle,\langle u^{\prime}z,b_{2}\rangle\in\mathcal{S}$ and $b_{1}\neq b_{2}$. Since $\mathcal{S}$ agrees with $\mathcal{M}$ it holds that $\Delta_{\mathcal{M}}(q_{\iota},u\sigma)\neq\Delta_{\mathcal{M}}(q_{\iota},u^{\prime})$. Now, $u\sigma$ and $u^{\prime}$ are all in $\Gamma_{\mathcal{M}}$ since from line 9 we have $A_{w}\subseteq\Sigma^{\prime*}$, and thus $\Delta_{\mathcal{D}_{\mathcal{M}}}(q_{\iota},u\sigma)\neq\Delta_{\mathcal{D}_{\mathcal{M}}}(q_{\iota},v)$, and from item 3 of Theorem 10 it holds that $u\sigma\not\sim_{\mathcal{S}_{\mathcal{M}}}u^{\prime}$. This proves the claim.

Then, for all $u^{\prime}\in A_{w}$ we have
$\Delta_{\mathcal{D}}(q_{\iota},u\sigma)\neq\Delta_{\mathcal{D}}(q_{\iota},u^{\prime})$.
Then, since we traverse words and letters in lexicographic order, $u\sigma$ is
a lex-access word for $\Delta_{\mathcal{D}}(q_{\iota},u\sigma)$. This
concludes the first direction.

For the second direction, we show that every lex-access word is in $A_{w}$ and
that $\Gamma_{\mathcal{M}}\subseteq\Sigma^{\prime}$.

Let $u\sigma$ be a lex-access word (for $\epsilon$ it holds that $\epsilon\in
A_{w}$). For all lex-access words $u^{\prime}$ found in previous iterations it
holds that $u\sigma\not\sim_{\mathcal{S}_{\mathcal{M}}}u^{\prime}$ from item 2
of Theorem 10, and thus $u\sigma\not\sim_{\mathcal{S}}u^{\prime}$ since
$\mathcal{S}_{\mathcal{M}}\subseteq\mathcal{S}$. Then, $u\sigma$ satisfies the
condition of line 9 and is added to $A_{w}$.

To prove $\Gamma_{\mathcal{M}}\subseteq\Sigma^{\prime}$, let
$\sigma\in\Gamma_{\mathcal{M}}$. From the construction of
${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ it holds that $\sigma$ is the left
endpoint of some interval that is an outgoing transition from $q_{\iota}$.
Then, indeed $\sigma$ is found in the first iteration of line 4. Inductively,
let $\sigma$ label an outgoing transition of $q$ for some $q\in Q$ and let
$u_{q}$ be the lex-access word of $q$. Since $A_{w}$ contains all lex-access
words, it holds that $u_{q}\in A_{w}$, and then the outgoing transitions of
$q$ will be considered in some following iteration. Thus, all minimal letters
indicating new intervals are added to $\Sigma^{\prime}$ and we have that
$\Gamma_{\mathcal{M}}\subseteq\Sigma^{\prime}$. We conclude that
$\Sigma^{\prime}=\Gamma_{\mathcal{M}}$.

######  Proposition 17.

The sufficient condition of Theorem 13 holds for the class
${\mathbb{M}}_{\mathpzc{A_{m}}}$ of SFAs over a monotonic Boolean algebra
$\mathpzc{A_{m}}$.

######  Proof 10.3.

In Proposition 15 we have shown that there exist functions
${\textsf{Concretize}}_{\mathpzc{A_{m}}}$ and
${\textsf{Generalize}}_{\mathpzc{A_{m}}}$ for a monotonic Boolean algebra
$\mathpzc{A_{m}}$, satisfying the criteria of Theorem 13. It is left to show
that ${\textsf{Decontaminate}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}$ is an
efficient decontaminating function. Assume that
$\mathcal{S}\supseteq\mathcal{S}_{\mathcal{M}}$ where
$\mathcal{S}_{\mathcal{M}}={{\textbf{{CharDFA}}}}({\textsf{Concretize}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}\\!(\mathcal{M}))$,
and ${\textsf{Concretize}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}\\!(\mathcal{M})$
is over alphabet $\Gamma_{\mathcal{M}}$. In Lemma 16 we showed that under
these assumptions it holds that the alphabet $\Sigma^{\prime}$ of the returned
sample $\mathcal{S^{\prime}}$ is $\Gamma_{\mathcal{M}}$. Then, for the set
$\mathcal{S^{\prime}}$ returned in line 13 (Algorithm 3) it holds that
$\mathcal{S^{\prime}}=\mathcal{S}\cap\Gamma_{\mathcal{M}}^{*}$. Since
$\mathcal{S}\supseteq\mathcal{S}_{\mathcal{M}}$ and
$\Gamma_{\mathcal{M}}^{*}\supseteq\mathcal{S}_{\mathcal{M}}$, it holds that
$\mathcal{S^{\prime}}\supseteq\mathcal{S}_{\mathcal{M}}$ and is defined over
the alphabet $\Gamma_{\mathcal{M}}$. Therefore,
${\textsf{Decontaminate}}_{{\mathbb{M}}_{\mathpzc{A_{m}}}}$ is a
decontaminating function. In addition, it runs in time polynomial in the size
of $\mathcal{S}$, thus the conditions of Theorem 13 are met.

We now provide an example for efficient identification of SFAs over the
interval algebra (Example 10), and an example for the need of a
decontaminating function (Example 10).

Continuing Example 8, let $\mathcal{M}$ be the SFA from Figure 1 and consider
the class ${\mathbb{M}}_{{\mathpzc{A_{\mathbb{N}}}}}$ of SFAs over the
interval algebra. Algorithm CharSFA computes the set $\Gamma_{\mathcal{M}}$
using the function
${\textsf{Concretize}}_{{\mathbb{M}}_{{\mathpzc{A_{\mathbb{N}}}}}}$ given in
Example 8. That is, for the predicates labeling outgoing transitions from
$q_{0}$ we have
${\textsf{Concretize}}_{{\mathpzc{A_{\mathbb{N}}}}}(\langle[0,100),[100,\infty)\rangle)=\langle\\{0\\},\\{100\\}\rangle$;
and for outgoing transitions from $q_{1}$, it holds that
${\textsf{Concretize}}_{{\mathpzc{A_{\mathbb{N}}}}}(\langle[0,200),[200,\infty)\rangle)=\langle\\{0\\},\\{200\\}\rangle$.
Then, $\Gamma_{\mathcal{M}}=\\{0,100,200\\}$, and CharSFA constructs the DFA
over $\Gamma_{\mathcal{M}}$ where concrete transitions agree with symbolic
transitions of the original SFA. See Figure 4 for the resulting DFA. Then,
using CharDFA, it returns the sample set

$\mathcal{S}_{\mathcal{M}}=\\{\langle\epsilon,0\rangle,\langle
0,1\rangle,\langle 100,0\rangle,\langle 200,0\rangle,\langle 0\cdot
0,1\rangle,\langle 0\cdot 100,1\rangle,\langle 0\cdot 200,0\rangle\\}.$

Now, assume algorithm InferSFA is given the set
$\mathcal{S}=\mathcal{S}_{\mathcal{M}}\cup\\{\langle 150,0\rangle\\}$ over the
alphabet $\Sigma=\\{0,100,150,200\\}$. The algorithm applies
${\textsf{Decontaminate}}_{{\mathbb{M}}_{{\mathpzc{A_{\mathbb{N}}}}}}$ that
generates the set $\mathcal{S^{\prime}}$ over $\Gamma_{\mathcal{M}}$. To do
so, it first finds the set $\Gamma_{\mathcal{M}}$ of all elements that are a
minimal left point of some interval, and then chooses from $\mathcal{S}$ the
words over $\Gamma_{\mathcal{M}}$. It does so as follows. First, note that
$100\sim_{\mathcal{S}}150$, $100\sim_{\mathcal{S}}200$ and
$150\sim_{\mathcal{S}}200$, while $0\not\sim_{\mathcal{S}}100,150,200$. Since
$0$ is the minimal element it has to be in $\Gamma_{\mathcal{M}}$; and since
$100$ is the minimal element that is not equivalent to $0$ it has to define a
new interval and thus is in $\Gamma_{\mathcal{M}}$ as well. Next, we consider
suffixes of words over $\\{0,100\\}$. These are $0\cdot 0$ and $0\cdot 100$
which are equivalent, and $0\cdot 200$ which is not equivalent to the former.
Since $100$ is equivalent to $0$ it does not define a new interval now, but
$200$ does as it is the minimal (and only) element that is not equivalent to
$0$ when considering suffixes of $0$. Then, we deduce that
$\Gamma_{\mathcal{M}}=\\{0,100,200\\}$ and thus
$\mathcal{S^{\prime}}=\\{\langle\epsilon,0\rangle,\langle 0,1\rangle,\langle
100,0\rangle,\langle 200,0\rangle,\langle 0\cdot 0,1\rangle,\langle 0\cdot
100,1\rangle,\langle 0\cdot 200,0\rangle\\}$.

Now Algorithm InferSFA is applied to the set $\mathcal{S^{\prime}}$ and the
resulting DFA would be the DFA $\mathcal{D}_{\mathcal{M}}$ of Figure 4. Then
it applies ${\textsf{Generalize}}_{{\mathbb{M}}_{{\mathpzc{A_{\mathbb{N}}}}}}$
described in Example 8 and the result will be the original SFA of Figure 1.
That is, for outgoing transitions of $q_{0}$ it applies
${\textsf{Generalize}}_{\mathpzc{A_{\mathbb{N}}}}(\langle\\{0\\},\\{100,200\\}\rangle)=\langle[0,100),[100,\infty)\rangle$
and for outgoing transitions of $q_{1}$ it applies
${\textsf{Generalize}}_{\mathpzc{A_{\mathbb{N}}}}(\langle\\{0,100\\},\\{200\\}\rangle)=\langle[0,200),[200,\infty)\rangle$
and uses these predicates to annotate the corresponding transitions in the
SFA.

$q_{0}$$q_{1}$$0$$0,100$$100,200$$200$ Figure 4. The DFA
$\mathcal{D}_{\mathcal{M}}$ constructed in CharSFA

$q_{\iota}$$q_{1}$$q_{2}$$q_{3}$$[0,100)$$[100,\mbox{ }\infty)$$[100,\mbox{
}\infty)$$[0,100)$$[100,\mbox{ }\infty)$$[0,100)$$[0,\infty)$ Figure 5. The
SFA $\mathcal{M}_{1}$ $0$$100$$150$$0$$100$$0$$100$$0$$250$ Figure 6. The
prefix-tree automaton for the set $\mathcal{S}^{\prime}$ of Example 10

$q_{\iota}$$q_{1}$$q_{2}$$q_{3}$$0,150$$100$$100$$0,250$$100$$0$$0,100,150$ | $q_{\iota}$$q_{1}$$q_{2}$$q_{3}$$0$$100,150$$100$$0$$100,250$$0$$0,100,150$
---|---
Figure 7. Two DFAs that are consistent with the set $\mathcal{S}^{\prime}$ of
Example 10.

Consider the SFA $\mathcal{M}_{1}$ of Figure 5. Applying
${{\textbf{{CharDFA}}}}({\textsf{Concretize}}_{{\mathbb{M}}_{\mathpzc{A}_{\mathbb{N}}}}(\mathcal{M}_{1}))$
results in the following $\mathcal{S}$.

$\mathcal{S}=\\{\langle\epsilon,0\rangle,\langle 0,1\rangle,\langle
100,1\rangle,\langle 0\cdot 0,1\rangle,\langle 0\cdot 100,0\rangle,\langle
100\cdot 100,1\rangle,\langle 100\cdot 0,0\rangle,\langle 0\cdot 100\cdot
0,0\rangle\\}$

Now, let $\mathcal{S}^{\prime}=\mathcal{S}\cup\\{\langle 150,1\rangle,\langle
150\cdot 250,1\rangle\\}$. Note that $\mathcal{S}^{\prime}$ is consistent with
$\mathcal{L}(\mathcal{M}_{1})$. When trying to learn an SFA from
$\mathcal{S}^{\prime}$ and applying
${{\textbf{{InferDFA}}}}(\mathcal{S}^{\prime})$, the algorithm cannot
distinguish between the words $150$ and $100$, as well as between $0$ and
$150$. The same holds also for $0\cdot 0$ vs. $150\cdot 250$, and $100\cdot
100$ vs. $150\cdot 250$.

Figure 7 presents two DFAs that are both consistent with the set
$\mathcal{S}^{\prime}$. Since $\mathcal{S}^{\prime}$ does not contain any
characteristic sample for DFAs over the alphabet $\\{0,100,150,250\\}$,
InferDFA concludes that $\mathcal{S}^{\prime}$ does not subsume any
characteristic sample, and returns the prefix-tree automaton, given in Figure
6.

This example illustrates that InferSFA cannot classify $150$ and $150\cdot
250$ by only applying InferDFA, without reasoning about the predicates of the
algebra. To this end we provide the function
${\textsf{Decontaminate}}_{{\mathbb{M}}{A}}$, which is able, in the case of a
monotonic algebra, to find which letters are the ones that should be used to
define new predicates.

##  11\. Negative Result

The result of Theorem 14 does not extend to the non-monotonic case, as stated
in Theorem 18 regarding SFAs over the general propositional algebra. Let
$\mathbb{D}_{\mathbb{B}}=\\{{\mathbb{B}^{k}}\\}_{k\in\mathbb{N}}$. Recall that
$\mathbb{B}=\\{0,1\\}$ and $\mathbb{B}^{k}$ is the set of all valuations of
$k$ atomic propositions. Let
$\mathbb{P}_{\mathbb{B}}=\\{\mathbb{P}_{\mathbb{B}_{k}}\\}_{k\in\mathbb{N}}$
where $\mathbb{P}_{\mathbb{B}_{k}}$ is the set of predicates over at most $k$
atomic propositions. Let $\mathpzc{A}_{\mathbb{B}}$ be the Boolean algebra
defined over the discrete domain $\mathbb{D}_{\mathbb{B}}$ and the set of
predicates $\mathbb{P}_{\mathbb{B}}$, and the usual operators $\vee$, $\wedge$
and $\neg$. Let ${\mathbb{M}}_{\mathpzc{A}_{\mathbb{B}}}$ be the class of SFAs
over the Boolean algebra $\mathpzc{A}_{\mathbb{B}}$. We show that unless
$P=NP$, this class of SFAs is not efficiently identifiable.111111 This result
may be contrasted with the positive learnability result in [AD18] who provide
a positive learnability result regarding SFAs over the OBDDs algebra. The
result of [AD18] is with respect to query learning, while Theorem 18 concerns
efficient identifiability in the limit. As we discuss in Acknowledgments, one
cannot derive efficient learnability from a positive result in the query
learning setting. Moreover, in Theorem 18 (as well as in Corollary 21 and the
discussion in section 12) we refer to efficient learnability with respect the
propositional algebra as defined in subsection 2.1 where the size is measured
with respect to the number of atomic propositions, while [AD18] refer to the
size of the SFAs in which the predicates are OBDDs, whose size is measured by
the number of nodes in the OBDD. However, the number of nodes in an OBDD can
be exponential in the number of atomic propositions. Therefore, our result has
no conflict with the result of [AD18].

######  Theorem 18.

The class ${\mathbb{M}}_{\mathpzc{A}_{\mathbb{B}}}$ is not efficiently
identifiable unless $P=NP$.

######  Proof 11.1.

We show that there is no pair of efficient dyadic concretizing and
generalizing functions
$f_{c}:\Pi_{\textsf{pred}}({{\mathbb{P}}_{\mathbb{B}}})\rightarrow\Pi_{\textsf{conc}}({\mathbb{D}_{\mathbb{B}}})$
and
$f_{g}:\Pi_{\textsf{conc}}({\mathbb{D}_{\mathbb{B}}})\rightarrow\Pi_{\textsf{pred}}({{\mathbb{P}}_{\mathbb{B}}})$
unless $P=NP$. From Theorem 11 it follows that ${\mathbb{M}}_{\mathbb{B}}$ is
not efficiently identifiable unless $P=NP$.

Assume towards contradiction that such a pair of functions exist. We provide a
polynomial time algorithm $\textsf{A}_{\textsf{SAT}}$ for SAT. On predicate
$\varphi$, the algorithm $\textsf{A}_{\textsf{SAT}}$ invokes
$f_{c}(\langle\varphi,\neg\varphi\rangle)$. Suppose the returned concrete
partition is $\langle\Gamma_{1},\Gamma_{2}\rangle$. Then
$\textsf{A}_{\textsf{SAT}}$ returns “true” if and only if
$\Gamma_{1}\neq\emptyset$. Correctness follows from the fact that if there
exists a system of characteristic samples for $\mathbb{P}_{\mathbb{B}}$ then
the set of positive examples associated with a satisfiable predicate $\varphi$
must be non-empty, as otherwise $f_{g}$ cannot distinguish $\varphi$ from
$\bot$.

##  12\. Query Learning

The paradigm of _query learning_ stipulates that the _learner_ can interact
with an _oracle_ (_teacher_) by asking it several types of allowed queries. In
this section we consider these queries to be _membership queries_ (mq) and
_equivalence queries_ (eq). We say that a class ${\mathbb{C}}$ of automata is
efficiently learnable using mqs / eqs / both mqs and eqs if there is an
algorithm that for every language $L$ with a representation in ${\mathbb{C}}$
asks a polynomial number of mqs / eqs / both mqs and eqs and outputs an
automaton in ${\mathbb{C}}$ that is polynomial in the minimal representation
of $L$ in ${\mathbb{C}}$.

Angluin showed, on the negative side, that regular languages cannot be
efficiently learned (in the exact model) from only mqs [Ang81] or only eqs
[Ang90]. On the positive side, she showed that regular languages, represented
as DFAs, can be efficiently learned using both mqs and eqs [Ang87]. The
celebrated algorithm, termed ${{\textbf{L}}}^{*}$, was extended to learning
many other classes of languages and representations, e.g., [Sak90, BV96, AV10,
BHKL09, AEF15, MP95, AF16, NFZ21]. See the survey [Fis18] for more references.

In particular, an extension of ${{\textbf{L}}}^{*}$, termed
${{\textbf{MAT}}}^{*}$, to learn SFAs was provided in [AD18] which proved that
SFAs over an algebra $\mathpzc{A}$ can be efficiently learned using
${{\textbf{MAT}}}^{*}$ if and only if the underlying algebra is efficiently
learnable, and the size of disjunctions of $k$ predicates does not grow
exponentially in $k$.121212As is the case, for instance, in the OBDD (Ordered
Binary Decisions Diagrams) algebra [Bry86]. From this it was concluded that
SFAs over the following underlying algebras are efficiently learnable: Boolean
algebras over finite domains, equality algebra, tree automata algebra, and
SFAs algebra. Efficient learning of SFAs over a monotonic algebra using mq and
eq was established in [CDYS17], which improved the results of [MM14, MM17] by
using a binary search instead of a helpful teacher.

The result of [AD18] provides means to establish new positive results on
learning classes of SFAs using mqs and eqs, but it does not provide means for
obtaining negative results for query learning of SFAs using mqs and eqs. We
strengthen this result by providing a learnability result that is independent
of the use of a specific learning algorithm. In particular, we show that
efficient learnability of a Boolean algebra $\mathpzc{A}$ using mqs and eqs is
a necessary condition for the learnability of a class of SFAs over
$\mathpzc{A}$, as we state in Theorem 19.

######  Theorem 19.

A class of SFAs ${\mathbb{M}}$ over a Boolean algebra $\mathpzc{A}$, that
contains all basic SFAs over $\mathpzc{A}$, is polynomially learnable using mq
and eq, only if $\mathpzc{A}$ is polynomially learnable using mq and eq.

######  Proof 12.1.

Assume that ${\mathbb{M}}$ is polynomially learnable using mqs and eqs, using
an algorithm ${{\textbf{Q}}}_{{{\mathbb{M}}}}$. We show that there exists a
polynomial learning algorithm ${{\textbf{Q}}}_{{\mathpzc{A}}}$ for the algebra
$\mathpzc{A}$ using mqs and eqs. The algorithm
${{\textbf{Q}}}_{{\mathpzc{A}}}$ uses ${{\textbf{Q}}}_{{{\mathbb{M}}}}$ as a
subroutine, and behaves as a teacher for ${{\textbf{Q}}}_{{{\mathbb{M}}}}$.
Whenever ${{\textbf{Q}}}_{{{\mathbb{M}}}}$ asks an ${\mathbb{M}}$-mq on word
$\gamma_{1}\ldots\gamma_{k}$, if $k>1$ then ${{\textbf{Q}}}_{{\mathpzc{A}}}$
answers “no”. If $k\\!=\\!1$ then the ${\mathbb{M}}$-mq is essentially an
$\mathpzc{A}$-mq, thus ${{\textbf{Q}}}_{{\mathpzc{A}}}$ issues this query and
passes the answer to ${{\textbf{Q}}}_{{{\mathbb{M}}}}$. Whenever
${{\textbf{Q}}}_{{{\mathbb{M}}}}$ asks a ${\mathbb{M}}$-eq on SFA
$\mathcal{M}$, if $\mathcal{M}$ is not of the form $\mathcal{M}_{\psi}$ for
some $\psi$ (as defined in Definition 6) then ${{\textbf{Q}}}_{{\mathpzc{A}}}$
answers “no” to the ${\mathbb{M}}$-eq and returns some word
$w\in\mathcal{L}({\mathcal{M}})$ s.t. $|w|>1$ and $w$ was not provided before,
as a counterexample. To this aim it can record the largest counterexample
given so far (according to the lexicographic order) and return the next one in
this order. Otherwise (if the SFA is of the form $\mathcal{M}_{\psi}$ for some
$\psi$) ${{\textbf{Q}}}_{{\mathpzc{A}}}$ asks an $\mathpzc{A}$-eq on $\psi$.
If the answer is “yes” then ${{\textbf{Q}}}_{{\mathpzc{A}}}$ terminates and
returns $\psi$ as the result of the learning algorithm; if the answer to the
$\mathpzc{A}$-eq on $\psi$ is “no”, then the provided counterexample
$\langle\gamma,b_{\gamma}\rangle$ is passed back to
${{\textbf{Q}}}_{{{\mathbb{M}}}}$ together with the answer “no” to the
${\mathbb{M}}$-eq. It is easy to verify that ${{\textbf{Q}}}_{{\mathpzc{A}}}$
terminates correctly in polynomial time.

From Theorem 19 we derive what we believe to be the first negative result on
learning SFAs from mqs and eqs, as we show that SFAs over the propositional
algebra over $k$ variables $\mathpzc{A}_{{\mathbb{B}}_{k}}$ are not
polynomially learnable using mq and eq. Polynomiality is measured with respect
to the parameters $\langle n,m,l\rangle$ representing the size of the SFA and
the number $k$ of atomic propositions. Note that the algebra
$\mathpzc{A}_{{\mathbb{B}}_{k}}$ is a restriction of the algebra
$\mathpzc{A}_{\mathbb{B}}$ considered in section 11 and therefore implies a
negative result also with regard to the algebra $\mathpzc{A}_{\mathbb{B}}$
considered there.

We achieve this by showing that no learning algorithm A for the propositional
algebra using mqs and eqs can do better than asking $2^{k}$ mqs/eqs, where $k$
is the number of atomic propositions.131313In [Nak00] Boolean formulas
represented using OBDDs are claimed to be polynomially learnable with mqs and
eqs. However, [Nak00] measures the size of an OBDD by its number of nodes,
which can be exponential in the number of propositions. We assume the learning
algorithm is _sound_ , that is, if $S_{i}^{+}$ and $S_{i}^{-}$ are the sets of
positive and negative examples observed by the algorithm up to stage $i$, then
at stage $i+1$ the algorithm will not ask a mq for a word in $S_{i}^{+}\cup
S_{i}^{-}$ or an eq for an automaton that rejects a word in $S_{i}^{+}$ or
accepts a word in $S_{i}^{-}$.

######  Proposition 20.

Let A be a sound learning algorithm for the propositional algebra over
$\mathbb{B}^{k}$. There exists a target predicate $\psi$ of size $k$, for
which A will be forced to ask at least $2^{k}-1$ queries (either mq or eq).

######  Proof 12.2.

Since A is sound, at stage $i+1$ we have $S_{i+1}^{+}\supseteq S_{i}^{+}$ and
$S_{i+1}^{-}\supseteq S_{i}^{-}$ and at least one inclusion is strict. Since
the size of the concrete alphabet is $2^{k}$, for every round $i<2^{k}$, an
adversarial teacher can answer both mqs and eqs negatively. In the case of an
eq there must be an element in $\mathbb{B}^{k}\setminus(S_{i}^{-}\cup
S_{i}^{+})$ with which the provided automaton disagrees. The adversary will
return one such element as a counterexample. This forces A to ask at least
$2^{k}\\!-\\!1$ queries. Note that for any element $v$ in $\mathbb{B}^{k}$
there exists a predicate $\varphi_{v}$ of size $k$ such that
$\llbracket{\varphi_{v}}\rrbracket=\\{v\\}$.

######  Corollary 21.

SFAs over the propositional algebra $\mathpzc{A}_{{\mathbb{B}}_{k}}$ with $k$
propositions cannot be learned in $\mathit{poly}(k)$ time using mqs and eqs.

The propositional algebra $\mathpzc{A}_{{\mathbb{B}}_{k}}$ is a special case
of the $n$-dimensional boxes algebra. Learning $n$-dimensional boxes was
studied using mq and eq [GGM94, BGGM98, BK98], as well as in the PAC setting
[BK00]. The algorithms presented in [GGM94, BGGM98, BK98, BK00] are mostly
exponential in $n$. Alternatively, [GGM94, BGGM98] suggest algorithms that are
exponential in the number of boxes in the union. In [BK98] a linear query
learning algorithm for unions of disjoint boxes is presented. Since
$n$-dimensional boxes subsume the propositional algebra, Corollary 21 implies
the following.

######  Corollary 22.

The class of SFAs over the $n$-dimensional boxes algebra cannot be learned in
$\mathit{poly}(n)$ time using mqs and eqs.

##  13\. Discussion

We examined the question of learnability of a class of SFAs over certain
algebras where the main focus of our study is on passive learning. We provided
a necessary condition for identification of SFAs in the limit using polynomial
time and data, as well as a necessary condition for efficient learning of SFAs
using membership and equivalence queries. We note that a positive result on
learning deterministic SFAs using mqs and eqs implies a positive result for
identification of deterministic SFAs in the limit using polynomial time and
data. The latter follows because a systematic set of characteristic samples
$\\{S_{L}\\}_{L\in{\mathbb{L}}}$ for a class of languages ${\mathbb{L}}$ may
be obtained by collecting the words observed by the query learner when
learning $L$, and given the SFA is deterministic, the words in the sample can
be restricted to ones of polynomial size, thus the size of the sample is
polynomial in the size of the SFA.141414For non-deterministic SFAs, as is the
case for NFAs, it might be the case that some exponentially long words are
required to learn the language [dlH97]. However, it does not imply a positive
result regarding the stronger notion of efficient identifiability, as the
latter requires the set to be also constructed efficiently, and the complexity
analysis for query learning does not include the complexity of the teacher in
computing queries, (e.g., deciding equivalence and in constructing
counterexamples). We thus provided a sufficient condition for efficient
identification of a class of SFAs, and showed that the class of SFAs over any
monotonic algebra satisfies these conditions.

We hope that these sufficient or necessary conditions will help to obtain more
positive and negative results for learning of SFAs, and spark an interest in
investigating characteristic samples in other automata models used in
verification.

## Acknowledgments

This research was partially supported by the Israel Science Foundation grant
2507/21. S. Zilles acknowledges financial support by the Natural Sciences and
Engineering Research Council (NSERC) of Canada, both through the Canada
Research Chairs program and the Discovery Grants program. She was also
supported through the Canada CIFAR AI Chairs program as an Affiliate Chair
with the Alberta Machine Intelligence Institute (Amii).

## References

  * [AD18] G. Argyros and L. D’Antoni.  The learnability of symbolic automata.  In Computer Aided Verification - 30th Int. Conf., CAV, volume 10981 of LNCS, pages 427–445. Springer, 2018.
  * [AEF15] D. Angluin, S. Eisenstat, and D. Fisman.  Learning regular languages via alternating automata.  In Proc. of the Twenty-Fourth Int. Joint Conf. on Artificial Intelligence, IJCAI, pages 3308–3314, 2015.
  * [AF16] D. Angluin and D. Fisman.  Learning regular omega languages.  Theor. Comput. Sci., 650:57–72, 2016.
  * [AFH99] R. Alur, L. Fix, and T. A. Henzinger.  Event-clock automata: A determinizable class of timed automata.  Theor. Comput. Sci., 211(1-2):253–273, 1999.
  * [Ang81] D. Angluin.  A note on the number of queries needed to identify regular languages.  Inf. Control., 51(1):76–87, 1981.
  * [Ang87] D. Angluin.  Learning regular sets from queries and counterexamples.  Inf. Comput., 75(2):87–106, 1987.
  * [Ang88] D. Angluin.  Queries and concept learning.  Machine Learning, 2(4):319–342, 1988.
  * [Ang90] D. Angluin.  Negative results for equivalence queries.  Mach. Learn., 5:121–150, 1990.
  * [ASJ+16] G. Argyros, I. Stais, S. Jana, A. D. Keromytis, and A. Kiayias.  Sfadiff: Automated evasion attacks and fingerprinting using black-box differential automata learning.  In Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security, pages 1690–1701. ACM, 2016.
  * [ASKK16] G. Argyros, I. Stais, A. Kiayias, and A. D. Keromytis.  Back in black: Towards formal, black box analysis of sanitizers and filters.  In IEEE Symposium on Security and Privacy, SP, pages 91–109, 2016.
  * [AV10] F. Aarts and F. Vaandrager.  Learning I/O automata.  In Concurrency Theory, 21th Int. Conf., CONCUR 2010, pages 71–85, 2010.
  * [BGGM98] N. H. Bshouty, P. W. Goldberg, S. A. Goldman, and H. D. Mathias.  Exact learning of discretized geometric concepts.  SIAM J. Comput., 28(2):674–699, 1998.
  * [BGJ+05] T. Berg, O. Grinchtein, B. Jonsson, M. Leucker, H. Raffelt, and B. Steffen.  On the correspondence between conformance testing and regular inference.  In Fundamental Approaches to Software Engineering, 8th Int. Conf., FASE, volume 3442, pages 175–189. Springer, 2005.
  * [BHKL09] B. Bollig, P. Habermehl, C. Kern, and M. Leucker.  Angluin-style learning of NFA.  In IJCAI, pages 1004–1009, 2009.
  * [BK98] A. Beimel and E. Kushilevitz.  Learning boxes in high dimension.  Algorithmica, 22(1/2):76–90, 1998.
  * [BK00] A. Beimel and E. Kushilevitz.  Learning unions of high-dimensional boxes over the reals.  Inf. Process. Lett., 73(5-6):213–220, 2000.
  * [BK08] C. Baier and J. P. Katoen.  Principles of model checking.  MIT Press, 2008.
  * [Bry86] R. E. Bryant.  Graph-based algorithms for boolean function manipulation.  IEEE Trans. Computers, 35(8):677–691, 1986.
  * [BV96] F. Bergadano and S. Varricchio.  Learning behaviors of automata from multiplicity and equivalence queries.  SIAM J. Comput., 25(6):1268–1280, 1996.
  * [CDYS17] K. Chubachi, Diptarama, R. Yoshinaka, and A. Shinohara.  Query learning of regular languages over large ordered alphabets.  In 1st Workshop on Learning and Automata (LearnAut), 2017.
  * [CGP01] E. M. Clarke, O. Grumberg, and D. A. Peled.  Model Checking.  MIT Press, 2001.
  * [CHYS19] K. Chubachi, D. Hendrian, R. Yoshinaka, and A. Shinohara.  Query learning algorithm for residual symbolic finite automata.  In Proc. Tenth Int. Symposium on Games, Automata, Logics, and Formal Verification, GandALF, pages 140–153, 2019.