Are Good-for-Games Automata Good for Probabilistic Model Checking?
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
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
| Originalsprache | Englisch |
|---|---|
| Titel | Language and Automata Theory and Applications |
| Redakteure/-innen | Adrian-Horia Dediu, Carlos Martín-Vide, José-Luis Sierra-Rodríguez, Bianca Truthe |
| Herausgeber (Verlag) | Springer, Cham |
| Seiten | 453-465 |
| Seitenumfang | 13 |
| ISBN (Print) | 978-3-319-04920-5 |
| Publikationsstatus | Veröffentlicht - 2014 |
| Peer-Review-Status | Ja |
Publikationsreihe
| Reihe | Lecture Notes in Computer Science, Volume 8370 |
|---|---|
| ISSN | 0302-9743 |
Konferenz
| Titel | 8th International Conference on Language and Automata Theory and Applications |
|---|---|
| Kurztitel | LATA 2014 |
| Veranstaltungsnummer | 8 |
| Dauer | 10 - 14 März 2014 |
| Bekanntheitsgrad | Internationale Veranstaltung |
| Stadt | Madrid |
| Land | Spanien |
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