On Finitely Ambiguous Buchi Automata

Unambiguous Buchi automata, i.e. Buchi automata allowing only one accepting run per word, are a useful restriction of Buchi automata that is well-suited for probabilistic model-checking. In this paper we propose a more permissive variant, namely finitely ambiguous Buchi 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 omega-languages and present a translation from arbitrary nondeterministic Buchi automata with n states to finitely ambiguous automata with at most 3(n) states and at most n accepting runs per word.