1737 LABEL:LastPageJan. 20, 2020Jul. 21, 2021 *A preliminary version of this
paper appeared in the proceedings of the 35th Symposium on Theoretical Aspects
of Computer Science (STACS) [MR18].

# Pumping lemmas for weighted automata

Agnishom Chattopadhyay  Chennai Mathematical Institute, India
<EMAIL_ADDRESS>,  Filip Mazowiecki  Max Planck Institute for Software
Systems, Germany<EMAIL_ADDRESS>,  Anca Muscholl  Université de Bordeaux,
France<EMAIL_ADDRESS>and  Cristian Riveros  Pontificia Universidad Católica
de Chile, Santiago, Chile<EMAIL_ADDRESS>
###### Abstract.

We present pumping lemmas for five classes of functions definable by fragments
of weighted automata over the min-plus semiring, the max-plus semiring and the
semiring of natural numbers. As a corollary we show that the hierarchy of
functions definable by unambiguous, finitely-ambiguous, polynomially-ambiguous
weighted automata, and the full class of weighted automata is strict for the
min-plus and max-plus semirings.

Agnishom Chattopadhyay was an intern at the University of Bordeaux, partially
supported by the UMI ReLaX and the French-Indian project IoTTTA

Filip Mazowiecki was partially supported by EPSRC grants EP/M011801/1 and
EP/M012298/1. The work was partly done during a postdoctoral stay at the
University of Bordeaux.

Anca Muscholl was partially supported by the ANR project DeLTA
(ANR-16-CE40-0007).

Cristian Riveros was funded by ANID – Millennium Science Initiative Program –
Code ICN17_002

##  1\. Introduction

Weighted automata (WA for short) are a quantitative extension of finite state
automata used to compute functions over words. They have been extensively
studied since Schützenberger’s early works [Sch61], see also [DKV09]. In
particular, decidability questions [Kro92, ABK11], model extensions [DG07],
logical characterisations [DG07, KR13], and various applications [Moh97,
CIK93] have been thoroughly investigated in recent years.

The class of functions computed by WA enjoys several equivalent
representations in terms of automata and logics. Alur et al. introduced the
model of cost register automata (CRA for short) [ADD+13, AR13], an alternative
model to compute functions over words inspired by programming paradigms, that
recently received a lot of attention [MR, MR19, DRT16, ACMP18]. It was proved
that the linear fragment of CRA is equally expressive to WA. Regarding logics,
Droste and Gastin introduced in [DG07] the so-called Weighted Logic (WL), a
natural extension of monadic second order logics (MSO) from the boolean
semiring to a commutative semiring. It was shown in [DG07] that a natural
syntactic restriction of WL is equally expressive to WA, giving the first
logical characterisation of WA (see also [KR13]).

The decidability and complexity of various decision problems for WA have also
been investigated, unfortunately often with negative results, such as for the
equivalence problem [Kro92, ABK11]. Another basic question, the decidability
of the determinisation problem for WA, is still open. For this reason,
research has focused on various fragments of WA over different semirings. For
example, over a one-letter alphabet, where WA are equivalent to linear
recurrences, some new decidability results were recently shown for limited
fragments [OW14a, OW14b, ABM+20]. Further restrictions of WA involve bounding
their numbers of runs. Among them, the most studied classes are _unambiguous
automata_ , _finitely-ambiguous automata_ , and _polynomially-ambiguous
automata_ , where the numbers of accepting runs are bounded by one, a
constant, a polynomial in the size of input, respectively [Web94, KLMP04,
KL09]. These subclasses of WA turned out to be robust, enjoying equivalent
characterisations in terms of cost register automata [ADD+13] and weighted
logics [KR13].

Although functions defined by WA and subclasses thereof have been studied in
terms of representations and decidability, not much is known about
expressibility issues. Indeed, we are not aware of any general techniques to
show if a function is definable or not by some WA, or any of its subclasses.
Results related to the expressiveness of WA usually require sophisticated
arguments for each particular function [KLMP04, MR] and there is no clear path
to generalise these techniques. For some semirings strict inclusions between
unambiguous, finitely-ambiguous, polynomially-ambiguous, and the full class of
WA are “well-known” to the community, but it is hard to find references to
formal proofs (see related work below). In contrast, for regular languages or
first-order logics there exist elegant and powerful techniques for showing
inexpressibility, as for example, the Myhill-Nerode congruence for regular
languages [HU79] or Ehrenfeucht-Fraïssé games [Fra84, Ehr61, Lib13] and
aperiodic congruences for first-order logic [Sch65]. One would like to have
similar techniques in the quantitative world that simplify inexpressibility
arguments for WA, CRA or WL. Such techniques would help to understand the
inner structure of these functions and unveil their limits of expressibility.

In this paper, we embark in the work of building an expressibility toolbox for
weighted automata. We present five pumping lemmas, each of them for a
different class or subclass of functions defined by WA over the min-plus
semiring, the max-plus semiring or the semiring of natural numbers. For each
pumping lemma we show examples of functions that do not satisfy the lemma,
giving very short inexpressibility proofs. Our results do not attempt to fully
characterise the class or subclasses of weighted automata in terms of pumping
properties, nor to provide conditions that can be verified by a computer. Our
goal is to devise a systematic way to reason about expressibility of weighted
automata and to provide simple arguments to show that functions do not belong
to a given class.

_Related work._ In [Kir08], it is shown that over the min-plus semiring
polynomially-ambiguous automata are strictly more expressive than finitely-
ambiguous automata. In [KLMP04] strict inclusions between unambiguous
automata, finitely-ambiguous automata, and the full class of WA are shown over
the max-plus semiring. Using results from [CKMT16] one can deduce that
unambiguous automata are strictly included in the other classes over the min-
plus and max-plus semirings. More recently, [DG19] studied aperiodic WA over
arbitrary weights, relating fragments of aperiodic WA with various degrees of
ambiguity, and providing separating examples over the min-plus, max-plus and
the natural semiring. In all these papers the strict inclusions are shown by
analysing particular functions. Gathering these results we obtain strict
inclusions between unambiguous automata, finitely-ambiguous automata, and the
full class of WA over the min-plus semiring. However, to our knowledge, there
is no reference for a strict inclusion between polynomially-ambiguous automata
and the full class of WA. There is some work on the semiring of rational
numbers with the usual sum and product [MR19, BFLM20]. In these papers the
polynomially-ambiguous fragment over the one-letter alphabet is characterised
in terms of a fragment of linear recurrence sequences. Both papers provide
proofs that polynomially-ambiguous weighted automata are strictly contained in
the full class of weighted automata over the semiring of rationals.

_Differences with the conference version._ Compared to [MR18], we present new
pumping lemmas for the max-plus semiring (Section 6) regarding finitely
ambiguous and polynomially ambiguous max-plus automata. As a corollary we
obtain a strict hierarchy of functions similar to the one for min-plus
automata.

_Organization_. In Section 2 we introduce weighted automata and some basic
definitions. In Section 3 and Section 4 we present pumping lemmas for weighted
automata over the semiring of natural numbers and its extension using the
operation $\min$. In Section 5 we show the pumping lemma for polynomially-
ambiguous automata over the min-plus semiring, then we turn to the max-plus
semiring in Section 6. Concluding remarks can be found in Section 7.

##  2\. Preliminaries

In this section, we recall the definitions of weighted automata. We start with
the definitions that are standard in this area. A monoid
$\mathbb{M}=(M,\otimes,\mathbb{1})$ is a set $M$ with an associative operation
$\otimes$ and a neutral element $\mathbb{1}$. Standard examples of monoids
are: the set of words $\Sigma^{*}$ with concatenation and empty word; or the
set of matrices with multiplication and the identity matrix. A semiring is a
structure $\mathbb{S}=(S,\oplus,\odot,\mathbb{0},\mathbb{1})$, where
$(S,\oplus,\mathbb{0})$ is a commutative monoid, $(S,\odot,\mathbb{1})$ is a
monoid, multiplication distributes over addition, and $\mathbb{0}\odot
s=s\odot\mathbb{0}=\mathbb{0}$ for each $s\in S$. If the multiplication is
commutative, we say that $\mathbb{S}$ is commutative. In this paper, we always
assume that $\mathbb{S}$ is commutative. We usually denote $S$ or $M$ by the
name of the semiring or monoid $\mathbb{S}$ or $\mathbb{M}$. We are interested
mostly in the tropical semirings: the _min-plus semiring_
$(\mathbb{N}\cup\\{+\infty\\},\min,+,+\infty,0)$ and the _max-plus semiring_
$(\mathbb{N}\cup\\{-\infty\\},\max,+,-\infty,0)$. We are also interested in
the _semiring of natural numbers with infinity_
$(\mathbb{N}\cup\\{\infty\\},+,\cdot,0,1)$, where $\infty+n=\infty$ for every
$n\in\mathbb{N}\cup\\{\infty\\}$ and $\infty\cdot n=\infty$ if $n\neq 0$ and
$0$ otherwise. We denote the tropical semirings by ${\rm Nature}_{\min,+}$ and
${\rm Nature}_{\max,+}$; and the latter semiring by ${\rm Nature}_{+,\times}$.
Note that ${\rm Nature}_{+,\times}$ is an extension of the standard semiring
of natural numbers ${\rm Nature}$ and all our results for ${\rm
Nature}_{+,\times}$ also hold for ${\rm Nature}$. We use the extended version
of ${\rm Nature}$ to transfer some results from ${\rm Nature}_{+,\times}$ to
${\rm Nature}_{\min,+}$ and ${\rm Nature}_{\max,+}$ (see Section 3 and Section
4). Notice that in ${\rm Nature}_{+,\times}$ we did not put a sign in front of
$\infty$. For the semiring structure, this is not relevant. However, some
statements in Section 3 and Section 4 will assume that the semiring is given
with an order. Then one should think that the results hold both when
$\infty=+\infty$ and when $\infty=-\infty$.

Given a finite set $Q$, we denote by $\mathbb{S}^{Q\times Q}$
($\mathbb{S}^{Q}$) the set of square matrices (vectors resp.) over
$\mathbb{S}$ indexed by $Q$. The algebra induced by $\mathbb{S}$ over
$\mathbb{S}^{Q\times Q}$ and $\mathbb{S}^{Q}$ is defined as usual.

We also consider two finite semirings that will be useful during proofs. We
consider the boolean semiring $\mathbb{B}=(\\{0,1\\},\vee,\wedge,0,1)$ and the
extended boolean semiring
$\mathbb{B}_{\infty}=(\\{0,1,\infty\\},\vee,\wedge,0,1)$ such that $\infty\vee
n=\infty$ for every $n\in\\{0,1,\infty\\}$, $\infty\wedge 0=0$, and
$\infty\wedge n=\infty$ if $n\in\\{1,\infty\\}$. These finite semirings will
be used as _abstractions_ of ${\rm Nature}_{\min,+}$, ${\rm Nature}_{\max,+}$
and ${\rm Nature}_{+,\times}$.

###  2.1. Weighted automata

Fix a finite alphabet $\Sigma$ and a commutative semiring $\mathbb{S}$. A
_weighted automaton_ (WA for short) over $\Sigma$ and $\mathbb{S}$ is a tuple
$\mathcal{A}=(Q,\Sigma,\\{M_{a}\\}_{a\in\Sigma},I,F)$ where $Q$ is a finite
set of states, $\\{M_{a}\\}_{a\in\Sigma}$ is a set of matrices such that
$M_{a}\in\mathbb{S}^{Q\times Q}$ and $I,F\in\mathbb{S}^{Q}$ are the initial
and the final vectors, respectively [Sak09, DKV09]. We say that a state $q$ is
initial if $I(q)\neq\mathbb{0}$ and accepting if $F(q)\neq\mathbb{0}$. We say
that $(p,a,s,q)$ is a transition, where $M_{a}(p,q)=s$ and we write
$p\>\raisebox{-1.0pt}[10.0pt][0.0pt]{$\overset{a/s}{\underset{}{\raisebox{0.0pt}[3.0pt][0.0pt]{$\relbar\mspace{-8.0mu}\rightarrow$}}}$}\>q$.
Furthermore, we say that a run $\rho$ of $\mathcal{A}$ over a word
$w=a_{1}\ldots a_{n}$ is a sequence of transitions:
$\rho=q_{0}\>\raisebox{-1.0pt}[10.0pt][0.0pt]{$\overset{a_{1}/s_{1}}{\underset{}{\raisebox{0.0pt}[3.0pt][0.0pt]{$\relbar\mspace{-8.0mu}\rightarrow$}}}$}\>q_{1}\>\raisebox{-1.0pt}[10.0pt][0.0pt]{$\overset{a_{2}/s_{2}}{\underset{}{\raisebox{0.0pt}[3.0pt][0.0pt]{$\relbar\mspace{-8.0mu}\rightarrow$}}}$}\>\cdots\>\raisebox{-1.0pt}[10.0pt][0.0pt]{$\overset{a_{n}/s_{n}}{\underset{}{\raisebox{0.0pt}[3.0pt][0.0pt]{$\relbar\mspace{-8.0mu}\rightarrow$}}}$}\>q_{n},$
where $s_{i}\neq\mathbb{0}$ for all $1\leq i\leq n$ and
$I(q_{0})\neq\mathbb{0}$. We refer to $q_{i}$ as the $i$-th state of the run
$\rho$. The run $\rho$ is accepting if $F(q_{n})\neq\mathbb{0}$, and the
weight of an accepting run $\rho$ is defined by
$|\rho|=I(q_{0})\odot(\bigodot_{i=1}^{n}s_{i})\odot F(q_{n}).$ We define
$\operatorname{Run}_{\mathcal{A}}(w)$ as the set of all accepting runs of
$\mathcal{A}$ over $w$. Finally, the output of $\mathcal{A}$ over a word $w$
is defined by ${{\llbracket{}{\mathcal{A}}\rrbracket}}(w)=I^{t}\cdot
M_{a_{1}}\cdot\ldots\cdot M_{a_{n}}\cdot
F=\bigoplus_{\rho\in\operatorname{Run}_{\mathcal{A}}(w)}|\rho|$ where $I^{t}$
is the transpose of $I$ and the sum is equal to $\mathbb{0}$ if
$\operatorname{Run}_{\mathcal{A}}(w)$ is empty. For a word $w=a_{1}\ldots
a_{n}$, by $M_{w}$ we denote $M_{a_{1}}\cdot\ldots\cdot M_{a_{n}}$, so that
${{\llbracket{}{\mathcal{A}}\rrbracket}}(w)=I^{t}\cdot M_{w}\cdot F$. Note
that $M_{w}(p,q)$ provides the cost of moving from state $p$ to state $q$
reading the word $w$. Functions defined by weighted automata are called
_recognisable functions_.

In this paper, we study the specification of functions from words to values,
namely, from $\Sigma^{*}$ to $\mathbb{S}$. We say that a function
$f:\Sigma^{*}\rightarrow\mathbb{S}$ is definable by a weighted automaton
$\mathcal{A}$ if $f(w)={{\llbracket{}{\mathcal{A}}\rrbracket}}(w)$ for all
$w\in\Sigma^{*}$.

A weighted automaton $\mathcal{A}$ is called _unambiguous_ (U-WA) if
$|\operatorname{Run}_{\mathcal{A}}(w)|\leq 1$ for every $w\in\Sigma^{*}$; and
$\mathcal{A}$ is called _finitely-ambiguous_ (FA-WA) if there exists a uniform
bound $N$ such that $|\operatorname{Run}_{\mathcal{A}}(w)|\leq N$ for every
$w\in\Sigma^{*}$ [Web94, KLMP04]. Furthermore, $\mathcal{A}$ is called
_polynomially-ambiguous_ (PA-WA) if the function
$|\operatorname{Run}_{\mathcal{A}}(w)|$ is bounded by a polynomial in the
length of $w$ [KL09]. We call the classes of functions definable by such
automata _unambiguously recognisable_ , _finite-ambiguously recognisable_ and
_polynomial-ambiguously recognisable_.

Note that every unambiguous WA over ${\rm Nature}_{\min,+}$ and ${\rm
Nature}_{\max,+}$ can be defined by a WA over the semiring ${\rm
Nature}_{+,\times}$ (recall that $\infty$ is in ${\rm Nature}_{+,\times}$).
Indeed, let $\mathcal{A}$ be an unambiguous WA over ${\rm Nature}_{\min,+}$
(or ${\rm Nature}_{\max,+}$). We define two copies of $\mathcal{A}$:
$\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ such that all previously
non-$\mathbb{0}$ transitions between the states inside each copy have weights
$1$. The initial vector is inherited from $\mathcal{A}$ in the copy
$\mathcal{A}_{1}$ and defined as $0$ for states in $\mathcal{A}_{2}$.
Conversely, the final vector is inherited from $\mathcal{A}$ in the copy
$\mathcal{A}_{2}$ and defined as $0$ for states in $\mathcal{A}_{1}$. Finally,
for every transition $(p,a,s,q)$ in $\mathcal{A}$ we add a transition
$(p_{1},a,s,q_{2})$, where $p_{1}$ is the copy of $p$ in $\mathcal{A}_{1}$ and
$q_{2}$ is the copy of $q$ in $\mathcal{A}_{2}$. Since $\mathcal{A}$ is
unambiguous it is easy to see that the construction works for words $w$ such
that $\mathcal{A}(w)\neq\infty$. Let $L$ be the language of the remaining
words. Then for $w\in L$ the new automaton outputs $0$ instead of $\infty$.
Since $L$ is regular it suffices to take a union with another weighted
automaton over ${\rm Nature}_{+,\times}$ that outputs $\infty$ for $w\in L$
and $0$ for $w\not\in L$.

Therefore, the class of unambiguously recognisable functions over ${\rm
Nature}_{\min,+}$ (and ${\rm Nature}_{\max,+}$) is included in the class of
recognisable functions over ${\rm Nature}_{+,\times}$. The inclusions are
strict since recognisable functions over ${\rm Nature}_{\min,+}$ (and ${\rm
Nature}_{\max,+}$) are always bounded by a linear function in the size of the
word, and it is easy to define the function $f(w)=2^{|w|}$ over ${\rm
Nature}_{+,\times}$. Below, we give several examples of functions defined by
WA over ${\rm Nature}_{+,\times}$ and ${\rm Nature}_{\min,+}$ that will be
used in paper. Recall that in the latter semiring $\mathbb{0}=\infty$ and
$\odot=+$. Transitions
$p\>\raisebox{-1.0pt}[10.0pt][0.0pt]{$\overset{a/s}{\underset{}{\raisebox{0.0pt}[3.0pt][0.0pt]{$\relbar\mspace{-8.0mu}\rightarrow$}}}$}\>q$,
where $s=\mathbb{0}$, are omitted.

$b\ /\ 0$$\begin{array}[]{c}a\ /\ 0\\\ b\ /\
0\end{array}$$\begin{array}[]{c}a\ /\ 1\end{array}$$\mathcal{W}_{1}$ over
${\rm Nature}_{\min,+}$$\infty$$a\ /\ 1$$b\ /\ 0$$\begin{array}[]{c}a\ /\ 1\\\
b\ /\ 1\end{array}$$\begin{array}[]{c}a\ /\
1\end{array}$$\mathcal{W}_{1}^{\prime}$ over ${\rm
Nature}_{+,\times}$$\begin{array}[]{c}a\ /\ 1\\\ b\ /\
0\end{array}$$\begin{array}[]{c}a\ /\ 0\\\ b\ /\
1\end{array}$$\mathcal{W}_{2}$ over ${\rm
Nature}_{\min,+}$$\begin{array}[]{c}b\ /\ 1\end{array}$$a,b\ /\ 0$$a,b\ /\
0$$b\ /\ 1$$a\ /\ 0$$a\ /\ 0$$\mathcal{W}_{4}$ over ${\rm
Nature}_{\min,+}$$\begin{array}[]{c}a\ /\ 1\\\ b\ /\
0\end{array}$$\begin{array}[]{c}a\ /\ 0\\\ b\ /\
1\end{array}$$\begin{array}[]{c}a\ /\ 0\\\ b\ /\
0\end{array}$$\mathcal{W}_{3}$ over ${\rm
Nature}_{\min,+}$$\begin{array}[]{c}a\ /\ 1\\\ b\ /\
0\end{array}$$\begin{array}[]{c}\\#\ /\ 0\end{array}$$\begin{array}[]{c}a\ /\
0\\\ b\ /\ 1\end{array}$$\\#\ /\ 0$$\\#\ /\ 0$$\begin{array}[]{c}a\ /\ 0\\\ b\
/\ 1\end{array}$$\begin{array}[]{c}a\ /\ 1\\\ b\ /\
0\end{array}$$\mathcal{W}_{5}$ over ${\rm Nature}_{\min,+}$

Figure 1. Examples of weighted automata. For WA over ${\rm Nature}_{\min,+}$
the initial and accepting states are labelled by 0 in the corresponding
vector, and $\infty$ otherwise. Similarly, for WA over ${\rm
Nature}_{+,\times}$ the initial and accepting states are labelled by 1 in the
corresponding vector, and $0$ otherwise; except for the initial state labeled
$\infty$.

Let $\Sigma=\\{a,b\\}$. Consider the function $f_{1}$ that for given word
$w\in\Sigma^{*}$ outputs the length of the biggest suffix of $a$’s (and
$\infty$ for the empty word). This is defined by the WA $\mathcal{W}_{1}$ over
${\rm Nature}_{\min,+}$ in Figure 1. One can easily check that
$\mathcal{W}_{1}$ is unambiguous, hence $f_{1}$ is an unambiguously
recognisable function over ${\rm Nature}_{\min,+}$. In Figure 1, the WA
$\mathcal{W}_{1}^{\prime}$ over ${\rm Nature}_{+,\times}$ also defines
$f_{1}$.

Let $\Sigma=\\{a,b\\}$. Consider the function $f_{2}$ that for a given word
$w\in\Sigma^{*}$ outputs $\min\\{|w|_{a},|w|_{b}\\}$, namely, counts the
number of each letter and returns the minimum. This is defined by the WA
$\mathcal{W}_{2}$ in Figure 1. The WA $\mathcal{W}_{2}$ is finitely-ambiguous,
hence $f_{2}$ is a finite-ambiguously recognisable function.

Let $\Sigma=\\{a,b\\}$. Consider the function $f_{3}$ that for a given word
$w=a_{1}\ldots a_{n}\in\Sigma^{*}$ outputs $\min_{0\leq i\leq
n}\\{|a_{1}\ldots a_{i}|_{a}+|a_{i+1}\ldots a_{n}|_{b}\\}$. This is defined by
the WA $\mathcal{W}_{3}$ in Figure 1. This WA is polynomially-ambiguous, hence
$f_{3}$ is a polynomial-ambiguously recognisable function.

Let $\Sigma=\\{a,b\\}$. Consider the function $f_{4}$ that for a given word
$w\in\Sigma^{*}$ computes the shortest subword of $b$’s (if there is none it
outputs $+\infty)$. This is defined by $\mathcal{W}_{4}$ in Figure 1. The WA
is polynomially-ambiguous, hence $f_{4}$ belongs to polynomially-ambiguous
functions.

Let $\Sigma=\\{a,b,\\#\\}$. Consider the function $f_{5}$ such that, for every
$w\in\Sigma^{*}$ of the form $w_{0}\\#w_{1}\\#\ldots\\#w_{n}$ with
$w_{i}\in\\{a,b\\}^{*}$, it computes $\min\\{|w_{i}|_{a},|w_{i}|_{b}\\}$ for
each subword $w_{i}$ and then it sums these values over all subwords $w_{i}$,
that is, $f_{5}(w)=\sum_{i=0}^{n}\min\\{|w_{i}|_{a},|w_{i}|_{b}\\}$. This
function is defined by the WA $\mathcal{W}_{5}$ in Figure 1. Given that this
WA has an exponential number of runs, the function $f_{5}$ is a recognisable
function, but not necessarily a polynomial-ambiguously recognisable function.

We will also discuss variants of the functions $f_{1}$, $f_{2}$, $f_{3}$,
$f_{4}$ and $f_{5}$ in the max-plus semiring in Section 6.

We assume that our weighted automata are always trim, namely, all their states
are reachable from some initial state (accessible in short) and they can reach
some final state (co-accessible in short). Verifying if a state is accessible
or co-accessible is reduced to a reachability test in the transition graph
[Pap93] and this can be done in NLogSpace. Thus, we can assume without loss of
generality that all our automata are trimmed.

###  2.2. Finite monoids and idempotents

We say that a monoid is finite if the set of its elements is finite. Let
$\mathbb{M}=(M,\otimes,\mathbb{1})$ be a finite monoid. We say that
$\iota\in\mathbb{M}$ is an idempotent if $\iota\otimes\iota=\iota$. The
following lemma is a standard result for finite monoids and idempotents (see
e.g. [Pin10]).

######  Lemma 1.

Let $\mathbb{M}$ be a finite monoid. There exists some $N>0$ such that every
sequence $m_{1},\ldots,m_{n}$, with $m_{i}\in\mathbb{M}$ and $n\geq N$, can be
factorised as:

$(m_{1}\otimes\ldots\otimes m_{i})\otimes(m_{i+1}\otimes\ldots\otimes
m_{j})\otimes(m_{j+1}\ldots\otimes m_{n})\,,$

where $i<j\leq n$ and $(m_{i+1}\otimes\ldots\otimes m_{j})$ is an idempotent.

We will mainly use two finite monoids of matrices, $\mathbb{B}^{Q\times Q}$
and $\mathbb{B}_{\infty}^{Q\times Q}$. We define abstractions, i.e.
homomorphisms of ${\rm Nature}_{\min,+}^{Q\times Q}$ to $\mathbb{B}^{Q\times
Q}$, ${\rm Nature}_{\max,+}^{Q\times Q}$ to $\mathbb{B}^{Q\times Q}$, and
${\rm Nature}_{+,\times}^{Q\times Q}$ to $\mathbb{B}_{\infty}^{Q\times Q}$.
They are obtained from the homomorphisms defined on elements of the matrices,
namely $h_{1}:{\rm Nature}_{\min,+}\to\mathbb{B}$, $h_{2}:{\rm
Nature}_{\max,+}\to\mathbb{B}$, and $h_{3}:{\rm
Nature}_{+,\times}\to\mathbb{B}_{\infty}$, by setting $h_{1}(m)=0$ iff
$m=+\infty$; $h_{2}(m)=0$ iff $m=-\infty$; $h_{3}(0)=0$,
$h_{3}(\infty)=\infty$, and $h_{3}(m)=1$ if $m\not=0,\infty$. For matrices
$M_{1}\in{\rm Nature}_{\min,+}^{Q\times Q}$, $M_{2}\in{\rm
Nature}_{\max,+}^{Q\times Q}$, or $M_{3}\in{\rm Nature}_{+,\times}^{Q\times
Q}$ we denote by $\bar{M_{1}}=h_{1}(M_{1})$, $\bar{M_{2}}=h_{2}(M_{2})$, or
$\bar{M_{3}}=h_{3}(M_{3})$ their abstractions in $\mathbb{B}^{Q\times Q}$ or
$\mathbb{B}_{\infty}^{Q\times Q}$. By abuse of language we say that a matrix
$M$ from ${\rm Nature}_{\min,+}^{Q\times Q}$, ${\rm Nature}_{\max,+}^{Q\times
Q}$ or ${\rm Nature}_{+,\times}^{Q\times Q}$ is _idempotent_ , if its
abstraction $\bar{M}$ is idempotent.

##  3\. Recognisable functions over ${\rm Nature}_{+,\times}$

In this section we consider recognisable functions over ${\rm
Nature}_{+,\times}$. As a corollary of the pumping lemma we show that FA-WA
are strictly more expressive than U-WA over ${\rm Nature}_{\min,+}$ and ${\rm
Nature}_{\max,+}$ (Example 3 and beginning of Section 6). Moreover, this shows
that there are finite-ambiguously recognisable functions over ${\rm
Nature}_{\min,+}$ and ${\rm Nature}_{\max,+}$ that cannot be defined by any
recognisable function over ${\rm Nature}_{+,\times}$.

We introduce some notation to simplify the presentation. Given $u\cdot v\cdot
w=\hat{u}\cdot\hat{v}\cdot\hat{w}$, where
$u,v,w,\hat{u},\hat{v},\hat{w}\in\Sigma^{*}$, we say that
$\hat{u}\cdot\underline{\hat{v}}\cdot\hat{w}$ is a _refinement_ of
$u\cdot\underline{v}\cdot w$ if there exist $u^{\prime},w^{\prime}$ such that
$u\cdot u^{\prime}=\hat{u}$, $w^{\prime}\cdot w=\hat{w}$,
$u^{\prime}\cdot\hat{v}\cdot w^{\prime}=v$, and $\hat{v}\neq\epsilon$. We
underline the infixes $v$ and $\hat{v}$ to emphasise the refined part.

######  Theorem 2 (Pumping Lemma for recognisable functions over ${\rm
Nature}_{+,\times}$).

