Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1091149, author = {Chatterjee, Krishnendu and Gaiser, Andreas and Křetínský, Jan}, address = {Heidelberg Dordrecht London New York}, booktitle = {Computer Aided Verification - 25th International Conference, CAV 2013}, doi = {http://dx.doi.org/10.1007/978-3-642-39799-8_37}, keywords = {linear temporal logic; automata; determinism; synthesis; probabilistic model checking}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Heidelberg Dordrecht London New York}, isbn = {978-3-642-39798-1}, pages = {559-575}, publisher = {Springer}, title = {Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis}, year = {2013} }
TY - JOUR ID - 1091149 AU - Chatterjee, Krishnendu - Gaiser, Andreas - Křetínský, Jan PY - 2013 TI - Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis PB - Springer CY - Heidelberg Dordrecht London New York SN - 9783642397981 KW - linear temporal logic KW - automata KW - determinism KW - synthesis KW - probabilistic model checking N2 - 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. ER -
CHATTERJEE, Krishnendu, Andreas GAISER a Jan KŘETÍNSKÝ. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In \textit{Computer Aided Verification - 25th International Conference, CAV 2013}. Heidelberg Dordrecht London New York: Springer, 2013, s.~559-575. ISBN~978-3-642-39798-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39799-8\_{}37.
|