Chasing the Best Büchi Automata for Nested Depth-first Search Based Model Checking
| 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 | |
| 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 | |
| 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: |