Let $f:\Sigma^{*}\to\mathbb{N}\cup\\{\infty\\}$ be a recognisable function
over ${\rm Nature}_{+,\times}$. There exists $N$ such that for all words of
the form $u\cdot v\cdot w\in\Sigma^{*}$ with $|v|\geq N$, $v\neq\epsilon$,
there exists a refinement $\hat{u}\cdot\underline{\hat{v}}\cdot\hat{w}$ of
$u\cdot\underline{v}\cdot w$ such that one of the following two conditions
holds:

  * •

$f(\hat{u}\cdot\underline{\hat{v}}^{i}\cdot\hat{w})\ =\
f(\hat{u}\cdot\underline{\hat{v}}^{i+1}\cdot\hat{w})$ for every $i\geq N$.

  * •

$f(\hat{u}\cdot\underline{\hat{v}}^{i}\cdot\hat{w})\ <\
f(\hat{u}\cdot\underline{\hat{v}}^{i+1}\cdot\hat{w})$ for every $i\geq N$.

Before going into the details of the proof let us show how to use the lemma.

We show that $f_{2}$ from Example 2.1 is not definable by any WA over ${\rm
Nature}_{+,\times}$. Indeed, suppose it is definable and fix $N$ from Theorem
2. Consider the word $w=a^{(N+1)^{2}}\underline{b^{N}}$ and notice that
$f_{2}(w)=N$. By refining $w$ we get
$\hat{u}\cdot\underline{\hat{v}}\cdot\hat{w}=a^{(N+1)^{2}}b^{n}\underline{b^{m}}b^{l}$
for some $n,m,l$ such that $1\leq m\leq N$ and $n+m+l=N$. Since $n+m\cdot
N+l<n+m\cdot(N+1)+l<(N+1)^{2}$ it must be the case that
$f_{2}(\hat{u}\cdot\underline{\hat{v}}^{i}\cdot\hat{w})<f_{2}(\hat{u}\cdot\underline{\hat{v}}^{i+1}\cdot\hat{w})$
for all $i\geq N$. However,
$f_{2}(\hat{u}\cdot\underline{\hat{v}}^{i}\cdot\hat{w})=(N+1)^{2}$ for $i$
sufficiently large, which is a contradiction.

On the other hand, the function $f_{1}$ from Example 2.1 satisfies Theorem 2.
Consider a word $u\cdot\underline{v}\cdot w\in\Sigma^{*}$ and its refinement
$\hat{u}\cdot\underline{\hat{v}}\cdot\hat{w}$. If $\hat{w}$ or $\hat{v}$
contain $b$ then $f(\hat{u}\cdot\underline{\hat{v}}^{i}\cdot\hat{w})\ =\
f(\hat{u}\cdot\underline{\hat{v}}^{i+1}\cdot\hat{w})$ because the suffix of
$a$’s remains the same. Otherwise,
$f(\hat{u}\cdot\underline{\hat{v}}^{i}\cdot\hat{w})\ <\
f(\hat{u}\cdot\underline{\hat{v}}^{i+1}\cdot\hat{w})$ since the suffix of
$a$’s increases when pumping. Moreover, it is straightforward to generalise
this argument and prove Theorem 2 for all U-WA over ${\rm Nature}_{\min,+}$.

To prove Theorem 2 we use the following definitions. For a matrix $M\in{\rm
Nature}_{+,\times}^{Q\times Q}$ recall that $\bar{M}$ is its homomorphic image
in $\mathbb{B}_{\infty}^{Q\times Q}$ (see Section 2.2). We write that $M$ and
$N$ in ${\rm Nature}_{+,\times}^{Q\times Q}$ are equivalent, denoted
$M\equiv_{\mathbb{B}_{\infty}}N$, iff $\bar{M}=\bar{N}$. We also extend the
homomorphic image and equivalence relation from matrices to vectors. We say
that $D\in{\rm Nature}_{+,\times}^{Q\times Q}$ is an _idempotent_ if $\bar{D}$
is an idempotent in the finite monoid $\mathbb{B}_{\infty}^{Q\times Q}$.

######  Lemma 3.

If $M\equiv_{\mathbb{B}_{\infty}}N$, then $x^{T}\cdot M\cdot y>0$ if and only
if $x^{T}\cdot N\cdot y>0$ for every $x,y\in{\rm Nature}_{+,\times}^{Q}$.

######  Proof 3.1.

Suppose that $x^{T}\cdot M\cdot y>0$. By definition $x^{T}\cdot M\cdot
y=\sum_{p,q}x(p)\cdot M(p,q)\cdot y(q)$. Then there exist $p,q\in Q$ such that
$x(p)\cdot M(p,q)\cdot y(q)>0$ and, in particular, $M(p,q)>0$. Given that
$M\equiv_{\mathbb{B}_{\infty}}N$ we conclude $N(p,q)>0$ and $x(p)\cdot
N(p,q)\cdot y(q)>0$, which proves $x^{T}\cdot N\cdot y>0$.

######  Proof 3.2 (Proof of Theorem 2).

Let $\mathcal{A}=(Q,\Sigma,\\{M_{a}\\}_{a\in\Sigma},I,F)$ be a WA over ${\rm
Nature}_{+,\times}$ such that $f={\llbracket{}{\mathcal{A}}\rrbracket}$.
Without loss of generality, we assume that $I(q)\neq\infty$ and
$M_{a}(p,q)\neq\infty$ for every $p,q\in Q$ and $a\in\Sigma$, namely, $\infty$
can only appear in the final vector $F$. Indeed, if $\infty$ is used in $I$ or
some $M_{a}$, we can construct two weighted automata
$\mathcal{A}^{\prime},\mathcal{A}^{\infty}$ such that $\mathcal{A}^{\prime}$
is the same as $\mathcal{A}$ but each $\infty$-initial state or each
$\infty$-transition is replaced with $0$, and $\mathcal{A}^{\infty}$ outputs
$\infty$ if there exists some run in $\mathcal{A}$ that outputs $\infty$ and 0
otherwise. Note that $\mathcal{A}^{\prime}$ has no $\infty$-transition or
$\infty$-initial state and $\mathcal{A}^{\infty}$ can be constructed in such a
way that only the final vector contains $\infty$-values. The disjoint union of
$\mathcal{A}^{\prime}$ and $\mathcal{A}^{\infty}$ is equivalent to
$\mathcal{A}$.

Let $N=\max\\{|Q|,K\\}$ where $K$ is the constant from Lemma 1 for the finite
monoid $\mathbb{B}_{\infty}^{Q\times Q}$. For every word $u\cdot v\cdot
w\in\Sigma^{*}$ such that $v=a_{1}\ldots a_{n}$ with $n\geq N$, consider the
output $I^{T}\cdot M_{u}\cdot M_{v}\cdot M_{w}\cdot F$ of $\mathcal{A}$ over
$u\cdot v\cdot w$. By Lemma 1, there exists a factorisation of the form:

$M_{v}=(M_{a_{1}}\cdot\ldots\cdot M_{a_{i}})\cdot(M_{a_{i+1}}\cdot\cdots\cdot
M_{a_{j}})\cdot(M_{a_{j+1}}\cdot\ldots\cdot M_{a_{n}})$

for some $i<j$ where $M_{a_{i+1}\dots a_{j}}$ is an idempotent (i.e.,
$\bar{M}_{a_{i+1}\dots a_{j}}$ is an idempotent). We define the refinement
$\hat{u}\cdot\underline{\hat{v}}\cdot\hat{w}$ of $u\cdot\underline{v}\cdot w$
such that $\hat{u}=u\cdot(a_{1}\ldots a_{i})$, $\hat{v}=a_{i+1}\ldots a_{j}$,
and $\hat{w}=(a_{j+1}\ldots a_{n})\cdot w$. Furthermore, define
$x^{T}=I^{T}\cdot M_{ua_{1}\dots a_{i}}$, $D=M_{a_{i+1}\dots a_{j}}$, and
$y=M_{a_{j+1}\dots a_{n}w}\cdot F$. Note that
$f(\hat{u}\cdot\hat{v}^{i}\cdot\hat{w})=x^{T}\cdot D^{i}\cdot y$ for every
$i\geq 0$ and $D$ is an idempotent (i.e., $\bar{D}$ is an idempotent). It
remains to show the following lemma.

######  Lemma 4.

For every idempotent $D\in{\rm Nature}_{+,\times}^{Q\times Q}$ and $x,y\in{\rm
Nature}_{+,\times}^{Q}$ where $D$ and $x$ do not contain $\infty$-values, one
of the conditions holds:

$\displaystyle x^{T}\cdot D^{i}\cdot y\;=\;x^{T}\cdot D^{i+1}\cdot
y\;\;\;\text{ for every }i\geq|Q|,\;\;\;\text{ or }$ (1) $\displaystyle
x^{T}\cdot D^{i}\cdot y\;<\;x^{T}\cdot D^{i+1}\cdot y\;\;\;\text{ for every
}i\geq|Q|.$ (2)

We start showing that Lemma 4 holds when $y=e_{p}$ for some $p\in Q$, where
$e_{p}(q)=1$ if $q=p$ and $0$ otherwise. Note that $z=\sum_{p\in Q}z(p)\cdot
e_{p}$ for every vector $z$.

We say that $p$ is _$D$ -stable_ (or just _stable_) if $D(p,p)>0$. Note that
if $p$ is stable, then $D^{i}(p,p)>0$ for every $i>0$ (recall that $D$ is
idempotent). Furthermore, $D\cdot e_{p}=e_{p}+z$ for some $z\in{\rm
Nature}_{+,\times}^{Q}$. Suppose that $p$ is stable and $D\cdot e_{p}=e_{p}+z$
for some vector $z$. Then for $i>0$:

$\begin{array}[]{rclrcl}x^{T}\cdot D^{i+1}\cdot e_{p}&=&x^{T}\cdot
D^{i}\cdot(e_{p}+z)&=&x^{T}\cdot D^{i}\cdot e_{p}+x^{T}\cdot D^{i}\cdot
z\end{array}$

Given that $D$ is idempotent and $D^{i}\equiv_{\mathbb{B}_{\infty}}D$, by
Lemma 3 we have that $x^{T}\cdot D^{i}\cdot z>0$ if, and only if, $x^{T}\cdot
D\cdot z>0$. Therefore, if $x^{T}\cdot D\cdot z>0$, we get that $x^{T}\cdot
D^{i}\cdot e_{p}<x^{T}\cdot D^{i+1}\cdot e_{p}$ for every $i>0$, in
particular, for every $i\geq|Q|$. Otherwise, $x^{T}\cdot D\cdot z=0$ and
$x^{T}\cdot D^{i}\cdot e_{p}=x^{T}\cdot D^{i+1}\cdot e_{p}$ for every $i>0$,
in particular, for every $i\geq|Q|$.

Consider the relation $\preceq_{D}\mathop{\subseteq}Q\times Q$ such that
$p\preceq_{D}q$ if $p=q$ or $D(p,q)>0$. Let $P\subseteq Q$ be the set of all
non-stable states in $D$. One can easily check that $\preceq_{D}$ restricted
to $P$ forms a partial order, namely, that $\preceq_{D}$ is reflexive,
antisymmetric, and transitive. Indeed, transitivity holds because $D$ is
idempotent. To prove antisymmetry, note that for every non-stable states $p$
and $q$, if $p\preceq_{D}q$, $q\preceq_{D}p$ and $p\neq q$ hold, then
$D(p,p)>0$. This is a contradiction since $p$ is non-stable.

Since $\preceq_{D}$ is a partial order, we prove the lemma for $y=e_{p}$ by
induction over $\preceq_{D}$. Formally, we strengthen the inductive hypothesis
such that conditions (1) and (2) hold for every $i\geq N_{q}$, where
$N_{q}=|\\{q^{\prime}\in P\ |\ q^{\prime}\preceq_{D}q\\}|$ (notice that
$N_{q}\leq|Q|$ for every $q$). The base case is for $N_{p}=1$, which means
that $p$ is stable. For the inductive case suppose that $N_{p}>1$. Then

$x^{T}\cdot D^{i+1}\cdot e_{p}\ =\ x^{T}\cdot D^{i}\cdot(c_{1}\cdot
e_{q_{1}}+\ldots+c_{k}\cdot e_{q_{k}})\ =\ c_{1}(x^{T}\cdot D^{i}\cdot
e_{q_{1}})+\ldots+c_{k}(x^{T}\cdot D^{i}\cdot e_{q_{k}})$

for pairwise different states $q_{1},\ldots,q_{k}$ and positive values
$c_{1},\ldots,c_{k}\in{\rm Nature}$ such that $q_{j}$ is either stable or
$q_{j}\prec_{D}p$. Thus all states $q_{1},\ldots,q_{k}$ satisfy our inductive
hypothesis.

Consider the partition of $q_{1},\ldots,q_{k}$ into sets $C_{=}$ and $C_{<}$
such that $C_{=}$ and $C_{<}$ satisfy condition (1) and (2), respectively. If
$C_{<}=\emptyset$, then for every $i\geq N_{p}$ we have:

$\displaystyle x^{T}\cdot D^{i+1}\cdot e_{p}\;\;$
$\displaystyle=\;\;c_{1}(x^{T}\cdot D^{i}\cdot
e_{q_{1}})+\ldots+c_{k}(x^{T}\cdot D^{i}\cdot e_{q_{k}})$
$\displaystyle=\;\;c_{1}(x^{T}\cdot D^{i-1}\cdot
e_{q_{1}})+\ldots+c_{k}(x^{T}\cdot D^{i-1}\cdot e_{q_{k}})$
$\displaystyle=\;\;x^{T}\cdot D^{i}\cdot e_{p}.$ (3)

Note that $x^{T}\cdot D^{i}\cdot e_{q_{j}}=x^{T}\cdot D^{i-1}\cdot e_{q_{j}}$
holds by the inductive hypothesis and because $N_{p}>N_{q_{j}}$ for every
$q_{j}$. Suppose otherwise, that $C_{<}\neq\emptyset$ and there exists a state
$q_{j}$ that satisfies $x^{T}\cdot D^{i}\cdot e_{q_{j}}<x^{T}\cdot
D^{i+1}\cdot e_{q_{j}}$ for every $i\geq N_{q_{j}}$. Then it is
straightforward that equality (3) becomes a strict inequality and condition
(2) holds.

We have shown that either (1) or (2) holds for $y=e_{p}$. It remains to extend
this to any vector $y\in{\rm Nature}_{+,\times}^{Q}$ (possibly with $\infty$).
Note that

$x^{T}\cdot D^{i+1}\cdot y\ =\ y(q_{1})\cdot(x^{T}\cdot D^{i+1}\cdot
e_{q_{1}})+\ldots+y(q_{k})\cdot(x^{T}\cdot D^{i+1}\cdot e_{q_{k}})$

for some states $q_{1},\ldots,q_{k}$ such that $y(q_{j})>0$ for every $j\leq
k$. We consider two cases. First, if there exists $j$ such that
$y(q_{j})=\infty$ and $x^{T}\cdot D^{i}\cdot e_{q_{j}}>0$ for $i\geq N$, then
$x^{T}\cdot D^{i}\cdot y=\infty$ for every $i\geq 0$. Thus, $x^{T}\cdot
D^{i}\cdot y$ satisfies condition (1). Second, suppose that for every $j$ we
have $y(q_{j})\neq\infty$ or $x^{T}\cdot D^{i}\cdot e_{q_{j}}=0$ for $i\geq
N$. It suffices to consider the case when $y(q_{j})\neq\infty$ for all $j$.
Then if some $x^{T}\cdot D^{i}\cdot e_{q_{j}}$ satisfies condition (2) we have
that $x^{T}\cdot D^{i}\cdot y$ satisfies condition (2). Conversely, if every
$x^{T}\cdot D^{i}\cdot e_{q_{j}}$ satisfies condition (1) we have that
$x^{T}\cdot D^{i}\cdot y$ satisfies condition (1).

One could try to simplify Theorem 2 changing the condition $i\geq N$ to $i\geq
0$. Unfortunately, we do not know if the theorem would remain true. A naive
approach would be to use a generalisation of Lemma 1, but intuitively, the
behaviour of non-stable states is problematic. We conclude with the following
remarks, straightforward from the proof. We will use them in Section 4.

######  Remark 5.

Changing $y$ to $y^{\prime}$ such that
$y\equiv_{\mathbb{B}_{\infty}}y^{\prime}$ does not influence whether condition
(1) or condition (2) holds in Lemma 4 (notice that here we need that the
abstractions have values in $\mathbb{B}_{\infty}$ not in $\mathbb{B}$).
Similarly, changing $x$ to $x^{\prime}$ such that
$x\equiv_{\mathbb{B}_{\infty}}x^{\prime}$ does not influence whether condition
(1) or (2) holds.

######  Remark 6.

The constant $N$ and the refinement of $w$ depend only on the finite monoid
$\mathbb{B}_{\infty}^{Q\times Q}$. In particular they are independent from the
initial and final vectors $I$ and $F$.

##  4\. Finite-min recognisable functions

In this section we focus on recognisable functions over ${\rm
Nature}_{+,\times}$ with some $\min$ operations allowed. Formally, we say that
$f:\Sigma^{*}\rightarrow\mathbb{N}\cup\\{\infty\\}$ is a finite-min
recognisable function, if there exist recognisable functions
$f_{1},\ldots,f_{m}$ over ${\rm Nature}_{+,\times}$ such that
$f(w)=\min\\{f_{1}(w),\ldots,f_{m}(w)\\}$. It is known that over ${\rm
Nature}_{\min,+}$, FA-WA are equivalent to a finite minimum of U-WA [Web94],
hence the functions defined by FA-WA are included in the class of finite-min
recognisable functions. As a corollary of the pumping lemma in this section we
show that PA-WA are strictly more expressive than FA-WA over ${\rm
Nature}_{\min,+}$ (Example 4 and Example 4).

We start by introducing some notation. Generalising the notation used in the
previous section, we define for $n>0$ an _$n$ -pumping representation_ for a
word $w\in\Sigma^{*}$ as a factorisation of the form

$w=u_{0}\cdot\underline{v_{1}}\cdot u_{1}\cdot\underline{v_{2}}\cdot\ldots
u_{n-1}\cdot\underline{v_{n}}\cdot u_{n},$

where $w=u_{0}\cdot v_{1}\cdot u_{1}\cdot v_{2}\cdot\ldots v_{n}\cdot u_{n}$
and $v_{k}\neq\epsilon$ for all $k$. A refinement of an $n$-pumping
representation for $w$ is given by

$w=u_{0}^{\prime}\cdot\underline{y_{1}}\cdot
u_{1}^{\prime}\cdot\underline{y_{2}}\cdot\ldots
u_{n-1}^{\prime}\cdot\underline{y_{n}}\cdot u_{n}^{\prime},$

if $v_{k}=x_{k}\cdot y_{k}\cdot z_{k}$, $u_{k}^{\prime}=z_{k}\cdot u_{k}\cdot
x_{k+1}$; where $z_{0}=x_{n+1}=\epsilon$ and $y_{k}\neq\epsilon$ for every
$k$. Let $S\subseteq\\{1,\ldots,n\\}$ such that $S\neq\emptyset$. Let
$\underline{y_{k}}$ be a factor of the refined $n$-pumping representation of
$w$. By $\underline{y_{k}}(S,i)$ we denote the word $y_{k}^{i}$ if $k\in S$
and $y_{k}$ otherwise. By $w(S,i)$ we denote the word

$w=u^{\prime}_{0}\cdot\underline{y_{1}}(S,i)\cdot
u^{\prime}_{1}\cdot\underline{y_{2}}(S,i)\cdot\ldots
u^{\prime}_{n-1}\cdot\underline{y_{n}}(S,i)\cdot u^{\prime}_{n}.$

In other words, in $w(S,i)$ we pump $i$ times each factor $y_{k}$, for all
$k\in S$. Note that the pumping always refers to the _refinement_ of the
$n$-pumping representation.

######  Theorem 7 (Pumping Lemma for finite-min recognisable functions).

Let $f:\Sigma^{*}\to\mathbb{N}\cup\\{\infty\\}$ be a finite-min recognisable
function. There exists $N$ such that for every $n$-pumping representation

$w=u_{0}\cdot\underline{v_{1}}\cdot u_{1}\cdot\underline{v_{2}}\cdot\ldots
u_{n-1}\cdot\underline{v_{n}}\cdot u_{n},$

where $|v_{i}|\geq N$ for all $i$, there exists a refinement

$w=u_{0}^{\prime}\cdot\underline{y_{1}}\cdot
u_{1}^{\prime}\cdot\underline{y_{2}}\cdot\ldots
u_{n-1}^{\prime}\cdot\underline{y_{n}}\cdot u_{n}^{\prime},$

such that for every sequence of non-empty, pairwise different subsets
$S_{1},\dots,S_{k}\subseteq\\{1,\ldots,n\\}$ with $k\geq N$ one of the
following holds:

  * •

there exists $j$ such that $f(w(S_{j},i))<f(w(S_{j},i+1))$ for all but
finitely many $i$;

  * •

there exist $j_{1}\neq j_{2}$ such that $f(w(S_{j_{1}}\cup
S_{j_{2}},i))=f(w(S_{j_{1}}\cup S_{j_{2}},i+1))$ for all but finitely many
$i$.

Before proving Theorem 7, we show how to use it with two examples.

We show that $f_{3}$ from Example 2.1 is not definable by finite-min
recognisable functions. Indeed, fix $N$ from Theorem 7 and consider the
$n$-pumping representation $w=(\underline{b^{N}}\cdot\underline{a^{N}})^{N}$.
We index each pumping factor with a pair $(s,j)$, where $j\leq N$ denotes the
block $b^{N}a^{N}$, and $s\in\\{1,2\\}$ denotes the factor in the block.
First, notice that $f_{3}(w)=N\cdot(N-1)$ because runs minimising the value
for $\mathcal{W}_{3}$ change the state after reading the last $b$ in one of
the blocks. We define the sets $S_{j}=\\{(1,j),(2,j)\\}$ for
$j\in\\{1,\ldots,N\\}$. Clearly $f_{3}(w(S_{j},i))=f_{3}(w)$ for all $j$ and
$i$, because the run minimising the value changes the state after the last $b$
in the $j$-th block. On the other hand $f_{3}(w(S_{j_{1}}\cup
S_{j_{2}},i))<f_{3}(w(S_{j_{1}}\cup S_{j_{2}},i+1))$ for all $i$ and
$j_{1}\neq j_{2}$. Hence $f_{3}$ does not satisfy the pumping lemma for
finite-min recognisable functions.

We show that $f_{4}$ from Example 2.1 is not definable by finite-min
recognisable functions. Indeed, fix $N$ from Theorem 7. Consider the
$N$-pumping representation $w=(\underline{b^{N}}a)^{N}$. Then by definition
$f_{4}(w)=N$. In the refinement all pumping parts will be of the form $b^{n}$
for $1\leq n\leq N$. We define the sets
$S_{j}=\\{1,\ldots,N\\}\setminus\\{j\\}$ for all $1\leq i\leq N$. Clearly
$f_{4}(w(S_{j},i))=N$ for all $j$ and $i$. On the other hand
$f_{4}(w(S_{j_{1}}\cup S_{j_{2}},i))<f_{4}(w(S_{j_{1}}\cup S_{j_{2}},i+1))$
for all $i$ and $j_{1}\neq j_{2}$. Hence $f_{4}$ does not satisfy the pumping
lemma for finite-min recognisable functions.

######  Proof 4.1 (Proof of Theorem 7).

Let $f_{1},\ldots,f_{m}$ be recognisable functions over ${\rm
Nature}_{+,\times}$ such that $f(w)=\min\\{f_{1}(w),\ldots,f_{m}(w)\\}$ for
every $w$. Furthermore, consider
$\mathcal{A}_{j}=(Q_{j},\Sigma,\\{M_{j,a}\\}_{a\in\Sigma},I_{j},F_{j})$ the
corresponding WA for $f_{j}$. Let $Q=\bigcup_{j}Q_{j}$ (we assume that
$Q_{1},\ldots,Q_{m}$ are pairwise disjoint) and consider the set of matrices
$\\{U_{a}\\}_{a\in\Sigma}$ where $U_{a}\in{\rm Nature}_{+,\times}^{Q\times Q}$
such that $U_{a}(p,q)=M_{j,a}(p,q)$ whenever $p,q\in Q_{j}$ and $0$ otherwise.
Then $f_{j}(w)=(I_{j}^{\prime})^{t}\cdot U_{w}\cdot F_{j}^{\prime}$ for every
$j$ and $w\in\Sigma^{*}$ where $I_{j}^{\prime}$ and $F_{j}^{\prime}$ are the
extensions of $I_{j}$ and $F_{j}$ from $Q_{j}$ into $Q$ such that
$I_{j}^{\prime}(q)=I_{j}(q)$ and $F_{j}^{\prime}(q)=F_{j}(q)$ whenever $q\in
Q_{j}$ and $0$ otherwise. Notice that $\\{U_{a}\\}_{a\in\Sigma}$ synchronise
the behaviour of $f_{1},\ldots,f_{m}$ in a single set of matrices and project
the output of $f_{j}$ with $I_{j}^{\prime}$ and $F_{j}^{\prime}$. Let
$N=\max\\{K,m+1\\}$ such that $K$ is the constant from Lemma 1 applied to
$\mathbb{B}_{\infty}^{Q\times Q}$.

Let $w=u_{0}\cdot\underline{v_{1}}\cdot u_{1}\cdot\underline{v_{2}}\cdot\ldots
u_{n-1}\cdot\underline{v_{n}}\cdot u_{n}.$ be an $n$-pumping representation as
in the statement of the theorem. For every $i$ we apply Theorem 2 to $u_{\leq
i}\cdot\underline{v_{i}}\cdot t_{\geq i}$, where $u_{\leq i}=u_{0}\cdot
v_{1}\cdot\ldots u_{i-1}$ and $t_{\geq i}=u_{i}\cdot v_{i+1}\cdot\ldots
u_{n}$, and $\\{U_{a}\\}_{a\in\Sigma}$ (recall that the refinement of $u_{\leq
i}\cdot\underline{v_{i}}\cdot t_{\geq i}$ depends only on
$\\{U_{a}\\}_{a\in\Sigma}$, and not on the initial or final vector, see Remark
6). As in the proof of Theorem 2 we obtain a refinement

$w\ =\ u_{0}^{\prime}\cdot\underline{y_{1}}\cdot
u_{1}^{\prime}\cdot\underline{y_{2}}\cdot\ldots
u_{n-1}^{\prime}\cdot\underline{y_{n}}\cdot u_{n}^{\prime},$

where each $y_{i}$ is idempotent w.r.t. $\\{U_{a}\\}_{a\in\Sigma}$.

Note that the refinement is the same for each function $f_{j}$. Therefore, we
obtain

$f_{j}(w)\ =\ (I_{j}^{\prime})^{t}\cdot U_{u_{0}^{\prime}}\cdot
D_{1}\cdot\ldots\cdot U_{u_{n-1}^{\prime}}\cdot D_{n}\cdot
U_{u_{n}^{\prime}}\cdot F_{j}^{\prime}$

where all $D_{i}=U_{y_{i}}$ are idempotents.

######  Lemma 8.

Let $S\subseteq\\{1,\ldots,n\\}$ be a non-empty set and fix one function
$f_{j}$. Then $f_{j}(w(S,i))<f_{j}(w(S,i+1))$ for every $i\geq N$ iff there
exists $k\in S$ such that $f_{j}(w(\\{k\\},i))<f_{j}(w(\\{k\\},i+1))$ for
every $i\geq N$.

######  Proof 4.2.

By definition $f_{j}(w(S,i))=(I_{j}^{\prime})^{t}\cdot U_{u_{0}^{\prime}}\cdot
D_{1}^{s_{1}}\cdot\ldots\cdot U_{u_{n-1}^{\prime}}\cdot D_{n}^{s_{n}}\cdot
U_{u_{n}^{\prime}}\cdot F_{j}^{\prime}$ where $s_{k}=i$ if $k\in S$ and
$s_{k}=1$ otherwise. Since all $D_{i}$ are idempotents then for all $k$:

$\displaystyle(I_{j}^{\prime})^{t}\cdot U_{u_{0}^{\prime}}\cdot
D_{1}^{s_{1}}\cdot\ldots\cdot D_{k-1}^{s_{k-1}}\cdot U_{u_{k-1}^{\prime}}$
$\displaystyle\ \equiv_{\mathbb{B}_{\infty}}\ (I_{j}^{\prime})^{t}\cdot
U_{u_{0}^{\prime}}\cdot D_{1}\cdot\ldots\cdot D_{k-1}\cdot
U_{u_{k-1}^{\prime}}$ $\displaystyle U_{u_{k}^{\prime}}\cdot
D_{k+1}^{s_{k+1}}\cdot\ldots\cdot D_{n}^{s_{n}}\cdot U_{u_{n}^{\prime}}\cdot
F_{j}^{\prime}$ $\displaystyle\ \equiv_{\mathbb{B}_{\infty}}\
U_{u_{k}^{\prime}}\cdot D_{k+1}\cdot\ldots\cdot D_{n}\cdot
U_{u_{n}^{\prime}}\cdot F_{j}^{\prime}.$

