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

• spin2014preprint.pdf

• 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

• Centrum excelence - Institut teoretické informatiky
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity