On finitely ambiguous B\"uchi automata

TL;DR

This paper introduces finitely ambiguous B"uchi automata, a generalization of unambiguous automata, allowing up to a fixed number of accepting runs per word, with a translation method from nondeterministic automata.

Contribution

It extends the concept of ambiguity in B"uchi automata to finitely ambiguous automata and provides a translation from nondeterministic automata with bounded state complexity.

Findings

Finitely ambiguous B"uchi automata generalize unambiguous automata.

A translation from nondeterministic automata to finitely ambiguous automata is proposed.

The translation results in automata with at most 3^n states and n accepting runs per word.

Abstract

Unambiguous B\"uchi automata, i.e. B\"uchi automata allowing only one accepting run per word, are a useful restriction of B\"uchi automata that is well-suited for probabilistic model-checking. In this paper we propose a more permissive variant, namely finitely ambiguous B\"uchi 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 B\"uchi automata with $n$ states to finitely ambiguous automata with at most $3^n$ states and at most $n$ accepting runs per word.