Chasing the Best Büchi Automata for Nested Depth-first Search Based 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 Honba na nejlepší Büchiho automaty pro metody ověřování modelu založené na vnořeném prohledávání do hloubky
Autoři

BLAHOUDEK František

Rok publikování 2014
Druh Článek ve sborníku
Konference 11th Summer School on Modelling and Verification of Parallel Processes (MOVEP'14)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova LTL, Büchi automata, model checking
Přiložené soubory
Popis Ověřování modelu pomocí automatů spoléhá na překlad formulí lineární temporální logiky (LTL) na Büchiho automaty (BA). Rychlost nástrojů pro ověřování modelu je tímto překladem ovlivňována. V této publikaci diskutujeme několik heuristik běžně používaných pro výběr nejvhodnějších BA pro danou úlohu ověřování modelu. Dále navrhujeme nové heuristiky pro tento problém a nabízíme srovnání všech zmíněných heuristik na sadě realistických verifikačních úloh s použitím model checkeru Spin a běžně používaných překladaču LTL na BA. Vyhodnocení těchto experimentů ukazuje, že klasické heuristiky používající pouze počet stavů nebo míru determinismu BA se často mýlí či nedokáží odpovědět. Na konkrétních příkladech demonstrujeme dále další uvažované vylepšení navrhované heuristiky, které využívá částečné znalosti o ověřovaném modelu.
Související projekty:

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