Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1187948,
author = {Komárková, Zuzana and Křetínský, Jan},
address = {Heidelberg Dordrecht London New York},
booktitle = {Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014},
doi = {http://dx.doi.org/10.1007/978-3-319-11936-6_17},
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-319-11935-9},
pages = {235-241},
publisher = {Springer},
title = {Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata},
year = {2014}
}
TY - JOUR
ID - 1187948
AU - Komárková, Zuzana - Křetínský, Jan
PY - 2014
TI - Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
PB - Springer
CY - Heidelberg Dordrecht London New York
SN - 9783319119359
KW - linear temporal logic
KW - automata
KW - determinism
KW - synthesis
KW - probabilistic model checking
N2 - We present a tool for translating LTL formulae into deterministic automata. It is the first tool that covers the whole LTL, while not using Safra's determinization or any of its variants, which leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.
ER -
KOMÁRKOVÁ, Zuzana and Jan KŘETÍNSKÝ. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In \textit{Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014}. Heidelberg Dordrecht London New York: Springer. p.~235-241. ISBN~978-3-319-11935-9. doi:10.1007/978-3-319-11936-6\_{}17. 2014.
|
