Boundedness for (min,plus)-automata

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

\mathcal{A} : A^* \to \mathbb{N}_{\infty}

where \mathbb{N}_{\infty} = \mathbb{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 \mathcal{A} is bounded, meaning

\exists N \in \mathbb{N},\ \forall w \in A^*,\ \mathcal{A}(w) \le N

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 \mathcal{A} is bounded if and only if the stabilisation monoid induced by \mathcal{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 \mathcal{A} be a (min,plus)-automaton. The transition for letter a is given by

\Delta(a) \in \mathbb{N}_{\infty}^{Q \times Q}

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

We also write \mathcal{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 \mathcal{A}(w) \in \{0,\infty\}, and \mathcal{A} is essentially a non-deterministic automaton, where \Delta(a)(p,q) = 0 means that there exists a transition from p to q, and \mathcal{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 \mathcal{M}_\mathcal{A} of a non-deterministic automaton \mathcal{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 \mathcal{M}_\mathcal{A} is finite and can be effectively computed using a simple saturation algorithm.

One can verify that \mathcal{A} is universal if and only if \mathcal{M}_\mathcal{A} does not contain a matrix M such that I \cdot M \cdot F = \infty. Indeed, the morphism \Delta : A^* \to \mathcal{M}_\mathcal{A} maps words to matrices in \mathcal{M}_\mathcal{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, i.e. in the semiring \mathbb{N}_{\infty}^{Q \times Q}.

The good news is that for answering the boundedness problem it is enough to project \mathbb{N}_{\infty} 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 \mathbb{N}_{\infty} 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}.

Stabilisation

We bring a new operator called stabilisation. Consider the following weighted automaton.

We have \mathcal{A}(a) = 1. The function \mathcal{A} is unbounded, because \mathcal{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!

Define

0^\sharp = 0 \quad 1^\sharp = \infty \quad \infty^\sharp = \infty

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

M^\sharp(s,t) = \min \left\{ M(s,p) + M(p,p)^\sharp + M(p,t) : p \in Q \right\}

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 \mathcal{A}, we define its stabilisation monoid \mathcal{M}_\mathcal{A} to be the stabilisation monoid generated by the matrices \pi(\Delta(a)) for a \in A. For convenience we let \mathbf{a} denote \pi(\Delta(a)). In other words, we start from \{\mathbf{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 \mathcal{A} be a (min,plus)-automaton. \mathcal{A} is bounded if and only if \mathcal{M}_\mathcal{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 \mathcal{M}_\mathcal{A} be an unbounded witness. One can associate with M a \sharp-expression explaining how M was computed in \mathcal{M}_\mathcal{A}: for instance, ((a^\sharp) b)^\sharp represents the computation:
* first apply the stabilisation operator to \mathbf{a},
* then multiply the result with \mathbf{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 \mathbb{N}} (essentially replacing \sharp by n) such that

\lim_n\ \mathcal{A}(w_n)(p,q) = \infty \text{ if and only if } M(p,q) = \omega

Hence the fact that M is an unbounded witness implies that \lim_n \mathcal{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 \mathcal{A} and we are looking at \mathcal{A}(w) for some word w (which we can think of as very long), for instance (ab)^{300000}. As an approximation let us think of this word as (ab)^n for a very large n.
We want to know whether \mathcal{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 (\mathbf{a} \cdot \mathbf{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 \mathcal{M} be a stabilisation monoid and a morphism \phi : A^* \to \mathcal{M}, the factorisation of \phi(w) is a tree such that
* each node is labeled by a pair (M,u) where M \in \mathcal{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 \mathcal{M} (meaning M^2 = M) and the label of the node is (M^\sharp, w_1 \cdots w_k).

Theorem:
Let \mathcal{M} be a stabilisation monoid and a morphism \phi : A^* \to \mathcal{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 \mathcal{M} but not on the word. The optimal K is 3|\mathcal{M}|.

Finishing the proof

Let us assume that there are no unbounded witness and prove that \mathcal{A} is bounded.
Consider a word w. Thanks to Simon’s factorisation theorem applied to the morphism
\phi : A^* \to \mathcal{M}_\mathcal{A} defined by \phi(a) = \mathbf{a}, 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 \mathcal{A}.

Lemma:
For all nodes labeled (M,u) at distance d from the leaves, for all states s,t we have
M(s,t) = 0 \implies \mathcal{A}(u)(s,t) = 0
M(s,t) = 1 \implies \mathcal{A}(u)(s,t) \le 2^d \cdot W

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 \mathcal{A}(u)(s,t) \le \mathcal{A}(u_1)(s,p) + \mathcal{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 M(s,p) + M^\sharp(p,p) + M(p,t) = 1 so M(s,p) = M(p,t) = 1 and M(p,p) = 0. It follows by induction hypothesis that

\mathcal{A}(w_1 \ldots w_k)(s,t) \le \mathcal{A}(w_1)(s,p) + \mathcal{A}(w_2)(p,p) + \cdots + \mathcal{A}(w_{k-1})(p,p) + \mathcal{A}(w_k)(p,t)
which is bounded by 2^{d-1} \cdot W + 0 + 2^{d-1} \cdot W.

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