Unambiguous and finitely ambiguous automata

Thesis

This thesis is concerned with unambiguous and finitely ambiguous automata, with a focus on automata on infinite words. In particular, it is concerned with the model checking question, which asks whether the traces of a (stochastic and / or non-deterministic) system satisfy a property given by an automaton. By studying these automata through the lens of matrix semigroups and making use of their spectral properties, we show that the model checking question can be solved efficiently in severa...

Expand abstract

Authors: Widdershoven, C

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: Büchi automata; model checking; automata; ambiguity; finitely ambiguous automata; Markov chains; LTL; unambiguous automata; branching processes
• Subjects: computer science