Given a preMealy machine ${\mathcal{M}}=(M,m_{{\sf init}},\Delta)$, we define
the (possibly partial) function
$f_{\mathbbm{i}\mathbbm{o}}:M\times{\mathcal{I}}^{*}\rightarrow({\mathcal{I}}{\mathcal{O}})^{*}$
by $f_{\mathbbm{i}\mathbbm{o}}(m,{\sf i}_{1}\dots\sf i_{k})={\sf i}_{1}{\sf
o}_{1}\dots\sf i_{k}{\sf o}_{k}$ such that for $1\leq j\leq k$,
$\textsf{Post}_{\mathcal{M}}(m,{\sf i}_{1}\dots\sf i_{j})$ is defined and
${\sf o}_{j}=\textsf{Out}_{\mathcal{M}}(m,{\sf i}_{1}\dots\sf i_{j})$. For all
$u\in{\mathcal{I}}^{*}$, we write $f_{\mathbbm{i}\mathbbm{o}}(u)$ instead of
$f_{\mathbbm{i}\mathbbm{o}}(m_{\sf init},u)$. Note that the language accepted
by ${\mathcal{M}}$ satisfies
$L({\mathcal{M}})=\\{f_{\mathbbm{i}\mathbbm{o}}(u)\in({\mathcal{I}}{\mathcal{O}})^{*}\mid
f_{\mathbbm{i}\mathbbm{o}}(u)\text{ is defined}\\}$.

######  Remark 2.

A Mealy machine is a preMealy machine without holes. If ${\mathcal{M}}$ is
Mealy machine then the domain of $f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{M}}$ is
$M\times{\mathcal{I}}^{*}$.

###  0.D.2 Generalization phase: prefix-tree acceptor and state-merging

######  Example 6.

Consider the preMealy machine $\textsf{PTA}(E_{0})$ where $E_{0}$ has been
defined in Example 4. The equivalence relation $\sim_{0}$ defined by the state
partition $\\{\\{0,2,3\\},\\{1,4\\}\\}$ is a congruence for
$\textsf{PTA}(E_{0})$, however it is not a Mealy-congruence because we have
$0\sim_{0}3$ but for input ${\sf i}^{\prime}$,
$\textsf{Out}_{\textsf{PTA}(E_{0})}(0,{\sf i}^{\prime})={\sf o}\neq{\sf
o}^{\prime}=\textsf{Out}_{\textsf{PTA}(E_{0})}(3,{\sf i}^{\prime})$.

However, the equivalence relation $\sim_{0}^{\prime}$ defined by the state
partition $\\{\\{0,1\\},$ $\\{2,3,4\\}\\}$ is a Mealy-congruence for
$\textsf{PTA}(E_{0})$. The quotient $\textsf{PTA}(E_{0})/_{\sim^{\prime}_{0}}$
is depicted on the right of Figure 2 and it turns out to be a (complete) Mealy
machine. Its language $L$ is denoted by the regexp $({\sf i}^{\prime}+{\sf
i}){\sf o}({\sf i}{\sf o}+{\sf i}^{\prime}{\sf o}^{\prime})^{*}$. Note that
$E_{0}\subset L$.

The following lemma states that the quotient of a preMealy machine
${\mathcal{M}}$ by a Mealy-congruence for ${\mathcal{M}}$ is a preMealy
machine which generalizes ${\mathcal{M}}$.

######  Lemma 6.

If $\sim$ is a Mealy-congruence for ${\mathcal{M}}$, then
${\mathcal{M}}/_{\sim}$ is a preMealy machine s.t. $L({\mathcal{M}})\subseteq
L({\mathcal{M}}/_{\sim})$.

###### Proof.

It is because any execution of ${\mathcal{M}}$ over a sequence of inputs $v$
corresponds to a unique execution of ${\mathcal{M}}/_{\sim}$ (whose sequence
of states is the sequence of equivalence classes of states of ${\mathcal{M}}$
over $v$), and which produces the same outputs.∎∎

A _non-congruent point_ for an equivalence relation $\sim$ over the states of
a preMealy machine ${\mathcal{M}}$ is a triple $(x,x^{\prime},{\sf i})\in
M\times M\times{\mathcal{I}}$ such that $x\sim x^{\prime}$,
$\textsf{Post}(x,{\sf i})$ and $\textsf{Post}(x^{\prime},{\sf i})$ are both
defined but $\textsf{Post}(x,{\sf i})\not\sim\textsf{Post}(x^{\prime},{\sf
i})$. Given a non-congruent point $p=(x,x^{\prime},{\sf i})$, the equivalence
relation $\sim$ can be updated to remove $p$, to a coarser equivalence
relation $U(\sim,p)$ defined for all $y,y^{\prime}\in M$ as
$yU(\sim,p)y^{\prime}$ if $y\sim y^{\prime}$, or $y\sim\textsf{Post}(x,{\sf
i})$ and $y^{\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$, or
$y^{\prime}\sim\textsf{Post}(x,{\sf i})$ and
$y\sim\textsf{Post}(x^{\prime},{\sf i})$.

######  Example 7.

As an example, consider the preMealy machine $\textsf{PTA}(E_{0})$ defined in
Example 4, and the equivalence relation $\sim_{1}$ induced by the state-
partition $\\{\\{0,2\\},\\{1\\},\\{3\\},\\{4\\}\\}$. Then, $p_{1}=(0,2,{\sf
i})$ is a non-congruent point, because
$\textsf{Post}_{\textsf{PTA}(E_{0})}(0,{\sf
i})=2\not\sim_{1}3=\textsf{Post}_{\textsf{PTA}(E_{0})}(2,{\sf i})$. Then,
$\sim_{2}=U(\sim_{1},p_{1})$ is induced by the partition
$\\{\\{0,2,3\\},\\{1\\},\\{4\\}\\}$. Then, $p_{2}=(0,3,{\sf i}^{\prime})$ is a
non-congruent point for $\sim_{2}$, and $U(\sim_{2},p_{2})$ is exactly
$\sim_{0}$ as defined in Example 6, which is a congruence, so, does not
contain any non-congruent point.

We denote that an equivalence relation $\sim$ is finer than some equivalence
relation $\sim^{\prime}$ by $\sim\sqsubseteq\sim^{\prime}$. The following
proposition is (easily) proved in App. 0.D.4:

######  Proposition 1.

$U(\sim,p)$ is an equivalence relation such that $\sim\sqsubseteq U(\sim,p)$.

Given an equivalence relation $\sim$ over $M$, we now want to define a
procedure which keeps on removing non-congruent points, i.e., keeps on
applying the function $U$ iteratively until there is no non-congruent points
anymore. Therefore the resulting equivalence relation is a congruence for
${\mathcal{M}}$. We prove in Lemma 7 that the order in which those points are
removed does not matter. We formalize this via the notion of _choice function_
, which is a function $ch$ which, given any equivalence relation on the states
of a preMealy machine, outputs a non-congruent point (if it exists), otherwise
it is undefined. Given an equivalence relation $\sim$, a choice function $ch$
and two states $m,m^{\prime}$, we denote by $\sim_{ch}^{m,m^{\prime}}$ the
fixpoint of the sequence $(\sim^{m,m^{\prime},n})_{n\geq 0}$ where for all
$x,x^{\prime}\in M$, $x\sim^{m,m^{\prime},0}x^{\prime}$ if $x\sim x^{\prime}$,
or $x\sim m$ and $x^{\prime}\sim m^{\prime}$, or $x\sim m^{\prime}$ and
$x^{\prime}\sim m$ (in terms of equivalence classes, $\sim^{m,m^{\prime},0}$
merges $[m]_{\sim}$ and $[m^{\prime}]_{\sim}$). For all $n>0$,
$\sim^{m,m^{\prime},n}=U(\sim^{m,m^{\prime},n-1},ch({\mathcal{M}},\sim^{m,m^{\prime},n-1}))$
if $ch({\mathcal{M}},\sim^{m,m^{\prime},n-1})$ is defined, otherwise
$\sim^{m,m^{\prime},n}=\sim^{m,m^{\prime},n-1}$.

######  Example 8.

This converging sequence is already illustrated in Example 7 for some
particular choice function which first picks $p_{1}=(0,2,{\sf i})$ and then
$p_{2}=(0,3,{\sf i}^{\prime})$, starting from the equivalence relation $\sim$
induced by the partition $\\{\\{s\\}\mid s=0,\dots,4\\}$. Then,
$\sim^{0,2,0}=\sim_{1}$, $\sim^{0,2,1}=U(\sim_{1},p_{1})=\sim_{2}$ and
$\sim^{0,2,3}=U(\sim_{2},p_{2})=\sim_{0}$ which is the fixpoint of the
sequence. Note that taking a different order, first $p_{2}$ and then $p_{1}$,
we would get the same fixed point: $U(\sim_{1},p_{2})$ is induced by the
partition $\\{\\{0,2\\},\\{3\\},\\{1,4\\}\\}$ and $U(U(\sim_{1},p_{1}))$ is
induced by the partition $\\{\\{0,2,3\\},\\{1,4\\}\\}$, so,
$U(U(\sim_{1},p_{1}),p_{2})=U(U(\sim_{1},p_{2}),p_{1})$. This observation can
be generalized, as shown by the following lemma (proved in App. 0.D.5).

######  Lemma 7.

For any equivalence relation $\sim$ and choice functions $ch_{1},ch_{2}$, we
have that $\sim^{m,m^{\prime}}_{ch_{1}}=\sim^{m,m^{\prime}}_{ch_{2}}$.

By the previous lemma, given an equivalence relation $\sim$ over the states of
a preMealy-machine ${\mathcal{M}}$, we can define $\sim^{m,m^{\prime}}$ as
$\sim^{m,m^{\prime}}_{ch}$ for any choice function $ch$. Note that
$\sim^{m,m^{\prime}}$ is a congruence for ${\mathcal{M}}$ because it is does
not contain non-congruent points anymore, but it is not necessarily a Mealy-
congruence for ${\mathcal{M}}$. We say that two states $m,m^{\prime}$ of
${\mathcal{M}}$ are _$\sim$ -mergeable_ if $\sim^{m,m^{\prime}}$ is a Mealy-
congruence for ${\mathcal{M}}$. We say that $m$ and $m^{\prime}$ are
_mergeable_ if they are $diag_{\mathcal{M}}$-mergeable, where $diag_{M}$ is
the finest equivalence relation over $M$, i.e. $diag_{M}=\\{(m,m)\mid m\in
M\\}$.

######  Example 9.

As an example, state $0$ and $2$ are not mergeable in Example 4, because
$diag_{E_{0}}^{0,2}=\sim_{0}$ is not a Mealy-congruence, as illustrated in
Example 7. However, $2$ and $3$ are mergeable, $3$ and $4$, and $1$ and $4$.

We denote by $\textsf{Mergeable}({\mathcal{M}},\sim,m,m^{\prime})$ (resp.
$\textsf{Mergeable}({\mathcal{M}},m,m^{\prime})$) the predicate which holds
true whenever $m$ and $m^{\prime}$ are $\sim$-mergeable (resp. mergeable).
When $m$ and $m^{\prime}$ are $\sim$-mergeable, we let
$\textsf{MergeClass}({\mathcal{M}},\sim,m,m^{\prime})=\sim^{m,m^{\prime}}$ and
$\textsf{MergeStates}({\mathcal{M}},\sim,m,m^{\prime})={\mathcal{M}}/_{\sim^{m,m^{\prime}}}$.

######  Lemma 8.

For all preMealy machine ${\mathcal{M}}$, all equivalence relation $\sim$ over
the states of ${\mathcal{M}}$, all $\sim$-mergeable states $m,m^{\prime}$, we
have $\sim\sqsubseteq\textsf{MergeClass}({\mathcal{M}},\sim,m,m^{\prime})$ and
therefore $L({\mathcal{M}})\subseteq
L(\textsf{MergeStates}({\mathcal{M}},\sim,m,m^{\prime}))$. Moreover, if
$m\not\sim m^{\prime}$, then
$\sim\sqsubset\textsf{MergeClass}({\mathcal{M}},\sim,m,m^{\prime})$ and
therefore $\textsf{MergeStates}({\mathcal{M}},\sim,m,m^{\prime})$ has strictly
less states than ${\mathcal{M}}/_{\sim}$.

###### Proof.

Immediate by Lemma 6 and the definition of $\sim$-mergeable states.∎∎

###  0.D.3 Termination and correctness of Algorithm GEN(Algo. 1)

We first prove that algorithm Gen indeed generalizes the examples while
preserving realizability of the specification.

######  Lemma 9.

For all merging strategy $\sigma_{G}$, all finite set of examples $E$ and all
specification ${\mathcal{S}}$ given as a deterministic safety automaton
${\mathcal{A}}$, if Gen$(E,{\mathcal{S}},\sigma_{G})\neq UNREAL$, then
$\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})$ is a preMealy machine
${\mathcal{M}}$ such that ${\mathcal{S}}$ is ${\mathcal{M}}$-realizable and
$E\subseteq L({\mathcal{M}})$. If
$\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})=UNREAL$, then there is no such
preMealy machine. Moreover, $\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})$
terminates in time polynomial in the size777The size of $E$ is defined as the
cardinality of ${\sf Prefs}(E)$ of $E$ and exponential in $n$ the number of
states of ${\mathcal{A}}$.

