Register-Bounded Synthesis from Constraint LTL

Program synthesis – the automatic generation of programs from high-level specifications – has emerged as a promising avenue to improve software reliability by producing programs that are correct by construction.

A particularly rich and well-studied area within the field of program synthesis is reactive synthesis [3], which focuses on the design of algorithmic methods for the automatic construction of reactive systems, i.e. systems that maintain ongoing interactions with their environments. Over the past fifteen years, there has been remarkable progress in the synthesis of reactive systems modeled as finite state machines (Mealy machines), from specifications expressed in linear-time temporal logic (LTL). These developments have led to the creation of powerful tools and solvers, whose performance is continuously evaluated through the annual Reactive Synthesis Competition [15].

Classical reactive synthesis methods focus on complex control aspects and typically assume that reactive systems process a finite set of Boolean signals, while ignoring data. More recent research has considered extensions of this purely Boolean setting to data-aware reactive systems. In particular, there is a line of work on the synthesis of infinite-state systems modeled as transducers with registers. In this setting, programs targeted by synthesis algorithms are modeled as a Mealy machine extended with registers that allow storing and comparing incoming data to produce data. In turn, the synthesis problem is parameterized by a data domain, i.e. an infinite set of data values and a finite set of predicates over those data values.

A natural candidate for expressing temporal specifications over data domains is constraint LTL (CLTL), which extends LTL with constraints over data values [9]. CLTL formulas are built over a finite set of variables $X$, which is extended by considering for any variable $x\in X$, $k+1$ copies $x^{(0)},\mathrm{\dots },x^{(k)}$ of $x$. The intended meaning of $x^{(i)}$ is to denote the content of $x$ in $i$ steps. The syntax of CLTL formulas is defined as for LTL, except that atomic formulas are predicates over the (copied) variables. As an example, the CLTL formula $G(x^{(0)}=y^{(2)})$ is satisfied if, at any instant $t$, $x$ holds the same data value as $y$ at instant $t+2$. Over a set of data values $𝔻$, models of CLTL formulas are sequences of valuations ${(X\to 𝔻)}^{\omega }$. It is worth noting that the satisfiability of a CLTL formula depends on the data domain. For instance, $G(x^{(0)}>x^{(1)})$ is satisfiable in $\mathbb{Z}$ but not in $\mathbb{N}$. The formula is satisfiable in $\mathbb{Q}$ but not in $\mathbb{Z}$.

In an attempt to classify data domains, the completion property has been considered in the literature [9]. For a data domain $𝒟$, it asks that for any satisfiable constraint $C$ (defined as a conjunction of predicates over $𝒟$), any partial valuation satisfying a sub-constraint of $C$ can be extended to a (total) valuation satisfying $C$. For example, the constraint is satisfiable in $\mathbb{Q}$, and any valuation of $x,z$ satisfying can be extended to a valuation of $x,y,z$ satisfying $C_0$, e.g. by taking $y=(x+z)/2$. While any domain $(𝔻,=)$ and the domain satisfy the completion property, important data domains such as and do not. As an example, the partial valuation $x=0,z=1$, which satisfies , cannot be extended to a valuation that satisfies $C_0$.

While the satisfiability problem for CLTL (over various data domains) has been quite studied in the literature [5, 9] (see also the survey [7] and the references therein), not much is known about the synthesis problem. In this context, the set of variables is further divided into variables $𝕀$ controlled by the environment (input variables) and variables $𝕆$ controlled by the system (output variables). The synthesis problem from specifications expressed in CLTL has been studied in [2]. It consists in deciding whether there exists a strategy that, at each step, reads data values of $𝕀$, and outputs data values for $𝕆$, resulting in an infinite data word over $𝕀\cup 𝕆$ that satisfies the CLTL formula. It is shown that over data domains with the completion property, CLTL synthesis is decidable. However, synthesis is shown to be undecidable for . To recover decidability, the authors of [2] consider some restriction, called single-sidedness, in which the power of the environment is restricted. In this paper, we take an orthogonal route to recover decidability.

While [2] considers arbitrary strategies, we focus on strategies represented by register transducers. A register transducer successively receives as input a valuation $(𝕀\to 𝒟)$, compares it with the data values stored in its registers, assigns some of the input values to its registers (or none), and finally produces some output valuation $(𝕆\to 𝒟)$ by assigning to each variable in $𝕆$ the content of some register. These strategies are more amenable to implementations, as they are close to real programs. We consider the register-bounded synthesis problem from $\mathrm{𝖢𝖫𝖳𝖫}$, defined as the problem of deciding, given as input a $\mathrm{𝖢𝖫𝖳𝖫}$ formula $\mathrm{\Phi }$ over $𝒟$ and some integer $r$, whether there exists a transducer with $r$ registers which realizes $\mathrm{\Phi }$ (and in that case output it). As we show, bounding the number of registers (but not the number of states) allows to recover decidability for CLTL synthesis over data domains such as . Register-bounded synthesis is also desirable for synthesizing systems with a minimal number of registers. As registers represent some auxiliary memory, this is particularly relevant in contexts where resources are limited.

Our objective is to develop general techniques that allow us to show decidability results for families of data domains. To that end, we develop reductions from the register-bounded synthesis problem to a realizability problem over a finite alphabet. The key in this approach is the analysis of the set ${𝒮}_{𝒟}$ of infinite constraint sequences over $𝒟$ that are satisfiable. Our contributions are as follows.

1. 1.

   We first show that if ${𝒮}_{𝒟}$ is an $\omega$-regular language, then the register-bounded synthesis problem from $\mathrm{𝖢𝖫𝖳𝖫}$ is decidable (Theorem 10). In particular, if a data domain $𝒟$ meets the completion property, then ${𝒮}_{𝒟}$ is $\omega$-regular. This allows us to prove that the register-bounded synthesis problem from CLTL is 2ExpTime-c over any domain $(𝔻,=)$ for an infinite set $𝔻$, and over the domain (Corollary 19).

2. 2.

   Yet, is not $\omega$-regular (see [10]), which reflects the undecidability result mentioned earlier. As a remedy, we show that if ${𝒮}_{𝒟}$ can be over-approximated by an $\omega$-regular language which coincides with ${𝒮}_{𝒟}$ on lasso words, then the register-bounded synthesis problem from $\mathrm{𝖢𝖫𝖳𝖫}$ is decidable (Theorem 22). We show that this is the case for numerous data domains including , , $({\mathrm{\Sigma }}^{\ast },{⪯}_{pref})$ for $\mathrm{\Sigma }$ any finite alphabet and ${⪯}_{pref}$ the prefix relation, as well as for any $k$ and the partial order on tuples (pairwise comparison), using a reduction to [16]. This implies that the register-bounded synthesis problem from CLTL is 2ExpTime-c for all these data domains (Corollary 28).

3. 3.

   Lastly, we consider a partial-observation generalization in which the CLTL formula has private and public input variables, but the system only has access to public ones. We show that our approach can be leveraged to this setting, yielding that the problem is 2ExpTime-c for any domain $(𝔻,=)$, and over the domain (Corollary 32).

Synthesis problems of register transducers over data domains have already been considered in the literature, but mostly when the specification is already given as an automaton, and in particular a register automaton, see [18, 11, 17, 12]. Beyond specifications given by deterministic register automata, synthesis quickly turns into undecidability. That is the case, for instance, for specifications given by non-deterministic or universal register automata [17, 11], which are strictly more expressive than their deterministic restrictions. When considering the data domains and , synthesis is already undecidable for specifications given by deterministic register automata [10].

Register-bounded synthesis has been considered for specifications given as register automata [17, 11, 16]. In particular, for specifications given as universal register automata over $(\mathbb{Z},=)$ and , register-bounded synthesis has been shown to be decidable [17, 12, 16]. A legitimate question is whether register-bounded synthesis from CLTL could be reduced to register-bounded synthesis from register automata and directly apply the results of [17, 12, 16]. We do not know of any reduction that would preserve the number of registers needed to realize the specification. Indeed, even though CLTL formulas can be converted into deterministic register automata, this conversion is however modulo some model encoding: CLTL formulas are interpreted over ${(X\to D)}^{\omega }$ while register automata are executed on words in $D^{\omega }$, and so tuples need to be encoded as chunks of $d=|X|$ consecutive data. Having access to $d$ data at once allows for register succinctness. This is because register transducers in [17, 12, 16] have access to only one data at a time, while the register transducers of this paper receive as input a tuple of data, to match the semantics of CLTL formulas. For example, a CLTL specification might require to output an input value only if it appears twice in a tuple. To check the latter property, a register transducer in [17, 12, 16] would need $d-1$ additional registers.

On top of the related papers already cited before, we would like to mention the work on constraint (infinite) tree automata over , whose emptiness problem is proved to be decidable in [8]. Whereas the connection between tree automata and synthesis is well-known in the boolean setting (see for instance [20]), it is not clear how register-bounded synthesis from constraint LTL could be reduced to the emptiness problem of the constraint tree automata of [8].

Given an alphabet $\mathrm{\Sigma }$ finite or not, let ${\mathrm{\Sigma }}^{\ast }$ (resp. ${\mathrm{\Sigma }}^{\omega }$) be the set of finite (resp. infinite) sequences, called words, over $\mathrm{\Sigma }$. In this paper, we denote finite words as $\overline{u}=u_1{u}_2\mathrm{\dots }{u}_n$ where $u_i\in \mathrm{\Sigma }$ for all $i\in \{1,\mathrm{\dots },n\}$. We let $|\overline{u}|=n$ denote its length and for $1\le i\le j\le |\overline{u}|$, we let ${\overline{u}}_{[i,j]}=u_i{u}_{i+1}\mathrm{\dots }{u}_j$. Similarly, if $\overline{u}=u_1{u}_2\mathrm{\dots }$ is an infinite word, we let ${\overline{u}}_{[i,+\mathrm{\infty }]}=u_i{u}_{i+1}\mathrm{\dots }$ be the infinite suffix starting at position $i$.

We define a data domain $𝒟$ as a tuple $(𝔻,P,d_0)$, where $𝔻$ is an infinite set whose elements are called data, $P$ is a finite set of predicates (relations over $𝔻$ of any arity) and $d_0\in 𝔻$ is a constant. It is also required that the set of predicates always contains the equality predicate, in order to be able to distinguish data values. In this paper, we will mostly use the data domains $(𝔻,=,d_0)$ (where $𝔻$ is arbitrary), and . Note that does not contain equality, but $x=y$ can be expressed as . In general, data domains are defined as interpretations of a set of predicate symbols; however, to simplify the presentation, in this paper we confuse symbols with their (intuitive) semantics. Lastly, we say that a data domain is decidable if its existential first-order theory is decidable.

Let $V$ be a finite set of variables, and let $𝒟=(𝔻,P,d_0)$ be a data domain. A valuation from $V$ to $𝔻$ is a (total) mapping $\nu$ from $V$ to $𝔻$. We extend it to $V\cup \{d_0\}$ by letting $\nu (d_0)=d_0$. We denote by $Va{l}_{V,𝔻}$ the set of valuations from $V$ to $𝔻$. Given two valuations ${\nu }_1,{\nu }_2$ defined over two distinct subsets $A_1,A_2$ of $V$, we let ${\nu }_1\uplus {\nu }_2$ be the valuation defined on $A_1\cup A_2$ by ${\nu }_1\uplus {\nu }_2(x)={\nu }_i(x)$ if $x\in A_i$.

A literal $\mathrm{\ell }$ over $V$ is a term of the form $p(x_1,\mathrm{\dots },x_k)$ or its negation $\neg p(x_1,\mathrm{\dots },x_k)$, with $p\in P$ of arity $k$ and $x_1,\mathrm{\dots },x_k\in V\cup \{d_0\}$. It is satisfied by a valuation $w\in Va{l}_{V,𝔻}$, written $w\vDash \mathrm{\ell }$, if $(w(x_1),\mathrm{\dots },w(x_k))\in p$ if $\mathrm{\ell }=p(x_1,\mathrm{\dots },x_k)$ (and $(w(x_1),\mathrm{\dots },w(x_k))\notin p$ for a negative literal). A constraint $C$ over $V$ is a conjunction of literals over $V$. We often view $C$ as the set of its conjuncts. We denote by ${𝒞}_V$ the set¹¹1Note that constraints may also use the constant symbol $d_0$. This is left implicit in the notation ${𝒞}_V$, for the sake of readability. of constraints over $V$. We say that a constraint $C\in {𝒞}_V$ is satisfiable if there exists a valuation $w\in Va{l}_{V,𝔻}$ such that $w\vDash \mathrm{\ell }$ for all literals $\mathrm{\ell }\in C$. We write $w\vDash C$ when this holds.

A constraint $C$ is consistent if it does not contain a literal and its negation. It is maximally consistent if it is consistent and for all predicates $p$ of arity $k$ and for all $(x_1,\mathrm{\dots },x_k)\in {(V\cup \{d_0\})}^k$, either $p(x_1,\mathrm{\dots },x_k)$ or its negation occurs in $C$. For example over , the constraint is not maximally consistent, but is. We denote by $ℳ{𝒞}_V$ the set of maximally consistent constraints over $V$.

For $V^{\prime }\subseteq V$, we define the restriction ${C|}_{V^{\prime }}$ of a constraint $C$, as the subset of literals of $C$ that use only variables in $V^{\prime }$. A satisfiable constraint $C$ is completable if for any $V^{\prime }\subseteq V$, for all $w^{\prime }\in Va{l}_{V^{\prime },𝔻}$ such that $w^{\prime }\vDash {C|}_{V^{\prime }}$, there exists $w\in Va{l}_{V,𝔻}$ such that $w^{\prime }(x)=w(x)$ for all $x\in V^{\prime }$ and $w\vDash C$.

A data domain has completion property (we also say it is completable) if all satisfiable and maximally consistent constraints are completable. For example, does not meet the completion property: if we consider the constraint $C_1$ defined before, it is satisfiable and maximally consistent. However, the valuation $w^{\prime }$ such that $w^{\prime }(y)=1$ satisfies ${C_1|}_{\{y\}}$, but we cannot find a value $d\in \mathbb{N}$ to map to $x$ such that . However, a slight generalization of Corollary 5.4 in [9] to handle constants yields:

Let $V$ be a finite set of variables and $𝒟=(𝔻,P,d_0)$ be a data domain. A data valuation word is a sequence $\overline{w}=w_1{w}_2\mathrm{\cdots }\in {(Va{l}_{V,𝔻})}^{\omega }$ where each $w_i$ is a valuation. Data valuation words are used to model the traces of the systems that we want to synthesize. As CLTL allows us to compare valuations that occur at different time points, we also introduce another notion of valuation word. Let $k\in \mathbb{N}$, and define the set of $k$-future variables as $V^{(k)}=\{x^{(i)}\mid x\in V,0\le i\le k\}$. A $k$-extended valuation word is a sequence $\overline{\nu }={\nu }_1{\nu }_2\mathrm{\cdots }\in {(Va{l}_{V^{(k)},𝔻})}^{\omega }$. Intuitively, ${\nu }_i(x^{(j)})$ is intended to be the value of $x$ at time $i+j$, and therefore it is required that ${\nu }_i(x^{(j)})={\nu }_{i+j}(x)$. This condition is enforced by the notion of compatible extended valuation words, defined as the sequences $\overline{\nu }\in {(Va{l}_{V^{(k)},𝔻})}^{\omega }$ such that

We define a bijection between valuation words and their compatible $k$-extended form, via the function ${\text{extend}}_k:{(Va{l}_{V,𝔻})}^{\omega }\to {(Va{l}_{V^{(k)},𝔻})}^{\omega }$ defined by ${\text{extend}}_k(\overline{w})=\overline{\nu }$ where for all $j\ge 1$ and all $x^{(i)}\in V^{(k)}$, ${\nu }_j(x^{(i)})=w_{j+i}(x)$. One can show that ${\text{extend}}_k$ is a bijection between valuation words and compatible $k$-extended valuation words, and we denote by compress its inverse. Last, we lift $\uplus$ from valuations to valuation words in the obvious way.

A constraint word is a sequence $\overline{c}=C_1{C}_2\mathrm{\cdots }\in {({𝒞}_V)}^{\omega }$ of constraints over $V$. A valuation word $\overline{w}\in {(Va{l}_{V,𝔻})}^{\omega }$ satisfies $\overline{c}$, written $\overline{w}\vDash \overline{c}$, if for all $i\ge 1,w_i\vDash C_i$. We let $⟦\overline{c}⟧=\{\overline{w}\in {(Va{l}_{V,𝔻})}^{\omega }\mid \overline{w}\vDash \overline{c}\}$. Given $\overline{c^{\prime }}\in {({𝒞}_V)}^{\omega }$, we write $\overline{c}\subseteq \overline{c^{\prime }}$ whenever for all $i\ge 1$, $C_i\subseteq C_i^{\prime }$ (seen as sets of literals). In particular, $\overline{c}\subseteq \overline{c^{\prime }}$ implies $⟦\overline{c^{\prime }}⟧\subseteq ⟦\overline{c}⟧$.

For clarity purposes, we write ${𝒞}_V^{(k)}$ for the set of constraints over $V^{(k)}$ instead of ${𝒞}_{V^{(k)}}$, the same goes for $ℳ{𝒞}_V^{(k)}$. Constraint words in ${𝒞}_V^{(k)}$ are said to be of rank $k$. The satisfiability notion is extended to constraint words $\overline{c}\in {({𝒞}_V^{(k)})}^{\omega }$ of rank $k$ via the function ${\text{extend}}_k$. Formally, $\overline{w}\in {(Va{l}_{V,𝔻})}^{\omega }$ satisfies $\overline{c}$ if ${\text{extend}}_k(\overline{w})$ satisfies $\overline{c}$, and $⟦\overline{c}⟧=\{\overline{w}\in {(Va{l}_{V,𝔻})}^{\omega }\mid \overline{w}\vDash \overline{c}\}$.

Fix a data domain $𝒟=(𝔻,P,d_0)$ and a finite set of variables $V$. $\mathrm{𝖢𝖫𝖳𝖫}(𝒟)$-formulas over $V$ are defined inductively as follows. The atomic formulas of rank $k\ge 0$ are terms of the form $p(x_1,\mathrm{\dots },x_{\mathrm{\ell }})$, where $p\in P$ is a predicate of arity $\mathrm{\ell }$ and $(x_1,\mathrm{\dots },x_{\mathrm{\ell }})\in {(V^{(k)}\cup \{d_0\})}^{\mathrm{\ell }}$. We denote this set by $Ato{m}_k$. $\mathrm{𝖢𝖫𝖳𝖫}$-formulas of rank $k$ are inductively defined as:

A $\mathrm{𝖢𝖫𝖳𝖫}$-formula is a $\mathrm{𝖢𝖫𝖳𝖫}$-formula of rank $k$ for some $k$. As usual, the Boolean connectives $\wedge$ and $\vee$ can be defined from $\Rightarrow$ and $\neg$, and we let $\top =a\vee \neg a$ (for some atomic formula $a$) and $⟂=\neg \top$. Moreover, as for LTL formulas, we define the temporal operators globally ($G$) and eventually ($F$) by $F\mathrm{\Phi }=\top U\mathrm{\Phi }$ and $G\mathrm{\Phi }=\neg F\neg \mathrm{\Phi }$. Finally, we may write $x$ instead of $x^{(0)}$, and just $\mathrm{𝖢𝖫𝖳𝖫}$ instead of $\mathrm{𝖢𝖫𝖳𝖫}$ when $𝒟$ is irrelevant.

The size $|\mathrm{\Phi }|$ of a formula $\mathrm{\Phi }$ is defined as the number of symbols in $\mathrm{\Phi }$, with the exception of variables $x^{(i)}$ that are defined to be of size $i$.

We define the semantics of $\mathrm{𝖢𝖫𝖳𝖫}$ by induction on formulas. Let $\mathrm{\Phi }$ be a $\mathrm{𝖢𝖫𝖳𝖫}$ formula over $V$ of rank $k$, and $\overline{\nu }\in {(Va{l}_{V^{(k)},𝔻})}^{\omega }$. We say that $\overline{\nu }$ satisfies $\mathrm{\Phi }$, written $\overline{\nu }\vDash \mathrm{\Phi }$, if the following holds (inductively):

• $\mathrm{■}$

  if $\mathrm{\Phi }=p(\overrightarrow{x})$ then ${\nu }_1\vDash p(\overrightarrow{x})$

• $\mathrm{■}$

  if $\mathrm{\Phi }=\neg \mathrm{\Psi }$ then $\overline{\nu }\vDash ̸\mathrm{\Psi }$

• $\mathrm{■}$

  if $\mathrm{\Phi }={\mathrm{\Psi }}_1\Rightarrow {\mathrm{\Psi }}_2$ then $\overline{\nu }\vDash ̸{\mathrm{\Psi }}_1$ or $\overline{\nu }\vDash {\mathrm{\Psi }}_2$

• $\mathrm{■}$

  if $\mathrm{\Phi }=X\mathrm{\Psi }$ then ${\nu }_{[2,+\mathrm{\infty }]}\vDash \mathrm{\Psi }$

• $\mathrm{■}$

  if $\mathrm{\Phi }={\mathrm{\Psi }}_{1}U{\mathrm{\Psi }}_2$ then $\exists n\ge 1$ such that ${\overline{\nu }}_{[i,+\mathrm{\infty }]}\vDash {\mathrm{\Psi }}_1$ and ${\overline{\nu }}_{[n,+\mathrm{\infty }]}\vDash {\mathrm{\Psi }}_2$

Given a valuation word $\overline{w}\in {(Va{l}_{V,𝔻})}^{\omega }$, we say that $\overline{w}$ satisfies $\mathrm{\Phi }$, also written $\overline{w}\vDash \mathrm{\Phi }$, if ${\text{extend}}_k(\overline{w})\vDash \mathrm{\Phi }$ holds. We let $L(\mathrm{\Phi })=\{\overline{w}\in {(Va{l}_{V,𝔻})}^{\omega }\mid \overline{w}\vDash \mathrm{\Phi }\}$.

A run of a CA over a valuation word $\overline{w}\in {(Va{l}_{V,𝔻})}^{\omega }$ is a sequence of transitions $\overline{t}\in {\mathrm{\Delta }}^{\omega }$ such that for all $i\ge 1$, $t_i=(q_{i-1},C_i,q_i)$, with $w_i\vDash C_i$ and $q_0\in I$. A run is accepting if the highest color seen infinitely often along the run is even. Under the non-deterministic semantics, the word $\overline{w}$ is accepted if there exists an accepting run. This yields the model of non-deterministic parity CA. The number of priorities of $𝒜$ is the size of $\chi (Q)$. We will also consider a universal semantics: in this case, a word $\overline{w}$ is accepted if all runs on $\overline{w}$ are accepting. An automaton is deterministic if for any two transitions of the form $(q,C_1,p_1)$ and $(q,C_2,p_2)$ such that $p_1\ne p_2$, for all valuation $w\in Va{l}_{V,𝔻}$, either $w\vDash ̸C_1$ or $w\vDash ̸C_2$. We also consider subclasses of CA: we say that an automaton has a Büchi acceptance condition (resp co-Büchi) if all its states have color $1$ or $2$, that is, $\chi (Q)\subseteq \{1,2\}$ (resp $\chi (Q)\subseteq \{0,1\}$). It has a reachability (resp safety) acceptance condition if it has a Büchi (resp co-Büchi) acceptance condition and there exists no transition from a state colored $2$ to a $1$ (resp from $1$ to $0$). Last, the language of a CA $𝒜$ is the set of accepted words, and is denoted $L(𝒜)$.

We call syntactic automaton ${𝒜}_{stx}$ the automaton $𝒜$ seen as a finite automaton over the finite alphabet ${𝒞}_V^{(k)}$ of constraints of rank $k$ and let $L_{stx}(𝒜)=L({𝒜}_{stx})$ denote its language.

It is well-known any LTL sentence can be converted into a Büchi automaton. This result carries over to $\mathrm{𝖢𝖫𝖳𝖫}$ and constraint automata.

The logic $\mathrm{𝖢𝖫𝖳𝖫}$ can be seen as LTL over the finite alphabet ${𝒞}_V^{(k)}$. As such we can use the classical exponential procedure that converts any LTL formula into an equivalent non-deterministic Büchi automaton, to build a non-deterministic Büchi constraint automaton equivalent to the $\mathrm{𝖢𝖫𝖳𝖫}$ formula (see Section 3.2 in [7]). The result follows by applying the latter construction on the negation of the formula and interpreting the resulting automaton with a universal co-Büchi condition. $◀$

First, in order to compare actions of register transducers and constraints of constraint automata, sequences of actions are canonically mapped to sequences of constraints, via a mapping $\text{cstr}:{(Ac{t}_{𝕀,𝕆,R})}^{\omega }\to {({𝒞}_{V\cup R}^{(1)})}^{\omega }$. Remember that an action is a triple $(C,{\rho }^{ass},{\rho }^{out})$ where $C$ is a constraint over $𝕀\cup R$, ${\rho }^{ass}:R\hookrightarrow 𝕀$ is a partial function and ${\rho }^{out}:𝕆\to R$ a function. The latter two assignments induce constraints between $V$ and $R$. It is also worth noting that the register valuation at step $i$ is the one used for the test, while the one at step $i+1$ is the one obtained after the assignment, which is used for producing the output. For example, the assignment ${\rho }^{ass}$ implies that the next content of register $r$ is equal to the value of variable ${\rho }^{ass}(r)$. Similarly, any output variable $y\in 𝕆$ holds a value equal to the next content of register ${\rho }^{out}(y)$. Formally, for all $\overline{a}=(C_1,{\rho }_1^{ass},{\rho }_1^{out})\mathrm{\dots }$, we let $\text{cstr}(\overline{a})=(C_1^{\prime }\wedge init)C_2^{\prime }{C}_3^{\prime }\mathrm{\dots }$ where $init{=}_{def}\left({\displaystyle \underset{r\in R}{\bigwedge }}r=d_0\right)$ and for all $i\ge 1$:

The latter transformation is correct in the following sense:

Since a specification has constraints over $V^{(k)}$, and a register transducer expresses properties of action words, which themselves hold constraints over $V=𝕀\uplus 𝕆$ and $R$, one needs a mechanism to synchronize these two types of constraints. This is done via the following function called extension, denoted $\text{join}:{(Ac{t}_{𝕀,𝕆,R})}^{\omega }\times {({𝒞}_V^{(k)})}^{\omega }\to ℳ{𝒞}_{V\cup R}^{(k)}$, defined for any $\overline{a}\in {(Ac{t}_{𝕀,𝕆,R})}^{\omega }$ and $\overline{c}\in {({𝒞}_V^{(k)})}^{\omega }$ as

Valuations satisfying constraint words in $\text{join}(\overline{a},\overline{c})$, when restricted to variables in $V$, satisfy both $\overline{a}$ and $\overline{c}$. Using Lemma 11, we prove:

The next lemma formalizes the reduction of synthesis from infinite to finite alphabets, and in particular to the alphabet of actions $Ac{t}_{𝕀,𝕆,R}$, which is finite as the set of registers $R$ is finite. In turn, a specification given by a universal coBüchi CA $𝒜$ is translated into a specification ${𝖶}_{𝒜,R}$ over the alphabet $Ac{t}_{𝕀,𝕆,R}$. A finite transducer realizing ${𝖶}_{𝒜,R}$ can then be regarded as a transducer with set of registers $R$. The specification ${𝖶}_{𝒜,R}$ is precisely defined to make sure that the latter register transducer satisfies $L(𝒜)$. Informally, in the finite alphabet specification, an action word $\overline{a}$ is considered to be correct if any constraint word $\overline{c}$ such that both $\overline{a}$ and $\overline{c}$ are satisfiable by the same data valuation word, belongs to $L_{stx}(𝒜)$. Formally, the reduction is ensured by the following transfer lemma:

$\Rightarrow$ Suppose $𝒜$ is realized by some RT $𝕋$, i.e. $L(𝕋)\subseteq L(𝒜)$. We show that ${𝕋}_{stx}$ realizes ${𝖶}_{𝒜,R}$, i.e., $L({𝕋}_{stx})\subseteq {𝖶}_{𝒜,R}$. Let $\overline{a}\in L({𝕋}_{stx})$. Let $\overline{c}\in {({𝒞}_V^{(k)})}^{\omega }$ such that $\exists \overline{c^{\prime }}\in \text{join}(\overline{a},\overline{c})$ and $\overline{c^{\prime }}\in {\mathrm{𝖲𝖠𝖳}}_{k,V\cup R}$. By definition of ${\mathrm{𝖲𝖠𝖳}}_{k,V\cup R}$, there exists $\overline{w}\in {(Va{l}_{V\cup R,𝔻})}^{\omega }$, such that $\overline{w}\vDash \overline{c^{\prime }}$. By Lemma 12, ${\overline{w}|}_V\vDash \overline{a}$ and ${\overline{w}|}_V\vDash \overline{c}$. As $\overline{a}\in L({𝕋}_{stx})$ and ${\overline{w}|}_V\vDash \overline{a}$, we get ${\overline{w}|}_V\in L(𝕋)$, and therefore ${\overline{w}|}_V\in L(𝒜)$. Let $\rho$ be a run of ${𝒜}_{stx}$ on $\overline{c}$. Since ${\overline{w}|}_V\vDash \overline{c}$, we have that $\rho$ is a run of $𝒜$ on ${\overline{w}|}_V$. From ${\overline{w}|}_V\in L(𝒜)$ we find that $\rho$ is accepting. Since this is true for all runs $\rho$ and $𝒜$ has a universal acceptance condition, we finally get $\overline{c}\in L({𝒜}_{stx})$. So, $\overline{a}\in {𝖶}_{𝒜,R}$, by definition of ${𝖶}_{𝒜,R}$. Finally, we have shown that $L({𝕋}_{stx})\subseteq {𝖶}_{𝒜,R}$.

$\Leftarrow$ Suppose ${𝖶}_{𝒜,R}$ is realized by a finite transducer ${𝕋}_f=(Q,I,{\mathrm{\Sigma }}_i,{\mathrm{\Sigma }}_o,\delta )$ where ${\mathrm{\Sigma }}_i=Tes{t}_{𝕀,R}$, ${\mathrm{\Sigma }}_o=Assig{n}_{𝕀,R}\times Outpu{t}_{𝕆,R}$ and $\delta :Q\times Tes{t}_{𝕀,R}\to Assig{n}_{𝕀,R}\times Outpu{t}_{𝕆,R}\times Q$. We have $L({𝕋}_f)\subseteq {𝖶}_{𝒜,R}$. The finite transducer ${𝕋}_f$ can be seen as an $R$-register transducer $𝕋$ over $𝒟$, i.e. such that ${𝕋}_{stx}={𝕋}_f$. We show that $𝕋$ realizes $𝒜$, i.e. $L(𝕋)\subseteq L(𝒜)$.

Let $\overline{w}\in L(𝕋)$. The run of $𝕋$ on $\overline{w}$ induces an action word that we write $\overline{a}$, as well as a word of valuations $\overline{w^{\prime }}\in {(Va{l}_{V\cup R,𝔻})}^{\omega }$ such that ${\overline{w^{\prime }}|}_V=\overline{w}$. We have $\overline{w}\vDash \overline{a}$ by semantics of register transducer. In particular $\overline{a}\in L({𝕋}_f)$. Remember that we want to show $\overline{w}\in L(𝒜)$. Let $\rho$ be a run of $𝒜$ on $\overline{w}$. We let $\overline{c}$ be the constraint word induced by $\rho$, by semantics of constraint word and automata $\overline{w}\vDash \overline{c}$. Let $\overline{c^{\prime }}\in ℳ{𝒞}_{V\cup R}^{(k)}$ the maximally consistent constraint word such that $\overline{w^{\prime }}\vDash \overline{c^{\prime }}$ (it is obtained by choosing for every literal and its negation the one that $\overline{w}$ satisfies). As both $\overline{w}\vDash \overline{a}$ and $\overline{w}\vDash \overline{c}$, by Lemma 12 we have $\overline{c^{\prime }}\in \text{join}(\overline{a},\overline{c})$. Moreover, since $\overline{w^{\prime }}\vDash \overline{c^{\prime }}$, we have $\overline{c^{\prime }}\in {\mathrm{𝖲𝖠𝖳}}_{k,V\cup R}$. As $\overline{a}\in L({𝕋}_f)$, so $\overline{a}\in {𝖶}_{𝒜,R}$ by hypothesis. By definition of ${𝖶}_{𝒜,R}$, we have $\overline{c}\in L({𝒜}_{stx})$. By definition of $\overline{c}$ and since ${𝒜}_{stx}$ is universal, $\rho$ is accepting. As this is true for all runs $\rho$ of $𝒜$ on $\overline{w}$, we get $\overline{w}\in L(𝒜)$. $◀$

The next lemma states that ${𝖶}_{𝒜,R}$ is $\omega$-regular whenever $𝒟$ has regular satisfiability and establishes some complexity bounds on the size of the representation of ${𝖶}_{𝒜,R}$.

We first consider the following definitions/equalities: