Games automata play

Boundedness for (min,plus)-automata

August 15, 2018 | by Nathanaël Fijalkow

We prove that the boundedness problem for (min,plus)-automata is decidable. One of the main application of this result is that the star-heigh problem of regular expressions reduces to (a slight extension of) it. The main point is to present a very useful tool in action: Simon's factorisation theorem. This proof scheme has been used in many, many papers recently.

We consider (min,plus)-automata, meaning that an automaton $\A$ computes a function

where $\Ninfty = \N \cup \{\infty\}$, by assigning to a word $w$ the minimum value of a run, where the value of a run is computed by summing the weights along the run.

The boundedness problem asks whether the function $\A$ is bounded, meaning

In this note, we will construct an algebraic structure from an automaton generalising the transition monoid for non-deterministic automata. This algebraic structure is a stabilisation monoid. The answer to the boundedness problem can be found by inspecting the stabilisation monoid: the function $\A$ is bounded if and only if the stabilisation monoid induced by $\A$ does not contain an unbounded witness. The correctness proof of this characterisation relies on a generic tool for stabilisation monoids called Simon’s factorisation theorem.

Extending the transition monoid

Let $\A$ be a (min,plus)-automaton. The transition for letter $a$ is given by

which reads “the cost of going from $p$ to $q$ reading $a$ is $\Delta(a)(p,q)$”. Algebraically, we consider the semiring $(\Ninfty,\min,+)$, inducing similar operations on matrices. The function $\A : A^* \to \Ninfty$ is defined by $\A(w) = I \cdot \Delta(w) \cdot F$ where $I,F \in \Ninfty^Q$ are the initial and final vectors and $\Delta$ is extended to a morphism $A^* \to \Ninfty^{Q \times Q}$.

We also write $\A(w)(s,t)$ for the cost of the minimal run from $s$ to $t$ over the word $w$.

The special case of non-deterministic automata

Let us consider a special case: $\Delta(a) \in \{0,\infty\}^{Q \times Q}$ and $I,F \in \{0,\infty\}^Q$. Then $\A(w) \in \{0,\infty\}$, and $\A$ is essentially a non-deterministic automaton, where $\Delta(a)(p,q) = 0$ means that there exists a transition from $p$ to $q$, and $\A(w) = 0$ if $w$ is accepted. Indeed in algebraic terms the semiring $(\{0,\infty\}, \min, +)$ is isomorphic to the usual boolean semiring $(\{0,1\},\vee,\wedge)$ (where $0$ is mapped to $1$ and $\infty$ to $0$). In this special case, the boundedness problem reduces to the universality problem (note that this implies PSPACE-hardness of the boundedness problem).

We show how to solve the universality problem by computing the transition monoid. The transition monoid $\M_\A$ of a non-deterministic automaton $\A$ is the monoid generated by the matrices $\Delta(a)$ for $a \in A$. In other words, we start from $\{\Delta(a) : a \in A\}$ and close under matrix product. For the sake of explanation let us see $\Delta(a)$ as a matrix in the boolean semiring $(\{0,\infty\}, \min, +)$. Since $\{0,\infty\}^{Q \times Q}$ is finite, the transition monoid $\M_\A$ is finite and can be effectively computed using a simple saturation algorithm.

One can verify that $\A$ is universal if and only if $\M_\A$ does not contain a matrix $M$ such that $I \cdot M \cdot F = \infty$. Indeed, the morphism $\Delta : A^* \to \M_\A$ maps words to matrices in $\M_\A$ and a word $w$ is rejected if $I \cdot \Delta(w) \cdot F = \infty$.

Projecting on a finite semiring

A crucial property for non-deterministic automata is that $\{0,\infty\}^{Q \times Q}$ is finite, implying that the transition monoid is finite, therefore computable. This does not hold anymore for (min,plus)-automata, ie in the semiring $\Ninfty^{Q \times Q}$.

The good news is that for answering the boundedness problem it is enough to project $\Ninfty$ into a finite semiring. The semiring we are looking at contains three elements: $0,1$ and $\infty$. The intuitive meaning is in terms of costs: $0$ is free, $1$ is a small cost, and $\infty$ a large cost. We let $\pi$ denote the projection from $\Ninfty$ to $\{0,1,\infty\}$, which simply sends $0$ to $0$, any finite value to $1$ and $\infty$ to $\infty$.

The two operations are $\min$ and $+$, with the expected semantics.

Using these two operations we can multiply matrices in $\{0,1,\infty\}^{Q \times Q}$.


We bring a new operator called stabilisation. Consider the following weighted automaton (can it be simpler?).

We have $\A(a) = 1$. The function $\A$ is unbounded, because $\A(a^n) = n$, diverges for $n \to \infty$. Hence we need an operator to capture the behaviour of a repeated sequence; the stabilisation operator will do just that!


At an intuitive level: $\sharp$ corresponds to iterating. Repeating a large number of times an operation with cost $0$ yields an operation with cost $0$. However, if each operation costs $1$, the whole operation becomes very costly.

A matrix $M$ is idempotent if $M^2 = M$. The stabilisation operator over matrices is defined for idempotent matrices by

Intuitively: how much does it cost to go from $s$ to $t$ by repeating the action $M$ a large number of times? The path achieving the minimum goes from $s$ to some $p$, follows a loop around $p$, and then from $p$ to $t$, with the whole operation of cost $M(s,p) + M(p,p)^\sharp + M(p,t)$.

We now have a unary operation on (idempotent) matrices. What we have done is defining a stabilisation monoid, which is given by a set (here matrices over $\{0,1,\infty\}$), a binary operation (multiplication of matrices) and a unary operation called stabilisation.

The stabilisation monoid of a (min,plus)-automaton

Given a (min,plus)-automaton $\A$, we define its stabilisation monoid $\M_\A$ to be the stabilisation monoid generated by the matrices $\pi(\Delta(a))$ for $a \in A$. For convenience we let $\widehat(a)$ denote $\pi(\Delta(a))$. In other words, we start from $\{\widehat(a) : a \in A\}$ and close under matrix product and stabilisation. Since the underlying semiring is finite, the stabilisation monoid is finite and can be effectively computed using a simple saturation algorithm.

We say that a matrix $M$ is an unbounded witness if $I \cdot M \cdot F = \infty$.

Theorem: Let $\A$ be a (min,plus)-automaton. $\A$ is bounded if and only if $\M_\A$ does not contain any unbounded witness

This yields an algorithm for deciding boundedness. A naive implementation is in EXPTIME; a further analysis of the stabilisation monoid gives a PSPACE algorithm.

One direction is easy: let $M \in \M_\A$ be an unbounded witness. One can associate with $M$ a $\sharp$-expression explaining how $M$ was computed in $\M_\A$: for instance, $((a^\sharp) b)^\sharp$ represents the computation:

  • first apply the stabilisation operator to $\widehat(a)$
  • then multiply the result with $\widehat(b)$
  • finally apply the stabilisation operator to the result

Following the inductive construction of the $\sharp$-expression, one can construct a sequence of words $(w_n)_{n \in \N}$ (essentially replacing $\sharp$ by $n$) such that

Hence the fact that $M$ is an unbounded witness implies that $\lim_n \A(w_n) = \infty$.

In the remainder of this post we prove the converse more challenging implication, called completeness.

Simon’s factorisation theorem

Imagine that we have some (min,plus)-automaton $\A$ and we are looking at $\A(w)$ for some word $w$ (which we can think of as very long), for instance

As an approximation let us think of this word as $(ab)^n$ for a very large $n$. We want to know whether $\A((ab)^n)$ is large, or in other words whether it diverges to infinity when $n \to \infty$: this is equivalent to asking whether $I \cdot (\widehat(a) \cdot \widehat(b))^\sharp \cdot F = \omega$.

The word $(ab)^{300000}$ had an obvious factorisation into $(ab)^n$ for a large $n$. Simon’s factorisation theorem says that any word can be factorised in a similar way. Let us formalise this notion of factorisation. Let $\M$ be a stabilisation monoid and a morphism $\phi : A^* \to \M$, the factorisation of $\phi(w)$ is a tree such that

  • each node is labeled by a pair $(M,u)$ where $M \in \M$ and $u \in A^*$
  • the leaves are labeled by $(\phi(a),a)$ for $a \in A$
  • reading the second component of the leaves from left to right yields the word $w$
  • the internal nodes are of two types: product nodes and stabilisation nodes
  • a product node has two children, let $(M_1,w_1)$ and $(M_2,w_2)$ be their labels, then the label of the node is $(M_1 \cdot M_2, w_1 w_2)$
  • a stabilisation node has $k \ge 3$ children, let $(M,w_i)$ be their labels, then $M$ is an idempotent of $\M$ (meaning $M^2 = M$) and the label of the node is $(M^\sharp, w_1 \cdots w_k)$
A factorisation tree of depth $3$ for $abaaaaa$

Theorem: Let $\M$ be a stabilisation monoid and a morphism $\phi : A^* \to \M$. There exists a constant $K$ such that for all words $w \in A^*$, there exists a factorisation of $\phi(w)$ of depth $K$

The theorem says that no matter of long, complicated and messy a word is, it can be factorised through $\phi$ by a tree of constant depth. Here constant means that the value depends on $\M$ but not on the word. The optimal $K$ is $3|\M|$.

Finishing the proof

Let us assume that there are no unbounded witness and prove that $\A$ is bounded. Consider a word $w$. Thanks to Simon’s factorisation theorem applied to the morphism $\phi : A^* \to \M_\A$ defined by

there exists a factorisation of $\phi(w)$ of depth $K$. We will reason on this tree.

We let $W$ denote the maximal weight appearing in the (min,plus)-automaton $\A$.

Lemma: For all nodes labeled $(M,u)$ at distance $d$ from the leaves, for all states $s,t$ we have

We prove the lemma by induction from the leaves to the root.

  • If the node is a leaf this is by definition of $\phi(a)$ and $W$.
  • If the node is a product node labeled $(M_1 M_2,w_1 w_2)$. The first item is easy to prove, let us focus on the second. Assume $(M_1 M_2)(s,t) = 1$, this implies that there exists $p$ such that $M_1(s,p) = 1$ and $M_2(p,t) = 1$. It follows by induction hypothesis that $\A(u)(s,t) \le \A(u_1)(s,p) + \A(u_2)(p,t) \le 2 \cdot 2^{d-1} \cdot W$.
  • If the node is a stabilisation node labeled $(M^\sharp,w_1 \ldots w_k)$. Again we only prove the second item, the first one is easy. Assume $(M^\sharp)(s,t) = 1$, this implies that there exists $p$ such that so $M(s,p) = M(p,t) = 1$ and $M(p,p) = 0$. It follows by induction hypothesis that

We can now finish the proof of completeness. Since $\M_\A$ does not contain any unbounded witness, the previous lemma implies that $\A(w)$ is bounded by $2^K W$ where $K$ is the consant inherited from Simon’s factorisation theorem.