###### Proof.

Suppose that $\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})\neq UNREAL$. Then $E$
is necessarily consistent and ${\mathcal{S}}$ is $\textsf{PTA}(E)$-realizable.
By Lemma 8, the loop at line 1 computes coarser and coarser Mealy-congruences
for $\textsf{PTA}(E)$. Therefore, if we denote by $\sim_{E}$ the relation
computed by the algorithm after exiting the loop, we have
$diag_{E}\sqsubseteq\sim_{E}$ and hence
$L(\textsf{PTA}(E)/_{diag_{E}})=L(\textsf{PTA}(E))=E\subseteq
L(\textsf{PTA}(E)/_{\sim_{E}})$. Moreover, line 1 also ensures that
${\mathcal{S}}$ is $\textsf{PTA}(E)/_{\sim}$-realizable for all equivalence
relation $\sim$ computed during iterations of the loop, and in particular for
$\sim_{E}$.

Now, suppose that $\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})=UNREAL$, then
either $E$ is not consistent, in which case it is clear that no preMealy
machine ${\mathcal{M}}$ satisfies $E\subseteq L({\mathcal{M}})$, or
${\mathcal{S}}$ is not $\textsf{PTA}(E)$-realizable. For the second case,
assume that there is a preMealy machine ${\mathcal{M}}$ such that $E\subseteq
L({\mathcal{M}})$ and ${\mathcal{S}}$ is ${\mathcal{M}}$-realizable by some
machine ${\mathcal{P}}$, and let us derive a contradiction. We show that
${\mathcal{S}}$ is $\textsf{PTA}(E)$-realizable by some Mealy machine
${\mathcal{P}}^{\prime}$ obtained by taking the synchronized product of
${\mathcal{P}}$ and $\textsf{PTA}(E)$: a state of ${\mathcal{P}}^{\prime}$ is
either a state $p$ of ${\mathcal{P}}$ or a pair $(p,e)$ where $e$ a state of
$\textsf{PTA}(E)$. The initial state of the product is $(p_{0},\epsilon)$
where $p_{0}$ is the initial state of ${\mathcal{P}}$. From a state $(p,e)$
and an input ${\sf i}\in{\mathcal{I}}$, if $\textsf{Out}_{\mathcal{P}}(p,{\sf
i})=\textsf{Out}_{\textsf{PTA}(E)}(e,{\sf i})={\sf o}$ for some ${\sf
o}\in{\mathcal{O}}$, then the product transitions to $({\sf
o},(\textsf{Post}_{\mathcal{P}}(p,{\sf i}),\textsf{Post}_{\textsf{PTA}(E)}))$,
otherwise, it transitions to $\Delta_{\mathcal{P}}(p,{\sf i})$. This is
correct since $L(\textsf{PTA}(E))={\sf Prefs}(E)\subseteq L({\mathcal{P}})$.
Moreover by definition of the product, $\textsf{PTA}(E)$ is a subgraph of
${\mathcal{P}}^{\prime}$ (up to state renaming).

For the complexity, there are $|{\sf Prefs}(E)|$ visits to the loop. Line 1
takes polynomial time (the computation of $\sim^{m,m^{\prime}}$ for any two
states $m,m^{\prime}$ of a preMealy machine is in ptime). According to 2, each
realizability test at Line 1 takes time polynomial in the number of states of
the preMealy machine and exponential in $n$. Here, the number of states of the
preMealy machine is smaller than the size of $E$. Overall, this gives the
claimed complexity.∎∎

###  0.D.4 Proof of Proposition 1

###### Proof.

For all $y\in M$, $y\sim y$ hence $y\ U(\sim,p)\ y$. Symmetry is also
immediate by definition. Let us prove transitivity. If $y\ U(\sim,p)\
y^{\prime}$ and $y^{\prime}\ U(\sim,p)\ y^{\prime\prime}$, then there are
several cases:

  1. 1.

$y\sim y^{\prime}$ and $y^{\prime}\sim y^{\prime\prime}$: hence $y\sim
y^{\prime\prime}$ and so $y\ U(\sim,p)\ y^{\prime\prime}$.

  2. 2.

$y\sim y^{\prime}$ and $y^{\prime}\sim\textsf{Post}(x,{\sf i})$ and
$y^{\prime\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$: hence
$y\sim\textsf{Post}(x,{\sf i})$ and $y^{\prime\prime}\sim\textsf{Post}(y,{\sf
i})$, so $y\ U(\sim,p)\ y^{\prime\prime}$.

  3. 3.

$y\sim y^{\prime}$ and $y^{\prime\prime}\sim\textsf{Post}(x,{\sf i})$ and
$y^{\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$: hence
$y^{\prime\prime}\sim\textsf{Post}(x,{\sf i})$ and
$y\sim\textsf{Post}(x^{\prime},{\sf i})$, so $y\ U(\sim,p)\ y^{\prime\prime}$.

  4. 4.

$y\sim\textsf{Post}(x,{\sf i})$ and
$y^{\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$ and $y^{\prime}\sim
y^{\prime\prime}$: therefore
$y^{\prime\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$ and so $y\ U(\sim,p)\
y^{\prime\prime}$.

  5. 5.

$y\sim\textsf{Post}(x,{\sf i})$ and
$y^{\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$ and
$y^{\prime}\sim\textsf{Post}(x,{\sf i})$ and
$y^{\prime\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$: so, $y\sim
y^{\prime}$ and $y^{\prime}\sim y^{\prime\prime}$, which implies $y\sim
y^{\prime\prime}$ and so $y\ U(\sim,p)\ y^{\prime\prime}$.

  6. 6.

$y\sim\textsf{Post}(x,{\sf i})$ and
$y^{\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$ and
$y^{\prime\prime}\sim\textsf{Post}(x,{\sf i})$ and
$y^{\prime}\sim\textsf{Post}(x^{\prime},{\sf i})$: we directly get $y\sim
y^{\prime\prime}$ and so $y\ U(\sim,p)\ y^{\prime\prime}$.

The remaining cases are symmetrical to the cases already proved by
substituting $y$ by $y^{\prime\prime}$ and $y^{\prime\prime}$ by $y$.

∎

∎

###  0.D.5 Proof of Lemma 7

###### Proof.

We define a relation $\rightarrow$ between equivalence relations as follows:
$\sim\rightarrow\sim^{\prime}$ if $\sim^{\prime}=U(\sim,p)$ for some some non-
congruent point $p$ (if it exists). We prove that $\rightarrow$ is locally
confluent, which by Newman’s lemma implies that $\rightarrow$ is globally
confluent. In other words, the reflexive and transitive closure
$\rightarrow^{*}$ of $\rightarrow$ satisfies that whenever
$\sim\rightarrow^{*}\sim_{1}$ and $\sim\rightarrow^{*}\sim_{2}$, then there
exists $\sim^{\prime}$ such that $\sim_{1}\rightarrow^{*}\sim^{\prime}$ and
$\sim_{2}\rightarrow^{*}\sim^{\prime}$. The proof of local confluence is not
difficult but technical, as many cases have to be considered. The main idea is
to show that if $p$ and $p^{\prime}$ are two different non-congruent points of
$\sim$, then $p^{\prime}$ is a non-congruent point of $U(\sim,p)$ and
$p^{\prime}$ is a non-congruent point of $U(\sim,p^{\prime})$, and then we
show that $U(U(\sim,p),p^{\prime})=U(U(\sim,p^{\prime}),p)$.

Formally, let $p=(x,y,{\sf i}),p=(x^{\prime},y^{\prime},{\sf i}^{\prime})$ be
two different non-congruent points for $\sim$. Let $\sim_{p}=U(\sim,p)$ and
$\sim_{p^{\prime}}=U(\sim,p^{\prime})$. So, $\sim\rightarrow\sim_{p}$ and
$\sim_{\rightarrow}\sim_{p^{\prime}}$. Assume that
$\sim_{p}\neq\sim_{p^{\prime}}$. We prove that $p^{\prime}$ is a non-congruent
point of $\sim_{p}$ (and symmetrically $p$ is a non-congruent point of
$\sim_{p^{\prime}}$). Suppose that $p^{\prime}$ is not a non-congruent point
of $\sim_{p}$. Then, $\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i})\sim_{p}\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i})$. We also know that
$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i})\not\sim\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i})$ because
$p^{\prime}$ is a non-congruent point of $\sim$. By definition of $\sim_{p}$,
it implies that the following symmetrical two cases can happen:

  1. 1.

$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$, or

  2. 2.

$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$.

We show that both cases imply that $\sim_{p}=\sim_{p^{\prime}}$ which is a
contradiction. Consider the first case. Then,

$u\sim_{p}v$ iff

$u\sim v$, or $u\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$, or
$v\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$u\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ iff

$u\sim v$, or $u\sim\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$
and $v\sim\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$, or
$v\sim\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$ and
$u\sim\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$ iff

$u\sim_{p^{\prime}}v$.

The second case is symmetrical. We have just shown that $p^{\prime}$ is a non-
congruent point of $\sim_{p}$ and by symmetry, $p$ is a non-congruent point of
$\sim_{p^{\prime}}$. We finally prove that
$U(\sim_{p},p^{\prime})=U(\sim_{p^{\prime}},p)$, concluding that $\rightarrow$
is locally confluent. We show that $U(\sim_{p},p^{\prime})$ is finer than
$U(\sim_{p^{\prime}},p)$, the other direction being completly symmetrical.
Suppose that $u\ U(\sim_{p},p^{\prime})\ v$ and let us show that $u\
U(\sim_{p^{\prime}},p)\ v$. Therefore, we have one the following cases:

  1. 1.

$u\sim_{p}v$,

  2. 2.

$u\sim_{p}\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$ and
$v\sim_{p}\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$,

  3. 3.

$u\sim_{p}\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$ and
$v\sim_{p}\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$.

Let us consider the first two cases (the third being symmetrical to the
second):

  1. 1.

$u\sim_{p}v$ implies that one of the following three cases holds:

    1. (a)

$u\sim v$: then $u\sim_{p^{\prime}}v$, and $uU(\sim_{p^{\prime}},p)v$.

    2. (b)

$u\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$: then
$u\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$v\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(y,{\sf i})$, and so $u\
U(\sim_{p^{\prime}},p)\ v$.

    3. (c)

$u\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$: this case is symmetric to the
former.

  2. 2.

$u\sim_{p}\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$ and
$v\sim_{p}\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$ implies
that one of the following cases hold:

    1. (a)

$u\sim\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$: so,
$u\sim_{p^{\prime}}v$ and hence $u\ U(\sim_{p^{\prime}},p)\ v$.

    2. (b)

$u\sim\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$: hence
$v\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(x,i)$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(y,{\sf i})$. By
definition of $\sim_{p^{\prime}}$, we also have
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})$. Since $u\sim\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})$, we have
$u\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$
and from the latter statement, we get
$u\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$
and hence $u\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(y,{\sf i})$. All this
imply that $u\ U(\sim_{p^{\prime}},p)\ v$.

    3. (c)

