Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
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. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), volume 9779 of LNCS, pages 23–42, 2016.


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},
    booktitle = {Proceedings of the 28th International Conference on Computer Aided Verification (CAV)},
    pages = {23--42},
    series = {LNCS},
    title = {{M}arkov Chains and Unambiguous {B}{\"{u}}chi Automata},
    volume = {9779},
    year = {2016}

PDF (428 kB)
See ...
Tech report version