Logics for Word Transductions with Synthesis

TL;DR

This paper introduces LT, a logic for expressing properties of transductions with a focus on synthesis, showing that any LT-definable transduction can be realized by a regular functional transduction, bridging logic and automata.

Contribution

The paper presents a new logic LT for transductions, proves its expressive power and decidability, and establishes a synthesis method linking LT-definable transductions to regular functions.

Findings

LT can express all regular functional transductions.

Decidable satisfiability and equivalence for LT with specific complexities.

Any LT-definable transduction can be synthesized into a regular functional transduction.

Abstract

We introduce a logic, called LT, to express properties of transductions, i.e. binary relations from input to output (finite) words. In LT, the input/output dependencies are modelled via an origin function which associates to any position of the output word, the input position from which it originates. LT is well-suited to express relations (which are not necessarily functional), and can express all regular functional transductions, i.e. transductions definable for instance by deterministic two-way transducers. Despite its high expressive power, LT has decidable satisfiability and equivalence problems, with tight non-elementary and elementary complexities, depending on specific representation of LT-formulas. Our main contribution is a synthesis result: from any transduction R defined in LT , it is possible to synthesise a regular functional transduction f such that for all input words u in the domain of R, f is defined and (u,f(u)) belongs to R. As a consequence, we obtain that any functional transduction is regular iff it is LT-definable. We also investigate the algorithmic and expressiveness properties of several extensions of LT, and explicit a correspondence between transductions and data words. As a side-result, we obtain a new decidable logic for data words.

Equations

$$\begin{array}[]{ll}\exists^{\texttt{out}}y\ (y<_{\texttt{out}}x\wedge\{\texttt{o}(x){=}\texttt{o}(y)\}\wedge C_{i}(y))\wedge\big{(}\forall y\ (y<x\wedge&\\ \{\texttt{o}(x){=}\texttt{o}(y)\})\to\neg(\exists^{\texttt{out}}x\ (x<_{\texttt{out}}y\wedge\{\texttt{o}(x){=}\texttt{o}(y)\}\wedge C_{i}(x))\big{)}&\\ \end{array}$$

$$\begin{array}[]{lll}\forall^{\texttt{out}}x,y\\ \ \big{(}\{\phi^{c_{i},d_{j}}_{\leq}(\texttt{o}(x),\texttt{o}(y))\wedge\phi_{c_{1},\dots,c_{l},v}(\texttt{o}(x))\wedge\phi_{d_{1},\dots,d_{l},w}(\texttt{o}(y))\}\\ \ \wedge C_{i}(x)\wedge C_{j}(y)\big{)}\rightarrow\left(x\leq_{\texttt{out}}y\wedge v(i)(x)\wedge w(j)(y)\right)\end{array}$$

$${\forall }^{\text{out}}x,y\psi (x,y)\wedge \underset{i=1}{\overset{m}{\bigwedge }}{\forall }^{\text{out}}x{\exists }^{\text{out}}y{\psi }_i(x,y)$$

$${\varphi }_{\text{cut}}(x)\equiv {\forall }^{\text{out}}y\cdot S_{\text{out}}(y,x)\to A_1(x)\wedge A_2(y)$$

$$\text{Lbag}\varphi {\text{Rbag}}_0(x)\equiv \varphi (x)\text{Lbag}\varphi {\text{Rbag}}_j(x)\equiv {\exists }^{\text{out}}y\cdot S_{\text{out}}(x,y)\wedge \text{Lbag}\varphi {\text{Rbag}}_{j-1}(y)$$

$$\begin{array}[]{lllllll}\phi_{u_{i},v_{i}}(x)&\equiv&\bigwedge_{j=1}^{|u_{i}|}\Lbag(u_{i}(j),1)(x)\Rbag_{j{-}1}(x)\\ &&\wedge\bigwedge_{j=1}^{|v_{i}|}\Lbag(v_{i}(j),2)(x)\Rbag_{j{-}1+|u_{i}|}(x)\\ &&\wedge\Lbag\phi_{\text{cut}}(x)\vee\text{max}_{\texttt{out}}(x)\Rbag_{|u_{i}|+|v_{i}|-1}(x)\end{array}$$

$${\varphi }_{\text{well-formed}}\equiv {\forall }^{\text{out}}x\cdot ({\varphi }_{\text{cut}}(x)\to \underset{i=1}{\overset{n}{\bigvee }}{\varphi }_{u_i,v_i}(x))$$

$$\begin{array}[]{rllllllllll}\phi_{\text{bij},\ell}&\equiv&\forall^{\texttt{in}}x\exists^{\texttt{out}}y\ A_{\ell}(y)\wedge\texttt{o}(y)=x\\ &&\!\!\!\!\wedge\forall^{\texttt{out}}x,y\ (\texttt{o}(x)=\texttt{o}(y)\wedge A_{\ell}(x)\wedge A_{\ell}(y))\\ &&\qquad\qquad\rightarrow x=y\\ \phi_{\text{ord-pres},\ell}&\equiv&\forall^{\texttt{out}}x,y\ (\texttt{o}(x)<_{\texttt{in}}\texttt{o}(y)\wedge A_{\ell}(x)\wedge A_{\ell}(y))\\ &&\qquad\qquad\rightarrow x<_{\texttt{out}}y\\ \phi_{\text{lab-pres},\ell}&\equiv&\forall^{\texttt{out}}x\bigwedge_{a\in A}(a,\ell)(x)\rightarrow a(\texttt{o}(x)))\end{array}$$

$$\varphi \equiv {\varphi }_{\text{well-formed}}\wedge \underset{\ell =1}{\overset{2}{\bigwedge }}{\varphi }_{\text{bij},\ell }\wedge {\varphi }_{\text{ord-pres},\ell }\wedge {\varphi }_{\text{lab-pres},\ell }$$

$${\varphi }_P(x)=\underset{c\in P}{\bigwedge }{\varphi }_{pos}^c(x)\underset{c\notin P}{\bigwedge }\neg {\varphi }_{pos}^c(x)$$

$${\varphi }_{c_1,\dots ,c_l}(x)={\varphi }_{\left\{c_1,\dots ,c_l\right\}}(x)\underset{1\le i\le j\le l}{\bigwedge }({\varphi }_{\le }^{c_i,c_j}(x,x))$$

$${\varphi }_{c_1,\dots ,c_l,v}(x)={\varphi }_{c_1,\dots ,c_l}(x)\underset{i\le l}{\bigwedge }{\varphi }_{v(i)}^{c_i}(x)$$

$${\varphi }_{c_1,\dots ,c_l,v,d_1,\dots ,d_m,w}(x,y)={\varphi }_{c_1,\dots ,c_l,v}(x)\wedge {\varphi }_{d_1,\dots ,d_m,w}(y)$$

$$C_1(x)=\text{out}(x)\wedge {\forall }^{\text{out}}yy{<}_{\text{out}}x\to \{\text{o}(x)\ne \text{o}(y)\}$$

$$\begin{array}[]{ll}C_{i+1}(x)=&\exists^{\texttt{out}}y\ (y<_{\texttt{out}}x\wedge\{\texttt{o}(x)=\texttt{o}(y)\}\wedge C_{i}(y))\\ &\wedge\forall^{\texttt{out}}y\ (y<_{\texttt{out}}x\wedge\{\texttt{o}(x)=\texttt{o}(y)\}\wedge C_{i}(y))\\ &\ \rightarrow\neg\exists^{\texttt{out}}x\ (x<_{\texttt{out}}y\wedge\{\texttt{o}(x)=\texttt{o}(y)\}\wedge C_{i}(x))\end{array}$$

$$\begin{array}[]{l}\{\phi_{dom}\}\wedge\forall^{\texttt{out}}x\ \neg C_{k+1}(x)\wedge\forall^{\texttt{in}}x\ \{\phi_{\varnothing}(x)\}\rightarrow(\forall^{\texttt{out}}y\ \{\texttt{o}(y)\neq x\})\\ \wedge\forall^{\texttt{out}}x,y\ \bigwedge_{m,l\leq k,c_{1},\dots,c_{l},v\in\Gamma^{l},d_{1},\dots,d_{m},w\in\Gamma^{m},i\leq l,j\leq m}\\ \qquad\qquad\quad\big{(}C_{i}(x)\wedge C_{j}(y)\wedge\\ \qquad\qquad\quad\{\phi^{c_{i},d_{j}}_{\leq}\}(\texttt{o}(x),\texttt{o}(y))\wedge\\ \qquad\qquad\quad\{\phi_{c_{1},\dots,c_{l},v,d_{1},\dots,d_{l},w}\}(\texttt{o}(x),\texttt{o}(y))\big{)}\\ \qquad\qquad\rightarrow\left(x\leq_{\texttt{out}}y\wedge v(i)(x)\wedge w(j)(y)\right)\\ \end{array}$$

$${\varphi }^{<♯}\wedge {\varphi }_{\text{id}}^{>♯}\wedge {\exists }^{\text{out}}x♯(x)\wedge {\text{min}}_{\text{in}}(\text{o}(x))\wedge {\forall }^{\text{out}}y♯(y)\to x=y$$

$$P_{i+1}=\{p\mid p\text{ is a position of w and }(w,p)\models {\xi }_i(x)\}.$$

$${\forall }^{\text{out}}x\underset{j=1}{\overset{k}{\bigwedge }}({\gamma }_j(x)\to {\exists }^{\text{out}}y\underset{\ell =1}{\overset{m}{\bigvee }}{t}_{j,\ell })$$

$$\pi =(\gamma ,R_1,\to )\dots (\gamma ,R_i,\to )(\gamma ,\cdot )(\gamma ,R_{i+1},\leftarrow )\dots (\gamma ,R_{i+k},\leftarrow )$$

$$(\gamma ,R_1,\to )\dots (\gamma ,R_{\text{o}(j)-1},\to )(\gamma ,\cdot )(\gamma ,R_{\text{o}(j)+1},\leftarrow )\cdots (\gamma ,R_n,\leftarrow )$$

$$\begin{array}[]{l|ccccccccccccccccc}&\lambda^{f}_{1}&&\lambda^{f}_{2}&&\ldots&&\lambda^{f}_{n}\\ \hline\cr\text{input symbol}&\sigma_{1}&&\sigma_{2}&&\ldots&&\sigma_{n}\\ \hline\cr\text{$S$-component}&S_{1}&&S_{2}&&\ldots&&S_{n}\\ \hline\cr trace(|v|)&B_{|v|}^{1}&\xrightarrow{S}&B_{|v|}^{2}&\xrightarrow{S}&\ldots&\xrightarrow{S}&B_{|v|}^{n}\\ trace(|v|-1)&B_{|v|-1}^{1}&\xrightarrow{S}&B_{|v|-1}^{2}&\xrightarrow{S}&\ldots&\xrightarrow{S}&B_{|v|-1}^{n}\\ \vdots&\vdots&\vdots&\vdots&\vdots&\vdots&\vdots&\vdots\\ trace(1)&B_{1}^{1}&\xrightarrow{S}&B_{1}^{2}&\xrightarrow{S}&\ldots&\xrightarrow{S}&B_{1}^{n}\\ \end{array}$$

$$\forall x\{\sigma (x^{\prime })\}(x)\to \exists y\{y^{\prime }{\le }_{\text{in}}{x}^{\prime }\}(\text{o}(y),x)$$

$$\begin{array}[]{ccc}\forall^{\texttt{in}}x\ \{\sigma(x^{\prime})\}(x)&\rightarrow&\exists^{\texttt{in}}y\ \{y^{\prime}\mathrel{\leq_{\texttt{in}}}x^{\prime}\}(\texttt{o}(y),x)\\ &&\vee\\ &&\exists^{\texttt{out}}y\ \{y^{\prime}\mathrel{\leq_{\texttt{in}}}x^{\prime}\}(\texttt{o}(y),x)\\ &\wedge&\\ \forall^{\texttt{out}}x\ \{\sigma(x^{\prime})\}(x)&\rightarrow&\exists^{\texttt{in}}y\ \{y^{\prime}\mathrel{\leq_{\texttt{in}}}x^{\prime}\}(\texttt{o}(y),x)\\ &&\vee\\ &&\exists^{\texttt{out}}y\ \{y^{\prime}\mathrel{\leq_{\texttt{in}}}x^{\prime}\}(\texttt{o}(y),x)\\ \end{array}$$

$$\begin{array}[]{ccc}\forall^{\texttt{in}}x\ \{\sigma(x^{\prime})\}(x)&\rightarrow&\exists^{\texttt{in}}y\ \bot\\ &&\vee\\ &&\exists^{\texttt{out}}y\ \{y^{\prime}\mathrel{\leq_{\texttt{in}}}x^{\prime}\}(\texttt{o}(y),x)\\ &\wedge&\\ \forall^{\texttt{out}}x\ \bot&\rightarrow&\exists^{\texttt{in}}y\ \bot\\ &&\vee\\ &&\exists^{\texttt{out}}y\ \{y^{\prime}\mathrel{\leq_{\texttt{in}}}x^{\prime}\}(\texttt{o}(y),x)\\ \end{array}$$

$${\forall }^{\text{in}}x\{\sigma (x^{\prime })\}(x)\to {\exists }^{\text{out}}y\{y^{\prime }{\le }_{\text{in}}{x}^{\prime }\}(\text{o}(y),x)$$

$$\forall x\{\sigma (x^{\prime })\}(x)\to \exists y\{y^{\prime }⪯x^{\prime }\}(y,x)$$

$$\begin{array}[]{rl}\text{cont}(X)\equiv\neg\big{(}\exists^{\texttt{out}}x\ x\in X&\wedge(\exists^{\texttt{out}}y\ x<_{\texttt{out}}y\wedge y\notin X\\ &\wedge(\exists^{\texttt{out}}x\ y<_{\texttt{out}}x\wedge x\in X))\big{)}\end{array}$$

$$\begin{array}[]{llll}\psi_{\text{well-formed}}(X)&\equiv&\text{cont}(X)\wedge|X|\leq m\\ &\rightarrow&\bigvee_{w\in F}w(X)\\ &&\wedge\bigvee_{w\in P}\min(X)\wedge|X|=|w|\rightarrow w(X)\\ &&\wedge\bigvee_{w\in S}\max(X)\wedge|X|=|w|\rightarrow w(X)\end{array}$$

$$\begin{array}[]{lcl}\phi_{var}&=&\forall^{\texttt{in}}x\ X^{p}_{q,r}(x)\rightarrow\left(L_{q,r}(x)\bigwedge_{\sigma\in\Sigma}\sigma(x)\rightarrow p.\sigma=q\right)\\ \phi_{succ}&=&\forall^{\texttt{in}}x,y\bigwedge_{p,q,r}\left(S_{\texttt{in}}(x,y)\wedge X^{p}_{q,r}(x)\rightarrow\bigvee_{s,t}X^{r}_{s,t}(x)\right)\\ \phi_{min}&=&\forall^{\texttt{in}}x\ \min(x)\rightarrow\bigvee_{p,q}X^{q_{0}}_{p,q}(x)\\ \phi_{max}&=&\forall^{\texttt{in}}x\ \max(x)\rightarrow\bigvee_{r_{f}\in F,p,q}X^{p}_{q,q_{f}}(x)\\ \end{array}$$

Full text

Despite its high expressive power, $\mathcal{L}_{T}$ has decidable satisfiability and equivalence problems, with tight non-elementary and elementary complexities, depending on specific representation of $\mathcal{L}_{T}$-formulas. Our main contribution is a synthesis result: from any transduction $R$ defined in $\mathcal{L}_{T}$, it is possible to synthesise a regular functional transduction $f$ such that for all input words $u$ in the domain of $R$, $f$ is defined and $(u,f(u))\in R$. As a consequence, we obtain that any functional transduction is regular iff it is $\mathcal{L}_{T}$-definable.

We also investigate the algorithmic and expressiveness properties of several extensions of $\mathcal{L}_{T}$, and explicit a correspondence between transductions and data words. As a side-result, we obtain a new decidable logic for data words.

Transductions, Origin, Logic, Synthesis, Data words

††journalyear: 2018††copyright: acmlicensed††conference: LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science; July 9–12, 2018; Oxford, United Kingdom††booktitle: LICS ’18: LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9–12, 2018, Oxford, United Kingdom††price: 15.00††doi: 10.1145/3209108.3209181††isbn: 978-1-4503-5583-4/18/07††copyright: acmlicensed

1. Introduction

The theory of regular languages of finite and infinite words is rich and robust, founded on the equivalence of a descriptive model (monadic second-order logic, MSO) and a computational one (finite automata), due the works of Büchi, Elgot, McNaughton and Trahtenbrot (Thomas, 1997). Since then, many logics have been designed and studied to describe languages (see for instance (Straubing, 1994; Diekert and Gastin, 2008)), among which temporal logics, with notable applications in model-checking (Vardi and Wolper, 1986).

In this paper, we consider transductions, i.e. binary relations relating input to output words. E.g. the transduction $\tau_{\text{shuffle}}$ associates with a word all its permutations – $(ab,ab),(ab,ba)\in\tau_{\text{shuffle}}$. Operational models, namely extensions of automata with outputs, called transducers, have been studied for computing transductions. This includes finite transducers, i.e. finite automata with outputs, which have been studied since the 60s (Jean Berstel, 1979; Sakarovich, 2009) and two-way transducers (two-way automata with a one-way output tape). When restricted to transducers defining functions (called functional transducers), the latter model has recently received a lot of attention due to its appealing algorithmic properties, its expressive power and its many equivalent models: deterministic two-way transducers (de Souza, 2013), reversible two-way transducers (Dartois et al., 2017), deterministic (one-way) transducers with registers (Alur and Černý, 2010) (also known as streaming string transducers), regular combinator expressions (Alur et al., 2014) and Courcelle’s MSO-transducers (Engelfriet and Hoogeboom, 2001) (MSOT), a model we will come back to in the related work section. Because of these many characterisations, the class defined by these models has been coined regular transductions, or regular functions.

However, much less is known about logics to describe transductions (see for instance (Filiot and Reynier, 2016) for a brief overview). Recently, Bojańczyk, Daviaud, Guillon and Penelle have considered an expressive logic, namely MSO over origin graphs (o-graphs) (Bojańczyk et al., 2017). Such graphs encode pairs of words together with an origin mapping, relating any output position to an input position, as depicted in Fig. 1. Intuitively, if one thinks of an operational model for transductions, the origin of an output position is the input position from which it has been produced.

As noticed in (Bojanczyk, 2014), most known transducer models not only define transductions, but origin transductions (o-transductions), i.e. sets of o-graphs, and can thus be naturally interpreted in both origin-free semantics (i.e. usual semantics) or the richer origin semantics. We denote by $\text{MSO}_{\texttt{o}}$ monadic second-order logic over o-graphs. Precisely, it is MSO equipped with monadic predicates $\sigma(x)$ for position labels, a linear order $\leq_{\texttt{in}}$ (resp. $\leq_{\texttt{out}}$) over input (resp. output) positions, and an origin function o. We denote by $\llbracket\phi\rrbracket_{o}$ the origin-transduction defined by $\phi$, i.e. the set of o-graphs satisfying $\phi$, and by $\llbracket\phi\rrbracket$ the transduction defined by $\phi$ (obtained by projecting away the origin mapping of $\llbracket\phi\rrbracket_{o}$). While (Bojańczyk et al., 2017) was mostly concerned with characterising classes of o-graphs generated by particular classes of transducers, the authors have shown another interesting result, namely the decidability of model-checking regular functions with origin against $\text{MSO}_{\texttt{o}}$ properties: it is decidable, given an $\text{MSO}_{\texttt{o}}$ sentence $\phi$ and a deterministic two-way transducer $T$, whether all $o$-graphs of $T$ satisfy $\phi$.

Satisfiability and synthesis

Important and natural verification-oriented questions are not considered in (Bojańczyk et al., 2017). The first is the satisfiability problem for $\text{MSO}_{\texttt{o}}$: given a sentence $\phi$, is it satisfied by some o-graph? While being one of the most fundamental problem in logic, its decidability would also entail the decidability of the equivalence problem, a fundamental problem in transducer theory: given two sentences $\phi_{1},\phi_{2}$ of $\text{MSO}_{\texttt{o}}$, does $\llbracket\phi_{1}\rrbracket_{o}=\llbracket\phi_{2}\rrbracket_{o}$ hold? The second problem is the regular synthesis problem: given an $\text{MSO}_{\texttt{o}}$-sentence $\phi$, does there exist a deterministic two-way transducer $T$ such that $(1)$ $T$ has the same domain as $\llbracket\phi\rrbracket$ (the set of words which have some image by $\llbracket\phi\rrbracket$) and $(2)$ for all $u$ in the domain of $T$, its image $T(u)$ satisfies $(u,T(u))\in\llbracket\phi\rrbracket$. Note that without requirement $(1)$, any transducer $T$ with empty domain would satisfy $(2)$. So, instead of designing a transducer and then verifying a posteriori that it satisfies some $\text{MSO}_{\texttt{o}}$ properties, the goal is to check whether some transducer can be automatically generated from these properties (and to synthesise it), making it correct by construction. Unsurprisingly, we show that both these problems are undecidable for $\text{MSO}_{\texttt{o}}$.

Contribution: The fragment $\mathcal{L}_{T}$

We define a fragment of $\text{MSO}_{\texttt{o}}$ called $\mathcal{L}_{T}$ for which, amongst other interesting properties, the two problems mentioned before are decidable. Before stating our precise results on $\mathcal{L}_{T}$, let us intuitively define it and provide examples. $\mathcal{L}_{T}$ is the two-variable fragment111Only two variable names can be used (and reused) in a formula, see e.g. (Straubing, 1994) of first-order logic – $\text{FO}^{2}$. The predicates in its signature are the output labels, the linear order $\leq_{\texttt{out}}$ for the output positions, the origin function o, and any binary MSO predicate restricted to input positions, using input label predicates and the input order $\leq_{\texttt{in}}$. We write it $\mathcal{L}_{T}:=\text{FO}^{2}[\Gamma,\mathrel{\leq_{\texttt{out}}},\texttt{o},\text{MSO}_{\text{bin}}[\mathrel{\leq_{\texttt{in}}},\Sigma]]$ where $\Gamma$ is the output alphabet and $\Sigma$ the input alphabet.

As an example, let us define the transduction $\tau_{\text{shuffle}}$ in $\mathcal{L}_{T}$. We express that $(1)$ o preserves the labelling: $\forall^{\texttt{out}}x\bigwedge_{\sigma\in\Gamma}\sigma(x)\rightarrow\{\sigma(\texttt{o}(x))\}$, and $(2)$ o is bijective, i.e. injective: $\forall^{\texttt{out}}x,y\ \{\texttt{o}(x)=\texttt{o}(y)\}\rightarrow x=y$ and surjective: $\forall^{\texttt{in}}x\exists^{\texttt{out}}y\ \{x=\texttt{o}(y)\}$. The notation $\forall^{\texttt{out}}$ is a macro which restricts quantification over output positions, and we use brackets $\{,\}$ to distinguish the binary MSO predicates. Extending this, suppose we have some alphabetic linear order $\preceq$ over $\Sigma$ and we want to sort the input labels by increasing order. This can be done by adding the requirement $\forall^{\texttt{out}}x,y\bigwedge_{\sigma\prec\sigma^{\prime}}\sigma(x)\wedge\sigma^{\prime}(y)\rightarrow x\leq_{\texttt{out}}y$. This simply defined transduction can be realised by a two-way transducer, which would make one pass per symbol $\sigma$ (in increasing order), during which it copies the $\sigma$-symbols on the output tape and not the others.

Results

We show the following results on $\mathcal{L}_{T}$:

• •

it is expressive: any regular functional transduction is definable in $\mathcal{L}_{T}$. Beyond functions, $\mathcal{L}_{T}$ is incomparable with non-deterministic two-way transducers and non-deterministic streaming string transducers (it can express $\tau_{\text{shuffle}}$ which is definable in none of these models).

• •

it characterises the regular functional transductions: a functional transduction is regular iff it is $\mathcal{L}_{T}$-definable. Moreover, given an $\mathcal{L}_{T}$-formula, it is decidable whether it defines a functional transduction.

• •

the satisfiability problem is decidable (in non-elementary time, which is unavoidable because of the binary MSO predicates), and ExpSpace-c if the binary MSO predicates are given by automata. Since $\mathcal{L}_{T}$ is closed under negation, we obtain as a consequence the decidability of the equivalence problem for $\mathcal{L}_{T}$-definable o-transductions.

• •

it admits regular synthesis: from any $\mathcal{L}_{T}$-sentence $\phi$, one can always synthesise a deterministic two-way transducer which has the same domain as $\llbracket\phi\rrbracket$ and whose o-graphs all satisfy $\phi$.

Finally, we provide two strictly more expressive extensions of $\mathcal{L}_{T}$, shown to admit regular synthesis, and hence decidable satisfiability problem. The first one $\exists\mathcal{L}_{T}$ extends any $\mathcal{L}_{T}$-formula with a block of existential monadic second-order quantifiers and it captures all transductions defined by non-deterministic MSO-transducers or equivalently non-deterministic streaming string transducers (Alur and Deshmukh, 2011). Then, we introduce $\exists\mathcal{L}_{T}^{\mathrm{so}}$ which extends $\exists\mathcal{L}_{T}$ with unary predicates $L(x)$ called single-origin predicates, where $L$ is a regular language, which holds in an input position $x$ if the word formed by the positions having origin $x$ belongs to $L$. For instance one could express that any input position labelled by $a$ has to produce a word in $(bc)^{*}$, which cannot be done with a $\text{FO}^{2}$ formula. This extension allows us to additionally capture any rational relation, i.e. the transductions defined by (nondeterministic) one-way transducers (Jean Berstel, 1979).

Our main and most technical result is regular synthesis. Indeed, it entails satisfiability (test domain emptiness of the constructed transducer), and, since no automata/transducer model is known to be equivalent to $\text{MSO}_{\texttt{o}}$ nor $\mathcal{L}_{T}$, we could not directly rely on automata-based techniques. The techniques of (Bojańczyk et al., 2017) for model-checking do not apply either because the target model is not given when considering satisfiability and synthesis. Instead, we introduce a sound and complete bounded abstraction of the o-graphs satisfying a given $\mathcal{L}_{T}$-formula. This abstraction was inspired by techniques used in data word logics (Schwentick and Zeume, 2012), although we could not directly reuse known results, since they were only concerned with the satisfiability problem. Nonetheless, we exhibit a tight connection between o-graphs and data words.

A consequence on data words

As a side contribution, we explicit a bijection between non-erasing origin graphs (the origin mapping is surjective) and words over an infinite alphabet of totally ordered symbols, called data words. Briefly, the origin becomes the data and conversely the data becomes the origin. We show that this bijection carries over to the logical level, and we obtain a new decidable logic for data words, which strictly extends the logic $\text{FO}^{2}[\leq,\preceq,S_{\preceq}]$ (linear position order and linear order and successor over data), known to be decidable from (Schwentick and Zeume, 2012), with any binary MSO$[\preceq]$ predicate talking only about the data.

Related Work

First, let us mention some known logical way of defining transductions. Synchronised (binary) relations, also known as automatic relations, are relations defined by automata running over word convolutions (Sakarovich, 2009). A convolution $u\otimes v$ is obtained by overlapping two words $u,v$ and by using a padding symbol $\bot$ if they do not have the same length. E.g. $aba\otimes bc=(a,b)(b,c)(a,\bot)$. By taking MSO over word convolutions, one obtains a logic to define transductions. It is however quite weak in expressive power, as it cannot even express all functional transductions definable by one-way input-deterministic finite transducers.

Courcelle has introduced MSO-transducers to define graph transductions (Courcelle, 1990) and which, casted to words, gives a logic-based formalism to define word transductions. Roughly, the predicates of the output word are defined by several MSO-formulas with free variables, interpreted over a bounded number of copies of the input structure. Additionally, several free parameters can be used to add a form of non-determinism. Functional MSO-transducers correspond exactly to functional regular transduction (Engelfriet and Hoogeboom, 2001). However, they have a relatively limited expressive power when it comes to relations, because, unlike $\mathcal{L}_{T}$, the number of images of a word is always finite. For instance, the universal transduction $\Sigma^{*}\times\Sigma^{*}$ is not definable in this formalism, while it is simply definable by the $\mathcal{L}_{T}$-formula $\top$, nor is $\tau_{\text{shuffle}}$ (this can be shown using cardinality arguments).

Finally, there is a number of recent works on reactive synthesis (Jacobs et al., 2017), since the seminal problem raised by Church (Alonzo Church, 1962), and studied by Pnueli and Rosner for LTL specifications (Pnueli and Rosner, 1989). In these works however, the specification is always a synchronised relation and the target implementation is a Mealy machine (an input-deterministic finite transducer alternatively reading and producing exactly one symbol at a time). While $\mathcal{L}_{T}$ does not make any synchronicity assumption, the target implementations in this paper are deterministic two-way transducer which are, computationally speaking, more powerful. We leave open the question of whether the following synthesis problem is decidable: given an $\mathcal{L}_{T}$-formula $\phi$, is there a (one-way) input-deterministic (also known as sequential) transducer realising $\phi$?

Transducer synthesis is also equivalently known as uniformisation in transducer theory (Sakarovich, 2009). This problem has been studied in the origin-free semantics for the class of rational relations. It is known that from any rational relation one can synthesise a rational function (Elgot and Mezei, 1965), and that checking whether it is realisable by a sequential function is undecidable (Carayol and Löding, 2014; Filiot et al., 2016). The former result is a consequence of our results on the extension $\mathcal{L}_{T}^{\mathrm{so}}$: we show that any rational relation defined by a one-way transducer is $\mathcal{L}_{T}^{\mathrm{so}}$-definable (while preserving the origin mappings) and moreover, any transduction defined in $\mathcal{L}_{T}^{\mathrm{so}}$ is realisable by a regular function . Hence, from rational relation given as a one-way transducer $T$ we obtain an order-preserving and functional regular o-transduction that realises the relation defined by $T$. Such o-transductions are easily seen to be equivalent to rational functions (Bojanczyk, 2014; Filiot, 2015). Finally, we mention that transducer synthesis has also been recently studied in the context of trees, where the specification is a tree automatic relation (Löding and Winter, 2014).

Due to the lack of space, some proofs are omitted or only sketched in the body of the paper. The full proofs are given in the appendix.

2. Logics with origin for transductions

Words and transductions

We denote by $\Sigma^{*}$ the set of finite words over some alphabet $\Sigma$, and by $\epsilon$ the empty word. The length of a word $u\in\Sigma^{*}$ is denoted by $|u|$, in particular $|\epsilon|=0$. The set of positions of $u$ is $\mathrm{dom}(u)=\{1,\dots,|u|\}$, an element $i\in\mathrm{dom}(u)$ denoting the $i$th position of $u$, whose symbol is denoted $u(i)\in\Sigma$.

Let $\Sigma$ and $\Gamma$ be two alphabets, without loss of generality assumed to be disjoint. A transduction is a subset of $\Sigma^{+}\times\Gamma^{*}$ of pairs $(u,v)$, where $u$ is called the input word and $v$ the output word. An origin mapping from a word $v\in\Gamma^{*}$ to a word $u\in\Sigma^{+}$ is a mapping $o:\mathrm{dom}(v)\rightarrow\mathrm{dom}(u)$. Intuitively, it means that position $i$ was produced when processing position $o(i)$ in the input word $u$. We exclude the empty input word from the definition of transductions, because we require every output position to have some origin. This does not weaken the modelling power of the logics we consider, up to putting some starting marker for instance. Following the terminology of (Bojańczyk et al., 2017), an origin-graph (o-graph for short) is a pair $(u,(v,o))$ such that $(u,v)\in\Sigma^{+}\times\Gamma^{*}$ and $o$ is an origin mapping from $v$ to $u$. We denote by $\mathcal{OG}(\Sigma,\Gamma)$ the set of o-graphs from $\Sigma$ to $\Gamma$. A transduction with origin (or just o-transduction) $\tau$ from $\Sigma$ to $\Gamma$ is a set of o-graphs. We say that $\tau$ is functional (or is a function) if for all $u$, there is at most one pair $(v,o)$ such that $(u,(v,o))\in\tau$, and rather denote it by $f$ instead of $\tau$. The domain of an o-transduction $\tau$ is the set $\mathrm{dom}(\tau)=\{u\mid\exists(u,(v,o))\in\tau\}$. Finally, the origin-free projection of $\tau$ is the transduction $\{(u,v)\mid\exists(u,(v,o))\in\tau\}$. Many results of this paper hold with or without origins. We always state them in their strongest version, usually without origin.

Regular functional transductions

Regular functional transductions (or regular functions) have many characterisations, as mentioned in the introduction. We will briefly define them as the transductions definable by deterministic two-way transducers, which are pairs $(A,\rho)$ such that $A$ is a deterministic two-way automaton with set of transitions $\Delta$, and $\rho$ is a morphism of type $\Delta^{*}\rightarrow\Gamma^{*}$. The transduction defined by $(A,\rho)$ has domain $L(A)$ (the language recognised by $A$) and for all words $u$ in its domain, the output of $u$ is the word $\rho(r)$, where $r$ is the accepting sequence of transitions of $A$ on $u$. Such transducers (as well as other known equivalent models) can be naturally equipped with an origin semantics (Bojanczyk, 2014) and we say that a functional $o$-transduction is regular if it is equal to the set of $o$-graphs of some deterministic two-way transducer.

FO and MSO logics for transductions

We consider FO and MSO over particular signatures. Without defining their syntax formally (we refer the reader e.g. to (Straubing, 1994)), recall that MSO over a set of predicates $S$ allows for first-order quantification $\exists x$ over elements, second-order quantification $\exists X$ over element sets, membership predicates $x\in X$, predicates of $S$ and all Boolean operators. We use the notation $\text{MSO}[S]$ (or $\text{FO}[S]$) to emphasise that formulas are built over a particular signature $S$. As usual, $\phi(x_{1},\dots,x_{n})$ denotes a formula with $n$ free first-order variables, and we call sentence a formula without free variables. Finally, $\models$ denotes the satisfiability relation.

Origin-graphs $(u,(v,o))$ of $\mathcal{OG}(\Sigma,\Gamma)$ are seen as structures with domain $\mathrm{dom}(u)\uplus\mathrm{dom}(v)$ over the signature $\mathcal{S}_{\Sigma,\Gamma}$ composed of unary predicates $\delta(x)$, for all $\delta\in\Sigma\cup\Gamma$, holding true on all positions labelled $\delta$, $\mathrel{\leq_{\texttt{in}}}$ a linear-order on the positions of $u$, $\mathrel{\leq_{\texttt{out}}}$ a linear-order on the positions of $v$, and o a unary function for the origin, which is naturally interpreted by $o$ over $\mathrm{dom}(v)$, and as the identity function222As functional symbols must be interpreted by total functions, we need to interpret o over $\mathrm{dom}(u)$ as well. over $\mathrm{dom}(u)$. We also use the predicates $=$, $<_{\texttt{in}}$ and $<_{\texttt{out}}$, which are all definable in the logics we consider. We denote by $\text{MSO}_{\texttt{o}}$ the logic $\text{MSO}[\mathcal{S}_{\Sigma,\Gamma}]$. Any $\text{MSO}_{\texttt{o}}$ sentence $\phi$ defines an o-transduction $\llbracket\phi\rrbracket_{o}=\{(u,(v,o))\in\mathcal{OG}(\Sigma,\Gamma)\mid(u,(v,o))\models\phi\}$ and its origin-free counterpart $\llbracket\phi\rrbracket$. An o-transduction (resp. transduction) $\tau$ is $\text{MSO}_{\texttt{o}}$-definable if $\tau=\llbracket\phi\rrbracket_{o}$ (resp. $\tau=\llbracket\phi\rrbracket$) for some sentence $\phi\in\text{MSO}_{\texttt{o}}$.

Example 1.

First, we define the transduction $\tau_{\text{cfl}}$ mapping $a^{n}b^{n}$ to $(ab)^{n}$, as the origin-free projection of the set of o-graphs defined by some $\text{MSO}_{\texttt{o}}$-sentence $\phi_{\text{cfl}}$, which expresses that (1) the domain is in $a^{*}b^{*}$, (2) the codomain in $(ab)^{*}$ (both properties are regular and, hence, respectively $\text{MSO}[\Sigma,\mathrel{\leq_{\texttt{in}}}]$- and $\text{MSO}[\Gamma,\mathrel{\leq_{\texttt{out}}}]$-definable), and (3) the origin-mapping is bijective and label-preserving (see introduction).

Satisfiability and synthesis problems

The satisfiability problem asks, given an $\text{MSO}_{\texttt{o}}$-sentence $\phi$, whether it is satisfied by some $o$-graph, i.e. whether $\llbracket\phi\rrbracket_{o}\neq\varnothing$ (or equivalently $\llbracket\phi\rrbracket\neq\varnothing$) holds. By encoding the Post Correspondence Problem, we show that $\text{MSO}_{\texttt{o}}$ has undecidable satisfiability problem, even if restricted to the two-variable fragment of FO with the $S_{\texttt{out}}$ predicate, denoting the successor relation over output positions:

Proposition 2**.**

Over o-graphs, the logic $\text{FO}^{2}[\Sigma,\Gamma,\mathrel{\leq_{\texttt{in}}},\mathrel{\leq_{\texttt{out}}},S_{\texttt{out}},\texttt{o}]$ has undecidable satisfiability problem.

Given a transduction $\tau$ and a functional transduction $f$, we say that $f$ realises $\tau$ if $\mathrm{dom}(f)=\mathrm{dom}(\tau)$, and for all input $u$, $(u,f(u))\in\tau$. The regular synthesis problem asks whether given an o-transduction $\tau$, there exists a regular functional o-transduction $f$ which realises it. As claimed in the introduction, this problem is undecidable when $\tau$ is defined in $\text{MSO}_{\texttt{o}}$.

Proposition 3**.**

The regular synthesis problem is undecidable for $\text{MSO}_{\texttt{o}}$-definable transductions.

Sketch.

We reduce the $\text{MSO}_{\texttt{o}}$ satisfiability problem. First, consider the $\text{MSO}_{\texttt{o}}$-sentence $\phi_{\text{cfl}}$ of Ex. 1 defining a transduction with non-regular domain. Then, given an $\text{MSO}_{\texttt{o}}$-formula $\psi$ of which one wants to check satisfiability, we define in $\text{MSO}_{\texttt{o}}$, using $\psi$ and $\phi_{\text{cfl}}$, the transduction $\tau$ mapping any word $u_{1}\#u_{2}$ to $v_{1}\#v_{2}$ such that $(u_{1},v_{1})\in\llbracket\psi\rrbracket$ and $(u_{2},v_{2})\in\llbracket\phi_{\text{cfl}}\rrbracket$. Then, $\mathrm{dom}(\tau)$ is non-regular iff it is nonempty. Since regular functions have regular domains, $\tau$ is realisable by a regular function iff $\mathrm{dom}(\tau)=\varnothing$ iff $\llbracket\psi\rrbracket=\varnothing$ iff $\llbracket\psi\rrbracket_{o}=\varnothing$. ∎

The logic $\mathcal{L}_{T}$ for transductions

Informally, the logic $\mathcal{L}_{T}$ extends the two-variable logic $\text{FO}^{2}[\Sigma,\Gamma,\mathrel{\leq_{\texttt{in}}},\mathrel{\leq_{\texttt{out}}},\texttt{o}]$ with any binary predicate definable in $\text{MSO}[\mathrel{\leq_{\texttt{in}}},\Sigma]$, i.e. any binary MSO predicate that is only allowed to talk about the input positions, in order to capture regular input properties. Formally, we denote by $\text{MSO}_{\text{bin}}[\mathrel{\leq_{\texttt{in}}},\Sigma]$ the set of $n$-ary predicates, $n\in\{0,1,2\}$, denoted by $\{\phi\}$, where $\phi$ is an $\text{MSO}[\mathrel{\leq_{\texttt{in}}},\Sigma]$-formula with at most $n$ free first-order variables. Over a word $u$, such a formula $\phi$ defines an $n$-ary relation $R_{\phi,u}$ on its position, and over an o-graph $(u,(v,o))$, we interpret $\{\phi\}$ by $R_{\phi,u}$. The logic $\mathcal{L}_{T}$ is the two-variable fragment of first-order logic over the output symbol predicates, the linear-order $\mathrel{\leq_{\texttt{out}}}$, and all predicates in $\text{MSO}_{\text{bin}}[\mathrel{\leq_{\texttt{in}}},\Sigma]$, i.e. $\mathcal{L}_{T}:=\text{FO}^{2}[\Gamma,\mathrel{\leq_{\texttt{out}}},\texttt{o},\text{MSO}_{\text{bin}}[\mathrel{\leq_{\texttt{in}}},\Sigma]]$. Modulo removing the brackets $\{,\}$, it is a proper fragment of $\text{MSO}_{\texttt{o}}$.

Examples of $\mathcal{L}_{T}$-transductions

The true formula $\top$ is satisfied by any o-graph. Hence $\llbracket\top\rrbracket=\Sigma^{+}\times\Gamma^{*}$. Let us now define several macros that will be useful throughout the paper. The formula $\texttt{in}(x)\equiv x\mathrel{\leq_{\texttt{in}}}x$ (resp. $\texttt{out}(x)\equiv x\mathrel{\leq_{\texttt{out}}}x$) holds true if $x$ belongs to the input word (resp. output word). Now for $\alpha\in\{\texttt{in},\texttt{out}\}$, we define the guarded quantifiers $\exists^{\alpha}x\ \phi$ and $\forall^{\alpha}x\ \phi$ as shortcuts for $\exists x\ \alpha(x)\wedge\phi$ and $\forall x\ \alpha(x)\rightarrow\phi$ (note that $\neg\exists^{\alpha}x\ \phi$ is equivalent to $\forall^{\alpha}x\ \neg\phi$).

Preservation of the input/output orders is expressed by the $\mathcal{L}_{T}$-formula $\forall^{\texttt{out}}x,y\ (x\mathrel{\leq_{\texttt{out}}}y)\rightarrow\{x^{\prime}\mathrel{\leq_{\texttt{in}}}y^{\prime}\}(\texttt{o}(x),\texttt{o}(y))$. Note that we could equivalently replace $x^{\prime}$ and $y^{\prime}$ by any variable (even $x$ and $y$), without changing the semantics: the formula $x^{\prime}\mathrel{\leq_{\texttt{in}}}y^{\prime}$ defines a binary relation on the input word, which is used as an interpretation of the predicate $\{x^{\prime}\mathrel{\leq_{\texttt{in}}}y^{\prime}\}$ in o-graphs. To ease the notations, any predicate $\{\phi\}(t_{1},t_{2})$ where $\phi$ has two free variables $x_{1}$ and $x_{2}$ may be sometimes written $\{\phi[x_{1}/t_{1},x_{2}/t_{2}]\}$, i.e. $\phi$ in which $t_{i}$ has been substituted for $x_{i}$. We keep the brackets $\{$ and $\}$ to emphasise the fact that it is a binary MSO formula which speaks about the input word. Hence, the previous formula may also be written $\phi_{\text{pres}}\equiv\forall^{\texttt{out}}x,y\ (x\mathrel{\leq_{\texttt{out}}}y)\rightarrow\{\texttt{o}(x)\mathrel{\leq_{\texttt{in}}}\texttt{o}(y)\}$.

The fact that $o$ is a bijective mapping is expressible by some $\mathcal{L}_{T}$-formula $\phi_{\text{bij}}$, as seen in the introduction. Then, the shuffle transduction $\tau_{\text{shuffle}}$ is defined by $\phi_{\text{shuffle}}\equiv\phi_{\text{bij}}\wedge\forall^{\texttt{out}}x\bigwedge_{\sigma\in\Gamma}\sigma(\texttt{o}(x))\rightarrow{\sigma}(x)$. If the origin mapping is also required to be order-preserving, we get a formula defining identity: $\phi_{\text{id}}\equiv\phi_{\text{shuffle}}\wedge\phi_{\text{pres}}$.

Let us now consider the transduction $\tau:(ab)^{n}\mapsto a^{n}b^{n}$. By taking any bijective and label-preserving origin mapping, e.g. as follows:

a$$b$$a$$b$$a$$b$$a$$b$$a$$a$$a$$a$$b$$b$$b$$b

one can define $\tau$, as long as the input word is in $(ab)^{*}$, which is regular, hence definable by some $\text{MSO}[\mathrel{\leq_{\texttt{in}}},\Sigma]$-formula $\phi_{(ab)^{*}}$. Then, $\tau$ is defined by: $\{\phi_{(ab)^{*}}\}\wedge\phi_{\text{bij}}\wedge\bigwedge_{\alpha\in\{a,b\}}\forall^{\texttt{out}}x\ \newline \alpha(x)\rightarrow\{\alpha(\texttt{o}(x))\}\wedge\forall^{\texttt{out}}x,y\ a(x)\wedge b(y)\rightarrow x\mathrel{\leq_{\texttt{out}}}y$. More generally, one could associate with any word $(ab)^{n}$ the set of all well-parenthesised words of length $n$ over $\Gamma$.

Remark 4*.*

According to the previous examples, one can express in $\mathcal{L}_{T}$ the transduction $\tau_{1}$ defined as the shuffle over the language $a^{*}b^{*}$, and also $\tau_{2}:(ab)^{n}\mapsto a^{n}b^{n}$. Hence the composition $\tau_{2}\circ\tau_{1}:a^{n}b^{n}\mapsto a^{n}b^{n}$ has a non-regular domain. However, as we will see in Section 3, the domain of an $\mathcal{L}_{T}$-transduction is always regular, which means that $\mathcal{L}_{T}$-transductions are not closed under composition.

3. Expressiveness, satisfiability and synthesis

3.1. Expressiveness of $\mathcal{L}_{T}$

Our first result is that $\mathcal{L}_{T}$ can express all regular functions. To show this result, we use their characterisation as deterministic MSO-transducers (Engelfriet and Hoogeboom, 2001). We briefly recall that an MSO-transducer is defined by some $\text{MSO}[\leq_{\texttt{in}},\Sigma]$-formulas interpreted over the input word structure (with linear order denoted here by $\leq_{\texttt{in}}$), which specify the predicates of the output word structure, the domain of which are copies of the input nodes. More precisely, a constant $k$ specifies the number of copies of the input word structure, $\text{MSO}[\leq_{\texttt{in}}]$-formulas $\phi_{pos}^{c}(x)$ specify whether the $c$th copy of node $x$ is kept in the output structure, monadic formulas $\phi_{\gamma}^{c}(x)$ for each copy $c\in\{1,\dots,k\}$ and $\gamma\in\Gamma$, specify whether the $c$th copy of input node $x$ is labelled $\gamma$ in the output structure, and ordering formulas $\phi_{\leq_{\texttt{out}}}^{c,d}(x,y)$, say if the $c$th copy of $x$ is before the $d$th copy of $y$ in the output.

Theorem 1.

Any regular function is $\mathcal{L}_{T}$-definable.

Sketch of proof.

Let $f$ be a regular function. Since it is regular, there exists an MSO-transducer defining it. We convert it into an $\mathcal{L}_{T}$-formula. First, it is not difficult to define an $\text{MSO}[\leq_{\texttt{in}},\Sigma]$-formula $\phi_{c_{1},\dots,c_{l},v}(x)$, $c_{1},\dots,c_{l}\in\{1,\dots,k\}$ and $v\in\Gamma^{*}$, which holds true if and only if in the output structure generated by the MSO-transducer, the copies of $x$ that are used are exactly $c_{1},\dots,c_{l}$, they occur in this order in the output structure, and they are respectively labelled $v(1),\dots,v(l)$. In other words, input position $x$ generates the subword $v$ in the output structure. Then, we define $\mathcal{L}_{T}$-formulas $C_{i}(x)$, for all $i\in\{1,\dots,k\}$ and $x$ an output node (in the o-graph), which hold, respectively, iff $x$ is the $i$th node (in the output order) whose origin is $\texttt{o}(x)$. This can be done using only two variables: $C_{1}(x)\equiv\texttt{out}(x)\wedge\forall^{\texttt{out}}y,\ y<_{\texttt{out}}x\rightarrow\{\texttt{o}(x)\neq\texttt{o}(y)\}$ and for $i\geq 1$, $C_{i+1}(x)\equiv$

[TABLE]

Finally, we construct the final $\mathcal{L}_{T}$-formula (omitting some minor details) as a conjunction, for all $m,l\leq k$, all copies $c_{1},\dots,c_{l}$ and $d_{1},\dots,d_{m}$, all words $v\in\Gamma^{l}$ and $w\in\Gamma^{m}$, all $i\leq l$ and $j\leq m$, of the formulas:

[TABLE]

∎

MSO-transducers have been extended with nondeterminism (NMSO-transducers or just NMSOT) to express non-functional transductions, by using a set of monadic second-order parameters $X_{1},\dots,X_{n}$ (Engelfriet and Hoogeboom, 2001). Each formula of an NMSO-transduction can use $X_{1},\dots,X_{n}$ as free variables. Once an interpretation for these variables as sets of positions has been fixed, the transduction becomes functional. Therefore, the maximal number of output words for the same input word is bounded by the number of interpretations for $X_{1},\dots,X_{n}$. NMSO-transducers are linear-size increase (the length of any output word is linearly bounded by the length of the input word), hence the universal transduction $\Sigma^{+}\times\Gamma^{*}$ is not definable in NMSO, while it is $\mathcal{L}_{T}$-definable by $\top$. The shuffle transduction is not definable in NMSOT as well (this can be shown by cardinality arguments). Conversely, it turns out that a transduction like $(u,vv)$ where $v$ is a subword of $u$ of even length is not $\mathcal{L}_{T}$-definable whereas is it in NMSOT.

Rational relations are transductions defined by (non-deterministic) finite transducers (finite automata over the product monoid $\Sigma^{*}\times\Gamma^{*}$), denoted 1NFT (Jean Berstel, 1979). This class is incomparable with $\mathcal{L}_{T}$: the shuffle is not a rational relation, while the relation $\{a\}\times L$, where $L$ is a non-$\text{FO}^{2}$-definable regular language is not $\mathcal{L}_{T}$-definable. Indeed, when all inputs are restricted to the word $a$, the expressive power of $\mathcal{L}_{T}$ is then restricted to $\text{FO}^{2}[\leq_{\texttt{out}},\Gamma]$ over the output.

Non-deterministic two-way transducers (2NFT), are incomparable to NMSO (Engelfriet and Hoogeboom, 2001), and also to $\mathcal{L}_{T}$, since they extend 1NFT and cannot define the shuffle transduction. Fig. 2 depicts these comparisons, summarised by the following proposition:

Proposition 2**.**

The classes of $\mathcal{L}_{T}$, 2NFT (resp. 1NFT), and NMSOT-definable transductions are pairwise incomparable.

3.2. Satisfiability and equivalence problems

Our first main contribution is the following result, whose proof is sketched in Section 4. Here and throughout the paper, by effectively we mean that the proof effectively constructs a finite object.

Proposition 3**.**

The input domain of any $\mathcal{L}_{T}$-transduction is (effectively) regular.

Theorem 4.

Over $o$-graphs, the logic $\mathcal{L}_{T}$ has decidable satisfiability problem.

This latter theorem is a consequence of Thm 5. We point out that it holds also for origin-free transductions, because given an $\mathcal{L}_{T}$-formula $\phi$, $\llbracket\phi\rrbracket=\varnothing$ iff $\llbracket\phi\rrbracket_{o}=\varnothing$. The equivalence problem asks, given two formulas $\phi_{1},\phi_{2}$, whether $\llbracket\phi_{1}\rrbracket_{o}=\llbracket\phi_{2}\rrbracket_{o}$, i.e. whether $\phi_{1}\leftrightarrow\phi_{2}$ is universally true. As a consequence of Thm. 4 and closure under negation of $\mathcal{L}_{T}$ we have the decidability of the equivalence problem for $\mathcal{L}_{T}$.

With respect to satisfiability, $\mathcal{L}_{T}$ seems to lie at the decidability frontier. Adding just the successor relation over outputs already leads to undecidability, by Prop. 2.

3.3. Regular synthesis of $\mathcal{L}_{T}$ and consequences

Our main result is the regular synthesis of $\mathcal{L}_{T}$-transductions.

Theorem 5 (Regular synthesis of $\mathcal{L}_{T}$).

Let $\phi$ be an $\mathcal{L}_{T}$ formula. The transduction defined by $\phi$ is (effectively) realisable by a regular function.

In other words, from any specification $\phi$ written in $\mathcal{L}_{T}$, one can synthesise a functional transduction $f$, in the proof represented by an MSO-transducer $T$, such that $\mathrm{dom}(f)=\mathrm{dom}(\llbracket\phi\rrbracket)$ and $f=\llbracket T\rrbracket\subseteq\llbracket\phi\rrbracket$. Moreover, it turns out that the constructed transducer $T$ defines a functional o-transduction $\llbracket T\rrbracket_{o}$ such that $\llbracket T\rrbracket_{o}\subseteq\llbracket\phi\rrbracket_{o}$. In other words, $T$ does not change the origins specified in $\phi$. Since we rely on MSO-to-automata translation in the construction, the size of the constructed MSO-transducer is non-elementary in the size of $\phi$. One of the main consequences of the synthesis and expressiveness results is a new characterisation of the class of regular functions.

Theorem 6 (New characterisation of regular functions).

Let $f:\Sigma^{*}\rightarrow\Gamma^{*}$. Then, $f$ is regular iff $f$ is $\mathcal{L}_{T}$-definable.

Proof.

By Thm. 1, $f$ regular implies $f$ is $\mathcal{L}_{T}$-definable, which implies by Thm. 5 that $f$ is regular. ∎

A consequence of synthesis is the following positive result on functionality:

Corollary 7** (Functionality).**

Given an $\mathcal{L}_{T}$-sentence $\phi$, it is decidable whether the o-transduction $\llbracket\phi\rrbracket_{o}$ is functional.

Proof.

To test whether $\llbracket\phi\rrbracket_{o}$ is functional, first realise it by a regular function (Thm. 5), defined e.g. by a deterministic two-way transducer $T$, and then test whether $\llbracket\phi\rrbracket_{o}\subseteq\llbracket T\rrbracket_{o}$. The latter is decidable since $T$ can be converted (while preserving origins) into an equivalent $\mathcal{L}_{T}$-formula $\psi$ (Thm. 1) and test that $\phi\rightarrow\psi$ is satisfiable (Thm.4). ∎

4. Domain regularity and synthesis: sketch of proofs

In this section, we sketch the proofs of Prop. 3 (domain regularity of $\mathcal{L}_{T}$-transductions) and Thm. 5 (regular synthesis). These two results are based on common tools which we now describe. We let $\phi$ be an $\mathcal{L}_{T}$-sentence over input and output alphabets $\Sigma,\Gamma$ respectively. We assume that $\mathcal{L}_{T}$ defines a non-erasing o-transduction, i.e. an o-transduction which uses every input position at least once (the origin mapping is surjective). This can be done without loss of generality, i.e. one can transform in polynomial time any $\mathcal{L}_{T}$-sentence into a non-erasing one (by adding dummy output positions the origins of which are the erased input positions), while preserving the domain and set of regular functions realising it (modulo the previous encoding).

Scott normal form

The $\mathcal{L}_{T}$ formula $\phi$ is then transformed into a Scott normal form (SNF), a standard transformation when dealing with two-variable logics (see for instance (Grädel and Otto, 1999)). By enriching the alphabet, the transformation allows to restrain ourself to the easier setting of formulas of quantifier-depth two. Precisely, we obtain a formula of the form:

[TABLE]

where the formulas $\psi$ and $\psi_{i}$, $i=1,\dots,m$, are quantifier free, but over an extended output alphabet $\Gamma\times\Gamma^{\prime}$ (where $\Gamma^{\prime}$ may be exponential in $\phi$). These subformulas can also still contain binary MSO predicates over the input, which are not restricted in any way. Up to projection over $\Gamma$, the SNF formula accepts the same models as $\phi$, and hence we now just assume that $\phi$ is a formula of the above form over an input alphabet $\Sigma$ and output alphabet $\Gamma$. In the full proof (Appendix), the SNF is further equivalently transformed into what we call a system of universal and existential constraints (in the vein of (Schwentick and Zeume, 2012)), which are easier to manipulate in the proofs than the formulas $\psi$ and $\psi_{i}$, but are not necessary at a conceptual level, so we do not include them in the sketch.

The profile abstraction

We define an abstraction which maps any o-graph $(u,(v,o))$ to a sequence of $|u|$ tuples $\lambda_{1}\dots\lambda_{|u|}$ called profiles, one for each input position. A profile contains bounded information (bounded in the size of $\phi$) about the binary input MSO predicates, the input symbol and some output positions. To explain this abstraction, we first informally define what we call the full graph of an o-graph $(u,(v,o))$. Intuitively, the full graph contains a node for each pair $(p,p^{\prime})\in\mathrm{dom}(u)\times\mathrm{dom}(v)$, labelled by some information called clause about the “effect” of position $p^{\prime}$ at position $p$. To understand it, it is convenient to see the full graph as a two-dimensional structure with the input position as $x$-axis (ordered by $\leq_{\texttt{in}}$) and the output position as the $y$-axis (ordered by $\leq_{\texttt{out}}$). Figure 3 shows such a representation. E.g. the top-left figure represents the full graph of an $o$-graph which translates $\sigma_{1}\dots\sigma_{5}$ into $(\beta\gamma)^{3}$ (for instance, the origin of the last output position, labelled $\gamma$, is the third input position, labelled $\sigma_{3}$), plus some additional information which we now detail.

Each row contains a single node labelled in $\Gamma$, corresponding to an output position, and placed according to its origin. Let $(p,p^{\prime})$ (output position $p^{\prime}$ with origin $p$) be such a node, labelled by some $\gamma\in\Gamma$. This node generates an horizontal trace around it, whose elements are of the form $\gamma\overleftarrow{R}$ or $\gamma\overrightarrow{R}$. The arrows indicate in which direction the $\gamma$-labelled node is. The elements $R$, say at coordinates $(s,p^{\prime})$, are $\text{MSO}[\Sigma,\mathrel{\leq_{\texttt{in}}}]$-types (of bounded quantifier rank) talking about the input word $u$ with the positions $s$ and $p$ marked. In the proof, we represent these MSO-types as state information of node selecting automata (or query automata, see e.g. (Niehren et al., 2005)). The idea behind this information is that, by looking independently at each column of the full graph of an o-graph, it is possible to decide whether this o-graph satisfies $\phi$. Suppose for instance we want to check whether the o-graph satisfies a formula of the form $\forall^{\texttt{out}}x\exists^{\texttt{out}}y\cdot\gamma(x)\rightarrow\gamma^{\prime}(y)\wedge y<_{\texttt{out}}x\wedge\{\xi\}(\texttt{o}(y),\texttt{o}(x))$. Then, for every column containing a $\gamma$-labelled node, say at coordinate $(p,p^{\prime})$, one has to check that there exists a node in the same column, say at position $(p,p^{\prime\prime})$, labelled by some $(\gamma^{\prime}\overleftarrow{R})$ or some $(\gamma^{\prime}\overrightarrow{R})$, such that $p^{\prime\prime}<p^{\prime}$ and $R$ satisfies $\xi$. Suppose that in the SNF we also have a conjunct of the form $\forall^{\texttt{out}}x,y\cdot(\gamma(x)\wedge\gamma^{\prime}(y)\wedge\{\texttt{o}(x)<_{\texttt{out}}\texttt{o}(y))\}\rightarrow\{\xi^{\prime}\}(\texttt{o}(x),\texttt{o}(y))$, then we must additionally checks that for every column, for every $\gamma$-labelled node in this column and every $\gamma^{\prime}\overrightarrow{R}$-labelled node on the same column, $R$ satisfies $\xi^{\prime}$. We call a column which satisfies the SNF formula $\phi$ a valid column.

A key property we now use is that, if on a column there exists at least three nodes with the same label, then removing all but the smallest and greatest (in output order) of these nodes does not influence the validity of the column. It is easy to see for subformulas of $\phi$ of the form $\forall^{\texttt{out}}x,y\ \psi(x,y)$ (removing nodes makes such a formula “easier” to satisfy). For subformulas of the form $\forall^{\texttt{out}}\exists^{\texttt{out}}y\ \psi_{i}(x,y)$, it is due to the fact that $\psi_{i}$ is quantifier-free, and therefore it is safe to keep only the extremal witnesses $y$ for $x$.

This observation leads us to the notion of abstract graph, the subgraph of the full graph obtained by keeping only the extremal occurrences of every node with same labels. Figure 3 illustrates this abstraction, on hypothetical full graphs where label equalities have been underlined. Each column indexed by position $p$ of this abstract graph, together with the input symbol, is what we call the profile of $p$. Note that this is a bounded object. Then, to any o-graph one can associate a sequence of profiles this way, but this association is not injective in general since we may lose information, as shown in the figure. Put differently, the abstract graph can in general be concretised in more than one full graph.

Properties of profile sequences

The key ingredient of the proof is to define properties on profile sequences $s$ (which are nothing but words over the finite alphabet of profiles), that can be checked in a regular manner (by an automaton) so that there exists at least one o-graph $g$ such that $(1)$ $s$ is the profile sequence of $g$ and $(2)$ $g\models\phi$. Property $(2)$ is ensured by the notion of validity defined before, and by a notion of maximality for the MSO-types $R$ (no information can be withheld). Property $(1)$ is ensured by a notion of consistency between profiles. Intuitively, it asks that the information declared in one profile is consistent, in some precise way, with the information declared in the next profile. Roughly, since we use automata to represent the information $R$, one step consistency corresponds to one step in the runs of the automata. Maximal and consistent sequences of valid profiles are called good profile sequences.

We then prove a completeness result: the profile sequence of any model of $\phi$ is good. We also prove a soundness result: any good profile sequence is the profile sequence of at least one model of $\phi$. As a matter of fact, we prove a slightly stronger result which allows one to recover not just one but potentially several models of $\phi$. As illustrated on the figure, every connected component of the abstract graph corresponds to exactly one node labelled in $\Gamma$. The notion of consistency ensures this property as well, and, as a matter of fact, the output positions of the models we reconstruct out of good profile sequences are in bijection with these connected components (CC). We can even order them partially, as illustrated on the figure, by overlapping: a CC is the successor of another one if they overlap horizontally, and the former is above the latter (again, our definition of consistency ensures that there is no “crossing” in abstract graphs, hence this relation can indeed be shown to be a partial order). Hence, a good profile sequence defines an abstract graph which gives us: the input position with their labels, the output positions with their labels and origins, and some partial order between these output positions. What’s missing is a linear order on these output positions, but we prove that any linearisation of this partial order actually defines an o-graph which satisfies $\phi$. Coming back to the example, the two possibly linearisations give the output words $\beta\gamma\beta\beta\gamma$ and $\beta\gamma\gamma\beta\gamma$.

Back to the theorems

To show domain regularity (Prop. 3), we observe that the domain is the projection on input alphabet $\Sigma$ of the set of good profile sequences, which turns out to be regular (the whole point of defining the notions of validity, maximality and consistency is that they can be checked by an automaton). Since regular languages are closed under projection, we get the result.

Showing regular synthesis (Thm. 5) is a bit more technical. The main idea is to show that the mapping which takes as input a word $u$ over $\Sigma$, and which outputs all the abstract graphs of o-graphs which satisfy $\phi$ and have $u$ as input, is definable by a non-deterministic MSO word-to-DAG transduction $T_{1}$. It is possible since the notions of consistency, maximality and validity are all MSO-definable, and an abstract graph is always a DAG. Then, we use a result of Courcelle which states that there exists a deterministic MSO DAG-to-word transduction $R_{2}$ which, given a DAG, produces a topological sort of it (Courcelle, 1996). The DAG additionally needs to be locally ordered (the successors of a node are linearly ordered), but we can ensure this property in our construction. Then, we use closure under composition of NMSOT to show that $R_{2}\circ R_{1}$ is definable by some word-to-word NMSOT, which can be easily realised by a (deterministic) MSOT, concluding the proof.

Comparison with (Schwentick and

Zeume, 2012)

We would like to point out that this proof was inspired by a decidability proof for the logic $\text{FO}^{2}[\leq,\preceq,S_{\preceq}]$ over data words (a linear order over positions and a linear order and successor over data). We somehow had to cast it to transductions, and extend it with binary MSO predicates. Moreover, further manipulations and notions were needed to extract the synthesis result. In particular, the ideas of using Scott normal form, to see o-graphs as two-dimensional structures, and the abstraction, were directly inspired from (Schwentick and Zeume, 2012).

5. A decidable logic for typed data words

We make here a bijective connection between o-transductions and what we call typed data words, which slightly generalise data words, and introduce a new decidable logic $\mathcal{L}_{D}$ for typed data words, whose decidability stems from the equivalence with $\mathcal{L}_{T}$.

Typed data words

We consider typed data words over an ordered data domain, such that each datum also carries a label (type) from a finite alphabet. Formally, a typed data word of length $n$ and data size $m$ over two disjoint alphabets $\Gamma$ and $\Sigma$ is a word over the alphabet $\Gamma\times\mathbb{N}\times\Sigma$, $w=(\gamma_{1},d_{1},\sigma_{1})\cdots(\gamma_{n},d_{n},\sigma_{n})$ verifying the following properties: $d_{i}$ is called the datum of position $i$, we have that $\left\{d_{1},\ldots,d_{n}\right\}=\left\{1,\ldots,m\right\}$ 333We make this assumption without loss of generality, because the logic we define will only be able to compare the order of data, and so cannot distinguish typed data words up to renaming of data, as long as the order is preserved. E.g. $(a,b,1)(c,d,3)(e,f,2)$ and $(a,b,2)(c,d,5)(e,f,4)$ will be indistinguishable by the logic. and we also have for any positions $i,j$ that $d_{i}=d_{j}\Rightarrow\sigma_{i}=\sigma_{j}$, hence $\sigma_{i}$ is called the type of datum $d_{i}$.

We denote by $\mathcal{TDW}(\Sigma,\Gamma)$ the set of typed data words over alphabets $\Sigma,\Gamma$ of any length $n$ and any data size $m$.

The data of a typed data word $w$ induce a total preorder $\preceq$ over the positions of $w$ defined by $i\preceq j$ if $d_{i}\leq d_{j}$. This preorder induces itself an equivalence relation $\sim$ defined by $i\sim j$ iff $i\preceq j$ and $j\preceq i$, which means that the positions $i$ and $j$ carry the same datum. Hence, a typed data word will equivalently be seen as a structure with letter predicates $\gamma\in\Gamma$, $\sigma\in\Sigma$, the linear order over positions and the total preorder $\preceq$ previously defined.

The logic $\mathcal{L}_{D}$ for typed data

words

It is known from (Bojańczyk et al., 2006) that the logic MSO over untyped data words (i.e. $|\Sigma|=1$) is undecidable (even the first-order fragment). We consider here a decidable fragment, over typed data words, called $\mathcal{L}_{D}$. A formula of $\mathcal{L}_{D}$ can be seen as an $\text{FO}^{2}$ formula using the linear order of the positions and some additional binary data predicates. The logic $\mathcal{L}_{D}$ is indeed built on top of MSO $n$-ary predicates, for $n\leq 2$, which are allowed to speak only about the data. Precisely, we define $\text{MSO}_{\text{bin}}[\Sigma,\preceq]$ to be the set of $n$-ary predicates written $\{\phi\}$, for $n\leq 2$, where $\phi$ is an MSO-formula with $n$-free first-order variables, over the unary predicates $\sigma(x)$ and the preorder $\preceq$, with the following semantic restriction444Note that the semantic restriction could also be enforced in the logic by guarding quantifiers $\exists X\psi$ with $\exists X[\forall x\forall y\ x\in X\wedge y\sim x)\rightarrow y\in X]\rightarrow\psi$.: second-order variables are interpreted by $\sim$-closed sets of positions. Over typed data words, predicates $\{\phi\}$ are interpreted by relations on positions defined by formulas $\phi$.

Due to the semantic restriction, formulas in $\text{MSO}_{\text{bin}}[\Sigma,\preceq]$ cannot distinguish positions with the same data and therefore, they can be thought of as formulas which quantify over data and sets of data. As an example, the formula $\forall y\ x\preceq y$ expresses that the datum of position $x$ is the smallest, and it holds true for any $x^{\prime}$ with the same datum. Then, the logic $\mathcal{L}_{D}$ is defined as $\mathcal{L}_{D}:=\text{FO}^{2}[\Gamma,\leq,\text{MSO}_{\text{bin}}[\Sigma,\preceq]]$.

Example 1.

First, let us mention that $\text{MSO}_{\text{bin}}[\Sigma,\preceq]$ predicates can express any regular properties about the data, in the following sense. Given a typed data word $w$, the total preorder $\preceq$ over positions of $w$ can be seen as a total order $\leq_{\sim}$ over the equivalence classes of $\mathrm{dom}(w)/_{\sim}$, by $[i]_{\sim}\leq_{\sim}[j]_{\sim}$ if $i\preceq j$. Then, any typed data word induces a word $\sigma_{1}\dots\sigma_{n}\in\Sigma^{*}$ such that $\sigma_{i}$ is the type of the elements of the $i$th equivalence class of $\leq_{\sim}$. Any regular property of these induced words over $\Sigma$ transfers into a regular property about the data of typed data words (it suffices to replace in the MSO-formula on $\Sigma$-words expressing the property, the linear order by $\preceq$ and the equality by $\sim$). Examples of properties are: $n$ is even, which transfers into “there is an even number of pieces of data”, or $\sigma_{1}\dots\sigma_{n}$ contains an even number of $\sigma\in\Sigma$, for some $\sigma$, meaning “there is an even number of pieces of data of type $\sigma$”.

From transductions to data words and

back

There is a straightforward encoding t2d of non-erasing o-graphs into typed data words, and conversely. A non-erasing o-graph $(u,(v,o))$, with $v=v_{1}\ldots v_{n}$ and $u=u_{1}\ldots u_{m}$ is encoded as the typed data word $\text{t2d}((u,(v,o)))=(v_{1},o(1),u_{o(1)})\ldots(v_{n},o(n),u_{o(n)})$. Given a typed data words $w=(\gamma_{1},d_{1},\sigma_{1})\ldots(\gamma_{n},d_{n},\sigma_{n})$, we set $\text{t2d}^{-1}(w)$ the non-erasing o-graph $\text{t2d}^{-1}(w)=(u,(v,o))$ such that $v=\gamma_{1}\ldots\gamma_{n}$, $o(i)=d_{i}$, and if we write $d_{i_{j}}=j$ then $u=\sigma_{i_{1}}\cdots\sigma_{i_{m}}$ where $m=\text{max}_{i}\ d_{i}$. We give here an example of this transformation:

\#$$\$$$@$$\#$$\#$$a$$b$$c$$c$$a$$b$$(a,3,@)$$(b,2,\)$(c,1,\#)$(c,3,@)$(a,5,\#)$(b,4,#)$

Theorem 2.

Non-erasing o-graphs of $\mathcal{OG}(\Sigma,\Gamma)$ and typed data words of $\mathcal{TDW}(\Sigma,\Gamma)$ are in bijection by t2d. Moreover, a non-erasing o-transduction $\tau$ is $\mathcal{L}_{T}$-definable iff $\text{t2d}(\tau)$ is $\mathcal{L}_{D}$-definable. Conversely, a language of typed data words $L$ is $\mathcal{L}_{D}$-definable iff $\text{t2d}^{-1}(L)$ is $\mathcal{L}_{T}$-definable.

The main idea of the proof is to make a bijective syntactic transformation that mimics the encoding t2d: once inconsistent use of terms have been removed (such as e.g., $o(x)\mathrel{\leq_{\texttt{out}}}y$), terms $o^{n}(x)$ are replaced by $x$, predicates $\mathrel{\leq_{\texttt{in}}}$ by $\preceq$ and $\mathrel{\leq_{\texttt{out}}}$ by $\leq$. Hence, this theorem and the decidability of $\mathcal{L}_{T}$ (Thm. 4) gives the following corollary.

Corollary 3**.**

Over typed data words, the logic $\mathcal{L}_{D}$ has a decidable satisfiability problem.

As a remark, we also note that thanks to the correspondence between transductions and data words and some minor manipulations, we can also obtain the decidability of $\text{FO}^{2}[\leq_{\texttt{in}},\leq_{\texttt{out}},S_{\texttt{in}},\texttt{o}]$ (for in the input successor), which is a strict fragment of $\mathcal{L}_{T}$, over o-graphs from the decidability of $\text{FO}^{2}[\leq,\preceq,S_{\preceq}]$ over data words, proved in (Schwentick and Zeume, 2012). However, the logic $\text{FO}^{2}[\leq,\preceq,S_{\preceq}]$ is a strict fragment of $\mathcal{L}_{D}$.

6. Complexity of satisfiability

To achieve decidability results for $\mathcal{L}_{T}$, the binary MSO predicates over the input of $\mathcal{L}_{T}$-formulas are decomposed into MSO-types, that we handle using query automata, as explained in the sketch of proof in Section 4. A query automaton for a binary MSO formula $\psi(x,y)$ is a non-deterministic finite automaton $\mathcal{A}=(Q,\Sigma,I,\Delta,F)$ equipped with a set ${SP}\subseteq Q^{2}$ of selecting pairs with the following property: for any word $u\in\Sigma^{*}$ and any pair of positions $(i,j)$ of $u$, we have $u\models\psi(i,j)$ if, and only if, there exists an accepting run $\pi$ of $\mathcal{A}$ and a pair $(p,q)\in{SP}$ such that $\pi$ reads $u(i)$ in state $p$ and $u(j)$ in state $q$. Due to the MSO-formulas and their translation into query automata, the complexity of the satisfiability of $\mathcal{L}_{T}$ is non-elementary, and this is unavoidable (Stockmeyer, 1974). However, if the binary MSO-formulas are already given as query automata, we get a tight elementary complexity. Likewise, the binary MSO predicates of the data word logic $\mathcal{L}_{D}$ can be also represented as query automata, and we get the same complexity as $\mathcal{L}_{T}$.

Theorem 1.

The satisfiability problem of $\mathcal{L}_{T}$ and $\mathcal{L}_{D}$ is ExpSpace-complete when the binary MSO predicates are given as query automata.

Sketch of proof.

First, as the translation between $\mathcal{L}_{T}$ and $\mathcal{L}_{D}$ is linear, the complexity of both logics is equivalent. In showing decidability of the satisfiability of $\mathcal{L}_{T}$, we obtain that the set of ”good” profile sequences is effectively regular by Prop. 3. With a careful analysis it is possible to construct a doubly exponential deterministic automaton recognising the good sequences. By checking emptiness on-the-fly instead of constructing the automaton, we get the NLogSpace emptiness of the automaton, and hence the ExpSpace complexity. Finally, since the logic $\text{FO}^{2}[\Gamma,\preceq,S_{\preceq},\leq]$ is ExpSpace-complete (Schwentick and Zeume, 2012), we get ExpSpace-hardness as this logic is a syntactic fragment of $\mathcal{L}_{D}$. ∎

7. Decidable Extensions of $\mathcal{L}_{T}$

We present here two main extensions to $\mathcal{L}_{T}$ showing its robustness. The first one consists in adding a block of existential monadic second-order quantifiers in front of the formula while the second one consists in adding new predicates to the logic; both extensions preserve many properties of the logic which we describe below.

Existential $\mathcal{L}_{T}$

This new logic is denoted by $\exists\mathcal{L}_{T}$ and allows us to capture all non-deterministic MSO-transductions, but we lose the closure under negation of the logic. Formally, we consider all formulas of the form $\exists X_{1}\dots\exists X_{n}\phi$ where $\phi$ is a formula of $\mathcal{L}_{T}$ which can additionally use predicates of the form $x\in X_{i}$. The variables $X_{i}$ range over sets of output, and also input positions.

Proposition 1**.**

Any NMSO-transduction is $\exists\mathcal{L}_{T}$-definable.

The synthesis result extends to $\exists\mathcal{L}_{T}$ using a quite common trick of considering for a formula $\exists X_{1}\dots\exists X_{n}\phi$, the formula $\phi$ but over an extended alphabet.

Proposition 2**.**

Any $\exists\mathcal{L}_{T}$-transduction can be (effectively) realised by a regular function.

One result of $\mathcal{L}_{T}$ does not carry over to $\exists\mathcal{L}_{T}$, namely the decidability of the equivalence problem. Indeed $\exists\mathcal{L}_{T}$ is not closed under negation and thus equivalence of formulas cannot be reduced to satisfiability. Equivalence turns out to be undecidable for $\exists\mathcal{L}_{T}$ and in fact the validity problem, which asks given a formula if it is satisfied by all o-graphs and which can be seen as the particular case of the equivalence with the formula $\top$, is itself undecidable for $\exists\mathcal{L}_{T}$.

Proposition 3**.**

The validity and equivalence problems for $\exists\mathcal{L}_{T}$ over o-graphs are undecidable.

Single-origin predicates

One “weak” point of $\mathcal{L}_{T}$ is that if the input is restricted to, for instance, a single position, then the expressive power over the output is only $\mathrm{FO}^{2}[\leq_{\texttt{out}}]$. For instance the transduction $\{a\}\times L$ is not definable if $L$ not an $\mathrm{FO}^{2}[\mathrel{\leq_{\texttt{out}}}]$-definable language. A more general expression of this problem is that the class of transductions definable by one-way transducers, also known as rational transductions (Jean Berstel, 1979), is incomparable with the class of $\mathcal{L}_{T}$ (resp. $\exists\mathcal{L}_{T}$) transductions. The following extension, called $\mathcal{L}_{T}^{\mathrm{so}}$ adds new predicates, called here single-origin predicates, and we show that it captures all the rational transductions. These new predicates allow to test any regular property of a subword of the output word restricted to positions with a given origin position.

Given an o-graph $(u,(v,o))$ and an input position $i$ of $u$, we denote by $v_{|i}$ the subword of $v$ consisting of all the positions of $v$ whose origin is $i$, and we call this word the single-origin restriction of $v$ to $i$.

Given any regular language $L$ (represented as an MSO formula for instance), we define a unary input predicate $L(x)$, whose semantics over an $o$-graph $(u,(v,o))$ is the set of input positions $i\in\mathrm{dom}(u)$ such that $v_{|i}\in L$. The logic $\mathcal{L}_{T}^{\mathrm{so}}$ (resp. $\exists\mathcal{L}_{T}^{\mathrm{so}}$) is the extension of $\mathcal{L}_{T}$ (resp. $\exists\mathcal{L}_{T}$) with the predicates $L(x)$, for any regular language $L$. These predicates can be used just as the other unary input predicates and using the previous notation we have $\mathcal{L}_{T}^{\mathrm{so}}:=\text{FO}^{2}[\Gamma,\mathrel{\leq_{\texttt{out}}},\texttt{o},\text{MSO}_{\text{bin}}[\mathrel{\leq_{\texttt{in}}},\Sigma\uplus\{L(x)|\ L\text{ regular}\}]]$. For instance, let $L$ denote the language $(ab)^{*}$ then the formula $\forall^{\texttt{out}}x\ a(x)\rightarrow\{\mathrm{even}(\texttt{o}(x))\wedge L(\texttt{o}(x))\}$ states that the origin of each output position $x$ labelled by $a$ must be even and that the subword of origin $o(x)$ must be in $L$.

Proposition 4**.**

Any rational transduction is $\mathcal{L}_{T}^{\mathrm{so}}$ definable.

Our synthesis result transfers to $\mathcal{L}_{T}^{\mathrm{so}}$ (and $\exists\mathcal{L}_{T}^{\mathrm{so}}$):

Proposition 5**.**

Any $\exists\mathcal{L}_{T}^{\mathrm{so}}$-transduction can be (effectively) realised by a regular function.

Remark 6*.*

From the regular synthesis of $\exists\mathcal{L}_{T}^{\mathrm{so}}$, we can deduce several results which we express in their strongest form: The input domain of any $\exists\mathcal{L}_{T}^{\mathrm{so}}$-transduction is effectively regular, the satisfiability problem for $\exists\mathcal{L}_{T}^{\mathrm{so}}$ is decidable, the equivalence problem for $\mathcal{L}_{T}^{\mathrm{so}}$ is decidable. Finally, given a functional transduction, it is regular if and only if it is $\exists\mathcal{L}_{T}^{\mathrm{so}}$-definable, and, given an $\exists\mathcal{L}_{T}^{\mathrm{so}}$ sentence $\phi$, it is decidable whether $\llbracket\phi\rrbracket_{o}$ is functional.

Extended logics over data words

We define similarly the extensions $\exists\mathcal{L}_{D}$, $\mathcal{L}_{D}^{\mathrm{sd}}$ and $\exists\mathcal{L}_{D}^{\mathrm{sd}}$ of the logic $\mathcal{L}_{D}$ and we obtain the same transfer results as in Thm. 2. In terms of data, the single-origin predicates become single datum predicates (sd) which can specify any regular property over a subword induced by a single datum.

8. Summary and Discussion

In this paper, we have introduced an expressive logic to define transductions, which we believe is a great tool from both a theoretical and a more practical point of view. It allows for high-level specification of transductions, while having some good properties for synthesis. As an interesting side contribution, we obtain a new characterisation of the class of regular transductions, as the (functional) transductions definable in $\mathcal{L}_{T}$ (and its extensions up to $\exists\mathcal{L}_{T}^{\text{so}}$). The expressiveness and decidability frontiers on the logic $\mathcal{L}_{T}$ and its extensions are summarised in Fig. 4. We obtained tight complexity results for satisfiability of $\mathcal{L}_{T}$ both in the case of binary input predicates given by MSO-formulas (non-elementary) or automata (ExpSpace). We have also shown that slightly extending the expressiveness by adding the successor over output positions leads to undecidability.

Another question is the definition of an automata model equivalent to $\mathcal{L}_{T}$, or even to $\text{MSO}_{\texttt{o}}$. Automata for data words have been defined (Bojańczyk et al., 2006; Manuel and Zeume, 2013), but none of these models capture $\mathcal{L}_{D}$.

The equivalence problem for $\mathcal{L}_{T}$ is origin-dependent. One could relax it by projecting away the origin information: given two $\mathcal{L}_{T}$-formulas $\phi_{1},\phi_{2}$, are the origin-free transductions they define equal, i.e. $\llbracket\phi_{1}\rrbracket=\llbracket\phi_{2}\rrbracket$ ? This (origin-free) equivalence problem is known to be decidable for regular functions (Gurari, 1982), and undecidable for 1NFT (and hence 2NFT) (Griffiths, 1968) as well as NMSOT (Alur and Deshmukh, 2011). It is shown by reduction from the Post Correspondence Problem and it turns out that the transductions constructed in the reduction of (Griffiths, 1968) are definable in $\mathcal{L}_{T}$, proving undecidability for $\mathcal{L}_{T}$ as well. An interesting line of research would be to consider less drastic relaxations of the equivalence problem with origin, by comparing transductions with similar origin, as done for instance in (Filiot et al., 2016) for rational relations. Similarly, the model-checking of two-way transducers against $\text{MSO}_{\texttt{o}}$-sentences is decidable, but it is again origin-sensitive. Instead, the origin-free version of this problem is to decide whether for all the pairs of words $(u,v)$ defined by a two-way transducer $T$, there exists some origin mapping $o$ such that the $o$-graph $(u,v,o)$ satisfies some formula $\phi$ . Once again, it is possible to show, by reducing PCP, that this relaxation yields undecidability, but it could be interesting to consider a stronger problem where the origin of $T$ is “similar” to the origin specified in $\phi$. A related problem is the satisfiability of logics where two or more origin mappings are allowed.

Another direction would be extending the logic to other structures (e.g. trees or infinite words), and other predicates over output positions. However, one has to be careful since the data point of view shows how close we are to undecidability (e.g. over data words, $\text{FO}^{2}$ with successor over data and positions is undecidable (Manuel et al., 2013)).

Finally, we have established a tight connection between transductions and data words, and thus a new decidable logic for data words. The data point of view allowed us to get decidability of the transduction logic $\mathcal{L}_{T}$, inspired by the decidability result of (Schwentick and Zeume, 2012). Conversely, the logic $\mathcal{L}_{D}$ extends the known results on data words by adding MSO predicates on the ordered and labelled data. We would like to investigate if further results from the theory of transductions can be translated into interesting results in the theory of data words.

Appendix A Logics with origin for transductions

See 2

Proof.

The proof is a reduction from the Post Correspondence Problem (PCP) and is an adaptation to o-tranductions of the undecidability, over data words, of $\text{FO}^{2}$ with a linear order and successor predicates over positions, and a linear-order on data (Bojańczyk et al., 2006).

Given an alphabet $A$ and $n$ pairs $(u_{i},v_{i})\in A^{+}\times A^{+}$ (they can be assumed to be non-empty without losing undecidability), we construct a sentence $\phi\in\text{FO}[\mathcal{T}_{\Sigma,\Gamma}]$ which is satisfiable iff there exist $i_{1},\dots,i_{k}\in\{1,\dots,n\}$ such that $u_{i_{1}}\dots u_{i_{k}}=v_{i_{1}}\dots v_{i_{k}}$. We let $\Sigma=A$ and $\Gamma=A_{1}\cup A_{2}$, where $A_{i}=A\times\{i\}$. Given a word $w=a_{1}\dots a_{p}\in A^{*}$ and $\ell=1,2$, we let $\ell(w)=(a_{1},\ell)\dots(a_{p},\ell)\in A_{\ell}^{*}$. For any two sequences of words $s=w_{1},w_{2},\dots,w_{k}\in A^{*}$ and $s^{\prime}=w^{\prime}_{1},\dots,w^{\prime}_{k}\in A^{*}$, we define $s\otimes s^{\prime}\in\Gamma^{*}$ their interleaving, by $1(w_{1})2(w^{\prime}_{1})1(w_{2})2(w^{\prime}_{2})\dots 1(w_{k})2(w^{\prime}_{k})$.

E.g. $(ab,ca)\otimes(a,bca)=(a,1)(b,1)(a,2)(c,1)(a,1)(b,2)(c,2)(a,2)$.

We will construct the formula $\phi$ in such a way that it defines the o-tranduction from $\Sigma$ to $\Gamma$ which maps any word $u\in\Sigma^{*}$ for which there exist $i_{1},\dots,i_{k}\in\{1,\dots,n\}$ such that $u_{i_{1}}\dots u_{i_{k}}=u=v_{i_{1}}\dots v_{i_{k}}$, to $w=(u_{i_{1}},\dots,u_{i_{k}})\otimes(v_{i_{1}},\dots,v_{i_{k}})$, with origin mapping $o$ which maps any position of $w$ corresponding to some $u_{i_{j}}$ (or to some $v_{i_{j}}$) to the same position in $u$. E.g., over $A=\{a,b,c\}$, if one takes $u_{1}=ab$, $u_{2}=ca$, $v_{1}=a$, $v_{2}=bca$, then the sequence $1,2$ is a solution to PCP, and it gives rise to the following o-graph:

a$$b$$c$$a$$a,1$$b,1$$a,2$$c,1$$a,1$$b,2$$c,2$$a,2$$u_{1}$$v_{1}$$u_{2}$$v_{2}

First, we express that the output word is of the form $(u_{i_{1}},\dots,u_{i_{k}})\otimes(v_{i_{1}},\dots,v_{i_{k}})$ for some $i_{1},\dots,i_{k}$. For that, we need to define a formula $\phi_{\text{cut}}(x)$ which holds true at output position $x$ if either $x$ is the first output position, or it is labelled in $A_{1}$ while its predecessor is labelled in $A_{2}$:

[TABLE]

where for all $\ell=1,2$, $A_{\ell}(x)$ stands for $\bigvee_{a\in A}(a,\ell)(x)$.

Now, the idea when $x$ is a cut (i.e. satisfies the formula $\phi_{\text{cut}}(x)$), is to guess an index $i\in\{1,\dots,n\}$ and check that the sequence of labels from position $x$ ($x$ included) to the next cut (if it exists) or to the end (if not) is $1(u_{i})2(v_{i})$.

To define this, we introduce, for all formulas $\phi$ with one free variable, the formula $\Lbag\phi\Rbag_{j}(x)$ which holds true if the $j$-th successor of $x$ exists and satisfies $\phi$. It is inductively defined by:

[TABLE]

where $y$ is a variable different from $x$. Then, we define the following formula for $i\in\{1,\dots,n\}$:

[TABLE]

Finally, the following formula expresses that the output word is of the form $(u_{i_{1}},\dots,u_{i_{k}})\otimes(v_{i_{1}},\dots,v_{i_{k}})$ for some $i_{1},\dots,i_{k}$:

[TABLE]

So far, we have not checked any property of the origin mapping, nor the fact that the output decomposition satisfies $u_{i_{1}}\dots u_{i_{k}}=v_{i_{1}}\dots v_{i_{k}}=u$ if $u$ is the input word. To achieve that, it remains to express, for all $\ell=1,2$, that the origin mapping restricted to positions labelled in $A_{\ell}$ is bijective and preserves the orders and labels.

[TABLE]

The final formula $\phi$ is then:

[TABLE]

Note that we have only used two variables $x$ and $y$ all over the construction. ∎

See 3

Proof.

First, let $\phi_{\text{cfl}}$ be the $\text{MSO}_{\texttt{o}}$-sentence defining the transduction $\tau_{\text{cfl}}$ of Example 1. We reduce the $\text{MSO}_{\texttt{o}}$ satisfiability problem, which is undecidable by Prop. 2, to the regular synthesis problem. Let $\psi$ be an $\text{MSO}_{\texttt{o}}$-sentence of which we want to test satisfiability, over alphabets $\Sigma,\Gamma$, which do not contain $a,b$. We construct an $\text{MSO}_{\texttt{o}}$ sentence $\psi^{\prime}$ over the input alphabet $\Sigma\cup\{a,\#\}$ and output alphabet $\Gamma\cup\{b,\#\}$, which defines the transduction consisting of the o-graphs $(u_{1}\#u_{2},(v_{1}\#v_{2},o))$ such that $(u_{1},(v_{1},o_{1}))\models\psi$, where $o_{1}$ is the restriction of $o$ to $v_{1}$, and $(u_{2},(v_{2},o_{2}))\models\phi_{\text{cfl}}$, where $o_{2}$ is the restriction of $o$ to $v_{2}$.

Before explaining how to construct $\psi^{\prime}$, let us convince the reader that $\llbracket\psi^{\prime}\rrbracket$ is realisable by a regular functional transduction iff $\mathrm{dom}(\llbracket\psi^{\prime}\rrbracket)=\varnothing$ iff $\llbracket\psi\rrbracket=\varnothing$ iff $\llbracket\psi\rrbracket_{o}=\varnothing$. Clearly, if $\llbracket\psi\rrbracket_{o}=\varnothing$, then $\mathrm{dom}(\llbracket\psi^{\prime}\rrbracket)=\varnothing$ and hence $\llbracket\psi^{\prime}\rrbracket$ is realisable by the regular function with empty domain. Conversely, if $\llbracket\psi\rrbracket_{o}\neq\varnothing$, there exists $(u_{1},(v_{1},o_{1}))\models\psi$. Towards a contradiction, suppose that $\llbracket\psi^{\prime}\rrbracket$ is realisable by a regular function $f$. Since regular functions are closed under regular domain restriction, the function $f^{\prime}=f|_{L}$ where $L=u_{1}\#(a+b)^{*}$ is regular, and hence has regular domain. This contradicts the fact that $\mathrm{dom}(f^{\prime})=\mathrm{dom}(f)\cap L=\{u_{1}\#a^{n}b^{n}\mid n\geq 0\}$ is non-regular.

Finally, we let $\psi^{\prime}=\psi_{dom}\wedge\psi_{codom}\wedge\psi^{<\#}\wedge\phi_{\text{cfl}}^{>\#}$ where $\psi_{dom}$ expresses that the domain is included in $\Sigma^{*}\#(a+b)^{*}$, $\psi_{codom}$ that the codomain is included in $\Sigma^{*}\#(a+b)^{*}$, $\psi^{<\#}$ is just the formula $\psi$ where the input (resp. output) quantifiers are guarded to range before the unique input (resp. output) position labelled $\#$, and symmetrically for $\phi_{\text{cfl}}^{>\#}$. ∎

Appendix B Expressiveness, decidability and synthesis for $\mathcal{L}_{T}$

B.1. Expressiveness of $\mathcal{L}_{T}$

See 1

Proof.

First let us define some unary and binary predicates for the input. Let $P$ be a subset of $\left\{1,\ldots,k\right\}$, we define the formula which states that the copies of $x$ which are used for the output are the ones of $P$:

[TABLE]

Let $c_{1},\ldots,c_{l}$ be a sequence of non-repeating integers smaller than $k$, then we define the formula which says that the order of the copies of $x$ in the output follow the sequence:

[TABLE]

Now let $v\in\Gamma^{l}$, we define the formula specifying the letters of the output positions:

[TABLE]

Let $d_{1},\ldots,d_{m}$ be a sequence of non-repeating integers smaller than $k$ and $w\in\Gamma^{m}$, then we define:

[TABLE]

Now we define an $\mathcal{L}_{T}$-formula $C_{i}(x)$ which states that $x$ is exactly the $i$th output position of some input position.

[TABLE]

And for $i\geq 1$:

[TABLE]

Note that we have used only two variables $x$ and $y$. Now we can define an $\mathcal{L}_{T}$ formula which defines the MSO-transduction:

[TABLE]

∎

See 2

Proof.

Firstly, since all MSO-transductions are $\mathcal{L}_{T}$-definable, and as NMSO are defined as MSO-transducers with additional existential parameters, it should be clear that \exists$$\mathcal{L}_{T} subsumes NMSO-transductions.

We now turn to the incomparability results. All witnesses of incomparability are given in Fig. 2 that is recalled here.

First, $\text{MSO}_{\texttt{o}}$ is strictly more expressive than the other formalisms since it is able to specify relations with non regular domain. Indeed a formula for $\tau_{9}$ simply states that the origin is bijective and label -preserving, that the output domain is $(ab)^{*}$ and that the input has all $a$s before $b$s.

Now the logic $\mathcal{L}_{T}$ and 2NFT are not included in NMSO as they can describe the universal relation $\tau_{4}=\Sigma^{+}\times\Gamma^{*}$, which cannot be defined in NMSO as the number of images of a word $u$ of length $n$ by an NMSO is bounded by the number of possible evaluation of the second order parameters $X_{i}$, hence bounded by $2^{cn}$, where $c$ is the number of parameters.

NMSO and $\mathcal{L}_{T}$ are not included in 2NFT as they can synchronise nondeterministic choices over several readings of the input word, which 2NFT cannot do. This is illustrated by relation $\tau_{5}$ which first selects a subword of the input and copies it twice. An $\mathcal{L}_{T}$ formula defining $\tau_{5}$ states that the input positions producing output produce exactly 2 outputs, that labels are preserved, and that the input order is respected within first copies, as well as the second copies. An NMSO describing $\tau_{5}$ simply non deterministically selects a subword via a parameter $X$ and produces $X$ twice, ordering the copies as in the input order.

Finally, NMSO and 2NFT are not included in $\mathcal{L}_{T}$ since they are able to specify arbitrary properties of the output that are not definable in $\text{FO}^{2}$, which is not doable with $\mathcal{L}_{T}$. The relation $\tau_{6}$ is easily done with a 2NFT, and can be done in NMSO with a single parameter $X$ which is required to be of even size. ∎

Appendix C Domain regularity and synthesis: proofs

C.1. Scott Normal Form

C.1.1. Non-erasing o-tranductions

The first step of the transformation consists in ensuring that all the o-graphs satisfying the formula are non-erasing, meaning that each input position produces at least one output position. Formally, an o-graph $(u,(v,o))\in\mathcal{OG}(\Sigma,\Gamma)$ is said to be non-erasing if $o$ is a surjective function, and an $\mathcal{L}_{T}$-formula $\phi$ is non-erasing if all o-graphs of $\llbracket\phi\rrbracket$ are non-erasing. Satisfiability of $\mathcal{L}_{T}$ is reducible to satisfiability of non-erasing formulas, by adjoining to the output a copy of the input.

Proposition 1**.**

For any $\mathcal{L}_{T}$-formula $\phi$ there exists a non-erasing $\mathcal{L}_{T}$-formula $\phi^{\prime}$ such that $\mathrm{dom}(\llbracket\phi\rrbracket)=\mathrm{dom}(\llbracket\phi^{\prime}\rrbracket)$. In particular, $\phi$ is satisfiable if, and only if, $\phi^{\prime}$ is.

Proof.

let $\phi$ be an $\mathcal{L}_{T}$-formula, we want to obtain an $\mathcal{L}_{T}$-formula $\phi^{\text{n.e.}}$ which is non-erasing. The idea is to extend the output of all o-graphs by a copy of the input word. We add a new output letter $\sharp$ which will separate the normal output and the copy of the input. We want to obtain $(u,(v,o))\models\phi$ iff $(u,(v\sharp u,o^{\prime}))\models\phi^{\text{n.e.}}$ where $o^{\prime}(i)=o(i)$ if $i\leq|v|$, $o^{\prime}(1+i+|v|)=i$ if $i\leq|u|$ and $o^{\prime}(|v|+1)=1$. From $\phi$, we construct $\phi^{<\sharp}$ where every quantification over the output positions is relativised as being before a position labelled by $\sharp$. Similarly, for $\phi_{\text{id}}$ the identity o-tranduction, we define $\phi_{\text{id}}^{>\sharp}$ where quantifications over the output are relativised as appearing after a position labelled by $\sharp$. Adding the guards can be done while staying in the two-variable fragment. Then we define $\phi^{\text{n.e.}}$ to be equal to:

[TABLE]

∎

An output formula is an $\mathcal{L}_{T}$ formula which is only allowed to quantify over output positions. The point of considering non-erasing formulas is that one can always transform a non-erasing formula into an equivalent output formula.

Proposition 2**.**

For an $\mathcal{L}_{T}$ formula, one can construct an output formula which is equivalent (over non-erasing o-graphs).

Proof.

This is shown by constructing inductively an output formula. Atomic formulas are not affected, and boolean connectives are left unchanged. The remaining case is when $\phi$ is of the form $\exists x\ \psi(x)$. Then $\phi$ is transformed into $\phi^{\prime}=\exists^{\texttt{out}}x\ \psi(x)\vee\exists^{\texttt{out}}x\ \psi(\texttt{o}(x))$. Over non-erasing o-graphs, the two formulas are satisfied by the same models, since any input position is the origin of some output position. ∎

C.1.2. Normal Form

The third step is to normalise any formula in $\mathcal{L}_{T}$ into a Scott normal form (SNF). The procedure to put a formula in SNF is the same as for $\text{FO}^{2}$ logics in general (see (Grädel and Otto, 1999) for instance). The point of the SNF is to obtain a formula with additional predicates, which are axiomatised in the formula itself, but with a quantifier depth limited to 2, which lowers the complexity of the formulas. We prove in our context, along with some preservation property, that any $\mathcal{L}_{T}$ formula can be put in SNF while preserving satisfiability. Since we aim to get stronger properties than satisfiability, we state a stronger result, yet the proof is similar.

Lemma 3.

For any $\mathcal{L}_{T}$-formula $\varphi$ over input alphabet $\Sigma$ and output alphabet $\Gamma$, one can construct an $\mathcal{L}_{T}$-formula $\phi$ over $\Sigma$ and $\Gamma\times\Gamma^{\prime}$ such that:

• •

$\Gamma^{\prime}$* is a finite alphabet,*

• •

up to projection on $\Gamma$, $\phi$ and $\varphi$ have the same models,

• •

$\phi$* is of the form $\forall^{\texttt{out}}x\forall^{\texttt{out}}y\ \psi(x,y)\wedge\bigwedge_{i=1}^{m}\forall^{\texttt{out}}x\exists^{\texttt{out}}y\ \psi_{i}(x,y)$ where the formulas $\psi$ and $\psi_{i}$, $i=1,\dots,m$, are quantifier free.*

Proof.

The proof is similar to (Schwentick and Zeume, 2012). We first assume without loss of generality that $\varphi$ is in negation normal form. We now construct the formula $\phi$ iteratively. At each iteration, we get formulas $\theta_{i}$ and $\phi_{i}$ where $\varphi$ is equivalent to $\theta_{i}\wedge\phi_{i}$, $\theta_{i}$ is in correct form, and $\phi_{i}$ has a number of quantifiers reduced by $i$ compared to $\varphi$, while using some additional unary predicates $P_{1},\ldots,P_{i}$. At first let $\theta_{0}=\top$ and $\phi_{0}=\varphi$. Then, at each step, consider a subformula $\xi_{i}(x)$ of $\phi_{i-1}$ with a single quantifier. Then $\xi_{i}(x)$ is either $\exists y\ \rho_{i}(x,y)$ or $\forall y\ \rho_{i}(x,y)$ where $\rho_{i}$ a quantifier free formula. In the first case, we set $\theta_{i}=\theta_{i-1}\wedge\forall x\exists y\ (P_{i}(x)\to\rho_{i}(x,y))$ and $\phi_{i}$ is obtained by replacing $\exists y\ \rho_{i}(x,y)$ by $P_{i}(x)$.

In the second case, we set $\theta_{i}=\theta_{i-1}\wedge\forall x\forall y\ (P_{i}(x)\to\rho_{i}(x,y))$ and $\phi_{i}$ is obtained by replacing $\forall y\ \rho_{i}(x,y)$ by $P_{i}(x)$.

This process ends as at each step the number of quantifiers of $\phi_{i}$ decreases. In the end, we get $\phi_{k}$ which is quantifier free and thus equivalent to $\forall x\forall y\ \phi_{k}$. By combining all the double $\forall$ conjuncts into one formula $\psi$, we finally set $\phi=\theta_{k}\wedge\forall x\forall y\ \psi$ which is in the required form. The size of $\phi$ is linear in the size of the negative normal form of $\varphi$. Finally, the unary predicates $P_{i}$ are added to the alphabet to be treated as letters. This is done by replacing the alphabet $\Gamma$ by $\Gamma\times\Gamma^{\prime}$ , where $\Gamma^{\prime}=2^{P_{1},\ldots,P_{k}}$, and replacing in the formula the predicates $P_{i}(x)$ by the conjunction of letter predicates $\bigvee\limits_{(\gamma,R)\mid P_{i}\in R}(\gamma,R)(x)$.

We need now to prove the first statement regarding domains. We prove this by induction on the formulas $\theta_{i}\wedge\phi_{i}$. Assume that the o-graph $w_{i}$ is a model for $\theta_{i}\wedge\phi_{i}$, we construct $w_{i+1}$ a model for $\theta_{i+1}\wedge\phi_{i+1}$ by adding truth values for the predicate $P_{i+1}$ by setting

[TABLE]

Conversely, if $(w_{i},P_{i+1})$ is a model for $\theta_{i+1}\wedge\phi_{i+1}$, then for any position $p$ of $w_{i}$ such that $(w_{i+1},p)\models P_{i+1}(x)$, we also have $(w_{i},p)\models\xi_{i+1}(x)$ since $P_{i+1}$ does not appear in $\xi_{i+1}$. And since $\varphi$ is in negative normal form, $\xi_{i+1}$ only appears positively and thus $w_{i}\models\varphi_{i}$. We conclude by noting that if $(w_{i},P_{i+1})\models\theta_{i+1}$ then $w_{i}\models\theta_{i+1}$. Notice that the number of predicates added is equal to the number of quantifications in $\varphi$ and hence is linear. However, since they are not mutually exclusive, thisleads to an exponential blow-up of the alphabet $\Gamma^{\prime}$.

Finally, we apply Proposition 2 to remove quantifications over input positions, a construction which preserves the normal form. ∎

C.1.3. Sets of constraints

In the spirit of (Schwentick and Zeume, 2012), we introduce another formalism, called system of constraints, which is equivalent to SNF $\mathcal{L}_{T}$. Constraints are built over label predicates, and some input and output predicates. Given an o-graph $(u,(v,o))$, a label predicate $\gamma\in\Gamma$ is satisfied by an output position $p$ of $v$ if $p$ is labelled $\gamma$. Output predicates are restricted to directions $\uparrow,\downarrow$, which are satisfied by a pair of output positions $(p,p^{\prime})$ if, respectively, $p<p^{\prime}$ and $p^{\prime}<p$. Input predicates are any MSO-definable binary predicate over the input using the labels $\Sigma$ and the input order $\mathrel{\leq_{\texttt{in}}}$. A pair of output positions $(i,j)$ satisfies an input predicate $\psi(x,y)\in\text{MSO}[\Sigma,\leq]$ if their origin satisfy it, i.e. $u\models\psi(\texttt{o}(i),\texttt{o}(j))$.

An existential constraint is a pair $(\gamma,E)$ where $\gamma\in\Gamma$ and $E$ is a set of tuples $(\gamma^{\prime},d,\psi)$ such that $d\in\{\uparrow,\downarrow\}$ is an output direction and $\psi$ is an input predicate. Given an o-graph $(u,(v,o))$, an output position $p$ of $v$ satisfies an $\exists$-constraint $(\gamma,E)$ if whenever $p$ is labelled $\gamma$, there exist a triple $(\gamma^{\prime},d,\psi)\in E$ and a $\gamma^{\prime}$-labelled position $q$ of $v$ such that $(p,q)$ satisfies $d$ and $\psi$. In the latter case, we call $q$ a valid witness of $p$ for $(\gamma,E)$.

A universal constraint is a tuple $(\gamma,\gamma^{\prime},d,\psi)$ where $d$ is an output direction and $\psi$ an input predicate. A pair $(p,q)$ of positions of $v$ satisfies a $\forall$-constraint $(\gamma,\gamma^{\prime},d,\psi)$ if it is not the case that $p$ is labelled by $\gamma$, $q$ by $\gamma^{\prime}$, and $(p,q)$ satisfy $d$ and $\psi$. A universal constraint can be thought of as a forbidden pattern over pairs of points.

An instance of the MSO constraint problem (MCP) is a pair $C=(C_{\exists},C_{\forall})$ of sets of existential and universal constraints respectively. A non-erasing o-graph $w=(u,(v,o))$ is a solution of (or model for) $C$, denoted $w\models C$, if every output position of $v$ satisfies all constraints in $C_{\exists}$ and every pair of output positions satisfy all constraints in $C_{\forall}$.

Proposition 4**.**

From any output $\mathcal{L}_{T}$-sentence $\phi$ in SNF over $\Sigma$ and $\Gamma$, one can construct an instance $C$ of MCP over $\Sigma$ and $\Gamma$ such that for any non-erasing o-graph $w\in\mathcal{OG}(\Sigma,\Gamma)$, $w\models\phi$ iff $w\models C$.

Proof.

Let $\phi=\forall^{\texttt{out}}x\forall^{\texttt{out}}y\ \varphi(x,y)\wedge\bigwedge\limits_{i=1}^{n}\forall^{\texttt{out}}x\exists^{\texttt{out}}y\ \varphi_{i}(x,y)$ with the binary input predicates $(\alpha_{i})_{i=1}^{k}$. We treat [math]-ary and unary predicates as binary predicates. Now given $x$ and $y$ quantifying positions of the output, an atomic type for $x$ and $y$ gives truth value for the predicates $(\alpha_{i})_{i=1}^{k}$ (evaluated over their origin for the input predicates). Formally, it is composed of labels for $x$ and $y$, an output direction $x\sim y$ for $\sim\in\{=,\leftarrow,\rightarrow\}$ and truth values for the binary formulas $\alpha_{i}$. Then a couple of output positions $(p,q)$ is of type $t$ if they satisfy exactly the true properties of $t$ when $x$ and $y$ are evaluated as $p$ and $q$ respectively, and the predicates $\alpha_{i}$ are evaluated on $\texttt{o}(x)$ and $\texttt{o}(y)$. Note that any atomic type can be described by a universal constraint using boolean combinations of the predicates $\alpha_{i}$. Note also that any model of $\phi$ has to satisfy the universal part $\forall^{\texttt{out}}x\forall^{\texttt{out}}y\ \varphi(x,y)$. Hence we want to weed out all atomic types that do not satisfy it. Then the set of universal constraints $C_{\forall}$ is set as all forbidden types, i.e. the atomic types that do not satisfy $\varphi(x,y)$. Then if $w=(u,(v,o))$ is an o-graph which satisfies $\phi$, any pair of positions of $v$ satisfy $\varphi(x,y)$ if and only if they satisfy every constraint of $C_{\forall}$.

We now turn to the formulas $\forall^{\texttt{out}}x\exists^{\texttt{out}}y\ \varphi_{i}(x,y)$. By doing an extensive case study over all atomic types for $x$ and $y$, and then factorising for each label $\gamma$ of $\Gamma$, we can rewrite the formulas as

[TABLE]

where $t_{j,\ell}$ are atomic types. We conclude depending on the nature of the direction $d_{j,\ell}$ of $t_{j,\ell}$. If $d_{j,\ell}$ is $x=y$, then if $t_{j,\ell}$ is compatible with $\gamma_{j}$ the conjunct $\gamma_{j}(x)\to\exists^{\texttt{out}}y\ t_{j,\ell}$ is either a tautology and the whole conjunct is trivially satisfied, or it cannot be satisfied and $t_{j,\ell}$ is removed from the disjunction. The remaining elements of the disjunction can be combined in a set $E$ to form an existential constraint with $\gamma_{j}$. Now if $w\models\forall^{\texttt{out}}x\bigwedge\limits_{j=1}^{k}(\gamma_{j}(x)\to\exists^{\texttt{out}}y\bigvee\limits_{\ell=1}^{m}t_{j,\ell})$, then for every position $p$ of $v$, if $p$ is labelled by $\gamma$ then there exists a position $q$ such that $(p,q)$ is of one of the types $t_{j,\ell}$ and thus $q$ is a valid witness for $p$. Conversely, the fact that any position $p$ has a valid witness means that for any output position labelled by $\gamma$, there is an other position corresponding to its witness which is a valid candidate for $y$, and thus $w$ satisfies $\forall^{\texttt{out}}x\bigwedge\limits_{j=1}^{k}(\gamma_{j}(x)\to\exists^{\texttt{out}}y\bigvee\limits_{\ell=1}^{m}t_{j,\ell})$.

This gives an instance $C=(C_{\exists},C_{\forall})$ of constraints such that for any non-erasing o-graph $w$, $w\models C$ if, and only if, $w\models\phi$. ∎

C.2. The profile abstraction

We define here the important notion of profile, which is a bounded abstraction, given an o-graph, of an input position, the output positions it produces, and its context within the o-graph (other output and input positions). An o-graph can then be abstracted by a sequence of profiles.

We define the notions of validity, with respect to an MCP instance $C$, and of maximal consistency, for sequences of profiles, which respectively talk about the satisfaction of constraints by the profiles of the sequence, and the consistency between consecutive profiles (the information stored in consecutive profiles is correct and consistent).

C.2.1. Automata for binary predicates

In the following we will be using automata for binary predicates. They will serve as MSO types that we can easily manipulate. It is well-known (see e.g. (Niehren et al., 2005)) that any binary $\text{MSO}[\Sigma,\leq]$-predicate $\psi(x,y)$ over $\Sigma$-labelled words, can be equivalently defined by a non-deterministic finite automaton (called here a predicate automaton) $\mathcal{A}_{\psi}=(Q_{\psi},\Sigma,I_{\psi},\Delta_{\psi},F_{\psi})$ equipped with a set ${SP}_{\psi}\subseteq Q_{\psi}^{2}$ of selecting pairs with the following semantics: for any word $u\in\Sigma^{*}$ and any pair of positions $(i,j)$ of $u$, we have $u\models\psi(i,j)$ if, and only if, there exists an accepting run $\pi$ of $\mathcal{A}_{\psi}$ and a pair $(p,q)\in{SP}_{\psi}$ such that $\pi$ is in state $p$ before reading $u(i)$ and in state $q$ before reading $u(j)$.

Example 5.

Let us consider as an example the binary between predicate $Bet_{\sigma}(x,y)=\exists z\ \sigma(z)\wedge(x<z)\wedge(z<y)$, which cannot be expressed using only two variables. The automaton for this predicate is depicted below and its unique selecting pair is $(q_{x},q_{y})$.

q_{x}$$q_{\sigma}$$q_{y}$$q_{f}$$\Sigma$$\Sigma$$\Sigma$$\Sigma$$\Sigma$$\sigma$$\Sigma

C.2.2. Profiles

Let $C$ be an instance of MCP over $\Sigma$ and $\Gamma$, and $\Psi$ the set of MSO-predicates occurring in $C$. For all $\psi{\in}\Psi$, we let $\mathcal{A}_{\psi}$ with set of states $Q_{\psi}$ and set of selecting pairs ${SP}_{\psi}$ be the predicate automaton for $\psi$. Let $S_{\Psi}=\biguplus_{\psi\in\Psi}Q_{\psi}$.

The main ingredient of profiles is a sequence of clauses, where a clause is an element of the set $\mathcal{C}=\Gamma\times(\{\cdot\}\cup\mathcal{P}(S_{\Psi}\times S_{\Psi})\times\left\{\leftarrow,\rightarrow\right\})$. Clauses of the form $(\gamma,\cdot)$ are called local clauses and clauses of the form $(\gamma,R,v)$ are called consistency clauses. Intuitively, in a o-graph, if the profile of an input position $i$ contains a local clause $(\gamma,\cdot)$, this clause describes an output position produced by $i$ (its origin is $i$) and labelled by $\gamma$. If the profile of $i$ contains a clause $(\gamma,R,v)$, it describes an output position whose origin $j$ appears in the direction $v$ with respect to position $i$ (i.e. if $v=\leftarrow$ then $j<i$, $i>j$ otherwise), is labelled $\gamma$ and such that for any pair $(p,q)$ of $R$, there exists an accepting run of $A_{\psi}$ which reads position $i$ in state $p$ and position $j$ in state $q$. A clause $A$ is compatible is with a set of states $S\subseteq S_{\Psi}$ if whenever $A$ is a consistency clause $(\gamma,R,v)$, then $\mathrm{dom}(R)=\{p\mid\exists(p,q)\in R\}\subseteq S$.

A $C$-profile (or just profile) is a tuple $\lambda=(\sigma,S,A_{1}\dots A_{n})$ where $\sigma\in\Sigma$ is an input label, $S\subseteq S_{\Psi}$ and $A_{1}\ldots A_{n}$ is a sequence of clauses from $\mathcal{C}$ such that any clause $A_{i}$ is compatible with $S$ and appears at most twice in the sequence, for all $i=1,\dots,n$. By definition, the number of profiles is bounded by $N=|\Sigma|\cdot 2^{|S_{\Psi}|}(|\Gamma|\cdot(2(2^{|S_{\Psi}|^{2}+1}+1))!$.

C.2.3. Profile of an input position

To define the profile of an input position $k$ of an o-graph $w=(u,(v,o))$, with respect to some MCP instance $C=(C_{\exists},C_{\forall})$, we first define the notion of full profile of that position, which keeps complete (and unbounded) information about the whole o-graph. The profile will be then a bounded abstraction of the full profile. The full profile of $k$ is defined as the tuple $\lambda^{f}=(\sigma,S,B_{1}\ldots B_{|v|})$, where each of its elements are defined as follows. The letter $\sigma$ is the $k$th letter of $u$ and $S$ is the set of states reached by all the accepting runs of the predicate automaton $A_{\Psi}$ on $u$ after reading the prefix $u_{1}\dots u_{k-1}$.

Let now $j\leq|v|$ be an output position with origin $k^{\prime}$. The element $B_{j}$ is a clause generated by the output position $j$, defined as follows. If $k^{\prime}=k$, then $B_{j}=(\gamma,\cdot)$. If $k<k^{\prime}$ (resp. $k>k^{\prime}$), then we define $B_{j}$ to be the consistency clause $(\gamma,R,\rightarrow)$ (resp. $(\gamma,R,\leftarrow)$) where $R$ is the set of all pairs $(p,q)$ from $S_{\Psi}$ such that there exists an accepting run on $u$ that reaches $p$ after reading $u_{1}\dots u_{k-1}$ and $q$ after reading $u_{1}\dots u_{k^{\prime}-1}$ (hence $p\in S$). Therefore in $R$, the first component always refers to the state at the current position $k$, and the second component to the state of described position $k^{\prime}$. The direction indicate whether the described position $k^{\prime}$ is to the right or the left of $k$. Hence, if $(p,q)\in R$ and the direction is $\rightarrow$, it means that the state $p$ eventually reaches $q$ on the right, and if the direction is $\leftarrow$, that the state $q$ was visited before $p$.

The profile $\lambda$ of position $k$ is obtained from $\lambda^{f}$ by keeping in $B_{1}\dots B_{|v|}$ the outermost occurrences of each clause. Formally, it is $\lambda=(\sigma,S,\alpha(B_{1}\dots B_{|v|}))$ where $\alpha:\mathcal{C}^{*}\to\mathcal{C}^{*}$ erases in a sequence of clauses, all but the left- and right-most occurrences of each clause of the sequence. In the following, we show that valid o-graphs give valid sequences of profiles, and that conversely we can construct valid o-graphs from valid sequences. An example of profile sequence is given in Fig. 3, in which clauses $(\gamma,R,\rightarrow)$ are denoted $\gamma\overrightarrow{R}$ (and similarly for clauses $(\gamma,R,\leftarrow)$.

C.2.4. Profile validity

As we have seen, an o-graph can be abstracted by the sequence of its profiles. We aim at defining conditions on profiles and profile sequences $s$ under which from such a sequence of profiles we can reconstruct an o-graph which is a model of an MCP instance $C$. The notion of profile validity takes care of the property of being a model, but not any sequence of profiles will be the profile sequence of an o-graph in general. The notion of profile consistency, defined in the next section, is introduced to ensure this property. First, we start with the notion of profile validity with respect to an MCP-instance $C$.

Definition 0 (Profile validity).

Let $C$ be an MCP-instance and $\lambda=(\sigma,S,A_{1}\ldots A_{n})$ a profile. It satisfies an existential constraint $c=(\gamma,E)$ if for every $i$ such that $A_{i}=(\gamma,\cdot)$ there exists a tuple $(\gamma^{\prime},d,\psi)$ of $E$, $j\leq n$ such that $i$ and $j$ respect the direction $d$ (i.e. $i<j$ if $d=\uparrow$ and $j<i$ otherwise), and either there exists $v\in\{\leftarrow,\rightarrow\}$ such that $A_{j}=(\gamma^{\prime},R,v)$ and $R\cap{SP}_{\psi}\neq\emptyset$, or $A_{j}=(\gamma^{\prime},\cdot)$ and there exists $p\in S$ such that $(p,p)\in{SP}_{\psi}$.

The profile $\lambda$ satisfies a universal constraint $(\gamma,\gamma^{\prime},d,\psi)$ if there do not exist $i$ and $j$ such that $i$ and $j$ respects direction $d$, $A_{i}=(\gamma,\cdot)$ and $A_{j}=(\gamma^{\prime},R,v)$ such that $R\cap{SP}_{\psi}\neq\emptyset$ or $A_{j}=(\gamma^{\prime},\cdot)$ and there exists $p\in S$ such that $(p,p)\in{SP}_{\psi}$.

Given an instance $C$ of MCP, a profile is $C$-valid (or just valid) if it satisfies every constraint. A sequence of valid profiles is also called valid sequence.

Intuitively, let us take the case of existential constraints. In the o-graph we aim to reconstruct from a sequence of profiles, the clause $A_{i}$ will correspond to an output position $p$ with origin $i$, and the clause $A_{j}$ will refer to an output position $p^{\prime}$ with origin $i^{\prime}$ produced before or after $i$ (depending on $v$) which is a witness $p$ and the constraint $(\gamma^{\prime},d,\psi)$, because the fact that $R\cap{SP}_{\psi}\neq\emptyset$ indicates that there is an accepting run of $A_{\psi}$ on the input word which selects the pair $(i,i^{\prime})$, i.e. $(i,i^{\prime})$ satisfies the MSO-condition $\psi$.

C.3. Properties of profile sequences

C.3.1. Profile consistency

Consistency is first defined between two consecutive profiles, ensuring consistent run information between the clauses of these two consecutive profiles.Then the consistency of every pair of successive profiles in a given sequence ensures a global consistency allowing to reconstruct full runs of $A_{\Psi}$ on the whole input.

We now need a central notion, that of successor (and predecessor) of clauses. Informally, a clause $A^{\prime}$ is a successor of $A$ if there is a o-graph and an input position $k$ such that in the full profiles $\lambda^{f},\lambda^{f}_{k+1}$ of positions $k$ and $k+1$ respectively, there exists $i$ such that $A$ is the $i$th clause of $\lambda^{f}_{k}$ and $A^{\prime}$ is the $i$th clause of $\lambda^{f}{k+1}$. This is just an intuition, and as a matter of fact a consequence of the formal definition, which is more constructive and not dependent on o-graphs.

Let us now give here the formal definitions concerning consistency of profiles. To do so, we first define a successor relation between clauses, parameterized by two sets $S,S^{\prime}\subseteq S_{\Psi}$ (we remind that $S_{\Psi}$ is disjoint union of the set of states $Q_{\psi}$ of all predicate automata). Informally, since a clause occurring at input position $k$ stores information about some output position (whose origin is either $k$, $k^{\prime}<k$ or $k^{\prime}>k$), the successor relation tells us how this information is updated at input position $k+1$, depending on these cases. We will use the following notation $s^{\prime}\in s\cdot\sigma$ whenever there exists a transition of $A_{\Psi}$ from state $s$ to $s^{\prime}$ on $\sigma$. We will also say that a pair of binary relations $(R,R^{\prime})$ on $S_{\Psi}$ is compatible with $\sigma$ if for all $(p,q)\in R$, there exists $(p^{\prime},q)\in R^{\prime}$ such that $p^{\prime}\in p\cdot\sigma$ and conversely, for all $(p^{\prime},q)\in R^{\prime}$, there exists $(p,q)\in R$ such that $p^{\prime}\in p\cdot\sigma$. Note that if $(R,R^{\prime})$ and $(R,R^{\prime\prime})$ are compatible with $\sigma$, then $(R,R^{\prime}\cup R^{\prime\prime})$ is as well compatible with $\sigma$. Hence, given $R$, there exists maximal relation $R_{m}$ (for inclusion) such that $(R,R_{m})$ is compatible with $\sigma$. Symmetrically, given $R^{\prime}$, there exists a maximal relation $R_{m}$ such that $(R_{m},R^{\prime})$ is compatible with $\sigma$.

Definition 0 (Successors of clauses).

Let $S,S^{\prime}\subseteq S_{\Psi}$, $\sigma\in\Sigma$ and $A$ a clause. The successors of $A$ with respect to $S,S^{\prime}$ and $\sigma$ are clauses $A^{\prime}$ defined as follows:

1. (1)

if $A=(\gamma,\cdot)$, there is a unique successor $A^{\prime}=(\gamma,\{(p^{\prime},p)\in S^{\prime}\times S\mid p^{\prime}\in p\cdot\sigma\},\leftarrow)$, 2. (2)

if $A=(\gamma,R,\leftarrow)$, there is a unique successor $A^{\prime}=(\gamma,R^{\prime},\leftarrow)$ such that $R^{\prime}$ is the maximal relation such that $(R,R^{\prime})$ is compatible with $\sigma$ and $\mathrm{dom}(R^{\prime})\subseteq S^{\prime}$. 3. (3)

if $A=(\gamma,R,\rightarrow)$, there are several possible successors $A^{\prime}$:

1. (a)

either $A^{\prime}=(\gamma,\cdot)$ under the condition that $R=\left\{(p,q)\in S\times S^{\prime}|\ q\in p\cdot\sigma\right\}$ 2. (b)

or $A^{\prime}=(\gamma,R^{\prime},\rightarrow)$ where $\mathrm{dom}(R^{\prime})\subseteq S^{\prime}$ and $R$ is the maximal relation such that $(R,R^{\prime})$ is compatible with $\sigma$.

By extension, given two profiles $\lambda=(\sigma,S,A_{1}\ldots A_{n})$ and $\lambda^{\prime}=(\sigma^{\prime},S^{\prime},A^{\prime}_{1}\ldots A^{\prime}_{n})$, a clause $A_{i}$ and a clause $A^{\prime}_{j}$, we say that $A^{\prime}_{j}$ is a successor of $A_{j}$ with respect to $\lambda,\lambda^{\prime}$ if it is a successor w.r.t. $S,S^{\prime}$ and $\sigma$.

As a remark, we notice that the successor relation is not necessarily functional in the case where $A=(\gamma,R,\rightarrow)$. This is consistent with the following observation. Given the full profile of an input position $k$, two occurrences of a clause $A=(\gamma,R,\rightarrow)$ may describe two output positions $j_{1},j_{2}$ whose origins $k_{1},k_{2}$ are to the right of the current position $k$. If for instance $k_{1}=k+1$ and $k_{2}>k_{1}$, then in the full profile of $k_{1}$, output position $j_{1}$ is described by a clause of the form $(\gamma^{\prime},\cdot)$ while output position $j_{2}$ be a clause of the form $(\gamma^{\prime\prime},R,\rightarrow)$, both clauses being successors of $A$. We also notice that in the profile of $k$ (the abstraction of the full profile), one occurrence, or both, of the clause $A$ may have been deleted.

Similarly, we define the predecessors of a clause $A$ with respect to $S,S^{\prime}$ and $\sigma$ as the set of clauses $B$ such that $A$ is a successor of $B$ with respect to $S,S^{\prime}$ and $\sigma$. We prove the following useful proposition:

Proposition 8**.**

Let $S,S^{\prime}\subseteq S_{\Psi}$, $\sigma\in\Sigma$ and $A$ be a clause of type $(\gamma,R,\rightarrow)$ or $(\gamma,\cdot)$. Then $A$ has a unique predecessor with respect to $S,S^{\prime}$ and $\sigma$.

Symmetrically, if $A$ is of type $(\gamma,R,\leftarrow)$ or $(\gamma,\cdot)$, then $A$ has a unique successor with respect to $S,S^{\prime}$ and $\sigma$

Proof.

The second statement is direct by definition. For the first statement, if $A$ is of the form $(\gamma,\cdot)$, then by definition, the unique predecessor of $A$ is $(\gamma,R,\rightarrow)$ where $R=\left\{(p,q)\in S\times S^{\prime}|\ q\in p\cdot\sigma\right\}$. If $A$ is of the form $(\gamma,R,\rightarrow)$, then suppose there are two different predecessors. They are necessarily of the form $(\gamma,R_{1},\rightarrow)$ and $(\gamma,R_{2},\rightarrow)$ where $R_{1}\neq R_{2}$. Then, neither $R_{1}$ nor $R_{2}$ are maximal relations such that $(R_{i},R)$ is compatible with $\sigma$ (it suffices to take $R_{1}\cup R_{2}$, contradicting the definition of successor 3.a. ∎

The notion of consistency is first defined between two profiles, then extended to sequence of profiles. Between two profiles $\lambda_{1},\lambda_{2}$, consistency is defined as structural properties of a bipartite graph $G_{\lambda_{1},\lambda_{2}}$ which we now define. The vertices of $G_{\lambda_{1},\lambda_{2}}$ are clause occurrences in $\lambda_{1}$ and $\lambda_{2}$, labelled by clauses, and the set of edges is a subset of the successor relation between those occurrences. Formally, let $s_{1}=A_{1}\dots A_{n}$ and $s_{2}=B_{1}\dots B_{m}$ be the sequence of clauses of $\lambda_{1},\lambda_{2}$ respectively. We let $G_{\lambda_{1},\lambda_{2}}=(V,E,\ell:V\rightarrow\mathcal{C})$ where $V=\{1\}\times\{1,\dots,n\}\cup\{2\}\times\{1,\dots,m\}$, where for all $i$, $\ell(1,i)=A_{i}$ and $\ell(2,i)=B_{i}$. We say that $i$ is the smallest occurrence of a clause $A$ in $s_{1}$ if $i=\text{min}\{j\mid A=A_{i}\}$ (and similarly of $s_{2}$, and the notion of greatest occurrence). The set of edges is defined as follows. There is an edge from $(1,i)$ to $(2,j)$ if one of the following condition holds:

1. (1)

$A_{i}$ is of the form $(\gamma,R,\rightarrow)$, $i$ is the smallest (resp. greatest) occurence of $A_{i}$ in $s_{1}$, and $j$ is the smallest index (resp. greatest index) such that $B_{j}$ is a successor of $A_{i}$ w.r.t. $\lambda_{1},\lambda_{2}$. 2. (2)

$B_{j}$ is of the form $(\gamma,R,\leftarrow)$, $j$ is the smallest (resp. greatest) occurence of $B_{j}$ in $s_{2}$, and $i$ is the smallest index (resp. greatest index) such that $A_{i}$ is a predecessor of $B_{i}$ w.r.t. $\lambda_{1},\lambda_{2}$.

We can now define consistency:

Definition 0 (Profile consistency).

A profile $\lambda_{1}=(\sigma_{1},S_{1},A_{1}\dots A_{n})$ is consistent with a profile $\lambda_{2}=(\sigma_{2},S_{2},B_{1}\dots B_{m})$ if the following three conditions hold:

1. (1)

for any state $s_{1}\in S_{1}$, there is a state $s_{2}\in S_{2}$ such that $s_{2}\in s_{1}\cdot\sigma_{1}$ and conversely for all $s_{2}\in S_{2}$, there exists $s_{1}\in S_{1}$ such that $s_{2}\in s_{1}\cdot\sigma_{1}$, 2. (2)

for all clause $A_{i}$, there exists $B_{j}$ such that $B_{j}$ is a successor of $A_{i}$, and conversely for all clause $B_{j}$, there exists $A_{i}$ such that $A_{i}$ is a predecessor of $B_{j}$, 3. (3)

the graph $G_{\lambda_{1},\lambda_{2}}$ does not contain the following patterns:

1. (a)

a vertex with two outgoing edges 2. (b)

a vertex with two ingoing edges 3. (c)

a crossing, i.e. two edges $((1,i_{1}),(2,j_{1}))$ and $((1,i_{2}),(2,j_{2}))$ such that $i_{1}<i_{2}$ and $j_{2}<j_{1}$.

A profile $\lambda=(\sigma,S,A_{1}\ldots A_{n})$ is initial if all states of $S$ are initial states and there is no consistency clause pointing to the left (i.e. clause $(\gamma,R,\leftarrow)$). It is final if for all states $s$ of $S$, we can reach a final state by reading $\sigma$, and there is no consistency clause pointing to the right. A sequence of profiles $\lambda_{1}\ldots\lambda_{n}$ is consistent if $\lambda_{1}$ is initial, $\lambda_{n}$ is final, and for all $i<n$, $\lambda_{i}$ is consistent with $\lambda_{i+1}$.

We generalise the notion of graph associated with two profiles, to sequences of profiles $s=\lambda_{1}\dots\lambda_{n}$. It is the disjoint union of all the graphs $G_{\lambda_{i},\lambda_{i+1}}$ where the second component of $G_{\lambda_{i},\lambda_{i+1}}$ is glued to the first component of $G_{\lambda_{i+1},\lambda_{i+2}}$. Formally, an occurrence of a clause $A$ in $s$ is a pair $(i,j)$ such that $A$ is the $j$th clause of $\lambda_{i}$. Then, we define $G_{s}=(V,E,\ell)$ where $V$ is the set of all clause occurrences, $\ell(i,j)$ is the $j$th clause of $\lambda_{i}$, and for all $1\leq i<n$, there is an edge from $(i,j)$ to $(i+1,j^{\prime})$ in $G_{s}$ iff there is an edge from $(1,j)$ to $(2,j^{\prime})$ in $G_{\lambda_{i},\lambda_{i+1}}$. The following lemma gives some structural properties of this DAG:

Proposition 10**.**

For any consistent sequence of profiles $s$, the following hold true:

1. (1)

$G_{s}$* is a union of disjoint directed paths,* 2. (2)

each maximal directed path $\pi$ of $G_{s}$ is of the form

[TABLE]

where $i,k\geq 0$ and $i+k<n$, $\gamma\in\Gamma$ and the $R_{j}$ are binary relations on $S_{\Psi}$, 3. (3)

there is bijection between local clause occurrences of $s$ and maximal paths of $G_{s}$. Therefore, we identify a local clause occurrence $(i,j)$ with its maximal directed path, which we denote by $\pi_{i,j}$.

Proof.

$(1)$ It is a direct consequence of conditions 3a. and 3b. in the definition of consistency.

$(2)$ First, any path which contains a local clause contains a unique local clause and is necessarily of this form. It is a direct consequence of the definition of the successor relation. Indeed, the successor of a clause of the form $(\gamma,R,\rightarrow)$ are clauses of the form $(\gamma,R^{\prime},\rightarrow)$ or $(\gamma,\cdot)$. The successor of clauses of the form $(\gamma,\cdot)$ is necessarily of the form $(\gamma,R,\leftarrow)$ and the successors of the latter are necessarily of the form $(\gamma,R^{\prime},\leftarrow)$.

It remains to prove that any maximal path contains a local clause. Suppose that it does not contain any local clause. Then, by similar arguments as before, we can show that it contains only clauses of the form $(\gamma,R,\rightarrow)$ or only clauses of the form $(\gamma,R,\leftarrow)$. Let us assume the first case (the other one being symmetric). Suppose that the last two vertices of this path are $(i,j_{1})$ and $(i+1,j_{2})$. If $i+1=n$, then we get a contradiction since $\lambda_{n}$ would not be final (which contradicts the fact that $s$ is supposed to be consistent). Suppose that $i+1<n$, let $A=\ell(i,j_{1})$ and $B=\ell(i+1,j_{2})$ the clauses associated with these vertices. We know that $B$ is a successor of $A$ w.r.t. $\lambda_{i},\lambda_{i+1}$. By definition of $G_{\lambda_{i},\lambda_{i+1}}$, it is even an extremal successor of $A$. Therefore, $(i,j_{2})$ is either the smallest occurrence of $B$ in $\lambda_{i+1}$ or the greatest one. By definition of consistency (second condition), we know that $B$ has necessarily a successor $C$ in $\lambda_{i+2}$, and by definition of $G_{\lambda_{i+1},\lambda_{i+2}}$, there must exist an edge from $(i+1,j_{2})$ to some occurrence of $C$ in $\lambda_{i+2}$, contradicting the fact that the considered path is maximal.

$(3)$ It is a direct consequence of $(1)$ and $(2)$. ∎

We now define the notion of maximal consistency for a sequence of profiles. Intuitively a consistent profile sequence is maximal if one cannot add states in the clauses without making it inconsistent.

Definition 0 (Maximality).

A consistent profile sequence $s$, with sequence of $\Sigma$-components $u=\sigma_{1}\dots\sigma_{n}$ and sequence of $S$-components $S_{1}\dots S_{n}$, is maximal if

1. (1)

for all $1\leq i\leq n$, $S_{i}$ is the set of all states $q$ such that there exists an accepting run $q_{1}\dots q_{n+1}$ of $A_{\Psi}$ on $u$ such that $q_{i}=q$, and, 2. (2)

for all local clause occurrence $(i,j)$, for all vertex $(i^{\prime},j^{\prime})$ labelled $(\gamma,R,v)$ on $\pi_{i,j}$, $R$ is the set of all pairs $(p,q)$ such that there exists an accepting run $q_{1}\dots q_{n+1}$ on $u$ satisfying $p=q_{i^{\prime}}$ and $q=q_{i}$.

We call good a sequence of profiles which is maximal, consistent and valid.

C.3.2. Completeness

Given an o-graph $w$, we denote by $\text{Seq}_{C}(w)$ (or just $\text{Seq}(w)$ when $C$ is clear from context) the sequence of $C$-profiles of its input word. In the following, we prove that given an instance $C$ of MCP, the set $\{\text{Seq}_{C}(w)\mid w\models C\}$ is included in the set of valid and maximally consistent sequences of $C$-profiles.

We first show that the profile sequence of an o-graph for an MCP is maximally consistent, while next lemma proves that validity of an o-graph ensures validity of its profile sequence.

Lemma 12.

Given an instance $C$ of MCP and an o-graph $w$, $\text{Seq}_{C}(w)$ is maximally consistent.

Proof.

Let $w=(u,(v,o))$, $\text{Seq}_{C}(w)=\lambda_{1}\ldots\lambda_{n}$, and for all $i$, $\lambda_{i}=(\sigma_{i},S_{i},A_{1}^{i}\ldots A_{m_{i}}^{i})$. Let also $\theta_{i}=(\sigma_{i},S_{i},B_{1}^{i}\dots B_{n_{i}}^{i})$ be the full profile of position $i$.

Consistency

We prove every condition of the definition one by one.

$(1)$ The first condition of the definition of consistency is fulfilled by construction of the sets $S_{k},S_{k+1}$, which are the set of states reached by the accepting runs of $A_{\Psi}$ on the prefixes $\sigma_{1}\dots\sigma_{k-1}$ and $\sigma_{1}\dots\sigma_{k}$ respectively. Clearly, for all $s\in S_{k}$, there exists $s^{\prime}\in s\cdot\sigma_{k}\cap S_{k+1}$ and conversely.

$(2)$ To show the other two conditions, let us define the full graph $G_{w}$ of $w$, whose vertices are clause occurrences of the full profiles of each position respectively. By definition of full profiles, every clause of a full profile of an input position contains information about some output position of $v$, in particular there is a bijection between the clauses of each full profile and the output positions of $v$. In other words, any output position $j$ of $v$ gives rise to a clause $B_{j}^{i}$ in the full profile of input position $i$, for all $i$. We let $trace(j)=B_{j}^{1}\dots B_{j}^{n}$ be the sequence of such clauses, taken in order of input positions. Note that by definition of full profiles, $trace(j)$ is necessarily of the form

[TABLE]

where $\gamma$ is the label of $j$ and $R_{1},\dots,R_{n}\subseteq S_{\Psi}^{2}$. It is not difficult to see that by definition of the successor relation, $B_{j}^{i+1}$ is a successor of $B_{j}^{i}$ with respect to $S_{i},S_{i+1}$ and $\sigma_{i}$, for all $i<n$ and all output position $j$. We can therefore picture the sequence of full profiles of $w$ as follows, where $\xrightarrow{S}$ denote the successor relation:

[TABLE]

It shall now be easy to see that condition (2) of the definition of consistency is fullfiled. Indeed, every clause occurrence in the full profile of position $k$ has at least one successor in the full profile of position $k+1$, and conversely for predecessors. Moreover, the profiles $\lambda_{k},\lambda_{k+1}$ are obtained by $\alpha$-abstraction of the full profiles of positions $k$ and $k+1$ respectively, and $\alpha$-abstraction preserves the set of clauses (i.e. for any full profile $\lambda^{f}$, the set of clauses occurring in $\lambda^{f}$ is the same as the set of clauses occurring in $\alpha(\lambda^{f})$).

$(3)$ Now, to prove the last condition, we formally define the full graph of $w$, which is roughly the labelled DAG given by the traces in the picture. Formally, it is the triple $G_{w}=(V,E,\ell)$ where $V=\{1,\dots,|u|\}\times\{1,\dots,|v|\}$ with $\ell(i,j)=B_{j}^{i}$, and $E=\{(i,j),(i+1,j)\mid 1\leq i<|u|,1\leq j\leq|v|\}$. For all $1\leq i\leq|u|$, let denote by $D_{i}$ the set of clause occurrences $(i,j)$ in $\lambda_{i}$ which are removed by the profile abstraction $\alpha$, i.e. all the $(i,j)$ such that there exist $j_{1}<j<j_{2}$ such that $B_{j_{1}}^{i}=B_{j}^{i}=B_{j_{2}}^{i}$. Let $K=V\setminus(\bigcup_{1\leq i\leq|u|}D_{i})$ (the vertices that are kept by the $\alpha$-abstraction). The subgraph of $G_{w}$ induced by $K$ is defined as the graph obtained by removing all vertices which are not in $K$, and their incoming / outgoing vertices. Let us denote by $G_{K}$ this subgraph.

Claim $G_{\text{Seq}(w)}$ and $G_{K}$ are isomorphic.

The graph $G_{\text{Seq}(w)}$ is obtained from the sequence of profiles of each input position, each profiles being itself obtained by the $\alpha$-abstraction on full profiles, the same operation as the one actually performed on the full graph to obtain $G_{K}$. Hence there exists a natural label-preserving bijection $\mu$ from the set of vertices of $G_{\text{Seq}(w)}$ to the set of vertices $G_{K}$, which preserves the vertical order, in the sense that any two vertices $(i,j_{1})$ and $(i,j_{2})$ of $G_{\text{Seq}(w)}$ satisfy $j_{1}\leq j_{2}$ iff $\mu(i,j_{1})=(i,k_{1})$ and $\mu(i,j_{2})=(i,k_{2})$ satisfy $k_{1}\leq k_{2}$.

We now prove that edges of $G_{K}$ appear in $G_{\text{Seq}(w)}$, and conversely, which concludes the proof of the claim. Let us consider an edge of $G_{K}$, between $(i,j)$ and $(i+1,j)$. Notice that either $\mu^{-1}(i,j)$ is labelled by some $(\gamma,R,\rightarrow)$, or $\mu^{-1}(i+1,j)$ is labelled by some $(\gamma,R,\leftarrow)$. The two cases are symmetrical, we prove only one case, and assume that $\mu^{-1}(i,j)$ is labelled by some clause $(\gamma,R,\rightarrow)$, or equivalently, that the position $i$ of $trace(j)$ is of the form $(\gamma,R,\rightarrow)$. Let us also assume without loss of generality that the position $(i,j)$ of $G_{K}$ corresponds to the maximal occurrence (for the vertical order) of the clause $(\gamma,R,\rightarrow)$ in the $i$th full profile of $w$. The case where it corresponds to the minimal occurrence is, again, symmetrical. Suppose that there is no edge $(\mu^{-1}(i,j),\mu^{-1}(i+1,j))$ in $G_{\text{Seq}(w)}$, we will show a contradiction. The considered vertices and edges are depicted on Fig. 3.

By definition of $G_{\text{Seq}(w)}$, there is necessarily an outgoing edge from $\mu^{-1}(i,j)$, say to a vertex $y$. This vertex $y$ is necessarily above (in the vertical order) as $\mu^{-1}(i+1,j)$, by construction of $G_{\text{Seq}(w)}$. Let $\ell$ be the label of $y$. Since $\ell$ is a successor clause of $(\gamma,R,\rightarrow)$ (according to the definition of successor clauses), $\ell$ is necessarily of the form $(\gamma,R^{\prime},\rightarrow)$ or $(\gamma,\cdot)$. By Prop. 8, $(\gamma,R,\rightarrow)$ is the unique predecessor clause of $\ell$. Now, consider the graph $G_{K}$. The vertex $\mu(y)$ is labelled by $\ell$ and is above $(i+1,j)$, since $\mu$ preserves labels and the vertical order. The vertex $\mu(y)$ has a predecessor (in $G_{k}$), say $x$, which is necessarily labelled by $(\gamma,R,\rightarrow)$. Indeed, as we saw, $\ell$ has a unique predecessor clause, and by definition of $G_{w}$, the edge relation is compatible with the successor clause relation (i.e. if there is an edge $(g,h)$ in $G_{K}$, $g$ is labelled by the clause $c_{1}$ and $h$ by the clause $c_{2}$, then $c_{2}$ is a successor clause of $c_{1}$). Moreover, $x$ is above $(i,j)$ in $G_{K}$, which contradicts the fact that $(i,j)$ was the maximal occurrence of $(\gamma,R,\rightarrow)$ in $G_{K}$. Therefore, $(\mu^{-1}(i,j),\mu^{-1}(i+1,j))$ is an edge of $G_{\text{Seq}(w)}$.

The converse is proved with similar arguments, so we rather sketch the proof than give the full details. Let us consider an edge $(p,q)$ in $G_{\text{Seq}(w)}$ with $p$ labelled by $(\gamma,R,\rightarrow)$ and with $\mu(p)=(i,j)$. Let us assume that $p$ is the maximal occurrence of the clause $(\gamma,R,\rightarrow)$, in the $i$th profile of $w$. Then it must correspond to the maximal position of the $i$th column of $G_{w}$. Then the successor of $(i,j)$ in $G_{w}$ corresponds to the maximal position in the $i+1$th column of $G_{w}$ which is a successor of $(\gamma,R,\rightarrow)$ (otherwise $j$ would not be maximal). Hence the edge $(p,q)$ of $G_{\text{Seq}(w)}$ corresponds to the edge between $(i,j)$ and $(i+1,j)$ in $G_{w}$, which must also appear in $G_{K}$ since its vertices are not deleted.

Clearly in the full graph of $w$, there is no edge with two incoming or two outgoing edges, nor any crossing. Since $G_{K}$ is obtained by removing nodes from the full graph, these properties are transfered to $G_{K}$, and by the claim, to $G_{\text{Seq}(w)}$, proving condition (3) of the consistency definition.

The fact that $\lambda_{1}$ and $\lambda_{n}$ are respectively initial and final are direct consequences of the definition of the profile of an input position.

Maximality

To prove maximality, first, notice that the sets $S_{i}$ are maximal. Assume it is not the case, i.e. there is a sequence $S^{\prime}_{1}\dots S^{\prime}_{n}$ such that $S_{i}\subseteq S^{\prime}_{i}$ for all $i$ and there exists $s\in S^{\prime}_{i}\setminus S_{i}$ for some $i$. Then by condition $1$ of the definition of consistency, we could construct an accepting run of $A_{\psi}$ on $u$, reaching $s$ at position $i$, and by definition of the set $S_{i}$, $s$ would have been already in $S_{i}$.

The second condition of maximality is rather direct from the claim and the definition of the sets $R$ in the profile of an input position. Indeed, by this definition, the sets $R$ are “maximal” in the full graph $G_{w}$, and this property is unchanged when going to $G_{K}$ (since the sets $R$ are not modified). ∎

Lemma 13.

Given an instance $C$ of MCP and $w$ a model of $C$ then $\text{Seq}(w)$ is $C$-valid.

Proof.

Let $C$ be an instance of MCP, let $w=(u,(v,o))$ be a model of $C$ and consider $\text{fullSeq}(w)$ the full profile sequence of $w$. The notion of validity can be extended to full profiles in a natural way (i.e. without changing the definition). It is quite easy to show that if $w$ is a model then $\text{fullSeq}(w)$ is valid. Indeed, by definition, if a profile of $\text{fullSeq}(w)$ violates a universal constraint $(\gamma,\gamma^{\prime},d,\psi)$ this means that we have two clauses $A_{i}=(\gamma,\cdot)$, $A_{j}=(\gamma^{\prime},R,v)$ such that $R\cap{SP}_{\psi}\neq\emptyset$ and $i$ and $j$ respect direction $d$. If we call $i^{\texttt{out}}$ and $j^{\texttt{out}}$ the $i$th and $j$th output positions, then we have that $i^{\texttt{out}}$ and $j^{\texttt{out}}$ violate the universal constraint. Similarly, if the $i$th output position of $w$ labelled by $\gamma$ satisfies an existential constraint $(\gamma,E)$, then there is a triple $(\gamma^{\prime},d,\psi)\in E$ and an output position labelled by $\gamma^{\prime}$, the $j$th, such that they satisfy $d$ and $\psi$.

Now we show that, by construction, going from $\text{fullSeq}(w)$ to $\text{Seq}(w)$ preserves validity. First it is obvious that removing clauses can only increase the chance of satisfying a universal constraint. Secondly we show that if a clause appears in a full profile more than twice, the middle occurrences can be safely removed without removing necessary witnesses for existential constraints. Let us assume that in some profile $(\sigma,S,A_{1}\ldots A_{m})$, a clause $A$ appears at positions $i_{0},\ldots,i_{n+1}$ with $n>0$. We claim that if $A_{i_{j}}$ with $1\leq j\leq n$ is a valid witness of another clause for some existential constraint, then either $A_{i_{0}}$ or $A_{i_{n+1}}$ as well. Going from the full profile to the profile preserves validity. ∎

Remark 14*.*

Note that the converse of the previous lemma is false: there are o-graphs which are not models but whose profile sequence is valid. However we show in the following that a valid sequence of profile is always the profile sequence of some model.

Finally, we obtain the following completeness corollary:

Corollary 15** (Completeness).**

For all models $w$ of an MCP instance $C$, $\text{Seq}(w)$ is good, i.e. it is maximal, consistent and $C$-valid.

C.3.3. Soundness

Given a good sequence of profiles for an MCP instance $C$, i.e. a valid and maximally consistent one, we prove that we are able to construct a valid o-graph of $C$. Its input word is the underlying word of the profile sequence, and the output of a given input position is given by the local clauses of its profile. Since we know what the output positions are, all that is needed to get a valid o-graph is an order over the local clauses in such a way that all constraints are satisfied. By definition of consistency local clauses are bijective with maximal paths. Since a profile is made of a sequence of clauses, the maximal paths meeting at one profile are naturally ordered. Extending this to all profiles leads to a partial order on maximal paths, and hence on local clauses. This partial order has to be verified by any o-graph having this sequence of profiles. We prove that for any total ordering of local clause satisfying this partial order, we are able to construct an o-graph having this sequence of profiles, and that this procedure preserves validity.

Partial order on maximal paths

Given a sequence of profiles $s=\lambda_{1}\dots\lambda_{n}$, we define a relation $\leqdot_{s}$ between maximal paths of $G_{s}$. Formally, $\leqdot_{s}$ is the transitive closure of the relation $\leqdot^{\prime}_{s}$ defined on maximal paths of $G_{s}$ by $\pi\leqdot^{\prime}_{s}\pi^{\prime}$ if there exist a vertex $(i,j_{1})\in\pi$ and a vertex $(i,j_{2})\in\pi^{\prime}$ such that $j_{1}\leq j_{2}$. The order is illustrated on Fig. 3.

Lemma 16.

Given a consistent sequence of profiles $s$, the relation $\leqdot_{s}$ is a partial order on the maximal paths of $G_{s}$.

Proof.

The relation $\leqdot_{s}$ is clearly reflexive and it is transitive by definition. All that remains to prove is that for any two diffrent paths $\pi$ and $\pi^{\prime}$, we do not have $\pi\leqdot_{s}\pi^{\prime}$ and $\pi^{\prime}\leqdot_{s}\pi$. We prove that this situation induces a crossing at some point in the graph. Which concludes the proof since crossing does not happen in a consistent sequence by condition $(3)$ of Proposition 10.

Assume that we have two such different paths $\pi$ and $\pi^{\prime}$. Then there exist two sequences of different paths $(\pi_{k})_{k=1}^{n}$ (resp. $(\pi^{\prime}_{\ell})_{\ell=1}^{m}$) such that $\pi=\pi_{1}\leqdot_{s}\ldots\leqdot_{s}\pi_{n}=\pi^{\prime}$ (resp. $\pi^{\prime}=\pi^{\prime}_{0}\leqdot_{s}\ldots\leqdot_{s}\pi^{\prime}_{m}=\pi$). Moreover, for all $1\leq k<n$ (resp. $\ell<m$), let $i_{k}$ (resp. $i^{\prime}_{\ell}$) be an input position on which we have two positions $j_{k,1}<j_{k,2}$ (resp. $(j^{\prime}_{\ell,1}<j^{\prime}_{\ell,2}$) such that $(i_{k},j_{k,1})\in\pi_{k}$ and $(i_{k},j_{k,2})\in\pi_{k+1}$ (resp. $(i^{\prime}_{\ell},j^{\prime}_{\ell,1})\in\pi^{\prime}_{\ell}$ and $(i^{\prime}_{\ell},j_{\ell,2})\in\pi^{\prime}_{\ell+1}$). Figure 4 illustrates these notations.

We prove that such sequences generate crossings by induction on $n+m$. If $n=m=1$, then the paths $\pi$ and $\pi^{\prime}$ appear one on top on another. In particular, we have that $(i_{1},j_{1,1})$ and $(i^{\prime}_{1},j^{\prime}_{1,2})$ belong to $\pi$, $(i_{1},j_{1,2})$ and $(i^{\prime}_{1},j^{\prime}_{1,1})$ belong to $\pi^{\prime}$, and on $i_{1}$ we have $j_{1,1}<j_{1,2}$ while on $i^{\prime}_{1}$ we have $j^{\prime}_{1,2}>j^{\prime}_{1,1}$. Since the paths are continuous by definition, this induces a crossing between $\pi$ and $\pi^{\prime}$.

Let assume now that $n>1$, and that if two different paths are ordered both ways by $\leqdot_{s}$ by a sequence of length smaller than $n+m$, then there exists a crossing. First, if there is a crossing between $\pi=\pi_{1}$ and $\pi_{2}$, then we get our conclusion. Secondly, if $\pi$ ranges over to $i_{2}$ as defined previously, then there is a clause $(i_{2},j)$ that belongs to $\pi$. If $j>j_{2,1}$, it implies that there is a crossing between $\pi$ and $\pi_{2}$. If $j=j_{2,1}$, then the âths $\pi$ and $\pi_{2}$ have one common node. Since they are different paths, we have a node with at least two ingoing or outgoing arrows, which contradicts the consistency definition. So if $j<j_{2,1}$, then we also have $j<j_{2,2}$ and hence $\pi_{2}$ is not needed in the sequence. We get a strictly smaller witness sequence for $\pi$ and $\pi^{\prime}$, and hence by induction there is a crossing in the subsequence with $\pi_{2}$ deleted.

Now assume that $\pi$ does not range over to $i_{2}$. By transitivity we have that $\pi_{2}\leqdot_{s}\pi^{\prime}$ and $\pi^{\prime}\leqdot_{s}\pi_{2}$. Then if we consider the sequence $(\pi^{\prime}_{\ell})_{\ell=1}^{m}$, the sequence has to pass by $i_{2}$ in order to reach the path $\pi$. In other words, there is a path $\pi^{\prime}_{h}$ that has a node $(i_{2},j_{h})$. If $j_{h}>j_{2,1}$, we get that the sequences $(\pi_{k})_{k=2}^{n}$ and $(\pi^{\prime}_{\ell})_{\ell=1}^{h}$ are respectively witnesses of $\pi_{2}\leqdot_{s}\pi^{\prime}$ and $\pi^{\prime}\leqdot_{s}\pi_{2}$ of length strictly smaller than $n+m$, and hence contain a crossing by induction. If $j_{h}=j_{2,1}$, we have a node with two ingoing or outgoing edges, which contradicts the consistency definition. If $j_{h}<j_{2,1}$, then the sequences $(\pi_{k})_{k=1}^{2}$ and $(\pi^{\prime}_{\ell})_{\ell=h}^{m}$ are a witness of $\pi\leqdot_{s}\pi^{\prime}_{h}$ and $\pi^{\prime}_{h}\leqdot_{s}\pi$ of length strictly smaller than $n+m$, and hence contain a crossing.

∎

We can now prove a soundness result: from any $C$-valid and maximally consistent sequence of profiles $s$, we can reconstruct models of $C$. As we have seen, the elements of the relation $\leqdot_{s}$ are in bijection with the local clause occurrences of $s$. By Lemma 16, the relation $\leqdot_{s}$ is a partial order when $s$ is consistent, and hence can be linearised. We call linearisation of $\leqdot_{s}$ any total order on the elements of $\leqdot_{s}$ which is compatible with this partial order. Since the paths of $\leqdot_{s}$ are in bijection with the local clause occurrences of $s$, any such linearisation $\leq$ induces an output word, and thus an o-graph $(u,(v,o))$. Formally, it is defined by $u$ the sequence of $\sigma$-symbols in $s$, and for any occurrence $(i,j)$ of a local clause $(\gamma,\cdot)$, if the path $\pi_{i,j}$ is the $k$th in the linearisation, then the $k$th position of $v$ is labelled by $\gamma$, and its origin is $o(k)=i$.

The next Lemma proves that for any linearisation of $\leqdot_{s}$, we can construct a model with $s$ as a sequence of profiles that respects the partial order $\leqdot_{s}$.

Lemma 17.

Given an instance $C$ of MCP, a valid and maximally consistent sequence of $C$-profiles $s=\lambda_{1}\ldots\lambda_{n}$, and a linearisation $\leq$ of $\leqdot_{s}$, the o-graph induced by $\leq$ is $C$-valid and verifies $\text{Seq}_{C}(w)=s$.

Proof.

Let $w=(u,(v,o))$ be the o-graph induced by $\leq$ and we set $s^{\prime}=\lambda_{1}^{\prime}\ldots\lambda_{n^{\prime}}^{\prime}$ the sequence of profiles of $w$. We now prove that $s=s^{\prime}$. First, let us remark that by construction the underlying word of $s^{\prime}$ is $u$, and equal to the underlying input word of $s$. Thus $n=n^{\prime}$, and for $k\leq n$, $\sigma_{k}=\sigma_{k}^{\prime}$ and since $s$ is maximal, $S_{k}=S_{k}^{\prime}$. All that is left to show is that for any $k\leq n$, the sequence of clauses of $\lambda_{k}$ is equal to the sequence of $\lambda_{k}^{\prime}$.

The local clauses of $s$ are exactly the output positions of $w$. Then the local clauses of $s^{\prime}$ are exactly the same as the ones of $s$ by construction of $w$, and there is a canonical bijection between the two. Now since $s^{\prime}$ is consistent, each consistency clause belongs to a maximal path that contains exactly one local clause. Let $((i_{\ell},j_{\ell}))_{\ell=1}^{n}$ (resp. $((i_{\ell},j_{\ell}))_{\ell=1}^{m}$) be the sequence of local clauses whose maximal path have a node in the profile $\lambda_{k}$ (resp. $\lambda^{\prime}_{k}$), ordered by their appearance in $\lambda_{k}$ (resp. $\lambda^{\prime}_{k}$). We aim to prove that these two sequences are equal, which would conclude the proof. Indeed, as $s$ and $s^{\prime}$ have the same input word and the same local clauses, each local clause generates the same path of clauses in each sequence profile, and if the profiles of the same input position have consistency clauses belonging to the same sequence of paths, then the sequences of clauses are the same.

First, since $w$ comes from a linearisation of $\leqdot_{s}$, the sequence $((i_{\ell},j_{\ell}))_{\ell=1}^{n}$ appears appear in the same order in $w$, and thus in $s^{\prime}$, and it generates $\lambda_{k}$ as a subsequence of the full profile of $k$ of $w$, i.e. the sequence of all traces of output positions of $w$ on $k$ before suppressing redondancy. Now take a clause $B^{k}_{i}$ of $\lambda_{k}^{\prime}$, and let $B^{k}_{i}=(\gamma,R,v)$. Then $B^{k}_{i}$ is either the minimal or maximal clause $(\gamma,R,v)$ in the full profile of $k$ of $w$. Without loss of generality, assume $B^{k}_{i}$ is minimal. Let $(i_{h},j_{h})$ be the local clause whose maximal path contains $B^{k}_{i}$. Since $s$ and $s^{\prime}$ have the same local clauses, there exists a local clause $(f,g)$ in $s$ which is the bijective image of $(i_{h},j_{h})$. Assume now that the path $\pi_{f,g}$ is not minimal at position $k$ (in $s$). This means there exists an element $e$ of $((i_{\ell},j_{\ell}))_{\ell=1}^{n}$ that generates the clause $(\gamma,R,v)$ on $k$ such that $(i_{e},j_{e})$ is strictly smaller than $(f,g)$ in the $\leqdot_{s}$ order, and hence the local clause bijective to $(i_{e},j_{e})$ in $s^{\prime}$ is smaller than $(i_{h},j_{h})$. But since $\lambda_{k}$ is a subsequence of the full profile of $k$ of $w$, we get that the local clause bijective to $(i_{e},j_{e})$ in $s^{\prime}$ generates a clause $(\gamma,R,v)$ in the full profile of $k$ of $w$ that is smaller than $B^{k}_{i}$, which is a contradiction to the fact that $B^{k}_{i}$ was the minimal occurrence of such a clause in the full profile of $k$ of $w$. Consequently, the clause $B^{k}_{i}$ is associated to the same local clause as the minimal clause $(\gamma,R,v)$ in $\lambda_{k}$ (up to the bijection between local clauses of $s$ and $s^{\prime}$). Applying this to any clause of $\lambda_{k}^{\prime}$, we get that the profiles $\lambda_{k}$ and $\lambda_{k}^{\prime}$ are associated to the same set of local clauses, concluding the proof as explained above.

Now it remains to prove that $w$ is $C$-valid. This is a direct consequence of the facts that its sequence of profiles $s$ is $C$-valid and that the output positions are exactly the local clauses of $s$. Indeed, since if $w$ does not satisfy a universal constraint, then there exists two output positions of $w$ that violates it. Then there exists two local clauses that violate it, and by definition of clauses there is a profile with two clauses that violates this constraint. Since $s$ is $C$-valid, this is not the case, and hence $w$ satisfies all universal constraints. Now given an output position of $w$ and an existential constraint, we know that the associated local clause either does not satisfy the constraint’s label, or it has a valid witness in the form of a clause in its profile. This consistency clause belongs to a maximal path to a local clause whose associated output position is a valid witness, concluding the proof. ∎

C.4. Back to the theorems

In this section, we prove Proposition 3 about the regularity of the input domain of any $\mathcal{L}_{T}$-o-tranduction, a result which we later use to prove our main result (Theorem 5) about the regular synthesis of $\mathcal{L}_{T}$.

The proof of these results rely mainly on the profile approach developped in the previous section. The proof of synthesis unfolds into two major steps. First, we use the profile automaton to create a non-deterministic one-way transducer which associates to an input word the set of its valid sequences of profiles. Then by realising it by a regular function, we associate to each input word a unique sequence of profiles. For the second part, we use some results by Courcelle to prove that any partial order (seen as DAG) can be linearised by some MSO-transduction, i.e. there exist DAG-to-words MSO-transductions that define linearisations.

Let us start with a key lemma. The size of an instance $C=(C_{\exists},C_{\forall})$ of MCP is $|C|=(\sum_{(\gamma,\gamma^{\prime},d,\Psi)\in C_{\forall}}|\Psi|+3)+\sum_{(\gamma,E)\in C_{\exists}}1+\sum_{(\gamma^{\prime},d,\Psi)\in E}2+|\Psi|$, where $|\Psi|$ is the number of symbols of the MSO-formula $\Psi$. If MSO-predicates are given by query automata, then we do not include the size of these automata in the size of $C$, i.e., it is defined as before where $|\Psi|$ is just replaced by [math].

Lemma 18.

Given an instance $C$ of MCP, the set $\{\text{Seq}(w)\mid w\models C\}$ is effectively regular.

Moreover, if the MSO predicates of $C$ are given as query automata, then checking emptiness of $C$ can be done in PSpace in the size of $C$ and ExpSpace in the number of states of the query automata.

Proof.

Let $G$ be the set of $C$-valid and maximally consistent sequences of profiles. We claim that $G=\{\text{Seq}(w)\mid w\models C\}$. If $w\models C$, then $\text{Seq}(w)$ is $C$-valid and maximally consistent by Corollary 15, hence $\text{Seq}(w)\in G$. Conversely, if $\lambda$ is a $C$-valid and maximally consistent sequences of profiles, then take any linearisation $\leq$ of $\leqdot_{s}$. It induces an o-graph $w$ such that $\text{Seq}(w)=\lambda$ and $w\models C$ by Lemma 17. Hence $\lambda\in\{\text{Seq}(w)\mid w\models C\}$.

Then, it suffices to show that $G$ is regular. We construct a single deterministic automaton $\mathcal{A}$ that reads sequences of profiles, and checks validity, consistency and maximality. Validity is a local property that can be checked on the profile read (as long as consistency holds), thus it only corresponds to restricting the profiles that can be read by $\mathcal{A}$ to the valid ones. Consistency and maximality are checked simultaneously. Indeed, consistency requires that clauses of two consecutive profiles are matched, and ensures that the runs appearing in one profile are present in the other one, up to one transition taken by the predicate automaton. Maximality is dual in the sense that once the matching is done by consistency, maximality amounts to check that the runs not considered in one profile do not merge with runs in the other one, and that we cannot globally add any accepting run.

Let us now be more precise. Let Cons (resp. Val) be the set of pairs $(\lambda,\lambda^{\prime})$ of consistent profiles (resp. of $C$-valid profiles). The states of the automaton $\mathcal{A}$ are profiles enriched with some information that allows one to check maximality. First, when $\mathcal{A}$ reads a profile $\lambda\not\in\text{Val}$, it rejects. If from a state consisting of the enrichment of a profile $\lambda$ it reads a profile $\lambda^{\prime}$ such that $(\lambda,\lambda^{\prime})\not\in\text{Cons}$, it rejects as well. Let us now explain what is the extra information added to the profiles. Let $S_{\Psi}$ be the union of the states of the predicate automata. An enrichment of a profile $\lambda=(\sigma,S,A_{1}\dots A_{n})$ is a tuple $\overline{\lambda}=(\sigma,(S,S^{\prime}),C_{1}\dots C_{n})$ such that $S^{\prime}\subseteq S_{\Psi}$ and $C_{i}=(\gamma,\cdot)$ if $A_{i}=(\gamma,\cdot)$, and $C_{i}=(\gamma,(R,R^{\prime}),v)$ for $R^{\prime}\subseteq S_{\Psi}^{2}$ if $A_{i}=(\gamma,R,v)$. The tuple $\overline{\lambda}$ is called an enriched profile. The states of $\mathcal{A}$ are enriched profiles. Intuitively, the set $S^{\prime}$ consists of all states not in $S$ which have been reached so far. If at some point, there exist $\sigma$, a state $s\in S$ and a state $s^{\prime}\in S^{\prime}$, and two transitions from $s$ and $s^{\prime}$ on reading $\sigma$, towards the same state, the automaton rejects (because $s^{\prime}$ could be added to $S$, contradicting its maximality). Otherwise, $S$ and $S^{\prime}$ are updated according to the transitions of the predicate automaton, as for a subset construction. If eventually $\mathcal{A}$ reads the whole word and ends up with some $S^{\prime}$ containing some accepting state, it rejects. Likewise, the information contained in $R^{\prime}$ is used by $\mathcal{A}$ to monitor candidate pairs of states that could be added to $R$.

Formally, suppose $\mathcal{A}$ read some profile $\lambda=(\sigma,S,C_{1}\ldots C_{n})$ and is in some state $\overline{\lambda}$ where we enrich $S$ with $S^{\prime}$ and each clause $(\gamma,R,v)$ is enriched with $R^{\prime}$. Upon reading a profile $\lambda^{\prime\prime}=(\sigma^{\prime\prime},S^{\prime\prime},A_{1}^{\prime\prime}\ldots A_{m}^{\prime\prime})$, if $\lambda^{\prime\prime}\not\in\text{Val}$ or $(\lambda,\lambda^{\prime\prime})\not\in\text{Cons}$, then $\mathcal{A}$ rejects (i.e., there is no transition). Otherwise, let $T=S^{\prime}\cdot\sigma$. If $T\cap S^{\prime\prime}\neq\emptyset$, then $A$ rejects. Otherwise we update $\mathcal{A}$ to the state $(\sigma,(S^{\prime\prime},T),D_{1}\ldots D_{m})$ constructed as follows. Let $j\leq m$, if $C_{i}$ is matched with $A^{\prime\prime}_{j}$ (according to consistency), we define $D_{j}$ in the following way:

• •

if $C_{i}=(\gamma,R,\rightarrow)$ and $A^{\prime\prime}_{j}=(\gamma,R^{\prime\prime},\rightarrow)$, then we set $Q=\left\{(p^{\prime\prime},q)\mid\exists(p^{\prime},q)\in R^{\prime}\wedge p^{\prime\prime}\in p^{\prime}\cdot\sigma\right\}$. If $R^{\prime\prime}\cap Q\neq\emptyset$, then we reject. Otherwise, we set $D_{j}=(\gamma,(R^{\prime\prime},Q),\rightarrow)$.

• •

if $C_{i}=(\gamma,R,\rightarrow)$ and $A^{\prime\prime}_{j}=(\gamma,\cdot)$, then if there is a pair $(p,q)\in R^{\prime}$ where $p\in q\cdot\sigma$ and $q\in S^{\prime\prime}$ we reject, otherwise we set $D_{j}=(\gamma,\cdot)$.

• •

if $C_{i}=(\gamma,\cdot)$ and $A^{\prime\prime}_{j}=(\gamma,R^{\prime\prime},\leftarrow)$, then we define $Q=\left\{(p,q)\mid\exists p\in T\wedge p\in q\cdot\sigma\right\}$. If $R^{\prime\prime}\cap Q\neq\emptyset$, then we reject, otherwise we set $D_{j}=(\gamma,(R^{\prime\prime},Q),\leftarrow)$.

• •

if $C_{i}=(\gamma,R,\leftarrow)$ and $A^{\prime\prime}_{j}=(\gamma,R^{\prime\prime},\leftarrow)$, then we set $Q=\left\{(p^{\prime\prime},q)\mid\exists(p^{\prime},q)\in R^{\prime}\wedge p^{\prime\prime}\in p^{\prime}\cdot\sigma\right\}$. If $R^{\prime\prime}\cap Q\neq\emptyset$, then we reject. Otherwise, we set $D_{j}=(\gamma,(R^{\prime\prime},Q),\leftarrow)$.

The initial state is a special state $init$. The transition from $init$ upon reading a profile $\lambda=(\sigma,S,C_{1}\ldots C_{n})$ exists only if $S$ contains only initial states and for each $C_{i}$ is of the form $(\gamma,\cdot)$ or $(\gamma,R,\rightarrow)$, where the first component of $R$ contains only initial states. This transition goes to state $\overline{\lambda}=(\sigma,(S,S^{\prime}),D_{1}\ldots D_{n})$ where $S^{\prime}$ is the set of all initial states of the query automata that are not in $S$, and $D_{i}=C_{i}$ if $C_{i}=(\gamma,\cdot)$ and $D_{i}=(\gamma,(R,R^{\prime}),\rightarrow)$ where $R^{\prime}=\{(p,q)\mid p\in S^{\prime}\}$ otherwise. The accepting states are the accepting profiles where there is not any addition $S^{\prime}$ or $R^{\prime}$ containing a final state.

The language recognized by $\mathcal{A}$ is exactly the set $G$ of good sequences of profiles. The size of an enriched profile is $1+2^{O(|S_{\Psi}|)}$, because it may contain all pairs of subsets of $S_{\Psi}$. Hence the number of states of $\mathcal{A}$ is doubly exponential in the number of states of $S_{\Psi}$. Constructing this automaton explicitly would give a doubly exponential time algorithm. Instead, we can use the classical NLogSpace emptiness checking algorithm of finite automata by constructing $\mathcal{A}$ on-the-fly. The algorithm needs a counter up to a doubly exponential value (which is singly-exponentially represented). We have to be careful though because constructing the automaton on-the-fly requires to check the properties $\lambda^{\prime\prime}\not\in\text{Val}$ and $(\lambda,\lambda^{\prime\prime})\not\in\text{Cons}$ with a reasonable complexity. Checking validity a profile $\lambda^{\prime\prime}$ requires for each clause of $\lambda^{\prime\prime}$ to scan all constraints of $C$, and possibly again all clauses of $\lambda^{\prime\prime}$ (because constraints of $C$ are between two clauses). Overall, this can be achieved in polynomial time w.r.t. the size of $C$ and of the profile, hence in time polynomial in $|C|$ and exponential in the number of states of the query automata, and so in space polynomial in $|C|$ and exponential in the number of states of the query automata. Consistency between two profiles can be checked with the same complexity. Overall, one obtains a non-deterministic algorithm to check emptiness of $G$, which runs in space polynomial in $|C|$ and exponential in the number of states of the query automata. The result follows since PSpace = NPSpace and NExpSpace = ExpSpace.

∎

We are now able to prove domain regularity.

See 3

Proof.

Let $\varphi\in\mathcal{L}_{T}$. By Proposition 1, there exists a non-erasing o-tranduction definable by some $\mathcal{L}_{T}$-formula $\varphi^{\prime}$ such that $\mathrm{dom}(\llbracket\varphi\rrbracket)=\mathrm{dom}(\llbracket\varphi^{\prime}\rrbracket)$. By Lemma 3, the formula $\varphi^{\prime}$ can in turn be converted into a formula $\varphi^{\prime\prime}$ in SNF which have the same models as $\varphi^{\prime}$, up to some output label morphism. In particular, $\mathrm{dom}(\llbracket\varphi^{\prime}\rrbracket)=\mathrm{dom}(\llbracket\varphi^{\prime\prime}\rrbracket)$. By Proposition 4, the formula $\varphi^{\prime\prime}$ can be transformed into an equivalent set of contraints $C$, i.e. such that any non-erasing o-graph $w$ satisfies $\varphi^{\prime\prime}$ iff it satisfies $C$. Since $\varphi^{\prime}$, and so $\varphi^{\prime\prime}$, are non-erasing, for all o-graphs $w$, $w\models\varphi^{\prime\prime}$ iff $w\models C$. Hence, $\mathrm{dom}(\varphi)=\mathrm{dom}(\varphi^{\prime\prime})=\{u\mid\exists w=(u,(v,o))\cdot w\models C\}$. Now, remind that any profile is of the form $(\sigma,S,A_{1}\dots A_{n})$ where $\sigma$ is an input label. Denote by $\pi_{1}$ the first projection over these tuples. We then have $\mathrm{dom}(\varphi)=\{\pi_{1}(\text{Seq}(w))\mid w\models C\}$, which is regular since by Lemma 18, $\{\text{Seq}(w)\mid w\models C\}$ is regular and regularity is preserved by morphisms (and in particular projection).

Now we can easily extend the result to any $\exists\mathcal{L}_{T}$ formula $\varphi$: If we see the second-order variables as new unary predicates, we obtain a formula $\varphi^{\prime}$ over an extended alphabet. By the above proof, the domain of $\varphi^{\prime}$ is effectively regular, and since regular languages are stable by alphabet projection, we can project away the additional letters and obtain effectively a regular domain for $\varphi$. ∎

See 5

Proof.

To ease the reading the proof, we have divided in several parts.

Preliminaries

First, let us show that we can assume without loss of generality that $\varphi$ defines a non-erasing o-tranduction. Indeed, if it is not the case, then by Proposition 1, $\varphi$ can be converted into a non-erasing $\mathcal{L}_{T}$-o-tranduction $\varphi^{\prime}$ such that $(u,(v,o))\models\varphi$ iff $(u,(v\#u,\texttt{o}^{\prime}))\models\varphi^{\prime}$, where $\texttt{o}^{\prime}$ coincides with o on $v$, maps $\#$ to $1$ and the $i$-th symbol of $u$ to position $i$ in the input. Suppose $\varphi^{\prime}$ is realisable by some MSOT $T$. Then, it is not difficult to transform $T$ into a realisation of $\varphi$. It suffices to compose $T$ with an MSOT $T^{\prime}$ which maps $v\#u$ to $v$ and use closure under composition of MSOT (Courcelle and Engelfriet, 2012) and the fact that closure under composition can be done while preserving origins, as noticed in (Bojanczyk, 2014). Hence, it suffices to show the result for non-erasing $\mathcal{L}_{T}$-o-tranductions.

Let $\varphi$ be a non-erasing $\mathcal{L}_{T}$-sentence over input alphabet $\Sigma$ and output alphabet $\Gamma$. By Lemma 3, one can construct a non-erasing $\mathcal{L}_{T}$-sentence $\varphi^{\prime}$ in Scott normal form, over input alphabet $\Sigma$ and output alphabet $\Gamma\times\Gamma^{\prime}$ which have the same models as $\varphi$ up to projection of $\Gamma\times\Gamma^{\prime}$ on $\Gamma$, i.e. $\llbracket\varphi\rrbracket=\{(u,(\pi_{\Gamma}(v),o))\mid(u,(v,o))\in\llbracket\varphi^{\prime}\rrbracket\}$. Any synthesis of $\varphi^{\prime}$ can be composed with an MSOT which defines the projection on $\Gamma$, and once again we use closure under composition of MSOT to get the result. Therefore, we now focus on realising $\varphi^{\prime}$, and write $\Lambda=\Gamma\times\Gamma^{\prime}$ (hence $\varphi^{\prime}$ defines an o-tranduction from $\Sigma^{*}$ to $\Lambda^{*}$). By Proposition 4, $\varphi^{\prime}$ is equivalent to a system of constraints $C\in\text{MCP}$, in the sense that $\llbracket\varphi^{\prime}\rrbracket_{o}=\llbracket C\rrbracket_{o}$.

General scheme of the proof

We first define four o-transductions, some of them being functional, whose composition has the same domain as $\varphi^{\prime}$ and is included in $\llbracket\varphi^{\prime}\rrbracket_{o}$. Then, by realising in a regular manner all non-functional transductions of this composition, and by composing all syntheses, we will get a regular synthesis of $\llbracket\varphi^{\prime}\rrbracket_{o}$. The four o-transductions are defined as follows (they are denoted with an $f$-symbol when they are functional):

1. (1)

$R_{pro}$ associates with any input word $u$ the set $R_{pro}(u)=\{(\text{Seq}(u,(v,o)),\texttt{o}_{1})\mid(u,(v,o))\models C\wedge\forall i\in\mathrm{dom}(u),\texttt{o}_{1}(i)=i\}$, 2. (2)

$f_{G}$ which associates with any consistent sequence of profiles $s$ the graph $G_{s}$, with origin mapping $\texttt{o}_{2}$ taking any vertex of $G_{s}$ corresponding to an input position $p$ of the sequence $s$, to $p$. 3. (3)

$f_{par}$ which takes $G_{s}=(V,E,\ell)$ as input and outputs the partial order denoted $\leqdot_{s}^{\Gamma}$, obtained by restricting $\leqdot_{s}$ to the nodes labelled in $\Gamma$, i.e. $\leqdot_{s}^{\Gamma}=\leqdot_{s}\cap\{(x,y)\mid\ell(x),\ell(y)\in\Gamma\}$. It corresponds to the partial order depicted in red in Fig. 3, where each maximal path is identified by a single local clause. The origin mapping is the identify: $\texttt{o}_{3}(x)=x$ for any element $x$ of the partial order $\leqdot_{s}^{\Gamma}$. 4. (4)

$R_{lin}$ which inputs $\leqdot_{s}^{\Gamma}$ and outputs all linearisations of it, again with an identity origin mapping $\texttt{o}_{4}$.

Claim Let555Note that we compose here relations with origin information: the origin mappings are as well composed. Formally, for any two relations $R_{1},R_{2}$, and element $u$, we define $(R_{2}\circ R_{1})(u)$ as the set $\{(v,\texttt{o}_{1}\circ\texttt{o}_{2})\mid\exists(v^{\prime},\texttt{o}_{1})\in R_{1}(u),\exists(v,\texttt{o}_{2})\in f_{2}(v^{\prime})\}$ $g=R_{lin}\circ f_{par}\circ f_{G}\circ R_{pro}$. Then,

1. (1)

$\mathrm{dom}(g)=\mathrm{dom}(\varphi^{\prime})$ 2. (2)

for all $u\in\mathrm{dom}(g)$, all $(v,o)\in g(u)$, $(u,(v,o))\in\llbracket\varphi^{\prime}\rrbracket$.

Before proving these two points, note that they imply that any realisation of $g$ which preserves origins is a synthesis of $\llbracket\varphi^{\prime}\rrbracket$.

Let us now prove these two points. Suppose that $u\in\mathrm{dom}(\varphi^{\prime})$, then there exists $(v,o)$ such that $w=(u,(v,o))\models\varphi^{\prime}$, hence $w\models C$ and $\text{Seq}(w)\in R_{pro}(u)$. Since $f_{G}$ is defined for all consistent sequences of profiles, $f_{par}$ is defined for all partial orders and $R_{lin}$ is total, we get that $\text{Seq}(w)\in\mathrm{dom}(R_{lin}\circ f_{par}\circ f_{G})$ and hence $u\in\mathrm{dom}(g)$.

The inclusion $\mathrm{dom}(g)\subseteq\mathrm{dom}(\varphi^{\prime})$ is a consequence of item $2$, so let us prove item 2. Let $u\in\mathrm{dom}(g)$ and $(v,o)\in g(u)$. By definition of $g$, there exists an o-graph $w$ with input $u$, a linearisation $l_{s}$ of $\leqdot^{\Gamma}_{s}$ for $s=\text{Seq}(w)$, and origin mappings $\texttt{o}_{1},\texttt{o}_{2},\texttt{o}_{3},\texttt{o}_{4}$ such that:

• •

$\texttt{o}=\texttt{o}_{1}\circ\texttt{o}_{2}\circ\texttt{o}_{3}\circ\texttt{o}_{4}$

• •

$(s,\texttt{o}_{1})=(\text{Seq}(w),\texttt{o}_{1})\in R_{pro}(u)$ (hence $w\models C$)

• •

$(G_{s},\texttt{o}_{2})=f_{G}(s)$

• •

$(\leqdot_{s}^{\Gamma},\texttt{o}_{3})=f_{par}(G_{s})$

• •

$(v,\texttt{o}_{4})\in R_{lin}(\leqdot_{s})$.

Then, $(u,(v,o))$ is the o-graph induced by some linearisation of $\leqdot_{s}$. Since $w\models C$, then $s=\text{Seq}(w)$ is $C$-valid by Lemma 13. It is also maximally consistent by Lemma 12. Therefore we can apply Lemma 17 and get that $(u,(v,o))\models C$, and so $(u,(v,o))\models\varphi^{\prime}$.

MSOT-definability of $f_{par}$, $f_{G}$ and

MSOT-Synthesis of $R_{pro}$ and $R_{lin}$

Our goal now is to show that the functions $f_{par}$ and $f_{G}$ are MSOT-definable, and that the relation $R_{pro}$ and $R_{lin}$ are realisable by MSOT-definable functions. Conclusion will follow as MSOT transductions are closed under composition (Courcelle and Engelfriet, 2012) and moreover, the composition procedure preserves origins.

MSOT-synthesis of $R_{pro}$. By Lemma 18, the set $\{\text{Seq}(w)\mid w\models C\}$ is regular. It implies that $R_{pro}$ is rational (Jean Berstel, 1979), i.e. is definable by a non-deterministic (one-way) transducer. Indeed, if $B$ is an automaton defining $\{\text{Seq}(w)\mid w\models C\}$, it suffices to turn each of its transitions on a clause $(\sigma,S,A_{1}\dots A_{n})$ into a (transducer) transition on input $\sigma$ producing output $(\sigma,S,A_{1}\dots A_{n})$. It is well-known that rational relations can be realised by rational functions (Jean Berstel, 1979), and most known realisation procedures (for instance based on a lexicographic ordering of runs) preserve origin mappings. We can conclude since rational functions, as a special case of functions definable by two-way deterministic transducers, are MSOT-definable (Engelfriet and Hoogeboom, 2001).

MSOT-definability of $f_{G}$. The function $f_{G}$ inputs a consistent sequence $s$ and outputs $G_{s}$, which is a graph. Hence by MSOT-definability we mean MSOT from string to graphs. We should now make clear how we represent $G_{s}$ as a structure. We use the signature $\mathcal{D}=\{E(x,y),(c(x))_{c\in\mathcal{C}},\rightarrow,\downarrow\}$ where $E$ is the edge relation, $\mathcal{C}$ is the set of clauses, $c\in\mathcal{C}$ are monadic predicates for node labels, $\rightarrow$ and $\downarrow$ are respectively induced by the input order on abscissas of $G_{s}$ and $\downarrow$ by ordinates of $G_{s}$ ($(p_{1},p_{2})\rightarrow(p^{\prime}_{1},p^{\prime}_{2})$ if $p_{1}\leq p^{\prime}_{1}$ and $(p_{1},p_{2})\downarrow(p^{\prime}_{1},p^{\prime}_{2})$ if $p_{2}\leq p^{\prime}_{2}$). Let us now sketch the definition of an MSO-transduction producing $G_{s}$ from $s$: since $s$ is a word and we aim to produce a graph whose nodes are the clause occurrences of $s$, we use as many copies of $s$ as the maximal number $m$ of clause occurrences in a profile of $s$. A copy node $(i,j)$ thus denote the $j$th clause of the $i$th profile of $s$. The predicate $\rightarrow$ is then naturally defined by a formula $\phi_{\rightarrow}^{i,j}(x,y)\equiv x\preceq y$ where $\preceq$ is the linear order on positions of $s$. We also have $\phi_{\downarrow}^{i,j}(x,y)\equiv x=y$ if $i<j$, and $\bot$ otherwise. To define the edge relation, we have to come back to the definition of $G_{s}$. For instance, there is an edge between $x^{i}$ and $y^{j}$ if $y$ is the successor of $x$ in the input sequence $s$, the $i$th clause $A$ of $\lambda_{x}$ is of the form $(\gamma,R,\rightarrow)$, $i$ is the smallest occurrence of $A$ in $\lambda_{x}$, and the $j$th clause $B$ of profile $\lambda_{y}$ is a successor of $A$, according to the definition of the successor relation between clauses, and $j$ is the smallest successor of $A$ in $\lambda_{y}$. Other cases are similar and it shall be clear that all these properties are MSO-definable.

MSOT-definability of $f_{par}$ Now, $f_{par}$ must output a partial order from $G_{s}$. We represent this partial order naturally as a DAG. To implement $R_{lin}$, we also need this DAG to be locally ordered, i.e. all the successors of a node are linearly ordered by some order we denote $\leq_{succ}$. Hence, the output structure is over the signature $\{E(x,y),\leq_{succ},(\gamma(x))_{\gamma\in\Gamma}\}$. Since $f_{par}$ only adds edges, we just take a single copy of the input structure, and we filter the nodes which are not labelled in $\Gamma$ (thanks to monadic MSO formulas). Then, there is an edge between two vertices $(x,y)$ in the DAG iff there was an edge in $G_{s}$ between these two vertices, or there is a vertex $x^{\prime}$ on the maximal path of $x$ in $G_{s}$, and a vertex $y^{\prime}$ on the maximal path of $y$ in $G_{s}$, such that $x^{\prime}\downarrow y^{\prime}$ and $x^{\prime},y^{\prime}$ have the same abscissa, i.e. $x^{\prime}\rightarrow y^{\prime}\wedge y^{\prime}\rightarrow x^{\prime}$. Since connectivity is MSO-definable on graphs, it should be clear that these properties are MSO-definable over $G_{s}$. The local order $\leq_{succ}$ is defined by the formula $\phi_{\leq_{succ}}(x,y)\equiv x\rightarrow y$. Finally, the labels are preserved, hence defined by a formula $\phi_{\gamma}(x)=\gamma(x)$.

MSOT-synthesis of $R_{lin}$ We use a known result by Courcelle (Courcelle, 1996) about MSO-definable topological sorts of graphs. More precisely, it is shown in Theorem 2.1 of (Courcelle, 1996) that there exists an MSOT that, given any locally ordered DAG, produces a linear order of the dag compatible with its edge relation. This MSOT uses only one copy of the input DAG structure, and is defined by some MSO formula $\phi_{<}(x,y)$ over the signature of $\leqdot_{s}^{\Gamma}$, with two free variables, which defines a linearisation $<$ of the DAG. Since one also needs to preserve the labels of the nodes of the DAG, we augment this MSOT with label formulas $\phi_{A}(x)=A(x)$ for all clauses $A$. ∎

Appendix D Data words

See 2

Proof.

The first part of the statement is a direct consequence of the definition of t2d. We now focus on the equivalence of logics.

Let $\varphi$ be an $\mathcal{L}_{T}$-sentence defining a non-erasing transduction, we want to obtain an $\mathcal{L}_{D}$-sentence $\phi$ defining its encoding as a typed data word. First we transform $\varphi$ into $\varphi^{\prime}$ a formula where all quantifications are either input or output quantifications. This can be done inductively on $\mathcal{L}_{T}$-formula by replacing $\exists x\ F(x)$ by $\exists^{\texttt{in}}x\ F(x)\vee\exists^{\texttt{out}}x\ F(x)$. Then, we simplify the resulting formula by removing inconsistent use of variables in the predicates with respect to the type of their quantifiers. For that, we say that the occurrence of a term $t$ is of type in if it is equal to $x$ where $x$ is quantified over the input, or of the form $\texttt{o}(t^{\prime})$ for some term $t^{\prime}$. It is of type out if $t=x$ for $x$ a variable quantified over the output. Now, we replace in $\phi$ all occurrences of the following atoms by $\bot$ under the following conditions:

• •

the atom is $\gamma(t)$, for $\gamma\in\Gamma$, and $t$ is not of type out,

• •

the atom is $t_{1}\mathrel{\leq_{\texttt{out}}}t_{2}$ and some $t_{i}$ is not of type out,

• •

the atom is $\{\psi\}(t_{1},t_{2})$ and some $t_{i}$ is not of type in.

By doing this we obtain a new formula which is equivalent to $\phi$, and makes a consistent use of its variables. We do not give a name to this new formula and rather assume that $\phi$ satisfies this property.

Then, we do the following replacement in $\phi$ to transform it into an equivalent $\mathcal{L}_{D}$-formula. First, similarly to the bijection t2d in which the origin of a position becomes its data value, any term of the form $\texttt{o}^{n}(x)$ is replaced by $x$. Then, any occurrence of an MSO predicate $\{\psi\}(x,y)$ is replaced by $\{\psi^{\prime}\}(x,y)$, where $\psi^{\prime}$ is obtained by replacing in $\psi$ all atoms of the form $x\mathrel{\leq_{\texttt{in}}}y$ by $x\preceq y$. We also replace the atom of the form $x\mathrel{\leq_{\texttt{out}}}y$ by $x\leq y$. If we denote by $\phi^{\prime}$ the obtained formula, by construction we have $(u,(v,o))\models\phi$ iff $\text{t2d}(u,(v,o))\models\phi^{\prime}$.

Example 1.

For instance, consider the following formula $\phi$:

[TABLE]

where $\sigma\in\Sigma$. It expresses the fact for any input position labelled $\sigma$, there is another input position before which is the origin of some output position. First, note that $\forall x\ \psi$ being a shortcut for $\neg\exists x\ \neg\psi$, the first replacement by typed quantifiers gives the formula $\forall^{\texttt{in}}x\ \psi\wedge\forall^{\texttt{out}}x\ \psi$. Then, the first rewriting step of $\phi$ gives:

[TABLE]

After the simplification step according to types, we get:

[TABLE]

which could be again simplified into:

[TABLE]

Then, according to all the replacement rules, one gets the $\mathcal{L}_{D}$-formula

[TABLE]

which expresses that for all positions $x$, if the data type of $x$ is $\sigma$, then there is a position $y$ whose data is smaller than that of $x$.

The converse is slightly easier, since we do not have to deal with inconsistent use of variables. Any $\mathcal{L}_{D}$-sentence $\psi$ is converted into an $\mathcal{L}_{T}$-sentence $\psi^{\prime}$ by doing the following replacements:

• •

any quantifier $\exists$ is replaced by $\exists^{\texttt{out}}$ (any variable is assumed to be quantified over outputs)

• •

$x\leq y$ is replaced by $x\leq_{\texttt{out}}y$

• •

predicates $\{\phi\}(x,y)$ are replaced by $\{\phi^{\prime}\}(\texttt{o}(x),\texttt{o}(y))$ where $\phi^{\prime}$ is obtained from $\phi$ by replacing $\preceq$ by $\leq_{\texttt{in}}$.

By construction, a typed data word $w$ satisfies $\psi$ iff $\text{t2d}^{-1}(w)$ satisfies $\psi^{\prime}$.

∎

Appendix E Complexity of satisfiability

See 1

Proof.

Let us first remark that the complexity of $\mathcal{L}_{D}$ and $\mathcal{L}_{T}$ is equivalent since the translation between the two is linear. Moreover, since the logic $\text{FO}^{2}[\Gamma,\preceq,S_{\preceq},\leq]$ is ExpSpace-complete (Schwentick and Zeume, 2012), we get ExpSpace-hardness as $\mathcal{L}_{D}$ strictly extends this logic.

Let us now prove the ExpSpace solvability of $\mathcal{L}_{T}$. As stated by Lemma 18, satisfiability of an MCP instance $C$ can be solved in ExpSpace with respect to the number of states in the query automata and in PSpace with respect to the size of $C$. Now given a formula in Scott Normal Form, we obtain a MCP instances $C$ whose size is linear in the size of the output alphabet and the size of the query automata. However, the construction from a formula of $\mathcal{L}_{T}$ to a formula in Scott Normal Form trades each quantification for a unary predicate, whichis then incorporated into the extended alphabet of the SNF formula. Since these predicates are not mutually exclusive, this results in an exponential blow up of the output alphabet, and hence an exponential number of constraints, while using the same query automata. Combining this and the complexity result from Lemma 18, we get an ExpSpace complexity for the satisfiability of $\mathcal{L}_{T}$, and hence $\mathcal{L}_{D}$.

∎

Appendix F Extensions of $\exists\mathcal{L}_{T}$

Existential $\mathcal{L}_{T}$

See 1

Proof.

Here the proof is exactly the same as the one of Theorem 1 where the existentially quantified monadic predicates play the role of the parameters. ∎

See 2

Proof.

The synthesis result of $\mathcal{L}_{T}$ can be extended to any $\exists\mathcal{L}_{T}$ formula $\psi=\exists X_{1}\ldots X_{n}\phi$: if we consider the monadic second-order variables as additional unary predicates, we obtain a formula $\phi$ over a signature extended with new unary predicates. Using Theorem 5, we are able to obtain, for instance, a deterministic two-way transducer $T$ realising $\phi$ but over an extended alphabet. By projecting back to the original alphabets what we obtain is a non-deterministic two-way transducer $\overline{T}$ realizing a relation included in $\llbracket\varphi\rrbracket$ and with the same domain. We can then make $\overline{T}$ deterministic using the result of (de Souza, 2013) – or even reversible using (Dartois et al., 2017) – and thus obtain a synthesis of $\psi$.

∎

See 3

Proof.

The main idea is to show that the satisfiability problem for the $\forall\mathcal{L}_{T}$ logic, i.e. formulas with a block of universal monadic quantifications followed by an $\mathcal{L}_{T}$-formula, is undecidable. To this end we encode the same transduction as in the proof of Proposition 2. We re-use the notations and definitions of the proof of Proposition 2 and our goal is to define a sentence $\psi$ defining the same transduction as $\phi$ as: $\psi\equiv\forall^{\texttt{out}}X\ \psi_{\text{well-formed}}(X)\wedge\bigwedge_{\ell=1}^{2}\phi_{\text{bij},\ell}\wedge\phi_{\text{ord-pres},\ell}\wedge\phi_{\text{lab-pres},\ell}$. We have left to define $\psi_{\text{well-formed}}(X)$, whose role is to ensure that the output word belongs to the language $(+_{1\leq i\leq n}1(u_{i})2(v_{i}))^{*}$. First we define a predicate which states that $X$ is a contiguous set of positions:

[TABLE]

Similarly, for a word $w\in(A_{1}+A_{2})^{*}$ we define in the logic a new predicate $w(X,x)$ which states that $w$ is a subword of the positions of $X$, starting at position $x$. The predicates are defined by induction. For a letter $\sigma$ and a word $w$: $\sigma(X,x)\equiv\sigma(x)\wedge x\in X$ and $\sigma w(X,x)\equiv\sigma(X,x)\wedge\exists^{\texttt{out}}y\ x<_{\texttt{out}}y\wedge w(X,y)$. Using the same technique, without considering labels, we can define predicates $|X|\bowtie i$ for any integer $i$ and $\bowtie\in\left\{<,>,\leq,\geq,=\right\}$. We also define $w(X)\equiv\exists^{\texttt{out}}x\ w(X,x)\wedge|X|=|w|$. Let $m=\max\left\{|u_{i}|+|v_{i}||\ 1\leq i\leq n\right\}+1$.

We define $F$ as the set of factors of words of the language $(+_{1\leq i\leq n}1(u_{i})2(v_{i}))^{*}$ of size $\leq m$, i.e. the set of acceptable output factors of length less than $m$. We also define $P$ as the set of words in $(+_{1\leq i\leq n}1(u_{i})2(v_{i}))A_{1}$ and $S$ as the set $A_{2}(+_{1\leq i\leq n}1(u_{i})2(v_{i}))$. Let $\min(X)$ and $\max(X)$ denote that the minimum, and respectively the maximum, position of the word belongs to $X$.

[TABLE]

Note that this formula does not consider the solutions of size one of the PCP instance, which is not a problem since if $u_{i}=v_{i}$ is a solution, then so is $u_{i}u_{i}=v_{i}v_{i}$. Intuitively, $\forall^{\texttt{out}}X\ \psi_{\text{well-formed}}(X)$ ensures that all factors (up to some length) of the output, the prefix and the suffix are of the correct form, which guarantees that the output word is indeed in the language $(+_{1\leq i\leq n}1(u_{i})2(v_{i}))^{*}$. ∎

Single-origin predicates

See 4

Proof.

Let us consider a one-way non-deterministic transducer $T$. Our goal is to define a formula of $\mathcal{L}_{T}^{\mathrm{so}}$ defining the same transduction. We can see $T$ as a deterministic automaton over the alphabet $\Sigma\uplus\Gamma$, with a state space $Q$, initial state $q_{0}\in Q$, set of final states $F\subseteq Q$. For a state $q\in Q$ and a letter $a\in\Sigma\uplus\Gamma$, we denote by $q{\cdot}a$ the state reached upon reading the letter $a$ from state $q$. In order to simplify the proof, and without loss of generality, we assume that the initial state $q_{0}$ has to read an input letter. We see $T$ as a transduction with the following semantics: let $a_{1}v_{1}\cdots a_{n}v_{n}$ be a word accepted by $T$ such that for $1\leq i\leq n$ we have $a_{i}\in\Sigma$ and $v_{i}\in\Gamma^{*}$. We define $(u,(v,o))$ with $u=a_{1}\cdots a_{n}$, $v=v_{1}\cdots v_{n}$ and for $|v_{1}\cdots v_{j-1}|<i\leq|v_{1}\cdots v_{j}|$, $o(i)=j$. Then we have $(u,(v,o))\in\llbracket T\rrbracket_{o}$. Let $p,q\in Q$ and let $L_{p,q}$ denote the set of words of $\Gamma^{*}$ which go from $p$ to $q$. We define the $\mathcal{L}_{T}^{\mathrm{so}}$-formula $\phi_{\mathrm{pres}}\wedge\{\exists_{p,q,r\in Q}\ X^{p}_{q,r}\phi\}$, with $\phi_{\mathrm{pres}}$ the same formula defined in Example 2. The formula $\phi$ will be a conjunction of four formulas: $\phi_{var}\wedge\phi_{succ}\wedge\phi_{min}\wedge\phi_{max}$. The formula $\phi_{var}$ will encode that each variable $X^{p}_{q,r}$ contains the input positions which can go from $p$ to $q$ upon reading the letter and then produce a word in $L_{q,r}$. The formula $\phi_{succ}$ encodes that two successive input positions must belong to some $X^{p}_{q,r}$ and $X^{r}_{s,t}$ respectively. The $\phi_{min}$ formula states that the first input position starts in the initial state and $\phi_{max}$ that the last input position produces a word which goes to some accepting state.

[TABLE]

∎

See 5

Proof.

Here we sketch how to synthesise a regular function from an $\mathcal{L}_{T}^{\mathrm{so}}$ formula $\phi$. The extension to $\exists\mathcal{L}_{T}^{\mathrm{so}}$ follows by the same procedure as Proposition 2. The idea is to view $\llbracket\phi\rrbracket_{o}$ as the composition of two transductions $\tau_{2}\circ\tau_{1}$, with $\tau_{1}$ being rational (i.e. given by a one-way transducer), and $\tau_{2}$ being an $\mathcal{L}_{T}$-transduction. We first synthesise $f_{2}$, realising $\tau_{2}$, using Theorem 5. Then the restriction $\tau_{1}^{\prime}$ of $\tau_{1}$ to $\Sigma^{*}\times dom(f_{2})$ is also rational since $f_{2}$ has a regular domain. Using (Elgot and Mezei, 1965), we can then synthesise $f_{1}$, realising $\tau_{1}^{\prime}$, and the composition $f_{2}\circ f_{1}$ realises the original formula $\phi$. The transduction $\tau_{1}$ is just a rational transduction which after a letter $a\in\Sigma$ produces an arbitrary word of $a\Gamma^{*}$. The idea is that now the single-origin predicates can talk directly about the input and in Fig. 5 we give an example of what $\tau_{2}$ is supposed to do. We transform $\phi$ syntactically into an $\mathcal{L}_{T}$-formula $\phi^{\prime}$ over an enriched signature, with the input alphabet being now $\Sigma\uplus\Gamma$ (we actually use a distinct copy of $\Gamma$ but don’t write it differently for simplicity). We need to define a binary input predicate which relates input positions labelled in $\Gamma$ to the previous input position labelled by $\Sigma$, i.e. its “origin” with respect to $\tau_{1}$ (which we call its virtual origin):

[TABLE]

For any regular language $L$ over $\Gamma^{*}$ we denote by $\phi_{L}$ the MSO formula recognizing it. The syntactic transformation only modifies the input predicates and is done in three steps:

1. We guard all quantifications such that they only talk about positions labelled in $\Sigma$, $(\exists^{\texttt{in}}x\ \psi(x))^{\prime}=\exists^{\texttt{in}}x\ \Sigma(x)\wedge\psi^{\prime}(x)$, $(\forall^{\texttt{in}}x\ \psi(x))^{\prime}=\forall^{\texttt{in}}x\ \Sigma(x)\rightarrow\psi^{\prime}(x)$.

2. The binary predicates of the form $\{P(x,y)\}$ are replaced by $\{\exists^{\texttt{in}}z,t\ \mathrm{vo}(x,z)\wedge\mathrm{vo}(y,t)\wedge P(z,t)\}$.

3. Finally all predicates $L(x)$ are replaced by $\phi_{L}^{\mathrm{vo}(\_,x)}$ where $\mathrm{vo}(\_,x)$ means that all quantifications of $\phi_{L}$ are restricted to positions with virtual origin $x$.

The final formula is $\phi^{\prime}\wedge\phi_{\mathrm{well-formed}}$ where $\phi_{\mathrm{well-formed}}$ states that:

1. The input positions labelled by $\gamma\in\Gamma$ produce exactly one position labelled by $\gamma$

2. The input positions labelled in $\Sigma$ don’t produce anything

3. Given two output positions $x,y$, if there exists an input position $z$ such that $\mathrm{vo}(\texttt{o}(x),z)\wedge\mathrm{vo}(\texttt{o}(y),z)$ then $x\mathrel{\leq_{\texttt{out}}}y\leftrightarrow\texttt{o}(x)\mathrel{\leq_{\texttt{in}}}\texttt{o}(y)$

∎