$u\sim\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf i}^{\prime})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$: this case is
symmetrical to the latter by substituting $y$ by $x$ and $x$ by $y$.

    4. (d)

$u\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$: by definition
of $\sim_{p^{\prime}}$, we have $\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})$ from which we get $v\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$
and therefore $v\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(y,{\sf i})$. From
$u\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ we get
$u\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(x,{\sf i})$. Therefore, $u\
U(\sim_{p^{\prime}},p)\ v$.

    5. (e)

$u\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$: we immediately get
$u\sim v$, so $u\sim_{p^{\prime}}v$ and hence $u\ U(\sim_{p^{\prime}},p)\ v$.

    6. (f)

$u\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$: from
$u\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ we get
$u\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and from
$v\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ we get
$v\sim_{p^{\prime}}\textsf{Post}_{\mathcal{M}}(y,{\sf i})$, hence $u\
U(\sim_{p^{\prime}},p)\ v$.

    7. (g)

$u\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf i}^{\prime})$: symmetric of
case $(d)$ by swapping $x$ and $y$.

    8. (h)

$u\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$: symmetric of case
$(e)$ by swapping $x$ and $y$.

    9. (i)

$u\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(x^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$ and
$v\sim\textsf{Post}_{\mathcal{M}}(y,{\sf i})$ and
$\textsf{Post}_{\mathcal{M}}(y^{\prime},{\sf
i}^{\prime})\sim\textsf{Post}_{\mathcal{M}}(x,{\sf i})$: symmetric of case
$(f)$ by swapping $x$ and $y$.

∎∎

###  0.D.6 Details and results on the completion phase

Our goal in this section is to prove correctness of Comp(${\mathcal{M}}_{0}$,
${\mathcal{S}}$, $\sigma_{C}$) and termination. The completion procedure may
not terminate for some completion strategies. It is because the completion
strategy could for instance keep on selecting a pairs of the form $({\sf
o},m^{\prime})$ where $m^{\prime}$ is a fresh state. However we prove that it
always terminates for _lazy_ completion strategies, as defined in Section 3.3.
Recall that lazy strategies always favour existing states. We first start by
proving correctness.

######  Lemma 10.

If the algorithm $\textsc{Comp}({\mathcal{M}}_{0},{\mathcal{S}},\sigma_{C})$
terminates and returns a Mealy machine ${\mathcal{M}}$, then ${\mathcal{S}}$
is ${\mathcal{M}}_{0}$-realized by ${\mathcal{M}}$., i.e., ${\mathcal{S}}$ is
realizable by ${\mathcal{M}}$ and ${\mathcal{M}}_{0}$ is a subgraph of
${\mathcal{M}}$ (${\mathcal{M}}_{0}\preceq{\mathcal{M}}$).

###### Proof.

Let ${\mathcal{M}}_{i}$ be the machine computed after the $i$th iteration of
the while-loop. As explained before, the tests at lines 2 and 2 ensures the
invariant that each ${\mathcal{M}}_{i}$ ${\mathcal{M}}_{0}$-realizes
${\mathcal{S}}$. It is trivial for the test at line 2. Since iteration $i+1$
of the algorithm completes the machine ${\mathcal{M}}_{i}$ into a machine
${\mathcal{M}}_{i+1}$, we get
${\mathcal{M}}_{0}\preceq{\mathcal{M}}_{1}\preceq{\mathcal{M}}_{2}\dots$.
Therefore, if ${\mathcal{S}}$ is ${\mathcal{M}}_{i}$-realizable, it is also
${\mathcal{M}}_{0}$-realizable by ${\mathcal{M}}_{i}$, so the test at line 2
guarantees that all the machines ${\mathcal{M}}_{i}$
${\mathcal{M}}_{0}$-realize ${\mathcal{S}}$. Moreover, the list of candidates
at line 2 is guaranteed to be non-empty. Indeed, by the invariant,
${\mathcal{M}}_{i}$ can always be completed into a Mealy machine realizing
${\mathcal{S}}$. So the selection at line 2 is well-defined. Hence, if the
algorithm returns a machine, this machine is necessarily a Mealy machine,
because it has no holes, and moreover it ${\mathcal{M}}_{0}$-realizes
${\mathcal{S}}$.∎∎

In the sequel, our goal is to prove termination for lazy strategies. The
following technical lemma is a key lemma towards showing termination. It gives
a sufficient condition for which a state of a preMealy machine can be reused
to complete a hole. We need some notation. Given a preMealy machine
${\mathcal{M}}=(M,m_{0},\Delta)$ and a deterministic parity automaton
$A=(Q,q_{0},{\mathcal{I}}\cup{\mathcal{O}},\delta_{A},d)$, for all $m\in M$,
we let $R_{m}^{A,{\mathcal{M}}}\subseteq Q$ (or just $R_{m}$ if $A$ and
${\mathcal{M}}$ are clear from the context, all the states of $A$ reachable
from its initial state when reading words that reach state $m$ when read by
${\mathcal{M}}$. Formally,

$R_{m}^{A,{\mathcal{M}}}=\\{\textsf{Post}^{*}_{A}(q_{0},u)\mid
u\in({\mathcal{I}}{\mathcal{O}})^{*},\textsf{Post}_{\mathcal{M}}^{*}(m_{0},u)=m\\}$

Given a subset $Q^{\prime}\subseteq Q$ and some input
$u\in({\mathcal{I}}{\mathcal{O}})^{*}$, we let
$\textsf{Post}_{A}^{*}(Q,u)=\\{\textsf{Post}_{A}^{*}(q,u)\mid q\in
Q^{\prime}\\}$.

######  Lemma 11.

Let ${\mathcal{S}}$ be a safety specification given as a (complete888Automata
in this paper are complete by definition, i.e. there is always a transition
from any state on any input, but we stress it here as it is a necessary
requirement for the statement to hold.) deterministic safety automaton
$A=(Q,Q_{usf},q_{0},\delta_{A})$. Let ${\mathcal{M}}=(M,m_{0},\delta)$ be a
preMealy-machine such that ${\mathcal{S}}$ is ${\mathcal{M}}$-realizable. Let
$(m,{\sf i})$ be a hole of ${\mathcal{M}}$ (if it exists). For all ${\sf
o}\in{\mathcal{O}}$ and $m^{\prime}\in M$, if
$\textsf{Post}_{A}^{*}(R_{m},{\sf i}{\sf o})\subseteq R_{m^{\prime}}$, then
${\mathcal{S}}$ is ${\mathcal{M}}^{\prime}$-realizable for
${\mathcal{M}}^{\prime}=(M,m_{0},\delta\cup\\{(m,{\sf i})\mapsto({\sf
o},m^{\prime})\\})$.

###### Proof.

We keep the same notations as in the statement of the lemma. Let
${\mathcal{M}}_{t}=(M_{t},m_{0},\Delta_{t})$ be a Mealy machine which realizes
${\mathcal{S}}$ and such that ${\mathcal{M}}$ is a subgraph of
${\mathcal{M}}_{t}$, i.e., ${\mathcal{M}}\preceq{\mathcal{M}}_{t}$. The
subscript $t$ stands for the fact that the transition function of
${\mathcal{M}}_{t}$ is total. We assume without loss of generality that
${\mathcal{M}}_{t}$ has a special form: when $M\subseteq M_{t}$ is left, it is
never visited again. Formally, for all $u\in{\mathcal{I}}^{*}$, if
$\textsf{Post}_{{\mathcal{M}}_{t}}^{*}(m_{0},u)\not\in M$, then for all
$v\in{\mathcal{I}}^{*}$,
$\textsf{Post}_{{\mathcal{M}}_{t}}^{*}(m_{0},uv)\not\in M$. The machine
${\mathcal{M}}_{t}$ can be modified, using one additional bit of memory, so
that it satisfies this assumption.

Let ${\sf o}=\textsf{Out}_{{\mathcal{M}}_{t}}(m,{\sf i})$ and let
${\mathcal{M}}^{\prime}=(M,m_{0},\delta^{\prime}:=\delta\cup\\{(m,{\sf
i})\mapsto({\sf o},m^{\prime})\\})$. We modify ${\mathcal{M}}_{t}$ into a
Mealy machine ${\mathcal{M}}^{\prime}_{t}$ by redirecting the transition from
$(m,{\sf i})$ to $({\sf o},m^{\prime})$. Formally,
${\mathcal{M}}^{\prime}_{t}=(M_{t},m_{0},\Delta_{t}^{\prime})$ where

$\Delta_{t}^{\prime}=(\Delta_{t}\setminus\\{(m,{\sf
i})\rightarrow\Delta_{t}(m,{\sf i})\\})\cup\\{(m,{\sf i})\mapsto({\sf
o},m^{\prime})\\}$

Clearly, ${\mathcal{M}}^{\prime}$ is a subgraph of
${\mathcal{M}}_{t}^{\prime}$ because ${\mathcal{M}}$ is a subgraph of
${\mathcal{M}}_{t}$. It remains to show that ${\mathcal{M}}_{t}^{\prime}$
realizes ${\mathcal{S}}$.

Assume that it is not the case and let us derive a contradiction. In other
words, there exists $w\in L_{\omega}({\mathcal{M}}^{\prime}_{t})$ ($u$ is a
finite word) such that $w\not\in L(A)$. Let
$u\in({\mathcal{I}}{\mathcal{O}})^{*}$ be the shortest unsafe prefix of $w$,
i.e. the prefix of $w$ such that the states visited by the execution of $A$ on
$u$ are safe but the last one. We decompose $u$ according to its execution in
${\mathcal{M}}^{\prime}_{t}$ and the visit to the new transition $(m,{\sf
i})\mapsto({\sf o},m^{\prime})$ (call it $t_{new}$). By our assumption on the
form of ${\mathcal{M}}_{t}$, whenever ${\mathcal{M}}$ is left, it is never
visited again. By definition of ${\mathcal{M}}^{\prime}_{t}$, we therefore
have that whenever ${\mathcal{M}}^{\prime}$ is left, it is never visited
again. So, the execution of ${\mathcal{M}}^{\prime}_{t}$ on $u$ visits
$t_{new}$ a couple of times (at least once) while staying in ${\mathcal{M}}$
and after the last visit to $t_{new}$, is continued by the execution of
${\mathcal{M}}_{t}$ on the remaining suffix of $u$, ending in an unsafe state.
Formally, there exist $u_{1},\dots,u_{k}\in({\mathcal{I}}{\mathcal{O}})^{*}$
and $p_{1},p^{\prime}_{1},\dots,p_{k-1},p^{\prime}_{k-1},p_{k}\in Q$ such that
$u=u_{1}{\sf i}{\sf o}u_{2}{\sf i}{\sf o}\dots\sf i{\sf o}u_{k}$ and

$\begin{array}[]{rllllllllllllllll}q_{0}&\xrightarrow{u_{1}}_{A}&p_{1}&\xrightarrow{{\sf
i}{\sf
o}}_{A}&p^{\prime}_{1}&\xrightarrow{u_{2}}_{\mathsf{assist}}&p_{2}&\dots&p^{\prime}_{k-1}&\xrightarrow{u_{k}}&p_{k}\in
Q_{usf}\\\ m_{0}&\xrightarrow{u_{1}}_{\mathcal{M}}&m&\xrightarrow{{\sf i}|{\sf
o}}&m^{\prime}&\xrightarrow{u_{2}}_{\mathcal{M}}&m&\dots&m^{\prime}&\xrightarrow{u_{k}}_{{\mathcal{M}}_{t}}&m^{\prime\prime}\end{array}$

We prove that for all $1\leq j\leq k-1$, there exists
$x_{j}\in({\mathcal{I}}{\mathcal{O}})^{*}$ such that
$\textsf{Post}_{\mathcal{M}}(m_{0},x_{j})=m^{\prime}$ and
$\textsf{Post}_{A}(p_{0},x_{j})=p^{\prime}_{j}$. We prove by induction on $j$.
For $j=1$, note that we have $p_{1}\in R_{m}^{A,{\mathcal{M}}}$, and so
$p^{\prime}_{1}\in\textsf{Post}_{A}(R_{m}^{A,{\mathcal{M}}},{\sf i}{\sf o})$.
So, $p^{\prime}_{1}\in R_{m^{\prime}}^{A,{\mathcal{M}}}$. It implies that
there exists $x_{1}\in({\mathcal{I}}{\mathcal{O}})^{*}$ satisfying the claim.
Suppose it is true at rank $j-1$. So, there exists $x_{j-1}$ such that
$\textsf{Post}_{\mathcal{M}}(m_{0},x_{j-1})=m^{\prime}$ and
$\textsf{Post}_{A}$ $(p_{0},x_{j-1})=p^{\prime}_{j-1}$. Therefore,
$\textsf{Post}_{\mathcal{M}}(m_{0},x_{j-1}u_{j})=m$ and
$\textsf{Post}_{A}(p_{0},x_{j-1}u_{j})=p_{j}$. This implies that $p_{j}\in
R_{m}^{A,{\mathcal{M}}}$, and so
$p^{\prime}_{j}\in\textsf{Post}_{A}(R_{m}^{A,{\mathcal{M}}},{\sf i}{\sf o})$,
and so there exists $x_{j}\in({\mathcal{I}}{\mathcal{O}})^{*}$ satisfying the
claim at rank $j$.

Now, consider the word $x_{k-1}u_{k}$ :
$\textsf{Post}_{A}(p_{0},x_{k-1}u_{k})=p_{k}\in Q_{usf}$ and
$\textsf{Post}_{{\mathcal{M}}_{t}}$ $(m_{0},x_{k-1}u_{k})$
$=m^{\prime\prime}$. This contradicts that ${\mathcal{M}}_{t}$ realizes
$L(A)$. ∎∎

We are now ready to prove termination of Algo 2. To establish the complexity,
we need to introduce some notions about chains and antichains of subsets. Let
$Y$ be a finite set of cardinality $n$. It is well-known that the set $2^{Y}$
is partially ordered by inclusion. Therefore, an antichain of elements of
$2^{Y}$ is a set $\mathcal{Y}\subseteq 2^{Y}$ such that for all
$Y_{1},Y_{2}\in\mathcal{Y}$, $Y_{1}$ and $Y_{2}$ are incomparable by
$\subseteq$. We denote by $\mathcal{A}\mathcal{C}_{\subseteq}(Y)$ the set of
$\subseteq$-antichains over $Y$. The set
$\mathcal{A}\mathcal{C}_{\subseteq}(Y)$ can be partially ordered by the
partial order denoted $\trianglelefteq$: for all
$\mathcal{Y}_{1},\mathcal{Y}_{2}\in\mathcal{A}\mathcal{C}_{\subseteq}(Y)$,
$\mathcal{Y}_{1}\trianglelefteq\mathcal{Y}_{2}$ if for all
$Y_{1}\in\mathcal{Y}_{1}$, there exists $Y_{2}\in\mathcal{Y}_{2}$ such that
$Y_{1}\subseteq Y_{2}$. It is well-known that
$(\mathcal{A}\mathcal{C}_{\subseteq}(Y),\trianglelefteq)$ is a lattice. A
chain in $(\mathcal{A}\mathcal{C}_{\subseteq}(Y),\trianglelefteq)$ is a
sequence
$\mathcal{Y}_{1}\vartriangleleft\mathcal{Y}_{2}\vartriangleleft\dots\vartriangleleft\mathcal{Y}_{m}$
(note that all relations are strict). The following lemma is key to bound the
termination time:

######  Lemma 12.

Let $Y$ be a set of cardinality $n$. Any $\vartriangleleft$-chain in
$(\mathcal{A}\mathcal{C}_{\subseteq}(Y),\trianglelefteq)$ has length at most
$2^{n}$.

###### Proof.

Given an antichain $\mathcal{Y}\in\mathcal{A}\mathcal{C}_{\subseteq}(Y)$, we
let $\downarrow\mathcal{Y}$ be the downward closure of $\mathcal{Y}$, i.e.,
$\downarrow\mathcal{Y}=\\{X\subseteq Y\mid\exists
X^{\prime}\in\mathcal{Y},X\subseteq X^{\prime}\\}$. Now, observe that for all
$\mathcal{Y}_{1},\mathcal{Y}_{2}\in\mathcal{A}\mathcal{C}_{\subseteq}(Y)$, we
have $\mathcal{Y}_{1}\vartriangleleft\mathcal{Y}_{2}$ iff
$\downarrow\mathcal{Y}_{1}\subsetneq\downarrow\mathcal{Y}_{2}$. Indeed, for
the ’only if’ direction, assume that
$\mathcal{Y}_{1}\vartriangleleft\mathcal{Y}_{2}$ and take
$X_{1}\in{\downarrow}\mathcal{Y}_{1}$. Hence there exists
$Y_{1}\in\mathcal{Y}_{1}$ s.t. $X_{1}\subseteq Y_{1}$. So, there exists
$Y_{2}\in\mathcal{Y}_{2}$ s.t. $Y_{1}\subseteq Y_{2}$, which implies that
$X_{1}\in{\downarrow}\mathcal{Y}_{2}$. Conversely, suppose that
$\downarrow\mathcal{Y}_{1}\subsetneq\downarrow\mathcal{Y}_{2}$. Let
$Y_{1}\in\mathcal{Y}_{1}$. Then, $Y_{1}\in{\downarrow}\mathcal{Y}_{1}$, so
$Y_{1}\in{\downarrow}\mathcal{Y}_{2}$, which means that there exists
$Y_{2}\in\mathcal{Y}_{2}$ s.t. $Y_{1}\subseteq Y_{2}$. This observation
implies that the length of any $\vartriangleleft$-chain of antichains is at
most the length of a maximal $\subsetneq$-chain of subsets of ${2^{Y}}$, which
is at most $2^{|Y|}$. ∎∎

We now prove termination (assuming the completion strategy $\sigma_{C}$ is
computable in exptime).

######  Lemma 13.

If $\sigma_{C}$ is lazy, Comp$({\mathcal{M}}_{0},S,\sigma_{C})$ terminates in
time polynomial in $|{\mathcal{I}}|$ and the number of holes in
${\mathcal{M}}_{0}$, and exponential in the number of states of the
deterministic safety automaton defining ${\mathcal{S}}$, and the number of
states of ${\mathcal{M}}_{0}$.

###### Proof.

Let $A=(Q,q_{0},\delta,d)$ be a deterministic parity automaton defining the
specification. Let ${\mathcal{M}}_{0}=(M_{0},m_{0},\Delta_{0})$ be a preMealy
machine such that ${\mathcal{S}}$ is ${\mathcal{M}}_{0}$-realizable (otherwise
the algorithm terminates at line 2). Suppose that the algorithm does not
terminate and for all $i\geq 1$, let
${\mathcal{M}}_{i}=(M_{i},m_{0},\Delta_{i})$ be the preMealy-machine computed
at the $i$th-iteration of the while-loop. For all $i\geq 0$ and $m\in M_{i}$,
we define $R_{m}^{i}$ as a shortcut for $R_{m}^{A,{\mathcal{M}}_{i}}$. Since
$m$ is a state of ${\mathcal{M}}_{i}$ and ${\mathcal{M}}_{i}$ is a subgraph of
${\mathcal{M}}_{i+1}$, the set of words reaching $m$ in ${\mathcal{M}}_{i}$ is
included in the set of words reaching $m$ in ${\mathcal{M}}_{i+1}$. Therefore
we obtain the following monotonicity property: $R_{m}^{i}\subseteq
R_{m}^{i+1}$.

Let $\mathcal{X}_{i}=\\{R_{m}^{i}\mid m\in M_{i}\\}$. Let denote by
$\lceil\mathcal{X}_{i}\rceil$ the maximal elements of $\mathcal{X}_{i}$ for
inclusion. By the monotonicity property, we get that the sequence
$(\lceil\mathcal{X}_{i}\rceil)_{i\geq 0}$ eventually stabilizes: there exists
$\alpha$ such that for all $i\geq\alpha$,
$\lceil\mathcal{X}_{i}\rceil=\lceil\mathcal{X}_{i+1}\rceil$.

Consider a machine ${\mathcal{M}}_{j}$ for $j\geq\alpha$ and the hole $(m,{\sf
i})$ of ${\mathcal{M}}_{j}$ completed at iteration $j$ by the algorithm, i.e.
$\Delta_{j+1}(m,{\sf i})=({\sf o},m^{\prime})$ for some ${\sf
o}\in{\mathcal{O}}$ and $m^{\prime}\in M_{j+1}$. We claim that $m^{\prime}\in
M_{j}$, i.e., the algorithm has reused some existing state of
${\mathcal{M}}_{j}$. Indeed, consider the set $R_{m,{\sf i},{\sf
o}}^{j}=\textsf{Post}_{A}^{*}(R_{m}^{j},{\sf i}{\sf o})$. We have that
$R_{m,{\sf i},{\sf o}}^{j}\subseteq R_{m^{\prime}}^{j+1}$ because
${\mathcal{M}}_{j+1}$ transitions from $(m,{\sf i})$ to $({\sf
o},m^{\prime})$. Clearly, there exists $X\in\lceil\mathcal{X}_{j+1}\rceil$
such that $R_{m,{\sf i},{\sf o}}^{j}\subseteq R_{m^{\prime}}^{j+1}\subseteq X$
and since $\lceil\mathcal{X}_{j}\rceil=\lceil\mathcal{X}_{j+1}\rceil$,
$X\in\lceil\mathcal{X}_{j}\rceil$. By definition of $\mathcal{X}_{j}$,
$X=R_{m^{\prime\prime}}^{j}$ for some $m^{\prime\prime}\in M_{j}$. Hence,
$R_{m,{\sf i},{\sf o}}^{j}\subseteq R_{m^{\prime\prime}}^{j}$. Let
${\mathcal{M}}^{\prime}=(M_{j},m_{0},\delta_{i}\cup\\{(m,{\sf i})\mapsto({\sf
o},m^{\prime\prime})\\}$. By Lemma 11, ${\mathcal{S}}$ is
${\mathcal{M}}^{\prime}$-realizable, therefore at iteration $j$, the set
$candidates$ at line 2 contains the pair $({\sf o},m^{\prime\prime})$. Since
the selection strategy is lazy, if $m^{\prime}\not\in M_{j}$, it would favour
$m^{\prime\prime}$. Hence, $m^{\prime}\in M_{j}$.

We have just proved that ${\mathcal{M}}_{j+1}$ has strictly one less hole than
${\mathcal{M}}_{j}$, for all $j\geq\alpha$. It implies that if
${\mathcal{M}}_{\alpha}$ has $k$ holes, then ${\mathcal{M}}_{\alpha+k}$ has no
holes, and the algorithm terminates, contradiction.

We now bound the number of iterations of the while-loop before termination. We
only give the main ideas. For all iteration $j$ of the algorithm, we let
$H_{j}$ be the number of holes of ${\mathcal{M}}_{j}$. The following claim is
proved in App. 0.D.7:

Claim. For all $j{<}\alpha$, either $H_{j+1}=H_{j}-1$ and
$\lceil\mathcal{X}_{j}\rceil\trianglelefteq\lceil\mathcal{X}_{j+1}\rceil$, or
$H_{j+1}=H_{j}+|{\mathcal{I}}|-1$ and
$\lceil\mathcal{X}_{j}\rceil\vartriangleleft\lceil\mathcal{X}_{j+1}\rceil$.

Call the first case of the claim a _decrease step_ and the other case an
_increase step_. Thanks to Lemma 12, the maximal number of increase steps is
bounded by $2^{|Q|}$. This allows us to bound the number of decrease steps as
well. A simple calculation detailed in App. 0.D.8 entails that the number of
iterations before termination is bounded by
$2^{|Q|}+k_{0}+(2^{|Q|}+1)(|{\mathcal{I}}|-1)\in
O(k_{0}+|{\mathcal{I}}|.2^{|Q|})$.

The overall time complexity for Comp to terminate is then the number of
iterations bounded by the expression above, multiplied by the time complexity
of each inner-computation of the while-loop, which is dominated by the
complexity of checking ${\mathcal{M}}_{{\sf o},m^{\prime}}$-realizability,
which is polynomial in the number of states of ${\mathcal{M}}_{{\sf
o},m^{\prime}}$ and exponential in the number of states of $A$, by Theorem
2.∎∎

###  0.D.7 Proof of the claim used in Lemma 13

We first start by proving the claim:

Claim At each iteration $j<\alpha$, either $H_{j+1}=H_{j}-1$ and
$\lceil\mathcal{X}_{j}\rceil\trianglelefteq\lceil\mathcal{X}_{j+1}\rceil$, or
$H_{j+1}=H_{j}+|{\mathcal{I}}|-1$ and
$\lceil\mathcal{X}_{j}\rceil\vartriangleleft\lceil\mathcal{X}_{j+1}\rceil$.

###### Proof.

By the monotonicity property, we always have that
$\lceil\mathcal{X}_{j}\rceil\trianglelefteq\lceil\mathcal{X}_{j+1}\rceil$.
Now, suppose that at step $j$ some of the states of ${\mathcal{M}}_{j}$ can be
reused to complete the selected hole, then $H_{j+1}=H_{j}-1$.

Suppose now that at step $j$, a new state has been created, and let $h=(m,{\sf
i})$ be the hole selected for completion. Clearly,
$H_{j+1}=H_{j}+|{\mathcal{I}}|-1$ since adding a new state creates
$|{\mathcal{I}}|$ holes. Since no state could be reused, it implies by Lemma
11 that for all ${\sf o}\in{\mathcal{O}}$ and all $m^{\prime}\in M_{j}$,
$\textsf{Post}^{*}_{A}(R_{m}^{j},{\sf i}{\sf o})\not\subseteq
R_{m^{\prime}}^{j}$. So, in particular, $\textsf{Post}^{*}_{A}(R_{m}^{j},{\sf
i}{\sf o})\not\subseteq X$ for all $X\in\lceil\mathcal{X}_{j}\rceil$. Let
$(m,{\sf i})\mapsto({\sf o},f)$ be the new transition added to
${\mathcal{M}}_{j}$, where $f\not\in M_{j}$. Note that
$R_{f}^{j+1}=\textsf{Post}^{*}_{A}(R_{m}^{j},{\sf i}{\sf o})$. Therefore,
$R_{f}^{j+1}\not\subseteq X$ for all $X\in\lceil\mathcal{X}_{j}\rceil$. Since
$R_{f}^{j+1}\in\mathcal{X}_{j+1}$, there exists
$Y\in\lceil\mathcal{X}_{j+1}\rceil$ such that $R_{f}^{j+1}\subseteq Y$.
Necessarily, $Y\not\in\lceil\mathcal{X}_{j+1}\rceil$, proving that
$\lceil\mathcal{X}_{j}\rceil\neq\lceil\mathcal{X}_{j+1}\rceil$. So,
$\lceil\mathcal{X}_{j}\rceil\vartriangleleft\lceil\mathcal{X}_{j+1}\rceil$.∎∎

###  0.D.8 Proof of the upper-bound given in the proof of Lemma 13

The following proof details the calculation done to bound the number of
iterations, call it $\beta$, of the while-loop before termination.

###### Proof.

Let $j_{1}<j_{2}<\dots<j_{t}\leq\alpha$ be the iterations corresponding to an
increase step. We also let $j_{t+1}=\beta$ and $j_{0}=0$. For all
$0\leq\ell\leq t+1$, let $x_{\ell}$ be the number of holes in the machine
${\mathcal{M}}_{j_{\ell}}$. In particular, $x_{t+1}=0$. Then, we have the
following relation:

$x_{0}=k_{0}\qquad
x_{\ell+1}=x_{\ell}-(j_{\ell+1}-j_{\ell}-1)+|{\mathcal{I}}|-1$

Indeed, in between two increase steps $j_{\ell}$ and $j_{\ell+1}$, there is
$j_{\ell+1}-j_{\ell}-1$ decrease steps and the increase step $j_{\ell+1}$ adds
$|{\mathcal{I}}|-1$ holes.

Clearly, $\beta$ is bounded by the maximal number of increase steps plus the
maximal number of decrease steps. The latter corresponds to

$\sum_{\ell=0}^{t}(j_{\ell+1}-j_{\ell}-1)=\sum_{\ell=0}^{t}(x_{\ell}-x_{\ell+1}+|{\mathcal{I}}|-1)$
$=x_{0}-x_{t+1}+(t+1)(|{\mathcal{I}}|-1)=k_{0}+(t+1)(|{\mathcal{I}}|-1)$

Moreover, $t$ is bounded by $2^{|Q|}$, and therefore

$\beta\leq 2^{|Q|}+k_{0}+(2^{|Q|}+1)(|{\mathcal{I}}|-1)\in
O(k_{0}+|{\mathcal{I}}|.2^{|Q|})$

∎∎

###  0.D.9 Proof of Theorem 3

The proof of this theorem is based on a series of Lemmas proved in App. 0.D.
Let us give an overview of how this appendix is structured:

  1. 1.

App. 0.D.2 formally defines the notions used in algorithm Gen: prefix-tree
acceptor, state merging, and in particular the notions of mergeable classes
and the result of merging them, together with examples. Lemma 8 states
properties about merging.

  2. 2.

Lemma 9 in App. 0.D.3 proves correctness properties about the generalization
phase (algorithm Gen), and provides an analysis of its termination time.

  3. 3.

App. 0.D.6 establishes correctness of the completion phase (Lemma 10). Then,
it provides a complexity analysis when the completion strategy is lazy (Lemmas
11, 12 and 13).

We now have all the ingredients to prove Theorem 3. First, we prove the
correctness part of the statement. Suppose that
$\textsc{SynthSafe}(E,{\mathcal{S}},\sigma_{G},\sigma_{C})$ terminates, then
there are two cases:

  1. 1.

SynthSafe $(E,{\mathcal{S}},\sigma_{G},\sigma_{C})=\textsc{UNREAL}$, then
either Gen $(E,{\mathcal{S}},\sigma_{G})=$ UNREAL, and we get the result by
Lemma 9, or $\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})$ returns some preMealy
machine ${\mathcal{M}}_{0}$ such that ${\mathcal{S}}$ is not
${\mathcal{M}}_{0}$-realizable. This case is impossible: by Lemma 9,
${\mathcal{S}}$ is necessarily ${\mathcal{M}}_{0}$-realizable.

  2. 2.

$\textsc{SynthSafe}(E,{\mathcal{S}},\sigma_{G},\sigma_{C})$ returns a Mealy
machine ${\mathcal{M}}$. Let ${\mathcal{M}}_{0}$ be the preMealy machine
returned by $\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})$. Then by Lemma 9,
${\mathcal{S}}$ is ${\mathcal{M}}_{0}$-realizable and $E\subseteq
L({\mathcal{M}}_{0})$. From Lemma 10 we get that ${\mathcal{S}}$ is
${\mathcal{M}}_{0}$-realizable by ${\mathcal{M}}$. Therefore, $E\subseteq
L({\mathcal{M}})$ and ${\mathcal{S}}$ is realizable by ${\mathcal{M}}$.

We now prove termination in the case of lazy strategies, together with the
complexity. First, $\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})$ always
terminate, in time polynomial in the size of $E$ and exponential in $n$ the
number of states of ${\mathcal{A}}$, according to Lemma 9. If
$\textsc{Gen}(E,{\mathcal{S}},\sigma_{G})\neq UNREAL$, then it outputs a
preMealy machine ${\mathcal{M}}_{0}$ obtained by merging states of PTA(E),
hence it has less states than the size of $E$. From Lemma 13,
$\textsc{Comp}({\mathcal{M}}_{0},{\mathcal{S}},\sigma_{c})$ terminates, in
time polynomial in $|{\mathcal{I}}|$ and the number of holes of
${\mathcal{M}}_{0}$ (which is bounded by $|E|$), and exponential in $n$. This
yields the claimed complexity.

###  0.D.10 Proof of Theorem 4

###### Proof.

We prove that the generalizing phase of SynthLearn is already complete, i.e.,
given a well-chosen set of examples, it already returns ${\mathcal{M}}$. So,
the completion phase immediately returns ${\mathcal{M}}$ as well, as there is
no holes in ${\mathcal{M}}$. The Mealy completeness result for the
generalizing phase is stated in Lemma 14 below. ∎∎

The next result states that any minimal Mealy machine realizing a given
specification can be learnt when given as input a set of examples which
includes a characteristic set of examples of polynomial size in the size of
the machine.

######  Lemma 14.

For all specification ${\mathcal{S}}$ given as a det. safety automaton and all
minimal Mealy machine ${\mathcal{T}}$ realizing ${\mathcal{S}}$, there exists
$E_{\mathcal{T}}\subseteq({\mathcal{I}}{\mathcal{O}})^{*}$ of polynomial size
(in the number of states and transitions of ${\mathcal{T}}$) such that for all
merging strategy $\sigma_{G}$ and all finite set $E$ s.t.
$E_{\mathcal{T}}\subseteq E\subseteq L({\mathcal{T}})$,
$\textsf{GEN}(E,{\mathcal{S}},\sigma_{G})={\mathcal{T}}$.

###### Proof.

We start by defining the characteristic sample and we provide an overview of
the proof. Then, we give more formal details. Let
${\mathcal{T}}=(T,t_{0},\Delta_{\mathcal{T}})$ and for all $t\in T$, let
$s_{t}\in{\mathcal{I}}^{*}$ be a $\preceq_{ll}$-minimal word to reach $t$,
i.e. such that $\textsf{Post}^{*}_{\mathcal{T}}(t_{0},s_{t})=t$. Note that
$s_{t_{0}}=\epsilon$. Since ${\mathcal{T}}$ is minimal, then for any two
states $t,t^{\prime}$ such that $t\neq t^{\prime}$, there exists a unique
$\preceq_{ll}$-minimal word $d_{t,t^{\prime}}\in{\mathcal{I}}^{+}$
distinguishing $t$ and $t^{\prime}$, i.e. such that the sequences of outputs
produced by ${\mathcal{T}}$ from $t$ and $t^{\prime}$ respectively, when
reading $d_{t,t^{\prime}}$, are different. Formally, it means that if
$d_{t,t^{\prime}}={\sf i}_{1}\dots\sf i_{n}$, there exists $1\leq j\leq n$
such that $\textsf{Out}_{\mathcal{T}}(t,{\sf i}_{1}\dots\sf
i_{j})\neq\textsf{Out}_{\mathcal{T}}(t^{\prime},{\sf i}_{1}\dots\sf i_{j})$.
Note that $d_{t,t^{\prime}}=d_{t^{\prime},t}$. Let us now define
$E_{\mathcal{T}}$ (the characteristic sample). For any pair $p=(t,{\sf i})$
such that $\Delta_{\mathcal{T}}(t,{\sf i})$ is defined, let
$e_{p}=f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{t}{\sf i})$ (the notation
$f_{\mathbbm{i}\mathbbm{o}}$ has been defined in App. 0.D.1). In other words,
we have one example per transition of the machine. Now, we also define
examples that prevent some states of the PTA to be merged. For all $t\neq
t^{\prime}\in T$, we define the example
$v_{t,t^{\prime}}=f_{\mathbbm{i}\mathbbm{o}}^{{\mathcal{T}}}(s_{t}d_{t,t^{\prime}})$
and finally let

$E_{\mathcal{T}}=\\{v_{t,t^{\prime}}\mid t,t^{\prime}\in T,t\neq
t^{\prime}\\}\cup\\{e_{p}\mid p\in
T\times{\mathcal{I}},\Delta_{\mathcal{T}}(p)\text{ is defined}\\}$

Let $E$ be a finite set such that $E_{\mathcal{T}}\subseteq E\subseteq
L({\mathcal{T}})$. To prove that
$\textsf{GEN}(E,{\mathcal{S}},\sigma_{G})={\mathcal{T}}$ (up to state
renaming), for any specification ${\mathcal{S}}$ and strategy $\sigma_{G}$, we
prove the following invariant: the equivalence relation $\sim_{e}$ computed at
iteration $e$ of the algorithm is coarser than the equivalence relation
$\sim_{\mathcal{T}}$ which identifies two states of $\textsf{PTA}(E)$, i.e.,
two examples of $E$, whenever they reach the same state in ${\mathcal{T}}$.
Moreover, both equivalence relations coincide when restricted to all examples
$e^{\prime}\preceq e$. To show this result, we prove that a $\sim_{e}$-class
$[e_{1}]$ can be merged with another $\sim_{e}$-class $[e_{2}]$ iff
$e_{1}\sim_{\mathcal{T}}e_{2}$.

We now give the formal proof. In the sequel, we assume that $E$ is prefix-
closed, in the sense that $E={\sf
Prefs}(E)\cap({\mathcal{I}}{\mathcal{O}})^{*}$. This is wlog as the algorithm
first computes the prefix closure of $E$ at line 1. We first prove some useful
claim.

For all $e\in E$, we let $\Phi(e)\in T$ such that
$\textsf{Post}_{\mathcal{T}}^{*}(t_{0},e)=\Phi(e)$. Given $e,e^{\prime}\in E$,
we say that $e$ and $e^{\prime}$ are ${\mathcal{T}}$-equivalent, denoted
$e\sim_{T}e^{\prime}$, if $\Phi(e)=\Phi(e^{\prime})$. The following claim
states that $\sim_{T}$ is a Mealy-congruence for $\textsf{PTA}(E)$ and
quotienting the latter by $\sim_{T}$ yields exactly ${\mathcal{T}}$ (up to
state renaming).

Claim 1 $\sim_{T}$ is a Mealy-congruence for $\textsf{PTA}(E)$ and
${\mathcal{T}}=\textsf{PTA}(E)/_{\sim_{T}}$ (up to state renaming).

We give a few intuitions for proving that claim. The detailed proof can be
found in App. 0.D.11. Since $E\subseteq L({\mathcal{T}})$, it can be proved
that $\Phi(\textsf{Post}_{\textsf{PTA}(E)}(e,{\sf
i}))=\textsf{Post}_{\mathcal{T}}(\Phi(e),{\sf i})$ (if there exists ${\sf
o}\in{\mathcal{O}}$ such that $e{\sf i}{\sf o}\in E$, otherwise
$\textsf{Post}_{\textsf{PTA}(E)}(e,{\sf i})$ is undefined). This entails that
$\sim_{T}$ is a congruence. Similarly, we also get that
$\textsf{Out}_{\textsf{PTA}(E)}(e,{\sf
i})=\textsf{Out}_{\mathcal{T}}(\Phi(e),{\sf i})$ (if defined) which entails
that $\sim_{T}$ is a Mealy-congruence for $\textsf{PTA}(E)$. To show that the
quotient of $\textsf{PTA}(E)$ by $\sim_{T}$ is ${\mathcal{T}}$, we first use
the fact that $E$ contains one example per state of ${\mathcal{T}}$, and so
$\sim_{T}$ has as many equivalence classes as the number of states of
${\mathcal{T}}$. We have already seen that the output produced by a transition
of $\textsf{PTA}(E)/_{\sim_{T}}$ is consistent with the output produced by
${\mathcal{T}}$, when the transition is defined, because $\sim_{T}$ is a
Mealy-congruence. We prove that for all classes of $\sim_{T}$ and all inputs,
the transition of $\textsf{PTA}(E)/_{\sim_{T}}$ is defined, because $E$
contains one example $e_{p}$ per transition of ${\mathcal{T}}$.

Now, let us come back to the proof of the lemma. For all $e\in E$, let
$\sim_{e}$ be the Mealy-congruence computed after iteration $e$ of the loop at
line 1. We prove that $\sim_{T}$ is coarser than any $\sim_{e}$ for all $e$
and $\sim_{T}$ is equal to $\sim_{e}$ if restricted to the
$\preceq_{ll}$-downward closure of $e$. This will be sufficient to conclude
that our algorithm returns ${\mathcal{T}}$ (up to state renaming). Formally,
given $e\in E$, we let $\downarrow
e=\\{e^{\prime}\in({\mathcal{I}}{\mathcal{O}})^{*}\mid
e^{\prime}\preceq_{ll}e\\}$. Note that $\downarrow e\subseteq E$. We prove the
following two invariants, which states that $\sim_{e}$ is always finer than
$\sim_{T}$ and that $\sim_{T}$ and $\sim_{e}$ coincides when restricted to
$\downarrow e$.

  * •

INV 1 For all $e\in E$, $\sim_{e}\sqsubseteq\sim_{T}$.

  * •

INV 2 For all $e$, $\sim_{e}\cap(\downarrow e)^{2}=\sim_{T}\cap(\downarrow
e)^{2}$.

Before proving the invariants, let us show that INV 2 implies the statement of
the lemma. Indeed, let $e^{*}=\text{max}_{\preceq_{ll}}(E)$. Then, $\downarrow
e^{*}=E$, so $\sim_{e^{*}}\cap(\downarrow e^{*})^{2}=\sim_{e^{*}}=\sim_{T}$.
Therefore, the machine returned by the algorithm is
$\textsf{PTA}(E)/_{\sim_{T}}$, so by Claim 1 we get the desired result.

We rely on a useful claim which states that if $\sim$ is finer than
$\sim_{T}$, and $x\sim_{T}y$, then merging the $\sim$-class of $x$ and the
$\sim$-class of $y$ yields an equivalence relation finer than $\sim_{T}$.
Intuitively, it is because $[x]_{\sim}$ and $[y]_{\sim}$ are subsets of the
same $\sim_{T}$-class, and any merge occurring recursively when computing
$\sim^{x,y}$ also preserves this property. The detailed proof can be found in
App. 0.D.11.

Claim 2: for all $x,y\in E$, if $x\sim_{T}y$ and $\sim\sqsubseteq\sim_{T}$,
then $\sim^{x,y}\sqsubseteq\sim_{T}$.

It remains to prove INV 1 and INV 2. We prove them together by induction.

Initialisation The initial step $e=\epsilon$ is simple. Indeed,
$\sim_{\epsilon}=diag_{E}$, so $\sim_{\epsilon}\sqsubseteq\sim_{T}$. Moreover,
$\downarrow\epsilon=\\{\epsilon\\}$, so,
$\sim_{\epsilon}\cap(\downarrow\epsilon)^{2}=\\{(\epsilon,\epsilon)\\}=\sim_{T}\cap(\downarrow\epsilon)^{2}$.

Induction step We now prove that the invariants are preserved after one
iteration. Suppose they are true for $e\in E$ and let us show it is true for
$f\in E$ such that $f$ is the immediate successor of $e$ in $E$ in llex-order.
Let us give some intuitions before the formal details. Intuitively, we prove
that a merge is possible between $[f]_{\sim_{e}}$ and some $[y]_{\sim_{e}}$
such that $y\preceq_{ll}e$, iff $f\sim_{T}y$. To prove the “only if”
direction, we exploit the fact that when $f\not\sim_{T}y$, merging their
$\sim_{e}$-classes would produce a congruence which is not a Mealy congruence,
because $\Phi(f)$ and $\Phi(y)$ can be distinguished by $d_{\Phi(f),\Phi(y)}$.

Let us proceed with the formal proof. We distinguish between two cases,
depending on whether $mergeCand$ at line 1 is empty or not. If it is empty,
then we prove that for all $y\preceq_{ll}e$, $\Phi(y)\neq\Phi(f)$. If it is
non-empty, we prove that any $y\in mergeCand$ satisfies $\Phi(y)=\Phi(f)$.

  * •

CASE 1: $mergeCand=\varnothing$. In this case, there is no merge, therefore
$\sim_{e}=\sim_{f}$. The induction hypothesis immediately gives INV 1. To
prove INV 2, we need to show that for all $x,y\in\downarrow f$, if
$x\sim_{T}y$ then $x\sim_{f}y$, i.e., $x\sim_{e}y$. It is the case by
induction hypothesis whenever $x,y\in\downarrow e$. If $x=y=f$, then it is
true by reflexivity of $\sim_{e}$. The remaining case is $x=f$ and
$y\preceq_{ll}e$. We show that this case is actually impossible, because
$\textsf{Mergeable}(\textsf{PTA}(E),\sim_{e},f,y)$ would hold otherwise (and
hence $mergeCand\neq\varnothing$). So, assume that $\Phi(f)=\Phi(y)$ and let
us prove that $\sim_{e}^{f,y}$ is a Mealy-congruence for $\textsf{PTA}(E)$.

By Claim 2, we have that for all $\alpha\sim_{e}^{f,y}\beta$,
$\Phi(\alpha)=\Phi(\beta)$. Now, suppose that there exist $\alpha{\sf i}{\sf
o}_{1}\in E$ and $\beta{\sf i}{\sf o}_{2}\in E$, then, ${\sf
o}_{1}=\textsf{Out}_{\mathcal{T}}(\Phi(\alpha),{\sf
i})=\textsf{Out}_{\mathcal{T}}(\Phi(\beta),{\sf i})={\sf o}_{2}$ (because
$E\subseteq L({\mathcal{T}})$). It means that $\sim_{e}^{f,y}$ is a Mealy-
congruence for $\textsf{PTA}(E)$, and hence $mergeCand\neq\varnothing$,
contradiction.

  * •

CASE 2: $mergeCand\neq\varnothing$. In that case, there is a merge between $f$
and some $y\preceq_{ll}e$. Therefore $\sim_{f}=\sim_{e}^{f,y}$.

We first prove INV 2. We need to show that for all $\alpha,\beta\preceq_{ll}f$
such that $\alpha\sim_{T}\beta$, we have $\alpha\sim_{f}\beta$. If
$\alpha,\beta\preceq_{ll}e$, then by IH, $\alpha\sim_{e}\beta$ and since
$\sim_{e}\sqsubseteq\sim_{f}$, we get $\alpha\sim_{f}\beta$. If
$\alpha=\beta=f$, then we are done by reflexivity. So, assume that $\alpha=f$
and $\beta\preceq_{ll}e$. We have $f\sim_{T}\beta$ and $y\sim_{T}f$, so
$y\sim_{T}\beta$ and since $y,\beta\preceq_{ll}e$, by induction hypothesis,
$y\sim_{e}\beta$. Now and informally, since $\sim_{f}$ merges the
$\sim_{e}$-class of $f$ and that of $y$ and propagates this merge, we get
$\beta\sim_{f}f\sim_{f}y$. Formally, by definition of $\sim_{e}^{f,y,0}$, we
get that $y\sim_{e}^{f,y,0}\beta$. Moreover, $f\sim_{e}^{f,y,0}y$, therefore
$f\sim_{e}^{f,y,0}\beta$. By Proposition 1, the $U$ is increasing for the
order $\sqsubseteq$, hence, $\sim_{e}^{f,y,0}\sqsubseteq\sim_{f}$ and
therefore $f\sim_{f}\beta$ and we are done proving INV 2.

Let us now prove INV 1. First, if $\Phi(f)=\Phi(y)$, then by Claim 2, we get
that for all $\alpha\sim_{f}\beta$, $\Phi(\alpha)=\Phi(\beta)$, i.e.,
$\alpha\sim_{T}\beta$. This shows $\sim_{f}\sqsubseteq\sim_{T}$ (INV 1). So,
it remains to show that $\Phi(f)=\Phi(y)$. Suppose that $\Phi(f)\neq\Phi(y)$.
We prove that $y\not\in mergeCand$, which is a contradiction, i.e. that
$\sim_{e}^{f,y}$ cannot be a Mealy-congruence for $\textsf{PTA}(E)$. Remind
that $s_{\Phi(y)}$ is the minimal word reaching $\Phi(y)$ in ${\mathcal{T}}$
and $s_{\Phi(f)}$ is the minimal word reaching $\Phi(f)$ in ${\mathcal{T}}$.
Hence $s_{\Phi(y)}\sim_{T}y$ and $s_{\Phi(f)}\sim_{T}f$. Since
$s_{\Phi(f)}\preceq_{ll}y\preceq_{ll}e$ and $s_{\Phi(f)}\preceq_{ll}f$, by INV
2 we get that $s_{\Phi(f}\sim_{f}f$ and $s_{\Phi(y)}\sim_{f}y$. Moreover, by
definition of $\sim_{f}$, $y\sim_{f}y$. Hence,
$s_{\Phi(f)}\sim_{f}s_{\Phi(y)}$. Consider the input word
$d_{\Phi(f),\Phi(y)}$ distinguishing $\Phi(f)$ and $\Phi(y)$ and decompose it
as $d{\sf i}$. By definition of $E$,
$f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(f)}d{\sf i})\in E$ and
$f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(y)}d{\sf i})\in E$ ((the
notation $f_{\mathbbm{i}\mathbbm{o}}$ has been defined in App. 0.D.1)). There
exists ${\sf o}_{1}\neq{\sf o}_{2}\in{\mathcal{O}}$ such that
$f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(f)}d{\sf
i})=f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(f)}d){\sf i}{\sf o}_{1}$
and $f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(y)}d{\sf
i})=f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(y)}d){\sf i}{\sf o}_{2}$.
Since $\sim_{f}$ is a congruence, we get
$f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(f)}d)\sim_{f}f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(y)}d)$
but
$\textsf{Out}_{\textsf{PTA}(E)}(f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(f)}d),{\sf
i})={\sf o}_{1}\neq{\sf
o}_{2}=\textsf{Out}_{\textsf{PTA}(E)}(f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{\Phi(y)}d),{\sf
i})$. This shows that $\sim_{f}$ is not a Mealy-congruence for
$\textsf{PTA}(E)$ and hence $y$ and $f$ cannot be merged. Therefore,
$\Phi(f)=\Phi(y)$ and we are done.

Note that the proof does not rely on any particular specification
${\mathcal{S}}$ nor any merging strategy $\sigma_{G}$. ∎

###  0.D.11 Proofs of the claims in the proof of Lemma 14

#### Proof of Claim 1

First, let us prove that $\sim_{T}$ is a congruence. Let $e\sim_{T}e^{\prime}$
and ${\sf i}\in{\mathcal{I}}$. Suppose that $\Delta_{\textsf{PTA}(E)}(e,{\sf
i})$ and $\Delta_{\textsf{PTA}(E)}(e^{\prime},{\sf i})$ are both defined,
i.e., $e{\sf i}{\sf o}\in E$ and $e^{\prime}{\sf i}{\sf o}^{\prime}\in E$ for
some ${\sf o},{\sf o}^{\prime}\in{\mathcal{O}}$. Then, we get $\Phi(e{\sf
i})=\textsf{Post}_{\mathcal{T}}(\Phi(e),{\sf
i})=\textsf{Post}_{\mathcal{T}}(\Phi(e^{\prime}),{\sf i})=\Phi(e^{\prime}{\sf
i})$. In other words, $e{\sf i}\sim_{T}e^{\prime}{\sf i}$. Let us show that
${\sf o}={\sf o}^{\prime}$. Clearly, ${\sf
o}=\textsf{Out}_{\mathcal{T}}(\Phi(e),{\sf i})$ because
$E=L(\textsf{PTA}(E))\subseteq L({\mathcal{T}})$. Similarly, ${\sf
o}^{\prime}=\textsf{Out}_{\mathcal{T}}(\Phi(e^{\prime}),{\sf i})$. So, ${\sf
o}={\sf o}^{\prime}$ follows since $\Phi(e)=\Phi(e^{\prime})$. Clearly,
$\sim_{T}$ has at most $|T|$ equivalence classes. Since $E$ contains for all
states $t\in T$, an example $s_{t}$ such that $\Phi(s_{t})=t$, it follows that
$\sim_{T}$ has at least $|T|$ equivalence classes. So far, we have proved that
$\sim_{T}$ is a Mealy-congruence for $\textsf{PTA}(E)$ with the same number of
equivalence classes as the number of states of ${\mathcal{T}}$. For $t\in T$,
we let $\Phi^{-1}(t)=\\{e\in E\mid\Phi(e)=t\\}$. Note that $\Phi^{-1}(t)=[e]$
for some representative $e\in E$. We finally show that ${\mathcal{T}}$ and
$\textsf{PTA}(E)/_{\sim_{T}}$ are equal, up to the state renamping
$\Phi^{-1}$. First, the initial state of ${\mathcal{T}}$ maps to $[\epsilon]$,
which is the initial state of $\textsf{PTA}(E)/_{\sim_{T}}$. Let us show that
$\Phi^{-1}$ preserves the transitions of ${\mathcal{T}}$. Let $t,{\sf i},{\sf
o},t^{\prime}$ such that $\Delta_{\mathcal{T}}(t,{\sf i})=({\sf
o},t^{\prime})$. We show that
$\Delta_{\textsf{PTA}(E)/_{\sim_{T}}}(\Phi^{-1}(t),{\sf i})=({\sf
o},\Phi^{-1}(t^{\prime}))$. First, $s_{t}\in\Phi^{-1}(t)$ since
$\Phi(s_{t})=t$. Moreover, by definition of $E$, $e_{t,{\sf
i}}=f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{t}{\sf
i})=f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{t}){\sf i}{\sf o}\in E$, so
$\Delta_{\textsf{PTA}(E)}(f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{t}),{\sf
i})=({\sf o},f_{\mathbbm{i}\mathbbm{o}}^{\mathcal{T}}(s_{t}{\sf i}))$.
Moreover, $\Phi(s_{t}{\sf i})=t^{\prime}$. This concludes that
$\Delta_{\textsf{PTA}(E)/_{\sim_{T}}}(\Phi^{-1}(t),{\sf i})=({\sf
o},\Phi^{-1}(t^{\prime}))$. The converse is a consequence of $\sim_{T}$ being
a Mealy-congruence for $\textsf{PTA}(E)$ and the fact that all outputs picked
by $\textsf{PTA}(E)$ are consistent with ${\mathcal{T}}$, i.e.,
$L(\textsf{PTA}(E))=E\subseteq L({\mathcal{T}})$. End of proof of Claim 1.∎

#### Proof of Claim 2

By definition of $\sim^{x,y}$, there exist some non-congruent points
$p_{1},\dots,p_{n}\in E\times E\times{\mathcal{I}}$ such that

$\sim^{x,y}=U(U(\dots(U(\sim^{x,y,0},p_{1}),\dots),p_{n-1}),p_{n})$

Let $\sim^{0}=\sim^{x,y,0}$ and $\sim^{j}=U(\sim^{j-1},p_{j})$ for $1\leq
j\leq n$. We prove by induction on $j$ that $\sim^{j}\sqsubseteq\sim_{T}$.

At rank $j=0$, $\alpha\sim^{0}\beta$ means that either $(i)$ $\alpha\sim\beta$
or, $(ii)$ $\alpha\sim x$ and $\beta\sim y$, or $(iii)$ $\beta\sim x$ and
$\alpha\sim y$. In case $(i)$, by hypothesis, $\sim\sqsubseteq\sim_{T}$ so we
are done. In case $(ii)$, by assumption, $x\sim_{T}y$ and as
$\sim\sqsubseteq\sim_{T}$, $\alpha\sim_{T}x$ and $y\sim_{T}\beta$. So,
$\alpha\sim_{T}\beta$. Case $(iii)$ is symmetrical to $(ii)$.

At rank $j>0$, if $p_{j}=(z_{1},z_{2},{\sf i})$, then $\alpha\sim^{j}\beta$
means that either $(i)$ $\alpha\sim^{j-1}\beta$, or $(ii)$
$\alpha\sim^{j-1}\textsf{Post}_{\textsf{PTA}(E)}(z_{1},{\sf i})$ and
$\beta\sim^{j-1}\textsf{Post}_{\textsf{PTA}(E)}(z_{2},{\sf i})$, or $(iii)$
symmetric of $(ii)$ by swapping $\alpha$ and $\beta$. In case $(i)$, we get
the statement by IH. In case $(ii)$, by IH, we get
$\Phi(\alpha)=\Phi(\textsf{Post}_{\textsf{PTA}(E)}(z_{1},{\sf i}))$, and
$\Phi(\beta)=\Phi(\textsf{Post}_{\textsf{PTA}(E)}(z_{2},{\sf i}))$. By
definition of a non-congruent point, we also have $z_{1}\sim^{j-1}z_{2}$, so,
$\Phi(z_{1})=\Phi(z_{2})$. Now,
$\Phi(\textsf{Post}_{\textsf{PTA}(E)}(z_{1},{\sf
i}))=\textsf{Post}_{\mathcal{T}}(\Phi(z_{1}),{\sf
i})=\textsf{Post}_{\mathcal{T}}(\Phi(z_{2}),{\sf
i}^{\prime})=\Phi(\textsf{Post}_{\textsf{PTA}(E)}(z_{2},{\sf i}))$ from which
we get $\Phi(\alpha)=\Phi(\beta)$. Case $(iii)$ is symmetrical to $(ii)$. End
of Proof of Claim 2. ∎

##  Appendix 0.E Details and results of Section 4

###  0.E.1 Optimizing ${\mathcal{P}}$-realizability checking for
specifications $\mathcal{D}({\mathcal{A}},k)$

.

As said in the main body of the paper, a direct application of Theorem 2 on
$\mathcal{D}({\mathcal{A}},k)$ to check its ${\mathcal{P}}$-realizability
would yield a doubly exponential upper-bound. We prove instead that one
exponential can be saved by exploiting the structure of
$\mathcal{D}({\mathcal{A}},k)$, as summarized by the following theorem:

######  Theorem 8.

Given a universal co-Büchi automaton ${\mathcal{A}}$ with $n$ states and
$k\in\mathbb{N}$ defining a safety specification
$S=L_{k}^{\forall}({\mathcal{A}})=L(\mathcal{D}({\mathcal{A}},k))$ and a
preMealy machine ${\mathcal{P}}$ with $m$ states and $n_{h}$ holes, deciding
whether ${\mathcal{S}}$ is ${\mathcal{P}}$-realizable is ExpTime-Complete.

In this theorem, $k$ is assumed to be given in binary. To establish the upper
bound, we exploit the fact that the set of states of
$\mathcal{D}({\mathcal{A}},k)$ forms a complete lattice with several
interesting properties.

######  Definition 3 (Lattice of counting functions).

For all co-Büchi automata ${\mathcal{A}}$ and $k\in\mathbb{N}$, let
$\preceq\subseteq CF({\mathcal{A}},k)\times CF({\mathcal{A}},k)$ be defined by
$f_{1}\preceq f_{2}$ if and only if $f_{1}(q)\leq f_{2}(q)$ for all $q\in Q$.
The set $(CF({\mathcal{A}},k),\preceq)$ forms a complete lattice with minimal
elements $\overline{-1}=\langle-1,-1,\dots,-1\rangle$, which denotes the
function that assigns value $-1$ to each state $q\in Q$, and with least upper
bound operator $\sqcup$ defined as: $f_{1}\sqcup f_{2}=f$ such that
$f(q)=\max(f_{1}(q),f_{2}(q))$ for all $q\in Q$. This upper bound operator
generalizes to any finite set of counting functions
$\mathcal{F}=\\{f_{1},f_{2},\dots,f_{n}\\}\subseteq CF({\mathcal{A}},k)$, and
the least upper bound of $\mathcal{F}$ is denoted $\bigsqcup\mathcal{F}$.

The essence of the structure in $\mathcal{D}({\mathcal{A}},k)$ is captured in
the following series of results.

######  Lemma 15.

For all co-Büchi automata ${\mathcal{A}}$, for all $k\in\mathbb{N}$, for all
counting functions $f_{1},f_{2}\in CF({\mathcal{A}},k)$, such that
$f_{1}\preceq f_{2}$, we have that
$L(\mathcal{D}({\mathcal{A}},k)[f_{2}])\subseteq
L(\mathcal{D}({\mathcal{A}},k)[f_{1}])$, and thus if
$L(\mathcal{D}({\mathcal{A}},k)[f_{2}])$ is realizable then
$L(\mathcal{D}({\mathcal{A}},k)[f_{1}])$ is realizable.

###### Proof.

As counting functions record the number of visits to accepting states so far,
starting from $f_{2}$ is more constraining than from $f_{1}$. So any word
accepted from $f_{2}$ is accepted from $f_{1}$.∎∎

######  Lemma 16 ([20]).

For all co-Büchi automata ${\mathcal{A}}$, for all $k\in\mathbb{N}$, for all
counting functions $f\in CF({\mathcal{A}},k)$, it is ExpTime-Complete to
decide if $L^{\forall}_{k}({\mathcal{A}}[f])$ is realizable.

######  Corollary 1.

For all co-Büchi automata ${\mathcal{A}}$, for all $k\in\mathbb{N}$, the set
of counting functions $W^{{\mathcal{A}}}_{k}=\\{f\in CF({\mathcal{A}},k)\mid
L(\mathcal{D}({\mathcal{A}},k)[f])\mbox{~{}is~{}realizable~{}}\\}$ is
$\preceq$-downward closed and can be represented by the $\preceq$-antichain
$\lceil W^{{\mathcal{A}}}_{k}\rceil$ of maximal elements in
$W^{{\mathcal{A}}}_{k}$. This set of maximal elements can be computed in
exponential time in the size of ${\mathcal{A}}$ and the binary encoding of
$k$.

We now formulate a lemma that will be instrumental, later in this section, to
improve the upper bound of the algorithm that solves the
${\mathcal{P}}$-realizability problem for universal coBüchi specifications.

######  Lemma 17.

For all co-Büchi automata ${\mathcal{A}}$, for all $k\in\mathbb{N}$, for all
sets of counting functions $\mathcal{F}=\\{f_{1},f_{2},\dots,f_{n}\\}\subseteq
CF({\mathcal{A}},k)$:

$L(\mathcal{D}({\mathcal{A}},k)[\bigsqcup\mathcal{F}]=\bigcap_{f\in\mathcal{F}}L(\mathcal{D}({\mathcal{A}},k)[f]).$

###### Proof.

As $CF({\mathcal{A}},k)$ is finite, it is sufficient to prove that for all
$f_{1},f_{2}\in CF({\mathcal{A}},k)$, we have
$L(\mathcal{D}({\mathcal{A}},k)[f_{1}\sqcup
f_{2}]=L(\mathcal{D}({\mathcal{A}},k)[f_{1}])\cap
L(\mathcal{D}({\mathcal{A}},k)[f_{1}]).$ To establish this property, let us
consider a word $w\in({\mathcal{I}}{\mathcal{O}})^{\omega}$ and the runs on
$w$ from $f_{1}$, $f_{2}$ and $f_{1}\sqcup f_{2}$. We denote those runs by
$r_{1}$, $r_{2}$, and $r_{1,2}$, respectively. Let $r_{1}=g_{0}g_{1}\dots
g_{n}\dots$ with $g_{0}=f_{1}$, $r_{2}=h_{0}h_{1}\dots h_{n}\dots$ with
$h_{0}=f_{2}$, and $r_{1,2}=l_{0}l_{1}\dots l_{n}\dots$ with
$l_{0}=f_{1}\sqcup f_{2}$. It is easy to show by induction, using the
definition of $\delta^{\mathcal{D}}$, that for all positions $i\geq 0$, for
all $q\in{\mathcal{A}}$, we have that $l_{i}(q)=\max(g_{i}(q),h_{i}(q))$ and
so $l_{i}=f_{i}\sqcup g_{i}$. Then clearly, we have that $r_{1,2}$ is
accepting if and only if both $r_{1}$ and $r_{2}$ are accepting. This is
because, for $l=f\sqcup g$, we have for $q\in Q$: $l(q)=k+1$ iff $f(q)=k+1$ or
$g(q)=k+1$.∎∎

#### Proof of Theorem 8

We are now ready to provide a proof to the statement. Given a preMealy
${\mathcal{P}}=(M,m_{0},\Delta)$, co-Büchi automata ${\mathcal{A}}=(Q,q_{{\sf
init}},\Sigma,\delta,d)$, $k\in\mathbb{N}$, we can compute according to
corollary 1 the $\preceq$-antichain $\lceil
W^{{\mathcal{A}}}_{k}\rceil\subseteq CF({\mathcal{A}},k)$ in exponential time.
Then to decide if ${\mathcal{P}}$ can be completed into a (full) Mealy machine
that realizes $L(\mathcal{D}({\mathcal{A}},k))$, we construct a labelling of
states of ${\mathcal{P}}$ defined by the function $F^{*}:M\rightarrow
CF({\mathcal{A}},k)$, for all $m\in M$, by

$F^{*}(m)=\bigsqcup\\{f\mid\exists
u\in({\mathcal{I}}{\mathcal{O}})^{*}\cdot\textsf{Post}_{{\mathcal{P}}}^{*}(m_{0},u)=m\land\delta^{\mathcal{D}}(f_{0},u)=f\\}$

Our goal is now to show that $F^{*}$ can be computed in polynomial time. To do
so, we first define the following sequence of functions $(F_{j}:M\rightarrow
CF({\mathcal{A}},k))_{j\in\mathbb{N}}$:

  * •

for all states $m\in M$ of ${\mathcal{P}}$, let $F_{0}(m)=f_{0}$ if $m=m_{0}$,
and $F_{0}(m)=\overline{-1}$ otherwise.

  * •

for $j>0$, for all states $m\in M$ of ${\mathcal{P}}$, let
$F_{j}(m)=\bigsqcup_{(m_{1},{\sf i},{\sf o},m)\mid\Delta(m_{1},{\sf i})=({\sf
o},m)}\delta^{\mathcal{D}}(F_{j-1}(m_{1}),({\sf i},{\sf o}))$, where
$\delta^{\mathcal{D}}$ is the transition function of
$\mathcal{D}({\mathcal{A}},k)$.

The following lemma formalizes properties of this sequence of functions.

######  Lemma 18.

The sequence $(F_{j}:M\rightarrow CF({\mathcal{A}},k))_{j\in\mathbb{N}}$
satisfies:

  1. 1.

The sequence stabilizes after at most $|M|\times|Q|\times(k+1)$ steps. We note
$G^{*}$ the function on which the sequence $(F_{j})_{j\in\mathbb{N}}$
stabilizes.

  2. 2.

Each iteration is computable in time bounded by ${\bf O}(|M|^{2}\times|Q|)$.

  3. 3.

For all $m\in M$, $F^{*}=G^{*}$.

Thus, there is a polynomial time algorithm in $|{\mathcal{P}}|$,
$|{\mathcal{A}}|$, $k\in\mathbb{N}$, and the size of $\lceil
W^{{\mathcal{A}}}_{k}\rceil$ to check the ${\mathcal{P}}$-realizability of
$L^{\forall}({\mathcal{A}})$.

###### Proof.

For point $(1)$, we first note that for all state $m$ of ${\mathcal{M}}$ the
sequence of counting function $(F_{j}(\cdot))_{j\in\mathbb{N}}$ stabilizes
after $|{\mathcal{M}}|\times|Q|\times(k+1)$. Indeed, for all $j\geq 0$, and
for all $m\in M$, we have that $F_{j}(m)\preceq F_{j+1}(m)$. As chains in the
lattice of counting function $CF({\mathcal{A}},k)$ has length at most
$|Q|\times(k+1)$, each $m$ can be updated at most this number of times. The
total number of iterations before stabilization of the $|M|$ state labels
defined by the $F_{j}$ is thus at most $|M|\times|Q|\times(k+1)$.

For point $(2)$, we note that the counting function $F_{j}(m)$ is computed as
the least upper bound applied of at most $|M|$ counting functions obtained by
applying the transition function of $\mathcal{D}({\mathcal{A}},k)$ on counting
functions defined by $F_{j-1}$. It is important to note that we de not need to
construct the entire automaton $\mathcal{D}({\mathcal{A}},k)$ for this purpose
as we can compute transitions on-demand based according to Definition 1(3). So
the complexity is bounded by ${\bf O}(|M|\times|Q|)$ for updating one state
$m$ and thus the overall complexity of one update of all the states is bounded
by ${\bf O}(|M|^{2}\times|Q|)$.

For $(3)$ we reason by induction, using the definition of $\Delta$ and
$\delta^{\mathcal{D}}$, to prove for all $j\geq 0$ and $m{\in}M$:

$F_{j}(m)=\bigsqcup\\{f\mid 0\leq i\leq j\land\exists
u\in({\mathcal{I}}{\mathcal{O}})^{i}\cdot\textsf{Post}^{*}(m_{0},u)=m\land\delta^{\mathcal{D}}(f_{0},u)=f\\}.$

∎∎

We now show that $L(\mathcal{D}({\mathcal{A}},k))$ is
${\mathcal{P}}$-realizable if and only if there does not exist $m\in M$ such
that $F^{*}(m)\not\in W^{{\mathcal{A}}}_{k}$. Following the proof of Theorem
1, we know that $L(\mathcal{D}({\mathcal{A}},k))$ is
${\mathcal{P}}$-realizable iff, $L_{\omega}({\mathcal{P}})\subseteq
L(\mathcal{D}({\mathcal{A}},k))$ and for every hole $h=(p,{\sf i})$ of
${\mathcal{P}}$, there exists ${\sf o}_{h}\in{\mathcal{O}}$ and a Mealy
machine ${\mathcal{M}}_{h}$ such that for all $u\in\textsf{Left}_{p}$,
${\mathcal{M}}_{h}$ realizes $(u{\sf i}{\sf
o}_{h})^{-1}L(\mathcal{D}({\mathcal{A}},k))$.

First, checking whether $L_{\omega}({\mathcal{P}})\subseteq
L(\mathcal{D}({\mathcal{A}},k))$ can be done by verifying that
$F^{*}(m)(q)\not=k+1$ for all $m\in M$. Second, checking the existence of
${\mathcal{M}}_{h}$ is equivalent to check that $\bigcap_{u{\sf
i}\in\textsf{Left}_{p}}(u{\sf i})^{-1}L(\mathcal{D}({\mathcal{A}},k))$ is
realizable. In turn, this is equivalent, by Lemma 17 and point $(3)$, to check
that $L(\mathcal{D}({\mathcal{A}},k)[F^{*}(p)])$ is realizable, which is
equivalent to check if $F^{*}(p)\in W^{{\mathcal{A}}}_{k}$. Both tests can be
done in polynomial time in the size of ${\mathcal{A}}$ and in the size of
$\lceil W^{{\mathcal{A}}}_{k}\rceil$.

We have established that given a preMealy ${\mathcal{P}}$, co-Büchi automata
${\mathcal{A}}$, $k\in\mathbb{N}$, and the $\preceq$-antichain $\lceil
W^{{\mathcal{A}}}_{k}\rceil$, we can compute the sequence of functions
$(F_{j}:M\rightarrow CF({\mathcal{A}},k))_{j\in\mathbb{N}}$ in polynomial time
in the size of those inputs, and thus decide (by point $(4))$ if the
specification $L(\mathcal{D}({\mathcal{A}},k))$ is ${\mathcal{P}}$-realizable.
According to Corollary 1, the antichain $\lceil W^{{\mathcal{A}}}_{k}\rceil$
can be computed in exptime in the size of ${\mathcal{A}}$ and the encoding of
$k$. We have thus established the upper-bound of Theorem 8. The lower bound is
a direct consequence of Theorem 2 which establishes the lower bound for any
specification given as a universal coBüchi automaton ${\mathcal{A}}$, and
Theorem 5 which reduces the ${\mathcal{P}}$-realizability of
$L^{\forall}({\mathcal{A}})$ to the ${\mathcal{P}}$-realizability of
$L_{k}^{\forall}({\mathcal{A}})$ for a $k$ which is exponential in the number
of states of ${\mathcal{A}}$. Since $k$ is in binary, its size remains
polynomial, so the reduction is polynomial. This ends the proof of Theorem 8.
∎