2016
From LTL to deterministic automata (A safraless compositional approach)
ESPARZA, Javier, Jan KŘETÍNSKÝ a Salomon SICKERTZákladní údaje
Originální název
From LTL to deterministic automata (A safraless compositional approach)
Autoři
ESPARZA, Javier (724 Španělsko), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí) a Salomon SICKERT (276 Německo)
Vydání
Formal Methods in System Design, Springer Netherlands, 2016, 0925-9856
Další údaje
Jazyk
angličtina
Typ výsledku
Článek v odborném periodiku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Spojené státy
Utajení
není předmětem státního či obchodního tajemství
Impakt faktor
Impact factor: 1.000
Kód RIV
RIV/00216224:14330/16:00088475
Organizační jednotka
Fakulta informatiky
UT WoS
000391458400003
Klíčová slova anglicky
automata; verification; logic
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 27. 4. 2017 07:04, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
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.
Návaznosti
| GBP202/12/G061, projekt VaV |
|