On finitely ambiguous Büchi automata

2018/09/25 by Christof Löding, Anton Pirogov · 1 citation
Computer Science · #cs.FL

paper · pdf · doi:10.1007/978-3-319-98654-8_41

arxiv created 2018/09/25 · arxiv updated 2018/09/26

Abstract

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

Cited by

• Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Related

• On the Power of Finite Ambiguity in Büchi Complementation
• Ambiguity through the lens of measure theory
• Model Checking Markov Chains Against Unambiguous Buchi Automata
• Congruence Relations for Büchi Automata
• Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata