When are emptiness and containment decidable for probabilistic automata?

Laure Daviaud, Marcin Jurdziński, Ranko Lazić, Filip Mazowiecki, Guillermo A. Pérez, James Worrell

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)


The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is known that both problems are undecidable. We provide a more refined view of these problems in terms of the degree of ambiguity of probabilistic automata. We show that a gap version of the emptiness problem (known to be undecidable in general) becomes decidable for automata of polynomial ambiguity. We complement this positive result by showing that emptiness remains undecidable when restricted to automata of linear ambiguity. We then turn to finitely ambiguous automata and give a conditional decidability proof for containment in case one of the automata is assumed to be unambiguous. Part of our proof relies on the decidability of the theory of real exponentiation, proved, subject to Schanuel's Conjecture, by Macintyre and Wilkie.

Original languageEnglish
Pages (from-to)78-96
Number of pages19
JournalJournal of Computer and System Sciences
Early online date10 Feb 2021
Publication statusPublished - Aug 2021


  • Ambiguity
  • Containment
  • Emptiness
  • Probabilistic automata

Cite this