Informace o publikaci

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 DURET-LUTZ Alexandre KŘETÍNSKÝ Mojmír STREJČEK Jan

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

Fakulta informatiky Středisko pro pomoc studentům se specifickými nároky

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.

Další info