Markov Chains and Unambiguous Büchi Automata

Christel BaierChristel Baier, Stefan KieferStefan Kiefer, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, David MüllerDavid Müller, James WorrellJames Worrell

DOI Link

Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, James Worrell
Markov Chains and Unambiguous Büchi Automata
Proc. of the 28th International Conference on Computer Aided Verification (CAV) - Part I, volume 9779 of Lecture Notes in Computer Science, 23--42, 2016. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-41528-4_2.

@inproceedings{BKKKMW2016,
  author    = {Christel Baier and Stefan Kiefer and Joachim Klein and Sascha
               Kl{\"{u}}ppelholz and David M{\"{u}}ller and James Worrell},
  title     = {Markov Chains and Unambiguous B{\"{u}}chi Automata},
  booktitle = {Proc. of the 28th International Conference on Computer Aided
               Verification (CAV) - Part I},
  series    = {Lecture Notes in Computer Science},
  volume    = {9779},
  publisher = {Springer},
  year      = {2016},
  pages     = {23--42},
  doi       = {10.1007/978-3-319-41528-4_2}
}