Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP202%2F10%2F1469" target="_blank" >GAP202/10/1469: Formal methods for analysis and verification of complex systems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Computer Aided Verification - 25th International Conference, CAV 2013
ISBN
9783642397981
ISSN
0302-9743
e-ISSN
—
Number of pages
17
Pages from-to
559-575
Publisher name
Springer
Place of publication
Heidelberg Dordrecht London New York
Event location
Heidelberg Dordrecht London New York
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—