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

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

GAISER Andreas KŘETÍNSKÝ Jan ESPARZA Javier

Year of publication 2012
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis - 10th International Symposium ATVA 2012
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-33386-6_7
Field Informatics
Keywords linear temporal logic; automata; determinism
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.