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.
Další formáty:   BibTeX LaTeX RIS
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
Změnil Změnil: RNDr. František Blahoudek, Ph.D., učo 208029. Změněno: 2. 9. 2014 14:21.
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 VaVNá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 MUNá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 MUNá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
Typ Název Vložil/a Vloženo Práva
Blahoudek.pdf Licence Creative Commons  Verze souboru Blahoudek, F. 2. 9. 2014

Vlastnosti

Adresa v ISu
https://is.muni.cz/auth/publication/1196482/Blahoudek.pdf
Adresa ze světa
https://is.muni.cz/publication/1196482/Blahoudek.pdf
Adresa do Správce
https://is.muni.cz/auth/publication/1196482/Blahoudek.pdf?info
Ze světa do Správce
https://is.muni.cz/publication/1196482/Blahoudek.pdf?info
Vloženo
Út 2. 9. 2014 14:07

Práva

Právo číst
  • kdokoliv v Internetu
Právo vkládat
 
Právo spravovat
  • osoba RNDr. František Blahoudek, Ph.D., učo 208029
Atributy
 

Blahoudek.pdf

Aplikace
Otevřít soubor.
Stáhnout soubor.
Adresa v ISu
https://is.muni.cz/auth/publication/1196482/Blahoudek.pdf
Adresa ze světa
http://is.muni.cz/publication/1196482/Blahoudek.pdf
Typ souboru
PDF (application/pdf)
Velikost
335,2 KB
Hash md5
3ceab4001dde2c6c2df1e17882d4dbaa
Vloženo
Út 2. 9. 2014 14:07

Blahoudek.txt

Aplikace
Otevřít soubor.
Stáhnout soubor.
Adresa v ISu
https://is.muni.cz/auth/publication/1196482/Blahoudek.txt
Adresa ze světa
http://is.muni.cz/publication/1196482/Blahoudek.txt
Typ souboru
holý text (text/plain)
Velikost
17,1 KB
Hash md5
4d5a26b5c836ecdbee6f5eb95438bcaa
Vloženo
Út 2. 9. 2014 14:11
Vytisknout
Nahlásit neoprávněně vložený soubor Zobrazeno: 28. 6. 2022 12:06