"Rabinizer 2: Small Deterministic Automata for LTL\\GU"@en . . "Rabinizer 2: Small Deterministic Automata for LTL\\GU"@en . "10.1007/978-3-319-02444-8_32" . . . "linear temporal logic; automata; determinism; synthesis; probabilistic model checking"@en . . "Rabinizer 2: Small Deterministic Automata for LTL\\GU" . "Springer-Verlag" . . "Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013" . "14330" . "1"^^ . . "9783319024431" . . . "P(GBP202/12/G061), S" . . . . "2"^^ . . . "RIV/00216224:14330/13:00066204!RIV14-MSM-14330___" . "Rabinizer 2: Small Deterministic Automata for LTL\\GU" . "Heidelberg Dordrecht London New York" . "0302-9743" . "K\u0159et\u00EDnsk\u00FD, Jan" . "Heidelberg Dordrecht London New York" . "Ledesma Garza, Ruslan" . . . . . "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."@en . "101291" . . "2013-01-01+01:00"^^ . "RIV/00216224:14330/13:00066204" . . "[9DEFF2F0BBBD]" . "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." . . "5"^^ .