Reference:

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.

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:

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