Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1112170,
author = {Křetínský, Jan and Ledesma Garza, Ruslan},
address = {Heidelberg Dordrecht London New York},
booktitle = {Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013},
doi = {http://dx.doi.org/10.1007/978-3-319-02444-8_32},
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-02443-1},
pages = {446-450},
publisher = {Springer},
title = {Rabinizer 2: Small Deterministic Automata for LTL\GU},
year = {2013}
}
TY - JOUR
ID - 1112170
AU - Křetínský, Jan - Ledesma Garza, Ruslan
PY - 2013
TI - Rabinizer 2: Small Deterministic Automata for LTL\GU
PB - Springer
CY - Heidelberg Dordrecht London New York
SN - 9783319024431
KW - linear temporal logic
KW - automata
KW - determinism
KW - synthesis
KW - probabilistic model checking
N2 - We present a tool that generates automata for LTL(X,F,G,U) where U does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures.
ER -
KŘETÍNSKÝ, Jan and Ruslan LEDESMA GARZA. Rabinizer 2: Small Deterministic Automata for LTL$\backslash$GU. In \textit{Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013}. Heidelberg Dordrecht London New York: Springer, 2013, p.~446-450. ISBN~978-3-319-02443-1. Available from: https://dx.doi.org/10.1007/978-3-319-02444-8\_{}32.
|
