Original title:
Inkrementální induktivní pokrytelnost pro alternující konečné automaty
Translated title:
Incremental Inductive Coverability for Alternating Finite Automata
Authors:
Vargovčík, Pavol ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor) Document type: Master’s theses
Year:
2018
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[cze][eng]
V tejto práci navrhujeme špecializáciu algoritmu inductive incremental coverability, ktorá rieši problém prázdnosti alternujúcich konečných automatov. Experimentujeme s rôznymi návrhovými rozhodnutiami, analyzujeme ich a dokazujeme ich korektnosť. Aj keď je známe, že problém je sám o sebe PSpace-ťažký, zameriavame sa na to, aby bolo rozhodovanie prázdnosti výpočetne prijateľné v niektorých triedach automatov s praktickým využitím. Dosiahli sme niekoľko zaujímavýcch výsledkov v porovnaní so špičkovými algoritmami, predovšetkým v porovnaní s algoritmami založenými na protireťazcoch.
In this work, we propose a specialization of the inductive incremental coverability algorithm that solves alternating finite automata emptiness problem. We experiment with various design decisions, analyze them and prove their correctness. Even though the problem itself is PSpace-complete, we are focusing on making the decision of emptiness computationally feasible for some practical classes of applications. We have obtained interesting comparative results against state-of-the-art algorithms, especially in comparison with antichain-based algorithms.
Keywords:
alternating finite automaton; emptiness; formal verification; incremental inductive coverability; well-structured transition system; alternujúci konečný automat; dobre štrukturovaný systém; formálna verifikácia; inkrementálna induktívna pokryteľnosť; prázdnosť
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/84996