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 automata. We furthermore show that
the complexity of this model checking problem lies in NC: the subclass of P
comprising those problems solvable in poly-logarithmic parallel time. These
complexity bounds match the known bounds for model checking Markov chains
against specifications given as deterministic automata, notwithstanding the
fact that unambiguous automata can be exponentially more succinct than
deterministic automata. We report on an implementation of our procedure,
including an experiment in which the implementation is used to model check LTL
formulas on Markov chains.
| Search Query: ArXiv Query: search_query=au:”David Muller”&id_list=&start=0&max_results=3