Reference:

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.

Abstract:

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:

@inproceedings{16BKKKMW-CAV,
    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}
}