TY - GEN
T1 - Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis
AU - Chatterjee, Krishnendu
AU - Gaiser, Andreas
AU - Křetínský, Jan
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84881192861&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39799-8_37
DO - 10.1007/978-3-642-39799-8_37
M3 - Conference contribution
AN - SCOPUS:84881192861
SN - 9783642397981
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 559
EP - 575
BT - Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings
T2 - 25th International Conference on Computer Aided Verification, CAV 2013
Y2 - 13 July 2013 through 19 July 2013
ER -