|
|
HyperLTL Model Checking
Alexaj, Ondrej ; Strejček, Jan (referee) ; Lengál, Ondřej (advisor)
HyperLTL model checking je technika pre overenie systému voči danej hypervlastnosti vyjadrenej logikou HyperLTL, ktorá dokáže prepojiť viaceré spustenia systému. Hoci bol vytvorený algoritmický prístup založený na automatoch, spolieha sa na štandardné operácie -automatov. Cieľom tejto práce je prekonať kompletný state-of-the-art HyperLTL model checker AutoHyper využitím efektívnejších čiastkových operácií nad automatmi, najmä komplementácie a inklúzie. Implementácia HyperLTL model checkingu v modulárne založenom nástroji pre komplementáciu, Kofola, viedla k výraznému zvýšeniu výkonu v porovnaní s referenčným nástrojom. Napokon, náš prístup ku kontrole jazykovej inklúzie vykazuje výrazné zmenšenie generovaného stavového priestoru. Keďže ide o bežne používanú operáciu nad automatmi, náš prístup by potenciálne mohol prispieť k pokroku aj v iných oblastiach verifikácie.
|
|
|
Abstraction in Automata Algorithms
Kocourek, Tomáš ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Tato práce si klade za cíl implementaci a experimentální porovnání protiřetězcových algoritmů s abstrakcí a bez abstrakce, které testují prázdnost alternujících automatů. Autor také navrhuje vlastní algoritmy s abstrakcí a navrhuje několik optimalizací pro existující abstraktní algoritmy. Práce popisuje teoretické pozadí studovaných algoritmů a navrhuje efektivní způsob implementace datových struktur, které jsou těmito algoritmy používány. Experimentální vyhodnocení na náhodných automatech ukazuje, že algoritmy bez abstrakce vykazují obecně lepší výsledky, neboť nevyužívají náročné operace průniku a komplementace shora a zdola uzavřených množin. V případě automatů s vysokou hustotou přechodů však algoritmy bez abstrakce zpomalují a algoritmy s abstrakcí naopak zrychlují.
|
|
|
Abstraction in Automata Algorithms
Kocourek, Tomáš ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Tato práce si klade za cíl implementaci a experimentální porovnání protiřetězcových algoritmů s abstrakcí a bez abstrakce, které testují prázdnost alternujících automatů. Autor také navrhuje vlastní algoritmy s abstrakcí a navrhuje několik optimalizací pro existující abstraktní algoritmy. Práce popisuje teoretické pozadí studovaných algoritmů a navrhuje efektivní způsob implementace datových struktur, které jsou těmito algoritmy používány. Experimentální vyhodnocení na náhodných automatech ukazuje, že algoritmy bez abstrakce vykazují obecně lepší výsledky, neboť nevyužívají náročné operace průniku a komplementace shora a zdola uzavřených množin. V případě automatů s vysokou hustotou přechodů však algoritmy bez abstrakce zpomalují a algoritmy s abstrakcí naopak zrychlují.
|
guest ::
