Is there a best Büchi automaton for explicit model checking?

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu?
Autoři

BLAHOUDEK František DURET-LUTZ Alexandre KŘETÍNSKÝ Mojmír STREJČEK Jan

Rok publikování 2014
Druh Článek ve sborníku
Konference 2014 International SPIN Symposium on Model Checking of Software
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1145/2632362.2632377
Obor Informatika
Klíčová slova linear temporal logic; Büchi automata; explicit model checking
Přiložené soubory
Popis 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.
Související projekty:

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