From LTL to deterministic automata (A safraless compositional approach)

Logo poskytovatele

Varování

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

ESPARZA Javier KŘETÍNSKÝ Jan SICKERT Salomon

Rok publikování 2016
Druh Článek v odborném periodiku
Časopis / Zdroj Formal Methods in System Design
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/s10703-016-0259-2
Obor Informatika
Klíčová slova automata; verification; logic
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 co-Büchi automaton for \phi and an array of Rabin automata, one for each G-subformula of \phi. The Rabin automaton for G\psi is in charge of recognizing whether FG\psi holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. 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.

Další info