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 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.