Paper Info
Title
Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis
Abstract
The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] 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.
Year
DOI
Venue
2013
10.1007/978-3-642-39799-8_37
computer aided verification
Keywords
DocType
Volume
probabilistic model checking,dgrw result,new translation,generalized rabin pair,dgrw condition,deterministic automaton,ltl synthesis,new algorithm,recent safraless translation,rabin automaton,smaller automaton,safraless translation
Conference
abs/1304.5281
Citations 
PageRank 
References 
22
0.83
24
Authors
3
Name
Order
Citations
PageRank
Krishnendu Chatterjee12179162.09
Andreas Gaiser2321.98
Jan Křetínský319012.05