Rabinizer 2: Small Deterministic Automata for LTL\GU

Investor logo

Warning

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

KŘETÍNSKÝ Jan LEDESMA GARZA Ruslan

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

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-02444-8_32
Field Informatics
Keywords linear temporal logic; automata; determinism; synthesis; probabilistic model checking
Description 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.
Related projects:

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