Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066041" target="_blank" >RIV/00216224:14330/13:00066041 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-642-39799-8_37" target="_blank" >http://dx.doi.org/10.1007/978-3-642-39799-8_37</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-39799-8_37" target="_blank" >10.1007/978-3-642-39799-8_37</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Popis výsledku v původním jazyce
The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.
Název v anglickém jazyce
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Popis výsledku anglicky
The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GAP202%2F10%2F1469" target="_blank" >GAP202/10/1469: Formální metody pro analýzu a verifikaci komplexních systémů</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2013
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Computer Aided Verification - 25th International Conference, CAV 2013
ISBN
9783642397981
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
17
Strana od-do
559-575
Název nakladatele
Springer
Místo vydání
Heidelberg Dordrecht London New York
Místo konání akce
Heidelberg Dordrecht London New York
Datum konání akce
1. 1. 2013
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—