2014
Is there a best Büchi automaton for explicit model checking?
BLAHOUDEK, František, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a Jan STREJČEKZákladní údaje
Originální název
Is there a best Büchi automaton for explicit model checking?
Název česky
Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu?
Autoři
BLAHOUDEK, František (203 Česká republika, domácí), Alexandre DURET-LUTZ (250 Francie), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)
Vydání
New York, 2014 International SPIN Symposium on Model Checking of Software, od s. 68-76, 9 s. 2014
Nakladatel
ACM
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
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í
Forma vydání
tištěná verze "print"
Kód RIV
RIV/00216224:14330/14:00073815
Organizační jednotka
Fakulta informatiky
ISBN
978-1-4503-2452-6
Klíčová slova anglicky
linear temporal logic; Büchi automata; explicit model checking
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 11. 7. 2019 13:31, RNDr. Pavel Šmerk, Ph.D.
V originále
LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.
Česky
Překladače LTL na Büchiho automaty jsou obvykle optimalizovány tak, aby produkovaly automaty s co nejmenším počtem stavů, či s co nejmenším počtem nedeterministických stavů. V této publikaci hledáme vlastnosti Büchiho automatů, které skutečně ovlivňují výkon nástrojů pro explicitní metodu ověřování modelu (model checking). A to pomocí manuální analýzy několika automatů a experimenty s běžnými překladače LTL na automaty a realistickými verifikačními úlohami. Výsledkem těchto experimentů je lepší porozumění charakteristik automatů, které jsou dobré pro model checker Spin.
Návaznosti
| GBP202/12/G061, projekt VaV |
| ||
| MUNI/A/0765/2013, interní kód MU |
| ||
| MUNI/A/0855/2013, interní kód MU |
|
