Kavli Affiliate: David Muller | First 5 Authors: Christel Baier, Stefan Kiefer, Joachim Klein, David Müller, James Worrell | Summary: Unambiguous automata are nondeterministic automata in which every word has at most one accepting run. In this paper we give a polynomial-time algorithm for model checking discrete-time Markov chains against omega-regular specifications represented as unambiguous […]