Markov chains and unambiguous Büchi automata

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 polynomia...

Full description

Bibliographic Details
Main Authors: Baier, C, Kiefer, S, Klein, J, Klüppelholz, S, Müller, D, Worrell, J
Format: Conference item
Published: Springer, Cham 2016
Description
Summary: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 Buchi automata specifications and report on our implementation and experiments.