TY - GEN
T1 - Rabinizer 2
T2 - 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
AU - Křetínský, Jan
AU - Garza, Ruslán Ledesma
PY - 2013
Y1 - 2013
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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84887498566&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-02444-8_32
DO - 10.1007/978-3-319-02444-8_32
M3 - Conference contribution
AN - SCOPUS:84887498566
SN - 9783319024431
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 446
EP - 450
BT - Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings
Y2 - 15 October 2013 through 18 October 2013
ER -