Název: Inkrementální induktivní pokrytelnost pro alternující konečné automaty
Překlad názvu: Incremental Inductive Coverability for Alternating Finite Automata
Autoři: Vargovčík, Pavol ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2018
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [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.
Klíčová slova: alternujúci konečný automat; dobre štrukturovaný systém; formálna verifikácia; inkrementálna induktívna pokryteľnosť; prázdnosť; alternating finite automaton; emptiness; formal verification; incremental inductive coverability; well-structured transition system

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/84996

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-590140


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Diplomové práce