Boundedness of Cost Register Automata over the Integer Min-Plus Semiring

Draghici, Andrei; Piórkowski, Radosław; Ryzhikov, Andrew

doi:10.4230/LIPIcs.CSL.2025.20

Boundedness of Cost Register Automata over the Integer Min-Plus Semiring

Andrei Draghici

Department of Computer Science, University of Oxford, UK Radosław Piórkowski

Department of Computer Science, University of Oxford, UK Andrew Ryzhikov

Department of Computer Science, University of Oxford, UK

Abstract

Cost register automata (CRAs) are deterministic automata with registers taking values from a fixed semiring. A CRA computes a function from words to values from this semiring. CRAs are tightly related to well-studied weighted automata. Given a CRA, the boundedness problem asks if there exists a natural number $N$ such that for every word, the value of the CRA on this word does not exceed $N$ . This problem is known to be undecidable for the class of linear CRAs over the integer min-plus semiring $(\mathbb{Z}\cup\{+\infty\},\min,+)$ , but very little is known about its subclasses. In this paper, we study boundedness of copyless linear CRAs with resets over the integer min-plus semiring. We show that it is decidable for such CRAs with at most two registers. More specifically, we show that it is, respectively, NL-complete and in coNP if the numbers in the input are presented in unary and binary. We also provide complexity results for two classes with an arbitrary number of registers. Namely, we show that for CRAs that use the minimum operation only in the output function, boundedness is PSPACE-complete if transferring values to other registers is allowed, and is coNP-complete otherwise. Finally, for each $f_{i}$ in the hierarchy of fast-growing functions, we provide a stateless CRA with $i$ registers whose output exceeds $N$ only on runs longer than $f_{i}(N)$ . Our construction yields a non-elementary lower bound already for four registers.

Keywords and phrases:

cost register automata, boundedness, decidability

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Quantitative automata

Acknowledgements:

We thank the anonymous reviewers for their helpful comments.

Funding:

^†^†margin:

All authors are supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).

DOI:

10.4230/LIPIcs.CSL.2025.20

Event:

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Editors:

Jörg Endrullis and Sylvain Schmitz

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

A cost register automaton (CRA), introduced by Alur et al. [3], is a deterministic finite automaton over finite words equipped with a finite set of registers storing values from a fixed semiring. When a CRA reads a word, the values of its registers are updated in a write-only way using the semiring operations, and at the end it outputs a value from the semiring. Thus, a CRA defines a function from finite words to elements of a semiring. CRAs can hence be used to model quantitative behaviour of systems, and are tightly related to well-studied weighted automata (WAs) introduced by Schützenberger in [36], see also surveys [18, 19]. In this context, a fundamental question is, given a CRA or WA, to decide if a certain property of the function computed by it (or even just a property of the image of this function) holds.

In this paper, we study the boundedness problem, which, given a CRA, asks if there exists a natural number $N$ such that the output of the CRA on every input is smaller than $N$ . As discussed in more detail below, very little is known about decidability of this problem compared to other natural problems for WAs and CRAs. Our work thus addresses and partially closes this gap, by studying it for restricted classes of CRAs. Below we provide an overview of such classes, and put them in the context of known classes of WAs.

We concentrate on CRAs over the integer min-plus semiring $(\mathbb{Z}\cup\{+\infty\},\min,+)$ . All CRAs are thus assumed to be over this semiring unless stated otherwise. Such CRAs can be seen as a variant of counter automata, specifically, as an extension of integer vector addition systems with states [21, 8]. Reachability properties of the latter are characterised by Presburger arithmetic, the first order theory of integer numbers with addition and order [21], which has good algorithmic features. For CRAs over the integer min-plus semiring, the situation changes significantly due to the presence of minimum operations in the updates. This makes the computed functions highly nonlinear: for example, they can compute iterated minimums. The results for integer vector addition systems thus cannot be directly used for CRAs. On the positive side, for subclasses of CRAs with decidable properties, this opens a possibility of finding new decidable extensions of Presburger arithmetic, by finding logical characterisation of the functions computed by CRAs from such subclasses.

More generally, many fundamental properties of CRAs and WAs can be defined by simple formulas in first-order logic, and can thus be considered as model checking CRAs against a fixed formula. For example, boundedness can be expressed by the formula

\exists N\in\mathbb{Z}\cup\{+\infty\}.\enspace N<+\infty\land\forall v\in% \mathbb{Z}\cup\{+\infty\}.\enspace\mathcal{I}(v)\to(v<N),

where $\mathcal{I}(v)$ is the predicate that holds true for $v\in\mathbb{Z}\cup\{+\infty\}$ if and only if the CRA outputs the value $v$ on some word. Understanding the decidability landscape of natural properties such as boundedness can thus be seen as a first step towards much more general model checking algorithms for subclasses of CRAs and WAs.

Relations between CRAs and WAs

In general, CRAs are strictly more expressive than WAs [3]. However, WAs are equally expressive to linear CRAs, which are CRAs where the updates of the registers are restricted to affine transformations. Transforming a linear CRA into an equivalent WA and vice versa can be done in polynomial time [3]. Hence, linear CRAs can be seen as a deterministic model for inherently nondeterministic WAs. WAs, and thus CRAs, find their applications in the areas of language and speech processing [34], verification [9], image processing [10], and the analysis of on-line algorithms [5] and probabilistic systems [39]. Functions computable by WAs are exactly those that can be defined in weighted monadic second order logic, a natural extension of monadic second order logic [16, 17]. Functions computed by a subclass of CRAs were also characterised in [31] by maximal partition logic, a logic with regular quantifiers that allow to partition words into segments and then aggregate the values computed for them.

Ambiguity hierarchy of WAs

To make decision problems tractable for WAs, it is usually required to restrict their expressiveness. The most well-studied way of doing that is by bounding the ambiguity, that is, the number of accepting runs labelled by a word. A WA is called finitely (respectively, linearly, polynomially or exponentially) ambiguous if there exists a constant (respectively, a linear, polynomial or exponential) function $f(n)$ such that for every word $w$ the number of accepting runs labelled by $w$ is bounded by $f(|w|)$ . If $f(n)=1$ , a WA is called unambiguous. Most classical decision problems, such as universality, inclusion and equivalence, are undecidable already for linearly ambiguous WAs over the integer min-plus semiring [28, 1, 12]. For finitely ambiguous WAs over this semiring, universality, inclusion and equivalence become decidable [40, 23].

For the boundedness problem, the situation is very different. A seminal paper [1] establishes undecidability of several classical decision problems for linearly ambiguous WAs over the integer min-plus semiring in a uniform fashion. However, it only proves boundedness to be undecidable for general (that is, exponentially ambiguous) WAs, and provides no classes with decidable boundedness. This indicates that boundedness is somehow different to other mentioned decision problems.

We remark that boundedness is PSPACE-complete for WAs over the natural min-plus semiring $(\mathbb{N}\cup\{+\infty\},\min,+)$ [1, 22, 29, 37], which requires completely different techniques than the integer case. We also remark that it is decidable for copyless linear CRAs over the semiring of positive rational numbers with usual addition and multiplication, and is undecidable for general WAs over the same semiring [11]. Transferring any such results to the min-plus semiring is unlikely, since these semirings has very different properties.

Restricted classes of CRAs

One useful feature of CRAs is that, by adding syntactic restrictions on them, it is possible to introduce subclasses whose expressiveness is incomparable to known classes of WAs. This allows to obtain a finer decidability landscape compared to the case where only the formalism of WAs is used.

One notable example of that is the class of so called copyless linear CRAs. Informally, a CRA is called copyless if for every transition, the value of each of its registers can only be used once in the updates. Copyless linear CRAs are strictly less expressive than linearly ambiguous WAs, and their expressivity is incomparable to unambiguous WAs [2]. A further restriction of copyless linear CRAs to the case where the minimum operation is only allowed in the output function makes them equally expressive to finitely sequential WAs, which are unions of WAs whose underlying NFAs are deterministic [4, 13].

Restricting the number of registers in a class of CRAs also usually provides a subclass whose expressivity is incomparable to that of known classes of WAs. For example, there exists a copyless (but not linear) CRA with only $3$ registers that computes a function not computed by any polynomially ambiguous WA [32]. For copyless linear CRAs restricted to only three registers universality is undecidable [15]. Moreover, there exist copyless linear CRAs with only two registers that are not equivalent to any unambiguous WA [2], see Example 6 on page 6 for one such CRA. All these results indicate that CRAs with few registers are quite expressive. Results on finding a CRA with the minimum number of registers computing a given function are presented in [13, 14, 25, 26].

More generally, for many problems the case of automata with two counters or registers often turns out to be already difficult enough. For example, most decision problems are undecidable for two-counter automata [33]. For vector addition systems with states, decidability of the reachability problem in the two-counter case was established in a seminal paper [24] several years before the proof that it is decidable for arbitrary number of counters was found [30], and it took over 20 more years to establish the precise computational complexity of the two-counter case [7].

Our contributions

The main technical contribution of the paper, Theorem 17, states that boundedness is decidable for copyless linear CRAs with resets with at most two registers. Namely, we show that it is NL-complete if the numbers in the updates are presented in unary, and is in coNP is they are presented in binary. Functions computed by CRAs, even when they have only two registers, are highly nonlinear and complex, mainly due to the presence of nested minimum operations. We illustrate this by providing in Section 6 a series of CRAs with very long shortest runs outputting a given value. To show that the two-register case is decidable, we identify several possible shapes of small witnesses of unboundedness (Section 4.2). The main challenge is then showing that if a CRA is unbounded, it contains one of these witnesses, which we do by carefully analysing the growth of the output value for a run providing a large enough value, and showing how to rearrange the cycles of this run to obtain a witness (Section 4.3). This requires in particular some geometrical arguments on the cones generated by the weight vectors of the cycles.

Our second contribution is establishing the complexity of boundedness for copyless linear CRAs with resets where the number of registers is arbitrary, but the minimum operation only occurs in the output function. As mentioned above, such CRAs compute the same class of functions as finitely sequential WAs. We show that boundedness is PSPACE-complete if registers are allowed to transfer values to other registers (Theorem 33), and is coNP-complete otherwise (Theorem 32). For upper bounds on the complexity, our techniques again rely on the combinatorial and geometrical analysis of cycles.

2 Main definitions

Symbols $\mathbb{N}$ and $\mathbb{Z}$ stand for natural and integer numbers respectively. Let $\mathbb{N}_{+}\coloneqq\mathbb{N}\setminus\left\{0\right\}$ . We assume that the reader is familiar with the basic concepts in the area of formal languages and automata, see e.g. [38]. The Kleene star is denoted as $(\mskip 1.5mu\cdot\mskip 1.5mu)^{*}$ . In regular expressions, we write $\cup$ for the sum and $\varepsilon$ for the empty string. The language of a nondeterministic finite automaton (NFA) $\mathcal{A}$ is denoted as $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ . When speaking of underlying digraphs of NFAs, we use standard terms like simple cycle, reachability and backwards-reachability. We emphasise that by a simple cycle we mean a cycle that does not visit the same vertex more than once, except for its first and last vertex. General cycles do not have this restriction.

In this paper, we focus on CRAs over the integer min-plus semiring $(\mathbb{Z}\cup\left\{+\infty\right\},\min,{+})$ . Hence, in what follows, we fix $\mathbb{K}\coloneqq(\mathbb{Z}\cup\left\{+\infty\right\},\min,{+})$ . For the proofs we present, the main focus lies on the operations on registers performed by CRAs, so we look at them in depth in Section 2.1. Then, in Section 2.2, we define CRAs and the boundedness problem.

2.1 Expressions, valuations and substitutions

Fix a finite set of variables $X$ . By $\text{{{Expr}}}\left(X\right)$ we denote the set of expressions constructed using operations $\min\left\{\mskip 1.5mu\cdot\mskip 1.5mu,\mskip 1.5mu\cdot\mskip 1.5mu\right\}$ and $+$ , variables from $X$ and constants from $\mathbb{K}$ . Expressions can be seen as polynomials over $\mathbb{K}$ . Due to associativity, we allow arbitrary arity of the semiring operations in the expression notation. For an expression $e\in\text{{{Expr}}}\left(\emptyset\right)\subseteq\text{{{Expr}}}\left(X\right)$ without variables, we denote by $\text{{{eval}}}\left(e\right)\in\mathbb{K}$ its value.

A substitution over $X$ is a function $\nu\colon X\to\text{{{Expr}}}\left(X\right)$ . We denote the set of all substitutions over $X$ by $\text{{{Sub}}}\left(X\right)$ . When defining substitutions, we often treat them as sets of “ $\mathit{argument}\leftarrow\mathit{value}$ ” pairs. When $X$ is clear from the context, we implicitly extend partial substitutions with the identity mapping for the omitted arguments. For example, if $X^{\prime}=\left\{x_{1},x_{2}\right\}\subsetneq X$ , then $\nu=\left\{x_{1}\leftarrow e_{1},\;x_{2}\leftarrow e_{2}\right\}$ denotes a substitution satisfying $\nu(x_{i})=e_{i}$ for $x_{i}\in X^{\prime}$ and $\nu(x)=x$ for $x\in X\setminus X^{\prime}$ . A valuation over $X$ is a substitution $\mu\colon X\to\mathbb{K}$ . We denote by $\text{{{Val}}}\left(X\right)\subset\text{{{Sub}}}\left(X\right)$ the set of all valuations over $X$ . We write $\mathrm{\mathbf{0}}\in\text{{{Val}}}\left(X\right)$ for the valuation with $\mathrm{\mathbf{0}}(x)=0$ for every $x\in X$ . We assume that there is a fixed order on the set of registers, and thus in particular consider valuations equivalently as vectors.

Example 1 (An expression, a substitution and a valuation).

Fix $X\coloneqq\left\{x,y,z\right\}$ .

$\displaystyle e$	$\displaystyle\coloneqq\min\left\{10,x+5,y+z\right\}$	$\displaystyle\hskip-45.52458pt\in\text{{{Expr}}}\left(X\right)$	(an expression)
$\displaystyle\nu$	$\displaystyle\coloneqq\left\{x\leftarrow 2+\min\left\{x,y\right\},\;y% \leftarrow 3\right\}$	$\displaystyle\hskip-45.52458pt\in\text{{{Sub}}}\left(X\right)$	(a substitution)
$\displaystyle\mu$	$\displaystyle\coloneqq\left\{x\leftarrow 2,\;y\leftarrow 5,\;z\leftarrow 10\right\}$	$\displaystyle\hskip-45.52458pt\in\text{{{Val}}}\left(X\right)$	(a valuation)

Substitutions can be applied to expressions: given $e\in\text{{{Expr}}}\left(X\right)$ and $\nu\in\text{{{Sub}}}\left(X\right)$ , by $e[\nu]$ we denote the result of simultaneously replacing each occurrence of $x$ with $\nu(x)$ for every $x\in X$ . Substitutions can be composed: for $\nu,\nu^{\prime}\in\text{{{Sub}}}\left(X\right)$ , we define the composition $(\nu;\nu^{\prime})\in\text{{{Sub}}}\left(X\right)$ as $(\nu;\nu^{\prime})(x)=\nu^{\prime}(x)[\nu]$ . Applying a valuation $\mu$ to an expression $e$ yields an expression without variables – thus, with a defined value from $\mathbb{K}$ . We hence define $\text{{{eval}}}_{\mu}\left(e\right)\coloneqq\text{{{eval}}}\left(e[\mu]\right)$ . For a valuation $\mu$ and a substitution $\nu$ , we let $\text{{{eval}}}_{\mu}\left(\nu\right)\coloneqq\text{{{eval}}}\left(\mu;\nu\right)$ .

