I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Markov Chains and Unambiguous Büchi Automata


Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous Büchi automata. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1605.00950.


Unambiguous automata, i.e., nondeterministic automata with the restriction of having at most one accepting run over a word, have the potential to be used instead of deterministic automata in settings where nondeterministic automata can not be applied in general. In this paper, we provide a polynomially time-bounded algorithm for probabilistic model checking of discrete-time Markov chains against unambiguous Büchi automata specifications and report on our implementation and experiments.

Suggested BibTeX entry:

    author = {Christel Baier and Stefan Kiefer and Joachim Klein and Sascha Kl{\"{u}}ppelholz and David M{\"{u}}ller and James Worrell},
    institution = {arXiv.org},
    note = {Available at https://arxiv.org/abs/1605.00950},
    title = {{M}arkov Chains and Unambiguous {B}{\"{u}}chi Automata},
    year = {2016}

See arxiv.org ...
Conference version