From LTL to Deterministic Automata: A Safraless Compositional Approach

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

ESPARZA Javier KŘETÍNSKÝ Jan

Rok publikování 2014
Druh Článek ve sborníku
Konference Computer Aided Verification - 26th International Conference, CAV 2014
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-08867-9_13
Obor Informatika
Klíčová slova linear temporal logic; automata; determinism; synthesis; probabilistic model checking
Popis We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of phi. The slave automaton for G(psi) is in charge of recognizing whether FG(psi) holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
Související projekty:

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