Example 2 (Application and composition of substitutions).

Continuing Example 1, we have

$\displaystyle e[\nu]$	$\displaystyle=\min\left\{10,(2+\min\left\{x,y\right\})+5,(3)+(z)\right\}$	$\displaystyle\hskip 0.0pt\in\text{{{Expr}}}\left(X\right)$	( $e$ with $\nu$ applied to it)
$\displaystyle e[\mu]$	$\displaystyle=\min\left\{10,(2)+5,(5)+(10)\right\}$	$\displaystyle\hskip 0.0pt\in\text{{{Expr}}}\left(\emptyset\right)$	( $e$ with $\mu$ applied to it)
$\displaystyle\text{{{eval}}}_{\mu}\left(e\right)$	$\displaystyle=\text{{{eval}}}\left(e[\mu]\right)=7$	$\displaystyle\hskip 0.0pt\in\mathbb{K}$	(the value of $e[\mu]$ )

For $e,e^{\prime}\in\text{{{Expr}}}\left(X\right)$ , we write $e\equiv e^{\prime}$ if $\text{{{eval}}}_{\mu}\left(e\right)=\text{{{eval}}}_{\mu}\left(e^{\prime}\right)$ for every $\mu\in\text{{{Val}}}\left(X\right)$ . Additionally, for $\nu,\nu^{\prime}\in\text{{{Sub}}}\left(X\right)$ , we write $\nu\equiv\nu^{\prime}$ whenever $\nu(x)\equiv\nu^{\prime}(x)$ for every $x\in X$ . For an expression $e$ , by $\text{{{maxc}}}\left(e\right)$ we denote the maximal absolute value of constants different to $+\infty$ appearing in $e$ , and $0$ if there are none. We extend maxc naturally to substitutions.

Copyless linear substitution with resets

In this paper, our main focus is on a special family of substitutions which are copyless and linear with resets. An expression $e$ is in a canonical linear form if

\displaystyle e=\min\left\{x_{1}+c_{1},x_{2}+c_{2},\ldots,x_{k}+c_{k}\right\}

for some pairwise-different $x_{1},\ldots,x_{k}\in X$ , $c_{1},\ldots,c_{k}\in\mathbb{K}$ , and $k\in\mathbb{N}$ . Any expression $e^{\prime}$ such that $e^{\prime}\equiv e$ for an expression $e$ in a canonical linear form is called linear. A substitution $\nu$ is linear with resets if for every $x\in X$ , $\nu(x)$ is either linear or $0$ (a reset). A linear substitution with resets is in a canonical form if all its linear expressions are in a canonical linear form. We remark that the only reason why we use linear substitutions with resets instead of affine substitutions (that is, substitutions whose expressions are sums of linear and constant expressions) is to simplify the presentation of our techniques. Clearly, by adding more registers one can transform an affine CRA into a linear CRA with resets.

A substitution $\nu$ is copyless if for all pairs $x,x^{\prime}\in X$ such that $x\neq x^{\prime}$ the expressions $\nu(x)$ and $\nu(x^{\prime})$ feature disjoint sets of variables. By $\text{{{${{\textrm{Expr}}}_{\mathrm{lin}}\kern-0.7pt$}}}\left(X\right)$ and $\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right)$ we denote the sets of linear expressions and copyless linear substitutions with resets, respectively.

Example 3 (Copyless linear substitutions with resets).

Consider the substitutions $\nu$ and $\nu^{\prime}$ :

\displaystyle\footnotesize\nu\coloneqq\begin{cases}x\leftarrow y+5\\ y\leftarrow\min\left\{x,z-2\right\}\\ z\leftarrow 5-5\end{cases}\hskip-8.53581pt\equiv\begin{cases}x\leftarrow\min% \left\{y+5\right\}\\ y\leftarrow\min\left\{x+0,z+(-2)\right\}\\ z\leftarrow 0\end{cases}\hskip-8.53581pt\,,\qquad\footnotesize\nu^{\prime}% \coloneqq\begin{cases}x\leftarrow\min\left\{x\right\}\\ y\leftarrow\min\left\{x,y\right\}\end{cases}

We have that $\nu\in\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(\left\{x,y,% z\right\}\right)$ because it is equivalent to a linear substitution with resets in a canonical form, and variables $x, y, z$ occur at most once in its expressions. In contrast, $\nu^{\prime}$ is linear, but not copyless, because $x$ occurs in both $\nu^{\prime}(x)$ and $\nu^{\prime}(y)$ .

2.2 Cost register automata

Definition 4 (CRA).

A copyless linear CRA with resets over $\mathbb{K}$ is a tuple

\mathcal{C}=(X,Q,\Sigma,\delta,q_{\mathrm{ini}},\text{{{out}}})

consisting of a finite set $X$ of registers, a finite alphabet $\Sigma$ , a finite set $Q$ of control states, an initial state $q_{\mathrm{ini}}\in Q$ , and two functions:

$\blacksquare$

a transition rule function $\delta\colon Q\times\Sigma\to Q\times\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}% \kern-0.7pt$}}}\left(X\right)$ ,
$\blacksquare$

an output function $\text{{{out}}}\colon Q\to\text{{{${{\textrm{Expr}}}_{\mathrm{lin}}\kern-0.7pt$% }}}\left(X\right)$ .

We also make the following assumptions that clearly preserve the property of being bounded or unbounded. We assume that all substitutions and expressions in $\mathcal{C}$ are in a canonical form. Furthermore, we assume that $+\infty$ never occurs as a constant in a substitution, since every such transition can be replaced with a transition leading to a new state, a self-loop incrementing the value of the corresponding register in this new state, and then a transition back.

In this paper, we consider only copyless linear CRAs with resets, hence for the rest of the paper we simply call them CRAs.

Definition 5 (Semantics of a CRA).

A CRA $\mathcal{C}=(X,Q,\Sigma,\delta,q_{\mathrm{ini}},\text{{{out}}})$ naturally induces a (possibly infinite) deterministic labelled transition system $\llbracket\mathcal{C}\rrbracket\coloneqq(\mathrm{Conf}_{\mathcal{C}},\Sigma,{% \Delta}_{\mathcal{C}},c_{\mathrm{ini}})$ , where $\mathrm{Conf}_{\mathcal{C}}\coloneqq Q\times\text{{{Val}}}\left(X\right)$ is the set of configurations, $c_{\mathrm{ini}}\coloneqq(q_{\mathrm{ini}},\mathrm{\mathbf{0}})$ is the initial configuration and ${\Delta}_{\mathcal{C}}\colon\mathrm{Conf}_{\mathcal{C}}\times\Sigma\to\mathrm{% Conf}_{\mathcal{C}}$ is a transition function defined as ${\Delta}_{\mathcal{C}}((q,\mu),\sigma)\coloneqq(q^{\prime},\text{{{eval}}}_{% \mu}\left(\nu\right))$ , where $(q^{\prime},\nu)=\delta(q,\sigma)$ . We extend $\Delta_{\mathcal{C}}$ to words as usually: for a configuration $t$ , a letter $\sigma\in\Sigma$ and a word $w\in\Sigma^{*}$ , $\Delta_{\mathcal{C}}(t,\sigma w)\coloneqq\Delta_{\mathcal{C}}(\Delta(t,\sigma)% ,w)$ and $\Delta_{\mathcal{C}}(t,\varepsilon)\coloneqq t$ . We further define the function $\mathcal{C}\colon\Sigma^{*}\to\mathbb{K}$ calculated by $\mathcal{C}$ as $\mathcal{C}(w)=\text{{{eval}}}_{\mu}\left(\text{{{out}}}\left(q\right)\right)$ , where $(q,\mu)=\Delta(c_{\mathrm{ini}},w)$ . Note that since we are only interested in the boundedness problem, the assumption that the initial value of each register is zero does not restrict the expressiveness of CRAs.

Example 6.

In Figure 1, we give an example of a CRA over the semiring $\mathbb{K}$ and alphabet $\Sigma=\left\{a,\#\right\}$ . It has two states $p$ and $q$ , where $p$ is the initial state, and two registers $x$ and $y$ . The output function for state $p$ (words ending with $a$ and the empty word) is $\min\{x,y\}$ and for state $q$ (words ending with $\#$ ) is $0$ . Both registers are initialised with value $0$ . If the input word ends with $\#$ or is empty, this CRA outputs $0$ . Call a sequence of consecutive $a$ ’s a block. A block is maximal if it is not contained in a longer block. If the input word ends with $a$ , the CRA outputs the length of the shortest maximal block. Register $x$ stores the number of $a$ ’s read in the current block, and $y$ stores the minimum length of maximal blocks read so far. This CRA is a copyless linear CRA with resets.

Figure 1: An example of a CRA over the semiring

\mathbb{K}

.

We say that a CRA $\mathcal{C}$ is bounded if there is $N\in\mathbb{N}$ such that $\mathcal{C}(w)<N$ for all $w\in\Sigma^{*}$ . We are now ready to state the main decision problem we are interested in.

Problem 7 (CRA boundedness).

Input: CRA $\mathcal{C}$ .

Question: Is $\mathcal{C}$ bounded?

3 Regular substitution languages

3.1 Substitution languages associated to CRAs

In the boundedness problem, the input alphabet of a CRA is redundant, since the formulation is existentially quantified for the word and the underlying finite automaton is deterministic. For this reason, in this paper we focus on sequences of substitutions that a CRA can perform.

A language of substitutions is an arbitrary subset of $\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right)^{*}$ . Every word $w\in\Sigma^{*}$ read by a CRA $\mathcal{C}$ induces a sequence of substitutions that $\mathcal{C}$ performs when reading $w$ . Fix a CRA $\mathcal{C}=(X,\Sigma,Q,q_{\mathrm{ini}},\delta,\text{{{out}}})$ . We define the language of substitutions $\text{{{$\mathcal{L}$}}}_{x}\left(\mathcal{C}\right)$ induced by it. Observe that the set of substitutions that occur in the transitions and output expressions of $\mathcal{C}$ is finite. We denote it by $\Gamma_{\mathcal{C},x}$ . The regular language $\text{{{$\mathcal{L}$}}}_{x}\left(\mathcal{C}\right)$ is then formally defined as the language of the following automaton $\text{{{NFA}}}_{x}\left(\mathcal{C}\right)$ . To simplify the presentation, we assume that the last substitution in the sequence corresponding to a word saves the output into a designated output register $x\in X$ .

Definition 8 ( $\text{{{NFA}}}_{x}\left(\mathcal{C}\right)$ ).

Given a CRA $\mathcal{C}=(X,Q,\Sigma,\delta,q_{\mathrm{ini}},\text{{{out}}})$ , define a nondeterministic finite automaton $\text{{{NFA}}}_{x}\left(\mathcal{C}\right)\coloneqq(Q^{\prime},\Gamma_{% \mathcal{C},x},\delta^{\prime},q_{\mathrm{ini}},\left\{q_{\mathrm{fin}}\right\})$ where $Q^{\prime}\coloneqq Q\cup\left\{q_{\mathrm{fin}}\right\}$ and the transition relation $\delta^{\prime}\subseteq Q^{\prime}\times\Gamma_{x,\mathcal{A}}\times Q^{\prime}$ contains transitions:

	$\displaystyle(q,\nu,q^{\prime})$	$\displaystyle\in\delta^{\prime}\qquad\text{for every $q,q^{\prime}\in Q$, and % $\nu,\sigma$ such that $\delta(q,\sigma)=(q^{\prime},\nu)$,}$
	$\displaystyle(q,\left\{x\leftarrow\text{{{out}}}\left(q\right)\right\},q_{% \mathrm{fin}})$	$\displaystyle\in\delta^{\prime}\qquad\text{for every $q\in Q$.}$

Fix an NFA $\mathcal{A}=(Q,S,\delta,q_{\mathrm{ini}},Q_{\mathrm{fin}})$ and a set of registers $X=\left\{x_{1},\dots,x_{d}\right\}$ for the rest of this subsection. An alternating sequence $\pi=q_{0}\xrightarrow[]{\nu_{1}}q_{1}\xrightarrow[]{\nu_{2}}q_{2}\to\cdots\to q% _{n-1}\xrightarrow[]{\nu_{n}}q_{n}$ of states from $Q$ and letters from $S$ is called a run in $\mathcal{A}$ labelled by the word $w=\nu_{1}\nu_{2}\cdots\nu_{n}$ . We write $q_{0}\xrightarrow[]{\pi,w}\mathrel{\mkern-14.0mu}\rightarrow q_{n}$ to denote the fact that $\pi$ is a run labelled by $w$ that begins in $q_{0}$ and ends in $q_{n}$ . For such a run and $\mu\in\text{{{Val}}}\left(X\right)$ , we define $\text{{{eval}}}_{\mu}\left(\pi\right)\coloneqq\text{{{eval}}}_{\mu}\left(w\right)$ . We identify words with compositions of the corresponding sequences of substitutions. The set of runs of $\mathcal{A}$ is denoted by $\text{{{Runs}}}\left(\mathcal{A}\right)$ . A run $\pi$ is accepting if $\smash{q_{\mathrm{ini}}\xrightarrow[]{\pi}\mathrel{\mkern-14.0mu}\rightarrow q% _{\mathrm{fin}}}$ . An NFA $\mathcal{A}$ accepts $w\in S^{*}$ whenever there exists an accepting run of $\mathcal{A}$ labelled by $w$ . The language of $\mathcal{A}$ , denoted $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ , is the set of words accepted by $\mathcal{A}$ .

To be able to refer to segments of runs, we combine the notation for single transitions $p\xrightarrow[]{\nu}q$ and runs $q\xrightarrow[]{\pi,w}\mathrel{\mkern-14.0mu}\rightarrow r$ . For example, we may consider a run $\pi=p\xrightarrow[]{\nu}q\xrightarrow[]{\pi^{\prime},w}\mathrel{\mkern-14.0mu}\rightarrow r$ labelled by a word $\nu\cdot w$ . When the labelling is not important, we write $q\xrightarrow[]{\pi}\mathrel{\mkern-14.0mu}\rightarrow r$ .

There is an obvious correspondence between runs in $\llbracket\mathcal{C}\rrbracket$ and in $\text{{{NFA}}}_{x}\left(\mathcal{C}\right)$ . In particular, for $k\in\mathbb{K}$ , there exists $w\in\Sigma^{*}$ such that $\mathcal{C}(w)=k$ if, and only if, there exists $u\in\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(u\right)(x)=k$ . This allows us to restate the boundedness problems in terms of languages of substitutions. We say that a regular language $L\subseteq\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right% )^{*}$ has bounded output in $x\in X$ if there exists $N\in\mathbb{N}$ such that for every $w\in L$ we have $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(s\right)(x)<N$ .

Problem 9 (Boundedness of regular $d$ -register substitution languages).

Input: NFA $\mathcal{A}$ over a finite set $S\subset\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right)$ , $\lvert X\rvert=d$ , output register $x\in X$ .

Question: Does $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ have bounded output in $x$ ?

Note that boundedness for CRAs (Problem 7) easily reduces to this problem in deterministic logarithmic space. Indeed, it suffices to compute $\text{{{NFA}}}\left(\mathcal{A}\right)$ for a given CRA with Definition˜8. This reformulation allows us to use a rich framework of regular languages, which streamlines the proofs presented in later sections.

Definition 10 (Elementary substitutions).

We say that a substitution $\nu\in\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right)$ is elementary if it has one of the following forms for some $x,y\in X$ , $c\in\mathbb{K}$ :

	$\displaystyle\left\{x\leftarrow x+c\right\}$	(additive sub.)	$\displaystyle\left\{x\leftarrow y,\;y\leftarrow x\right\}$		(transposition)
	$\displaystyle\left\{x\leftarrow\min\left\{x,y\right\},\;y\leftarrow 0\right\}$	(minimum sub.)	$\displaystyle\left\{x\leftarrow 0\right\}$		(reset sub.)

Let $\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)% \subseteq\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right)$ be the set of elementary substitutions, and let $T_{X}\cup R_{X}\cup A_{X}\cup M_{X}$ be its partition into sets of transpositions, and reset, additive, and minimum substitutions.

Lemma 11.

For every $\nu\in\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right)$ in a canonical form, there exists a word of substitutions $u\in\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)^{*}$ of length ${O(d^{2})}$ such that $u\equiv\nu$ .

Note that the statement of the above lemma is not true in the general setting of $\text{{{Sub}}}\left(X\right)$ , as its proof relies on copylessness. Note also that Lemma 11 implies the existence of a homomorphism $\text{{{to-elem}}}\colon\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}% }\left(X\right)^{*}\to\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}% \left(X\right)^{*}$ such that $\nu\equiv\text{{{to-elem}}}\left(\nu\right)$ for every $\nu\in\text{{{${{\textrm{Sub}}}_{\mathrm{clr}}\kern-0.7pt$}}}\left(X\right)$ . For a finite set $S\subset\text{{{Sub}}}\left(X\right)$ , we define $\text{{{maxc}}}\left(S\right)\coloneqq\max\left\{\text{{{maxc}}}\left(\nu% \right)\nonscript\>\middle|\allowbreak\nonscript\>\mathopen{}\nu\in S\right\}$ . The following two claims are not difficult to prove.

Claim 12 (Maximal constant grows linearly w.r.t. length).

Fix a finite $S\subset\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)$ . For every $w\in S^{*}$ , we have $\text{{{maxc}}}\left(w\right)\leq\lvert w\rvert\cdot\text{{{maxc}}}\left(S\right)$ .

Claim 13 (Elementary substitutions assumption).

We may assume w.l.o.g. that the alphabet $S$ of $\mathcal{A}$ consists only of elementary substitutions, i.e., $S\subset\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)$ .

3.2 The structure of witnesses with additive and reset substitutions only

In this subsection, we show how to simplify and decompose runs that do not contain any minimum substitutions or transpositions. We then use these results in the complexity upper bounds and to analyse runs with a more complex structure.

For the rest of this subsection, fix a set of registers $X=\left\{x_{1},\ldots,x_{d}\right\}$ , an output register $x\in X$ , and an NFA $\mathcal{A}$ over a finite alphabet $S\subset A_{X}\cup R_{X}\subset\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-% 0.7pt$}}}\left(X\right)$ of elementary additive and reset substitutions. Similarly to Claim 13, this covers a more general case where the alphabet of $\mathcal{A}$ consists of substitutions adding integer values to some registers and resetting other registers.

Let $w\in A_{X}^{*}$ be such that $w\equiv\left\{x_{1}\leftarrow x_{1}+c_{1},\dots,x_{d}\leftarrow x_{d}+c_{d}\right\}$ for some $c_{1},\ldots,c_{d}\in\mathbb{K}$ . We define $\text{{{eff}}}\left(w\right)\coloneqq(c_{1},\dots,c_{d})\in\mathbb{K}^{X}$ , and we call it the effect of $w$ . The integer conic hull $\text{{{Cone}}}_{\mathbb{N}}\left(V\right)$ of a set of vectors $V$ is the set of linear combinations of vectors from $V$ with nonnegative integer coefficients. The following theorem is a direct consequence of a classical result by Carathédory, see, e.g., [35].

Theorem 14 (Only $d$ vectors are sufficient to represent a positive point).

Let $V\subseteq\mathbb{Z}^{d}$ . If all components of a vector $\vec{b}$ are strictly positive and $\vec{b}\in\text{{{Cone}}}_{\mathbb{N}}\left(V\right)$ , then there exists $V^{\prime}\subseteq V$ with $\lvert V^{\prime}\rvert\leq d$ and a constant $\lambda>0$ such that $\lambda\vec{b}\in\text{{{Cone}}}_{\mathbb{N}}\left(V^{\prime}\right)$ .

We now state two important lemmas describing the shape of runs labelled by words over $A_{X}$ and $A_{X}\cup R_{X}$ , respectively.

Lemma 15 (Decomposition lemma for additive runs).

For every run $q\xrightarrow[]{\pi,w}\mathrel{\mkern-14.0mu}\rightarrow q^{\prime}$ of $\mathcal{A}$ such that $w\in A_{X}^{*}$ , there exist $n\in\mathbb{N}$ , words $w_{1},\dots,w_{n},,w^{\prime},z_{1},\dots,z_{n+1}\in A_{X}^{*}$ , and integers $a_{1},\dots,a_{n}\in\mathbb{N}$ such that

$\blacksquare$

for every word $z\in z_{1}w_{1}^{*}z_{2}\dots z_{n}w_{n}^{*}z_{n+1}$ , there exists a run $q\xrightarrow[]{z}\mathrel{\mkern-14.0mu}\rightarrow q^{\prime}$ ,
$\blacksquare$

$\text{{{eff}}}\left(w\right)=\text{{{eff}}}\left(w^{\prime}\right)+a_{1}\text{% {{eff}}}\left(w_{1}\right)+\dots+a_{n}\text{{{eff}}}\left(w_{n}\right)$ , and
$\blacksquare$

$\lvert w_{1}\rvert,\dots,\lvert w_{n}\rvert,\lvert w^{\prime}\rvert\leq\lvert Q\rvert$ and $\lvert z_{1}\dots z_{n+1}\rvert\leq\lvert Q\rvert^{2}$ .

Proof idea.

We iterate a process that eliminates all the simple cycles from $\pi$ . These simple cycles are labelled by some words $w_{1},\dots,w_{d}$ and the process returns a cycle-free run $\pi^{\prime}$ that is labelled by a word $w^{\prime}$ . We can describe the additive effect of the run $\pi$ as the effect of $w^{\prime}$ plus the effect of all the simple cycles that we eliminated. Finally, we argue there exists a short run from $q$ to $q^{\prime}$ that contains a vertex from each of these simple cycles. $\hfill\blacktriangleleft$

Proof.

Consider the following iterative process on $\pi$ . Initialise $\vec{b}=\mathrm{\mathbf{0}}\in\mathbb{Q}^{X}$ .

$\blacksquare$

Identify the first simple cycle $r\xrightarrow[]{\pi_{i},w_{i}}\mathrel{\mkern-14.0mu}\rightarrow r$ in $\pi$ and replace it by $r$ . By simple cycle we mean a run where only the first and last states are equal.
$\blacksquare$

Update the value of the vector $\vec{b}$ to $\vec{b}+\text{{{eff}}}\left(w_{i}\right)$ .

Let $q\xrightarrow[]{\pi^{\prime},w^{\prime}}\mathrel{\mkern-14.0mu}\rightarrow q^{\prime}$ be the resulting run. This process guarantees that $\pi^{\prime}$ is cycle-free and that $\text{{{eff}}}\left(w\right)=\text{{{eff}}}\left(w^{\prime}\right)+\vec{b}=% \text{{{eff}}}\left(w^{\prime}\right)+a_{1}\text{{{eff}}}\left(w_{1}\right)+% \dots+a_{n}\text{{{eff}}}\left(w_{n}\right)$ , where $a_{i}$ is the number of times we have eliminated a simple cycle with effect $w_{i}$ , for all $1\leq i\leq n$ .

Let $Q^{\prime}\subseteq Q$ be the set of states visited by $\pi$ . The shortest run that visits all states of $Q^{\prime}$ has length at most $\lvert Q\rvert^{2}$ . Since every word $w_{i}$ corresponds to a simple cycle eliminated by the process, it follows that there exists words $z_{1},\dots,z_{n+1}$ such that for every word $z\in z_{1}w_{1}^{*}z_{2}\dots z_{n}w_{n}^{*}z_{n+1}$ , there exists a run $q\xrightarrow[]{z}\mathrel{\mkern-14.0mu}\rightarrow q^{\prime}$ and $\lvert z_{1}\dots z_{n+1}\rvert\leq\lvert Q\rvert^{2}$ even if $n$ can be as large as $2^{\lvert Q\rvert}$ . $\hfill\blacktriangleleft$

Lemma 16 (Pumping lemma).

If $S\subseteq A_{X}\cup R_{X}$ , then there exists a word $w\in\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ with $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w\right)>2d\lvert Q\rvert C$ , where $C\coloneqq\text{{{maxc}}}\left(S\right)$ if and only if there exist words $\alpha_{1},\dots,\alpha_{d+1}$ , $\beta_{1},\dots,\beta_{d}\in A_{X}^{*}$ such that

$\blacksquare$

$\alpha_{1}\beta_{1}^{+}\alpha_{2}\dots\alpha_{d}\beta_{d}^{+}\alpha_{d+1}\eta_% {X}\subseteq\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ ,
$\blacksquare$

$\lvert\beta_{1}\rvert,\dots,\lvert\beta_{d}\rvert\leq\lvert Q\rvert$
$\blacksquare$

$|\alpha_{1}\dots\alpha_{d+1}|<(d+1)\lvert Q\rvert^{2}$ , and
$\blacksquare$

for each $N\in\mathbb{N}$ , there are $a_{1},\dots,a_{d}\in\mathbb{N}$ with $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\alpha_{1}\beta_{1}^{a_{1}}\alpha_{% 2}\dots\alpha_{d}\beta_{d}^{a_{d}}\alpha_{d+1}\eta_{X}\right)(x_{1})>N$ .

Proof idea.

Given a run in $\mathcal{A}$ of sufficiently large value, we can split it into different segments such that in each segment we know for every register if it is going to be reset in the future or not. Thus, for every register, we can determine if a segment of the run is relevant for determining its final value. Subsequently, we identify all cycles of this run and argue that since all the registers hold large values at the end of the run, the total !! effect of the relevant cycles (the ones after the last reset of the register) must be a large positive number for each register. This allows us to use Lemma 15 to conclude that we do not have too many such cycles and that we can pump them up in order to achieve unbounded register values. $\hfill\blacktriangleleft$

Proof.

The right to left implication of this lemma is immediate, so we focus on the left to right implication. Assume there exists a run $\pi=q_{\mathrm{ini}}\xrightarrow[]{w}q_{\mathrm{fin}}$ , for some $q_{\mathrm{fin}}\in Q_{\mathrm{fin}}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w\right)(x_{1})>2d\lvert Q\rvert C$ .

We can assume that the value of each register is reset at least once along $\pi$ , since we can add additional reset substitutions to the beginning of $w$ without changing the value of $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w\right)(x_{1})$ . For each $i$ , $1\leq i\leq d$ , the $\nu_{i}$ be the last reset substitution for register $x_{i}$ in $w$ . Without loss of generality, we can assume that in $w$ the registers are reset for the last time in the increasing order of their indices. Then $\pi$ can be represented as

\pi=q_{\mathrm{ini}}\xrightarrow[]{\pi_{1},w_{1}}\mathrel{\mkern-14.0mu}% \rightarrow q_{1}\xrightarrow[]{\nu_{1}}q_{1}^{\prime}\xrightarrow[]{\pi_{2},w% _{2}}\mathrel{\mkern-14.0mu}\rightarrow q_{2}\xrightarrow[]{\nu_{2}}\dots% \xrightarrow[]{\pi_{d},w_{d}}\mathrel{\mkern-14.0mu}\rightarrow q_{d}% \xrightarrow[]{\nu_{d}}q_{d}^{\prime}\xrightarrow[]{\pi_{d+1},w_{d+1}}\mathrel% {\mkern-14.0mu}\rightarrow q_{d+1}\xrightarrow[]{\eta_{X}}q_{\mathrm{fin}}\,.

Observe that for each $i$ , $1\leq i\leq d-1$ , we can replace in $w_{i}$ all reset substitutions of registers $x_{i+1},\ldots,x_{d}$ with the identity substitution without changing the value of $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w\right)(x_{1})$ . Thus, $w_{1},\ldots,w_{d+1}$ become words over additive substitutions only. Hence we now get that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{1}\nu_{1}\cdots w_{d+1}\right)=% \text{{{eff}}}\left(w_{1}\right)+\cdots+\text{{{eff}}}\left(w_{d+1}\right)$ . By applying Lemma 15 to each run $\pi_{1},\dots,\pi_{d+1}$ , we obtain that

	$\displaystyle\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{1}\nu_{1}\dots w_{d% +1}\right)={}$	$\displaystyle\hskip 22.76228pt\mathclap{\text{{{eff}}}\big{(}w_{1}^{\prime}% \big{)}}\hskip 22.76228pt+\hskip 39.83368pt\mathclap{a_{1}^{(1)}\text{{{eff}}}% \left(w_{1}^{(1)}\right)}\hskip 39.83368pt\mathrlap{{}+\cdots+{}}\hskip 76.822% 34pt\mathclap{a_{n_{1}}^{(1)}\text{{{eff}}}\left(w_{n_{1}}^{(1)}\right)}$
		$\displaystyle\hskip 22.76228pt\mathclap{\vdots}\hskip 22.76228pt\hskip 39.8336% 8pt\mathclap{\vdots}\hskip 39.83368pt\hskip 76.82234pt\mathclap{\vdots}$
		$\displaystyle\hskip 22.76228pt\mathclap{\text{{{eff}}}\big{(}w_{d+1}^{\prime}% \big{)}}\hskip 22.76228pt+\hskip 39.83368pt\mathclap{a_{1}^{(d+1)}\text{{{eff}% }}\left(w_{1}^{(d+1)}\right)}\hskip 39.83368pt\mathrlap{{}+\cdots+{}}\hskip 76% .82234pt\mathclap{a_{n_{d+1}}^{(d+1)}\text{{{eff}}}\left(w_{n_{d+1}}^{(d+1)}% \right)}$

where $w_{1}^{(1)},\dots,w_{n_{d+1}}^{(d+1)},w_{1}^{\prime},\dots,w_{d+1}^{\prime}$ are all words of length smaller than $\lvert Q\rvert$ . Since

\displaystyle\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{1}\nu_{1}\cdots w_{% d+1}\right)(x)>2d\lvert Q\rvert C

and

\displaystyle\text{{{eff}}}\left(w_{1}^{\prime}\cdots w_{d+1}^{\prime}\right)(% x)\leq(d+1)\lvert Q\rvert C

for every $x\in X$ , there must exists a vector $\vec{b}\in\mathbb{N}_{+}^{X}$ such that $\vec{b}\in\text{{{Cone}}}_{\mathbb{N}}\left(\left\{w_{1}^{(1)},\dots,w_{d+1}^{% (d+1)}\right\}\right)$ . By Theorem 14, there exists a subset $\left\{\beta_{1},\dots,\beta_{d}\right\}\subseteq\left\{w_{1}^{(1)},\dots,w_{d% +1}^{(d+1)}\right\}$ such that $\vec{b}^{\prime}\in\text{{{Cone}}}_{\mathbb{N}}\left(\left\{\beta_{1},\dots,% \beta_{d}\right\}\right)$ and $\vec{b}^{\prime}>\mathrm{\mathbf{0}}$ (pointwise).

It remains to show that there exist words $\alpha_{1},\dots,\alpha_{d+1}$ such that $\lvert\alpha_{1}\dots\alpha_{d+1}\rvert<(d+1)\lvert Q\rvert^{2}$ and $\alpha_{1}\beta_{1}^{+}\alpha_{2}\dots\alpha_{d}\beta_{d}^{+}\alpha_{d+1}\eta_% {X}\in\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ . Indeed, consider a run $\pi_{i}$ for some $1\leq i\leq d+1$ . Either $\pi_{i}$ contains no cycles from $\left\{\beta_{1},\dots,\beta_{d}\right\}$ , in which case there exists a word $w_{i}^{\prime}$ of length at most $\lvert Q\rvert$ corresponding to the run $\pi_{i}^{\prime}$ , or it does contain some cycles $\left\{\beta_{j},\dots,\beta_{j+h}\right\}$ from $\left\{\beta_{1},\dots,\beta_{d}\right\}$ . In the latter case, we can use Lemma 15 to argue that there exist words $z_{j}^{\prime},\dots,z_{j+h+1}^{\prime}$ such that for every word $z\in z_{j}^{\prime}\beta_{j}^{*}z_{j+1}^{\prime}\dots z_{j+h}^{\prime}\beta_{j% +h}^{*}z_{j+h+1}^{\prime}$ , there exists a run $q_{i-1}^{\prime}\xrightarrow[]{z}\mathrel{\mkern-14.0mu}\rightarrow q_{i}$ . In both cases, either $\lvert w^{\prime}\rvert\leq\lvert Q\rvert$ or $\lvert z_{j}^{\prime}\dots z_{j+h+1}^{\prime}\rvert\leq\lvert Q\rvert^{2}$ . Thus, we can obtain the required words $\alpha_{1},\dots,\alpha_{d+1}$ by possibly concatenating the $w_{i}^{\prime}$ and $z_{i}^{\prime}$ words that we identified. $\hfill\blacktriangleleft$

4 CRAs with two registers

In this section, we prove the following result.

Theorem 17.

The boundedness problem for CRAs with two registers is NL-complete if the numbers in the substitutions are presented in unary, and in coNP if they are in binary.

By the results of the previous section, this theorem is equivalent to the following statement.

Proposition 18.

Boundedness of regular $2$ -register substitution languages is NL-complete if the numbers in the substitutions are presented in unary, and in coNP if they are in binary.

The remainder of the section is devoted to proving Proposition 18. For the rest of this section, fix the set of registers $X\coloneqq\left\{x,y\right\}$ and the output register $x$ . Let us also fix for the rest of the section an input NFA $\mathcal{A}=(Q,S,\delta,q_{\mathrm{ini}},Q_{\mathrm{fin}})$ such that $S\subset T_{X}\cup A_{X}\cup M_{X}\cup R_{X}\subset\text{{{${{\textrm{Sub}}}_{% \mathrm{elem}}\kern-0.7pt$}}}\left(X\right)$ (which we can assume by Claim 13). We begin by providing a series of simplifying assumptions for the automaton $\mathcal{A}$ in the input.

4.1 Simplifying assumptions

In this subsection, we introduce a normal form that significantly simplifies our arguments.

Definition 19 (Graphical notation for $\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)$ ).

We depict elementary substitutions in $\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)$ as shown in Figure 2; details of the notation are discussed in its caption.

$\begin{cases}x\leftarrow y\\ y\leftarrow x\end{cases}\hskip-8.53581pt\in T_{X}$

(a) Transposition.

$\begin{cases}x\leftarrow 0\\ y\leftarrow y\end{cases}\hskip-8.53581pt\in R_{X}$

(b) Reset substitution.

$\begin{cases}x\leftarrow x+c\\ y\leftarrow y\end{cases}\hskip-8.53581pt\in A_{X}$

(c) Additive substitution.

$\begin{cases}x\leftarrow\min\left\{x,y\right\}\\ y\leftarrow 0\end{cases}\hskip-8.53581pt\in M_{X}$

(d) Minimum substitution.

Figure 2: Pictorial representation of elementary substitutions in

\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(\left\{x,y\right% \}\right)

. Register

x

is always drawn above

y

. A black dot stands for adding a constant – our graphical notation disregards the particular values of constants in the substitutions. A branching depicts the minimum operation. For the operations on

y

, the diagrams are symmetric. The effect of gluing several drawings together horizontally naturally corresponds to composition of depicted substitutions.

For a word $w=\nu_{1}\nu_{2}\cdots\nu_{n}\in\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern% -0.7pt$}}}\left(X\right)^{*}$ , we define the output derivation tree $\text{{{out-tree}}}\left(w\right)$ as the derivation tree of the expression $w(x)$ . This tree can have three kinds of leaves: constants $0$ originating from reset or minimum substitutions, arbitrary constants from $\mathbb{K}$ coming from additive substitutions, and variables occurring in $\nu_{1}(x)$ or $\nu_{1}(y)$ of the first substitution $\nu_{1}$ . We say that a path from a leaf to the root in $\text{{{out-tree}}}\left(w\right)$ is leading if its starting leaf comes from a substitution $\nu_{i}$ with the smallest $i$ among all leaves that have a path to the root. A path is called $x$ -aligned if all its vertices originate from expressions $(\nu_{i}(x))_{1\leq i\leq n}$ . A word $w$ is called $x$ -aligned if the leading path of $\text{{{out-tree}}}\left(w\right)$ is $x$ -aligned.

Example 20 (Depiction of $\text{{{out-tree}}}\left(w\right)$ ).

For $w\in\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)^{*}$ , $\text{{{out-tree}}}\left(w\right)$ corresponds to the tree rooted at the rightmost position corresponding to $x$ in the pictorial representation. Consider

	$\displaystyle w\coloneqq$	$\displaystyle\scriptsize\begin{cases}x\leftarrow{\text{\smash{\lx@texthl@color% {$x$}}}}\\ y\leftarrow{y+3}\end{cases}\begin{cases}x\leftarrow{\text{\smash{% \lx@texthl@color{$x$}}}}\\ y\leftarrow{0}\end{cases}\begin{cases}x\leftarrow{\text{\smash{% \lx@texthl@color{$x+2$}}}}\\ y\leftarrow{y}\end{cases}\begin{cases}x\leftarrow{\text{\smash{% \lx@texthl@color{$x$}}}}\\ y\leftarrow{y+2}\end{cases}\begin{cases}x\leftarrow{\text{\smash{% \lx@texthl@color{$\min\left\{x,y\right\}$}}}}\\ y\leftarrow{0}\end{cases}\begin{cases}x\leftarrow{y}\\ y\leftarrow{\text{\smash{\lx@texthl@color{$x$}}}}\end{cases}\begin{cases}x% \leftarrow{x+3}\\ y\leftarrow{\text{\smash{\lx@texthl@color{$y$}}}}\end{cases}$
		$\displaystyle\qquad\qquad\scriptsize\begin{cases}x\leftarrow{x+3}\\ y\leftarrow{\text{\smash{\lx@texthl@color{$y$}}}}\end{cases}\begin{cases}x% \leftarrow{\min\left\{x,\text{\smash{\lx@texthl@color{$y$}}}\right\}}\\ y\leftarrow{0}\end{cases}\begin{cases}x\leftarrow{\text{\smash{% \lx@texthl@color{$x$}}}}\\ y\leftarrow{y+5}\end{cases}\begin{cases}x\leftarrow{\text{\smash{% \lx@texthl@color{$x$}}}}\\ y\leftarrow{0}\end{cases}\begin{cases}x\leftarrow{\text{\smash{% \lx@texthl@color{$\min\left\{x,y\right\}$}}}}\\ y\leftarrow{0}\end{cases}$

The depiction of $w$ , in line with Definition˜19, is as follows:

The $\text{{{out-tree}}}\left(w\right)$ corresponds to the subgraph drawn in black. The leading path $\pi$ of $\text{{{out-tree}}}\left(w\right)$ is marked with a blue outline. Expressions in $w$ corresponding to vertices of $\pi$ are typeset on blue background. As not all of them come from $x\leftarrow e$ mappings, path $\pi$ is not $x$ -aligned. An $x$ -aligned word $w^{\prime}$ such that $w(x)\equiv w^{\prime}(x)$ has the following shape:

Lemma 21 (Leading branch $x$ -aligned assumption).

We can assume that each $w\in\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ is $x$ -aligned.

Therefore, in the remainder of this section we assume that each $w\in\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ is $x$ -aligned. This means that only parts (b), (c) and (d) from Figure 2 (and not their symmetric $y$ -counterparts) can be segments of runs.

4.2 Unboundedness witnesses

In this subsection, we define the shape of witnesses that prove unboundedness of CRAs. Next subsection shows that if a CRA is unbounded, it must contain such a witness. For the rest of this section, fix two substitutions

\eta=\left\{x\leftarrow\min\left\{x,y\right\},\;y\leftarrow 0\right\}\mbox{ % and }\rho=\left\{x\leftarrow x,\;y\leftarrow 0\right\},

which will be referred to throughout the whole section. Let $N\coloneqq\lvert Q\rvert$ and $C\coloneqq\text{{{maxc}}}\left(S\right)$ . We introduce two new notations for special types of runs of $\mathcal{A}$ :

and

used to signify that $w_{1}\in A_{X}^{*}$ (i.e., has additive substitutions only), and $w_{2}\in\left(A_{X}\cup\left\{\rho\right\}\right)^{*}$ .

Definition 22 (Unboundedness witness).

A run $\pi$ in $\mathcal{A}$ is called a trivial unboundedness witness if it has the form

such that $\lvert\pi\rvert\leq 3N$ , $\text{{{eff}}}\left(\theta\right)(x)>0$ and $q_{\mathrm{fin}}\in Q_{\mathrm{fin}}$ .

A run $\pi$ in $\mathcal{A}$ is called a nontrivial unboundedness witness if it has the form

\displaystyle\pi=q_{\mathrm{ini}}\xrightarrow[]{\pi_{a}}\mathrel{\mkern-14.0mu% }\rightarrow q_{a}\xrightarrow[]{\pi_{b}}\mathrel{\mkern-14.0mu}\rightarrow q_% {b}\xrightarrow[]{\pi_{c}}\mathrel{\mkern-14.0mu}\rightarrow q_{c}

such that $\lvert\pi_{a}\rvert\leq N$ , $\lvert\pi_{b}\rvert,\lvert\pi_{c}\rvert\leq 3N^{2}$ , run $\mathit{\pi_{b}}$ is pumpable, and $\pi_{c}$ is sustainable, where pumpable and sustainable runs are defined below.

A trivial or nontrivial unboundedness witness is called just an unboundedness witness.

Intuitively, $\pi_{a}$ from this definition is used to reach a gadget enabling pumping, $\pi_{b}$ witnesses that we can pump up the value of $x$ to an arbitrarily large number and then end up in $q_{b}$ , and $\pi_{c}$ certifies that we can maintain a large value of $x$ to be output in $q_{c}\in Q_{\mathrm{fin}}$ .

Definition 23 (Pumpable run).

A run $\pi_{b}$ is called pumpable if it has one of the four forms:

$\blacksquare$

Type A.1 (a cycle with a positive effect on $x$ , then a reset of $y$ )

$\left(\raisebox{2.0pt}{\includegraphics{dagpub-standalone-combined-2025-04-10-% 18-59-45-page-12.pdf2svg.svg} }\ \right)$

such that $\theta$ is a cycle with $\text{{{eff}}}\left(\theta\right)(x)>0$ and $\alpha$ is a run with no $\eta$ substitutions.
$\blacksquare$

Type A.2 (a cycle with a positive effect on both $x$ and $y$ , then a minimum substitution)

$\left(\raisebox{2.0pt}{\includegraphics{dagpub-standalone-combined-2025-04-10-% 18-59-45-page-14.pdf2svg.svg} }\ \right)$

such that $\theta$ is a cycle with no $\eta$ and no $\rho$ substitutions and with $\text{{{eff}}}\left(\theta\right)\in\mathbb{N}_{+}^{2}$ , and $\alpha$ is a run with no $\eta$ and no $\rho$ substitutions.
$\blacksquare$

Type A.3 (two cycles combining for a positive effect on both $x$ and $y$ , then a minimum)

$\left(\raisebox{2.0pt}{\includegraphics{dagpub-standalone-combined-2025-04-10-% 18-59-45-page-16.pdf2svg.svg} }\ \right)$

such that $\theta_{1},\theta_{2}$ are cycles with no $\eta$ and no $\rho$ substitutions and with $a_{1}\text{{{eff}}}\left(\theta_{1}\right)+a_{2}\text{{{eff}}}\left(\theta_{2}% \right)\in\mathbb{N}_{+}^{2}$ , for some $a_{1},a_{2}\in\mathbb{N}$ . Furthermore, $\alpha_{1},\alpha_{2}$ are runs with no $\eta$ and no $\rho$ substitutions.
$\blacksquare$

Type B (a cycle with a positive effect on $x$ together with cycles supporting its value)

$\displaystyle\pi=p_{1}\xrightarrow[]{\pi_{1}}\mathrel{\mkern-14.0mu}% \rightarrow p_{2}\xrightarrow[]{\pi_{2}}\mathrel{\mkern-14.0mu}\rightarrow p_{% 3}\xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow\cdots\xrightarrow[]{}% \mathrel{\mkern-14.0mu}\rightarrow p_{n-1}\xrightarrow[]{\pi_{n-1}}\mathrel{% \mkern-14.0mu}\rightarrow p_{n}\xrightarrow[]{\pi_{n}}\mathrel{\mkern-14.0mu}% \rightarrow p_{1}$

for some $n\in\mathbb{N}$ , where $p_{1}=q_{a}=q_{b}$ , and for every $i$ , $1\leq i\leq n$ :

$\left(\raisebox{2.0pt}{\includegraphics{dagpub-standalone-combined-2025-04-10-% 18-59-45-page-18.pdf2svg.svg} }\right)$

such that $\alpha_{i}$ is a run with no $\eta$ substitutions, $\theta_{i}$ is a cycle with no $\eta$ and no $\rho$ substitutions with $\text{{{eff}}}\left(\theta_{i}\right)\in\mathbb{N}\times\mathbb{N}_{+}$ and $\beta_{i}$ is a run with no $\eta$ substitutions. Furthermore, we require $\text{{{eff}}}\left(\alpha_{1}\theta_{1}\beta_{1}\alpha_{2}\theta_{2}\beta_{2}% \cdots\alpha_{n}\theta_{n}\beta_{n}\right)(x)>0$ .

Definition 24 (Sustainable run).

A run $\pi_{c}$ is called sustainable if it is labelled by $w_{c}\in\left(A_{X}\cup\left\{\rho,\eta\right\}\right)^{*}$ and has the following form:

