Are Good-for-Games Automata Good for Probabilistic Model Checking?

Joachim KleinJoachim Klein, David MüllerDavid Müller, Christel BaierChristel Baier, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Joachim Klein, David Müller, Christel Baier, Sascha Klüppelholz
Are Good-for-Games Automata Good for Probabilistic Model Checking?
Proc. of the 8th International Conference on Language and Automata Theory and Applications (LATA), volume 8370 of Lecture Notes in Computer Science, 453--465, 2014. Springer

Details
Bibtex

KurzfassungAbstract
The potential double exponential blow-up for the generation of deterministic ω-automata for linear temporal logic formulas motivates research on weaker forms of determinism. One of these notions is the good-for-games property that has been introduced by Henzinger and Piterman together with an algorithm for generating good-for-games automata from nondeterministic Büchi automata. The contribution of our paper is twofold. First, we report on an implementation of this algorithms and exhaustive experiments. Second, we show how good-for-games automata can be used for the quantitative analysis of systems modeled by Markov decision processes against ω-regular specifications and evaluate this new method by a series of 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-04921-2_37.

@inproceedings{KMBK2014,
  author    = {Joachim Klein and David M{\"{u}}ller and Christel Baier and
               Sascha Kl{\"{u}}ppelholz},
  title     = {Are Good-for-Games Automata Good for Probabilistic Model
               Checking?},
  booktitle = {Proc. of the 8th International Conference on Language and
               Automata Theory and Applications (LATA)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8370},
  publisher = {Springer},
  year      = {2014},
  pages     = {453--465},
  doi       = {10.1007/978-3-319-04921-2_37}
}