On Finitely Ambiguous Buechi Automata

摘要

Unambiguous Buechi automata, i.e. Buechi automata allowing only one accepting run per word, are a useful restriction of Buechi automata that is well-suited for probabilistic model-checking. In this paper we propose a more permissive variant, namely finitely ambiguous Buechi automata, a generalisation where each word has at most k accepting runs, for some fixed k. We adapt existing notions and results concerning finite and bounded ambiguity of finite automata to the setting of ω-languages and present a translation from arbitrary nondeterministic Buechi automata with n states to finitely ambiguous automata with at most 3~n states and at most n accepting runs per word.