for $n\in\mathbb{N}$ , runs $\alpha_{i},\beta_{i}$ of the form as depicted in the picture, and cycles $\theta_{i}$ such that $\text{{{eff}}}\left(\theta_{i}\right)\in\mathbb{Z}\times\mathbb{N}_{+}$ for every $i$ , $1\leq i\leq n$ .

Proposition 25.

Given $\mathcal{A}$ , deciding if there exists a run in it which is an unboundedness witness is in NL if the numbers in the substitutions are presented in unary, and in NP if they are in binary.

Proof.

Intuitively, using nondeterminism, we can guess a nontrivial witness $\pi=\pi_{a}\pi_{b}\pi_{c}$ as in Definition 22 and verify that it has all the required properties. The case of a trivial witness is handled in a similar way and is thus omitted.

Indeed, starting in $q_{\mathrm{ini}}$ , we guess one transition at a time until we verify the existence of a witness or exceed the bound $N+4N^{2}$ on its length. During the traversal, we guess the positions of states $q_{a},q_{b},q_{c}$ at appropriate distances from $q_{\mathrm{ini}}$ . This splits the search into three phases corresponding to $\pi_{a},\pi_{b}$ and $\pi_{c}$ . We need to verify that $\pi_{b}$ is of one of four types of pumpable runs (cf. Definition 23). At any point in time, if the definition of a pumpable run requires it, we can guess that the current state $r$ marks the start of the occurrence of a simple cycle $\theta$ . In this case, we store $r$ , follow only labels from $A_{X}\cup\left\{\rho\right\}$ and compute the effect of the run until $r$ occurs again. This can easily be done in NL or NP depending on the representation of the numbers in the substitutions. $\hfill\blacktriangleleft$

In order to complete the proof of Proposition 18, we need to show that the existence of an unboundedness witness is equivalent to the fact that $\mathcal{A}$ is not bounded. We show it by two implications stated below. We start with proving Lemma 26, and Lemma 29 is proved in the next subsection.

Lemma 26.

If there exists an unboundedness witness then $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ is not bounded.

Proof.

The proof is straightforward in case of a trivial unboundedness witness. Fix a nontrivial unboundedness witness $\pi$ as in Definition 22:

\displaystyle\pi=q_{\mathrm{ini}}\xrightarrow[]{\pi_{a}}\mathrel{\mkern-14.0mu% }\rightarrow q_{a}\xrightarrow[]{\pi_{b}}\mathrel{\mkern-14.0mu}\rightarrow q_% {b}\xrightarrow[]{\pi_{c}}\mathrel{\mkern-14.0mu}\rightarrow q_{c}\,.

Fix an arbitrary number $N\in\mathbb{N}$ . We construct a run $\pi^{\prime}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi^{\prime}\right)(x)\geq N$ . We first prove that

Claim 27.

For every $M\in\mathbb{N}$ there is a run $\pi^{\prime}_{b}$ of $\mathcal{A}$ from $q_{a}$ to $q_{b}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{a}\pi_{b}^{\prime}\right)=(M^{% \prime},0)$ for some $M^{\prime}>M$ .

First, by Claim 12 we have that $-CN\leq\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{a}\right)(x)\leq CN$ . The claim is immediate if $\pi_{b}$ contains a certificate of type A.1, A.2, or A.3. Indeed, we simply repeat the cycles that occur there a sufficient number of times. If $\pi_{b}$ contains a certificate of type B, then $\pi_{b}=p_{1}\xrightarrow[]{\pi_{1}}\mathrel{\mkern-14.0mu}\rightarrow p_{2}% \xrightarrow[]{\pi_{2}}\mathrel{\mkern-14.0mu}\rightarrow p_{3}\xrightarrow[]{% }\mathrel{\mkern-14.0mu}\rightarrow\cdots\xrightarrow[]{}\mathrel{\mkern-14.0% mu}\rightarrow p_{n-1}\xrightarrow[]{\pi_{n-1}}\mathrel{\mkern-14.0mu}% \rightarrow p_{n}\xrightarrow[]{\pi_{n}}\mathrel{\mkern-14.0mu}\rightarrow p_{1}$ is a cycle such that the overall effect on $x$ is positive. Since every sub-path $\pi_{1},\dots,\pi_{n}$ contains a cycle with a positive effect on $y$ and a non-negative effect on $x$ , there is a path $\pi_{b}^{\prime\prime}$ that repeats each such cycle $M+CN$ times. Note that $\pi_{b}^{\prime\prime}$ is now a cycle with positive effect on $x$ for any value of $x$ smaller than $M+CN$ . Thus, we can take $\pi_{b}^{\prime}$ to be the cycle $\pi_{b}^{\prime\prime}$ taken $M+CN$ times.

This finishes the proof of the claim. Now, it suffices to show the following:

Claim 28.

For every $M\in\mathbb{N}$ there exists a run $\pi^{\prime}_{c}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{a}\pi_{b}^{\prime}\pi_{c}^{% \prime}\right)(x)\geq M$ .

We prove this claim by induction on the number of occurrences of $\eta$ in $\pi_{c}$ . Assume that $\pi_{c}$ does not contain any occurrences of $\eta$ . By Claim 27, there exists a path $\pi_{b}^{\prime}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{a}\pi_{b}^{\prime}\right)(x)% \geq M+CN$ . Thus, $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{a}\pi_{b}^{\prime}\pi_{c}% \right)(x)\geq M$ by Claim 12, since the length of $\pi_{c}$ is bounded.

Assume now that there is at least one occurrence of $\eta$ in $\pi_{c}$ . Then $\pi_{c}$ can be represented as follows:

\pi_{c}=q_{b}\xrightarrow[]{\rho_{1},\alpha_{1}}\mathrel{\mkern-14.0mu}% \rightarrow q_{1}\xrightarrow[]{\rho_{2},\alpha_{2}}\mathrel{\mkern-14.0mu}% \rightarrow q_{2}\xrightarrow[]{\rho_{3},\alpha_{3}}\mathrel{\mkern-14.0mu}% \rightarrow\cdots\xrightarrow[]{\rho_{r},\alpha_{r}}\mathrel{\mkern-14.0mu}% \rightarrow q_{\mathrm{fin}}\,,

where the cutting points are states reached after reading $\eta$ . Assume that there is a run $q_{\mathrm{ini}}\xrightarrow[]{\pi_{i-1},w_{i-1}}\mathrel{\mkern-14.0mu}% \rightarrow q_{i-1}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{i-1}\right)(x)\geq M^{\prime}$ , for every $M^{\prime}\in\mathbb{N}$ . Then we can use the cycle with positive effect on $y$ inside $\rho_{i}$ in order to conclude that there exists a run $q_{\mathrm{ini}}\xrightarrow[]{\pi_{i},w_{i}}\mathrel{\mkern-14.0mu}% \rightarrow q_{i}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{i}\right)\geq M^{\prime}$ , for every $M^{\prime}\in\mathbb{N}$ . This concludes the proof. $\hfill\blacktriangleleft$

Lemma 29.

If $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ is not bounded, there exists an unboundedness witness.

4.3 Unboundedness implies the existence of a witness

Proof of Lemma 29..

Assume that $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ is not bounded. Let $M\coloneqq 15C^{2}N^{3}$ and $W\coloneqq 12CN^{2}$ . Let $\pi$ be the shortest accepting run of $\mathcal{A}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi\right)(x)>M+W$ , and let $w$ be the word labelling $\pi$ . Since $\pi$ is $x$ -aligned, it can be split into two parts

\displaystyle\pi=q_{\mathrm{ini}}\xrightarrow[]{\pi_{\mathrm{pre}}}\mathrel{% \mkern-14.0mu}\rightarrow q_{0}\xrightarrow[]{\pi_{\mathrm{suf}}}\mathrel{% \mkern-14.0mu}\rightarrow q_{\mathrm{fin}}

for some $q_{0}\in Q$ and $q_{\mathrm{fin}}\in Q_{\mathrm{fin}}$ , such that $\pi_{\mathrm{suf}}$ is the shortest suffix of $\pi$ satisfying $\text{{{out-tree}}}\left(\pi\right)=\text{{{out-tree}}}\left(\pi_{\mathrm{suf}% }\right)$ . Note that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{\mathrm{pref}}\right)(x)=0$ , and $\pi_{\mathrm{suf}}$ features no substitution $\nu$ that resets $x$ (i.e., for which $\nu(x)=0$ ). Recall that we defined

\eta=\left\{x\leftarrow\min\left\{x,y\right\},\;y\leftarrow 0\right\}\text{ % and }\rho=\left\{x\leftarrow x,\;y\leftarrow 0\right\}.

Since $\pi$ is $x$ -aligned, we have that $w_{\mathrm{suf}}\in\left(A_{X}\cup\left\{\eta,\rho\right\}\right)^{*}$ , where $w_{\mathrm{suf}}$ is the word labelling $\pi_{\mathrm{suf}}$ . Let $n\in\mathbb{N}$ be the number of substitutions $\eta$ in $w$ . Split the run $\pi_{\mathrm{suf}}$ into segments (some possibly empty)

\displaystyle q_{0}\xrightarrow[]{\pi_{1},w_{1}}\mathrel{\mkern-14.0mu}% \rightarrow q_{1}\xrightarrow[]{\pi_{2},w_{2}}\mathrel{\mkern-14.0mu}% \rightarrow q_{2}\xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow\cdots% \xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow q_{n}\xrightarrow[]{\pi_{n+% 1},w_{n+1}}\mathrel{\mkern-14.0mu}\rightarrow q_{n+1}

such that $q_{1},\ldots,q_{n}$ are all the states reached directly after reading $\eta$ each time. Define $v_{i}\coloneqq\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{\mathrm{pref}}% \pi_{1}\cdots\pi_{i}\right)(x)$ for $0\leq i\leq n+1$ . Observe that $v_{0}=0$ and $v_{n+1}\geq M+W$ .

Example 30.

Consider a run $\pi$ partitioned into segments as defined above:

Let us overlook the slight inaccuracy that a run reaching a large value would have many more additive transitions (cf. Claim 12). The $\text{{{out-tree}}}\left(w\right)$ is drawn in black, other (irrelevant) lines are drawn in light grey. Run $\pi_{\mathrm{suf}}$ is the shortest one that contains all black lines. There are $n=4$ occurrences of $\eta$ in $w_{\mathrm{suf}}$ , thus $\pi_{\mathrm{suf}}$ is split into $5$ parts, and runs $\pi_{1},\ldots,\pi_{4}$ end with a transition labelled by $\eta$ .

We first show that unboundedness guarantees the existence of a sustainable part $\pi_{c}$ of a witness. Define $m\coloneqq\max\left\{i\nonscript\>\middle|\allowbreak\nonscript\>\mathopen{}v_% {i}<M\right\}$ .

Claim 31.

For every $i>m$ and every transition $s\xrightarrow[]{\nu}t$ in $\mathcal{A}$ such that $t$ is a state visited by $\pi_{i}$ and $\nu(y)=0$ , there exists a sustainable run $\pi_{c}$ from $t$ to $q_{\mathrm{fin}}$ of length at most $3N^{2}$ .

We prove the claim by downward induction on $i$ , the index of the segment $\pi_{i}$ incident with the state $t$ of $\nu$ . Base case ( $i=n+1$ ) is trivial, as $w_{n+1}\in A_{X}^{*}$ . Assume our claim holds for $i+1$ . Fix a transition $s\xrightarrow[]{\nu}t$ such that $t$ is a state visited by $\pi_{i}$ , and $\nu(y)=0$ . Similarly to the case of a trivial boundedness witness, a steep increase on $y$ implies existence of a run $\pi_{c}^{\prime}=t\xrightarrow[]{\alpha}\mathrel{\mkern-14.0mu}\rightarrow r% \xrightarrow[]{\theta,w_{\theta}}\mathrel{\mkern-14.0mu}\rightarrow r% \xrightarrow[]{\beta,w_{\beta}}\mathrel{\mkern-14.0mu}\rightarrow s% \xrightarrow[]{\eta}q_{i}$ such that $w_{\theta},w_{\beta}\in A_{X}^{*}$ , $\alpha,\beta$ are simple paths and $\theta$ a simple cycle, and that $\text{{{eff}}}\left(\theta\right)(y)>0$ . Finally, by applying the inductive hypothesis to $s\xrightarrow[]{\eta}q_{i}$ , we get a pumpable $\pi^{\prime\prime}_{c}$ from $q_{i}$ to $q_{\mathrm{fin}}$ ; we have thus constructed a sustainable run $\pi_{c}^{\prime}\pi_{c}^{\prime\prime}$ , as required.

It remains to show how to find $\pi_{b}$ , the pumpable part of the run. We consider two cases.

Case 1: $v_{i+1}-v_{i}>4CN$ for some $i\in\mathbb{N}\cap[m,n]$ .

(aim: pumpable run of type A) Fix such $i\in\mathbb{N}$ . Let $\mathcal{A}^{\prime}=(S,Q\cup{\{q_{i+1}^{\prime}\}},q_{i},{\{q_{i+1}^{\prime}% \}},\delta^{\prime})$ , where $\delta^{\prime}$ is constructed from $\delta$ by removing transitions with minimum substitutions, and adding $q\xrightarrow[]{\eta}q_{i+1}^{\prime}$ whenever $q\xrightarrow[]{\eta}q_{i+1}$ for some $q\in Q$ . Note that $w_{i}\in\text{{{$\mathcal{L}$}}}\left(\mathcal{A}^{\prime}\right)$ and that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{i}\right)(x)>4CN$ , thus automaton $\mathcal{A}^{\prime}$ satisfies the premises of Lemma 16. Using this lemma, we obtain a short pumpable run $\pi^{\prime}_{b}$ of type A of $\mathcal{A}^{\prime}$ – cases A.1, A.2 and A.3 were designed to match all possible loop arrangements. It naturally induces $\pi_{b}$ in $\mathcal{A}$ from $q_{i}$ to $q_{i+1}$ of the same properties. Since $q_{i}$ is reachable from $q_{\mathrm{ini}}$ , there exists a short run $\pi_{a}$ between them. Finally, by Claim 31, we obtain a sustainable part $\pi_{c}$ of the witness, which completes the analysis of this case.

Case 2: $v_{i+1}-v_{i}\leq 4CN$ for all $i\in\mathbb{N}\cap[m,n]$ .

(aim: witness exists or contradiction) This case proves to be more difficult, as it involves a more complicated type B pumpable run. The proof is by contradiction. Here, since $v_{n+1}-v_{m}>(M+W)-M=12CN^{2}$ and each $v_{i+1}$ provides an increase of at most $4CN$ compared to the previous value $v_{i}$ , any maximal increasing subsequence of $(v_{i})_{m\leq i\leq n}$ must have at least $\frac{12CN^{2}}{4CN}=3N$ elements. Therefore, there exist $k,\ell\in\mathbb{N}$ such that

m\leq k<\ell\leq n,\quad v_{k}<v_{\ell},\quad M<v_{i}<M+W\quad\mbox{for}\quad k% \leq i\leq\ell,\quad\mbox{and }\quad q_{k}=q_{\ell}

thus $\pi_{(k\ell]}\coloneqq\pi_{k+1}\cdots\pi_{l}$ is a cycle. For each $i$ , $k\leq i\leq l$ , define $c_{i}\in\mathbb{K}$ to be the effect on $x$ of the run $\pi_{i}$ without its last transition labelled with $\eta$ . We have $v_{i+1}\leq v_{i}+c_{i}$ , and therefore $\sum_{i=k}^{\ell-1}c_{i}>v_{\ell}-v_{k}>0$ . Assume that $\mathcal{A}$ has no pumpable run of type B from $q_{k}$ to $q_{\ell}$ (otherwise we obtain a witness easily). Therefore, there exists $i\in\mathbb{N}\cap[k,l]$ such that $\pi_{i}$ decomposes into

\displaystyle\pi_{i}

\displaystyle\coloneqq q_{i-1}\xrightarrow[]{\alpha,u}\mathrel{\mkern-14.0mu}% \rightarrow r_{1}\xrightarrow[]{\beta,v}\mathrel{\mkern-14.0mu}\rightarrow r_{% 2}\xrightarrow[]{\eta}q_{i},

where $\beta$ is the run of maximal length labelled by some $v\in A_{X}^{*}$ without $\rho$ , run $\alpha$ is labelled by $u\in\left(A_{X}\cup\left\{\rho\right\}\right)^{*}$ (possibly empty), and no simple cycle $\theta$ with $\text{{{eff}}}\left(\theta\right)\in\mathbb{N}\times\mathbb{N}_{+}$ is reachable from $r_{1}$ and backwards-reachable from $r_{2}$ . Note that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\pi_{\mathrm{pre}}\pi_{1}\pi_{2}% \cdots\pi_{i-1}\alpha\right)(y)=0$ .

Assume that $\alpha$ contains a simple cycle $\theta$ . If $\text{{{eff}}}\left(\theta\right)(x)\leq 0$ , this cycle can be removed from $\pi$ without decreasing the output value, which contradicts the assumption that $\pi$ is the shortest. If otherwise $\text{{{eff}}}\left(\theta\right)(x)>0$ , we obtain a pumpable run of type A.1 featuring $\theta$ and a simple path to $r_{1}$ . Again, a sustainable run to the final state $q_{\mathrm{fin}}$ is guaranteed by Claim 31, and thus in this case the proof is finished.

Hence, we can assume that $\alpha$ does not have simple cycles. Due to Claim 12, we have that $\text{{{eff}}}\left(\alpha\right)(x)\in[-CN,CN]$ . By Lemma 15, $\text{{{eff}}}\left(\beta\right)$ decomposes into $\text{{{eff}}}\left(\beta\right)=\text{{{eff}}}\left(\beta^{\prime}\right)+(A,B)$ for a run $\beta^{\prime}$ from $r_{1}$ to $r_{2}$ of length $\leq N$ , and $(A,B)\in\text{{{Cone}}}_{\mathbb{N}}\left(\Theta\right)$ , where $\Theta$ is the set of simple cycles that are reachable from $r_{1}$ and backwards-reachable from $r_{2}$ by transitions not involving $\rho$ . By assumption, $\text{{{eff}}}\left(\theta\right)\not\in\mathbb{N}\times\mathbb{N}_{+}$ for any $\theta\in\Theta$ . Thus, for each $\theta\in\Theta$ , either $\text{{{eff}}}\left(\theta\right)(x)<0$ or $\text{{{eff}}}\left(\theta\right)(y)\leq 0$ . Hence, for $\theta$ with $\text{{{eff}}}\left(\theta\right)(y)>0$ , we have $\text{{{eff}}}\left(\theta\right)(x)<0$ . Take $\theta_{\circlearrowright}$ such that $\text{{{eff}}}\left(\theta_{\circlearrowright}\right)=(a,b)$ , $b>0$ (and hence $a<0$ ) and $\frac{b}{-a}$ is the largest possible among cycles satisfying these conditions. Every simple cycle has length at most $N$ , therefore its effect belongs to $[-CN,CN]^{2}$ . Thus, $\frac{CN}{1}\geq\frac{b}{-a}$ . Let $\ell(t)\coloneqq\frac{b}{a}t$ . If there exists $\theta^{\prime}$ such that $\text{{{eff}}}\left(\theta^{\prime}\right)$ lies above line $\ell$ , then we have identified two cycles that span a cone having a nonempty intersection with the positive quadrant; this yields a pumpable run of type A.3, and, by Claim 31, we get a sustainable run starting at $q_{i}$ .

Otherwise, $\text{{{Cone}}}_{\mathbb{N}}\left(\Theta\right)$ lies below $\ell$ . Since $\pi_{i}$ ends with $\eta$ and has effect at least $M$ , $\text{{{eff}}}\left(\beta\right)(y)>M$ , therefore $B>0$ . This in turn implies $A<0$ , because $(A,B)$ is bellow $\ell$ . Hence $B<\ell A=\frac{b}{a}A\leq-CNA$ . We know that $\text{{{eval}}}_{(v_{i-1},0)}\left(\pi_{i}\right)\geq M$ , therefore

\displaystyle\begin{cases}\text{{{eval}}}_{(v_{i-1},0)}\left(\alpha\beta\right% )(x)\geq M\\ \text{{{eval}}}_{(v_{i-1},0)}\left(\alpha\beta\right)(y)\geq M\end{cases}

and thus

\displaystyle\begin{cases}v_{i-1}+\text{{{eff}}}\left(\alpha\right)(x)+\text{{% {eff}}}\left(\beta^{\prime}\right)(x)+A\geq M\\ \mathrlap{\,0}\phantom{v_{i-1}+\text{{{eff}}}\left(\alpha\right)(x)}+\text{{{% eff}}}\left(\beta^{\prime}\right)(y)+B\geq M\end{cases}

Since $v_{i}<M+W$ , and effects of simple runs $\alpha$ and $\beta^{\prime}$ are bounded by Claim 12, we get

\displaystyle\left\{\begin{aligned} \cancel{M}+W+2CN+A&\geq\cancel{M}\\ CN+B&\geq M\end{aligned}\right.

and

\displaystyle\left\{\begin{aligned} 12C^{2}N^{3}+2C^{2}N^{2}&\geq-CNA\\ B&\geq 15C^{2}N^{3}-CN\end{aligned}\right.

Since $B<-CNA$ , we have $15C^{2}N^{3}-CN<12C^{2}N^{3}+2C^{2}N^{2}$ and finally $3C^{2}N^{3}<2C^{2}N^{2}+CN$ which yields a contradiction that concludes the proof. $\hfill\blacktriangleleft$

5 Output-minimum CRAs

In this section, we consider CRAs in which minimum substitutions can only appear in the output function. We call such CRAs output-minimum for brevity.

The main results of this section are as follows.

Theorem 32.

Boundedness of output-minimum CRAs with no transpositions is coNP-complete, even if the numbers in the substitutions are presented in unary.

Theorem 33.

Boundedness of output-minimum CRAs is PSPACE-complete, even if the numbers in the substitutions are presented in unary.

For the rest of the section, fix the set of registers $X\coloneqq\left\{x_{1},\ldots,x_{d}\right\}$ . Let $\eta_{X^{\prime}}\coloneqq\left\{x_{1}\leftarrow\min\left\{x\mid x\in X^{% \prime}\right\}\right\}$ for $X^{\prime}\subseteq X$ . Once again, we use the formalism of regular languages of substitutions presented in Section 3. Recall that $\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)=T_{X}% \cup R_{X}\cup A_{X}\cup M_{X}$ . Since we are considering output-minimum CRAs, similarly to Claim 13, we can assume that the alphabet contains only elementary substitutions from $T_{X}\cup R_{X}\cup A_{X}$ , with the only exception of a minimum transition which comes at the end of the word. Thus, in Section 5.1 and Section 5.2 we consider the language boundedness problem for NFAs $\mathcal{A}$ such that for some $X^{\prime}\subseteq X$ , we have, respectively, $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)\subseteq\left(A_{X}\cup R_{X}% \right)^{*}\eta_{X^{\prime}}$ and $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)\subseteq\left(A_{X}\cup R_{X}% \cup T_{X}\right)^{*}\eta_{X^{\prime}}$ . As shown in Section 3, this is enough to prove Theorems 32 and 33.

5.1 Output-minimum CRAs with no transpositions

Proposition 34.

Boundedness for regular subsets of $\left(A_{X}\cup R_{X}\right)^{*}\eta_{X^{\prime}}$ is coNP-complete, even if the numbers in the substitutions are presented in unary.

Proof.

As a certificate of unboundedness, we consider substitutions $\alpha_{1},\dots,\alpha_{d+1}$ , $\beta_{1},\dots,\beta_{d}$ respecting the conditions of Lemma 16, together with a run $\pi$ of $\mathcal{A}$ witnessing that $\alpha_{1}\beta_{1}^{+}\alpha_{2}\dots\alpha_{d}\beta_{d}^{+}\alpha_{d+1}\eta_% {X^{\prime}}\subseteq\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ . Checking the second and third conditions of Lemma 16 is trivial and by having $\pi$ in the certificate, it is also easy to check the first condition in linear time.

Checking the last conditions requires a bit more work. As argued in the proof of Lemma 16, all substitutions in $\beta_{1},\dots,\beta_{d}$ can be modified so that they become additive substitutions without changing the value of $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(\alpha_{1}\beta_{1}^{a_{1}}\alpha_{% 2}\dots\alpha_{d}\beta_{d}^{a_{d}}\alpha_{d+1}\eta_{X^{\prime}}\right)(x_{1})$ . Now, let the vectors $\vec{v}_{1},\dots,\vec{v}_{d}$ be the effects of the modified substitutions $\beta_{1},\dots,\beta_{d}$ . By Theorem 14, we only need to solve the following linear program

\exists a_{1},\dots,a_{d}\in\mathbb{Q}_{\geq 0}\text{ s.t. }a_{1}\vec{v}_{1}+a% _{2}\vec{v}_{2}+\dots+a_{d}\vec{v}_{d}>0,

which can be done in polynomial time.

To prove coNP-hardness, we reduce the satisfiability problem, which is NP-complete [20], to the complement of the boundedness problem.

Problem 35 (Satisfiability).

Input: A set $C=\left\{c_{1},\ldots,c_{m}\right\}$ of clauses over boolean variables $p_{1},\ldots,p_{n}$ .

Question: Does there exist an assignment of Boolean values to the variables satisfying all the clauses?

As registers, we take the set of all clauses: $X=C=\left\{c_{1},\ldots,c_{m}\right\}$ . Let $C_{p}\coloneq\left\{c\in C\nonscript\>\middle|\allowbreak\nonscript\>\mathopen% {}p\vDash c\right\}$ and $C_{\neg p}\coloneq\left\{c\in C\mid\neg p\vDash c\right\}$ be the sets of clauses satisfied by $p=\top$ and $p=\bot$ , respectively. Also, for a literal $x$ , let $\text{{{inc}}}\left(x\right)\coloneq\left\{c\leftarrow c+1\nonscript\>\middle|% \allowbreak\nonscript\>\mathopen{}c\in C_{x}\right\}$ . Consider the generalised NFA $\mathcal{A}$ in Figure 3.

Figure 3: Generalised NFA

\mathcal{A}

for satisfiability. Transitions are labelled by regular expressions.

It is readily seen that for any $N\in\mathbb{N}$ , there exists a word

w\in\left(\text{{{inc}}}\left(C_{p_{1}}\right)^{N}\cup\text{{{inc}}}\left(C_{% \neg p_{1}}\right)^{N}\right)\cdots\left(\text{{{inc}}}\left(C_{p_{n}}\right)^% {N}\cup\text{{{inc}}}\left(C_{\neg p_{n}}\right)^{N}\right)\eta_{X}

such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w\right)(x_{1})\geq N$ if and only if the variable assignment induced by $w$ for variables $p_{1},\dots,p_{n}$ satisfies all the clauses $c_{1},\dots,c_{m}$ . $\hfill\blacktriangleleft$

5.2 Output-minimum CRAs with transpositions

Proposition 36.

Boundedness for regular subsets of $\left(A_{X}\cup R_{X}\cup T_{X}\right)^{*}\eta_{X}$ is in PSPACE.

Proof idea.

We prove containment in PSPACE by operating on an exponentially larger NFA $\mathcal{P}_{\mathcal{A}}$ , called permutation NFA. This NFA encodes all possible register permutations inside its state space, and hence its alphabet contains only additive and reset substitutions. It can be checked in NPSPACE whether this larger NFA admits a certificate of the type presented in Lemma 16. By Savitch’s theorem we get that the problem is in PSPACE [38]. $\hfill\blacktriangleleft$

Proof.

Fix a finite alphabet $S\subset A_{X}\cup R_{X}\cup T_{X}$ and let $C=\text{{{maxc}}}\left(S\right)$ . Fix NFA $\mathcal{A}=(Q,S\cup\left\{\eta_{X^{\prime}}\right\},\delta,q_{\mathrm{ini}},Q% _{\mathrm{fin}})$ such that $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)\subseteq S^{*}\eta_{X^{\prime}}$ . Let $G_{X}$ be the set of all permutations of the set $X$ and let $\mathcal{P}_{\mathcal{A}}=(Q^{\prime},S^{\prime}\cup\left\{\eta_{X^{\prime}}% \right\},\delta^{\prime},q_{\mathrm{ini}}^{\prime},Q_{\mathrm{fin}}^{\prime})$ , where $Q^{\prime}=Q\times G_{X}$ , $S^{\prime}=S\setminus T_{X}$ , and $Q_{\mathrm{fin}}^{\prime}=Q_{\mathrm{fin}}\times G_{X}$ . We also take ${q_{\mathrm{ini}}}^{\prime}=(q_{\mathrm{ini}},\tau_{0})$ , where $\tau_{0}$ is the identity permutation. Let $\text{{{id}}}\in S$ be the additive substitution that adds $0$ to every register. For $s\in T_{X}$ and $\tau\in G_{X}$ we define $(\tau\circ s)(x)=s(\tau(x))$ . Finally, $\delta^{\prime}$ contains transitions

	$\displaystyle((q,\tau),\text{{{id}}},(q^{\prime},\tau\circ s))$	$\displaystyle\in\delta^{\prime}\qquad\text{for every $(q,s,q^{\prime})\in% \delta$ such that $s\in A_{X}$},$
	$\displaystyle((q,\tau),s,(q^{\prime},\tau))$	$\displaystyle\in\delta^{\prime}\qquad\text{for every $(q,s,q^{\prime})\in% \delta$ such that $s\notin T_{X}$}.$

Clearly, $\mathcal{A}$ is unbounded if and only if $\mathcal{P}_{\mathcal{A}}$ is unbounded if and only if there exist words $\alpha_{1},\dots,\alpha_{d+1},\beta_{1},\dots,\beta_{d}$ that adhere to the conditions of Lemma 16 and run $\pi$ of $\mathcal{P}_{\mathcal{A}}$ witnessing that $\alpha_{1}\beta_{1}^{+}\alpha_{2}\dots\alpha_{d}\beta_{d}^{+}\alpha_{d+1}\eta_% {X^{\prime}}\subseteq\text{{{$\mathcal{L}$}}}\left(\mathcal{P}_{\mathcal{A}}\right)$ . Since $\lvert Q^{\prime}\rvert=\lvert Q\rvert\cdot d!$ , we can store one state with polynomial space. Hence, an NPSPACE algorithm can non-deterministically search for the run $\pi$ without constructing $\mathcal{P}_{\mathcal{A}}$ explicitly. Verifying the first three conditions of Lemma 16 can be done on the fly in linear space. Also, a non-deterministic algorithm can guess and verify that $\vec{v}_{1}\dots,\vec{v}_{d}$ are the effects of cycles $\beta_{1},\dots,\beta_{d}$ on the fly. Finally, it is easy to verify that a positive linear combination of them has positive effect on all registers. Thus, we can conclude the argument by recalling that $\textup{{NPSPACE}}=\textup{{PSPACE}}$ by Savitch’s theorem [38]. $\hfill\blacktriangleleft$

Proposition 37.

Boundedness for regular subsets of $\left(A_{X}\cup R_{X}\cup T_{X}\right)^{*}\eta_{X}$ is PSPACE-hard, even if the numbers in the substitutions are presented in unary.

Proof idea.

We reduce the DFA intersection problem, which is PSPACE-complete [27]. For every state of each DFA, we create a separate register in the constructed CRA $\mathcal{C}$ . We simulate reading a letter by all the DFAs by moving a large value to the registers corresponding to the new active states of the DFAs, and keeping the values of all remaining registers zero. These large values come from a self-loop transition in the initial state of $\mathcal{C}$ , and $\mathcal{C}$ cannot return to the initial state afterwards. All DFAs accept the same word if and only the large values can be simultaneously brought to the registers corresponding to the final states of the DFAs. The output of $\mathcal{C}$ is thus set to be the minimum of these registers. $\hfill\blacktriangleleft$

Proof.

We reduce from the following PSPACE-complete problem [27]:

Problem 38 (DFA intersection).

Input: $n\in\mathbb{N}$ , alphabet $\Sigma$ , $n$ DFAs $\mathcal{A}_{i}=(Q_{i},\Sigma,\delta_{i},q_{\mathrm{ini}}^{(i)},Q^{(i)}_{% \mathrm{fin}})$ , $1\leq i\leq n$ .

Question: Does there exist a word accepted by all the DFAs?

We can assume that each DFA has only one final state, which can be ensured as follows: add a new letter $\#$ to $\Sigma$ and two new states $q^{+}_{i}$ , $q^{-}_{i}$ to each $\mathcal{A}_{i}$ . For each $i$ , make this new letter $\#$ send all states from $Q^{(i)}_{\mathrm{fin}}$ to $q^{+}_{i}$ , and all other states of $\mathcal{A}_{i}$ to $q^{-}_{i}$ . Make the new letter induce a self-loop for both $q^{+}_{i},q^{-}_{i}$ and make $q^{+}_{i}$ to be the only final state in each DFA.

We construct an NFA $\mathcal{A}$ such that the language $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ is bounded if and only if $\bigcap_{1\leq i\leq n}\text{{{$\mathcal{L}$}}}\left(\mathcal{A}_{i}\right)$ is empty. Let $X=\left\{q_{i}^{(j)}\mid 1\leq j\leq n,q_{i}\in Q_{j}\right\}$ . The idea is that the registers correspond to the states of the DFAs, and register $r_{i}^{(j)}$ has a positive value after reading $w\in\Sigma$ if and only if the $i$ ’th state in $\mathcal{A}_{j}$ is active after reading $w$ . Next, we describe $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)$ in terms of a regular language.

Let $\nu_{\mathrm{inc}}=\left\{q_{\mathrm{ini}}^{(i)}\leftarrow q_{\mathrm{ini}}^{(% i)}+1\mid 1\leq i\leq n\right\}$ be a substitution that increments the registers representing initial states for each $\mathcal{A}_{i}$ . Also, for every $\sigma\in\Sigma$ , let

	$\displaystyle T_{i,\sigma}=\left\{\left\{q^{\prime}\leftarrow q\right\}\cup% \left\{q\leftarrow 0\mid q\neq q^{\prime}\right\}\mid(q,\sigma,q^{\prime})\in% \delta_{i},q\neq q^{\prime}\right\}\text{ and }$
	$\displaystyle T_{\sigma}=T_{1,\sigma}\cdot T_{2,\sigma}\cdot\dots\cdot T_{n,% \sigma},$
	$\displaystyle T=\bigcup_{\sigma\in\Sigma}T_{\sigma}.$

There is a substitution in $T_{i,\sigma}$ that simulates every transition inside $\mathcal{A}_{i}$ for letter $\sigma\in\Sigma$ . The idea is that after we guess the next letter $\sigma\in\Sigma$ , for each $\mathcal{A}_{i}$ we need to simulate the transition that is executed when reading this letter. If we pick the correct transition, we move our positive value from register $q_{i}$ to $q_{i}^{\prime}$ , and resetting all other registers does not change their values. However, if we pick a wrong transition, we reset our positive value and we can never recover. Then, a substitution from $T_{\sigma}$ simulates executing a transition labelled by letter $\sigma$ in all $\mathcal{A}_{i}$ and a substitution from $T$ simulates choosing a letter $\sigma\in\Sigma$ and executing a transition labelled by $\sigma$ in all $\mathcal{A}_{i}$ . Finally let $\nu_{\text{{{out}}}}=\left\{x\leftarrow\min\{q_{\mathrm{fin}}^{{(i)}}\mid 1% \leq i\leq n\}\right\}$ . We argue that $\text{{{$\mathcal{L}$}}}\left(\mathcal{A}\right)=\nu_{\mathrm{inc}}^{*}\cdot T% ^{*}\cdot\nu_{\text{{{out}}}}$ is unbounded if and only if $\bigcap_{1\leq i\leq n}L(A_{i})$ is non-empty.

Consider a word $w=\sigma_{1}\dots\sigma_{m}\in\Sigma^{*}$ and an integer $N\in\mathbb{N}$ . For every $1\leq i\leq n$ it follows inductively that there exists a word $w_{j}^{\prime}\in\mathrm{inc}^{N+1}\cdot T_{\sigma_{1}}\cdot T_{\sigma_{2}}% \cdot\dots\cdot T_{\sigma_{j}}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{j}^{\prime}\right)(q^{(i)})=N+1$ , for $q\in Q_{i}$ if and only if $q_{\mathrm{ini}}^{(i)}\xrightarrow{\sigma_{1}\dots\sigma_{j}}q^{(i)}$ . Thus, there exists a word $w_{m}^{\prime}\in\nu_{\mathrm{inc}}^{*}\cdot T^{*}\cdot\nu_{\text{{{out}}}}$ such that $\text{{{eval}}}_{\mathrm{\mathbf{0}}}\left(w_{m}^{\prime}\right)=N+1$ if and only if $\bigcap_{1\leq i\leq n}L(A_{i})$ is non-empty. $\hfill\blacktriangleleft$

6 Stateless CRAs

In this section, for every $d\geq 2$ we present a fairly restricted family of unbounded CRAs with $d$ registers such that the length of a shortest run outputting a value $N\in\mathbb{N}$ is lower bounded by $F_{d-1}(N)$ , the $(d-1)$ st function in the hierarchy of fast-growing functions. These functions are defined as follows. Let $F_{1}(n)=2n$ and for every $k\geq 2$ let $F_{k}(n)=F_{k-1}\circ\dots\circ F_{k-1}(1)$ , where $\circ$ denotes the composition of functions, and this composition is taken $n$ times. For example, $F_{2}(n)=2^{n}$ and $F_{3}(n)=2^{2^{\cdot^{\cdot^{\cdot^{2}}}}}=\text{Tower}(n)$ , where exponentiation is taken $n$ times. We construct these CRAs inductively in the following theorem.

Theorem 39.

For every $d\geq 2$ , there exists a stateless CRA $\mathcal{C}$ with $d$ registers and $d$ transitions such that for every $N\in\mathbb{N}_{+}$ , any run of $\mathcal{C}_{d}$ that outputs a value of at least $N$ must have length at least $F_{d-1}(N)$ .

Proof.

For $d=2$ and $d=3$ consider the two CRAs in Figure 4.

Figure 4: Unbounded CRAs

\mathcal{C}_{2}

(left) and

\mathcal{C}_{3}

(right) with 2 and 3 registers.

Let us prove that $\mathcal{C}_{2}$ and $\mathcal{C}_{3}$ satisfies the statement of the lemma. Let $N\in\mathbb{N}_{+}$ be an arbitrary positive integer. Since we are dealing with stateless CRAs, we denote a configuration $(q,\left\{x_{1}\leftarrow k_{1},x_{2}\leftarrow k_{2},\dots,x_{n}\leftarrow k_% {n}\right\})$ by a vector $(k_{1},k_{2},\dots,k_{n})$ . Clearly, for both $\mathcal{C}_{2}$ and $\mathcal{C}_{3}$ , the transitions labelled by $a_{1}$ are the only ones that can increase the value of register $x_{1}$ and since these transitions reset the values of all other counters, any run outputting $N$ must start by taking this transition $m$ many times, $m>0$ , reaching in $\mathcal{C}_{2}$ and $\mathcal{C}_{3}$ the configurations $(m,0)$ and $(m,0,0)$ , respectively. The value $m$ can be seen as the initial budget that is necessary for increasing the values of other registers. Clearly, the shortest run that outputs $N$ in $\mathcal{C}_{2}$ reaches the configuration $(2N,0)$ , then takes $N$ times the transition labelled by $a_{2}$ and outputs. Since it must start by getting to the configuration $(2N,0)$ , its length is at most $F_{1}(N)=2N$ .

Let now $\pi_{3}$ be a shortest run in $\mathcal{C}_{3}$ that outputs $N$ . Clearly, $\pi_{3}$ needs to increase the value of register $x_{3}$ . The transition labelled by $a_{3}$ is the only one that increases $x_{3}$ , however, it contains a minimum update for $x_{1}$ . Since $\pi_{3}$ is a shortest path outputting $N$ , before reading $a_{3}$ it reaches a configuration in which the values of registers $x_{2},x_{3}$ are equal, otherwise some transitions can be removed from it without changing the output value.

Thus, $\pi_{3}$ initialises the budget by reading $a_{1}^{m}$ , and then, before reading $a_{3}$ , it reads a word in $a_{2}^{*}$ which applies the function $F_{1}^{-1}(\cdot)=\frac{\cdot}{2}$ to the value of register $x_{1}$ . We argue that in order to output $N$ , $m=F_{2}^{-1}(N)=2^{N}$ . Indeed, $\pi_{3}$ must reach a value $m$ in register $x_{1}$ and then apply $N$ many times the function $F_{1}^{-1}(\cdot)$ to register $x_{1}$ , so $m=F_{2}^{-1}(N)$ . Thus, the length of $\pi_{3}$ must be longer than $F_{2}(N)$ . Furthermore, we see that $\pi_{3}$ has the following shape $(0,0,0)\xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow(F_{2}(N),0,0)% \xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow(N,N,N)$ .

Assume now that there exists $\mathcal{C}_{d-1}$ with the property from the statement of the lemma. We modify it by adding a new letter $a_{d}$ to the alphabet $\Sigma$ , and extend the substitutions of the transitions as follows:

$\blacksquare$

add $x_{d}\leftarrow 0$ to $a_{1}$ ,
$\blacksquare$

add $x_{d}\leftarrow x_{d}$ to $a_{i}$ for $1<i<d-1$ , and
$\blacksquare$

let the substitution of $a_{d}$ be
$\left\{x_{1}\leftarrow\min\{x_{1},\dots,x_{d-1}\},x_{2}\leftarrow 0,\dots,x_{d% -1}\leftarrow 0,x_{d}\leftarrow x_{d}+1\right\}$ .

We know that there exists a shortest path $\pi_{d-1}$ with the following shape $(0,\dots,0)\xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow(F_{d-2}(N),0,% \dots,0)\xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow(N,N,\dots,N,0)$ . So, in order to increase the register $x_{d}$ by one, we need to have enough budget on register $x_{1}$ to be able to apply the function $F_{d-2}^{-1}$ to its value. Since we need to increase the value of $x_{d}$ by one $N$ times, it follows that we need to repeat this process $N$ times so that $\pi_{d}$ has shape $(0,\dots,0)\xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow(F_{d-1}(N),0,% \dots,0)\xrightarrow[]{}\mathrel{\mkern-14.0mu}\rightarrow(N,N,\dots,N,N)$ . Thus its length must be at least $F_{d-1}(N)$ . $\hfill\blacktriangleleft$

7 Conclusions and open problems

The most obvious open problem left by this work is the decidability of boundedness for copyless linear CRAs with resets with more than two registers. We conjecture that it is decidable for arbitrary number of registers. Our techniques and the shapes of the witnesses for the two-register case might be useful for proving that.

Another interesting open problem is the precise complexity of the two-register case where numbers in the substitutions are presented in binary. We have proved that this problem is NL-hard and in coNP, but no better bound is known even if minimum substitutions are only allowed in the output. In the latter case, it follows from our results that the witness of unboundedness consists of at most two cycles and some paths connecting them. This relates to the following natural problem whose complexity we were not able to find in the literature. Let $G=(V,E)$ be a digraph, and $\omega:E\to\mathbb{Z}^{2}$ be a (bi-criteria) weighting function on its edges. Given $G$ and $\omega$ , find a cycle in $G$ such that the sum of weights of its edges is component-wise positive. This is of course a generalisation of the problem of finding a cycle of negative weight in a digraph, which can be solved in polynomial time by e.g. Bellman-Ford-Moore algorithm [6].

References

[1] Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata? Information and Computation, 282:104651, 2022. doi:10.1016/j.ic.2020.104651.
[2] Shaull Almagor, Michaël Cadilhac, Filip Mazowiecki, and Guillermo A. Pérez. Weak cost register automata are still powerful. International Journal of Foundations of Computer Science, 31(6):689–709, 2020. doi:10.1142/S0129054120410026.
[3] Rajeev Alur, Loris D’Antoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), pages 13–22, 2013. doi:10.1109/LICS.2013.65.
[4] Rajeev Alur and Mukund Raghothaman. Decision problems for additive regular functions. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 37–48. Springer, 2013. doi:10.1007/978-3-642-39212-2_7.
[5] Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 6(2):28:1–28:36, 2010. doi:10.1145/1721837.1721844.
[6] Jørgen Bang-Jensen and Gregory Z Gutin. Digraphs: theory, algorithms and applications. Springer Science & Business Media, 2008.
[7] Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in two-dimensional vector addition systems with states is pspace-complete. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 32–43. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.14.
[8] Michael Blondin, Christoph Haase, Filip Mazowiecki, and Mikhail A. Raskin. Affine extensions of integer vector addition systems with states. Log. Methods Comput. Sci., 17(3), 2021. doi:10.46298/LMCS-17(3:1)2021.
[9] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Transactions on Computational Logic, 11(4):23:1–23:38, 2010. doi:10.1145/1805950.1805953.
[10] Karel Culík and Jarkko Kari. Digital images and formal languages. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 599–616. Springer, 1997. doi:10.1007/978-3-642-59126-6_10.
[11] Wojciech Czerwiński, Engel Lefaucheux, Filip Mazowiecki, David Purser, and Markus A. Whiteland. The boundedness and zero isolation problems for weighted automata over nonnegative rationals. In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 15:1–15:13. ACM, 2022. doi:10.1145/3531130.3533336.
[12] Laure Daviaud. Containment and equivalence of weighted automata: Probabilistic and max-plus cases. In Alberto Leporati, Carlos Martín-Vide, Dana Shapira, and Claudio Zandron, editors, Language and Automata Theory and Applications - 14th International Conference, LATA 2020, Milan, Italy, March 4-6, 2020, Proceedings, volume 12038 of Lecture Notes in Computer Science, pages 17–32. Springer, 2020. doi:10.1007/978-3-030-40608-0_2.
[13] Laure Daviaud. Register complexity and determinisation of max-plus automata. ACM SIGLOG News, 7(2):4–14, 2020. doi:10.1145/3397619.3397621.
[14] Laure Daviaud, Pierre-Alain Reynier, and Jean-Marc Talbot. A generalised twinning property for minimisation of cost register automata. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2016), pages 857–866, 2016. doi:10.1145/2933575.2934549.
[15] Laure Daviaud and Andrew Ryzhikov. Universality and forall-exactness of cost register automata with few registers. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPIcs, pages 40:1–40:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.MFCS.2023.40.
[16] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theoretical Computer Science, 380(1-2):69–86, 2007. doi:10.1016/J.TCS.2007.02.055.
[17] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. In Handbook of weighted automata, pages 175–211. Springer, 2009.
[18] Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer Berlin, Heidelberg, 1st edition, 2009. doi:10.1007/978-3-642-01492-5.
[19] Manfred Droste and Dietrich Kuske. Weighted automata. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 113–150. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. doi:10.4171/Automata-1/4.
[20] Michael R Garey and David S Johnson. Computers and intractability, volume 174. freeman San Francisco, 1979.
[21] Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 112–124. Springer, 2014. doi:10.1007/978-3-319-11439-2_9.
[22] Kosaburo Hashiguchi. New upper bounds to the limitedness of distance automata. Theor. Comput. Sci., 233(1-2):19–32, 2000. doi:10.1016/S0304-3975(97)00260-0.
[23] Kosaburo Hashiguchi, Kenichi Ishiguro, and Shuji Jimbo. Decisability of the equivalence problem for finitely ambiguous automata. International Journal of Algebra and Computation, 12(03):445–461, 2002. doi:10.1142/S0218196702000845.
[24] John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135–159, 1979. doi:10.1016/0304-3975(79)90041-0.
[25] Daniel Kirsten and Sylvain Lombardy. Deciding Unambiguity and Sequentiality of Polynomially Ambiguous Min-Plus Automata. In 26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009), volume 3 of LIPIcs, pages 589–600, 2009. doi:10.4230/LIPIcs.STACS.2009.1850.
[26] Ines Klimann, Sylvain Lombardy, Jean Mairesse, and Christophe Prieur. Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. Theoretical Computer Science, 327(3):349–373, 2004. doi:10.1016/j.tcs.2004.02.049.
[27] Dexter Kozen. Lower bounds for natural proof systems. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 254–266. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.16.
[28] Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. International Journal of Algebra and Computation, 4(3):405–426, 1994. doi:10.1142/S0218196794000063.
[29] Hing Leung and Viktor Podolskiy. The limitedness problem on distance automata: Hashiguchi’s method revisited. Theor. Comput. Sci., 310(1-3):147–158, 2004. doi:10.1016/S0304-3975(03)00377-3.
[30] Ernst W. Mayr. An algorithm for the general petri net reachability problem. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 238–246. ACM, 1981. doi:10.1145/800076.802477.
[31] Filip Mazowiecki and Cristian Riveros. Maximal partition logic: Towards a logical characterization of copyless cost register automata. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 144–159. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPICS.CSL.2015.144.
[32] Filip Mazowiecki and Cristian Riveros. Copyless cost-register automata: Structure, expressiveness, and closure properties. Journal of Computer and System Sciences, 100:1–29, 2019. doi:10.1016/j.jcss.2018.07.002.
[33] Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, USA, 1967.
[34] Mehryar Mohri. Finite-state transducers in language and speech processing. Computational Linguistics, 23(2):269–311, 1997. URL: https://aclanthology.org/J97-2003.
[35] Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., USA, 1986.
[36] Marcel-Paul Schützenberger. On the definition of a family of automata. Information and Control, 4(2):245–270, 1961. doi:10.1016/S0019-9958(61)80020-X.
[37] Imre Simon. On semigroups of matrices over the tropical semiring. RAIRO Theor. Informatics Appl., 28(3-4):277–294, 1994. doi:10.1051/ITA/1994283-402771.
[38] Michael Sipser. Introduction to the Theory of Computation. Course Technology, Boston, MA, third edition, 2013.
[39] Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In 26th Annual Symposium on Foundations of Computer Science (FOCS 1985), pages 327–338, 1985. doi:10.1109/SFCS.1985.12.
[40] Andreas Weber. Finite-valued distance automata. Theoretical Computer Science, 134(1):225–251, 1994. doi:10.1016/0304-3975(94)90287-9.

[bib.bib1] [1] Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata? Information and Computation, 282:104651, 2022. doi:10.1016/j.ic.2020.104651.

[bib.bib2] [2] Shaull Almagor, Michaël Cadilhac, Filip Mazowiecki, and Guillermo A. Pérez. Weak cost register automata are still powerful. International Journal of Foundations of Computer Science, 31(6):689–709, 2020. doi:10.1142/S0129054120410026.

[bib.bib3] [3] Rajeev Alur, Loris D’Antoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), pages 13–22, 2013. doi:10.1109/LICS.2013.65.

[bib.bib4] [4] Rajeev Alur and Mukund Raghothaman. Decision problems for additive regular functions. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 37–48. Springer, 2013. doi:10.1007/978-3-642-39212-2_7.

[bib.bib5] [5] Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 6(2):28:1–28:36, 2010. doi:10.1145/1721837.1721844.

[bib.bib6] [6] Jørgen Bang-Jensen and Gregory Z Gutin. Digraphs: theory, algorithms and applications. Springer Science & Business Media, 2008.

[bib.bib7] [7] Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in two-dimensional vector addition systems with states is pspace-complete. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 32–43. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.14.

[bib.bib8] [8] Michael Blondin, Christoph Haase, Filip Mazowiecki, and Mikhail A. Raskin. Affine extensions of integer vector addition systems with states. Log. Methods Comput. Sci., 17(3), 2021. doi:10.46298/LMCS-17(3:1)2021.

[bib.bib9] [9] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Transactions on Computational Logic, 11(4):23:1–23:38, 2010. doi:10.1145/1805950.1805953.

[bib.bib10] [10] Karel Culík and Jarkko Kari. Digital images and formal languages. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 599–616. Springer, 1997. doi:10.1007/978-3-642-59126-6_10.

[bib.bib11] [11] Wojciech Czerwiński, Engel Lefaucheux, Filip Mazowiecki, David Purser, and Markus A. Whiteland. The boundedness and zero isolation problems for weighted automata over nonnegative rationals. In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 15:1–15:13. ACM, 2022. doi:10.1145/3531130.3533336.

[bib.bib12] [12] Laure Daviaud. Containment and equivalence of weighted automata: Probabilistic and max-plus cases. In Alberto Leporati, Carlos Martín-Vide, Dana Shapira, and Claudio Zandron, editors, Language and Automata Theory and Applications - 14th International Conference, LATA 2020, Milan, Italy, March 4-6, 2020, Proceedings, volume 12038 of Lecture Notes in Computer Science, pages 17–32. Springer, 2020. doi:10.1007/978-3-030-40608-0_2.

[bib.bib13] [13] Laure Daviaud. Register complexity and determinisation of max-plus automata. ACM SIGLOG News, 7(2):4–14, 2020. doi:10.1145/3397619.3397621.

[bib.bib14] [14] Laure Daviaud, Pierre-Alain Reynier, and Jean-Marc Talbot. A generalised twinning property for minimisation of cost register automata. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2016), pages 857–866, 2016. doi:10.1145/2933575.2934549.

[bib.bib15] [15] Laure Daviaud and Andrew Ryzhikov. Universality and forall-exactness of cost register automata with few registers. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPIcs, pages 40:1–40:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.MFCS.2023.40.

[bib.bib16] [16] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theoretical Computer Science, 380(1-2):69–86, 2007. doi:10.1016/J.TCS.2007.02.055.

[bib.bib17] [17] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. In Handbook of weighted automata, pages 175–211. Springer, 2009.

[bib.bib18] [18] Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer Berlin, Heidelberg, 1st edition, 2009. doi:10.1007/978-3-642-01492-5.

[bib.bib19] [19] Manfred Droste and Dietrich Kuske. Weighted automata. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 113–150. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. doi:10.4171/Automata-1/4.

[bib.bib20] [20] Michael R Garey and David S Johnson. Computers and intractability, volume 174. freeman San Francisco, 1979.

[bib.bib21] [21] Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 112–124. Springer, 2014. doi:10.1007/978-3-319-11439-2_9.

[bib.bib22] [22] Kosaburo Hashiguchi. New upper bounds to the limitedness of distance automata. Theor. Comput. Sci., 233(1-2):19–32, 2000. doi:10.1016/S0304-3975(97)00260-0.

[bib.bib23] [23] Kosaburo Hashiguchi, Kenichi Ishiguro, and Shuji Jimbo. Decisability of the equivalence problem for finitely ambiguous automata. International Journal of Algebra and Computation, 12(03):445–461, 2002. doi:10.1142/S0218196702000845.

[bib.bib24] [24] John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135–159, 1979. doi:10.1016/0304-3975(79)90041-0.

[bib.bib25] [25] Daniel Kirsten and Sylvain Lombardy. Deciding Unambiguity and Sequentiality of Polynomially Ambiguous Min-Plus Automata. In 26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009), volume 3 of LIPIcs, pages 589–600, 2009. doi:10.4230/LIPIcs.STACS.2009.1850.

[bib.bib26] [26] Ines Klimann, Sylvain Lombardy, Jean Mairesse, and Christophe Prieur. Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. Theoretical Computer Science, 327(3):349–373, 2004. doi:10.1016/j.tcs.2004.02.049.

[bib.bib27] [27] Dexter Kozen. Lower bounds for natural proof systems. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 254–266. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.16.

[bib.bib28] [28] Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. International Journal of Algebra and Computation, 4(3):405–426, 1994. doi:10.1142/S0218196794000063.

[bib.bib29] [29] Hing Leung and Viktor Podolskiy. The limitedness problem on distance automata: Hashiguchi’s method revisited. Theor. Comput. Sci., 310(1-3):147–158, 2004. doi:10.1016/S0304-3975(03)00377-3.

[bib.bib30] [30] Ernst W. Mayr. An algorithm for the general petri net reachability problem. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 238–246. ACM, 1981. doi:10.1145/800076.802477.

[bib.bib31] [31] Filip Mazowiecki and Cristian Riveros. Maximal partition logic: Towards a logical characterization of copyless cost register automata. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 144–159. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPICS.CSL.2015.144.

[bib.bib32] [32] Filip Mazowiecki and Cristian Riveros. Copyless cost-register automata: Structure, expressiveness, and closure properties. Journal of Computer and System Sciences, 100:1–29, 2019. doi:10.1016/j.jcss.2018.07.002.

[bib.bib33] [33] Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, USA, 1967.

[bib.bib34] [34] Mehryar Mohri. Finite-state transducers in language and speech processing. Computational Linguistics, 23(2):269–311, 1997. URL: https://aclanthology.org/J97-2003.

[bib.bib35] [35] Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., USA, 1986.

[bib.bib36] [36] Marcel-Paul Schützenberger. On the definition of a family of automata. Information and Control, 4(2):245–270, 1961. doi:10.1016/S0019-9958(61)80020-X.

[bib.bib37] [37] Imre Simon. On semigroups of matrices over the tropical semiring. RAIRO Theor. Informatics Appl., 28(3-4):277–294, 1994. doi:10.1051/ITA/1994283-402771.

[bib.bib38] [38] Michael Sipser. Introduction to the Theory of Computation. Course Technology, Boston, MA, third edition, 2013.

[bib.bib39] [39] Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In 26th Annual Symposium on Foundations of Computer Science (FOCS 1985), pages 327–338, 1985. doi:10.1109/SFCS.1985.12.

[bib.bib40] [40] Andreas Weber. Finite-valued distance automata. Theoretical Computer Science, 134(1):225–251, 1994. doi:10.1016/0304-3975(94)90287-9.

Boundedness of Cost Register Automata over the Integer Min-Plus Semiring

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Relations between CRAs and WAs

Ambiguity hierarchy of WAs

Restricted classes of CRAs

Our contributions

2 Main definitions

2.1 Expressions, valuations and substitutions

Example 1 (An expression, a substitution and a valuation).

Example 2 (Application and composition of substitutions).

Copyless linear substitution with resets

Example 3 (Copyless linear substitutions with resets).

2.2 Cost register automata

Definition 4 (CRA).

Definition 5 (Semantics of a CRA).

Example 6.

Problem 7 (CRA boundedness).

3 Regular substitution languages

3.1 Substitution languages associated to CRAs

Definition 8 (NFAx⁢(𝒞)).

Problem 9 (Boundedness of regular d-register substitution languages).

Definition 10 (Elementary substitutions).

Lemma 11.

Claim 12 (Maximal constant grows linearly w.r.t. length).

Claim 13 (Elementary substitutions assumption).

3.2 The structure of witnesses with additive and reset substitutions only

Theorem 14 (Only d vectors are sufficient to represent a positive point).

Lemma 15 (Decomposition lemma for additive runs).

Proof idea.

Proof.

Lemma 16 (Pumping lemma).

Proof idea.

Proof.

4 CRAs with two registers

Theorem 17.

Proposition 18.

4.1 Simplifying assumptions

Definition 19 (Graphical notation for Subelem⁢(X)).

Example 20 (Depiction of out-tree⁢(w)).

Lemma 21 (Leading branch x-aligned assumption).

4.2 Unboundedness witnesses

Definition 22 (Unboundedness witness).

Definition 23 (Pumpable run).

Definition 24 (Sustainable run).

Proposition 25.

Proof.

Lemma 26.

Proof.

Claim 27.

Claim 28.

Lemma 29.

4.3 Unboundedness implies the existence of a witness

Proof of Lemma 29..

Example 30.

Claim 31.

Case 1: 𝒗𝒊+𝟏−𝒗𝒊>𝟒⁢𝑪⁢𝑵 for some 𝒊∈ℕ∩[𝒎,𝒏].

Case 2: 𝒗𝒊+𝟏−𝒗𝒊≤𝟒⁢𝑪⁢𝑵 for all 𝒊∈ℕ∩[𝒎,𝒏].

5 Output-minimum CRAs

Theorem 32.

Theorem 33.

5.1 Output-minimum CRAs with no transpositions

Proposition 34.

Proof.

Problem 35 (Satisfiability).

5.2 Output-minimum CRAs with transpositions

Proposition 36.

Proof idea.

Proof.

Proposition 37.

Proof idea.

Definition 8 ( $\text{{{NFA}}}_{x}\left(\mathcal{C}\right)$ ).

Problem 9 (Boundedness of regular $d$ -register substitution languages).

Theorem 14 (Only $d$ vectors are sufficient to represent a positive point).

Definition 19 (Graphical notation for $\text{{{${{\textrm{Sub}}}_{\mathrm{elem}}\kern-0.7pt$}}}\left(X\right)$ ).

Example 20 (Depiction of $\text{{{out-tree}}}\left(w\right)$ ).

Lemma 21 (Leading branch $x$ -aligned assumption).

Case 1: $v_{i+1}-v_{i}>4CN$ for some $i\in\mathbb{N}\cap[m,n]$ .

Case 2: $v_{i+1}-v_{i}\leq 4CN$ for all $i\in\mathbb{N}\cap[m,n]$ .