. "2012-01-01+01:00"^^ . . "[39C44940EC40]" . "Rabinizer: Small Deterministic Automata for LTL(F,G)"@en . "RIV/00216224:14330/12:00057565!RIV13-GA0-14330___" . "Gaiser, Andreas" . "We present Rabinizer, a tool for translating formulae of the fragment of linear temporal logic with the operators $\\F$ (eventually) and $\\G$ (globally) into deterministic Rabin automata. Contrary to tools like ltl2dstar, which translate the formula into a B\\%22uchi automaton and apply Safra's determinization procedure, Rabinizer uses a direct construction based on the logical structure of the formulae. We describe a number of optimizations of the basic procedure, crucial for the good performance of Rabinizer, and present an experimental comparison."@en . . . "9783642333859" . "Springer-Verlag" . "Rabinizer: Small Deterministic Automata for LTL(F,G)" . "Automated Technology for Verification and Analysis - 10th International Symposium ATVA 2012" . . "Rabinizer: Small Deterministic Automata for LTL(F,G)"@en . . "K\u0159et\u00EDnsk\u00FD, Jan" . . "163892" . . . "Esparza, Javier" . . . "10.1007/978-3-642-33386-6_7" . "RIV/00216224:14330/12:00057565" . "P(GBP202/12/G061)" . "3"^^ . . "1"^^ . "0302-9743" . . . . "linear temporal logic; automata; determinism"@en . "14330" . "Berlin Heidelberg" . "Berlin Heidelberg" . "Rabinizer: Small Deterministic Automata for LTL(F,G)" . "5"^^ . . "We present Rabinizer, a tool for translating formulae of the fragment of linear temporal logic with the operators $\\F$ (eventually) and $\\G$ (globally) into deterministic Rabin automata. Contrary to tools like ltl2dstar, which translate the formula into a B\\%22uchi automaton and apply Safra's determinization procedure, Rabinizer uses a direct construction based on the logical structure of the formulae. We describe a number of optimizations of the basic procedure, crucial for the good performance of Rabinizer, and present an experimental comparison." . .