The universality problem for automata with bounded ambiguity

Given an automaton \mathcal{A} on alphabet A recognising the language L(\mathcal{A}), the universality problem asks whether

\forall w \in A^*, w \in L(\mathcal{A})

The universality problem is PSPACE-complete for the class of all non-deterministic automata. In this note, we will prove that the problem is decidable in polynomial time if the automaton has fixed ambiguity. This result was proved in this paper. Our proof is very similar. Most of the credit goes to Ritam Raha for rediscovering the proof, with the support and supervision of Nathan Lhote, Filip Mazowiecki, and Vincent Penelle.

Background on linear recurrence sequences

Recall that an LRS of order k is a sequence (u_\ell)_{\ell \in \mathbb{N}} such that

u_\ell = X \cdot A^{\ell} \cdot Y

where A \in \mathbb{R}^{k \times k} and X,Y \in \mathbb{R}^k.
For instance, the Fibonacci sequence (0,1,1,2,3,5,8,13,\ldots) is

F_\ell = (1 \qquad 0) \cdot \left( \begin{matrix} 1&1 \\ 1&0 \end{matrix} \right)^{\ell} \cdot (0 \qquad 1)

\begin{pmatrix} 1&1 \\ 1&0 \end{pmatrix}

The two properties of LRS we rely on are:

Theorem:
* The \ell-th term of an LRS of order k can be computed in time O(\log(\ell) \cdot k^3)
* Two LRS of order at most k are equal if and only if they agree on the first 2k terms

These two properties are well known and best proved using an algebraic point of view.

The following lemma shows how LRS naturally appear in the study of automata.
We let n be the number of states of the automaton \mathcal{A}.

Lemma:
For any non-deterministic automaton, the sequence
(ACC(\ell))_{\ell \in \mathbb{N}} calculating the number of accepting runs of length \ell
is an LRS of order n

The proof is one line long
ACC(\ell) = I \cdot \Delta^{\ell} \cdot F

The universality problem for unambiguous automata

Recall that an automaton is k-ambiguous if for every word, there are at most k accepting runs for w. Note that we consider only accepting runs; there might be more (non-accepting) runs. For k = 1 we speak of unambiguous automata instead of 1-ambiguous automata: every accepted word has exactly one accepting run.

Theorem:
The universality problem for unambiguous automata is in PTIME

The crux is to show that the sequence

\alpha(\ell) = \text{ number of words of length } \ell \text{ accepted by } \mathcal{A}

is a linear recurrence sequence (LRS) of order n.

We prove the theorem: observe that for an unambiguous automaton \mathcal{A}, we have \alpha = ACC since counting accepted words is the same as counting accepting runs. Hence (\alpha(\ell))_{\ell \in \mathbb{N}} is an LRS of order n. Note that (|A|^{\ell})_{\ell \in \mathbb{N}} is an LRS of order 1. It follows that to check universality of \mathcal{A}, it is enough to check whether

\alpha(\ell) = |A|^{\ell}

for \ell \le n, which can be done in polynomial time.

The universality problem for finitely ambiguous automata

We fix k \in \mathbb{N}.

Theorem:
The universality problem for k-ambiguous automata is in PTIME

We will get a complexity in n^{O(k)}, hence the algorithm is polynomial only when k is constant. One can indeed show that for non-constant k the universality problem is PSPACE-complete again.

The main difficulty in extending the previous idea is that counting accepted words cannot be easily reduced to counting accepting runs, because to an accepted word corresponds to a number of accepting runs between 1 and k. Nevertheless, we will show that the sequence

\alpha(\ell) = \text{ number of words of length } \ell \text{ accepted by } \mathcal{A}

is a linear recurrence sequence (LRS) of order n^{O(k)}.

For p \le k, denote
\alpha_p(\ell) = \text{ number of words of length } \ell \text{ having exactly } p \text{ accepting runs over } \mathcal{A}

We have \alpha(\ell) = \sum_{p = 1}^k \alpha_p(\ell) hence it suffices to show that each (\alpha_p(\ell))_{\ell \in \mathbb{N}} is an LRS of order n^{O(k)}.

We construct an automaton \mathcal{A}_p as follows. On a first approximation, we use the powerset construction capped to sets of size at most p. It is technically convenient for what follows to identify two runs of \mathcal{A}_p which contain exactly the same runs of \mathcal{A}. To this end, we fix a linear order on Q and choose as set of states for \mathcal{A}_p non-decreasing tuples of Q of size at most p. A state is final if it is a tuple of size exactly p containing only accepting states of \mathcal{A}. Hence a word w is accepted by \mathcal{A}_p if and only if w has at least p accepting runs over \mathcal{A}. The automaton \mathcal{A}_p has O(n^p) states.

We let ACC_p(\ell) be the number of accepting runs of length \ell of \mathcal{A}_p.
We observe that

ACC_p(\ell) = \sum_{j = p}^k {j \choose p} \alpha_j(\ell)

Indeed:
* each word having exactly p runs induce one run of \mathcal{A}_p
* each word having exactly p+1 runs induce p+1 runs of \mathcal{A}_p, obtained by choosing p runs among p+1
* more generally, each word having exactly j runs induce {j \choose p} runs of \mathcal{A}_p, obtained by choosing p runs among j

In other words, writing ACC for the vector of length k with (ACC_1,\ldots,ACC_k) and \alpha for (\alpha_1,\ldots,\alpha_k) we obtain

ACC = M \cdot \alpha

with M upper triangular and invertible. Hence

\alpha = M^{-1} ACC

Thanks to the lemma above each ACC_p is an LRS of order n^{O(k)}, which implies that each \alpha_p as well.

This yields a polynomial time algorithm similarly as for unambiguous automata. Note that this also implies that if \mathcal{A} is k-ambiguous and not universal, then there exists a word w that is not accepted by \mathcal{A} of length n^{O(k)}.