Chasing the Best Büchi Automata for Nested Depth-first Search Based Model Checking

BLAHOUDEK, František. Chasing the Best Büchi Automata for Nested Depth-first Search Based Model Checking. In 11th Summer School on Modelling and Verification of Parallel Processes (MOVEP'14). Nantes, Francie, 2014, s. 89-94.

Zá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

• Originální 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)
• 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

Anotace

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.

Anotace č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: Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

• MUNI/A/0765/2013, interní kód MU: Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

• MUNI/A/0855/2013, interní kód MU: Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty