|
Automata in Verification
Šmahlíková, Barbora ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Regular model checking is an automata-based technique used for verification of infinite-state systems. The configurations of a system are encoded as a finite automaton and transitions between these configurations as a finite transducer. A technique for verifying arbitrary properties of parameterized systems specified in a temporal logic LTL(MSO) has already been introduced. We present an extension of this algorithm allowing verification of hyperproperties of parameterized systems where an explicit quantification over multiple execution traces is allowed. We specify conditions that need to hold for a pair of advice bits (a finite automaton and a finite transducer) that serves as a witness of the fact that the property holds in the system. The technique presented in this work is implemented in our tool ParaHyper - the only existing tool for the verification of hyperproperties of parameterized systems. The tool uses a SAT solver to generate automata and transducers. If a pair satisfying the conditions for advice bits is found, the property holds in the system. We performed an experimental evaluation of our approach and found that ParaHyper is able to generate advice bits for formulae with an alphabet up to 4 symbols if both the automaton and the transducer have at most 2 states. When a candidate pair is given by the user, ParaHyper can, however, efficiently check if it satisfies the conditions for advice bits even for larger alphabets and greater number of states.
|
|
New Parallel and Regulated Automata and Grammars
Kučera, Jiří ; Průša, Daniel (oponent) ; Sawa, Zdeněk (oponent) ; Meduna, Alexandr (vedoucí práce)
This thesis introduces and studies four new language models with focus on regulation and parallelism in automata and grammars. First, state-synchronized automata systems , present systems consisting of a finite number of pushdown automata controlled by words of a control language over a set of states. Second, unlimited deep pushdown automata , are a modification of deep pushdown automata with no restrictions imposed on the depth of expansion on the pushdown. Third, jumping pure grammars , introduces jumping grammars with no nonterminal symbols. The last one, k#$-rewriting systems , extends #-rewriting systems with additional pushdown memory. The contents of this thesis are divided into three parts. The first part outlines the motivation for introduction of the studied language models and puts them into the context of related formal language theory areas. Furthermore, it gives an overview of the structure of the thesis, reviews fundamental notions of formal language theory and gives a survey of current knowledge related to the subject of research. The second part presents the core of this thesis. Here, formal definitions of all newly introduced language models are given and their expressive power is studied. Finally, this thesis is concluded with a summary of achieved theoretical results as well as related open problem areas, and an outline of the possibilities for further research along with a sketch of possible applications.
|
|
Nové struktury a operace v matematické informatice
Bureš, Richard ; Krčmář, Radim (oponent) ; Meduna, Alexandr (vedoucí práce)
Cílem této práce je podívat se na některé známé a na některé v této práci vytvořené operace a na jejich vlastnosti nad především regulárními, ale i bezkontextovými jazyky. Dále si zde ukážeme, jak je možné takové operace provádět nad konečnými a zásobníkovými automaty a nakonec také jak je možné tyto automaty a operace nad nimi implementovat.
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
Hra pro Oculus Quest
Kryštůfek, Jakub ; Novák, Jiří (oponent) ; Pomikálek, Jiří (vedoucí práce)
Cílem této bakalářské práce je vytvořit prototyp hry ve virtuální realitě pro cílovou platformu Oculus Quest 2. Hra byla vytvořena v herním enginu Unity s kladeným důrazem na optimalizaci a rozšiřitelnost implementovaných systémů. V rámci hry byl vytvořen systém řízení autonomních agentů pomocí konečných automatů a plánovací architektury s názvem cílem řízené plánování akcí. Jednou z nejzajímavějších herních mechanik je systém šíření ohně implementovaný pomocí celulárního automatu.
|
|
Klasifikace a využití gramatik, jazyků a automatů
Jancek, Libor ; Novotná, Veronika (oponent) ; Bobalová, Martina (vedoucí práce)
Tato bakalářská práce se zabývá teorií jazyků, gramatik a automatů. Ukázky použití konečných automatů v praxi na názorných příkladech a vytvoření programu, pro firmu Paradise Casino Admiral a.s. . Účelem tohoto programu je vyplnění evidence docházky na základě rozpisu služeb, který musí navrhnout manažerka pro svoje oddělení každý měsíc. Tento program by měl manažerce usnadnit a hlavně urychlit práci, kterou doposud vykonávala ručně.
|
|
Syntaktická analýza založená na stavových gramatikách
Svatý, Lukáš ; Vrábel, Lukáš (oponent) ; Solár, Peter (vedoucí práce)
V této bakalářské práci je zaveden syntaxí řízený překlad za pomocí stavových gramatik. Teoretická část práce je zaměřená na zavedení teoretických modelů potřebných pro pochopení syntaktické analýzy za pomocí stavových gramatik. Mezi nejdůležitejší z teoretických formálních modelů v této práci patří hluboký zásobníkový převodník a překladová gramatika vytvořená ze stavové gramatiky, které lze využít k syntaktické analýze. Praktická část práce sa zaměřuje hlavně na syntaktickou analýzu zdola nahoru pomocí stavových gramatik a její implementaci.
|
|
Modifikované hluboké zásobníkové automaty
Škvařilová, Radka ; Horáček, Petr (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce představuje dvě nové modifikace hlubokých zásobníkových automatů - bezestavové hluboké zásobníkové automaty a paralelní bezestavové hluboké zásobníkové automaty.V teoretické části jsou zavedeny formální definice a také je zde zkoumána síla těchto automatů. V pratické části je ukázána na jednoduchém příkladu implementace těchto automatů.
|
|
Demonstrační program simulace zásobníkových automatů
Kuželová, Ludmila ; Koutný, Jiří (oponent) ; Lukáš, Roman (vedoucí práce)
Tato práce se zabývá zpracováním simulace zásobníkových a rozšířených automatů. Součástí práce je demonstrační program, který umožňuje uživateli zadat nastavení automatu a následně spustit simulaci přijetí vstupního řetězce automatem. Vybrána je vhodná metoda prohledávání stavového prostoru, z oboru umělé inteligence - prohledávání do šířky - Breadth First Search.
|
|
Paralelní hluboké zásobníkové automaty
Solár, Peter ; Křivka, Zbyněk (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce představuje paralelní hluboké zásobníkové automaty jako paralelní verzi hlubokých zásobníkových automatů. Jsou založeny na pravidlech, podle kterých může automat provést expanzi současně až n nejvýše položených neterminálních symbolů na vrcholu zásobníku pouze jednou aplikací pravidla. Podmínkou je, aby se na zásobníku vyskytoval dostatečný počet neterminálů. Hlavní výhoda použití paralelních hlubokých zásobníkových automatů spočívá v rychlejším rozhodování.
|