Rabinizer: Small Deterministic Automata for LTL(F,G)

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

GAISER Andreas KŘETÍNSKÝ Jan ESPARZA Javier

Rok publikování 2012
Druh Článek ve sborníku
Konference Automated Technology for Verification and Analysis - 10th International Symposium ATVA 2012
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-33386-6_7
Obor Informatika
Klíčová slova linear temporal logic; automata; determinism
Popis 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\"uchi 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.