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

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Abstract

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.

Details

OriginalspracheEnglisch
TitelLanguage and Automata Theory and Applications
Redakteure/-innenAdrian-Horia Dediu, Carlos Martín-Vide, José-Luis Sierra-Rodríguez, Bianca Truthe
Herausgeber (Verlag)Springer, Cham
Seiten453-465
Seitenumfang13
ISBN (Print)978-3-319-04920-5
PublikationsstatusVeröffentlicht - 2014
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 8370
ISSN0302-9743

Konferenz

Titel8th International Conference on Language and Automata Theory and Applications
KurztitelLATA 2014
Veranstaltungsnummer8
Dauer10 - 14 März 2014
BekanntheitsgradInternationale Veranstaltung
StadtMadrid
LandSpanien

Externe IDs

Scopus 84898075853
ORCID /0000-0002-5321-9343/work/142236743
ORCID /0000-0003-1724-2586/work/165453607

Schlagworte

Schlagwörter

  • Good-for-Games Automata, probabilistic model checking

Bibliotheksschlagworte