Rabinizer 2: Small Deterministic Automata for LTL\GU

Logo poskytovatele

Varování

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

KŘETÍNSKÝ Jan LEDESMA GARZA Ruslan

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

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-02444-8_32
Obor Informatika
Klíčová slova linear temporal logic; automata; determinism; synthesis; probabilistic model checking
Popis 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.
Související projekty:

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