11institutetext: Université libre de Bruxelles, Brussels, Belgium
22institutetext: University of Antwerp – Flanders Make, Antwerp, Belgium

# Active Learning of Sequential Transducers with Side Information about the
Domain

Raphaël Berthon 1122 Adrien Boiret 11 Guillermo A. Pérez 22 Jean-François
Raskin 11

###### Abstract

Active learning is a setting in which a student queries a teacher, through
membership and equivalence queries, in order to learn a language. Performance
on these algorithms is often measured in the number of queries required to
learn a target, with an emphasis on costly equivalence queries. In graybox
learning, the learning process is accelerated by foreknowledge of some
information on the target. Here, we consider graybox active learning of
subsequential string transducers, where a regular overapproximation of the
domain is known by the student. We show that there exists an algorithm using
string equation solvers that uses this knowledge to learn subsequential string
transducers with a better guarantee on the required number of equivalence
queries than classical active learning.

##  1 Introduction

Angluin’s seminal work on (active) learning regular languages from queries and
counterexamples [2] initiated a body of works around the automated “learning”
of black-box models. Active learning is a way for a non-expert user to
describe a formal object through behavioural examples and counterexamples, or
to obtain formal models for the behaviour of legacy or black-box systems which
can subsequently be formally verified [14]. In this context, additional
information about black-box systems made available to the student can make
learning more efficient in practice [7, 12].

The $L^{*}$ algorithm from [2] has been extended to learn various classes of
formal object, e.g. probabilistic automata [5] and, more relevant to this
paper, (subsequential deterministic) transducers on words [15]. In this work,
we aim to learn transducers, and focus on a specific class of side
information: an upper bound on the domain of the transduction. The advantage
of this _graybox_ model is twofold. First and more directly, it can be used to
skip some membership queries outside the transformation’s domain. Second, by
looking for transducers with the proper behaviour when limited to the upper
bound, we allow for solutions that are smaller than the canonical objects
learned by $L^{*}$. This, in turn, offers better guarantees than $L^{*}$ when
we consider the number of equivalence queries required to learn a target. This
is relevant, as in cases like non-expert description or legacy-system
learning, the equivalence test is realistically unreliable, or prohibitively
costly, when compared to the rest of the operations.

One motivation to focus on learning transducers, and more specifically Mealy
machines, with an upper bound on the domain comes from games. In multi-player
verification games, assumptions about other players have been proposed to
facilitate strategy synthesis [6, 4, for instance]. Such assumptions also make
sense when a strategy has already been obtained (via synthesis [3] or some
alternative means) and one wishes to “minimize” it or its encoding. A simple
way to do so is to restrict the domain of the strategy to the reachable set of
game configurations (under the assumptions made about the adversaries).
Finally, when the game formalism considered allows for delays or multiple
choices made unilaterally by some player — as is the case in regular infinite
games [8] — strategies are not implementable by Mealy machines but rather
require general transducers.

### Related work.

The classical algorithm for active learning is $L^{*}$ [2]. It saturates a
table of observations with membership queries, then building a minimal
deterministic automaton compatible with those observations to send as
candidate for an equivalence query. A polynomial number of membership queries
and at most $n$ equivalence queries are always sufficient to learn the
automaton.

For transducers, the OSTIA algorithm [15] generalizes $L^{*}$, follows a
similar structure, and offers comparable guarantees. Like in $L^{*}$, the
number of queries is polynomial in the size of the minimal normal form of the
target transducer.

In the case of graybox learning, the methods differ and this alters the
complexity guarantees. For instance, when learning languages from so-called
“inexperienced teachers” [9], one considers a case where the teacher sometimes
answers a membership query with “I don’t know”. Under those circumstance, it
is impossible to learn a unique minimal automaton. This leads to a trade-off
in complexity. On the one hand, finding the minimal automaton compatible with
an incomplete table of observations necessitates calls to oracles (a SAT
encoding is used in [9]). On the other hand, obscuring a regular language by
replacing some information with “I don’t know” will always make the size of
the minimal solution smaller or equal to the canonical minimal deterministic
automaton. When the area where the inexperienced teacher cannot answer with
certainty is assumed to be regular, an $L^{*}$-like algorithm is provided in
[9].

Another work on the topic [1] concerns Mealy machines, i.e. transducers that
write one letter exactly for each letter they read. It is shown that one can
learn a composition of two Mealy machines if the first one is already known.
Just like in [9], the $L^{*}$-type algorithm uses oracles to find minimal
machines compatible with an incomplete table of observations (as we can only
know the behaviour of the second machine on the range of the first) and offers
a guarantee in the number of equivalence queries bound to the number of states
of the minimal second machine, rather than that of the composition in whole.

### Contributions.

We show how to use string equations that can be encoded into SAT to find a
minimal transducer compatible with incomplete observations, and to use this in
an $L^{*}$-like algorithm. Our algorithm is guaranteed to issue a number of
equivalence query that is bounded by the minimal compatible transducer, rather
than the canonical one. This difference can be a huge benefit when our upper
bound is the result of known complex logical properties or elaborate formats
respected by the input, and the transformation we wish to learn is simple.

We note the differences with [9, 1] in objects learned, learning frameworks,
and available queries. We focus on transducers, a class that subsumes automata
and Mealy machine. As an added benefit, transducers are as compact as
automata, and as or more compact than Mealy machines they are equivalent to.
This compactness preserves or improves the equivalence queries guarantees. In
our learning framework, the upper bound is supposed to be known by the
student. This is in contrast to the inexperienced teacher case, where the
scope of possible observations is unknown, and has to be assumed regular and
learned on the fly. When it comes to available queries, [9] assumes the
student has access to containment queries i.e. student can ask teacher if the
candidates’ language contains or is contained in the target, this to obtain
better the guarantees. In our model, a simple equivalence query is considered.
Conversely, in [1], the only way to do a membership query is to do so on the
composition of both machines. In that regard, learning a composition is more
constraining than learning with a known upper bound. However, since finding a
reverse image to an output word through a transducer is possible with good
complexity, our algorithm can be adapted to learn a composition of two
transducers, in the framework of [1].

##  2 Preliminaries

A (subsequential string) transducer $\mathcal{M}$ is a tuple
$(\Sigma,\Gamma,Q,q_{0},w_{0},\delta,\delta_{F})$ where $\Sigma$ is the finite
input alphabet, $\Gamma$ is the finite output alphabet, $Q$ is the finite set
of states, $q_{0}\in Q$ is the initial state, $w_{0}\in\Gamma^{*}$ is an
initial production, $\delta$ is the transition function, a partial function
$Q\times\Sigma\to Q\times\Gamma^{*}$ and $\delta_{F}$ is the final function, a
partial function $Q\to\Gamma^{*}$. If $\delta(q,a)=(q^{\prime},w)$ we note
$q\xrightarrow{a|w}q^{\prime}$. If $\delta_{F}(q)=w$ we say that $q$ is final,
and note $q\xrightarrow{w}\top$. We define the relation $\rightarrow^{*}$ by
combining the input and output of several transitions: $\rightarrow^{*}$ is
the smallest relation such that
$q\mathrel{\vphantom{\xrightarrow{\varepsilon|\varepsilon}}\smash{\xrightarrow{\varepsilon|\varepsilon}}\vphantom{\to}^{*}}q$,
and if
$q\mathrel{\vphantom{\xrightarrow{u|w}}\smash{\xrightarrow{u|w}}\vphantom{\to}^{*}}q^{\prime}$
and $q^{\prime}\xrightarrow{a|w^{\prime}}q^{\prime\prime}$ then
$q\mathrel{\vphantom{\xrightarrow{ua|w\cdot
w^{\prime}}}\smash{\xrightarrow{ua|w\cdot
w^{\prime}}}\vphantom{\to}^{*}}q^{\prime\prime}$. We write
$q_{0}\mathrel{\vphantom{\xrightarrow{u|w}}\smash{\xrightarrow{u|w}}\vphantom{\to}^{*}}q$
when $u$ reaches the state $q$ with partial output $w$.

For every state $q\in Q$, we associate a partial function
$\llbracket\mathcal{M}^{q}\rrbracket(u)$ to $\mathcal{M}$ from input words
over $\Sigma$ to output words over $\Gamma$. Formally,
$\llbracket\mathcal{M}^{q}\rrbracket(u)=w\cdot w^{\prime}$ if
$q\mathrel{\vphantom{\xrightarrow{u|w}}\smash{\xrightarrow{u|w}}\vphantom{\to}^{*}}q_{F}$
and $q_{F}\xrightarrow{w^{\prime}}\top$ for some $q_{F}\in Q$ and is undefined
otherwise. Finally, we define $\llbracket\mathcal{M}\rrbracket\coloneqq
w_{0}\cdot\llbracket\mathcal{M}^{q_{0}}\rrbracket$ and write that
$\mathcal{M}$ implements $\llbracket\mathcal{M}\rrbracket$.

We write $\text{dom}(\llbracket\mathcal{M}\rrbracket)$ to denote the domain of
$\llbracket\mathcal{M}\rrbracket$, that is the set of all $u\in\Sigma^{*}$
that reach a final state $q_{F}\in Q$. We often consider the restriction of
$\llbracket\mathcal{M}\rrbracket$ to a given domain $D\subseteq\Sigma^{*}$,
and denote it $\llbracket\mathcal{M}\rrbracket_{|D}$.

$q_{0}$$q_{a}$$q_{b}$$a|\varepsilon$$b|1$$c,a|\varepsilon$$c|1$$\varepsilon$$\varepsilon$

| $\varepsilon$ | $c$
---|---|---
$\varepsilon\in[\varepsilon]$ | $\bot$ | $\bot$
$a\in[a]$ | $\varepsilon$ | $\\#$
$b\in[b]$ | $\bot$ | $1$
$ac\in[a]$ | $\\#$ | $\\#$
$bc\in[a]$ | $1$ | $\\#$

$q_{0}$$q_{a}$$q_{b}$$a|\varepsilon$$b|1$$c|\varepsilon$$c|\varepsilon$$\varepsilon$$\varepsilon$

Figure 1: On the left, a transducer compatible with the merging map in the
center, on the right the transducer resulting from this merging map.

###### Example 1

Consider the function $\tau_{abc}$ with domain $\mathit{Up}_{abc}=(a+bc)c^{*}$
and $\tau_{abc}(ac^{n})=\tau_{abc}(bc^{n})=1^{n}$. It is implemented by the
left transducer in Figure 1.

We note that if we want to restrict a transducer’s function to a regular
language $L$ for which we have a deterministic word automaton $\mathcal{A}$, a
classic construction is to build the product transducer
$\mathcal{M}\times\mathcal{A}$, where the states are the Cartesian products of
both state spaces, and the final function $\delta_{F}$ is only defined for
pairs $(q,p)$ where $q$ is in the domain of the final function of
$\mathcal{M}$ and $p$ is final in $\mathcal{A}$. This transducer implements
the function $\llbracket\mathcal{M}\rrbracket_{\mathcal{A}}$.

#### Assumptions.

We write $|\mathcal{M}|$ to denote the _size_ of $\mathcal{M}$, i.e. its
number of states. For convenience, we only consider _trim_ transducers, that
is to say that every state $q$ is reachable from $q_{0}$ and co-reachable from
a final state.

#### Active learning.

Let $\Sigma$ and $\Gamma$ be finite input and output alphabets respectively.
Further, let $\tau\colon\Sigma^{*}\to\Gamma^{*}$ be a partial function
implementable by a transducer. In this work we will be interested in _actively
learning_ a transducer implementing $\tau$ by interacting with a _teacher_ who
knows $\tau$ and can answer questions our algorithm asks about $\tau$.
Formally, the teacher is an oracle that can answer _membership_ and
_equivalence_ queries.

Given $u\in\Sigma^{*}$, a membership query answers $\tau(u)$ if
$u\in\text{dom}(\tau)$, and $\bot$ otherwise Given $\mathcal{M}$ a transducer,
an equivalence query answer _true_ if $\llbracket\mathcal{M}\rrbracket=\tau$,
otherwise it provides $u\in\Sigma^{*}$, a non-equivalence witness such that
$u\in\text{dom}(\llbracket\mathcal{M}\rrbracket)\backslash\text{dom}(\tau)$,
or
$u\in\text{dom}(\tau)\backslash\text{dom}(\llbracket\mathcal{M}\rrbracket)$,
or $u\in\text{dom}(\llbracket\mathcal{M}\rrbracket)\cap\text{dom}(\tau)$ but
$\llbracket\mathcal{M}\rrbracket(u)\neq\tau(u)$. The goal of a learning
algorithm in this context is to produce a transducer $\mathcal{M}$ such that
$\llbracket\mathcal{M}\rrbracket=\tau$.

#### Side information about the domain.

We generalize the active learning problem by introducing side information
available to the learning algorithm. Concretely, we assume that an _upper
bound_ on the domain of $\tau$ is known in advance. That is, we are given a
DFA $\mathcal{A}_{\mathit{Up}}$ whose language $\mathit{Up}$ is such that
$\text{dom}(\tau)\subseteq\mathit{Up}$. The goal of a learning algorithm to
produce a transducer $\mathcal{M}$ such that
$\llbracket\mathcal{M}\rrbracket_{|\mathit{Up}}=\tau$.

The domain upper bound $\mathit{Up}$ may allow us to learn much simpler
transducers $\mathcal{M}$ than the canonical minimal transducer describing
$\tau$ — i.e. the class of transducers learnt by OSTIA. For instance, if
$\tau$ is the identity transformation over a complex regular language $L$,
then the canonical transducer $\mathcal{M}_{\tau}$ will have as many states as
the minimal DFA $\mathcal{A}$ for $L$, and thus will be as difficult to learn
and require several equivalence tests, potentially many. However, if
$\mathit{Up}=L$ is already known, then the smallest transducer $\mathcal{M}$
such that $\llbracket\mathcal{M}\rrbracket_{|\mathit{Up}}=\tau$ is a simple
one-state transducer, and will be identified in a single equivalence query.

##  3 Learning transducers with side information

Our algorithm uses an “observation table” $T$ based on a finite prefix-closed
subset $P$ of $\Sigma^{*}$ and a finite suffix-closed subset $S$ of
$\Sigma^{*}$. Formally, we define $T$ as a function $(P\cup P\cdot\Sigma)\cdot
S\to\Gamma^{*}\cup\\{\\#,\bot\\}$ and maintain the following invariant for all
$u\in(P\cup P\cdot\Sigma)$ and all $v\in S$. If $u\cdot v\not\in\mathit{Up}$
then $T(u\cdot v)=\\#$. If $u\cdot v\in\mathit{Up}\setminus\text{dom}(\tau)$
then $T(u\cdot v)=\bot$, otherwise $T(u\cdot v)=\tau(u\cdot v)$. For technical
reasons, we often consider the set $P_{T}$ of prefixes of the elements of
$(P\cup P\Sigma)\cdot S$.

######  Definition 1 (Compatible transducer)

Let $T$ be an observation table and $\mathcal{M}$ a transducer of input
alphabet $\Sigma$ and output alphabet $\Gamma$. We say that $\mathcal{M}$ is
compatible with $T$ if for all $u,v\in P\cup P\Sigma$, if $T(u\cdot
v)\in\Gamma^{*}$ then $\llbracket\mathcal{M}\rrbracket(u\cdot v)=T(u,v)$ and
if $T(u\cdot v)=\bot$ then $u\cdot
v\not\in\text{dom}(\llbracket\mathcal{M}\rrbracket)$.

To “fill” the table so as to satisfy the invariant, we pose membership queries
to the teacher. Once $T$ has certain satisfactory properties (as defined in
the OSTIA algorithm and elaborated upon briefly), we are able to construct a
transducer $\mathcal{M}$ from it. As a table $T$ can be filled with $\\#$,
multiple minimal transducers may be _compatible with $T$_. To minimize the
number of equivalence queries posed, we will send an equivalence query only if
there is a unique minimal transducer $\mathcal{M}$ (up to equivalence in
$\mathit{Up}$) compatible with $T$.

Instead of searching directly for transducers, we work only with the
information on how those transducers behave on $P_{T}$. We represent this
information using objects we call _merging maps_. We show that we can
characterize when there exist two competing minimal transducers with two
different merging maps, or two competing minimal transducers with the same
merging map. If neither is the case, then there is a unique minimal compatible
transducer $\mathcal{M}$, and we build it by guessing its merging map. We then
pose an equivalence query to the teacher in order to determine whether
$\mathcal{A}_{\mathit{Up}}\times\mathcal{M}$ implements the target function
$\tau$.

#### Satisfactory properties.

The following properties are those that allow the OSTIA algorithm [15] to
work. Under these properties, we are sure that a transducer can be derived
from the table $T$. They are defined on a specific table $T:(P\cup
P\Sigma)\cdot S\rightarrow\Gamma^{*}\cup\\{\bot\\}$. Given $u\in P\cup
P\Sigma$, we call $\text{lcp}_{T}(u)$ the longest common prefix of all the
$T(u\cdot v)$ in $\Gamma^{*}$. For $u,u^{\prime}\in P\cup P\Sigma^{*}$, we say
that $u\equiv_{T}u^{\prime}$ iff for all $v\in S$, we have both $T(u\cdot
v)=\bot\iff T(u^{\prime}\cdot v)=\bot$ and if $T(u\cdot v)\in\Gamma^{*}$ then
$\text{lcp}_{T}(u)^{-1}T(u\cdot
v)=\text{lcp}_{T}(u^{\prime})^{-1}T(u^{\prime}\cdot v)$. A table $T$ is closed
if for all $ua\in P\Sigma$ there exists $u^{\prime}\in P$ such that
$ua\equiv_{T}u^{\prime}$; $\equiv$-consistent, if for all $u,u^{\prime}\in P$,
$a\in\Sigma$ such that $ua,u^{\prime}a\in P_{T}$, then
$u\equiv_{T}u^{\prime}\implies ua\equiv_{T}u^{\prime}a$; lcp-consistent, if
for all $ua\in P\cup P\Sigma$, we have that $\text{lcp}_{T}(u)$ is a prefix of
$\text{lcp}_{T}(ua)$.

The role of these notions in Algorithm 2 is twofold. First, it guarantees that
the algorithm could, at worst, find the same transducer as the OSTIA algorithm
[15] as a candidate for an equivalence query from a closed,
$\equiv$-consistent, lcp-consistent table. Second, it can be seen as an
efficient way to acquire information for a learner. We can see closed,
$\equiv$-consistent, lcp-consistent tables as those that are saturated with
membership queries, which means that no further information can be obtained by
a learner without resorting to more costly operations, e.g. MinGen($T$),
CompetingMinGen($T$), or an equivalence query.

#### Merging maps.

For any given table $T$ there are infinitely many compatible transducers. This
was already the case in automata or Mealy Machines [9, 1]. However, where
transducers differ, is that even when limiting ourselves to transducers with a
minimal number of states, this might still be the case. Indeed, on some
transitions, the output can be arbitrary (see Example 2). As a consequence,
the method we will use to obtain a compatible transducer from a finite search
space combines the methods of [9] with the addition of partial output
information and an additional constraint on the output of transitions.

We want to obtain concomitantly an equivalence $\equiv$ on $P_{T}$ that
describes the set of states of the transducer and a _partial output_ function
$f:P_{T}\rightarrow\Gamma^{*}$ that describe which output is produced while
reading an input. In the context of transducers, side information adds another
restriction: A transducer can contain transitions that do not link together
elements of $P_{T}$ for which we have actual output information in $T$. This
is a problem, as the output of such transitions is arbitrary and leads to an
infinite number of candidates.

We will represent the behaviour of a transducer on $P_{T}$ but keep only the
output information that can be corroborated in $T$. We call
$P_{\Gamma}\subseteq P_{T}$ the set of all $u\in P_{T}$ such that there exists
$v\in\Sigma^{*}$ for which $T(u\cdot v)\in\Gamma^{*}$. We call
$P_{\varnothing}\subseteq P_{T}$ the set of all $u\in P_{T}$ such that there
is no $v\in\Sigma^{*}$ for which $T(u\cdot v)\in\Gamma^{*}$.

######  Definition 2 (Merging map)

Let $T$ be an observation table. A _merging map_ (MM) on $T$ is a pair
$(\equiv,f)$ where $\equiv$ is an equivalence relation on $P_{T}$, and $f$ is
a partial function from $P_{T}$ to $\Gamma^{*}$, such that for all
$u,u^{\prime}\in P_{T}$ and $a\in\Sigma$:

  1. 1.

If $f(u)$ does not exist then $u\equiv u^{\prime}\ f(u^{\prime})$ does not
exist.

  2. 2.

If there exists $v\in\Sigma^{*}$ and $T(u\cdot v)\in\Gamma^{*}$ then $f(u)$ is
a prefix of $T(u\cdot v)$.

  3. 3.

If $f(ua)$ exists, then $f(u)$ exists and is a prefix of $f(ua)$.

  4. 4.

If we have that $f(u)$ exists, $u\equiv u^{\prime}$ and $ua,u^{\prime}a\in
P_{T}$ then $ua\equiv u^{\prime}a$ and if $f(ua)$ exists then
$f(u)^{-1}f(ua)=f(u^{\prime})^{-1}f(u^{\prime}a)$.

  5. 5.

If $T(u)\in\Gamma^{*}$, $u\equiv u^{\prime}$ then $T(u^{\prime})\neq\bot$ and
if $T(u^{\prime})\in\Gamma^{*}$ then
$f(u)^{-1}T(u)=f(u^{\prime})^{-1}T(u^{\prime})$.

  6. 6.

If $f(ua)$ exists, there is no $v\in P_{T}$ such that $v\equiv u$, and $va\in
P_{\Gamma}$, then $f(ua)=f(u)$.

The idea behind this definition is that a MM $(\equiv,f)$ contains the
information necessary to model the behaviour on $P_{T}$ of a transducer
compatible with $T$, while rule $6$ ensures we only keep output information
from $P_{\Gamma}$. If such a couple $(u,a)$ exists, we say that it is _muted_.
Notably, every transducer $\mathcal{M}$ compatible with $T$ has an underlying
MM $(\equiv,f)$, and conversely, every MM $(\equiv,f)$ can be used to build a
transducer $\mathcal{M}$ compatible with $T$. The size of a MM is the number
of equivalence classes of $\equiv$ in $\text{dom}(f)$.

######  Definition 3 (Resulting Transducer)

Let $T$ be an observation table and $(\equiv,f)$ a MM on $T$. In the
transducer $\mathcal{M}$ _resulting from_ $(\equiv,f)$ the set of states is
the set of equivalence classes of $\equiv$ in $\text{dom}(f)$ (For
convenience, for $u\in P_{T}$ we call $q_{u}$ the state associated to it), the
initial state is $q_{\varepsilon}$, the initial production is
$f(\varepsilon)$, the transitions are
$q_{u}\xrightarrow{a|f(u)^{-1}f(ua)}q_{ua}$ for $u,ua\in\text{dom}(f)$, and
for each $u$ such that $T(u)\in\Gamma^{*}$, we have
$\delta_{F}(q_{u})=f(u)^{-1}T(u)$

######  Definition 4 (Induced MM)

Let $T$ be an observation table and $\mathcal{M}$ a transducer compatible with
$T$. The MM $(\equiv,f)$ _induced by the transducer_ $\mathcal{M}$ is such
that we have  (A) $u\equiv v$iff $u$ and $v$ reach the same state of
$\mathcal{M}$;  (B) for all $u\in P_{T}$, $a\in\Sigma$ such that $ua\in P_{T}$
reaches a state $q$ of $\mathcal{M}$:  (B.I) if there exists $v\in P_{T}$ such
that $v\equiv u$, and $va\in P_{\Gamma}$, then $f(ua)=f(u)\cdot\delta(q,a)$
(B.II) and if $(u,a)$ is muted, then $f(ua)=f(u)$.

As an important note, these transformations are not one-to-one and do not
establish a bijection between transducers and MMs. Notably, some transducers
compatible with $T$ cannot be obtained with this method. For instance, let us
consider a table full of $\\#$. Since no $T(u)$ is ever in $\Gamma^{*}$, there
is no final state in any transducer created with this method.

Rather than a problem, this is the goal of projecting the transducers’
behaviour on $P_{T}$, as we naturally eliminate candidates that are needlessly
elaborate outside of the observations of $T$. The MM induced by $\mathcal{M}$
only contains information on its behaviour on $P_{T}$, and the transducer
resulting from a MM is the transducer with the smallest amount of states and
transitions whose behaviour on $P_{T}$ matches what is described in the MM.

#### Learning algorithm.

Our learning algorithm works as follows:  (1) We build up $T$ until it is
closed and $\equiv$ and lcp-consistent.  (2) If two minimal compatible
transducers exist, we find them and a word $u$ to tell them apart. We use a
membership query on $u$ and start again.  (3) If only one minimal compatible
transducer $\mathcal{M}$ remains, we find it. We use an equivalence query on
$\mathcal{A}_{\mathit{Up}}\times\mathcal{M}$.

Algorithm 1

1:Let $P=S=\\{\varepsilon\\}$

2:while True do

3: if $(u,a,v,v^{\prime})$ is a witness of non-lcp-consistency then add
$av,av^{\prime}$ to $S$

4: else if $(u,u^{\prime},a,v)$ is a witness of non-$\equiv$-consistency then
add $av$ to $S$

5: else if $ua$ is a witness of non-closure then add $ua$ to $P$

6: else if $u$ := CompetingMinGen($T$) $\neq\varnothing$ then add $u$ and its
suffixes to $S$

7: else $\mathcal{M}$ := MinGen($T$)

8: if $u$ is a non-equiv. witness for
$\mathcal{A}_{\mathit{Up}}\times\mathcal{M}$ then add all its suffixes to $S$

9: else return $\mathcal{M}$

Algorithm 2 MinTransducerUp($L$,$\mathcal{A}_{\mathit{Up}}$)

Such an algorithm allows using the knowledge of $\mathit{Up}$ to propose more
compact candidates, as the minimal transducer compatible with a table $T$ is
always smaller than the canonical transducer that can be derived from $T$ if
we substitute $\bot$ for the $\\#$. This smaller model size leads to a better
guarantee when it comes to the number of required equivalence queries. The
full algorithm is in Algorithm 2. It uses the subprocedures CompetingMingGen
and MinGen which we elaborate upon later.

###### Theorem 3.1

Algorithm 2 terminates and makes a number of equivalence queries bounded by
the number of states of a minimal $\mathcal{M}$ such that
$\llbracket\mathcal{M}\rrbracket_{|\mathit{Up}}=\tau$.

######  Proof (Sketch)

We first assume termination and focus on the bound on equivalence queries.
Note that, by construction of the tables, any minimal $\mathcal{M}$ such that
$\llbracket\mathcal{M}\rrbracket_{|\mathit{Up}}=\tau$ is compatible with all
of them. Thus, it suffices to argue that every equivalence query our algorithm
poses increases the size of a minimal transducer compatible with it. For
termination, it remains to bound the number of membership queries and calls to
the subprocedures. Unlike for automata, it is impossible to enumerate all
transducers with $n$ states compatible with an observation table. Termination
will follow from the fact that we do not consider the all such transducers.
Rather, we enumerate a finite subset of them (see Prop. 4).∎

##  4 Merging maps to guess a minimal transducer

Algorithm 2 relies on the two subprocedures CompetingMinGen(T) and MinGen(T)
to find one or several competing transducers compatible with an observation
table. This type of procedures is absent from blackbox learning algorithms,
but central to graybox learning algorithm [9]. In the automata case, an oracle
that guesses a minimal compatible automaton needs only to guess an equivalence
relation on $P_{T}$ For transducers, we guess a function $f$ that associates
to each element of $P_{T}$ an output in $\Gamma^{*}$. Since this is not a
finite search space, we aim to restrict ourselves to a finite subspace that
still allows us to find one unique or two non-equivalent minimal candidates,
when they exist. We will limit the scope of this search with Definition 5 and
6 of _muted_ and _open_ transitions, to fix arbitrary outputs at
$\varepsilon$.

To combine the two subprocedures CompetingMinGen($T$) and MinGen($T$), we
characterize a necessary and sufficient condition under which there exist two
possible minimal candidates, tested by CompetingMinGen($T$). When we ensure
that the minimal candidate is unique up to equivalence on $\mathit{Up}$, we
use MinGen($T$) to generate it, then send an equivalence query.

#### MinGen(T) using MMs.

Recall that there are transducers compatible with a table $T$ that do not
result from a MM on $T$. We will show that to implement MinGen($T$) and
CompetingMinGen($T$), it is enough to focus on minimal MMs and to take the
resulting transducers as candidates. To justify that this method provides the
right result, we prove that it provides valid candidates.

###### Lemma 1

Let $(f,\equiv)$ be a minimal MM on a table $T$ and $\mathcal{M}$ its
resulting transducer. Then, $\mathcal{M}$ is compatible with $T$.

Among the minimal transducers compatible with $T$, there is one resulting from
a MM. Indeed, from a transducer $\mathcal{M}$ compatible with $T$ one can
create a smaller one using the MM induced by $\mathcal{M}$ and Definition 3.

###### Proposition 1

Let $T$ be a table, $\mathcal{M}$ a transducer compatible with $T$. There is a
transducer $\mathcal{M}^{\prime}$, with as many states, compatible with $T$
resulting from a MM.

#### CompetingMinGen(T) using MMs.

While guessing a MM is enough to guess a minimal transducer, it does not
provide a reliable way to decide whether two non-equivalent minimal compatible
transducers exist. For the subroutine CompetingMinGen($T$), we must find a way
to detect whether this is the case. A natural first step is to say that if we
can find minimal MMs whose resulting transducers are non-equivalent on
$\mathit{Up}$, then we have found a solution to CompetingMinGen($T$).
Unfortunately, this condition is not necessary. Indeed, there are minimal MM
induced by several non-equivalent transducers. This arises when a transition
going out of the state associated to some $u\in P_{T}$ can have an arbitrarily
defined output, because $ua\in P_{\varnothing}$, or $ua\not\in P_{T}$.

###### Example 2

In Figure 1, we note the special case of two transitions in the left
transducer: the transition $q_{a}\xrightarrow{c|1}q_{a}$ linking $a\in
P_{\Gamma}$ to $ac\in P_{\varepsilon}$, and the transition
$q_{b}\xrightarrow{a|\varepsilon}q_{a}$ linking $b\in P_{\Gamma}$ to $ba\notin
P_{T}$. In both cases, the transition is never used by any $u\in P_{T}$ such
that $T(u)\in\Gamma^{*}$. In other words, those transitions could be deleted,
or their output arbitrarily changed for any $w\in\Gamma^{*}$, without breaking
compatibility. The right transducer is also compatible with $T$, but the
output of $q_{a}\xrightarrow{c|1}q_{a}$ has been changed to $\varepsilon$ and
the transition $q_{b}\xrightarrow{a|\varepsilon}q_{a}$ has been deleted.

The first case, $ua\in P_{\varnothing}$, is the one we aimed to eliminate by
erasing the output in muted pairs $(u,a)$. We call muted transitions those
whose output has to be $\varepsilon$ in a transducer induced from a MM.

###### Definition 5

Let $T$ be a table, $(\equiv,f)$ a MM, and $\mathcal{M}$ its resulting
transducer. For all $u\in P_{T}$, $a\in\Sigma$, $(u,a)$ is a _muted pair_ of
$(\equiv,f)$, and $q_{u}\xrightarrow{a|\varepsilon}q_{ua}$ is a _muted
transition_ of $\mathcal{M}$, if $u,ua\in\text{dom}(f)$ but there is no $v\in
P_{T}$ such that $u\equiv v$ and $va\in P_{\Gamma}$.

The second case, $ua\not\in P_{T}$, is new. We formalize this notion as open
ends on a MM. An open end is a place where a transition could be added without
influencing the behaviour of the resulting transducer on $P_{T}$. We decide to
fix the output of such transitions to $\varepsilon$.

###### Definition 6

Let $T$ be a table and $(\equiv,f)$ a MM. For all $u\in P_{T}$, $a\in\Sigma$,
$(u,a)$ is an _open end_ of the map if there exists no $v\in P_{T}$ such that
$v\equiv u$ and $va\in P_{T}$.

Let $\mathcal{M}$ be the resulting transducer of $(\equiv,f)$. We say that
$\mathcal{M}^{\prime}$ is an _open completion_ of $(\equiv,f)$ (or of
$\mathcal{M}$) if it is the transducer $\mathcal{M}$ with at most one
additional transition $u\xrightarrow{a|\varepsilon}u^{\prime}$ per open end
$(u,a)$. We call such transitions _open transitions_.

Muted and open transitions allow arbitrary output, meaning there can exist
several non-equivalent compatible transducers: if there exists a word
$u\in\mathit{Up}$ that goes through a muted transition, that is sufficient to
build several compatible transducers that give different outputs on $u$. This
condition together with the existence of competing minimal MMs give a
necessary, sufficient and effective, condition for CompetingMinGen($T$).

###### Lemma 2

Let $T$ be an observation table, $(\equiv,f)$ a MM on $T$ and $\mathcal{M}$
its resulting transducer. If there exists an open completion
$\mathcal{M}^{\prime}$ and an element $u\in\mathit{Up}$ such that
$u\in\text{dom}(\llbracket\mathcal{M}^{\prime}\rrbracket)$ and $u$ uses a
muted or open transition in its run in $\mathcal{M}^{\prime}$, then there
exist competing minimal transducers compatible with $T$.

#### Implementation:

We prove that the following is a possible implementation of
CompetingMinGen($T$):  (1) search for two minimal MMs with non-equivalent
corresponding transducers,  (2) if these do not exist, search for a minimal MM
and an open completion as in Lemma 2;  (3) otherwise, we have a unique minimal
transducer up to equivalence on $\mathit{Up}$.

###### Proposition 2

Let $T$ be a table. If there exist two minimal transducers $\mathcal{M}_{1}$
and $\mathcal{M}_{2}$ compatible with $T$ but not equivalent on $\mathit{Up}$,
one of the following exists:  (i) two minimal MMs with non-equivalent
resulting transducers $\mathcal{M}^{\prime}_{1},\mathcal{M}^{\prime}_{2}$, or
(ii) an open completion $\mathcal{M}^{\prime}$ of a minimal MM compatible with
$T$ and a word
$u\in\text{dom}(\llbracket\mathcal{M}^{\prime}\rrbracket)\cap\mathit{Up}$
using at least one open or muted transition of $\mathcal{M}^{\prime}$.

##  5 Encoding into string equations

To align our result with other graybox algorithms [9, 1], we wish to encode
the minimal generation subroutines into an problem like SAT. While a direct
encoding is possible, it is easier to go through a first encoding into string
equations. We only use operations that are easily encoded into SAT: word
equality and inequality, concatenation, first order operators, and a
restricted use of quantifiers. Universal quantifiers are limited to sets of
polynomial size, and as such are a shortcut for a conjunction, and existential
quantifiers are limited to words of polynomial size, that can be encoded using
a polynomial number of variables.

This setting has the advantage of being more directly relevant to the notions
we consider, while keeping the theoretical bound. Furthermore, SMT solvers
have specialized tools [16, 10] to solve such equations, that may yield better
practical results than direct SAT encoding.

We encode an observation table $T$, merging maps $(\equiv,f)$, and runs of
$u\in\mathit{Up}$ with output $w\in\Gamma^{*}$ in the resulting transducer of
$T$. We use word variables $T_{u}$ for $T(u)$, booleans $E_{u,v}$ for $u\equiv
v$, word variables $f_{u}$ for $f(u)$, word variable $u$ and letter variables
$a_{i}\in[1,k]$ with $u=a_{1}\cdot\dots\cdot a_{k}$ for an input word of
length $k$, and word variables $w=w_{0}\cdot w_{1}\cdot\dots\cdot w_{k}\cdot
w_{k+1}$ for their output step by step. The bounds on the size of $u$ is given
by small model theorems in automata and transducers.

We use string equation formulae to encode the properties we combine in the
minimal generation subroutines. We classically build $\varphi_{eq}$ that
ensures $E_{u,v}$ denotes an equivalence. Then, each point of Definition 2 can
be seen as a simple combination of string equations on $T_{u}$ and $f_{u}$
using the binary variables $E_{u,v}$ for $u,v\in P_{T}$. We can thus build
$\varphi_{mm}$ that ensures $E_{u,v}$ and $f_{u}$ denote a MM.

For the transducer resulting from $(\equiv,f)$, and its open completions, we
add booleans $m_{u,a}$, $o_{u,a}$ that indicate leaving $q_{u}$ with $a$ is a
muted or open transition.

To model runs, we use $\varphi_{run}(u,w)$ ensuring $u$ has a run with output
$w$ in the transducer resulting from $E_{u,v}$ and $f_{u}$. We build it by
making sure the run starts in the initial state with production $w_{0}$, ends
in a final state with production $w_{k+1}$, and at the $i^{\text{th}}$ step,
the input letter is $a_{i}$ and the output word is $w_{i}$.

To encode MinGen($T$) we only need to find $E_{u,v},f_{u}$ that respect
$\varphi_{mm}$ with $n$ states, where $n$ starts at $1$ and increases until a
solution is found.

For CompetingMinGen($T$) we use Proposition 2 to split the encoding in two. To
encode the case where there exist two non-equivalent MMs, we use variables
$E_{u,v}$ and $f_{u}$ respecting $\varphi_{mm}$ for a first MM, copies
$E^{\prime}_{u,v}$ and $f^{\prime}_{u}$ respecting $\varphi_{mm}$ for a second
MM, and $\varphi_{\mathit{Up}}$ and $\varphi_{run}$ to encode the existence of
$u\in\mathit{Up}$ whose run differs in the transducers resulting from both
MMs.

It is easy to encode the case where there exist an open completion and a word
$u\in\mathit{Up}$ that uses an open or muted transition, by using $m_{u,a}$
and $o_{u,a}$ on the run of $u$ in the transducer resulting from the MM of
$E_{u,v}$ and $f_{u}$.

Combined together, they encode the minimal generating subroutines in string
equations, that could then be encoded in SAT, leading to our result:

###### Proposition 3

Let $T$ be an observation table. The subroutines MinGen($T$) and
CompetingMinGen($T$) can be effectively implemented.

#### Note on complexity:

As this string-constraints encoding is a polynomial shortcut for a SAT
encoding, each oracle call solves an problem. Coarsely, MinGen($T$) and
CompetingMinGen($T$) are of complexity $\P^{\NP}$. To find a minimal MM of
size $n$, we need $n-1$ of those oracles to fail on sizes $1\leq i<n$.

If we take Algorithm 2 in its entirety, then it is not each call to
MinGen($T$) and CompetingMinGen($T$) that needs $n$ of those oracles to fail
to find a minimum of size $n$, as we can keep the memory of the current
minimal size for future calls.

##  6 Conclusion

Adapting graybox learning to transducers revealed more complex than expected.
Our solution relies on merging maps, muted and open transitions while offering
better bounds on equivalence queries than OSTIA. Two main questions remain
open:  (1) The bound on the number of equivalence queries was the aim of this
paper, but the number of membership queries or call to string equations
solvers are not considered. Providing tight bounds or proposing a potential
tradeoff, like the one described in [1], would increase the viability of the
implementation of such an algorithm.  (2) We could consider other classes of
side information like general upper bound that cut sections of
$\Sigma^{*}\times\Gamma^{*}$.

## References

  * [1] A. Abel and J. Reineke.  Gray-box learning of serial compositions of mealy machines.  In NASA Formal Methods Symposium, pages 272–287. Springer, 2016\.
  * [2] D. Angluin.  Learning regular sets from queries and counterexamples.  Inf. Comput., 75(2):87–106, 1987.
  * [3] R. Bloem, K. Chatterjee, and B. Jobstmann.  Graph games and reactive synthesis.  In Handbook of Model Checking, pages 921–962. Springer, 2018.
  * [4] R. Brenguier, J. Raskin, and O. Sankur.  Assume-admissible synthesis.  Acta Informatica, 54(1):41–83, 2017.
  * [5] C. De La Higuera and J. Oncina.  Learning stochastic finite automata.  In International Colloquium on Grammatical Inference, pages 175–186. Springer, 2004.
  * [6] D. Fisman, O. Kupferman, and Y. Lustig.  Rational synthesis.  In TACAS 2010, volume 6015 of LNCS, pages 190–204. Springer, 2010.
  * [7] B. Garhewal, F. W. Vaandrager, F. Howar, T. Schrijvers, T. Lenaerts, and R. Smits.  Grey-box learning of register automata.  In Integrated Formal Methods, volume 12546 of LNCS, pages 22–40. Springer, 2020.
  * [8] M. Holtmann, L. Kaiser, and W. Thomas.  Degrees of lookahead in regular infinite games.  Log. Methods Comput. Sci., 8(3), 2012.
  * [9] M. Leucker and D. Neider.  Learning minimal deterministic automata from inexperienced teachers.  In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, pages 524–538. Springer, 2012.
  * [10] T. Liang, A. Reynolds, N. Tsiskaridze, C. Tinelli, C. Barrett, and M. Deters.  An efficient smt solver for string constraints.  FMSD, 48(3):206–234, 2016.
  * [11] A. W. Lin and R. Majumdar.  Quadratic word equations with length constraints, counter systems, and presburger arithmetic with divisibility.  In ATVA, pages 352–369. Springer, 2018.
  * [12] D. Neider, R. Smetsers, F. W. Vaandrager, and H. Kuppens.  Benchmarks for automata learning and conformance testing.  In Models, Mindsets, Meta: The What, the How, and the Why Not?, volume 11200 of LNCS, pages 390–416. Springer, 2018.
  * [13] M.-P. Schutzenberger.  Sur les relations rationnelles.  In Automata Theory and Formal Languages, pages 209–213. Springer, 1975.
  * [14] F. W. Vaandrager.  Model learning.  Commun. ACM, 60(2):86–95, 2017.
  * [15] J. M. Vilar.  Query learning of subsequential transducers.  In International Colloquium on Grammatical Inference, pages 72–83. Springer, 1996.
  * [16] Y. Zheng, X. Zhang, and V. Ganesh.  Z3-str: A z3-based string solver for web application analysis.  In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pages 114–124, 2013.

Appendix

##  Appendix 0.A Proof of Theorem 3.1

###### Proof

We first assume termination and focus on the bound on equivalence queries.
Note that, by construction of the tables, any minimal $\mathcal{M}$ such that
$\llbracket\mathcal{M}\rrbracket_{|\mathit{Up}}=\tau$ is compatible with all
of them. Thus, it suffices to argue that every equivalence query our algorithm
poses increases the size of a minimal transducer compatible with it. Let $T$
be the table and $\mathcal{M}$ be the input transducer in an equivalence
query, and $T^{\prime}$ the table and $\mathcal{M}^{\prime}$ the transducer in
the next one. We prove that $\mathcal{M}^{\prime}$ has at least one more state
than $\mathcal{M}$.

We know two things about $\mathcal{M}^{\prime}$. First, it is compatible with
$T$ as every observation of $T$ is still present in $T^{\prime}$ and
$\mathcal{M}^{\prime}$ is compatible with $T^{\prime}$. Second, it is not
equivalent to $\mathcal{M}$ on $\mathit{Up}$ since $\mathcal{M}$ was sent as
candidate for an equivalence query that failed. This means the teacher
provided a counterexample $u\in\mathit{Up}$ that $\mathcal{M}$ disagreed with.
This new $u$ is added to the table to obtain $T^{\prime}$. Hence,
$\mathcal{M}$ is not compatible with $T^{\prime}$, while
$\mathcal{M}^{\prime}$ is and they differ at least on $u\in\mathit{Up}$.

We now prove that $\mathcal{M}^{\prime}$ has strictly more states than
$\mathcal{M}$. Since $\mathcal{M}$ was sent as candidate for an equivalence
query, that means CompetingMinGen($T$) found that all minimal transducers
compatible with $T$ were equivalent on $\mathit{Up}$, and MinGen($T$) found
that $\mathcal{M}$ was a minimal transducer compatible with $T$. We know that
$\mathcal{M}^{\prime}$ is compatible with $T$ but not equivalent with
$\mathcal{M}$. Hence, it is not a minimal transducer compatible with $T$,
which means it has strictly more states.

For termination, it remains to bound the number of membership queries and
calls to the subprocedures. Note that, unlike in automata, it is impossible to
enumerate all transducers with $n$ states or less compatible with an
observation table. Termination will actually follow from the fact that we do
note consider the set of all such transducers. Rather, we enumerate a useful
finite subset of them, as we end up showing in Proposition 4.∎

##  Appendix 0.B Proof of Lemma 1

###### Proof

First, it can be proven by simple induction that for $u\notin\text{dom}(f)$,
$u$ has no run in $\mathcal{M}$, and for $u\in\text{dom}(f)$,
$q_{\varepsilon}\xrightarrow{u|f(u)}q_{u}$ in $\mathcal{M}$. Then, we finish
with the final output in $\mathcal{M}$. If $T(u)\in\Gamma^{*}$ then $q_{u}$ is
final in $\mathcal{M}$ with a final output of $f(u)^{-1}T(u)$. This means that
$\llbracket\mathcal{M}\rrbracket(u)=f(u)\cdot f(u)^{-1}T(u)=T(u)$. Conversely,
if $T(u)=\bot$, then either $u\notin\text{dom}(f)$ and $u$ has no run in
$\mathcal{M}$, or $u\in\text{dom}(f)$, and by point $5$ of Definition 2 we
obtain that for all $u^{\prime}\in P_{T}$ such that $u^{\prime}\equiv u$ we
have $T(u^{\prime})=\bot$.This means that $q_{u}$ is not final and thus
$\llbracket\mathcal{M}\rrbracket(u)$ is undefined.∎

##  Appendix 0.C Proof of Proposition 1

###### Proof

We consider the equivalence $\equiv_{\mathcal{M}}$ and function
$f_{\mathcal{M}}$ induced by Definition 4 on $\mathcal{M}$.

We show that ($\equiv_{\mathcal{M}}$,$f_{\mathcal{M}}$) is a merging map:

  1. 1.

for $u,u^{\prime}\in P_{T}$, if $f_{\mathcal{M}}(u)$ does not exist then $u$
is not in $\text{dom}(\llbracket\mathcal{M}\rrbracket)$. Thus,
$u\equiv_{\mathcal{M}}u^{\prime}\iff
u^{\prime}\not\in\text{dom}(\llbracket\mathcal{M}\rrbracket)\iff
f(u^{\prime})$ does not exist

  2. 2.

if there exists $v$ such that $T(u\cdot v)\in\Gamma^{*}$, then as
$\mathcal{M}$ is compatible with $T$ we have that
$\llbracket\mathcal{M}\rrbracket(u\cdot v)=T(u\cdot v)$. Thus $u$ has a
partial output in $\mathcal{M}$, this is $f_{\mathcal{M}}(u)$, and it is a
prefix of $T(u\cdot v)$.

  3. 3.

for all $u\in P_{T}$ and $a\in\Sigma$, if $f_{\mathcal{M}}(ua)$ exists, then
it is either $f_{\mathcal{M}}(u)$ or $f_{\mathcal{M}}(u)\cdot\delta(q,a)$. In
both cases $f_{\mathcal{M}}(u)$ is a prefix of $f_{\mathcal{M}}(ua)$.

  4. 4.

for all $u\in P_{T}$ if $f_{\mathcal{M}}(u)$ exists then for all
$u^{\prime}\in P_{T}$ and $a\in\Sigma$ such that
$u\equiv_{\mathcal{M}}u^{\prime}$ and $ua,u^{\prime}a\in P_{T}$, in
$\mathcal{M}$ the transition linking the state of $u$ to the state of $ua$ is
the same as the one linking the state of $u^{\prime}$ to the state of
$u^{\prime}a$. The output on that transition is the difference between the
partial output of $u$ and $ua$, and the same difference between the partial
output of $u$ and $ua$. In other word, it is $f_{\mathcal{M}}(u)^{-1}f(ua)$
and the identical
$f_{\mathcal{M}}(u^{\prime})^{-1}f_{\mathcal{M}}(u^{\prime}a)$.

  5. 5.

for all $u\in P_{T}$, if $T(u)\in\Gamma^{*}$, then
$u\in\text{dom}(\llbracket\mathcal{M}\rrbracket)$. Hence if
$u\equiv_{\mathcal{M}}u^{\prime}$, then
$u^{\prime}\in\text{dom}(\llbracket\mathcal{M}\rrbracket)$. Since
$\mathcal{M}$ is compatible with $T$, that means $T(u^{\prime})\neq\bot$.
Furthermore, if $T(u^{\prime})\in\Gamma^{*}$, then
$f_{\mathcal{M}}(u^{\prime})^{-1}T(u^{\prime})$ is whatever output is left to
produce $\llbracket\mathcal{M}\rrbracket(u^{\prime})$ from the partial output
of $u^{\prime}$. This is the image of the state of $u^{\prime}$ by
$\delta_{F}$. Since this is also the case for $u$ we get that
$f_{\mathcal{M}}(u)^{-1}T(u)=f_{\mathcal{M}}(u^{\prime})^{-1}T(u^{\prime})$

  6. 6.

for all $u\in P_{T}$ and $a\in\Sigma$, if $(u,a)$ is muted, then
$f_{\mathcal{M}}(ua)=f(u)$.

By Lemma 1, the transducer $\mathcal{M}^{\prime}$ obtained by using the
merging map ($\equiv_{\mathcal{M}}$,$f_{\mathcal{M}}$) in Definition 3 is
compatible with $T$. The number of equivalence classes in
$\equiv_{\mathcal{M}}$ (and thus the number of states of the resulting
transducer) is equal to or smaller than the number of states of
$\mathcal{M}$.∎

##  Appendix 0.D Muted Transitions and Open Ends

We will presently prove Lemma 2. Before that, though, we first establish some
intermediate results.

###### Lemma 3

Let $T$ be a table, $(\equiv,f)$ a merging map, $\mathcal{M}$ its resulting
transducer, and $(u,a)$ a muted transition. Deleting
$u\xrightarrow{a|\varepsilon}u$ or for any $u^{\prime}\in
P_{T},w\in\Gamma^{*}$ replacing it by $u\xrightarrow{a|w}u^{\prime}$ in
$\mathcal{M}$ creates a transducer $\mathcal{M}^{\prime}$ compatible with $T$.

######  Proof (of Lemma 3)

If a muted transition $(u,a)$ exists, it is never used in the run of any
element $v\in P_{T}$ such that $T(v)\in\Gamma^{*}$. If it was, that would mean
that for some $v_{pref}\in P_{T},v_{suf}\in\Sigma^{*}$ we have
$v=v_{pref}\cdot a\cdot v_{suf}$ where $a$ is the letter that uses the muted
transition. We would then have $v_{pref}\equiv u$,but also that $v_{pref}\in
P_{T}\backslash P_{\varnothing}$ as $T(v)\in\Gamma^{*}$, which contradicts the
fact that $(u,a)$ is a muted transition.

Since the muted transition is not used by any element $v\in P_{T}$ such that
$T(v)\in\Gamma^{*}$, it can be deleted or its output arbitrarily modified
without impacting the compatibility of the transducer.∎

###### Lemma 4

Let $T$ be a table, $(\equiv,f)$ a merging map, $\mathcal{M}$ its resulting
transducer, and $(u,a)$ an open end for $T$. For all
$u^{\prime}\in\text{dom}(f),w\in\Gamma^{*}$, adding
$u\xrightarrow{a|w}u^{\prime}$ to $\mathcal{M}$ creates a transducer
$\mathcal{M}^{\prime}$ compatible with $T$.

######  Proof (of Lemma 4)

It is possible to add this transition as no transition outgoing $u$ reading
$a$ exists in $\mathcal{M}$. If it did, it would have been created by a couple
$v,va\in P_{T}$ where $v\equiv u$. Since $(u,a)$ is an open end, no such
$v,va$ exist.

This transition does not break compatibility with $T$, as no element of
$P_{T}$ will go through this transition during a run. If such an element
$va\in P_{T}$ used this transition as its last step, this would provide $v\in
P_{T}$ such that $v$ reaches the state of $u$, which means $v\equiv u$. Since
$(u,a)$ is an open end, no such $v,va$ exist.∎

We are now ready to give the announced proof.

######  Proof (of Lemma 2)

$\mathcal{M}^{\prime}$ has the same number of states as $\mathcal{M}$, as we
just add transitions. Lemma 4 guarantees that $\mathcal{M}^{\prime}$ is
compatible with $T$. Conversely, Lemma 3 guarantees that removing the muted
transitions of $\mathcal{M}$ would give another transducer
$\mathcal{M}^{\prime\prime}$ compatible with $T$.

Since $u$ uses an open transition in its run in $\mathcal{M}^{\prime}$, it
would fail a run in $\mathcal{M}^{\prime\prime}$, where this transition would
not exist. From this we deduce
$u\not\in\text{dom}(\llbracket\mathcal{M}^{\prime\prime}\rrbracket)$. Since
$u\in\text{dom}(\llbracket\mathcal{M}^{\prime}\rrbracket)$, and
$u\in\mathit{Up}$ we have
$\llbracket\mathcal{M}^{\prime}\rrbracket_{|\mathit{Up}}\neq\llbracket\mathcal{M}^{\prime\prime}\rrbracket_{|\mathit{Up}}$.
Hence, $\mathcal{M}^{\prime}$ and $\mathcal{M}^{\prime\prime}$ are competing
minimal transducers compatible with $T$.∎

##  Appendix 0.E Proof of Proposition 2

###### Proof

We take $\mathcal{M}_{1},\mathcal{M}_{2}$ and consider their induced merging
map. This merging map cannot have less states as
$\mathcal{M}_{1},\mathcal{M}_{2}$ are minimal. We call
$\mathcal{M}^{\prime}_{1},\mathcal{M}^{\prime}_{2}$ its resulting transducers.
We note that they have the same states than $\mathcal{M}_{1},\mathcal{M}_{2}$
but some of the transitions’ outputs might have been deleted.

If $\mathcal{M}^{\prime}_{1}$ and $\mathcal{M}^{\prime}_{2}$ are not
equivalent on $\mathit{Up}$, then the first statement is true, as both
$\mathcal{M}^{\prime}_{1},\mathcal{M}^{\prime}_{2}$ are minimal and come from
merging maps.

If $\mathcal{M}^{\prime}_{1}$ and $\mathcal{M}^{\prime}_{2}$ are equivalent on
$\mathit{Up}$, then either $\mathcal{M}_{1}$ and $\mathcal{M}^{\prime}_{1}$
are not equivalent on $\mathit{Up}$, or $\mathcal{M}_{2}$ and
$\mathcal{M}^{\prime}_{2}$ are not equivalent on $\mathit{Up}$. We call
$\mathcal{M},\mathcal{M}^{\prime}$ this non-equivalent pair. Since
$\mathcal{M}^{\prime}$ was built as the resulting transducer of the induced
map of $\mathcal{M}$,we have that $\mathcal{M}^{\prime}$ is identical to
$\mathcal{M}$ for all transitions except the transitions coming from open ends
(that are not built by Definition 3), and the outputs of muted transitions.
Lemmas 4 and 3 ensure that we can thus put the output of all those transitions
at $\varepsilon$ to change $\mathcal{M}$ into $\mathcal{M}^{\prime\prime}$, a
minimal transducer compatible with $T$ and an open completion of the
transducer $\mathcal{M}^{\prime}$.

Since $\mathcal{M}$ and $\mathcal{M}^{\prime}$ are not equivalent on
$\mathit{Up}$, we consider $u\in\mathit{Up}$ a counterexample.
$\mathcal{M}^{\prime}$ is identical to $\mathcal{M}$ except for deleted
outputs on muted transitions in $\mathcal{M}^{\prime}$, and additional
transitions coming from open ends in $\mathcal{M}$. Hence either
$u\in\text{dom}(\llbracket\mathcal{M}\rrbracket)$ but
$u\in\text{dom}(\llbracket\mathcal{M}^{\prime}\rrbracket)$, in which case $u$
uses a transition from an open end in its run in $\mathcal{M}$, or
$\llbracket\mathcal{M}\rrbracket(u)\neq\llbracket\mathcal{M}^{\prime}\rrbracket(u)$,
in which case $u$ uses a muted transition in its run in
$\mathcal{M}^{\prime}$.

$\mathcal{M}^{\prime\prime}$ is identical to $\mathcal{M}$ except for the
output of the muted and open transitions. Hence, when we run the
counterexample $u$ in $\mathcal{M}^{\prime\prime}$, we know it will use a
muted or open transition, and thus that the second statement is true.∎

##  Appendix 0.F Finiteness proof for Theorem 3.1

Theorem 3.1 necessitates two thing to prove that Algorithm 2 terminates.
First, the number of equivalence queries must be bounded. This is the core of
the use of CompetingMinGen($T$) in Algorithm 2 and what provides the improved
guarantee of graybox learning.

Second, we need to ensure that the number of calls to CompetingMinGen($T$)
between two equivalence queries is bounded. To that effect, we show that for
each number of states $n$, the number of transducers that Algorithm 2
considers and eliminates is bounded.

###### Proposition 4

Algorithm 2 considers finitely many transducers of size $n$.

###### Proof

Each membership test asked by CompetingMinGen($T$) eliminates a possible
transducer compatible with $T$ in its current state. What we will show is that
for each number of states $n$, the number of transducers to eliminate is
finite. This works by considering a transducer as a series of finite choices.

_States:_ Since the equivalence relations of MMs are right congruences, there
exists a prefix-closed set of $n$ elements, each belonging in a different
state. Since the number of finite prefix-closed sets of $\Sigma^{*}$ is
finite, this choice is bounded.

_Transitions without output:_ The transitions (output excluded) are partial
functions from $Q\times\Sigma$ to $Q$, where $Q$ is the set of $n$ states.
Since the number of such functions is finite, this choice is bounded.

_Open and muted transitions:_ Each transition can be open, muted, or neither,
depending on the state of $T$. That leaves less than $3^{D}$ possibilities,
where $D$ is the number of transitions. This choice is bounded. This is not a
tight analysis: adding observations can make a transition no longer open, or
no longer muted, but never the other way around, so we will never explore all
$3^{D}$ possibilities.

_Transition outputs and final outputs:_ Open and muted transitions have a
fixed output of $\varepsilon$. Other transitions have an output bounded by
rule $3$ of Definition 2. As we add observations, this bound gets more and
more restrictive, never less. The final outputs’ existence and value are
dictated by rule $5$ of Definition 2. Hence the choice of transition outputs
and final outputs is bounded.

In conclusion, for every number of states $n$, we have a final number of
transducers to eliminate, and each membership query by CompetingMinGen($T$)
eliminates one. Since $n$ goes from $1$ to the size of the smallest transducer
compatible with the target of our learning algorithm, Algorithm 2 terminates.

##  Appendix 0.G Small model theorems to bound witness sizes in
CompetingMinGen($T$)

The finiteness of counterexamples $u\in\Sigma^{*}$ such that $u\in\mathit{Up}$
and two competing candidates have a different image for $u$, or $u$ uses a
muted or open transition, is guaranteed by small model theorems on
transducers.

###### Lemma 5

Let $\mathcal{M}_{1},\mathcal{M}_{2}$ be two transducers. If
$\llbracket\mathcal{M}_{1}\rrbracket_{|\mathit{Up}}\neq\llbracket\mathcal{M}_{2}\rrbracket_{|\mathit{Up}}$,
then there is $u\in\mathit{Up}$ s.t. $|u|\leq
2\cdot(|\mathcal{M}_{1}|\cdot|\mathcal{M}_{2}|\cdot|\mathcal{A}_{\mathit{Up}}|)^{2}$
and $\llbracket\mathcal{M}_{1}\rrbracket$,
$\llbracket\mathcal{M}_{2}\rrbracket$ differ on $u$.

###### Proof

The case where
$u\in\text{dom}(\llbracket\mathcal{M}_{1}\rrbracket)\backslash\text{dom}(\llbracket\mathcal{M}_{2}\rrbracket$
(or vice-versa) is a simple case of difference between the languages
$\text{dom}(\llbracket\mathcal{M}_{1}\rrbracket)\cap\mathit{Up}$ described by
$\mathcal{A}_{\mathit{Up}}\times\mathcal{M}_{1}$ and
$\text{dom}(\llbracket\mathcal{M}_{2}\rrbracket)\cap\mathit{Up}$ described by
$\mathcal{A}_{\mathit{Up}}\times\mathcal{M}_{2}$. Such a difference is of size
less than the size of the product of those two automata, which is
$2\cdot(|\mathcal{M}_{1}|\cdot|\mathcal{M}_{2}|\cdot|\mathcal{A}_{\mathit{Up}}|^{2})$
(although the square on $|\mathcal{A}_{\mathit{Up}}|$ can easily be removed).

The case where
$\llbracket\mathcal{M}_{1}\rrbracket(u)\neq\llbracket\mathcal{M}_{2}\rrbracket(u)$
is a classical result, provided in [13]. Lemma 1 ensures that if the
transducer
$\mathcal{A}_{\mathit{Up}}\times(\mathcal{M}_{1}\cup\mathcal{M}_{2})$ has a
word with more than one output, there exists a $u\in\Sigma^{*}$ of size less
than
$1+2\cdot(|\mathcal{M}_{1}|\cdot|\mathcal{M}_{2}|\cdot|\mathcal{A}_{\mathit{Up}}|)\cdot(|\mathcal{M}_{1}|\cdot|\mathcal{M}_{2}|\cdot|\mathcal{A}_{\mathit{Up}}|-1)$
such that $u$ has more than one output.

###### Lemma 6

Let $\mathcal{M}$ be a transducer. If there exists
$v\in\text{dom}(\llbracket\mathcal{M}\rrbracket_{|\mathit{Up}})$ that uses a
specific transition of $\mathcal{M}$, then there exists
$u\in\text{dom}(\llbracket\mathcal{M}\rrbracket_{|\mathit{Up}})$ of size less
or equal than $2\cdot|\mathcal{A}_{\mathit{Up}}|\cdot|\mathcal{M}|$ that uses
this same transition.

###### Proof

This is a small model theorem on the transducer
$\mathcal{A}_{|\mathit{Up}}\times\mathcal{M}$. We consider the path that leads
$v$ to and from the targeted transition $q\xrightarrow{a|w}q^{\prime}$ in
$\mathcal{M}$, and cut $v$ into $v_{0}\cdot a\cdot v_{1}$, where $v_{0}$ is
the part of $v$ from the initial state to $q$, and $v_{1}$ is the part of $v$
from $q^{\prime}$ to a final state. We can remove from $v_{0}$ and $v_{1}$ any
loop of $\mathcal{M}\cdot\mathcal{A}_{|\mathit{Up}}$, to obtain $u_{0}$ and
$u_{1}$ such that $|u_{0}|$ and $|u_{1}|$ are both strictly smaller than
$|\mathcal{A}_{|\mathit{Up}}|\times|\mathcal{M}|$, $u_{0}$ still goes from the
initial state of $\mathcal{M}$ to $q$, $u_{1}$ still goes from $q^{\prime}$ to
a final state of $\mathcal{M}$, and $u=u_{0}\cdot a\cdot u_{1}$ is still
accepted by $\mathcal{A}_{|\mathit{Up}}$. Hence $u\in\mathit{Up}$ and $u$ uses
the targeted transition $q\xrightarrow{a|w}q^{\prime}$ in $\mathcal{M}$.

##  Appendix 0.H Effective computation of CompetingMinGen($T$)

We present a way to encode the problem of finding merging maps. More
specifically, to build the oracle CompetingMinGen($T$), we need to see if,
given a state number $n$, there exists one merging map with two minimal
resulting transducers (and its witness), or two non-equivalent merging maps
(and their witness).

We encode this problem as word equations, that is conjunctions and
disjunctions of both equality and inequalities between words in a given domain
[11], with additional operators: concatenation and membership in a finite set.
SMT solvers have specialized tools [16, 10] to solve such equations. As we
consider a bounded domain of definition once we have fixed the size of
transducers we are considering, we could alternatively write these equations
as a SAT query, as all the operators except the universal quantification can
be polynomially encoded into SAT. Since we consider universal formulae over
either $P_{T}$ or $\Sigma$, such formulae could also be encoded in SAT by
replacing universal quantifiers by a conjunction on polynomially many
variables in $P_{T}$ or $\Sigma$. This allows us to keep the theoretical NP
bound of a SAT encoding, with a more readable string equations encoding, more
adapted to the problems we consider.

For convenience, we say in what follows that a word variable $s$ can be
undefined (denoted $s=\bot$). In practice, we add a boolean variable $s^{def}$
associated to every word variable, that is true if and only if the associated
variable is defined.

We now present equations for the various objects introduced in Section 3:

#### Table:

A table $T:(P\cup P\Sigma)\cdot S\to\Gamma^{*}\cup\\{\bot,\\#\\}$ is
represented as the set that contains for all $u\in P_{T}$ a boolean
$T^{\\#}_{u}$ that is true if and only if $T(u)=\\#$, and a word $T_{u}$ on
$\Gamma^{*}$ that we assign to $T(u)$ if $T(u)$ is defined and $\bot$
otherwise. We call $\varphi_{T}$ the conjunction of assignations that describe
the table $T$.

#### Merging map:

A merging map $(\equiv,f)$ is represented as a boolean $E_{u,v}$ for all
$u,v\in P_{T}$ representing if $u\equiv v$, and a word $f_{u}$ on $\Gamma^{*}$
for all $u\in P_{T}$ that represents the output of $f(u)$. Every $f_{u}$ is of
size smaller than $|u|\cdot\text{max}\\{|T(v)|\\}$.

The following equations ensure that $\equiv$ is an equivalence relation: For
all $u,v,w\in P_{T}$, $E_{u,u}=\mathtt{true}$, $E_{u,v}=E_{v,u}$, and
$E_{u,v}\wedge E_{v,w}\Rightarrow E_{u,w}$. We call $\varphi_{eq}$ the
conjunction of those constraints.

We encode each point of Definition 2 in word equations. For all $u,v\in
P_{T}$:

  1. 1.

$f_{u}=\bot\Rightarrow(f_{v}=\bot\Longleftrightarrow E_{u,v})$

  2. 2.

$(\exists u^{\prime}\in P_{T}.\ T_{u\cdot u^{\prime}}\neq\bot\wedge\neg
T^{\\#}_{u\cdot u^{\prime}})\Rightarrow(f_{u}\neq\bot\wedge\exists
x\in\Gamma^{*}.\ f_{u}\cdot x=f_{u\cdot u^{\prime}})$

  3. 3.

For all $a\in\Sigma$: $f_{ua}\neq\bot\Rightarrow(f_{u}\neq\bot\wedge\exists
x\in\Gamma^{*}.\ f_{u}\cdot x=f_{ua})$

  4. 4.

For all $a\in\Sigma$ such that $ua,va\in P_{T}$: $(f_{u}\neq\bot\wedge
E_{u,v})\Rightarrow(E_{ua,va}\wedge f_{ua}\neq\bot\Rightarrow(\exists
x\in\Gamma^{*}.\ f_{u}\cdot x=T_{u}\wedge f_{v}\cdot x=T_{v}))$

  5. 5.

$(T_{u}\neq\bot\wedge\neg T^{\\#}_{u}\wedge E_{u,v})\Rightarrow(\neg
T^{\\#}_{u}\Rightarrow(\exists x\in\Gamma^{*}.\ f_{u}\cdot x=T_{u}\wedge
f_{v}\cdot x=T_{v}))$

  6. 6.

$(\forall v\in P_{T},\ va\notin P_{\Gamma}\vee\neg E_{u,v})\Rightarrow
f_{ua}=\bot\lor f_{ua}=f_{u}$

We call $\varphi_{\text{mm}}$ the conjunction of those constraints and
$\varphi_{eq}$.

###### Lemma 7

Let $T$ be an observation table. If the variables $T(u)$, $E_{u,v}$, and
$f_{u}$ respect $\varphi_{T}\wedge\varphi_{mm}$, then $(E_{u,v},f_{u})$
represents a merging map of $T$.

#### Transducer run:

To encode the case of CompetingMinGen($T$) where there exists two minimal
merging map with non-equivalent corresponding transducers, we first show how
to encode that a word $u\in\Sigma^{\ell}$ is accepted by the resulting
transducer of a merging map with output $w$. We define letters
$a_{1},\ldots,a_{\ell}\in\Sigma$ such that $u=a_{1}\cdot\ldots\cdot a_{\ell}$,
input words $v_{0},v_{1},\ldots,v_{\ell}\in P_{T}$ that are representative of
the equivalence classes of the states visited, output words
$w_{1},\ldots,w_{\ell},w_{out}\in\Gamma^{*}$ such that
$w=w_{1}\cdot\ldots\cdot w_{n}\cdot w_{out}$, and a word $\delta_{u,a}$ on
$\Gamma^{*}$ that represents the output of transition $(u,a,ua)$.

The following equations ensure that $u$ is accepted by the transducer
corresponding to the merging map, with output $w$: $\forall u\in
P_{T},a\in\Sigma:f_{u}\cdot\delta_{u,a}=f_{ua}$ $v_{0}=\varepsilon$, $\forall
i\in[1,n],E_{v_{i},(v_{i-1}\cdot a_{i})}$, $\forall
i\in[1,n],w_{i}=\delta_{v_{i-1},a_{i}}$, and $f_{v_{n}}\cdot
w_{out}=T_{v_{n}}$. We call $\varphi_{run}(u,w)$ the conjunction of those
constraints.

Conversely, we can create a formula that ensures that a word $u$ fails in the
transducer resulting from the MM described by $E_{u,v}$ and $f_{u}$. We still
use $a_{1},\ldots,a_{\ell}\in\Sigma$ such that $u=a_{1}\cdot\ldots\cdot
a_{\ell}$, and input words $v_{0},v_{1},\ldots,v_{\ell}\in P_{T}$ that are
representative of the equivalence classes of the states visited, except we now
allow $v_{i}$ to be undefined ($v_{i}=\bot$). We do not care about the output.

The following equations ensure that $u$ fails in the transducer corresponding
to the merging map, by failing to be able to read a letter or ending in a non-
final state: $v_{0}=\varepsilon$, $\forall i\in[1,n],E_{v_{i},(v_{i-1}\cdot
a_{i})}\lor v_{i}=\bot$, and $v_{n}=\bot\lor\forall v\in
P_{T},E_{v,v_{n}}\implies T(v)=\bot$. We call $\varphi_{\lnot{run}}(u)$ the
conjunction of those constraints.

###### Lemma 8

Let $T$ be an observation table. If $(E_{u,v},f_{u})$ represents a merging map
of $T$, and $u\in\Sigma^{*}$, $w\in\Gamma^{*}$ respect $\varphi_{run}(u,w)$,
then $u$ is accepted by the resulting transducer of this merging map with
output $w$.

We can, using classical methods, encode that a word accepted by a regular
language $\mathit{Up}$ is accepted by two different merging maps with
different output. We call this formula $\varphi_{\mathit{Up}}(u)$. Thus:

###### Lemma 9

Let $T$ be an observation table. It can be encoded with word equations there
exists two merging maps of $T$ of size $n$ and corresponding transducers non-
equivalent on $\mathit{Up}$. If this is the case, a witness $u$ can be
returned.

###### Proof

Using several sets of word equations, what we want is:

  1. 1.

a merging map represented by the variables $E,f$ of size $n$

  2. 2.

an input-output pair $u,w$ of its resulting transducer, where $|u|\leq\ell$

  3. 3.

a merging map represented by the variables $E^{\prime},f^{\prime}$ of size $n$

  4. 4.

     * •

that $u$ fails its run in the resulting transducer of $E^{\prime},f^{\prime}$,
or

     * •

an input-output pair $u^{\prime},w^{\prime}$ of its resulting transducer,
$|u^{\prime}|\leq\ell$ and that $u=u^{\prime}\in\mathit{Up}$ but $w\neq
w^{\prime}$,

The four first points have been proven in Lemma 7 and 8. To create two merging
maps we use variables $E_{u,v}$ and $f_{u}$ for the first one, and
$E^{\prime}_{u,v}$ and $f^{\prime}_{u}$ for the second. We call
$\varphi^{\prime}_{mm}$, $\varphi^{\prime}_{run}(u,w)$ and
$\varphi^{\prime}_{\lnot run}(u,w)$ the versions of $\varphi_{mm}$,
$\varphi_{run}(u,w)$ and $\varphi_{\lnot run}(u,w)$ that use the variables
$E^{\prime}_{u,v}$ and $f^{\prime}_{u}$ instead of $E_{u,v}$ and $f_{u}$. If
we want to find two different outputs for $u$, the resulting formula is:

$\Phi_{wit1}=\varphi_{T}\wedge\wedge\varphi_{mm}\wedge\varphi_{run}(u,v)\wedge\varphi^{\prime}_{mm}\wedge\varphi^{\prime}_{run}(u^{\prime},v^{\prime})\wedge
u=u^{\prime}\wedge\varphi_{\mathit{Up}}(u)\wedge w\neq w$

If we want to find $u$ that has a run in the first transducer but not the
second, the resulting formula is:

$\Phi_{wit1}=\varphi_{T}\wedge\wedge\varphi_{mm}\wedge\varphi_{run}(u,v)\wedge\varphi^{\prime}_{mm}\wedge\varphi^{\prime}_{\lnot
run}(u)\wedge*\varphi_{\mathit{Up}}(u)$

The length $\ell$ to limit the size of $u$ comes from Lemma 5.

#### Merged and open transitions:

It now remains to encode the case where a single merging map uses muted or
open transitions. As shown in Proposition 2, the output of the witness does
not matter as much as finding a word $u\in\mathit{Up}$ that uses one of those
transitions. We define letters $a_{1},\ldots,a_{n}\in\Sigma^{n}$ such that
$u=a_{1}\cdot\ldots\cdot a_{n}$, words $v_{0},\ldots,v_{n}\in P_{T}$ that are
representatives of the equivalence classes of the states visited, booleans
$m_{u,a}$ with $u\in P_{T}$ and $a\in\Sigma$ representing whether $u$ reading
$a$ is a muted transition, as specified in point 6 of Definition 2, and
booleans $o_{u,a}$ with $u\in P_{T}$ and $a\in\Sigma$ representing whether $u$
reading $a$ is an open transition, as specified by their definition.

$m_{u,a}$ and $o_{u,a}$ are encoded as follows: $m_{u,a}\iff(\forall v\in
P_{T},\ va\notin P_{\Gamma}\lor u\not\equiv v)\land(\exists v\in P_{T},\
u\equiv v\land f(va)\neq\bot)$, and $o_{u,a}\iff(\forall v\in P_{T},\ va\notin
P_{T}\lor u\not\equiv v)$

As before, we know how to encode in equations that a word $u$ is accepted by
$\mathit{Up}$. Adding the following equations ensures that this $u$ goes
through an open or muted transition in an open completion of the transducer
resulting from the merging map. As seen in the proof of Proposition 2, this is
sufficient to prove that there exists several (and in fact infinitely many)
transducers compatible with this merging map that would write different
outputs when reading $u$: $v_{0}=\varepsilon$, $\forall
i\in[1,\ell],f_{v_{i}}\neq\bot$, $\forall i\in[1,\ell],\
E_{v_{i},(v_{i-1}\cdot a_{i})}\lor o_{v_{i-1},a_{i}}$, $\forall
i,j\in[1,\ell],\ E_{v_{i},v_{j}}\Rightarrow E_{v_{i+1},v_{j+1}}$,
$T(v_{\ell})\neq\bot$, and $\exists i\in[1,\ell],\ o_{v_{i-1},a_{i}}\lor
m_{v_{i-1},a_{i}}$. We call $\varphi_{mo}(u)$ the conjunction of those
constraints and the definitions of $m_{u,a}$ and $o_{u,a}$.

###### Lemma 10

Let $T$ be an observation table, if $(E_{u,v},f_{u})$ represents a merging map
of $T$, and $u\in\Sigma^{*}$ respects $\varphi_{mo}(u)$, then $u$ uses a muted
or open transition in an open completion of the transducer resulting from the
merging map.

###### Proof

The conditions above describe a path in the transducer resulting from the
merging map, with three additional conditions:

  * •

$\forall i\in[1,\ell],\ E_{v_{i},(v_{i-1}\cdot a_{i})}\lor o_{v_{i-1},a_{i}}$
allows for a path to continue from an open end ($o_{v_{i-1},a_{i}}$) when no
transition is available.

  * •

$\forall i,j\in[1,\ell],\ E_{v_{i},v_{j}}\Rightarrow E_{v_{i+1},v_{j+1}}$
ensures that reading a certain $a$ in a certain state will always lead to the
same successor. This is necessary as transitions coming from an open
completion are not constrained by the equations defining the merging map.

  * •

$\exists i\in[1,\ell],\ o_{v_{i-1},a_{i}}\lor m_{v_{i-1},a_{i}}$ ensures that
$u$ uses at least one muted or open transition

###### Lemma 11

Let $T$ be an observation table. It can be encoded with word equations there
exists a merging map of $T$ of size $n$ and a word $u\in\mathit{Up}$ such that
$u$ uses a muted or open transition in an open completion of the transducer
resulting from this merging map.

###### Proof

Using several sets of word equations, what we want is a merging map
represented by the variables $E,f$ of size $n$ and an input word
$u\in\mathit{Up}$ such that $|u|\leq\ell$, and $u$ uses a muted or open
transition in an open completion of the transducer resulting from the merging
map.

Encoding $u\in\mathit{Up}$ is possible through classical results. Lemma 10
ensures us that it is possible to encode those points, with the resulting
formula being
$\Phi_{wit2}=\varphi_{T}\wedge\varphi_{mm}\wedge\varphi_{mo}(u)\wedge\varphi_{\mathit{Up}}(u)$.
The length $\ell$ to limit the size of $u$ comes from Lemma 5.

We can thus conclude with the following proposition:

###### Proposition 5

Let $T$ be an observation table. The subroutines MinGen($T$) and
CompetingMinGen($T$) can be effectively implemented.

###### Proof

Lemma 7, 9 and 11 ensure that we can decide the existence of a merging map,
two competing merging maps, or a word using a muted or open transition, if
given a number $n$ of states. Notably, those last two points combine thanks to
ooposition 2 to guarantee that if two competing transducers of size $n$ exist,
then we can find them that way.

To find the proper number of state $n$, we try to guess a transducer with $i$
states, $i$ starting at $1$ and incremented each time we cannot find a
transducer.