Detailed Information on Publication Record
2013
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
CHATTERJEE, Krishnendu, Andreas GAISER and Jan KŘETÍNSKÝBasic information
Original name
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Authors
CHATTERJEE, Krishnendu (356 India), Andreas GAISER (276 Germany) and Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution)
Edition
Heidelberg Dordrecht London New York, Computer Aided Verification - 25th International Conference, CAV 2013, p. 559-575, 17 pp. 2013
Publisher
Springer
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Germany
Confidentiality degree
není předmětem státního či obchodního tajemství
Publication form
printed version "print"
Impact factor
Impact factor: 0.402 in 2005
RIV identification code
RIV/00216224:14330/13:00066041
Organization unit
Faculty of Informatics
ISBN
978-3-642-39798-1
ISSN
Keywords in English
linear temporal logic; automata; determinism; synthesis; probabilistic model checking
Tags
International impact, Reviewed
Změněno: 27/4/2014 23:03, RNDr. Pavel Šmerk, Ph.D.
Abstract
V originále
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.
Links
GAP202/10/1469, research and development project |
| ||
MUNI/A/0739/2012, interní kód MU |
| ||
MUNI/A/0760/2012, interní kód MU |
|