Hence, the lemma follows from Remark 5.

To finish the proof we analyse
$f(w(S,i))=\min\\{f_{1}(w(S,i)),\ldots,f_{m}(w(S,i))\\}$. Consider a sequence
of subsets $S_{1},\ldots,S_{k}$ with $k\geq N$. Suppose there is a set $S_{l}$
such that for every $1\leq j\leq m$, we have
$f_{j}(w(S_{l},i))<f_{j}(w(S_{l},i+1))$ for every $i\geq N$. In this case,
$f(w(S_{l},i))<f(w(S_{l},i+1))$ holds for all $i\geq N$, so the first
condition of the theorem is met.

Suppose otherwise that no such $S_{l}$ exists. In particular, for every
$S_{l}$ there is at least one $j$ such that
$f_{j}(w(\\{s\\},i))=f_{j}(w(\\{s\\},i+1))$ for all $i\geq N$ and all $s\in
S_{l}$, hence $f_{j}(w(S_{l},i))=f_{j}(w(S_{l},i+1))$ for all $i\geq N$. For
every $S_{l}$ let $X_{l}\subseteq\\{1,\ldots,m\\}$ be the set of indices $j$
such that $f_{j}(w(S_{l},i))=f_{j}(w(S_{l},i+1))$ for all $i\geq N$. By the
above assumptions, every $X_{l}$ is non-empty. Since $k\geq N>m$ there exists
$l_{1},l_{2}$ such that $X_{l_{1}}\cap X_{l_{2}}\neq\emptyset$. From Lemma 8
it follows that for $i\geq N$ it holds: $f_{j}(w(S_{l_{1}}\cup
S_{l_{2}},i))=f_{j}(w(S_{l_{1}}\cup S_{l_{2}},i+1))$ for all $j\in
X_{l_{1}}\cap X_{l_{2}}$; and $f_{j}(w(S_{l_{1}}\cup
S_{l_{2}},i))<f_{j}(w(S_{l_{1}}\cup S_{l_{2}},i+1))$ for all
$j\in\\{1,\ldots,m\\}\setminus(X_{l_{1}}\cap X_{l_{2}})$. Hence for $i$
sufficiently large $f(w(S_{l_{1}}\cup S_{l_{2}},i))=\min_{j\in X_{l_{1}}\cap
X_{l_{2}}}(f_{j}(w(S_{l_{1}}\cup S_{l_{2}},i)))=f(w(S_{l_{1}}\cup
S_{l_{2}},i+1))$, which concludes the proof.

##  5\. Poly-ambiguous recognisable functions over the min-plus semiring

In this section we focus on polynomial-ambiguously recognisable functions over
${\rm Nature}_{\min,+}$. We expect that there is a wider class of functions,
definable like in the previous section, where Theorem 9 holds, but this is
left for future work. A consequence of this section is that WA are strictly
more expressive than PA-WA (see Examples 5 and 5).

We will use in the following the notation of $n$-pumping representations from
Section 4. A sequence of non-empty sets $S_{1},\ldots,S_{m}$ over
$\\{1,\ldots,n\\}$ is called a _partition_ if the sets are pairwise disjoint
and their union is $\\{1,\ldots,n\\}$. Furthermore, we say that
$S\subseteq\\{1,\ldots,n\\}$ is a _selection set_ for $S_{1},\ldots,S_{m}$ if
$|S\cap S_{i}|=1$ for every $i$.

######  Theorem 9 (Pumping Lemma for polynomially-ambiguous automata).

Let $f:\Sigma^{*}\to\mathbb{N}\cup\\{\infty\\}$ be a polynomial-ambiguously
recognisable function over ${\rm Nature}_{\min,+}$. There exist $N$ and a
function $\varphi:{\rm Nature}\to{\rm Nature}$ such that for every $n$-pumping
representation:

$w=u_{0}\cdot\underline{v_{1}}\cdot
u_{1}\cdot\underline{v_{2}}\cdot\ldots\cdot u_{n-1}\cdot\underline{v_{n}}\cdot
u_{n},$

where $|v_{i}|\geq N$ for every $i\leq n$, there exists a refinement:

$w=u_{0}^{\prime}\cdot\underline{y_{1}}\cdot
u_{1}^{\prime}\cdot\underline{y_{2}}\cdot\ldots
u_{n-1}^{\prime}\cdot\underline{y_{n}}\cdot u_{n}^{\prime},$

such that for every partition $\pi=S_{1},\ldots,S_{m}$ of $\\{1,\ldots,n\\}$
with $m\geq\varphi(\max_{j}(|S_{j}|))$, one of the following holds:

  * •

there exists $j$ such that $f(w(S_{j},i))=f(w(S_{j},i+1))$ for all but
finitely many $i$;

  * •

there exists a selection set $S\subseteq\\{1,\ldots,n\\}$ for $\pi$ such that
$f(w(S,i))<f(w(S,i+1))$ for all but finitely many $i$.

We show that $f_{5}$ from Example 2.1 is not definable by any PA-WA. Indeed,
let $N$ and $\varphi$ be the constant and the function from Theorem 9.
Consider the following $2m$-pumping representation:
$w=(\underline{a^{N}}\cdot\underline{b^{N}}\\#)^{m}$ where $m\geq\varphi(2)$
(here $\max_{i}(|S_{i}|)$ will be equal to 2). We index the $j$-th block of
$a$’s with $j$ and the $j$-th block of $b$’s with $j^{\prime}$. We define the
subsets $S_{1},\ldots,S_{m}$ as $S_{j}=\\{j,j^{\prime}\\}$. Clearly, for all
$j$ we have $f_{5}(w(S_{j},i))<f_{5}(w(S_{j},i+1))$. On the other hand for
every selection set $S$ we have $f_{5}(w(S,i))=f_{5}(w(S,i+1))$. Hence $f_{5}$
does not satisfy Theorem 9.

The function $f_{5}$ in Example 2.1 is essentially the function $f_{2}$ from
Example 2.1 applied to the subwords between the symbols $\\#$, where the
outputs are aggregated with $+$. In a similar way one can define a min-plus
automaton recognising $f_{6}(w)=\sum_{i}f_{4}(w_{i})$ for any $w\in\Sigma^{*}$
of the form $w_{0}\\#w_{1}\\#\ldots\\#w_{n}$ with $w_{i}\in\\{a,b\\}^{*}$,
where $f_{4}$ is the function computing the minimal block of $b$’s from
Example 2.1. We show that $f_{6}$ is not definable by PA-WA over ${\rm
Nature}_{\min,+}$. Consider the following $2m$-pumping representation:
$w=(\underline{b^{N}}\cdot a\cdot\underline{b^{N}}\\#)^{m}$ where
$m\geq\varphi(2)$ (here $\max_{i}(|S_{i}|)$ is again 2). As in Example 5, we
index the first $j$-th block of $b$’s with $j$ and the second $j$-th block of
$b$’s with $j^{\prime}$, and we set $S_{j}=\\{j,j^{\prime}\\}$, for $1\leq
j\leq m$. Clearly, for all $j$ we have
$f_{6}(w(S_{j},i))<f_{6}(w(S_{j},i+1))$. On the other hand for every selection
set $S$ we have $f_{6}(w(S,i))=f_{6}(w(S,i+1))$. Hence $f_{6}$ does not
satisfy Theorem 9 either.

Consider the set of matrices ${\rm Nature}_{\min,+}^{Q\times Q}$ over the min-
plus semiring. Recall that here $\oplus=\min$, $\odot=+$, $\mathbb{0}=\infty$,
$\mathbb{1}=0$, and the product of matrices $M,N\in{\rm
Nature}_{\min,+}^{Q\times Q}$ is defined by $M\cdot
N(p,q)=\min_{r}(M(p,r)+N(r,q))$. Also, recall that for any $M\in{\rm
Nature}_{\min,+}^{Q\times Q}$ we denote by $\bar{M}$ the homomorphic image of
$M$ into the finite monoid $\mathbb{B}^{Q\times Q}$ (see Section 2.2). Similar
as in Section 3 and Section 4, we say that $D\in{\rm Nature}_{\min,+}^{Q\times
Q}$ is an idempotent if $\bar{D}$ is an idempotent in the finite monoid
$\mathbb{B}^{Q\times Q}$.

The following lemma states a special property of polynomially-ambiguous
automata that we exploit in the proof of Theorem 9.

######  Lemma 10.

Let $\mathcal{A}=(Q,\Sigma,\\{M_{a}\\}_{a\in\Sigma},I,F)$ be a polynomially-
ambiguous weighted automaton over the min-plus semiring. For every idempotent
$D\in\\{M_{w}\mid w\in\Sigma^{*}\\}$ and for every $p,q\in Q$, there exist
constants $c,d\in{\rm Nature}_{\min,+}$ and $b\in{\rm Nature}$ such that
$D^{b+i}(p,q)=c\cdot i+d$ for all $i\geq 0$.

######  Proof 5.1.

We can view $\bar{D}\in\mathbb{B}^{Q\times Q}$ as the adjacency matrix of a
graph. Now we show that the cycles of the directed graph defined by $\bar{D}$
can be only self-loops. Indeed, assume by contradiction that there exists a
cycle passing through $r,s\in Q$ with $r\neq s$ then
$\bar{D}(r,s)=\bar{D}(s,r)=\bar{D}(r,r)=\bar{D}(s,s)=1$ (because $\bar{D}$ is
an idempotent). Since $D\in\\{M_{w}\mid w\in\Sigma^{*}\\}$, it can be verified
that $\mathcal{A}$ cannot be polynomially-ambiguous [WS91]. Indeed, let $w$ be
the word such that $D=M_{w}$. Then there are at least two different paths from
$r$ to $r$ when reading $w^{2}$. Hence when reading $w^{2n}$ the number of
paths is at least $2^{n}$. Since all automata considered in this paper are
trimmed the state $r$ is both accessible and co-accessible. Hence for every
$n$ there is a word of length linear in $n$ with at least $2^{n}$ accepting
runs. This is a contradiction with the assumption that $\mathcal{A}$ is
polynomially-ambiguous.

We conclude that $\bar{D}$ forms an acyclic graph with some self-loops and the
states in $Q$ can be ordered as $p_{1},\ldots,p_{n}$, such that
$\bar{D}(p_{j},p_{i})=+\infty$ for every $i<j$.

If $D(p,q)=+\infty$ then it suffices to take $c=d=+\infty$ since $D$ is an
idempotent. Otherwise, $D^{i}(p,q)=\min\left(\sum_{1\leq k\leq
i}D(p_{j_{k-1}},p_{j_{k}})\right)$, where the minimum is over all sequences
$(j_{k})_{k=0}^{i}$ such that $p_{j_{0}}=p$, $p_{j_{i}}=q$. Since
$D(p,q)<+\infty$ we can restrict to sequences such that
$D(p_{j_{k-1}},p_{j_{k}})<+\infty$ for all $k$. Let $A_{i}$ be the set of
indices such that $k\in A_{i}$ if: $0<k\leq i$;
$D(p_{j_{k-1}},p_{j_{k}})<+\infty$; and $p_{j_{k-1}}\neq p_{j_{k}}$. Since
$\bar{D}$ is acyclic it follows that $|A_{i}|\leq|Q|$. In particular this
means that the number of possible sets $A_{i}$ depends only on $|Q|$, not on
$i$.

Suppose a sequence $(j_{k})_{k=0}^{i}$ is a witness for the value of
$D^{i}(p,q)$. Let $k\not\in A_{i}$ such that $0<k\leq i$. Then
$D(p_{j_{k}},p_{j_{k}})\leq D(p_{j_{s}},p_{j_{s}})$ for all $0<s\leq i$. Thus
we can modify $(j_{k})_{k=0}^{i}$ into a witness such that for all $k\not\in
A_{i}$ such that $k>0$ the states $p_{j_{k}}$ are all the same. We denote this
state $p_{j}$. Notice that for $i$ big enough the value of $D^{i}(p,q)$
depends mostly on $D(p_{j},p_{j})$. Then $p_{j}$ can be only one of the states
$r$ such that $c=D(r,r)$ is minimal. In particular $c$ does not depend on $i$.
Let $d_{i}=\sum_{k\in A_{i}}D(p_{j_{k-1}},p_{j_{k}})$. Then
$D^{i}(p,q)=d_{i}+c\cdot(i-|A_{i}|)=d_{i}-c\cdot|A_{i}|+c\cdot i$. Therefore
for $i$ big enough, denoted $i\geq i_{0}$, this sum is achieved for $A_{i}$
such that $d_{i}-c\cdot|A_{i}|$ is minimal. Since the number of different
$A_{i}$ is bounded we can assume that $A_{i}$ and $d_{i}$ do not depend on
$i$, for $i\geq i_{0}$, and denote them $A$ and $d^{\prime}$, respectively.

The lemma follows by fixing $c$ as above, $b=|A|+i_{0}$, and
$d=d^{\prime}+c\cdot i_{0}$.

######  Proof 5.2 (Proof of Theorem 9).

Consider a polynomially-ambiguous WA
$\mathcal{A}=(Q,\Sigma,\\{M_{a}\\}_{a\in\Sigma},I,F)$ over ${\rm
Nature}_{\min,+}$ such that $f={\llbracket{}{\mathcal{A}}\rrbracket}$. We take
for $N$ the constant from Lemma 1 for the finite monoid $\mathbb{B}^{Q\times
Q}$. The function $\varphi:{\rm Nature}\rightarrow{\rm Nature}$ will be
determined later in the proof.

Consider an $n$-pumping representation $w$ like in the statement of the
theorem. By Lemma 1, for every $v_{k}$ there exists a factorisation
$v_{k}=x_{k}y_{k}z_{k}$ such that $M_{y_{k}}$ is an idempotent and
$|y_{k}|\leq N$. We denote $D_{k}=M_{y_{k}}$ and define:

$w\;=\;u_{0}^{\prime}\cdot\underline{y_{1}}\cdot
u_{1}^{\prime}\cdot\underline{y_{2}}\cdot\ldots
u_{n-1}^{\prime}\cdot\underline{y_{n}}\cdot u_{n}^{\prime}$

such that each word $y_{k}$ is the factor of $v_{k}$ corresponding to the
idempotent $D_{k}$. In the remainder of the proof we denote $w_{\leq
k}=u_{0}^{\prime}\cdot y_{1}\cdot\ldots u_{k-1}^{\prime}$. For every
$S\subseteq\\{1\ldots n\\}$ we denote by $w_{\leq k}(S,i)$ the word $w_{\leq
k}$ with all $y_{j}$ pumped $i$ times for all $j<k$ such that $j\in S$.

Recall that $\operatorname{Run}_{\mathcal{A}}(w)$ is the set of all accepting
runs on $w$, and let $\rho\in\operatorname{Run}_{\mathcal{A}}(w)$. Every run
induces two states for each $1\leq k\leq n$: states preceding and following
each word $y_{k}$. In the rest of the proof these will be the most important
parts of a run. To work with them, we define the abstraction of $\rho$,
denoted by $\bar{\rho}:\\{1,\ldots,n\\}\to Q\times Q$, such that
$\bar{\rho}(k)=(p,q)$ where $p$ and $q$ are the states of $\rho$ reached after
$w_{\leq k}$ and $w_{\leq k}\cdot y_{k}$, respectively. Similarly, for
$S\subseteq\\{1,\ldots,n\\}$, $i\geq 1$, and
$\rho\in\operatorname{Run}_{\mathcal{A}}(w(S,i))$ we define
$\bar{\rho}:\\{1,\ldots,n\\}\to Q\times Q$ such that $\bar{\rho}(k)=(p,q)$
where $p$ and $q$ are the states of $\rho$ reached after $w_{\leq k}(S,i)$ and
$w_{\leq k}(S,i)\cdot y_{k}(S,i)$, respectively. We denote by
$\overline{\operatorname{Run}_{\mathcal{A}}}(w)$ the set of all $\bar{\rho}$
with $\rho\in\operatorname{Run}_{\mathcal{A}}(w)$, and same for
$\overline{\operatorname{Run}_{\mathcal{A}}}(w(S,i))$. Observe that since all
$D_{k}$ are idempotents,
$\overline{\operatorname{Run}_{\mathcal{A}}}(w(S,i))=\overline{\operatorname{Run}_{\mathcal{A}}}(w)$
for all subsets $S$ and $i\geq 1$.

The next step is to prove that the cardinality of
$\overline{\operatorname{Run}_{\mathcal{A}}}(w)$ is bounded by a polynomial
$P(\cdot)$ depending only on $\mathcal{A}$, namely such that
$|\overline{\operatorname{Run}_{\mathcal{A}}}(w)|\leq P(n)$. Let $w^{\prime}$
be the word obtained from $w$ where each $u_{i}^{\prime}$ is replaced with a
word $u_{i}^{\prime\prime}$ of length at most $|\mathbb{B}^{Q\times Q}|$ such
that $\overline{M_{u_{i}^{\prime}}}=\overline{M_{u_{i}^{\prime\prime}}}$. To
see that $u_{i}^{\prime\prime}$ exists suppose that
$u_{i}^{\prime}=a_{1}\ldots a_{s}$ and $s>|\mathbb{B}^{Q\times Q}|$. By the
pigeonhole principle in the sequence of matrices
$\overline{M_{a_{1}}},\overline{M_{a_{1}a_{2}}},\ldots,\overline{M_{a_{1}\ldots
a_{s}}}$ there is a repetition that can be removed giving a shorter
$u_{i}^{\prime\prime}$ such
that$\overline{M_{u_{i}^{\prime}}}=\overline{M_{u_{i}^{\prime\prime}}}$. Then
$|\operatorname{Run}_{\mathcal{A}}(w^{\prime})|\geq|\overline{\operatorname{Run}_{\mathcal{A}}}(w)|$.
Recall that $|y_{i}|\leq N$ and that $N$ depends only on $\mathbb{B}^{Q\times
Q}$. Then by definition $|w^{\prime}|\leq(N+|\mathbb{B}^{Q\times
Q}|)\cdot(n+1)$ and thus $|\operatorname{Run}_{\mathcal{A}}(w^{\prime})|\leq
R((N+|\mathbb{B}^{Q\times Q}|)\cdot(n+1))$, where $R$ is the polynomial
bounding the number of runs in $\mathcal{A}$. Recall that $\mathcal{A}$ is
polynomially-ambiguous. The claim follows for $P(n)=R((N+|\mathbb{B}^{Q\times
Q}|)\cdot(n+1))$.

Fix a non-empty set $S\subseteq\\{1,\ldots,n\\}$ and a run
$\rho\in\operatorname{Run}_{\mathcal{A}}(w)$. For every $k\in S$ let
$b_{\bar{\rho}}^{k}$, $c_{\bar{\rho}}^{k}$ and $d_{\bar{\rho}}^{k}$ be the
constants from Lemma 10 such that
$D_{k}^{b_{\bar{\rho}}^{k}+i}[\bar{\rho}(k)]=c_{\bar{\rho}}^{k}\cdot
i+d_{\bar{\rho}}^{k}$ for $i\geq 0$. Since $\rho$ is accepting,
$c_{\bar{\rho}}^{k},d_{\bar{\rho}}^{k}<+\infty$. We show that:

  1. (1)

${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i))={\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i+1))$
for all sufficiently large $i$ iff there exists a run
$\rho\in\operatorname{Run}_{\mathcal{A}}(w)$ such that $c_{\bar{\rho}}^{k}=0$
for every $k\in S$;

  2. (2)

${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i))<{\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i+1))$
for all sufficiently large $i$ iff for every run
$\rho\in\operatorname{Run}_{\mathcal{A}}(w)$ there exists $k$ such that
$c_{\bar{\rho}}^{k}>0$.

Since the number of different $b_{\bar{\rho}}^{k}$ is bounded we can assume
that they are all equal to some $i_{0}$ by choosing the maximal
$b_{\bar{\rho}}^{k}$. Let $\rho\in\operatorname{Run}_{\mathcal{A}}(w(S,i+1))$
be a run realising the minimum value for $i\geq i_{0}$. Given that $D_{k}$ is
idempotent one can obtain a run
$\rho^{\prime}\in\operatorname{Run}_{\mathcal{A}}(w(S,i))$ such that
$\bar{\rho}^{\prime}=\bar{\rho}$ by removing one copy of each $y_{k}$. In
particular $|\rho^{\prime}|\leq|\rho|$, which proves
${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i))\leq{\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i+1))$.
It follows that it suffices to show (1) above.

To prove (1) suppose first that
${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i))={\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i+1))$
for all sufficiently large $i$. Let $\rho\in\mathcal{A}(w(S,i+1))$ and
$\rho^{\prime}\in\mathcal{A}(w(S,i))$ be the previous runs realising the
minimum on $w(S,i+1)$ and its shortening, respectively. By Lemma 10
$D_{k}^{i_{0}+i+1}[\bar{\rho}(k)]=c_{\bar{\rho}}^{k}\cdot(i+1)+d_{\bar{\rho}}^{k}$.
If $c_{\bar{\rho}}^{k}>0$ for some $k$ then the inequality
${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i_{0}+i))\leq{\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i_{0}+i+1))$
would be sharp, which is a contradiction. For the other direction suppose
there exists a run $\rho\in\operatorname{Run}_{\mathcal{A}}(w)$ such that
$c_{\bar{\rho}}^{k}=0$ for every $k\in S$. Then for every $i\geq 0$ there
exists a run $\rho_{i}\in\operatorname{Run}_{\mathcal{A}}(w(S,i_{0}+i))$ such
that $|\rho_{i}|\leq|\rho|+\sum_{k}d_{\bar{\rho}}^{k}$. Since
${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i_{0}+i))\leq{\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i_{0}+i+1))\leq|\rho|+\sum_{k}d_{\bar{\rho}}^{k}$
it follows that
${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i_{0}+i))={\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i_{0}+i+1))$
for all sufficiently large $i$.

Given the previous discussion, let
$\bar{R}_{k}=\\{\bar{\rho}\in\overline{\operatorname{Run}}_{\mathcal{A}}(w)\mid
c_{\bar{\rho}}^{k}>0\\}$ for every $k\in\\{1,\ldots,n\\}$. The set
$\bar{R}_{k}$ represents the abstractions of the runs over $w$ that will grow
when pumping $w(\\{k\\},i)$. Then, we can restate (2) as:
${\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i))<{\llbracket{}{\mathcal{A}}\rrbracket}(w(S,i+1))$
for all sufficiently large $i$ iff $\bigcup_{k\in
S}\bar{R}_{k}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$.

We are now ready to prove the theorem. Fix a partition $S_{1},\ldots,S_{m}$ of
$\\{1,\ldots,n\\}$ for some $m\geq\varphi(\max|S_{l}|)$ ($\varphi$ will be
defined below). Suppose the first condition is not true, namely, for all
$1\leq j\leq m$ there exist arbitrarily big values $i$ such that
$f(w(S_{j},i))\neq f(w(S_{j},i+1))$. From (2) it follows that
$f(w(S_{j},i))<f(w(S_{j},i+1))$ for all sufficiently large $i$ and
$\bigcup_{k\in
S_{j}}\bar{R}_{k}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$ for every
$j\leq m$. Let $L=\max|S_{l}|$. We assume that $L>1$, otherwise every
selection $S$ contains a whole set $S_{k}$ for some $k$ and we are done.

To construct the selection set $S=\\{k_{1},\ldots,k_{m}\\}$ we define by
induction the sets $G_{j}$. For every $j\in\\{1,\ldots,m\\}$ let
$G_{j}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)\setminus\bigcup_{l\leq
j}\bar{R}_{k_{l}}$ (where $k_{0}$ is undefined, so
$G_{0}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$). Intuitively, $G_{j}$
correspond to runs that are not covered by the set $\\{k_{1},\ldots,k_{j}\\}$.
For the inductive case, suppose that $j\geq 0$ and $G_{j}\neq\emptyset$. Since
$\bigcup_{k\in
S_{j+1}}\bar{R}_{k}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$, by the
pigeonhole principle there exist $k_{j+1}\in S_{j+1}$ such that
$|\bar{R}_{k_{j+1}}\cap G_{j}|\geq|G_{j}|/|S_{j+1}|$. We add $k_{j+1}$ to $S$
and so
$|G_{j+1}|\leq|G_{j}|-|G_{j}|/|S_{j+1}|=|G_{j}|\cdot(|S_{j+1}|-1)/|S_{j+1}|\leq|G_{j}|\cdot(L-1)/L$.
Suppose this procedure continues until $j=m$ and $G_{m}\neq\emptyset$. Then
$1\leq|\overline{\operatorname{Run}}_{\mathcal{A}}(w)|\cdot((L-1)/L)^{m}$, and
$|\overline{\operatorname{Run}}_{\mathcal{A}}(w)|\geq(L/(L-1))^{m}$. However,
we know that $|\overline{\operatorname{Run}}_{\mathcal{A}}(w)|$ is bounded by
a polynomial function $P(n)$ depending on $|\mathcal{A}|$. Thus, it suffices
to choose $\varphi$ such that $m\geq\varphi(L)$ implies
$(L/(L-1))^{m}>P(L\cdot m)\geq
P(n)\geq|\overline{\operatorname{Run}}_{\mathcal{A}}(w))|$ (recall that
$S_{1},\ldots,S_{m}$ is a partition of $\\{1,\ldots,n\\}$ and $L\cdot m\geq
n$). Therefore, $G_{m}=\emptyset$ and thus $\bigcup_{k\in
S}\bar{R}_{k}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$, which concludes
the proof.

##  6\. Pumping lemmas for the max-plus semiring

In this section, we consider finitely ambiguous and polynomially ambiguous
weighted automata over the ${\rm Nature}_{\max,+}$ semiring. Notice that U-WA
over ${\rm Nature}_{\max,+}$ is the same class of functions as U-WA over ${\rm
Nature}_{\min,+}$ and thus Theorem 2 also holds for this class. For this
reason, here we focus on the ambiguous cases, dividing the section into two
parts to deal separately with the finitely ambiguous and polynomially
ambiguous cases.

###  6.1. Pumping Lemma for Finitely Ambiguous Weighted Automata over ${\rm
Nature}_{\max,+}$

We use the definitions of refinements and n-pumping representations from
Section 3 and Section 4. In order to formulate the pumping lemma for finitely-
ambiguous functions over the $\mathbb{N}_{\max,+}$ semiring, we define a few
more notations.

Fix a function $f:\Sigma^{*}\to\mathbb{N}$ and a word $w\in\Sigma^{*}$.
Suppose that we have an $n$-pumping representation for $w$, and a refinement
thereof. Let $\\{1,\ldots,n\\}$ be the set of all indices in the refinement.
We say that a refinement is _linear_ if for every subset
$S\subseteq\\{1,\ldots,n\\}$, there exists $K$ such that
$f(w(S,i+1))=K+f(w(S,i))$ for all sufficiently large $i$. For linear
refinements we let $\Delta(S)$ denote the above value $K$ (note that $\Delta$
depends on $f$ and $w$, which are fixed). Furthermore, we say that
$S\subseteq\\{1,\ldots,n\\}$ is decomposable if

$\Delta(S)=\sum_{j\in S}\Delta(\\{j\\}).$

######  Theorem 11.

Let $f:\Sigma^{*}\to\mathbb{N}$ be a finitely ambiguous function over the
semiring $\mathbb{N}_{\max,+}$. There exists $N\in\mathbb{N}$ such that for
every $n$-pumping representation

$w=u_{0}\cdot\underline{v_{1}}\cdot
u_{1}\cdot\underline{v_{2}}\cdot\ldots\underline{v_{n}}\cdot u_{n},$

where $n\geq N$ and and $|v_{i}|\geq N$ for all $i$, there exists a linear
refinement

$w=x_{0}\cdot\underline{y_{1}}\cdot
x_{1}\cdot\underline{y_{2}}\cdot\ldots\underline{y_{n}}\cdot x_{n}$

such that for every sequence of pairwise different, non-empty sets
$S_{1},S_{2},\ldots S_{k}\subseteq\\{1,\ldots,n\\}$ with $k\geq N$, one of the
following holds:

  * •

there exists $j$ such that $S_{j}$ is not decomposable;

  * •

there exist $j_{1}$ and $j_{2}$ such that $\\{l_{1},l_{2}\\}$ is decomposable
for every $l_{1}\in S_{j_{1}}$ and $l_{2}\in S_{j_{2}}$.

Before proving the theorem we show how to use the pumping lemma on two
examples.

Consider the function $g_{3}$ which computes

$\max_{0\leq i\leq n}{|a_{1}\ldots a_{i}|_{a}+|a_{i+1}\ldots a_{n}|_{b}},$

for any $w=a_{1}\dots a_{n}\in\\{a,b\\}^{*}$. This is defined by a small
modification of $\mathcal{W}_{3}$ in Figure 1. The weights of the transitions
changing the states is modified to $1$ and the semiring is changed from ${\rm
Nature}_{\min,+}$ to ${\rm Nature}_{\max,+}$. We show that this function
cannot be expressed by any finitely ambiguous WA over ${\rm Nature}_{\max,+}$.
Towards a contradiction fix $N$ from Theorem 11 and consider the
$(2N+2)$-pumping representation
$(\underline{a^{N+1}}\,\underline{b^{N+1}})^{N+1}$. In the refinement, we
index the $j$-th block of $a$’s with $j$ and the $j$-th block of $b$’s with
$j^{\prime}$. Let $x_{1},\ldots,x_{N+1}$ and $y_{1},\ldots,y_{N+1}$ be the
lengths of all blocks of $a$’s and $b$’s in the refinement. We define the sets
$S_{j}=\\{j,j^{\prime}\\}$ for all $1\leq j\leq N+1$. We show that none of the
conditions of the pumping lemma hold. First, it is easy to see that all sets
$S_{j}$ are decomposable. Indeed
$\Delta(S_{j})=x_{j}+y_{j}=\Delta(\\{j\\})+\Delta(\\{j^{\prime}\\})$. For the
second condition we can assume that $j_{2}>j_{1}$. Since the function counts
$a$’s before $b$’s, the set $\\{j_{1}^{\prime},j_{2}\\}$ is not decomposable
because $\Delta(\\{j_{1}^{\prime},j_{2}\\})=\max(y_{j_{1}},x_{j_{2}})$. Thus,
any $S_{j_{1}}$ and $S_{j_{2}}$ will not satisfy the second condition either.

Consider the function $g_{4}$ which computes the length of longest block of
$b$’s. This is defined by $\mathcal{W}_{4}$ in Figure 1 if we change the
semiring of the automaton from ${\rm Nature}_{\min,+}$ to ${\rm
Nature}_{\max,+}$. We shall show that $g_{4}$ cannot be expressed by a FA-WA
over ${\rm Nature}_{\max,+}$. Towards a contradiction let $N$ be the constant
from Theorem 11. Consider the $(N+1)$-pumping representation
$(\underline{b^{N+1}}a)^{N+1}$. We define the sets $S_{j}=\\{j\\}$ for all
$1\leq j\leq N+1$. First, each set is also decomposable for trivial reasons.
Second, every index is not decomposable with any other since the function
takes into account the value of at most one block of $b$’s.

######  Proof 6.1 (Proof of Theorem 11).

Let $\mathcal{A}$ be the finitely ambiguous WA that computes $f$. Suppose that
$\mathcal{A}$ has ambiguity at most $m$. Let $N=\max\\{K,m+1\\}$ such that $K$
is the constant from Lemma 1 applied to $\mathbb{B}^{Q\times Q}$. Now,
consider a word $w$ and an $n$-pumping representation of $w$ according to the
theorem. Since each $v_{j}$ in the representation has length more than $K$ we
can refine every $v_{j}$ to $y_{j}$ such that every $\bar{M}_{y_{j}}$ is an
idempotent.

We prove that this refinement is linear. Fix $S\subseteq\\{1,\ldots,n\\}$. We
prove that $f(w(S,i+1))=K^{\prime}+f(w(S,i))$ such that $K^{\prime}$ does not
depend on $i$ for all $i$ big enough. Consider $i>|Q|$. Let $\rho$ be an
accepting run over $w(S,i)$. For every $j\in S$ let $p_{j,0}$ be the state in
the run $\rho$ before reading $y_{j}$ and $p_{j,1},\ldots p_{j,i}$ the states
after reading $y_{j}$ the respective amount of times. Notice that by
definition $\bar{M}_{y_{j}}(p_{j,s},p_{j,s+1})=1$ for all
$s\in\\{0,\ldots,i-1\\}$. We will need some observations that follow from the
assumption that $\mathcal{A}$ is finitely-ambiguous.

First, let $0\leq s<s^{\prime}\leq i$ such that $p_{j,s}=p_{j,s^{\prime}}$. We
prove that $p_{j,s}=p_{j,s^{\prime\prime}}$ for all $s\leq
s^{\prime\prime}\leq s^{\prime}$. Since $\rho$ is an accepting run and
$\bar{M}_{y_{j}}$ is idempotent
$\bar{M}_{y_{j}}(p_{j,s},p_{j,s^{\prime\prime}})=\bar{M}_{y_{j}}(p_{j,s^{\prime\prime}},p_{j,s})=1$
for all $s\leq s^{\prime\prime}\leq s^{\prime}$. Therefore, if there exists
$s^{\prime\prime}$ such that $p_{j,s}\neq p_{j,s^{\prime\prime}}$ then there
would be two different accepting runs from $p_{j,s}$ to $p_{j,s}$ when reading
$(y_{j})^{2}$ (with $p_{j,s}$ or $p_{j,s^{\prime\prime}}$ in the middle). This
contradicts the EDA criterion in [WS91] (by pumping $(y_{j})^{2}$ one could
generate arbitrary many accepting runs).

To state the second property we introduce some notation. We say that
$(s,s^{\prime})$ is a maximal cycle in $p_{j,0},\ldots,p_{j,i}$ if $0\leq
s<s^{\prime}\leq i$, $p_{j,s}=p_{j,s^{\prime}}$ and $p_{j,s-1}\neq p_{j,s}$,
$p_{j,s^{\prime}}\neq p_{j,s^{\prime}+1}$ (the last condition is required for
$s>0$ and $s^{\prime}<i$). We prove that there is at most one maximal cycle in
every $p_{j,0},\ldots,p_{j,i}$. Suppose otherwise that there are $0\leq
s<s^{\prime}<t<t^{\prime}\leq i$ such that $(s,s^{\prime})$ and
$(t,t^{\prime})$ are maximal cycles. Since $\rho$ is an accepting run and
$\bar{M}_{y_{j}}$ is idempotent
$\bar{M}_{y_{j}}(p_{j,s},p_{j,s})=\bar{M}_{y_{j}}(p_{j,s},p_{j,t})=\bar{M}_{y_{j}}(p_{j,t},p_{j,t})=1$.
This contradicts the IDA criterion in [WS91], i.e. for every $k$ when reading
when reading $(y_{j})^{k}$ there would be at least $k$ runs from $s$ to $t$.

We conclude that every run $\rho$ over $w(S,i)$ has a unique maximal cycle in
every block $j\in\\{1,\ldots,n\\}$. Notice that the number of accepting runs
over $w(S,i+1)$ can only increase compared to the number of runs over $w(S,i)$
since every accepting run $\rho$ over $w(S,i)$ can be prolonged by increasing
the maximal cycle. Recall that $\mathcal{A}$ is finitely-ambiguous. Therefore,
for $i$ big enough the number of accepting runs over $w(S,i)$ and $w(S,i+1)$
will be always the same. We denote this number by $m$.

Let $\rho_{1},\ldots,\rho_{m}$ be all accepting runs over $w(S,i)$. Let
$\operatorname{wt}[\rho_{s}]$ denote the weight of the run $\rho_{s}$ for
$1\leq s\leq m$, i.e.
$f(w(S,i))=\max(\operatorname{wt}(\rho_{1}),\ldots,\operatorname{wt}(\rho_{m}))$.
For every $j\in\\{1,\ldots,n\\}$ and $l\in\\{1,\ldots,m\\}$ we denote by
$\operatorname{wt}(\rho_{l}[j])$ the weight ${M}_{y_{j}}(p,p)$, where $p$ is
the state defining the corresponding maximal cycle. Note that by construction,
each $\rho_{l}[j]$ is a cycle. Then

$\displaystyle
f(w(S,i+1))=\max_{l\in\\{1,\ldots,m\\}}\operatorname{wt}(\rho_{l})+\sum_{i\in
S}\operatorname{wt}{\rho_{l}[i]}.$

Therefore this refinement is linear, where
$\Delta(S)=\max_{l\in\\{1,\ldots,m\\}}\sum_{i\in
S}\operatorname{wt}{\rho_{l}[i]}$.

We say that a cycle $\rho_{l}[j]$ is dominant if
$\operatorname{wt}(\rho_{l^{\prime}}[j])\leq\operatorname{wt}(\rho_{l}[j])$
for all $l^{\prime}$. The rest of the proof involves reasoning about the
dominant cycles. First we make a simple observation. Suppose $\rho_{l}[j]$ is
dominant, then $\operatorname{wt}(\rho_{l}[j])=\Delta(\\{j\\})$. We make one
more observation.

Assume that we have a linear refinement and $S\subseteq\\{1,\ldots,n\\}$ is a
subset of indices of the refinement. Then $S$ is decomposable if and only if
there exists some run $\rho$ such that for all $j\in S$, $\rho[j]$ is
dominant.

Proof. Assume first that $S$ is decomposable, and consider some run $\rho$
such that $\sum_{j\in S}\operatorname{wt}(\rho[j])$ is maximal among all runs
on $w$. We claim that $\rho[j]$ is dominant for all $j\in S$. Assume this is
not the case. Notice that the value computed by the automaton increases by
$\sum_{j\in S}\operatorname{wt}(\rho[j])$ when $S$ is pumped in $\rho$. By the
choice of $\rho$ and the fact that the refinement is linear, we have that
$\Delta(S)=\sum_{j\in S}\operatorname{wt}(\rho[j])$. By assumption we know
that there is some $j^{*}\in S$ such that $\rho$ is not dominant for $j^{*}$,
so $\operatorname{wt}(\rho[j^{*}])<\Delta(\\{j^{*}\\})$. But this means that
$\Delta(S)=\sum_{j\in S}\operatorname{wt}(\rho[j])<\sum_{j\in
S}{\Delta(\\{j\\})}$, which is a contradiction to $S$ being decomposable.

For the reverse implication, consider a run $\rho$ such that $\rho[j]$ is
dominant for all $j\in S$. In particular, $\sum_{j\in
S}\operatorname{wt}(\rho[j])\geq\sum_{j\in
S}\operatorname{wt}(\rho^{\prime}[j])$ for any other run $\rho^{\prime}$. This
means that when the set $S$ is pumped, the value computed by the automaton
increases by $\sum_{j\in S}\operatorname{wt}(\rho[j])$, which also happens to
be $\sum_{j\in S}\Delta(\\{j\\})$ since the cycles in consideration are
dominant. $\blacksquare$

To conclude we show that if the first condition of the pumping lemma does not
hold then the second condition must hold. Indeed, suppose that all sets are
decomposable. Then by Claim 6.1 for every set $S_{j}$ there is some run
$\rho_{l_{j}}$ in which all the cycles corresponding to $S_{j}$ are dominant.
But since there are more sets than runs, there must be some $j_{1}\neq j_{2}$
such that $l_{j_{1}}=l_{j_{2}}$, namely, two sets which have the same
corresponding runs. However, by Claim 6.1 this means that $\\{k_{1},k_{2}\\}$
is decomposable for every $k_{1}\in S_{j_{1}}$ and $k_{2}\in S_{j_{2}}$.

###  6.2. Pumping Lemma for Polynomially Ambiguous Weighted Automata over
${\rm Nature}_{\max,+}$

In this section, we will re-use the definition of linear refinement and
decomposability from the previous section. We will also re-use the definition
of selection set from Section 5.

######  Theorem 12.

Let $f:\Sigma^{*}\to\mathbb{N}$ be a polynomial-ambiguously recognisable
function over $\mathbb{N}_{\max,+}$. There exist $N$ and a function
$\varphi:\mathbb{N}\to\mathbb{N}$ such that for all $n$-pumping
representations

$w=u_{0}\cdot\underline{v_{1}}\cdot u_{1}\cdot\underline{v_{2}}\cdot\ldots
u_{n-1}\cdot\underline{v_{n}}\cdot u_{n},$

where $|v_{i}|\geq N$ for every $1\leq i\leq n$, there exists a linear
refinement

$w=u_{0}^{\prime}\cdot\underline{y_{1}}\cdot
u_{1}^{\prime}\cdot\underline{y_{2}}\cdots
u_{n-1}^{\prime}\cdot\underline{y_{n}}\cdot u_{n}^{\prime},$

such that for every partition $\pi=S_{1},S_{2},\ldots S_{m}$ of
$\\{1,\ldots,n\\}$ with $m\geq\varphi(\max_{j}(|S_{j}|))$ one of the following
holds:

  * •

there exists $j$ such that $S_{j}$ is decomposable;

  * •

there exists a selection set $S$ for $\pi$ such that $S$ is not decomposable.

Before proving this lemma, we show how to use it on examples.

Consider the function $g_{5}$ such that, for any $w$ of the form
$w_{0}\\#w_{1}\\#\ldots\\#w_{n}$ with $w_{i}\in\\{a,b\\}^{*}$ it computes
$g_{5}(w)=\sum_{i=0}^{n}\max\\{|w_{i}|_{a},|w_{i}|_{b}\\}$. This is defined by
$\mathcal{W}_{5}$ in Figure 1 if we change the semiring of the automaton to
${\rm Nature}_{\max,+}$. We show that $g_{5}$ cannot be expressed by a PA-WA.
Assume the contrary and let $N$ and $\varphi$ be the constant and the function
from Theorem 12. Let $m$ be a number larger than $\varphi(2)$. We consider the
refinements of the pumping representation
$(\underline{a^{N}}\,\underline{b^{N}}\\#)^{m}$. In the refinement, we refer
to the $j$-th block of $a$’s as $j$ and to the $j$-th block of $b$’s as
$j^{\prime}$. We define the sets in the partition as
$S_{j}=\\{j,j^{\prime}\\}$ for all $1\leq j\leq m$. It is clear from the
definition of the function $g_{5}$ that no set $S_{j}$ is decomposable, since
only one of the blocks $j$ and $j^{\prime}$ is relevant for the outer sum.
Now, consider any selection set $S$. Since any two elements of $S$ belong to
different blocks of the word separated by $\\#$’s, $S$ is a decomposable set
of indices. Therefore, the function $g_{5}$ is not polynomially ambiguous over
${\rm Nature}_{\max,+}$.

Consider the function $g_{6}$ that given a word of the form
$w_{0}\\#w_{1}\\#\ldots\\#w_{n}$ with $w_{i}\in\\{a,b\\}^{*}$ computes
$g_{6}(w)=\sum_{i=0}^{n}g_{3}(w_{i})$, where $g_{3}$ from Example 6.1. We show
now that $g_{6}$ cannot be expressed as a PA-WA over ${\rm Nature}_{\max,+}$.
Assume the contrary and let $N$ and $\varphi$ be the constant and the function
from the lemma above. Let $m$ be a number larger than $\varphi(2)$. We
consider the refinements of the pumping representation
$(\underline{b^{N}}\,\underline{a^{N}}\\#)^{m}$. Like in Example 6.2 in the
refinement we refer to the $j$-th block of $b$’s as $j$ and to the $j$-th
block of $a$’s as $j^{\prime}$. Let $x_{j}$ and $y_{j}$ be the lengths of the
block of $b$’s and the block of $a$’s, respectively. We define the sets in the
partition as $S_{j}=\\{j,j^{\prime}\\}$ for all $1\leq j\leq m$. Every set
$S_{j}$ is not decomposable since $\Delta(S_{j})=\max(x_{j},y_{j})$. Consider
any selection set $S$ of $\pi$. It is easy to see that $S$ is decomposable
given that all elements belong to different blocks. We conclude that $g_{6}$
cannot be defined by PA-WA over ${\rm Nature}_{\max,+}$.

######  Proof 6.2 (Proof of Theorem 12).

The first part of the proof is the same as in the proof of Theorem 9 which
only depends on the (polynomial) ambiguity of the automaton, and not on the
semiring. We will use the same same notation for the refinement $(y_{k})_{k}$
and in particular, all $D_{k}=M_{y_{k}}$ are idempotents. We will also use the
notation $\overline{\operatorname{Run}_{\mathcal{A}}}(w)$ of abstractions of
runs and the notation $\bar{\rho}:\\{1,\ldots,n\\}\to Q\times Q$. Finally
recall from the proof of Theorem 9 that
$|\overline{\operatorname{Run}_{\mathcal{A}}}(w)|\leq P(n)$ for some
polynomial $P(\cdot)$.

We will also reuse Lemma 10, but over the ${\rm Nature}_{\max,+}$ semiring.
One can easily check that this lemma continues to hold over the max-plus
semiring. The difference is that then $c,d\in{\rm Nature}_{\max,+}$.
Therefore, for every $k\in S$ let $b_{\bar{\rho}(k)}^{k}$,
$c_{\bar{\rho}(k)}^{k}$ and $d_{\bar{\rho}(k)}^{k}$ be the constants from
Lemma 10 such that:

$D_{k}^{b_{\bar{\rho}(k)}^{k}+i}[\bar{\rho}(k)]=c_{\bar{\rho}(k)}^{k}\cdot
i+d_{\bar{\rho}(k)}^{k}$

for $i\geq 0$. Since $\rho$ is accepting, we have
$c_{\bar{\rho}(k)}^{k},d_{\bar{\rho}(k)}^{k}\neq-\infty$.

First, we argue that the refinement defined by $(y_{k})_{k}$ is linear. Fix a
non-empty set $S\subseteq\\{1,\ldots,n\\}$. For
$\bar{\rho}\in\overline{\operatorname{Run}_{\mathcal{A}}}(w)$ let
$c_{\bar{\rho}}=\sum_{k\in S}c_{\bar{\rho}(k)}^{k}$. Recall that every run in
$\operatorname{Run}_{\mathcal{A}}(w(S,i))$ has some abstraction in
$\overline{\operatorname{Run}_{\mathcal{A}}}(w)$ and $\mathcal{A}$ outputs the
maximal value among all runs. It follows by considering $i$ big enough that
$\Delta(S)=\max\\{c_{\bar{\rho}}\mid\bar{\rho}\in\overline{\operatorname{Run}_{\mathcal{A}}}(w)\\}$.

Let $k\in\\{1,\ldots,n\\}$. We say that
$\overline{\rho}\in\overline{\operatorname{Run}_{\mathcal{A}}(w)}$ is
$k$-dominant if $c_{\bar{\rho}(k)}^{k}\geq c_{\bar{\sigma}(k)}^{k}$ for every
$\bar{\sigma}\in\overline{\operatorname{Run}_{\mathcal{A}}}(w)$. Given
$k\in\\{1,\ldots,n\\}$ we define
$\bar{R}_{k}=\\{\overline{\rho}\in\overline{\operatorname{Run}_{\mathcal{A}}}(w)\mid\overline{\rho}\text{
is not $k$-dominant}\\}$.

Assume that we have a linear refinement and $S\subseteq\\{1,\ldots,n\\}$ is a
subset of indices of the refinement. Then $S$ is decomposable if and only if
there exists $\overline{\rho}$ such that for all $j\in S$,
$\overline{\rho}[j]$ is $j$-dominant.

Proof. Follows the same steps as the proof of Claim 6.1. $\blacksquare$

By Claim 6.2, $S$ is not decomposable if and only if $\bigcup_{k\in
S}\bar{R}_{k}=\overline{\operatorname{Run}_{\mathcal{A}}}(w)$.

We are ready to prove the theorem. Fix a partition $S_{1},\ldots,S_{m}$ for
some $m\geq\varphi(\max_{l}|S_{l}|)$. Suppose the first condition is not true,
namely, for every $j$, the set $S_{j}$ is not decomposable. Let
$L=\max_{l}|S_{l}|$. Since no set $S_{l}$ is decomposable we know that $L>1$.
By the observations in the previous paragraph it suffices to construct a
selection set $S$ such that $\bigcup_{k\in
S}\bar{R}_{k}=\overline{\operatorname{Run}_{\mathcal{A}}}(w)$, which will
imply that $S$ is not decomposable.

The remaining part of the proof follows the same steps as the last part in the
proof of Theorem 9. To construct the selection set
$S=\\{k_{1},\ldots,k_{m}\\}$ we define by induction the sets $G_{j}$. For
every $j\in\\{1,\ldots,m\\}$ let
$G_{j}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)\setminus\bigcup_{l\leq
j}\bar{R}_{k_{l}}$ (where $k_{0}$ is undefined, so that
$G_{0}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$). Intuitively, $G_{j}$
correspond to runs that are not covered by the set $\\{k_{1},\ldots,k_{j}\\}$.
For the inductive case, suppose that $j\geq 0$ and $G_{j}\neq\emptyset$. Since
$\bigcup_{k\in
S_{j+1}}\bar{R}_{k}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$, by the
pigeonhole principle there exist $k_{j+1}\in S_{j+1}$ such that
$|\bar{R}_{k_{j+1}}\cap G_{j}|\geq|G_{j}|/|S_{j+1}|$. We add $k_{j+1}$ to $S$
and so
$|G_{j+1}|\leq|G_{j}|-|G_{j}|/|S_{j+1}|=|G_{j}|\cdot(|S_{j+1}|-1)/|S_{j+1}|\leq|G_{j}|\cdot(L-1)/L$.
Suppose this procedure continues until $j=m$ and $G_{m}\neq\emptyset$. Then
$1\leq|\overline{\operatorname{Run}}_{\mathcal{A}}(w))|\cdot((L-1)/L)^{m}$,
and $|\overline{\operatorname{Run}}_{\mathcal{A}}(w)|\geq(L/(L-1))^{m}$.
However, we know that $|\overline{\operatorname{Run}}_{\mathcal{A}}(w)|$ is
bounded by a polynomial function $P(n)$ depending on $|\mathcal{A}|$. Thus, it
suffices to choose $\varphi$ such that $m\geq\varphi(L)$ implies
$(L/(L-1))^{m}>P(L\cdot m)\geq
P(n)\geq|\overline{\operatorname{Run}}_{\mathcal{A}}(w)|$ (recall that
$S_{1},\ldots,S_{m}$ is a partition of $\\{1,\ldots,n\\}$ and $L\cdot m\geq
n$). Therefore, $G_{m}=\emptyset$ and thus $\bigcup_{k\in
S}\bar{R}_{k}=\overline{\operatorname{Run}}_{\mathcal{A}}(w)$, which concludes
the proof.

##  7\. Conclusion

We have shown five pumping lemmas for five different classes of functions. We
believe that the pumping lemmas in Section 5 and in Section 6 could be proved
for a wider class of functions that would contain the class ${\rm
Nature}_{+,\times}$, but this is left for future work. As a corollary of our
results, we showed that recognisable functions over ${\rm Nature}_{\min,+}$
and ${\rm Nature}_{\max,+}$ form a strict hierarchy, namely:

$\text{U-WA}\ \subsetneq\ \text{FA-WA}\ \subsetneq\ \text{PA-WA}\ \subsetneq\
\text{WA}.$

All strict inclusions, except for PA-WA $\subsetneq$ WA, could be extracted
from the analysis of examples in [KLMP04]. However, our results provide a
general machinery to prove such results.

#### Acknowledgments

We thank Shaull Almagor and the anonymous referees of STACS 2018 and LMCS for
their helpful comments.

## References

  * [ABK11] Shaull Almagor, Udi Boker, and Orna Kupferman.  What’s decidable about weighted automata?  In ATVA, pages 482–491, 2011.
  * [ABM+20] S. Akshay, Nikhil Balaji, Aniket Murhekar, Rohith Varma, and Nikhil Vyas.  Near-optimal complexity bounds for fragments of the skolem problem.  In 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France, pages 37:1–37:18, 2020.
  * [ACMP18] Shaull Almagor, Michaël Cadilhac, Filip Mazowiecki, and Guillermo A. Pérez.  Weak cost register automata are still powerful.  In Developments in Language Theory - 22nd International Conference, DLT 2018, Tokyo, Japan, September 10-14, 2018, Proceedings, pages 83–95, 2018.
  * [ADD+13] Rajeev Alur, Loris D’Antoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan.  Regular functions and cost register automata.  In LICS, pages 13–22. IEEE Computer Society, 2013.
  * [AR13] Rajeev Alur and Mukund Raghothaman.  Decision problems for additive regular functions.  In Automata, Languages, and Programming, pages 37–48. Springer, 2013.
  * [BFLM20] Corentin Barloy, Nathanaël Fijalkow, Nathan Lhote, and Filip Mazowiecki.  A robust class of linear recurrence sequences.  In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, pages 9:1–9:16, 2020.
  * [CIK93] Karel Culik II and Jarkko Kari.  Image compression using weighted finite automata.  In Mathematical Foundations of Computer Science 1993, pages 392–402. Springer, 1993.
  * [CKMT16] Thomas Colcombet, Denis Kuperberg, Amaldev Manuel, and Szymon Toruńczyk.  Cost functions definable by min/max automata.  In 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France, pages 29:1–29:13, 2016.
  * [DG07] Manfred Droste and Paul Gastin.  Weighted automata and weighted logics.  Theor. Comput. Sci., 380(1-2):69–86, 2007.
  * [DG19] Manfred Droste and Paul Gastin.  Aperiodic weighted automata and weighted first-order logic.  In 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, pages 76:1–76:15, 2019.
  * [DKV09] Manfred Droste, Werner Kuich, and Heiko Vogler.  Handbook of Weighted Automata.  Springer, 1st edition, 2009.
  * [DRT16] Laure Daviaud, Pierre-Alain Reynier, and Jean-Marc Talbot.  A generalised twinning property for minimisation of cost register automata.  In LICS, 2016.
  * [Ehr61] Andrzej Ehrenfeucht.  An application of games to the completeness problem for formalized theories.  Fund. Math, 49(129-141):13, 1961.
  * [Fra84] Ronald Fraïssé.  Sur quelques classifications des systèmes de relations.  Université d’Alger, Publications Scientifiques, Série A, 1:35–182, 1984.
  * [HU79] John E. Hopcroft and Jeffrey D. Ullman.  Introduction to Automata Theory, Languages and Computation.  Addison-Wesley, 1979.
  * [Kir08] Daniel Kirsten.  A Burnside approach to the termination of Mohri’s algorithm for polynomially ambiguous min-plus-automata.  ITA, 42(3):553–581, 2008.
  * [KL09] Daniel Kirsten and Sylvain Lombardy.  Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata.  In STACS, pages 589–600, 2009.
  * [KLMP04] Ines Klimann, Sylvain Lombardy, Jean Mairesse, and Christophe Prieur.  Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton.  Theor. Comput. Sci., 327(3):349–373, 2004.
  * [KR13] Stephan Kreutzer and Cristian Riveros.  Quantitative monadic second-order logic.  In LICS, pages 113–122. IEEE Computer Society, 2013.
  * [Kro92] Daniel Krob.  The equality problem for rational series with multiplicities in the tropical semiring is undecidable.  In ICALP, pages 101–112, 1992.
  * [Lib13] Leonid Libkin.  Elements of finite model theory.  Springer Science & Business Media, 2013.
  * [Moh97] Mehryar Mohri.  Finite-state transducers in language and speech processing.  Computational Linguistics, 23(2):269–311, 1997.
  * [MR] Filip Mazowiecki and Cristian Riveros.  Maximal partition logic: towards a logical characterization of copyless cost register automata.  In _CSL_ , 2015.
  * [MR18] Filip Mazowiecki and Cristian Riveros.  Pumping lemmas for weighted automata.  In 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, pages 50:1–50:14, 2018\.
  * [MR19] Filip Mazowiecki and Cristian Riveros.  Copyless cost-register automata: Structure, expressiveness, and closure properties.  J. Comput. Syst. Sci., 100:1–29, 2019.
  * [OW14a] Joël Ouaknine and James Worrell.  On the positivity problem for simple linear recurrence sequences,.  In ICALP, pages 318–329, 2014.
  * [OW14b] Joël Ouaknine and James Worrell.  Ultimate positivity is decidable for simple linear recurrence sequences.  In ICALP, pages 330–341, 2014.
  * [Pap93] Christos H. Papadimitriou.  Computational complexity.  Addison-Wesley, 1993.
  * [Pin10] Jean-Éric Pin.  Mathematical foundations of automata theory.  Lecture notes LIAFA, Université Paris, 7, 2010.
  * [Sak09] Jacques Sakarovitch.  Elements of Automata Theory.  Cambridge University Press, 2009.
  * [Sch61] M.-P. Schützenberger.  On the definition of a family of automata.  Information and Control, 4:245–270, 1961.
  * [Sch65] M.-P. Schützenberger.  On finite monoids having only trivial subgroups.  Information and Control, 8:190–194, 1965.
  * [Web94] Andreas Weber.  Finite-valued distance automata.  Theor. Comput. Sci., 134(1):225–251, 1994.
  * [WS91] Andreas Weber and Helmut Seidl.  On the degree of ambiguity of finite automata.  Theoretical Computer Science, 88(2):325–349, 1991.