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

Permalink: http://www.nusl.cz/ntk/nusl-590140


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses