Decidable Weighted Expressions with Presburger Combinators

TL;DR

This paper explores the expressive power and decision problems of weighted expressions combining automata and Presburger arithmetic, introducing a decidable class of synchronized expressions despite the undecidability of extensions with Kleene star.

Contribution

It extends existing weighted expression formalism with Presburger combinators, analyzes their decision problems, and introduces a decidable class of synchronized expressions.

Findings

Decision problems are PSpace-complete for the extended expressions.

Extending with Kleene star leads to undecidability.

Synchronized expressions form a decidable and expressive subclass.

Abstract

In this paper, we investigate the expressive power and the algorithmic properties of weighted expressions, which define functions from finite words to integers. First, we consider a slight extension of an expression formalism, introduced by Chatterjee. et. al. in the context of infinite words, by which to combine values given by unambiguous (max,+)-automata, using Presburger arithmetic. We show that important decision problems such as emptiness, universality and comparison are PSpace-c for these expressions. We then investigate the extension of these expressions with Kleene star. This allows to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. The decision problems turn out to be undecidable, but we introduce the decidable and still expressive class of synchronised expressions.

Equations

$$E::=D\mid \min (E_1,E_2)\mid \max (E_1,E_2)\mid E_1+E_2\mid E_1-E_2$$

$$|E(u)-E(v)|\le K\cdot d(u,v)$$

$$|\min (E_1(u),E_2(v))|\le K\cdot d(u,v)$$

$$\begin{array}[]{ll}{}&|E_{1}(u)-E_{2}(v)|\\ =&E_{1}(u)-E_{2}(v)\\ \leq&E_{1}(u)-E_{1}(v)\\ \leq&K_{1}\cdot d(u,v)\\ \leq&\max(K_{1},K_{2})\cdot d(u,v)\\ =&K\cdot d(u,v)\end{array}$$

$$\begin{array}[]{l}\phi(\dots,x_{i,1},\dots,x_{i,m_{i}},\dots,y)=\\ \qquad\exists y_{1},\dots,y_{n}.\;\psi(y_{1},\dots,y_{n},y)\land\bigwedge_{i=1}^{n}\left(\psi_{i}(x_{i,1},\dots,x_{i,m_{i}},y_{i})\right)\end{array}$$

$$\psi (x_1,\dots ,x_n)=\exists x.(x=0\vee x>0)\wedge \varphi (x_1,\dots ,x_n,x)$$

$$\begin{array}[]{l}L_{\mathbb{0}}(M_{A}\cdot M_{\psi})\neq\varnothing\\ \iff\exists u\in L_{\mathbb{0}}(M_{A}).\;(\bigwedge_{i=1}^{n}\nu(x_{i})=M_{A}(u,\mathbb{0})(x_{i}^{+})-M_{A}(u,\mathbb{0})(x_{i}^{-}))\land L_{\nu_{M}}(M_{\psi})\neq\varnothing\\ \iff\exists u\in\bigcap_{i=1}^{n}L_{\mathbb{0}}(M_{i}).\;(\bigwedge_{i=1}^{n}\nu(x_{i})=M_{i}(u,\mathbb{0})(x_{i}^{+})-M_{i}(u,\mathbb{0})(x_{i}^{-}))\land\nu\models\psi\\ \iff\exists u\in\bigcap_{i=1}^{n}L(A_{i}).\;(\bigwedge_{i=1}^{n}\nu(x_{i})=A_{i}(u))\land\exists x.\;x\geq 0\land\phi(\nu(1),\dots,\nu(n),x)\\ \iff\exists u\in\text{dom}(E).\;\exists x.\;x\geq 0\land\phi(A_{1}(u),\dots,A_{n}(u),x)\\ \iff\exists u\in\text{dom}(E).\;E(u)\geq 0\end{array}$$

$$\begin{array}[]{ll}\{w\in\Sigma^{*}\mid w\in\bigcap_{i=1}^{n}L(A_{i})\}=\varnothing&\iff\forall w\in\Sigma^{*},\exists 1\leq i\leq n.\;w\notin L(A_{i})\\ &\iff\forall w\in\Sigma^{*}.\;\min(W_{1}(w),\dots,W_{n}(u))=0\\ \{w\in\Sigma^{*}\mid w\in\bigcap_{i=1}^{n}L(A_{i})\}\neq\varnothing&\iff\exists w\in\Sigma^{*}.\;\min(W_{1}(w),\dots,W_{n}(u))=1\\ &\iff\exists w\in\Sigma^{*}.\;\min(W_{1}(w),\dots,W_{n}(u))-1\geq 0\end{array}$$

$$(q_0,v_0){\delta }_0(q_1,v_1){\delta }_1\dots (q_{n-1},v_{n-1}){\delta }_n(q_n,v_n)$$

$$\begin{array}[]{l}\vdash q_{0}a^{v_{0}(x)}b^{v_{0}(y)}\triangleleft\delta_{0}\triangleright q_{1}a^{v_{1}(x)}b^{v_{1}(y)}\dashv\vdash q_{1}a^{v_{1}(x)}b^{v_{1}(y)}\triangleleft\delta_{1}\triangleright q_{2}a^{v_{2}(x)}b^{v_{2}(y)}\dashv\dots\\ \vdash q_{n-1}a^{v_{n-1}(x)}b^{v_{n-1}(y)}\triangleleft\delta_{n-1}\triangleright q_{n}a^{v_{n}(x)}b^{v_{n}(y)}\dashv\end{array}$$

$$\{a^{|u_1|}\#a^{|u_2|}\#\dots \#a^{|u_n|},a^{|v_1|}\#a^{|v_2|}\#\dots \#a^{|v_n|}\}$$

$$L_1\odot L_2=L(B)=\bigcup _{(q,\overline{q_2})\in Q\times \overline{I_2}}{L}_{q,q_2}{R}_{q,q_2}$$

$$[[\varphi (C_1,\dots ,C_n)]](u)=[[\varphi ]]([[C_1]](u),\dots ,[[C_n]](u))$$

$$\left\{([[C_1]](u),\dots ,[[C_n]](u))\mid u\in \bigcap \text{dom}(C_i)\right\}$$

$$\begin{array}[]{l}\text{dec}_{C_{1}}(u)=(u_{1},(E_{1,1},\dots,E_{1,m})),\dots,(u_{n},(E_{n,1},\dots,E_{n,m}))\\ \text{dec}_{C_{2}}(u)=(u^{\prime}_{1},(E^{\prime}_{1,1},\dots,E^{\prime}_{1,m^{\prime}})),\dots,(u^{\prime}_{n},(E^{\prime}_{n^{\prime},1},\dots,E^{\prime}_{n^{\prime},m^{\prime}}))\end{array}$$

$$S_{p,q}=\text{Range}([[\lambda (p,q)]])=\{[[({\varphi }_1(C_1^1,\dots ,C_{k_1}^1)]](u),\dots ,[[{\varphi }_n(C_1^1,\dots ,C_{k_n}^1)]](u))\mid u\in \Delta (p,q)\}$$

$${\mathbb{E}}^{\prime }=(E_1,\dots ,E_{i-1},F_1,F_2,E_{i+1},\dots ,E_n)$$

$${\mathbb{C}}^{\prime }=(C_1,\dots ,C_{i-1},C_i^1,C_i^2,C_{i+1},\dots ,C_n)$$

$$\mathbb{C}=({\varphi }_{id}(C_1),\dots ,{\varphi }_{id}(C_{i-1}),\varphi (C_i^1,C_i^2),{\varphi }_{id}(C_{i+1}),\dots ,{\varphi }_{id}(C_n))$$

$$\text{dom}(C_i^{⊛})=\text{dom}(C_i{)}^{\#}=\text{dom}(F_j{)}^{\#}=\text{dom}(F_j^{⊛})$$

$$[[C_i^{⊛}]](u)=\sum _{k=1}^p[[C_i]](u_k)=\sum _{k=1}^p[[F_i]](u_k)=[[F_i^{⊛}]](u)$$

$$\text{dom}(F^{\circledast})=\bigcup\left\{L_{q_{0},q_{1}}L_{q_{1},q_{2}}\dots L_{q_{m-1},q_{m}}\begin{array}[]{l|ll}&&q_{0},q_{1},\dots,q_{m}\text{ are states of $B$,}\\ &&\text{$q_{0}$ is initial and $q_{m}$ final}\\ \end{array}\right\}$$

Full text

1 Introduction

Quantitative languages

Quantitative languages (QL), or series, generalise Boolean languages to function from finite words into some semiring. They have recently received a particular attention from the verification community, for their application in modeling system quality [4], lifting classical Boolean verification problems to a quantitative setting. In this paper, we consider the case of integer weights and in this context, the comparison problem asks whether two QL $f,g:\Sigma^{*}\rightarrow\mathbb{Z}$ satisfy $f(u)\leq g(u)$ for all $u\in\Sigma^{*}$. Similarly, the universality ($f\geq\nu$ where $\nu$ is a constant) and equivalence problem ($f=g$) can be defined, as well as emptiness (does there exists a word whose value is above some given threshold). We say that a formalism for QL is decidable if all these problems are decidable. A popular formalism to define QL is that of weighted automata (WA) [7]. However, WA over the semiring $(\mathbb{Z},\max,+)$, called $(\max,+)$-automata, are undecidable [13], even if they are linearly ambiguous $(\max,+)$-automata [6].

Decidable formalisms for quantitative languages and objectives

The largest known class of $(\max,+)$-automata enjoying decidability is that of finitely ambiguous $(\max,+)$-automata, which is also expressively equivalent to the class of finite-valued $(\max,+)$-automata (all the accepting executions over the same input run yields a constant number of different values) [9]. Moreover, $(\max,+)$-automata are not closed under simple operations such as $\min$ and the difference $-$ [12]. Basic functions such as $u\mapsto\min(\#_{a}(u),\#_{b}(u))$ and111$\#_{\sigma}(u)$ is the number of occurrences of $\sigma$ in $u$ (as a consequence) $u\mapsto|f(u)-g(u)|$ are not definable by $(\max,+)$-automata, even if $f,g$ are [12].To cope with the expressivity and undecidability issues, a class of weighted expressions was introduced in [3] in the context of $\omega$-words. Casted to finite words, the idea is to use deterministic $(\max,+)$-automata as atoms, and to combine them using the operations $\max$, $\min$, $+$, and $-$. The decision problems defined before were shown to be PSPace-c [14] over $\omega$-words. One limitation of this formalism, casted to finite words, if that it is not expressive enough to capture finitely ambiguous $(max,+)$-automata, yielding two incomparable classes of QL. In this paper, our objective is to push the expressiveness of weighted expressions as far as possible while retaining decidability, and to capture both finitely ambiguous $(\max,+)$-automata and the expressions of [3], for finite words.

Monolithic expressions with Presburger combinators

We define in Section 3 a class of expressions, inspired from [3], that we call monolithic in contrast to another class of expressions defined in a second contribution. The idea is to use unambiguous $(\max,+)$-automata as atoms, and to combine them using $n$-ary functions definable in Presburger arithmetics (we call them Presburger combinators). Any finitely ambiguous $(\max,+)$-automaton being equivalent to a finite union of unambiguous ones [9], this formalism captures finitely ambiguous $(\max,+)$-automata (using the Presburger combinator $\max)$. We show that all the decision problems are PSpace-c, matching the complexity of [14]. It is important to mention that this complexity result cannot be directly obtained from [14] which is on $\omega$-words with mean-payoff automata as atoms (hence the value of an infinite word is prefix-independent). Moreover, unlike in [14], we can rely on existing results by encoding expressions into reversal-bounded counter machines [11].

Expressions with iterated sum

The previous expressions are monolithic in the sense that first, some values are computed by weighted automata applied on the whole input word, and then these values are combined using Presburger combinators. It is not possible to iterate expressions on factors of the input word, and to aggregate all the values computed on these factors, for instance by a sum operation. The basic operator for iteration is that of Kleene star (extended to quantitative languages), which we call more explicitly iterated sum. It has already been defined in [7], and its unambiguous version considered in [1] to obtain an expression formalism equivalent to unambiguous $(\max,+)$-automata. Inspired by [1], we investigate in Section 4 the extension of monolithic expressions with unambiguous iterated sum, which we just call iterated sum in the paper. The idea is as follows: given an expression $E$ which applies on a domain $D$, the expression $E^{\circledast}$ is defined only on words $u$ that can be uniquely decomposed (hence the name unambiguous) into factors $u_{1}u_{2}\dots u_{n}=u$ such that $u_{i}\in D$, and the value of $u$ is then $\sum_{i=1}^{n}E(u)$. Unfortunately, we show that such an extension yields undecidability (if 2 or more iterated sum operations occur in the expression). The undecidability is caused by the fact that subexpressions $E^{\circledast}$ may decompose the input word in different ways. We therefore define the class of so called synchronised expressions with iterated sum, which forbids this behaviour. We show that while being expressive (for instance, they can define QL beyond finitely ambiguous $(\max,+)$-automata), decidability is recovered. The proof goes via a new weighted automata model (Section 5), called weighted chop automata, that slice the input word into smaller factors, recursively apply smaller chop automata on the factors to compute their values, which are then aggregated by taking their sum. In their synchronised version, we show decidability for chop automata. We finally discuss some extensions in Section 6222Due to lack of space, full proofs are given in Appendix..

2 Quantitative Languages

Words, languages and quantitative languages

Let $\Sigma$ be a finite alphabet and denote by $\Sigma^{*}$ the set of finite words over $\Sigma$, with $\epsilon$ the empty word. Given two words $u,v\in\Sigma^{*}$, $|u|$ and $|v|$ denote their length, and the distance between $u$ and $v$ is defined as $d(u,v)=|u|+|v|-2|\sqcap(u,v)|$, where $\sqcap(u,v)$ denotes the longest common prefix of $u$ and $v$. A quantitative language (QL)333Also called formal series in [7] is a partial function $f:\Sigma^{*}\rightarrow\mathbb{Z}$, whose domain is denoted by $\text{dom}(f)$. E.g., consider the function mapping any word $w\in\Sigma^{*}$ to the number of occurrences $\#_{\sigma}(w)$ of some symbol $\sigma\in\Sigma$ in $w$. A QL $f$ is Lipschitz-continuous if there exists $K\in\mathbb{N}$ such that for all words $u,v\in\Sigma^{*}$, $|f(u)-f(v)|\leq K\cdot d(u,v)$.

Combinators for quantitative languages

Any binary operation $\boxplus:\mathbb{Z}^{2}\rightarrow\mathbb{Z}$ is extended to quantitative languages by $f_{1}\boxplus f_{2}(w)=f_{1}(w)\boxplus f_{2}(w)$ if $w\in\text{dom}(f_{1})\cap\text{dom}(f_{2})$, otherwise it is undefined. We will consider operations defined in existential Presburger logic. An existential Presburger formula (simply called Presburger formula in the sequel) is built over terms $t$ on the signature $\{0,1,+\}\cup X$, where $X$ is a set of variables, as follows: $\phi\ \Coloneqq\ t=t\mid t>t\mid\phi\vee\phi\mid\phi\wedge\phi\mid\exists x.\;\phi$. If a formula $\phi$ has $n+1$ free variables $x_{1},\dots,x_{n+1}$, for all $v_{1},\dots,v_{n+1}\in\mathbb{Z}$, we write $\phi(v_{1},\dots,v_{n+1})$ if $\phi$ holds for the valuation mapping $x_{i}$ to $v_{i}$. When $n\geq 1$, we say that $\phi$ is functional if for all $v_{1},\dots,v_{n}\in\mathbb{Z}$, there exists a unique $v_{n+1}\in\mathbb{Z}$ such that $\phi(v_{1},\dots,v_{n+1})$ holds. Hence, $\phi$ defines a (total) function from $\mathbb{Z}^{n}$ to $\mathbb{Z}$ that we denote $[\![\phi]\!]$. We call $n$ the arity of $\phi$ and may write $\phi(x_{1},\dots,x_{n})$ to denote the unique $x_{n+1}$ such that $\phi(x_{1},\dots,x_{n+1})$ holds. We say that a function $f:\mathbb{Z}^{n}\rightarrow\mathbb{Z}$ is Presburger-definable if there exists a functional Presburger-formula $\phi$ such that $f=[\![\phi]\!]$. E.g., the $\max$ of values $x_{1},\dots,x_{n}$ is definable by $\phi_{\max}(x_{1},\dots,x_{n},x)\equiv(\bigwedge_{i=1}^{n}x_{i}\leq x)\wedge(\bigvee_{i=1}^{n}x_{i}=x)$.

Semi-linear sets

Let $k\geq 1$. A set $S\subseteq\mathbb{Z}^{k}$ is linear if there exist $x_{1},\dots,x_{n}\in\mathbb{Z}^{k}$, called the period vectors, and $x_{0}\in\mathbb{Z}^{k}$, called the base, such that $S=\{x_{0}+\sum_{i=1}^{n}a_{i}x_{i}\mid a_{1},\dots,a_{n}\in\mathbb{N}\}$. $S$ is semi-linear if it is a finite a union of linear sets. Note that the set of base and periodic vectors of each linear set of the union provides a finite representation of $S$. It is a folklore result that a set $S\subseteq\mathbb{Z}^{k}$ is semi-linear iff it is definable by some existential Presburger formula.

Decision problems

In this paper, we are interested by fundamental decision problems on (finite representations of) quantitative languages, namely universality, emptiness and comparison. Given finitely represented quantitative languages $f,f_{1},f_{2}$ and $v\in\mathbb{Z}$,

• •

the $v$-emptiness (resp. $v$-universality) problem asks whether there exists $u\in\text{dom}(f)$ such that $f(u)\succsim v$ (resp. whether all $u\in\text{dom}(f)$ satisfies $f(u)\succsim v$), for $\succsim\ \in\{>,\geq\}$.

• •

the $\succsim$-inclusion problem (denoted $f_{1}\succsim f_{2}$) with $\succsim\ \in\{>,\geq\}$ asks whether $\text{dom}(f_{1})\supseteq\text{dom}(f_{2})$ and for all $w\in\text{dom}(f_{2})$, $f_{1}(w)\succsim f_{2}(w)$.

• •

the equivalence problem, denoted $f_{1}\equiv f_{2}$, asks whether $f_{1}{\geq}f_{2}\wedge f_{2}{\geq}f_{1}$.

Remark 1

For classes of QL (effectively) closed under regular domain restriction and difference, and with decidable domain inclusion, the $v$-universality, inclusion and equivalence problems, are reducible to the [math]-emptiness problem as follows:

to establish $\forall w\in\text{dom}(f):f(w)\geq v$ (universality), it suffices to check that it is not the case that $\exists w\in\text{dom}(f):-(f(w)-v)>0$ ([math]-emptiness). 2. 2.

to establish $\text{dom}(f_{2})\subseteq\text{dom}(f_{1})$ and for all $w\in\text{dom}(f_{2})$, $f_{1}(w)\geq f_{2}(w)$, when the first check succeeds, we reduce the second one as follows: construct a new QL $g$ on $\text{dom}(f_{2})$ such that $\forall w\in\text{dom}(f_{2}):g(w)=f_{2}(w)-f_{1}(w)$ and check that $\forall w\in\text{dom}(f_{2}):g(w)\geq 0$ ([math]-emptiness).

The other variants with strict inequalities are treated similarly. Note also with similar arguments, we can show that the [math]-emptiness problem can be reduced to the universality and the inclusion problems. The quantitative expression formalisms that we define in this paper have those closure properties (in PTime) and so, we concentrate, in most of our results, on the [math]-emptiness problem.

Weighted automata

Weighted automata (WA) have been defined as a representation of QL (more generally with values in a semiring). Here, we consider weighted automata over the semiring $(\mathbb{Z}\cup\{-\infty\},\max,+)$ and just call them weighted automata. They are defined as tuples $M=(A,\lambda)$ where $A=(Q,I,F,\Delta)$ is a finite automaton over $\Sigma$ whose language is denoted by $L(A)$ and $\lambda:\Delta\rightarrow\mathbb{Z}$ is a weight function on transitions. Given a word $w\in L(A)$ and an accepting run $r=q_{1}a_{1}\dots q_{n}a_{n}q_{n+1}$ of $A$ on $w$, the value $V(r)$ of $r$ is defined by $\sum_{i=1}^{n}\lambda(q_{i},a_{i},q_{i+1})$ if $n>1$, and by [math] if444Sometimes, initial and final weight functions are considered in the literature [7], so that non-zero values can be assigned to $\epsilon$ $n=1$. Finally, $M$ defines a quantitative language $[\![M]\!]:L(A)\rightarrow\mathbb{Z}$ such that for all $w\in L(A)$, [\![M]\!](w)=\max\{V(r)\mid r\text{ is an accepting run of A$on$w}\}. $M$ is called deterministic if $A$ is deterministic. We say that $M$ is $k$-ambiguous if $A$ is $k$-ambiguous, i.e. there are at most $k$ accepting runs on words of $L(A)$. A $1$-ambiguous WA is also called unambiguous. $M$ is $k$-valued if for all $w\in L(A)$, the set \{V(r)\mid r\text{ is an accepting run of A$on$w}\} has cardinality at most $k$. In particular, any $k$-ambiguous WA is $k$-valued. The converse also holds, and it is decidable whether a WA is $k$-valued, for a given $k$ [9]. While emptiness is decidable for WA [10], inclusion and universality are undecidable [13]. However, all these problems are decidable for $k$-valued WA, for a fixed $k$ [9].

3 Monolithic Expressions

We start our study of weighted expressions by a definition directly inspired by [3] where weighted automata555Chatterjee et al. studied quantitative expressions on infinite words and the automata that they consider are deterministic mean-payoff automata. are used as building blocs of quantitative expressions that can be inductively composed with functions such as $\min$, $\max$, addition and difference. The equivalence checking problem for those expressions is decidable in PSpace. We start here with deterministic $(\max,+)$-automata as building blocs.

Definition 1

A simple expression (s-expression) is a term $E$ generated by

[TABLE]

where $D$ is a deterministic WA (we remind that by WA we mean $(\max,+)$-automata).

Any s-expression $E$ defines a quantitative language $[\![E]\!]:\Sigma^{*}\rightarrow\mathbb{Z}$ on a domain $\text{dom}(E)$ inductively as follows: if $E\equiv A$, then $\text{dom}(E)=L(A)$ and for all $u\in L(A)$, $[\![E]\!](u)=[\![A]\!](u)$ (the semantics of WA is defined in Section 2); if $E\equiv\min(E_{1},E_{2})$, then $\text{dom}(E)=\text{dom}(E_{1})\cap\text{dom}(E_{2})$ and for all $u\in\text{dom}(E)$, $[\![E]\!](u)=\min([\![E_{1}]\!](u),[\![E_{2}]\!](u))$, symmetrical works for $\max$, $+$ and $-$. We say that two s-expressions $E_{1},E_{2}$ are equivalent if $[\![E_{1}]\!]=[\![E_{2}]\!]$ (in particular $\text{dom}(E_{1})=\text{dom}(E_{2})$). To characterise the expressiveness of s-expressions, we note that:

Lemma 1

Any s-expression defines a Lipschitz continous quantitative language.

As we show in Appendix, unambiguous WA can define non Lipschitz continuous functions, hence not definable by s-expressions. On the contrary, the function $u\mapsto\min(\#_{a}(u),\#_{b}(u))$ is definable by an s-expression while it is not definable by a WA [12].

Proposition 1

There are quantitative languages that are definable by unambiguous weighted automata and not by s-expressions. There are quantitative languages that are definable by s-expressions but not by a WA.

To unleash their expressive power, we generalise s-expressions. First, instead deterministic WA, we consider unambiguous WA as atoms. This extends their expressiveness beyond finite valued WA. Second, instead of considering a fixed (and arbitrary) set of composition functions, we consider any function that is (existential) Presburger definable. Third, we consider the addition of Kleene star operator. While the first two extensions maintain decidability in PSpace, the third extension leads to undecidability and sub-cases need to be studied to recover decidability. We study the two first extensions here and the Kleene star operator in the next section.

Definition 2

Monolithic expressions (m-expression) are terms $E$ generated by the grammar $E\ \Coloneqq\ A\mid\phi(E_{1},\dots,E_{n})$, where $A$ is an unambiguous WA, and $\phi$ is a functional Presburger formula of arity $n$.

The semantics $[\![E]\!]:\Sigma^{*}\rightarrow\mathbb{Z}$ of an m-expression $E$ is defined inductively, and similarly as s-expression. In particular, for $E=\phi(E_{1},\dots,E_{n})$, $\text{dom}(E)=\bigcap_{i=1}^{n}\text{dom}(E_{i})$ and for all $u\in\text{dom}(E)$, $[\![E]\!](u)=[\![\phi]\!]([\![E_{1}]\!](u),\dots,[\![E_{n}]\!](u))$ (the semantics of functional Presburger formulas is defined in Section 2).

Example 1

As seen in Section 2, $\max$ is Presburger-definable by a formula $\phi_{\max}$, it is also the case for $\min(E_{1},\dots,E_{n})$, $E_{1}+E_{2}$, $E_{1}-E_{2}$ and the unary operation $-E$. For m-expressions $E_{1},E_{2}$, the distance $|E_{1}-E_{2}|\ :\ w\in\text{dom}(E_{1})\cap\text{dom}(E_{2})\mapsto|E_{1}(w)-E_{2}(w)|$ is defined by the m-expression $\max(E_{1}-E_{2},E_{2}-E_{1})$. This function is not definable by a WA even if $E_{1},E_{2}$ are 2-ambiguous WA, as a consequence of the non-expressibility by WA of $\min(\#_{a}(.),\#_{b}(.))=|0-\max(-\#_{a}(.),-\#_{b}(.))|$ [12].

Lemma 2

M-expressions are more expressive than finite valued WA. There are functions definable by m-expressions and not by a WA.

We finally come to the main result of this section:

Theorem 3.1

For m-expressions, the emptiness, universality and comparison problems are PSpace-Complete.

Proof (Sketch)

By Remark 1, all the problems reduce in PTime to the [math]-emptiness problem for which we establish PSpace membership. Clearly, by combining Presburger formulas, any m-expression is equivalent to an m-expression $\phi(A_{1},\dots,A_{n})$ where $A_{i}$ are unambiguous WA. Now, the main idea is to construct a product $A_{1}\times\dots\times A_{n}$ (valued over $\mathbb{Z}^{n}$), which maps any word $u\in\bigcap_{i}\text{dom}(A_{i})$ to $(A_{1}(u),\dots,A_{n}(u))$. (Effective) semi-linearity of $\text{range}(A_{1}\times\dots\times A_{n})$ is a consequence of Parikh’s theorem, which implies semi-linearity of $\text{range}(\phi(A_{1},\dots,A_{n}))$. Then it suffices to check for the existence of a positive value in this set. To obtain PSpace complexity, the difficulty is that $A_{1}\times\dots\times A_{n}$ has exponential size. To overcome this, we encode $\phi(A_{1},\dots,A_{n})$ into a counter machine. First, $A_{1}\times\dots\times A_{n}$ is encoded into a machine $M$ whose counter valuation, after reading $u$, encodes the tuple $(A_{1}(u),\dots,A_{n}(u))$. Then, $M$ is composed with another counter machine $M_{\phi}$ that compute, on reading the word $\epsilon$, the value $\phi((A_{1}(u),\dots,A_{n}(u))$ (stored in an extra counter). Finally, the compositional machine $M\cdot M_{\phi}$ accepts iff this latter value is positive, hence it suffices to check for its emptiness. We define $M\cdot M_{\phi}$ in such a way that it is reversal-bounded (its counters change from increasing to decreasing mode a constant number of times [11]). Reversal-bounded counter machines have decidable emptiness problem. While $M_{\phi}$ can be constructed in PTime, $M$ has an exponential size in general. However, we can use a small witness property given in [11] to devise a Pspace algorithm that does not construct $M$ explicitly.

PSpace-hardness for emptiness is obtained from the emptiness problem of the intersection of $n$ DFAs. ∎

4 Expressions with iterated sum

Given $f:\Sigma^{*}\rightarrow\mathbb{Z}$ a quantitative language, the iterated sum of $f$ (or unambiguous Kleene star), denoted by $f^{\circledast}$, is defined by $f^{\circledast}(\epsilon)=0$, and for all $u\in\Sigma^{+}$, if there exists at most one tuple $(u_{1},\dots,u_{n})\in(\text{dom}(f)\setminus\{\epsilon\})^{n}$ such that $u_{1}\dots u_{n}=u$, then $f^{\circledast}(u)=\sum_{i=1}^{n}f(u_{i})$. Note that $\epsilon\in\text{dom}(f^{\circledast})$ for any $f$. By extending m-expressions with iterated sum, we obtain iterated-sum expressions (i-expressions).

Definition 3

An iterated-sum expression $E$ (i-expression for short) is a term generated by the grammar $E\ \Coloneqq\ A\mid\phi(E,E)\mid E^{\circledast}$, where $A$ is some unambiguous WA over $\Sigma$ and $\phi$ is a functional Presburger formula.

As for m-expressions, the semantics of any i-expression $E$ is a quantitative language $[\![E]\!]:\Sigma^{*}\rightarrow\mathbb{Z}$ inductively defined on the structure of the expression.

Example 2

Assume that \Sigma=\{a,b,\}$and consider the QL$f$defined for all$u\in\Sigma^{}$by$u_{1}$u_{2}$\dots u_{n}$\ \mapsto\ \sum_{i=1}^{n}\max(#{a}(u{i}),#{b}(u{i}))$where each$u_{i}$belongs to${a,b}^{}$, and$#{\sigma}$counts the number of occurrences of$\sigma$in a word. Counting the number of$\sigma$in$v$$where$v\in{a,b}^{*}$is realisable by a 2 states deterministic WA$A{\sigma}$. Then,$f$is defined by the i-expression$\max(A_{a},A_{b})^{\circledast}$.

We show a positive and a negative result.

Proposition 2

The domain of any i-expression is (effectively) regular.

Theorem 4.1

Emptiness, universality and comparisons for i-expressions are undecidable problems, even if only s-expressions are iterated.

Proof (Sketch)

The proof of this theorem, inspired by the proof of [6] for the undecidability of WA universality, consists of a reduction from the 2-counter machine halting problem to the [math]-emptiness problem of i-expressions. This establishes undecidability for the other decision problems by Remark 1. In this reduction, a transition between two successive configurations $...(q_{1},(x\mapsto c_{1},y\mapsto d_{1}))\delta(q_{2},(x\mapsto c_{2},y\mapsto d_{2}))...$ is coded by a factor of word of the form: $...\vdash q_{1}a^{c_{1}}b^{d_{1}}\triangleleft\delta\triangleright q_{2}a^{c_{2}}b^{d_{2}}\dashv\vdash q_{2}a^{c_{2}}b^{d_{2}}\triangleleft...$.

We show that such a word encodes an halting computation if it respects a list of simple requirements that are all are regular but two: one that expresses that increments and decrements of variables are correctly executed, and one that imposes that, from one transition encoding to the next, the current configuration is copied correctly. In our example above, under the hypothesis that $x$ is incremented in $\delta$, this amounts to check that the number of $a$ occurrences before $\delta$ is equal to the number of occurrences of $a$ after $\delta$ minus one. This property can be verified by s-expression on the factor between the $\vdash$ and $\dashv$ that returns [math] if it is the case and a negative value otherwise. The second property amounts to check that the number of occurrences of $a$ between the first $\triangleright$ and $\dashv$ and the number of $a$ between the second $\vdash$ and second $\triangleleft$ are equal. Again, it is easy to see that this can be done with an s-expression that returns [math] if it is the case and a negative value otherwise. Then, with i-expressions we decompose the word into factors that are between the markers $\vdash$ and $\dashv$, and other factors that are between the markers $\triangleright$ and $\triangleleft$, and we iterate the application of the s-expressions mentioned above. The sum of all the values computed on the factors is equal to [math] if the requirements are met and negative otherwise.∎

A close inspection of the proof above, reveals that the undecidability stems from the asynchronicity between parallel star operators, and in the way they decompose the input word (decomposition based on $\vdash\dots\dashv$ or $\triangleright\dots\triangleleft$). The two overlapping decompositions are needed. By disallowing this, decidability is recovered: subexpressions $F^{\circledast}$ and $G^{\circledast}$ at the same nested star depth must decompose words in exactly the same way.

Let us formalise the notion of star depth. Given an i-expression $E$, its syntax tree $T(E)$ is a tree labeled by functional Presburger formulas $\phi$, star operators ⊛, or unambiguous WA $A$. Any node $p$ of $T(E)$ defines a subexpression $E|_{p}$ of $E$. The star depth of node $p$ is the number of star operators occurring above it, i.e. the number of nodes $q$ on the path from the root of $T(E)$ to $p$ (excluded) labeled by a star operator. E.g. in the expression $\phi(A_{1}^{\circledast},\phi(A_{2}^{\circledast}))^{\circledast}$, the subexpression $A_{1}^{\circledast}$ has star depth $1$, $A_{1}$ has star depth $2$, and the whole expression has star depth [math].

Definition 4

An $i$-expression $E$ is synchronised if for all nodes $p,q$ of $T(E)$ at the same star depth, if $E|_{p}=F^{\circledast}$ and $E|_{q}=G^{\circledast}$, then $\text{dom}(F)=\text{dom}(G)$.

By Proposition 2, this property is decidable. Asking that $F$ and $G$ have the same domain enforces that any word $u$ is decomposed in the same way by $F^{\circledast}$ and $G^{\circledast}$. Given a set $S=\{E_{1},\dots,E_{n}\}$ of $i$-expressions, we write $\text{Sync}(S)$ the predicate which holds true iff $\phi(E_{1},\dots,E_{n})$ is synchronised, where $\phi$ is some arbitrary functional Presburger formula of arity $n$.

Example 3

An i-expression $E$ is star-chain if for any distincts subexpressions $F^{\circledast}$ and $G^{\circledast}$ of $E$, $F^{\circledast}$ is a subexpression of $G$, or $G^{\circledast}$ is a subexpression of $F$. E.g. $\max(A^{\circledast},B)^{\circledast}$ is star-chain, while $\max(A^{\circledast},B^{\circledast})^{\circledast}$ is not. The expression of Example 2 is also a star-chain, hence it is synchronised, as well as $\min(\max(A_{a},A_{b})^{\circledast},A_{c})$ (note that in the latter, $A_{c}$ applies on the whole input word, while $A_{a}$ and $A_{b}$ apply on factors of it).

Finitely ambiguous WA is the largest class of WA for which emptiness, universality and comparisons are decidable [9]. Already for linearly ambiguous WA, universality and comparison problems are undecidable [6]. Example 2 is realisable by a synchronised i-expression or a WA which non-deterministically guess, for each factor $u_{i}$, whether it should count the number of $a$ or $b$. However, as shown in [12] (Section 3.5), it is not realisable by any finitely ambiguous WA. As a consequence:

Proposition 3

There is a quantitative language $f$ such that $f$ is definable by a synchronised i-expression or a WA, but not by a finitely ambiguous WA.

As a direct consequence of the definition of i-expressions and synchronisation, synchronised i-expressions are closed under Presburger combinators and unambiguous iterated-sum in the following sense:

Proposition 4

Let $E_{1},\dots,E_{n},E$ be i-expressions and $\phi$ a functional Presburger formula of arity $n$. If $\text{Sync}(E_{1},\dots,E_{n})$, then $\phi(E_{1},\dots,E_{n})$ is synchronised, and if $E$ is synchronised, so is $E^{\circledast}$.

Despite the fact that synchronised i-expressions can express QL that are beyond finitely ambiguous WA, we have decidability (proved in the next section):

Theorem 4.2

The emptiness and universality problems are decidable for synchronised i-expressions. The comparisons problems for i-expressions $E_{1},E_{2}$ such that $\text{Sync}\{E_{1},E_{2}\}$ are decidable.

5 Decidability of synchronised iterated sum expressions

In this section, we introduce a new weighted automata model, called weighted chop automata (WCA), into which we transform i-expressions. It is simple to see that the proof of undecidability of i-expressions (Theorem 4.1) can be done the same way using WCA. We introduce the class of synchronised WCA, to which synchronised i-expressions can be compiled, and by which we recover decidability, thus proving Theorem 4.2. The intuitive behaviour of a WCA is as follows. An unambiguous generalised automaton (whose transitions are not reading single letters but words in some regular language) “chop” the input word into factors, on which expressions of the form $\phi(C_{1},\dots,C_{n})$, where $C_{i}$ are smaller WCA, are applied to obtain intermediate values, which are then summed to obtain the value of the whole input word.

Formally, a generalised finite automaton is a tuple $A=(Q,I,F,\Delta)$ where $Q$ is a set of states, $I$ its initial states and $F$ its final states, and $\Delta$ maps any pair $(p,q)\in Q^{2}$ to a regular language $\Delta(p,q)\subseteq\Sigma^{*}$ (finitely represented by some NFA). A run of $A$ over a word $u=u_{1}\dots u_{n}$ is a sequence $r=q_{0}u_{1}\dots q_{n-1}u_{n}q_{n}$ such that $u_{i}\in\Delta(q_{i-1},q_{i})$ for all $1\leq i\leq n$. It is accepting if $q_{0}\in I$ and $q_{n}\in F$. We say that $A$ is unambiguous if for all $u\in\Sigma^{*}$, there is at most one accepting run of $A$ on $u$ (and hence its decomposition $u_{1}\dots u_{n}$ is unique). This property can be decided in PTime (Proposition 9 in Appendix 0.D.1).

Definition 5

A [math]-weighted chop automaton is an unambiguous WA. Let $n>0$. An $n$-weighted chop automaton ($n$-WCA) is a tuple $C=(A,\lambda)$ where $A$ is an unambiguous generalised finite automaton and $\lambda$ is a function mapping any pair $(p,q)\in Q^{2}$ to some expression $E=\phi(C_{1},\dots,C_{m})$ where for all $i$, $C_{i}$ is an $n^{\prime}$-WCA, for some $n^{\prime}<n$, and $\phi$ is a functional Presburger formula of arity $m$. Moreover, it is required that at least one $C_{i}$ is an $(n-1)$-WCA. A WCA is an $n$-WCA for some $n$.

Semantics

A WCA $C$ defines a quantitative language $[\![C]\!]$ of domain $\text{dom}(C)$ inductively defined as follows. If $C$ is a [math]-WCA, then its semantics is that of unambiguous WA. Otherwise $C=(A,\lambda)$, and the set $\text{dom}(C)$ is the set of words $u=u_{1}\dots u_{n}$ on which there exists one accepting run $r=q_{0}u_{1}\dots q_{n-1}u_{n}q_{n}$ of $A$ such that for all $1\leq i\leq n$, if $\lambda(q_{i-1},q_{i})$ is of the form $\phi(C_{1},\dots,C_{m})$, then $u_{i}\in\bigcap_{j=1}^{m}\text{dom}(C_{j})$, and in this case we let $v_{i}=[\![\phi]\!]([\![C_{1}]\!](u),\dots,[\![C_{m}]\!](u))$. The value of $r$ (which also defines the value of $u$) is then $\sum_{i=1}^{n}v_{i}$. We denote by $\text{dec}_{C}(u)$ the (unique) sequence $(u_{1},\lambda(q_{0},q_{1}))\dots(u_{n},\lambda(q_{n-1},q_{n}))$.

Example 4

Let $\Sigma=\{a,b,c,d\}$ and \bullet,\\notin\Sigma$, the WCA depicted below realises the function mapping any word of the form$u_{1}$\dots u_{n}$\bullet v_{1}$\dots v_{m}$$, where$u_{i},v_{i}\in{a,b,c,d}^{*}$, to$\sum_{i=1}^{n}\max(#{a}(u{i}),#{b}(u{i}))+\sum_{i=1}^{m}\max(#{c}(v{i}),#{d}(v{i}))$. The automata$A_{\sigma}$are unambiguous WA counting the number of occurences of$\sigma$, and$C_{i}$are shortcuts for$\phi_{id}(C_{i})$where$\phi_{id}$ defines the identify function.

$C$:\begin{array}[]{l|l}(\Sigma^{*}\)^{}\bullet&C_{1}\end{array}$$\begin{array}[]{l|l}(\Sigma^{}$)^{*}&C_{2}\end{array}$

$C_{1}$:\begin{array}[]{l|l}\Sigma^{*}\&\max{A_{a},A_{b}}\end{array}$

$C_{2}$:\begin{array}[]{l|l}\Sigma^{*}\&\max{A_{c},A_{d}}\end{array}$

Synchronised WCA

The notion of synchronisation of WCA is inductively defined. Two expressions $\phi_{1}(C_{1},\dots,C_{n})$ and $\phi_{2}(C^{\prime}_{1},\dots,C^{\prime}_{m})$ are synchronised if $C_{i}$ is synchronised with $C^{\prime}_{j}$ for all $i,j$. We say that two WCA $C_{1},C_{2}$ are synchronised, denoted by $C_{1}||C_{2}$, if they are either both [math]-WCA, or $C_{1}=(A_{1},\lambda_{1})$ and $C_{2}=(A_{2},\lambda_{2})$, and the following holds: for all $u\in L(A_{1})\cap L(A_{2})$, if $\text{dec}_{C_{1}}(u)=(u_{1},E_{1}),\dots,(u_{n},E_{n})$ and $\text{dec}_{C_{2}}(u)=(v_{1},F_{1}),\dots,(v_{m},F_{m})$, then $n=m$ and for all $1\leq i\leq n$, we have $u_{i}=v_{i}$ and $E_{i}$ is synchronised with $F_{i}$. We write $\text{Sync}(\{C_{1},\dots,C_{n}\})$ if $C_{i}||C_{j}$ for all $i,j\in\{1,\dots,n\}$. Now, a WCA $C$ is synchronised if it is an unambiguous WA, or it is of the form $(A,\lambda)$, and any expression $\phi(C_{1},\dots,C_{n})$ in the range of $\lambda$ satisfies $\text{Sync}(\{C_{1},\dots,C_{n}\})$. E.g., the WCA of Example 4 is synchronised, and it can be seen that if $C_{1}||C_{2}$, then both $C_{1}$ and $C_{2}$ are $n$-WCA for the same $n$.

Proposition 5

Synchronisation is decidable in PTime for WCA.

We now investigate the closure properties of WCA. Given two quantitative languages $f_{1},f_{2}$, let us define their split sum $f_{1}\odot f_{2}$ as the function mapping any word $u$ which can be uniquely decomposed into $u_{1},u_{2}$ such that $u_{i}\in\text{dom}(f_{i})$ for all $i$, to $f_{1}(u_{1})+f_{2}(u_{2})$ [1]. We also define the conditional choice $f_{1}\triangleright f_{2}$ as the mapping of any word $u\in\text{dom}(f_{1})$ to $f_{1}(u)$, and of any word $u\in\text{dom}(f_{2})\setminus\text{dom}(f_{1})$ to $f_{2}(u)$ [1]. These operators may be thought of as (unambiguous) concatenation and disjunction in rational expressions. Synchronised WCA are closed under these operations, as well as Presburger combinators and (unambiguous) iterated sum, in the following sense:

Proposition 6

Let $C_{1},\dots,C_{n}$ be WCA such that $\text{Sync}\{C_{1},\dots,C_{n}\}$ and $C,D$ two synchronised WCA. Let $\phi$ be a functional Presburger formula of arity $n$, and $L\subseteq\Sigma^{*}$ a regular language. There exists synchronised WCA respectively denoted by $\phi(C_{1},\dots,C_{n})$, $C^{\circledast}$, $C\odot D$, $C\triangleright D$ and $C|_{L}$ such that

• •

for all $u\in\bigcap_{i=1}^{n}\text{dom}(C_{i})$, $[\![\phi(C_{1},\dots,C_{n})]\!](u)=[\![\phi]\!]([\![C_{1}]\!](u),\dots,[\![C_{n}]\!](u))$ and $\text{dom}(\phi(C_{1},\dots,C_{n}))=\bigcap_{i=1}^{n}\text{dom}(C_{i})$

• •

$[\![C^{\circledast}]\!]=[\![C]\!]^{\circledast}$, $[\![C\odot D]\!]=[\![C]\!]\odot[\![D]\!]$, $[\![C\triangleright D]\!]=[\![C]\!]\triangleright[\![D]\!]$ and $[\![C|_{L}]\!]=[\![C]\!]|_{L}$

The key lemma towards decidability of synchronised WCA is the following:

Lemma 3

Let $C$ be a synchronised weighted chop automaton. Then $\{[\![C]\!](u)\mid u\in\text{dom}(C)\}$ is semi-linear and effectively computable.

Proof (Sketch)

The proof goes by induction on $C$. If $C$ is an unambiguous WA, then semi-linearity is known (for instance by using Parikh theorem or reversal-bounded counter machine as in the proof of Theorem 3.1). If $C=(A,\lambda)$ and $A$ has set of states $Q$, we first assume that for all states $p,q\in Q$, $\lambda(p,q)$ (which is an expression of the form $\phi(C_{1},\dots,C_{n})$), has semi-linear range $S_{p,q}$. Consider the morphism $\mu$ from the free monoid $(Q\times Q)^{*}$ to the monoid of semi-linear sets of $\mathbb{Z}$ (with neutral element $\{0\}$ and addition), defined by $\mu((p,q))=S_{p,q}$. Clearly, for any regular language $L\subseteq(Q\times Q)^{*}$, $\mu(L)$ is semi-linear, because semi-linear sets are closed under addition, finite union, and Kleene star (see [8] for instance). Then, we can show that $\text{range}(C)=\mu(L)$ for $L$ the set of words over $Q\times Q$ of the form $(q_{0},q_{1})(q_{1},q_{2})\dots(q_{k},q_{k+1})$ such that $q_{0}$ is initial, $q_{k+1}$ final, and for all $i$, $\Delta(q_{i},q_{i+1})\neq\varnothing$. $L$ is clearly regular, as the $\Delta(q_{i},q_{i+1})$ are.

To show that the expressions $\phi(C_{1},\dots,C_{n})$ have semi-linear ranges, the key idea is that thanks to synchronisation, we can safely construct a kind of product between the WCA $C_{1},\dots,C_{n}$. This product is not a proper WCA but a “generalised” WCA with values in $\mathbb{Z}^{n}$. By induction, we can show that this product has semi-linear range (in fact, our induction is on generalised WCA rather than proper WCA), whose values can be combined into a semilinear set thanks to the Presburger combinator $\phi$.∎

The following theorem is a direct consequence of Lemma 3, Remark 1 and Proposition 6.

Theorem 5.1

The following problems are decidable: emptiness and universality of synchronised WCA, comparisons of WCA $C_{1},C_{2}$ such that $\text{Sync}\{C_{1},C_{2}\}$.

We conclude this section by showing that any synchronised i-expression can be converted into a synchronised WCA. This conversion is effective, this entails by Theorem 5.1 the decidability of synchronised i-expressions (Theorem 4.2).

Theorem 5.2

Any synchronised i-expression $E$ is (effectively) equivalent to some synchronised weighted chop automaton $C_{E}$, i.e. $[\![E]\!]=[\![C_{E}]\!]$.

Proof (Sketch)

Let us illustrate the main idea of this proof on an example. Suppose that $E=\phi(A,B^{\circledast})$ for some unambiguous WA $A,B$, and Presburger formula $\phi$. The difficulty with this kind of expression comes from the fact that $A$ is applied on the whole input word, while $B$ is applied iteratively on factors of it. Clearly, $A$ is also a [math]-WCA, and $B$ could be inductively converted into some WCA $C$, in turn used to construct a WCA $C^{\circledast}$ (as done in Proposition 6). However, $A$ and $C^{\circledast}$ are not synchronised in general: by definition of synchronisation for WCA, $n$-WCA are synchronised with $n$-WCA only. This latter property is crucial to make a product construction of synchronised WCA and to prove semi-linearity of their ranges (Lemma 3).

Hence, the main idea to prove this result is to “chop” $A$ into smaller WA that are synchronised with $\text{dom}(B)$, and to express $A$ as a combination of these smaller automata. More precisely, for all states $p,q$ of $A$ we can define $A_{p,q}$ to be the WA $A$ with initial state $p$, final state $q$, whose domain is restricted to $\text{dom}(B)$. Then, all the smaller automata $A_{p,q}$ are combined into a single WCA which simulates successive applications of the automata $A_{p,q}$, by taking care of the fact that the words it accepts must be uniquely decomposable into factors of $\text{dom}(B)$. This resulting WCA, say $C^{\prime}$, is necessarily synchronised with $C^{\circledast}$, and we can return the single synchronised WCA $\phi(C^{\prime},C^{\circledast})$, as defined in Proposition 6, which is equivalent to the i-expression $\phi(A,B^{\circledast})$. The general case is just a technical generalisation of this main idea. ∎

6 Discussion

First, iterating $\max$ instead of sum also yields undecidability for i-expressions (Remark 2 in Appendix). Second, the decidability of synchronised i-expressions goes by the model weighted chop automata, which slice the input word into factors on which subautomata are applied. Any synchronised i-expression can be converted into a synchronised chop automaton (Theorem 5.2). We conjecture that the converse of Theorem 5.2 is not true, i.e. synchronised WCA are strictly more expressive than synchronised i-expressions. In particular, we conjecture that synchronised i-expressions are not closed under split sum, unlike synchronised WCA (Proposition 6). The quantitative language of Example 4 does not seem to be definable by any synchronised i-expression.

It turns out that extending i-expressions with split sum $\odot$ and conditional choice $\triangleright$, with a suitable notion of synchronisation, gives a formalism equivalent to synchronised WCA. Due to lack of space, and since the notion of synchronisation for such extended expressions is quite technical (and a bit ad-hoc), we decided not to include it.

An expression formalism with unambiguous iterated sum, conditional choice and split sum, whose atoms are constant quantitative languages (any word from a regular language is mapped to a same constant value), was already introduced by Alur et. al. [1]. It is shown that this formalism is equivalent to unambiguous WA. Our goal was to go much beyond this expressivity, by having a formalism closed under Presburger combinators. Adding such combinators to the expressions of [1] would immediately yield an undecidable formalism (as a consequence of Theorem 4.1). This extension would actually correspond exactly to the extension we discussed in the previous paragraph, and one could come up with a notion of synchronisation by which to recover decidability. We did not do it in this paper, for the reason explained before, but it would be interesting to have an elegant notion of synchronisation for the extension of [1] with Presburger combinators. More generally, our notion of synchronisation is semantical (but decidable). This raises the question of whether another weighted expression formalism with a purely syntactic notion of synchronisation could be defined.

Finally, Chatterjee et. al. have introduced a recursive model of WA [5]. They are incomparable to weighted chop automata: they can define QL whose ranges are not semilinear, but the recursion depth is only 1 (a master WA calls slave WA).

Acknowledgements

We are very grateful to Ismaël Jecker and Nathan Lhote for fruitful discussions on this work, and for their help in establishing the undecidability result.

Appendix 0.A Additional Notations

For $w\in\Sigma^{*}$, $|w|$ denotes its length, $pos(w)=\{1,\dots,|w|\}$ its set of positions (in particular $pos(\epsilon)=\varnothing$), and for $i\in pos(w)$, $w[i]$ is the $i$th symbol of $w$. A language $L$ is a subset of $\Sigma^{*}$.

Sizes of objects

We define the size $|\phi|$ of a Presburger formula $\phi$ as the number of nodes in its syntactic tree.

We define the representation size of a WA $M=(A,\lambda)$ with $A=(Q,I,F,\Delta)$ as $|M|=|Q|+|\Delta|.\text{log}(\ell)$ where $\ell$ is the maximal absolute weight of $A$.

We define the representation size $|E|$ of a m-expression $E$ inductively, if $E\equiv A$ then $|E|=|A|$ otherwise if $E\equiv\phi(E_{1},\dots,E_{n})$ then $|E|=|\phi|+\sum_{i=1}^{n}|E_{i}|$.

Appendix 0.B Proof of Section 3

0.B.1 Proof of Lemma 1

Proof

To prove that s-expressions define Lipschitz continuous functions, we need to show that for all s-expression $E$, there exists $K\in\mathbb{N}$ such that for all words $u,v\in\Sigma^{*}$:

[TABLE]

Remember that $d(u,v)=|u|+|v|-2|\sqcap(u,v)|$.

We reason by induction on the structure of the s-expressions. First, let us consider the base case where $E=D$. As $D$ is deterministic, the partial sum on $u=w.\;u^{\prime}$ and $v=w.\;v^{\prime}$ on their common prefix $w=\sqcap(u,v)$ is equal in the two cases to some value $s_{w}$ then on the two different suffixes $u^{\prime}$ and $v^{\prime}$, their sum may differ but at most by the following amount: $|u^{\prime}|\times M+|v^{\prime}|\times M$. Where $M$ is the maximum of the set of absolute value of weights appearing in the automaton $D$. It is clear that the inequality 1 is true when we take $K$=M.

Second, we consider the operation $\min$ for the inductive case, i.e. $E=\min(E_{1},E_{2})$. The other operators are treated similarly. By induction hypothesis, $E_{1}$ and $E_{2}$ defines Lipschitz continuous functions, and we note $K_{1}$ and $K_{2}$ their respective Lipschitz constants. We claim that $K=\max(K_{1},K_{2})$ is an adequate constant to show the Lipschitz continuity of $E$, i.e.: for all words $u,v\in\Sigma^{*}$

[TABLE]

Let us assume that $\min(E_{1},E_{2})(u)=E_{1}(u)$ and $\min(E_{1},E_{2})(v)=E_{2}(v)$, and that $E_{1}(u)\leq E_{2}(v)$. All the other cases are treated similarly:

[TABLE]

∎

0.B.2 Proof of Proposition 1

Proof

We first define an unambiguous WA $A$ that realises a function, called “last block”, which is non Lipschitz continuous. This establishes that s-expressions are not as expressive as finite valued WA (which extends unambiguous WA). The function “last block”, which associates to any word of the form $a^{n_{k}}ba^{n_{k-1}}b\dots ba^{n_{0}}$ where $n_{0}>0$, the value $n_{0}$, i.e. the length of the last block of $a$ (which necessarily exists since $n_{0}>0$). When reading the first $a$ or the first $a$ after a $b$, $A$ uses its non-determinism to guess whether this $a$ belongs to the last block or not.

To prove the second statement, it was shown in [12] (Section 3.6) that the function $f:u\mapsto\min(\#_{a}(u),\#_{b}(u))$ is not definable by any WA. Clearly, $u\mapsto\#_{\sigma}(u)$ for $\sigma\in\{a,b\}$ is definable by a deterministic WA $A_{\sigma}$, hence $f$ is definable by the s-expression $\min(A_{a},A_{b})$.

Another example is the following. Given two multi-sequential666Multi-sequential WA are finite unions of sequential, i.e. (input) deterministic, WA. WA $B_{1},B_{2}$ with domain $\Sigma^{*}$, the function $g:u\mapsto|B_{1}(u)-B_{2}(u)|$ is not definable by a WA, while it is definable by an s-expression. Multi-sequential automata, as they are unions of (input) deterministic WA, are easily defined by s-expression (by using the closure under $\max$). Let $S_{1},S_{2}$ be s-expressions defining $B_{1},B_{2}$ respectively, then $g$ is defined by the s-expression $\max(S_{1}-S_{2},S_{2}-S_{1})$.

Suppose that $g$ is definable by some WA. Then by taking $B_{1}$ such that $[\![B_{1}]\!](u)=0$ for all $u$, and $B_{2}$ such that $[\![B_{2}]\!](u)=\max(-\#_{a}(u),-\#_{b}(u))$, then $|B_{1}-B_{2}|=f$. Clearly, $B_{1}$ and $B_{2}$ can be taken to be multi-sequential, and we get a contradiction because $f$ is not definable by any WA. ∎

0.B.2.1 Proof of Lemma 2

Proof

We show that m-expressions can express any quantitative language definable by a $k$-valued WA. It is known that any $k$-valued WA $A$ can be decomposed into a disjoint union of $k$ unambiguous WA $A_{i}$ [9]. It is tempting to think that $A$ is equivalent to the m-expression $\max(A_{1},\dots,A_{k})$. However, this latter expression is defined only on $\bigcap_{i}\text{dom}(A_{i})$, which may be strictly included in $\text{dom}(A)$. Hence, we first complete any automaton $A_{i}$ into $B_{i}$, where $\text{dom}(B_{i})=\text{dom}(A)$, as follows: if $\alpha$ is the smallest value occurring on the transitions of the automata $A_{i}$, then, $B_{i}$ is the disjoint union of $A_{i}$ and some deterministic WA $A_{i}^{c}$ such that $\text{dom}(A_{i}^{c})=\text{dom}(A)\setminus\text{dom}(A_{i})$ and $[\![A_{i}^{c}]\!](w)=\alpha|w|$. $A_{i}^{c}$ can be easily constructed from any DFA recognising $\text{dom}(A)\setminus\text{dom}(A_{i})$ and weight function associating $\alpha$ to any transitions. Then, $A$ is equivalent to the m-expression $\max(B_{1},\dots,B_{k})$.

For the second statement, it is already the case for s-expressions (Proposition 1).∎

0.B.3 Decision problems are PSpace-c for m-expressions

Proposition 7 (Normal form)

From any m-expression $E$ with $A_{1},\dots,A_{n}$ its unambiguous weighted automata, one can construct in linear-time an equivalent m-expression $\phi(A_{1},\dots,A_{n})$, for some functional Presburger formula $\phi$.

Proof

We construct $E^{\prime}$ the normal form of $E$ such that $E\equiv E^{\prime}$ and $|E^{\prime}|=|E|+\mathcal{O}(1)$, by structural induction on $E$:

Base case. If $E=A$ then $E^{\prime}=\phi_{id}(A)$ where $\phi_{id}(x,y)=(x=y)$.

Inductive step. If $E=\psi(E_{1},\dots,E_{n})$ then we have $E_{i}\equiv\psi_{i}(A_{i,1},\dots,A_{i,m_{i}})$ for each $i\in[1..n]$ by induction hypothesis. We construct $\phi$ as follow:

[TABLE]

We define $E^{\prime}=\phi(A_{1,1},\dots,A_{1,m_{1}},\dots,A_{n,1},\dots,A_{n,m_{n}})$.∎

Counter machines

A $k$-counter machine (abbreviated as CM) is defined as a tuple $M=\langle\Sigma,X,Q,q_{\it init},F,\Delta,\alpha,\tau,\lambda\rangle$ where $\Sigma$ is an alphabet, $X$ is a finite set of $k$ counters interpreted over $\mathbb{N}$, $Q$ is a finite set of states, $q_{\it init}\in Q$ is an initial state, $F\subseteq Q$ is a set of accepting states, $\Delta:Q\times Q$ is a transition relation, $\alpha:\Delta\rightarrow\Sigma\cup\{\varepsilon\}$ assigns a letter from $\Sigma$ or the empty word $\epsilon$ to each transition, $\tau:\Delta\rightarrow\{\texttt{=0},\texttt{>0},\texttt{true}\}^{k}$ assigns a guard to each transition, and $\lambda:\Delta\rightarrow\{\texttt{decr},\texttt{nop},\texttt{incr}\}^{k}$ assigns an update to each counter and each transition.

A configuration of $M$ is a pair $(q,\nu)$ where $q\in Q$ is a state and $\nu:X\rightarrow\mathbb{N}$ is a valuation for the counters. Given a transition $\delta\in\Delta$, and two valuations $\nu,\nu^{\prime}:X\rightarrow\mathbb{N}$, we write $\nu\models\tau(\delta)$ when the valuation $\nu$ satisfies the guard $\tau(\delta)$ (with the obvious semantics), and $(\nu,\nu^{\prime})\models\lambda(\delta)$ when the update of the values of counters from $\nu$ to $\nu^{\prime}$ satisfies $\lambda(\delta)$.

A computation of $M$ from $(q,\nu)$ to $(q^{\prime},\nu^{\prime})$ on a word $w\in\Sigma^{*}$ is a finite sequence of configurations and transitions $\rho=(q,\nu_{0})\delta_{0}(q_{1},\nu_{1})\delta_{1}\dots\delta_{n-1}(q_{n},\nu_{n})$ such that $q_{0}=q$, $\nu_{0}=\nu$, $q_{n}=q^{\prime}$, $\nu_{n}=\nu^{\prime}$, and for all $i$, $0\leq i<n$, $\nu_{i}\models\tau(\delta_{i})$, $(\nu_{i},\nu_{i+1})\models\lambda(\delta_{i})$, and $\alpha(\delta_{0})\cdot\alpha(\delta_{1})\cdot\ldots\cdot\alpha(\delta_{n-1})=w$, i.e. the concatenation of the symbols on transitions given by $\alpha$ is equal to the word $w$.

The semantics of a machine $M$ from valuation $\nu$ on a word $w$ is the set of valuations $\nu^{\prime}$ such that there exists an accepting state $q^{\prime}\in F$ and a computation of $M$ from $(q_{\it init},\nu)$ to $(q^{\prime},\nu^{\prime})$, this set of valuations is denoted by $[\![M]\!](w,\nu)$. The language of a machine $M$ from valuation $\nu$ is the set of words $w$ such that there exists an accepting state $q^{\prime}\in F$, a valuation $\nu^{\prime}$, and a computation of $M$ from $(q_{\it init},\nu)$ to $(q^{\prime},\nu^{\prime})$ on $w$, this set of words is denoted by $L_{\nu}(M)$. If for all words $w\in L_{\nu}(M)$, the set $[\![M]\!](w,\nu)$ is a singleton, we say that the machine $M$ is unambiguous from valuation $\nu$; in such case then $[\![M]\!](w,\nu)$ can be interpreted directly as a valuation and we write for $x\in X$, $[\![M]\!](w,\nu)(x)$ for the value of $x$ in the valuation reached after reading the word $w$ with $M$ from $\nu$.

While any non-trivial question about the sets $[\![M]\!](w,\nu)$ and $L_{\nu}(M)$ is undecidable for counter machines with two counters or more, Ibarra et al. has shown in [11] that $[\![M]\!](w,\nu)$ is semi-linear and effectively constructible when the machine $M$ is reversal bounded, and so the emptiness of $L_{\nu}(M)$ is decidable in that case. We recall the notion of reversal bounded here. Given a computation $\rho$, a counter $x$ has $r$ reversals in $\rho$ if the counter $x$ alternates $r$ times between increment and decrement phases in $\rho$. A machine $M$ is $r$-reversal bounded if for all its computations $\rho$, for all its counters $x\in X$, $x$ has at most has $r$ reversals in $\rho$. A machine $M$ is reversal bounded if there exists $r\in\mathbb{N}$ such that $M$ is $r$-reversal bounded.

Theorem 0.B.1 (Lemma 2 of [11])

Let $M$ be a $1$-reversal $k$-counter machine with $m$ transitions and $\nu$ a valuation of its counters. $L_{\nu}(M)\neq\varnothing$ if and only if $M_{\nu}$ accepts some input in $(k(m+|\nu|)^{kC})$ transitions where $|\nu|=\max\{\nu(i)\mid 1\leq i\leq k\}$ and $C$ is constant.

We will use counter machines as an algorithmic tool in the sequel. Some of our algorithms rely on the following lemmas that relates reversal bounded machines, Presburger expressions and weighted automata.

Lemma 4 (Presburger term to CM)

For all Presburger terms $t$ with $P$ the set of positions of its syntactic tree, and for all valuation $\nu\colon{\it free}(t)\rightarrow\mathbb{N}$, one can construct a $1$-reversal deterministic counter machine $M=\langle\Sigma,X,Q,q_{\it init},F,\Delta,\alpha,\tau,\lambda\rangle$ (which is increasing-decreasing) with $X=\{x^{+}_{p},x^{-}_{p}\mid p\in P\}$ and a valuation $\nu_{M}:X\rightarrow\mathbb{N}$, such that $M$ has a (unique) computation from $(q_{\it init},\nu_{M})$ to $(q_{f},\nu^{\prime}_{M})$ on the empty word $\epsilon$, and $q_{f}\in F$ and $\nu(p_{0})=\nu^{\prime}_{M}(x^{+}_{p_{0}})-\nu^{\prime}_{M}(x^{-}_{p_{0}})$ where $p_{0}$ the position of term $t$. The sizes of $M$ and $\nu_{M}$ are bounded linearly in the sizes of $t$ and $\nu$ respectively.

Proof (Sketch)

Let us give the main ideas on the example $t=x+x$. We want to construct a machine $M$ which, given a valuation of $x$, returns $x+x$. There are two issues: (1) counters in counter machines can only be positive, whereas $x$ can be negative, (2) there are two occurrences of $x$. To address these two issues, for each occurrence $p\in\{1,2\}$, we use two counters $x_{p}^{+}$ and $x_{p}^{-}$, such that at any moment, $x_{p}^{+}$ stores the content of $x$ if $x$ is positive (and $x_{p}^{-}=0$), otherwise $x_{p}^{-}$ stores $-x$ (and $x_{p}^{+}=0$). The machine $M$ copies $x_{1}^{+}+x_{2}^{+}$ into $x_{p_{0}}^{+}$ ($p_{0}$ is the position of $t$), and $x_{1}^{-}+x_{2}^{-}$ into $x_{p_{0}}^{-}$. This can be done by decreasing $x_{1}^{+}$, $x_{2}^{+}$ and increasing $x_{p}^{+}$ (which is initially set to [math]) in parallel, until both counters $x_{1}^{+}$ and $x_{2}^{+}$ have reached [math] (and similarly for the negative parts).

More generally, for every occurrence $p$ of a subterm $st$, we use two counters $x_{p}^{+},x_{p}^{-}$ to encode the value of this subterm by $x_{p}^{+}-x_{p}^{-}$. We define $\nu_{M}$ as follows. Each occurrence $p_{v}$ of a variable $v\in\textit{free}(t)$ such that $\nu(v)\geq 0$ (resp. $<0$) we let $\nu_{M}(x_{p_{v}}^{+})=\nu(v)$ (resp. $\nu_{M}(x_{p_{v}}^{-})=-\nu(v)$). All variables associated with a subterm which is not a free variable are mapped to zero by $\nu_{M}$.

The construction of $M$ can be done by structural induction on $t$. For a constant $C\in\{0,1\}$, we can trivially construct a machine that computes a pair of counters which encodes $C$. For a variable occurrence, the pairs of counters corresponding to that occurrence is already valued by the initial valuation $\nu_{M}$ since all variables of $t$ are free.

Finally, for an occurrence $p$ of a subterm $st$ of the form $t_{1}+t_{2}$ (with respective occurrences $p_{1},p_{2}$), we inductively use counter machines $M_{p_{1}}$ and $M_{p_{2}}$ to compute the values of $x_{p_{i}}^{+},x_{p_{i}}^{-}$ for $i=1,2$. The machine for $p$ is defined by the successive execution of $M_{p_{1}}$, $M_{p_{2}}$, and a machine which realises the operations $x_{p}^{+}=x_{p_{1}}^{+}+x_{p_{2}}^{+}$ and $x_{p}^{-}=x_{p_{1}}^{-}+x_{p_{2}}^{-}$.

We conclude by saying that the size of $M$ is bounded linearly in the sizes of $t$ since its a linear combination of constant size gadgets. ∎

Lemma 5 (Presburger formula to CM)

For all functional Presburger formula $\phi$ with $P$ set of positions in its syntactic tree, and valuation $\nu\colon{\it free}(\phi)\rightarrow\mathbb{N}$ for the free variables in $\phi$, one can construct a $1$-reversal (increasing-decreasing) unambiguous counter machine $M=\langle\Sigma,X,Q,q_{\it init},F,\Delta,\alpha,\tau,\lambda\rangle$ with $X=\{x^{+}_{p},x^{-}_{p}\mid p\in P\}$ and a valuation $\nu_{M}:X\rightarrow\mathbb{N}$, such that $\nu\models\phi$ if and only if $L_{\nu_{M}}(M)\neq\varnothing$. The sizes of $M$ and $\nu_{M}$ are bounded linearly in the sizes of $\phi$ and $\nu$ respectively.

Proof (Sketch)

We define $\nu_{M}$ as in Lemma 4. Each occurrence $p_{v}$ of a free variable $v$ of $\phi$ such that $\nu(v)\geq 0$ (resp. $<0$) we let $\nu_{M}(x_{p_{v}}^{+})=\nu(v)$ (resp. $\nu_{M}(x_{p_{v}}^{-})=-\nu(v)$). All variables associated with a subterm occurring in $\phi$ which is not a free variable are mapped to zero by $\nu_{M}$.

The construction of $M$ is done by structural induction on $\phi$. The base case are atomic formulas, which are either of the form $t_{1}=t_{2}$ or $t_{1}>t_{2}$. As done in Lemma 4, for all variable $x$ occurring at position $p$ in $t_{i}$, we use counters $x_{p}^{+}$ and $x_{p}^{-}$ to encode its value. We first construct counter machines $M_{p_{1}}$ and $M_{p_{2}}$ inductively corresponding to terms $t_{1},t_{2}$, obtained by Lemma 4, which computes the values of $x_{p_{i}}^{+},x_{p_{i}}^{-}$ for $i=1,2$. The machine for $p$ is defined by the successive execution of $M_{p_{1}}$, $M_{p_{2}}$, and a machine which realises the operations $x_{p}^{+}=x_{p_{1}}^{+}+x_{p_{2}}^{-}$, $x_{p}^{-}=x_{p_{1}}^{-}+x_{p_{2}}^{+}$ and then check that $x_{p}^{+}>x_{p}^{-}$ by decreasing simultaneously $x_{p}^{+},x_{p}^{-}$ until $x_{p}^{-}=0$ and $x_{p}^{+}>0$ (otherwise it halts and rejects the input). The procedure is similar for $\psi$ of the form $t_{1}=t_{2}$ (both $x_{p}^{+}$ and $x_{p}^{-}$ must reach 0 at the same time when decreased).

If $\psi$ is of the form $\psi_{1}\lor\psi_{2}$ (with respective positions $p_{1},p_{2}$), the machine for $p$ execute non-derterministicaly the machines of $M_{p_{1}}$ or $M_{p_{2}}$ both inductively constructed.

If $\psi$ is of the form $\psi_{1}\land\psi_{2}$ (with respective positions $p_{1},p_{2}$), we combine the machines $M_{p_{1}}$ and $M_{p_{2}}$ both inductively constructed, with some $\varepsilon$-transition from accepting state of the first one to the initial state of the second one.

If $\psi$ is of the form $\exists x.\;\psi_{1}$ (with respective position $p_{1}$), we define $P_{x}\subseteq P$ the set of all free occurrences of $x$ in the syntactic tree of $\psi$. The machine for $p$ first goes to a loop which increases non-deterministically, and in parallel, each $x_{q}^{+}$ or $x_{q}^{+}$ where $q\in P_{x}$ and then execute the machine $M_{p_{1}}$ inductively constructed.

We conclude by saying that the size of $M$ is bounded linearly in the sizes of $\phi$ since its almost a linear combination of constant size gadgets. In fact, the only gadget which have not a constant size is the gadget of quantifier case but, w.l.o.g we can assume that all non-free variables of $\phi$ is quantified once and thus the sum of all size of quantifier gadget is bounded linearly in the sizes of $\phi$. ∎

Lemma 6 (uWA to CM)

Let $A$ be an unambiguous WA with $m$ transitions and $\ell$ be the maximum among the set of absolute values of weights in $A$. One can construct an unambiguous [math]-reversal (increasing only) $2$-counter machine $M$ over $X=\{x^{+},x^{-}\}$ and with $\mathcal{O}\left(m\ell\right)$ transitions such that $L(A)=L_{\mathbb{0}}(M)$ and $\forall u\in L(A).\;A(u)=M(u,\mathbb{0})(x^{+})-M(u,\mathbb{0})(x^{-})$ where $\mathbb{0}$ maps any counter to zero.

Proof

We construct $M$ from the same state space as $A$, same initial state and same final states, and the same transition relation. We handle weights as follows. As weights in $A$ can be positive as well as negative, and variable in $M$ can only carry nonnegative integers, we use two variables to encode the sum of weights along runs: each time a positive weights is crossed in $A$ then $x^{+}$ is incremented with this weight in $M$, and each time a negative weight is crossed in $A$ then $x^{-}$ is incremented with the opposite of this weight in $M$. As a consequence, after reading a prefix of a word in $A$ and $M$ using the same sequence of transitions, the two devices are in the same state and the difference $x^{+}-x^{-}$ is equal to the sum of weights along the run in $A$. ∎

Proof (of Theorem 3.1)

We show that the quantitative emptiness, universality and comparison problems for m-expressions are PSpace-Complete.

PSpace-easiness. By Remark 1 and since PSpace is close under negation, we must only show that the quantitative 0-emptiness problem is in PSpace. Let $E$ be a m-expression, we can assume w.l.o.g that $E$ is of the form $\phi(A_{1},\dots,A_{n})$ by Proposition 7. Then, $|E|=|\phi|+\mathcal{O}(1)+\sum_{i=1}^{n}|A_{i}|$.

The idea is to reduce this problem to the emptiness of the language of a reversal bounded counter machine. This machine will be the concatenation of two machines $M_{A}$ and $M_{\psi}$. Given an input word $w\in\text{dom}(E)$, our computation will start in $M_{A}$ over $w$ where all counters start with the value zero. $M_{A}$ simulates the product of all uWA i.e compute the unique valuation $\nu$ such that $\nu(i)=A_{i}(w)$ for each $1\leq i\leq n$. Then our computation continues in $M_{\psi}$ over $\varepsilon$ which guesses a value $y\geq 0$ and accepts if and only if $\phi(\nu(1),\dots,\nu(n),y)$ holds.

For all $1\leq i\leq n$, let $m_{i}$ the number of transition in $A_{i}$ and $\ell_{i}$ the maximal of the absolute values of its weights. We set $m=\max\{m_{i}:1\leq i\leq n\}$ and $\ell=\max\{\ell_{i}:1\leq i\leq n\}$. For all $1\leq i\leq n$, we apply Lemma 6 on $A_{i}$ to construct the unambiguous increasing-only $2$-counter machine $M_{i}$ over $\{x_{i}^{+},x_{i}^{-}\}$ with $\mathcal{O}(m\ell)$ transitions such that $L(A_{i})=L_{\mathbb{0}}(M_{i})$ and for all $u\in L(A_{i})$ we have $A_{i}(u)=M_{i}(u,\mathbb{0})(x_{i}^{+})-M(u_{i},\mathbb{0})(x_{i}^{-})$ where $\mathbb{0}$ maps any counter to zero.

To ensure that all atoms read the same word, we consider the unambiguous increasing-only counter machine $M_{A}$ over $\bigcup_{i=1}^{n}\{x_{i}^{+},x_{i}^{-}\}$ and with $\mathcal{O}((m\ell)^{n})$ transitions which is defined such that $L_{\mathbb{0}}(M_{A})=\bigcap_{i=1}^{n}L(M_{i})$ and for all $u\in L_{\mathbb{0}}(M_{A})$, for all $1\leq i\leq n$ we have $M_{A}(u,\mathbb{0})(x_{i}^{+})=M_{i}(u,\mathbb{0})(x_{i}^{+})$ and $M_{A}(u,\mathbb{0})(x_{i}^{-})=M_{i}(u,\mathbb{0})(x_{i}^{-})$. The machine $M_{A}$ is obtained as the product of the machines $M_{i}$ (its set of states are tuples of states of the machines $M_{i}$). Now, we define the existential Presburger formula $\psi$ as:

[TABLE]

Let define the valuation $\nu\colon{\it free}(\psi)\rightarrow\mathbb{N}$ as $\nu(x_{i})=M_{A}(u,\mathbb{0})(x_{i}^{+})-M_{A}(u,\mathbb{0})(x_{i}^{-})$ for each $1\leq i\leq n$.

By applying Lemma 5 on $\psi$ with valuation $\nu$, we can construct an increasing-decreasing counter machine $M_{\psi}$ over $\{x^{+}_{u},x^{-}_{u}\mid{\it u}\in\mathcal{T}(\psi)\}$ and a valuation $\nu_{\psi}:X\rightarrow\mathbb{N}$, such that $\nu\models\psi$ if and only if $\epsilon\in L_{\nu_{\psi}}(M)$. The sizes of $M$ and $\nu_{\psi}$ are bounded linear in the sizes of $\psi$ and $\nu$ respectively. Note that since $|\psi|=|\phi|+\mathcal{O}(1)$, the size of $M_{\psi}$ is bounded linear in the sizes of $\phi$ and then also in the size of $E$.

Let consider the concatenation $M_{A}\cdot M_{\psi}$ which is the combination of the machines of $M_{A}$ and $M_{\psi}$ with some $\varepsilon$-transition from accepting states of $M_{A}$ to the initial state $M_{\psi}$. We show that $L_{\mathbb{0}}(M_{A}\cdot M_{\psi})\neq\varnothing$ iff there exists $w\in dom(E)$ such that $E(w)\geq 0$:

[TABLE]

In fact, $|M_{A}|$ is exponential in $n$ while $|E|$ is linear in $n$. But, by Theorem 0.B.1 we can obtain an upper bound $B$777$(\mathcal{O}(|\phi|)\times\mathcal{O}(|M_{A}\cdot M_{\psi}|))^{\mathcal{O}(|\phi|)}$ on the size of minimal accepting executions of $M_{A}\cdot M_{\psi}$, with $\mathbb{0}$ as initial valuation. Note that the binary encoding of $B$ is polynomial in $|E|$. Then, we can use the bound $B$ as an upper bound on the size of minimal accepting executions of $M_{A}$ with $\mathbb{0}$ as initial valuation. Algorithm 1 allows us to calculate a valuation $\nu$ of the atoms of $E$ with a space polynomial in $B$.

Since $|M_{\psi}|$ is polynomial in $|\phi|$ and then in $|E|$, the machine $M_{\psi}$ can be effectively constructed with a space polynomial in $|E|$. To do that, we apply Lemma 5 on $\psi$ and $\nu$. Note that, the bound $B$ is also the upper bound on the size of minimal accepting executions of $M_{\psi}$ with $\nu_{\psi}$ as initial valuation. Thus, we can guess a computation smaller than $B$ of $M_{\psi}$ with $\nu_{\psi}$ as initial valuation and we check in polynomial space with $M_{\psi}$ if the guessed computation is correct and accepting.

PSpace-hardness. By reduction from the finite automaton intersetion problem (INT). Let $A_{1},\dots,A_{n}$ be $n$ deterministic regular automata with a common alphabet $\Sigma$, determining whether $\{w\in\Sigma^{*}\mid w\in\bigcap_{i=1}^{n}L(A_{i})\}\neq\varnothing$ is PSpace-Hard. Moreover, since PSpace is close under negation, we also have that $\{w\in\Sigma^{*}\mid w\in\bigcap_{i=1}^{n}L(A_{i})\}=\varnothing$ (notINT) is PSpace-Hard.

For each $1\leq i\leq n$, we construction the uWA $W_{i}$ such that for all $u\in\Sigma^{*}$ if $u\in L(A_{i})$ then $W_{i}(u)=1$ otherwise $W_{i}(u)=0$. Note that for each $1\leq i\leq n$, we can construct $W_{i}$ in linear time since $A_{i}$ is deterministic and then the regular automaton which recognise the complementary of $L(A_{i})$ can be construct in linear time.

We show that INT can be reduced to the quantitative emptiness problem and notINT can be reduced to the quantitative equivalence problem:

[TABLE]

Finally, the PSpace-Hardness of the quantitative equivalence implies trivially the PSpace-Hardness of the quantitative inclusion. ∎

Appendix 0.C Proof of Section 4

0.C.1 The language of uniquely decomposable words

Let $L\subseteq\Sigma^{*}$ be a language. We denote by $L^{\#}\subseteq L^{*}$ the set of words $u\in L^{*}$ such that either $u=\epsilon$, or there exists at most one tuple $(u_{1},\dots,u_{n})\in(L\setminus\{\epsilon\})^{n}$ such that $u=u_{1}\dots u_{n}$.

Proposition 8

If $L\subseteq\Sigma^{*}$ is regular, then $L^{\#}$ is (effectively) regular.

Proof

Let $A=(Q,q_{0},F,\Delta)$ be a DFA recognising $L\setminus\{\epsilon\}$. First, from $A$, one can define the non-deterministic automaton (with $\epsilon$-transitions) $B=(Q,\{q_{0},q^{\prime}_{0}\},F\cup\{q^{\prime}_{0}\},\Delta\cup\{(q_{f},\epsilon,q_{0})\mid q_{f}\in F\})$ which accepts $\epsilon$ and all words that are decomposable into nonempty factors of $L$. Then, by taking the product of $B$ with itself, and by adding a bit of memory in this product to remember whether some $\epsilon$-transition was fired in parallel of a non-$\epsilon$ one (which implies in that case, if the two simulated runs of $B$ terminates, that there are two decompositions), one obtains an automaton which accepts all words which can be non-uniquely decomposed. It suffices then to complement this automaton, concluding the proof. ∎

0.C.2 The domain of an i-expression is regular: proof of Proposition 2

Proof

The domain of a WA is regular, and defined by its underlying finite automaton. For an expression $\phi(E_{1},\dots,E_{n})$, by induction, $\text{dom}(E_{i})$ is regular for all $i$, and by definition, $\text{dom}(\phi(E_{1},\dots,E_{n})=\bigcap_{i}\text{dom}(E_{i})$ which is regular since regular languages are effectively closed under intersection. Consider now the case of an expression of the form $E^{\circledast}$. By induction hypothesis, $\text{dom}(E)$ is regular, and since $\text{dom}(E^{\circledast})=\text{dom}(E)^{\circledast}$, by Proposition 8 we get the result. ∎

0.C.2.1 Undecidability: Proof of Theorem 4.1

Proof

By Remark 1, we only need to prove the undecidability of the [math]-emptiness problem to obtain the undecidability of the universality and the comparison problems. We prove this undecidability by providing a reduction from the halting problem of two-counter machines.

Let $M=\langle\Sigma,\{x,y\},Q,q_{\it init},F,\Delta,\tau,\lambda,\alpha\rangle$ be a deterministic two-counter machine, let $\nu_{0}$ be such that $\nu_{0}(x)=0$ and $\nu_{0}(y)=0$, and w.l.o.g., let us assume that the states in $F$ are the halting states of $M$. We reduce the problem of deciding if the unique888The computation is unique as $M$ is deterministic. computation of $M$ that starts from configuration $(q_{\it init},\nu_{0})$ reaches or not an accepting state (from which it halts) to the problem of deciding if for some effectively constructible iterated-sum expression $E$, there exists a word $w\in L(E)$ such that $E(w)\geq 0$.

Before defining $E$, we first explain how we encode computations of $M$ into words over the alphabet $\Gamma=Q\cup\{\vdash,\dashv,\triangleright,\triangleleft,a,b\}\cup\Delta$. Let $\rho$

[TABLE]

be a computation of $M$, we encode it by the following word over $\Gamma$:

[TABLE]

So a word $w\in\Gamma^{*}$ encodes of the halting computation of $M$ from $\nu_{0}$ if the following conditions holds:

the word $w$ must be in the language defined by the following regular expression $(\vdash Qa^{*}b^{*}\triangleleft\Delta\triangleright Qa^{*}b^{*}\dashv)^{*}$; 2. 2.

the first element of $Q$ in $w$ is equal to $q_{\it init}$, i.e. the computation is starting in the initial state of $M$; 3. 3.

the last element of $Q$ in $w$ belongs to set $F$, i.e. the computation reaches an accepting state of $M$; 4. 4.

the first element of $Q$ in $w$ is directly followed by an element in $\Delta$, i.e. the computation starts from the valuation $\nu_{0}$; 5. 5.

for each factor of the form $\vdash q_{1}a^{n_{1}}b^{m_{1}}\delta q_{2}a^{n_{2}}b^{m_{2}}\dashv$:

1. (a)

$\delta$ is a transition from $q_{1}$ to $q_{2}$; 2. (b)

$(n_{1},m_{1})\models\tau(\delta)$, i.e. the guard of $\delta$ is satisfied; 3. (c)

$((n_{1},m_{1}),(n_{2},m_{2}))\models\lambda(\delta)$, i.e. the updates of $\delta$ are correctly realised; 6. 6.

for each factor of the form $\triangleright q_{1}a^{n_{1}}b^{m_{1}}\vdash\dashv q_{2}a^{n_{2}}b^{m_{2}}\triangleleft$, it is the case that:

1. (a)

$q_{1}=q_{2}$, i.e. the control state is preserved from one configuration encoding to the next one; 2. (b)

$n_{1}=n_{2}$ and $m_{1}=m_{2}$, i.e. valuations of counters are preserved from one configuration encoding to the next one.

Let us now explain how we can construct an expression $E$ that maps a word $w$ to value [math] if and only if this word is the encoding of an halting computation of $M$ from valuation $\nu_{0}$, and to a negative value otherwise.

First, we note that this can be done by providing for each of the conditions an expression which returns [math] when the condition is satisfied and a negative value otherwise. Then we simply need to combine those expressions with the $\min$ operator: the $\min$ expression will be equal to [math] only if all the expressions are equal to [math], and it will be negative otherwise.

Second, we note that all the constraints in the list above are regular constraints with the exception of $5(c)$ and $6(b)$. Being regular, all the other constraints can be directly encoded as deterministic WA and so trivially as i-expressions. We concentrate here on the constraints that require the use of iteration, and we detail the construction for constraint $5(c)$ as the construction for $6(b)$ is similar and simpler.

For constraints $5(c)$, we construct an i-expression $E_{5(c)}$ that decomposes the word uniquely as factors of the form $\vdash q_{1}a^{n_{1}}b^{m_{1}}\delta q_{2}a^{n_{2}}b^{m_{2}}\dashv$. On each factor, we evaluate an s-expression whose value is nonnegative if and only if the update defined by $\delta$ is correctly realised in the encoding. To show how to achieve this, assume for the illustration that $\delta$ is incrementing the counter $x$ et let us show how this can be checked. The expression that we construct in this case computes the minimum of $1+n_{1}-n_{2}$ and $-1-n_{1}+n_{2}$. It should be clear that this minimum is equal to [math] if and only if $n_{2}=n_{1}+1$ (i.e. when the increment is correctly realised). In turn, it is a simple exercise to construct a deterministic weighted automaton to compute $n_{1}+1-n_{2}$ and one to compute $n_{2}-n_{1}-1$. All the different updates can be treated similarly. Now, the i-expression $E_{5(c)}$ simply take the sum of all the values obtained locally on all the factors of the decomposition. This sum is nonnegative if and only if all the values computed locally are nonnegative. ∎

Remark 2 (Iteration of $\max$)

Another option would be to define the semantics of $E^{\circledast}$ has an iteration of $\max$, i.e. $\text{dom}(E^{\circledast})$ is still the set of words $u$ that are uniquely decomposed into $u_{1}\dots u_{n}$ with $u_{i}\in\text{dom}(E)$, but $[\![E]\!](u)=\max\{[\![E]\!](u_{i})\mid i=1,\dots,n\}$. This variant is again undecidable with respect to emptiness, universality and comparisons. Indeed, an careful inspection of the proof above show that in constraint $E_{5(c)}$ and $E_{6(b)}$, we can replace the iteration of sum by iteration of $\min$, or equivalently, if we first reverse the sign of all expression, by the iteration of $\max$. In that case the $\max$ will be nonpositive if and only if the two-counter machine has an halting computation.

Appendix 0.D Proof of Section 5

0.D.1 Unambiguity of Generalised Finite Automata

Proposition 9

We can decide whether a generalised finite automaton is unambiguous in polynomial time.

Proof

Let $A=(Q,I,F,\Delta)$ be a generalised finite automaton whose languages $\Delta(p,q)$ are given by NFA $A_{p,q}=(Q_{p,q},I_{p,q},F_{p,q},\Delta_{p,q})$. We construct in polynomial time a finite transducer $T=(P,I,\{p_{f}\},\Delta^{\prime})$ which, given a word $u\in L(A)$, outputs any run of $A$ on $u$ (seen as a word over the alphabet $Q\cup\Sigma$). Clearly, $T$ defines a function iff $A$ is unambiguous. We refer the reader for instance to [2] for a definition of finite transducers, but let us recall that it is an automaton extended with outputs. In particular, the transition relation $\Delta^{\prime}$ has type $\Delta^{\prime}\subseteq P\times\Sigma^{*}\times\Gamma^{*}\times P$, where $\Gamma$ is the output alphabet. Transitions are denoted by $p\xrightarrow{u|v}q$ where $u$ is the input word and $v$ the output word. In general, a transducer defines a binary relation from input to output words, but functionality is decidable in Ptime for finite transducers (see for instance [2]).

To construct $T$, the idea is simple. We take $\Gamma=Q\cup\Sigma$ has output alphabet. Then, $P=\{p_{f}\}\cup Q\uplus\biguplus_{p,q\in Q}Q_{p,q}$ where $p_{f}$ is a new state. The transition function contains the following rules:

• •

$q\xrightarrow{\epsilon|q}s_{0}$ for all $q\in Q$ and $s_{0}\in\bigcup_{q^{\prime}\in Q}I_{q,q^{\prime}}$: when entering a new subautomaton $A_{q,q^{\prime}}$, the transducer starts by writing the state $q$ on the output.

• •

$s\xrightarrow{\sigma|\sigma}s^{\prime}$ for all $(s,\sigma,s^{\prime})\in\bigcup_{p,q\in Q}\Delta_{p,q}$: inside a subautomaton $A_{o,q}$, only symbols from $\Sigma$ are written on the output.

• •

$s\xrightarrow{\sigma|\sigma}q$ if there are $p,q\in Q$ and $s^{\prime}\in F_{p,q}$ such that $(s,\sigma,s^{\prime})\in\Delta_{p,q}$: when reaching an accepting state in a subautomaton, the transducer make exit the subautomaton.

• •

$q\xrightarrow{\epsilon|q}p_{f}$ for all $q\in F$: the transducer write the last seen accepting state (when the end of the word is reached) on the output and goes to $p_{f}$, which is accepting and is a deadlock (no outgoing transitions).

∎

0.D.2 Synchronisation of Weighted Chop Automata (Proposition 5)

First, we define the size of a WCA $C=(A,\lambda)$ where $A=(Q,I,F,\Delta)$. It is the natural $|C|$ define as $\sum_{p,q\in Q}n_{p,q}+|Q|^{2}\times\ell\times\gamma\times k$ where $n_{p,q}$ is the number of states of the NFA recognising $\Delta(p,q)$, $\ell>0$ is the maximal number of arguments in functionnal Presburger formula appearing in $\lambda$ plus one, $\gamma>0$ is the maximal size of the sub-WCA occurring in the range of $\lambda$ and $k>0$ is the maximal size of the Presburger formula appearing $\lambda$.

Proof (of Proposition 5)

We show how to check in PTime that two chop automata $C_{1},C_{2}$, or two expressions are synchronised. The algorithm is recursive. If $C_{1}$ and $C_{2}$ are both unambiguous WA, then the algorithm returns 1. If one of them is an unambiguous WA and the other not, then the algorithm returns 0.

Now, consider the case where we have chop automata $C_{1}=(A_{1},\lambda_{1})$ and $C_{2}=(A_{2},\lambda_{2})$. We first show how to decide the following (weaker) property: for all $u\in L(A_{1})\cap L(A_{2})$, if $\text{dec}_{C_{1}}(u)=(u_{1},E_{1}),\dots,(u_{n},E_{n})$ and $\text{dec}_{C_{2}}(u)=(v_{1},F_{1}),\dots,(v_{m},F_{m})$, then $n=m$ and for all $i\in[1..n]$, we have $u_{i}=v_{i}$.

One again the idea is to construct a transducer $T$, which defines a function from $\Sigma^{*}$ to $2^{\Sigma^{*}}$, whose domain is $L(A_{1})\cap L(A_{2})$. To $u\in\text{dom}(T)$, if $\text{dec}_{C_{1}}(u)=(u_{1},E_{1}),\dots,(u_{n},E_{n})$ and $\text{dec}_{C_{2}}(u)=(v_{1},F_{1}),\dots,(v_{m},F_{m})$, then $T$ returns the set of words

[TABLE]

Since $u_{1}\dots u_{n}=v_{1}\dots v_{n}=u$, the latter set is a singleton iff the two decompositions are equal. Hence, it suffices to decide whether $T$ defines a function (i.e. is functional), which can be done in PTime in the size of $T$ (see for instance [2]).

It remains to show how to construct $T$. $T$ is the disjoint union of two transducers $T_{1}$ and $T_{2}$, which respectively output $a^{|u_{1}|}\#a^{|u_{2}|}\#\dots\#a^{|u_{n}|}$ and $a^{|v_{1}|}\#a^{|v_{2}|}\#\dots\#a^{|v_{n}|}$. Consider $T_{1}$. It will simulate the behaviour of $C_{1}$ in the following way. If $A_{1}=(Q,q_{0},F,\Delta)$ and $(A_{p,q})_{p,q}$ are NFA that recognise $\Delta(p,q)$, then $T_{1}$ start in a copy of $A_{q_{0},p}$, where $p$ is non-deterministically chosen. Whenever a transition $(\alpha,\sigma,\beta)$ of $A_{q_{0},p}$ is fired, $T_{1}$ makes several choices: either $p$ is not final in $A_{q_{0},p}$ and $T_{1}$ moves to state $\beta$ and write $a$ on the output, or $p$ is final, in that case $T_{1}$ may move to state $\beta$ while writing $a$ on the output, or move to the initial state of some automaton $A_{p,q}$ for some non-deterministically chosen state $q$, and write $a\#$ on the output. Then, its behaviour is the same as in $A_{q_{0},p}$, but now in $A_{p,q}$, etc.. Clearly, $T_{1}$ has a polynomial size in the size of $C_{1}$.

Now, we also want to check that $E_{i}||F_{i}$ for all subexpressions $E_{i},F_{i}$ that occur at the same position in some decomposition. Formally, let $S$ be the set of expressions $E,F$ such that there exists $u\in L(A_{1})\cap L(A_{2})$, such that $\text{dec}_{C_{1}}(u)=(u_{1},E_{1}),\dots,(u_{n},E_{n})$ and $\text{dec}_{C_{2}}(u)=(v_{1},F_{1}),\dots,(v_{m},F_{m})$ and there exists $i$ such that $E_{i}=E$ and $F_{i}=F$. We will show that $S$ can be computed in PTime. Once $S$ has been computed, for every pair $(\phi(C_{1},\dots,C_{n}),\phi^{\prime}(C^{\prime}_{1},\dots,C^{\prime}_{m}))\in S$, it suffices to call the algorithm on each pair $(C_{i},C^{\prime}_{j})$ for all $i,j$.

It remains to show that $S$ can be computed in polynomial time. Again, for all expressions $E,F$ occurring in the range of $\lambda_{1}$ and $\lambda_{2}$ respectively, one could define some automaton $A_{E,F}$ (of polynomial size) which accepts a word $u\in L(A_{1})\cap L(A_{2})$ iff $E,F$ occurs together in the respective decomposition of $u$, i.e. $\text{dec}_{C_{1}}(u)$ and $\text{dec}_{C_{1}}(u)$. Then, for all these pairs, if $L(A_{E,F})\neq\varnothing$ (which can be checked in PTime), then we add $(E,F)$ to $S$. To construct $A_{E,F}$, the idea is to simulate, via a product construction, an execution of $C_{1}$ and an execution of $C_{2}$ in parallel (by also simulating the smaller automata defining the regular languages on the transitions of $C_{1}$ and $C_{2}$). In this product construction, one bit of memory is used to remember whether a pair of states $(p_{1},p_{2})$ of $C_{1}$ and $C_{2}$ respectively, such that $E=\lambda_{1}(p_{1})$ and $F=\lambda_{2}(p_{2})$, was reached. The automaton accepts if such a pair was found, and the simulation of the two runs accept (meaning that $u\in L(A_{1})\cap L(A_{2})$). ∎

0.D.3 Closure properties of WCA: Proof of Proposition 6

Before proving the proposition, we need to intermediate results.

Lemma 7 (Unambiguous Concatenation)

Given two regular languages $L_{1},L_{2}$, if $L_{1}\odot L_{2}$ denotes the set of words $u$ which can be uniquely decomposed into $u_{1}u_{2}$ with $u_{i}\in L_{i}$, then there exists $2n$ regular languages $N_{i},M_{i}$ such that $N_{i}\subseteq L_{1}$ and $M_{i}\subseteq L_{2}$, and $L_{1}\odot L_{2}=\bigcup_{i=1}^{n}N_{i}M_{i}$.

Proof

Let $A_{1},A_{2}$ be two NFA recognising $L_{1},L_{2}$ respectively. We can construct an automaton $A$ that accepts the words in $L_{1}L_{2}$ which admits at least two different factorisations with respect to $L_{1},L_{2}$. It suffices to simulate two runs of $A_{1}$ in parallel, whenever a copy of $A_{1}$ goes to an accepting state, this copy either stays in $A_{1}$ or, thanks to an added $\epsilon$-transition, goes to some initial state of $A_{2}$. We also add one bit of memory to check that $\epsilon$-transitions have been taken at two different moments in the two simulated runs. The accepting states are states $(q_{2},q^{\prime}_{2},1)$ where $q_{2},q^{\prime}_{2}$ are accepting states of $A_{2}$. By complementing $A$, we obtain an automaton, say $B$, recognising $L_{1}\odot L_{2}$.

Now, we again make a kind of product between $B$, $A_{1}$ and $A_{2}$. If $Q$ are the states of $B$, $Q_{1}$ of $A_{1}$, $Q_{2}$ of $A_{2}$ (with initial states $I_{2}$), the set of states of this product is $Q\times(Q_{1}\uplus Q_{2}\uplus\overline{I_{2}})$ where $\overline{I_{2}}$ is a copy of $I_{2}$. $B$ initially runs in parallel of $A_{1}$ and, when $A_{1}$ enters an accepting state, i.e. the product is in state $(q,q_{1})$ where $q_{1}\in F_{1}$, then we add some $\epsilon$-transition to any state $(q,\overline{q_{2}})$ where $q_{2}\in I_{2}$. Then, from states of this form, the product continues its simulation of $B$ and simulates in parallel $A_{2}$ (in normal states $Q_{2}$, so that the copy $\overline{I_{2}}$ is only met once, when the product switches to $A_{2}$). Let denote by $B\times(A_{1}A_{2})$ this product. We set its accepting states to be any pair $(q,q_{2})$ or $(q,\overline{q_{2}})$ where $q_{2}$ is accepting and $q$ is accepting.

For all states $(q,p)$ of $B\times(A_{1}A_{2})$, we denote by $L_{q,p}$ and $R_{q,p}$ the left language of $(q,p)$ and the right language of $(q,p)$ respectively. We claim that

[TABLE]

Clearly, $\bigcup_{(q,\overline{q_{2}})\in Q\times\overline{I_{2}}}L_{q,q_{2}}R_{q,q_{2}}\subseteq L(B)$ since the product also checks that the input words are accepted by $B$. Conversely, if $u\in L(B)$, then it is uniquely decomposed into $u_{1}u_{2}$ where $u_{i}\in L(A_{i})$. From an accepting run $r=q_{1}\dots q_{n+1}p_{1}\dots p_{m+1}$ on $u$ (where $n=|u_{1}|$ and $m=|u_{2}|$), an accepting run $r_{1}=\alpha_{1}\dots\alpha_{n+1}$ of $A_{1}$ on $u_{1}$, and a accepting run $r_{2}=\beta_{1}\dots\beta_{m+1}$ of $A_{2}$, we can construct the following accepting run of $B\times(A_{1}A_{2})$: $(q_{1},\alpha_{1})\dots(q_{n+1},\alpha_{n+1})(p_{1},\overline{\beta_{1}})(p_{2},\beta_{2})\dots(p_{m+1},\beta_{m+1})$.∎

Proposition 10 (Domain regularity)

The domain of any gWCA is (effectively) regular.

Proof

Let $C=(A,\lambda)$ be an $m$-gWCA where $A=(Q,I,F,\Delta)$. We show by induction on $m$ that $\text{dom}(C)$ is (effectively) regular. If $m=0$ then $C$ is an unambiguous WA and its domain is (effectively) regular (given by its underlying (input) automaton). Otherwise, assume by induction hypothesis that for all $k<m$ the domain of any $k$-gWCA is (effectively) regular. We construct a generalized finite automaton to recognise $\text{dom}(C)$. Let $p,q\in Q$ and $\lambda(p,q)=(v_{1},\dots,v_{n})$. For all $i\in\{1,\dots,n\}$, we define $\text{dom}(v_{i})=\bigcap_{j=1}^{k}\text{dom}(C_{j})$ if $v_{i}=\phi(C_{1},\dots,C_{k})$. By induction hypothesis each $\text{dom}(v_{i})$ is (effectively) regular since all $C_{j}$ is a $m^{\prime}$-gWCA with $m^{\prime}<m$. Finally, we define $\text{dom}(\lambda(p,q))$ as $\bigcap_{i=1}^{n}\text{dom}(v_{i})$. By definition of $\text{dom}(C)$, the domain of $C$ is the language of the generalized finite automaton $A^{\prime}=(Q,I,F,\Delta^{\prime})$ where for all $q,p\in Q$ we have $\Delta^{\prime}(p,q)=\Delta(p,q)\cap\text{dom}(\lambda(p,q))$.∎

0.D.3.1 Proof of Proposition 6

Proof

Let $C_{1},\dots,C_{n}$ be WCA such that $\text{Sync}\{C_{1},\dots,C_{n}\}$ and $C,D$ two synchronised WCA. Let $\phi$ be a functional Presburger formula of arity $n$, and $L\subseteq\Sigma^{*}$ a regular language. We show that there exists synchronised WCA respectively denoted by $\phi(C_{1},\dots,C_{n})$, $C^{\circledast}$, $C\odot D$, $C\triangleright D$ and $C|_{L}$ such that

• •

$\text{dom}(\phi(C_{1},\dots,C_{n}))=\bigcap_{i=1}^{n}\text{dom}(C_{i})$ and for all $u\in\bigcap_{i=1}^{n}\text{dom}(C_{i})$,

[TABLE]

• •

$[\![C^{\circledast}]\!]=[\![C]\!]^{\circledast}$, $[\![C\odot D]\!]=[\![C]\!]\odot[\![D]\!]$ and $[\![C\triangleright D]\!]=[\![C]\!]\triangleright[\![D]\!]$, $[\![C|_{L}]\!]=[\![C]\!]|_{L}$.

Closure under star. $C^{\circledast}$ is the WCA $(A,\lambda)$ defined as follows. The only difficulty is that it should be unambiguous (because we want decomposition to be unique), hence it is not correct to add some $\epsilon$-transition from accepting states of $C$ to its initial states. However, it is possible to define an unambiguous NFA $B=(Q,I,F,\Delta)$ with a set of special states $S\subseteq Q$ such that $L(B)=\text{dom}(C)^{\circledast}$ and such that for all $u\in L(B)$, the occurrences of special states in the accepting run of $B$ on $u$ decomposes (uniquely) $u$ into factors that belong to $\text{dom}(C)$. Then, the states of $C^{*}$ are the states $S\cup I$, the initial states $I$, final states $S\cap F$, and $\Delta(s,s^{\prime})$ for all $s\in S\cup I$ and $s^{\prime}\in S$, is the set of words on which there is a run of $B$ from $s$ to $s^{\prime}$ that does not pass by any state of $S$ (except at the end and beginning). This set is easily shown to be regular. Finally, $\lambda(s,s^{\prime})=\phi_{id}(C)$ where $\phi_{id}$ defines the identity function.

Closure under regular domain restriction. If $C=(A,\lambda)$, then it suffices to take the product of $A$ with any DFA $B$ such that $L(B)=L$. Since $A$ is a generalised automaton, the product is a bit different than the usual automata product. Assume $A=(Q,I,F,\Delta)$ and $B=(P,p_{0},F^{\prime},\delta^{\prime})$ (a classical DFA). Then $A\times B=(Q\times P,I\times\{p_{0}\},F\times F^{\prime},\Delta\times\delta^{\prime})$ where for all $(q,p)$, $(q^{\prime},p^{\prime})$, $(\Delta\times\delta^{\prime})((q,p),(q^{\prime},p^{\prime}))$ is the set of words in $\Delta(q,q^{\prime})$ such that there exists a run of $B$ from state $p$ to state $p^{\prime}$. This set is effectively regular. The resulting generalized NFA is unambiguous since $B$ was taken to be deterministic and $A$ is unambiguous.

Closure under Presburger combinators. The WCA $\phi(C_{1},\dots,C_{n})$ is defined as:

\begin{array}[]{l|l}\Sigma^{*}&\phi(C_{1},\dots,C_{n})\end{array}

Closure under conditional choice. The WCA $C_{1}\triangleright C_{2}$ is defined as

\begin{array}[]{l|l}\text{dom}(C_{1})&\phi_{id}(C_{1})\end{array}$$\begin{array}[]{l|l}\text{dom}(C_{2})\setminus\text{dom}(C_{1})&\phi_{id}(C_{2})\end{array}

Note that $\text{dom}(C_{i})$ are regular by Proposition 10.

Closure under split sum. By Lemma 7, $\text{dom}(C_{1})\odot\text{dom}(C_{2})=\bigcup_{i=1}^{n}N_{i}M_{i}$ for some regular languages $N_{i}\subseteq\text{dom}(C_{1})$ and $M_{i}\subseteq\text{dom}(C_{2})$. For all $i=1,\dots,n$, we define the WCA $(C_{1}\odot C_{2})|_{N_{i}M_{i}}$ as depicted below:

\begin{array}[]{l|l}N_{i}&\phi_{id}(C_{1})\end{array}$$\begin{array}[]{l|l}M_{i}&\phi_{id}(C_{2})\end{array}

Note that it is unambiguous since $N_{i}M_{i}\subseteq\text{dom}(C_{1})\odot\text{dom}(C_{2})$, $N_{i}\in\text{dom}(C_{1})$ and $M_{i}\in\text{dom}(C_{2})$. Futhermore, for all $u\in N_{i}M_{i}$ such that $u=u_{1}u_{2}$ with $u_{1}\in\text{dom}(C_{1})$ and $u_{2}\in\text{dom}(C_{2})$ we have $[\![(C_{1}\odot C_{2})|_{N_{i}M_{i}}]\!](u)=[\![C_{1}]\!](u_{1})+[\![C_{2}]\!](u_{2})$. Finally, we let C_{1}\odot C_{2}=\scalebox{1.5}{\triangleright}_{i=1}^{n}(C_{1}\odot C_{2})|_{N_{i}M_{i}} (the way this expression is parenthesised, as well as the order in which the index $i$ are taken, does not change the semantics). ∎

0.D.4 The range of a WCA is Semi-Linear (Lemma 3)

Intuitions

Let us give the main intuitive ideas on how the proof works. Assume for time being that we consider a synchronised WCA $C=(A,\lambda)$ with a single state $q$, and hence a single transition from $q$ to $q$ on any word of $\Delta(q,q)$. Assume that $\lambda(q,q)=\phi(C_{1},\dots,C_{n})$. Then, in order to prove semilinearity of the range of $[\![C]\!]$, we have to show that the set $\{([\![C_{1}]\!](u),\dots,[\![C_{n}]\!](u)\mid u\in\Delta(q,q)\cap\bigcap\text{dom}(C_{i})\}$ is semi-linear. For a general synchronised WCA, if one wants to prove the result by induction on its structure, a stronger statements is needed, namely to consider tuples of WCA instead of a single one. A stronger statement would be formally the following: let $C_{1},\dots,C_{n}$ be WCA such that $\text{Sync}\{C_{1},\dots,C_{n}\}$. Then the set

[TABLE]

is effectively semi-linear. This statement clearly entails Lemma 3 by taking $n=1$.

In the case of monolithic expressions, we had to show a similar result, when the $C_{i}$ are replaced by unambiguous WA $A_{i}$. This was solved by doing a product construction, i.e. by definition a single unambiguous WA $A_{1}\times\dots\times A_{n}$ with values in $\mathbb{Z}^{n}$, for which it was easily shown semi-linearity.

The idea of the proof for WCA is similar. Thanks to synchronisation, we can also define a product construction of WCA. However, unlike the case of the product of unambiguous WA, for which semilinearity was shown by using reversal-bounded counter machines, it was not clear how to use these machines to encode the range of a product of WCA. The problem comes from iteration (induced for instance by cycles in WCA). Even if the range of some WCA can be defined by a reversal-bounded counter machine, iterating this counter machine on decompositions of input words may not yield a reversal-bounded counter machine anymore.

Therefore, our proof only rely on reversal-bounded counter machine for the base case (when the WCA are unambiguous WA). Then, the proof is inductive: we describe the decompositions of input words with some unambiguous regular expression, and transfer the operation of this regular expression into operations on semi-linear sets.

Product construction

First, to formally define the product construction, we extend the definition of WCA to WCA with values in $\mathbb{Z}^{k}$. We call them generalised WCA. A [math]-gWCA is a unambiguous WA with values in $\mathbb{Z}^{k}$. For $n>0$, an $n$-gWCA is defined as a WCA $(A,\lambda)$, except that $\lambda$ returns $k$-tuples of expressions of the form $E=\phi(C_{1},\dots,C_{n})$, where $C_{i}$ are $n$-gWCA and $\phi$ is a functional Presburger formula of arity $kn$ that returns a $k$-tuple of values (i.e. $\phi$ has $k(n+1)$ free variables the last $k$ of them being the result of the function). The semantics and the notion of synchronisation are both defined the same way as for WCA. Just to make it clear for synchronisation, $C_{1}=(A_{1},\lambda_{1})$ and $C_{2}=(A_{2},\lambda_{2})$ are synchronised if for all $u\in\text{dom}(C_{1})\cap\text{dom}(C_{2})$, let set:

[TABLE]

then $n=n^{\prime}$, for each $i\in[1..n]$, $j\in[1..m]$ and $j^{\prime}\in[1..m^{\prime}]$ we have $u_{i}=u^{\prime}_{i}$ and if $E_{i,j}$ and $E^{\prime}_{i,j^{\prime}}$ are of the respective form $\phi(C_{1},\dots,C_{\ell})$ and $\phi^{\prime}(C^{\prime}_{1},\dots,C^{\prime}_{\ell^{\prime}})$, then $C_{k}||C^{\prime}_{k^{\prime}}$ for all $k\in[1..\ell]$ and $k^{\prime}\in[1..\ell^{\prime}]$.

Product

If $C_{1},C_{2}$ are unambiguous WA with values in $\mathbb{Z}^{k_{1}}$ and $\mathbb{Z}^{k_{2}}$ respectively, then the product construction is a classical state product construction, whose transitions are valued in $\mathbb{Z}^{k_{1}+k_{2}}$. Given two $n$-gWCA $C_{1},C_{2}$ ($n>0$) such that $C_{i}=(Q_{i},I_{i},F_{i},\Delta_{i},\lambda_{i})$ for each $i\in[1..2]$, we define the product $C_{1}\times C_{2}=(Q_{1}\times Q_{2},I_{1}\times I_{2},F_{1}\times F_{2},\Delta,\lambda)$ where $\Delta((p_{1},p_{2}),(q_{1},q_{2}))=\Delta_{1}(p_{1},q_{1})\cap\Delta_{2}(p_{2},q_{2})$ and $\lambda((p_{1},p_{2}),(q_{1},q_{2}))=(\lambda_{1}(p_{1},q_{1}),\lambda_{2}(p_{2},q_{2}))$ for all $p_{1},q_{1}\in Q_{1}$ and $p_{2},q_{2}\in Q_{2}$.

Lemma 8

If $\text{Sync}\{C_{1},C_{2}\}$, then $\text{dom}(C_{1}\times C_{2})=\text{dom}(C_{1})\cap\text{dom}(C_{2})$ and for all $u\in\text{dom}(C_{1})\cap\text{dom}(C_{2})$, $[\![C_{1}\times C_{2}]\!](u)=([\![C_{1}]\!](u),[\![C_{2}]\!](u))$.

Proof

It is a direct consequence of the construction and the definition of synchronisation.∎

Semi-linearity for generalised WCA

We come to the main lemma of this section, which entails Lemma 3, by taking $n=1$ and since any WCA is a gWCA.

Lemma 9

Given a tuple $(C_{1},\dots,C_{n})$ of gWCA such that $\text{Sync}(\{C_{1},\dots,C_{n}\})$ then $\{([\![C_{1}]\!](u),\dots,[\![C_{n}]\!](u))\mid u\in\bigcap_{i=1}^{n}L(C_{i})\}$ is effectively semi-linear.

Proof

First, if $\text{Sync}\{C_{1},\dots,C_{n}\}$, then the $C_{i}$ are all $m$-gWCA for some $n$. It is because of the base case of the definition of synchronisation: weighted automata can be synchronised with weighted automata only. If $m=0$, then the $C_{i}$ are all unambiguous WA whose transitions are valued by tuples of integers, and we can take their product, whose range can be shown to be semi-linear, just as in the case of monolithic expressions (see Section 3).

Now, suppose that $m>0$. First, we construct the product $C=(\prod_{i=1}^{n}C_{i})$ of the gWCA $C_{i}$. By Lemma 8 we have $\text{dom}(C)=\bigcap_{i}\text{dom}(C_{i})$ and for all $u\in\text{dom}(C)$, $[\![C]\!](u)=([\![C_{1}]\!](u),\dots,[\![C_{n}]\!](u))$. Therefore, it suffices to show that $\text{Range}(C)=\{[\![C]\!](u)\mid u\in\text{dom}(C)\}$ is semi-linear to prove the lemma. Suppose that $C=(A,\lambda)$ where $A=(Q,I,F,\Delta)$ and $\lambda$ maps any pair $p,q\in Q$ to some $n$-ary tuple of expressions $\lambda(p,q)=(\phi_{1}(C_{1}^{1},\dots,C_{k_{1}}^{1}),\dots,\phi_{n}(C_{1}^{1},\dots,C_{k_{n}}^{1}))$. Wlog, we can assume that $\Delta(p,q)=\text{dom}(C_{j}^{i})$ for all $1\leq i\leq n$ and all $1\leq j\leq k_{i}$.

Otherwise, if $L=\bigcap_{1\leq i\leq n}\bigcap_{1\leq j\leq k_{i}}\text{dom}(C_{j}^{i})$ (which is regular by Proposition 10), we restrict the domain of any $C^{i}_{j}$ to $L$ and replace $\Delta(p,q)$ by $\Delta(p,q)\cap L$, this does not change the semantics of $C$. Closure under regular domain restriction was shown for synchronised (non-generalised) WCA (Proposition 6), but the same proof works for synchronised gWCA. With this assumption, we get $\text{dom}(C)=L(A)$. We also define

[TABLE]

Since the $C_{i}^{j}$ are $m^{\prime}$-WCA for $m^{\prime}<m$, by applying the induction hypothesis on the tuple $(C_{1}^{1},\dots,C_{k_{1}}^{1},\dots,C_{1}^{n},\dots,C_{k_{n}})$ (which are all mutually synchronised since $C$ is synchronised), we can show semilinearity of $S_{p,q}$.

Now, sets of $n$-tuple of integers have the structure of a monoid $(2^{\mathbb{Z}^{n}},+,\mathbb{0}_{n})$ where $+$ is defined by $S+S^{\prime}=\{s+s^{\prime}\mid s\in S,s^{\prime}\in S^{\prime}\}$ and $\mathbb{0}_{n}=\{(0,\dots,0)\}$ (tuple of arity $n$). Consider the free monoid over $Q\times Q$ and the morphism $\mu$ from this monoid to $(2^{\mathbb{Z}^{n}},+,\mathbb{0}_{n})$, defined by $\mu((p,q))=S_{p,q}$ for all $(p,q)\in Q\times Q$. It is easily shown that for any language regular language $N\subseteq(Q\times Q)^{*}$, $\mu(N)$ is semi-linear (and this is effective is $N$ is given, for instance, by a regular expression). It is because the $S_{p,q}$ are semi-linear, and semi-linear sets are (effectively) closed under sum, union, and Kleene star (see for instance [8]).

Finally, consider $N\subseteq(Q\times Q)^{*}$ defined as the set of words $(p_{1},p_{2})(p_{2},p_{3})\dots(p_{k-1},p_{k})$ such that $p_{1}$ is initial ($p_{1}\in I$), $p_{k}\in F$, and for all $i\in\{1,\dots,k-1\}$, $\Delta(p_{i},p_{i+1})\neq\varnothing$. We prove the following statements:

$N$ is regular 2. 2.

$\mu(N)$ is semi-linear 3. 3.

$\text{Range}(C)=\mu(N)$.

Clearly, 2. and 3. gives the desired result, namely that $\text{Range}(C)$ is semi-linear. Let us prove the statements:

1. Let $A_{p,q}$ be the NFA recognising $\Delta(p,q)$. It is simple to combine the automata $A_{p,q}$ such that $\Delta(p,q)\neq\varnothing$ into a single automaton recognising $N$. For instance, one can take the disjoint union of all $A_{p,q}$ such that $\Delta(p,q)\neq\varnothing$, add the states of $A$, with $I$ the set of initial states and $F$ the set of final states, and add the following $\epsilon$-transitions: from any state $p\in Q$, add $\epsilon$-transitions to the initial states of any NFA $A_{p,q}$, and from any final state of any automaton $A_{p,q}$, add some $\epsilon$-transition to $q$.

2. Since $N$ is regular, by the remark above, we get that $\mu(N)$ is semi-linear.

3. $\subseteq$: Let $\overline{x}\in\text{Range}(C)$. Hence, there exists $u\in\text{dom}(C)$ such that $[\![C]\!](u)=\overline{x}$. Let $p_{1}\xrightarrow{u_{1}}p_{2}\xrightarrow{u_{2}}p_{3}\dots p_{k}\rightarrow{u_{k}}p_{k+1}$ be the accepting run of $A$ and $u$, i.e. $u_{i}\in\Delta(p_{i},p_{i+1})$ for all $i=1,\dots,k$. We also have $\alpha=(p_{1},p_{2})(p_{2},p_{3})\dots(p_{k},p_{k+1})\in N$. By the semantics of WCA, $\overline{x}=\overline{x_{1}}+\dots+\overline{x_{k}}$ where $\overline{x_{i}}=[\![\lambda(p_{i},p_{i+1})]\!](u_{i})$ for all $i=1,\dots,k$. Hence $\overline{x_{i}}\in S_{p_{i},p_{i+1}}$ and $\overline{x}\in\mu(\alpha)\subseteq\mu(N)$.

4. $\supseteq$: Let $\overline{x}\in\mu(N)$. By definition of $\mu$ and $N$, there exists $\alpha=(p_{1},p_{2})\dots(p_{k},p_{k+1})\in N$ such that $\overline{x}\in S_{p_{1},p_{2}}+\dots+S_{p_{k},p_{k+1}}$, and hence $\overline{x}=\sum_{i=1}^{k}\overline{x_{i}}$ for some $\overline{x_{i}}\in S_{p_{i},p_{i+1}}$. By definition of the $S_{p_{i},p_{i+1}}$, there exists $u_{1},\dots,u_{k}\in\Sigma^{*}$ such that $u_{i}\in\Delta(p_{i},p_{i+1})$ and $\overline{x_{i}}=[\![\lambda(p_{i},p_{i+1})]\!](u_{i})$. Moreover, by definition of $N$, $p_{1}$ is initial and $p_{k+1}$ is final, hence $u_{1}\dots u_{k}\in\text{dom}(C)$, and by the semantics of $C$, $[\![C]\!](u)=\sum_{i}\overline{x_{i}}$, i.e. $\overline{x}\in\text{Range}(C)$. ∎

0.D.5 Proof of Theorem 5.2

We actually prove the stronger statement below.

Lemma 10

For all tuples of i-expressions $\mathbb{E}=(E_{1},\dots,E_{n})$ such that $\text{Sync}(\mathbb{E})$, one can construct a tuple of WCA $\mathbb{C}=(C_{1},\dots,C_{n})$ such that the following condition hold:

for all $i\in\{1,\dots,n\}$, $\text{dom}(C_{i})=\bigcap_{j=1}^{n}\text{dom}(E_{j})$, 2. 2.

for all $i\in\{1,\dots,n\}$, for all $u\in\bigcap_{j=1}^{n}\text{dom}(E_{j})$, $[\![E_{i}]\!](u)=[\![C_{i}]\!](u)$, 3. 3.

$\text{Sync}(\mathbb{C})$.

Applied on $\mathbb{E}=(E)$, the latter lemma shows Theorem 5.2.

0.D.5.1 Notations

For an i-expression $E$, we define $||E||\in\mathbb{N}$ inductively by $||A||=0$, $||E^{\circledast}||=||E||+1$, $||\phi(E_{1},E_{2})||=1+||E_{1}||+||E_{2}||$. For a tuple $\mathbb{E}=(E_{1},\dots,E_{n})$ of i-expressions, we let $||\mathbb{E}||=\sum_{i=1}^{n}||E_{i}||$.

0.D.5.2 Proof of Lemma 10

Proof

The proof goes by induction on $||\mathbb{E}||$. If $||\mathbb{E}||=0$, then all expressions in $\mathbb{E}$ are unambiguous WA $A_{1},\dots,A_{n}$, and hence are [math]-WCA. However, the conditions in the lemma requires that the domains of all WCA are equal to $D=\bigcap_{i=1}^{n}\text{dom}(A_{i})$. It suffices to restrict $A_{1},\dots,A_{n}$ to $D$, which is always possible since unambiguous WA are closed under regular domain restriction, and $D$ is regular. One obtains unambiguous WA $A^{\prime}_{1},\dots,A^{\prime}_{n}$, i.e. [math]-WCA, which satisfy the requirements of the Lemma (for condition 3., by the definition of synchronisation, both for i-expressions and WCA, unambiguous WA are always mutually synchronised). The case $||\mathbb{E}||>0$ is more involved and is a disjunction of three cases.

Case 1 There exists $i$ such that $E_{i}=\phi(F_{1},F_{2})$ Then we define the tuple999Note that this case exhibits already the need to consider tuples of expressions rather a single expression, to prove Theorem 5.2 inductively.

[TABLE]

which satisfies $\text{Sync}(\mathbb{E}^{\prime})$ by definition of synchronisation for i-expressions. We also have $||\mathbb{E}^{\prime}||<||\mathbb{E}||$, hence we can apply the induction hypothesis on $\mathbb{E}^{\prime}$, and obtain a tuple

[TABLE]

of WCA such that, if we let $D^{\prime}=\bigcap_{\alpha\in\mathbb{E^{\prime}}}\text{dom}(\alpha)$, we have the property $\star$:

• •

for all $j\neq i$, $\text{dom}(C_{j})=\text{dom}(C_{i}^{1})=\text{dom}(C_{i}^{2})=D^{\prime}$,

• •

for all $j\neq i$, $[\![E_{j}]\!]|_{D^{\prime}}=[\![C_{j}]\!]$, $[\![F_{1}]\!]|_{D^{\prime}}=[\![C_{i}^{1}]\!]$, $[\![F_{2}]\!]|_{D^{\prime}}=[\![C_{i}^{2}]\!]$,

• •

$\text{Sync}(\mathbb{C^{\prime}})$.

We return the tuple of WCA

[TABLE]

where $\phi_{id}$ is a Presburger-formula denoting the identity function, and the Preburger operations on WCA has been defined in Proposition 6. We return $\phi_{id}(C_{j})$ instead of $C_{j}$ for all $j\neq i$, to preserve synchronisation. Indeed, the definition of synchronisation for WCA implies that all WCA in $\mathbb{C}^{\prime}$ are $k$-WCA for some $k$, and that a $k_{1}$-WCA and a $k_{2}$-WCA are never synchronised when $k_{1}\neq k_{2}$. Now, $\phi(C_{i}^{1},C_{i}^{2})$ is a $(k+1)$-WCA, as well as $\phi_{id}(C_{j})$ for all $j\neq i$, and synchronisation is preserved, i.e. $\text{Sync}(\mathbb{C})$ is true.

Let us show the correctness, i.e., if $D=\bigcap_{j}\text{dom}(E_{j})$, we must show that

for all $C\in\mathbb{C}$, $\text{dom}(C)=D$ 2. 2.

for all $j\neq i$, $[\![E_{j}]\!]|_{D}=[\![\phi_{id}(C_{j})]\!]$, $[\![E_{i}]\!]|_{D}=[\![\phi(C_{1}^{i},C_{2}^{i})]\!]|_{D}$.

Since $\text{dom}(\phi(F_{1},F_{2}))=\text{dom}(F_{1})\cap\text{dom}(F_{2})$, we have $D=D^{\prime}$. Now, for all $j\neq i$, we have $\text{dom}(\phi_{id}(C_{j}))=\text{dom}(C_{j})=D^{\prime}$ (by $\star$), hence $\text{dom}(\phi_{id}(C_{j}))=D$, and $[\![E_{j}]\!]|_{D}=[\![E_{j}]\!]|_{D^{\prime}}=[\![C_{j}]\!]$ (by star), which is again equal to $[\![\phi_{id}(C_{j})]\!]$. Finally, $\text{dom}(\phi(C_{i}^{1},C_{i}^{2}))=\text{dom}(C_{i}^{1})\cap\text{dom}(C_{i}^{2})=D^{\prime}$ (by $\star$), which equals $D$, and $[\![\phi(F_{1},F_{2})]\!]|_{D}=\{\phi(v_{1},v_{2})\mid v_{\ell}\in[\![F_{i}]\!]|_{D}\}=\{\phi(v_{1},v_{2})\mid v_{\ell}\in[\![C_{i}^{\ell}]\!]\}=[\![\phi(C_{i}^{1},C_{i}^{2})]\!]$.

Case 2 $\mathbb{E}=(F_{1}^{\circledast},\dots,F_{n}^{\circledast})$. In this case we apply our induction hypothesis on $(F_{1},\dots,F_{n})$ (which is synchronised since $(F_{1}^{\circledast},\dots,F_{n}^{\circledast})$ is synchronised), obtain a tuple of WCA $(C_{1},\dots,C_{n})$, and return $(C_{1}^{\circledast},\dots,C_{n}^{\circledast})$ (the sharp operation ⊛ on WCA has been defined in Proposition 6).

Let us show the correctness. By synchronisation of $\mathbb{E}$, there is $D\subseteq\Sigma^{*}$ such that $D=\text{dom}(F_{1})=\dots=\text{dom}(F_{n})$. Let $i\in\{1,\dots,n\}$. By induction hypothesis, $\text{dom}(C_{i})=\bigcap_{j}\text{dom}(F_{j})=D$ and $[\![F_{i}]\!]|_{D}=[\![C_{i}]\!]$. Now, for all $i,j\in\{1,\dots,n\}$,

[TABLE]

We remind that $L^{\#}$ is the set of words that are uniquely decomposed by factors in $L$. In particular, $\text{dom}(C_{i}^{\circledast})=\bigcap_{j}\text{dom}(F_{j}^{\circledast})$, satisfying condition (1) of the Lemma. Let us show condition (2). Let $u\in\text{dom}(C_{i}^{\circledast})$,

[TABLE]

where $u_{1}\dots u_{p}$ is the unique decomposition of $u$ into factors in $L$. Finally, to show condition (3), by induction hypothesis we have $\text{Sync}\{C_{1},\dots,C_{n}\}$ and by construction of $C_{1}^{\circledast},\dots,C_{n}^{\circledast}$ and since all $C_{i}$ have the same domain, synchronisation is preserved.

Case 3 The automata and star expressions are mixed, i.e. each $E_{i}$ is either an unambiguous WA or an iterated expression. This case is the most technical. Let us explain the construction with only a single automaton and a single star expression, i.e. $\mathbb{E}=(A,F^{\circledast})$. The case where there are arbitrarily many automata and star expressions is more technical but not more difficult, the main difficulties being found in this special case. The difficulty comes from the fact that $A$ and $F$ does not apply at the same “level”: $A$ runs on the whole input word, while $F$ runs on factors of it. The definition of synchronisation for WCA requires that any two synchronised WCA must “run” at the same level. In this sense, the definition of synchronisation may seem a bit strong, unlike that of synchronisation of i-expressions, but it makes the decidability (and in particular the semi-linearity property – see Lemma 3) way easier to prove, because it allows for a product construction, just as in the non-iterated case (monolithic expressions).

Hence, we have to decompose $A$ into “partial” weighted automata that will run on factors of the input word in $\text{dom}(F)$. We assume wlog that $A$ is trim101010All its states are accessible from an initial state and co-accessible from a final state. It is well-known that any automaton can be trimmed in polynomial time., and for all states $p_{1},p_{2}$ of $A$, define $A_{p_{1},p_{2}}$ to be $A$ with only initial state $p_{1}$ and only accepting state $p_{2}$. Since $A$ is unambiguous and trim, so are the WA $A_{p_{1},p_{2}}$.

Let $B$ be a DFA accepting the set of words $u$ that are uniquely decomposed into factors in $\text{dom}(F)$ (see the proof of Proposition 8 for a construction of $B$). For all states $q_{1},q_{2}$ of $B$, let $L_{q_{1},q_{2}}$ be the set of words in $\text{dom}(F)$ such that there exists a run of $B$ from state $q_{1}$ to state $q_{2}$. Clearly:

[TABLE]

Now, for all states $p_{1},p_{2}$ of $A$ and all states $q_{1},q_{2}$ of $B$, define $A_{p_{1},p_{2},q_{1},q_{2}}$ as the WA $A_{p_{1},p_{2}}$ restricted to the domain $L_{q_{1},q_{2}}$. It can be assumed to be unambiguous as well, since $A_{p_{1},p_{2}}$ is unambiguous. Then, apply the induction hypothesis on the pairs $(A_{p_{1},p_{2},q_{1},q_{2}},F)$ (which is synchronised) to get equivalent synchronised WCA $(C_{p_{1},p_{2},q_{1},q_{2}}^{1},C_{p_{1},p_{2},q_{1},q_{2}}^{2})$.

We now explain how to combine these WCA into a pair of WCA $(C_{1},C_{2})$ equivalent to $(A,F^{*})$ (on $\text{dom}(A)\cap\text{dom}(F^{*})$). We will return the tuple $(C_{1},C_{2})$. Let $C_{p_{1},p_{2},q_{1},q_{2}}=C_{p_{1},p_{2},q_{1},q_{2}}^{1}\times C_{p_{1},p_{2},q_{1},q_{2}}^{2}$, the product of this two WCA (hence with values in $\mathbb{Z}^{2}$). We now have to combine all these WCA into a single one $C$ running on the whole input word. We construct $C$ by taking the union of all WCA $C_{p,p^{\prime},q,q^{\prime}}$, and by “merging”, for all states $p_{1},p_{2},p_{3}$ of $A$ and all states $q_{1},q_{2},q_{3}$ of $B$, the accepting states of $C_{p_{1},p_{2},q_{1},q_{2}}$ with the initial states of $C_{p_{2},p_{3},q_{2},q_{3}}$. The merging operation is non-deterministic, because we may need to stay in the automaton $C_{p_{1},p_{2},q_{1},q_{2}}$ even if we have already seen one of its accepting state: when $C_{p_{1},p_{2},q_{1},q_{2}}$ triggers a transition to one of its accepting state, it either go to it, or to some initial state of $C_{p_{2},p_{3},q_{2},q_{3}}$. The initial states of $C$ are the initial states of any $C_{p,p^{\prime},q,q^{\prime}}$ such that $p$ is initial in $A$, $q$ is initial in $B$. The accepting states of $C$ are the accepting states of any $C_{p,p^{\prime},q,q^{\prime}}$ such that $p^{\prime}$ is accepting in $A$ and $q^{\prime}$ is accepting in $B$. That way, we have $\text{dom}(C)=\text{dom}(A)\cap\text{dom}(F^{\circledast})$.

The WCA $C_{1},C_{2}$ are obtained from $C$ by projecting the pairs of expressions occurring in $C$ to their first and second component respectively.

Finally, let us sketch how to proceed if there are more than one automaton $A_{1},\dots,A_{n}$ in $\mathbb{E}$ and more than one star expression $F_{1}^{\circledast},\dots,F_{m}^{\circledast}$ in $\mathbb{E}$. The idea is very similar, but we consider an automaton $B$ that accept all words that are uniquely decomposed according to $\bigcap_{j}\text{dom}(F_{j})$. Since the star expressions are synchronised, they all decompose the input word the same way, making this construction sound. Then, in the sub-weighted automata $A_{p,p^{\prime},q,q^{\prime}}$, $p$ and $p^{\prime}$ are instead tuples of states of each automata $A_{j}$.∎