The universality problem for automata with bounded ambiguity
We prove that the universality problem for automata with fixed ambiguity is decidable in polynomial time.
Given an automaton on alphabet recognising the language , the universality problem asks whether
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 is a sequence such that
where and .
For instance, the Fibonacci sequence is
The two properties of LRS we rely on are:
Theorem:
* The -th term of an LRS of order can be computed in time
* Two LRS of order at most are equal if and only if they agree on the first 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 be the number of states of the automaton .
Lemma:
For any non-deterministic automaton, the sequence
calculating the number of accepting runs of length
is an LRS of order
The proof is one line long
The universality problem for unambiguous automata
Recall that an automaton is -ambiguous if for every word, there are at most accepting runs for . Note that we consider only accepting runs; there might be more (non-accepting) runs. For we speak of unambiguous automata instead of -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
is a linear recurrence sequence (LRS) of order .
We prove the theorem: observe that for an unambiguous automaton , we have since counting accepted words is the same as counting accepting runs. Hence is an LRS of order . Note that is an LRS of order . It follows that to check universality of , it is enough to check whether
for , which can be done in polynomial time.
The universality problem for finitely ambiguous automata
We fix .
Theorem:
The universality problem for -ambiguous automata is in PTIME
We will get a complexity in , hence the algorithm is polynomial only when is constant. One can indeed show that for non-constant 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 and . Nevertheless, we will show that the sequence
is a linear recurrence sequence (LRS) of order .
For , denote
We have hence it suffices to show that each is an LRS of order .
We construct an automaton as follows. On a first approximation, we use the powerset construction capped to sets of size at most . It is technically convenient for what follows to identify two runs of which contain exactly the same runs of . To this end, we fix a linear order on and choose as set of states for non-decreasing tuples of of size at most . A state is final if it is a tuple of size exactly containing only accepting states of . Hence a word is accepted by if and only if has at least accepting runs over . The automaton has states.
We let be the number of accepting runs of length of .
We observe that
Indeed:
* each word having exactly runs induce one run of
* each word having exactly runs induce runs of , obtained by choosing runs among
* more generally, each word having exactly runs induce runs of , obtained by choosing runs among
In other words, writing for the vector of length with and for we obtain
with upper triangular and invertible. Hence
Thanks to the lemma above each is an LRS of order , which implies that each as well.
This yields a polynomial time algorithm similarly as for unambiguous automata. Note that this also implies that if is -ambiguous and not universal, then there exists a word that is not accepted by of length .