Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Stefan Kiefer, Cas Widdershoven

We introduce a novel technique to analyse unambiguous Büchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that orig…