2014
Chasing the Best Büchi Automata for Nested Depth-first Search Based Model Checking
BLAHOUDEK, FrantišekZákladní údaje
Originální název
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
BLAHOUDEK, František
Vydání
Nantes, Francie, 11th Summer School on Modelling and Verification of Parallel Processes (MOVEP'14), od s. 89-94, 6 s. 2014
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Francie
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
paměťový nosič (CD, DVD, flash disk)
Označené pro přenos do RIV
Ne
Organizační jednotka
Fakulta informatiky
Klíčová slova česky
LTL, Büchiho automaty, model checking
Klíčová slova anglicky
LTL, Büchi automata, model checking
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 2. 9. 2014 14:21, RNDr. František Blahoudek, Ph.D.
V originále
The automata-based model checking uses a translation of formulae in Linear Temporal Logic (LTL) into Büchi automata (BA). The performance of the model checkers can be heavily influenced by the BA used. In this paper we discuss several heuristics commonly used to decide which BA should be used for given verification task, suggest a novel heuristic for this problem and finally evaluate the heuristics using common LTL-to-BA translators, model checker Spin and benchmark of real verification tasks. Our evaluation shows that heuristics based only on number of states of BA or the degree of determinism often give wrong answer or are unable to answer. On a concrete example we further demonstrate our suggestion to exploit some partial knowledge about systems to improve our heuristic.
Česky
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.
Návaznosti
| GBP202/12/G061, projekt VaV |
| ||
| MUNI/A/0765/2013, interní kód MU |
| ||
| MUNI/A/0855/2013, interní kód MU |
|
