|
|
Non-Returning Turing Machines
Surovič, Marek ; Vrábel, Lukáš (referee) ; Meduna, Alexandr (advisor)
This work introduces a restricted variant of the Turing machine which cannot move left, thus return on its tape. Other properties, such as the potentially infinite symbol tape or the ability to rewrite symbols on the tape, remain unchanged. By introducing this restriction we limit the expressive power of the Turing machine to the point, where a non-returning Turing machine is equivalent to a finite automaton and can be transformed into one. A transformation algorithm is presented and described in detail.
|
|
|
Construction of the Generalized Finite Automaton
Šoka, Martin ; Košař, Vlastimil (referee) ; Kaštil, Jan (advisor)
The thesis deals with the creation of an algorithm for the construction of the generalized finite automaton. This automaton differs from the conventional finite automaton by the fact that its transitions are defined by words, therefore it is possible to reduce the number of states of the generalized finite automaton. The introduction includes definitions of terms used later in the thesis. In the next chapters I describe the algorithm itself, including the comprehensive analysis of the heuristics for finding a maximal acyclic subgraph in the graph of the automaton. It also describes implementation of the algorithm and experimentation with automatons created by the algorithm.
|
|
|
Generic Flow Analysis in Computer Networks
Jančová, Markéta ; Holkovič, Martin (referee) ; Kolář, Dušan (advisor)
Tato práce se zabývá problematikou popisu síťového provozu pomocí automaticky vytvořeného modelu komunikace. Hlavním zaměřením jsou komunikace v řídicích systémech , které využívají speciální protokoly, jako je například IEC 60870-5-104 . V této práci představujeme metodu charakteristiky síťového provozu z pohledu obsahu komunikace i chování v čase. Tato metoda k popisu využívá deterministické konečné automaty , prefixové stromy a analýzu opakovatelnosti. Ve druhé části této diplomové práce se zaměřujeme na implementaci programu, který je schopný na základě takového modelu komunikace verifikovat síťový provoz v reálném čase.
|
|
| |
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (referee) ; Lengál, Ondřej (advisor)
Presburgerova aritmetika (PrA) je rozhodnutelná teorie přirozených čísel prvního řádu, která nachází uplatnění v mnoha oblastech formální verifikace vlastností softwaru. Řešiče SMT nástroje implementující různé algoritmické přístupy k rozhodování, zda má formule řešení hrají ve formální verifikaci klíčovou roli. V této práci dokumentujeme vytvoření nového automatického SMT řešiče pro PrA založeného na konečných automatech přístupu, který v současnosti žádný SMT řešič nepoužívá. Uvádíme přehled výzev a jejich řešení vyplývajících ze složitosti takového nástroje, včetně výsledků z provedených experimentů, které již identifikují problémy, kde tento alternativní přístup překonává nejmodernější řešiče. Uvádíme také identifikované problémy, u nichž výkonnost postupu založeného na automatech naráží na problémy, které představují otevřené možnosti výzkumu.
|
|
|
Generic Flow Analysis in Computer Networks
Jančová, Markéta ; Holkovič, Martin (referee) ; Kolář, Dušan (advisor)
Tato práce se zabývá problematikou popisu síťového provozu pomocí automaticky vytvořeného modelu komunikace. Hlavním zaměřením jsou komunikace v řídicích systémech , které využívají speciální protokoly, jako je například IEC 60870-5-104 . V této práci představujeme metodu charakteristiky síťového provozu z pohledu obsahu komunikace i chování v čase. Tato metoda k popisu využívá deterministické konečné automaty , prefixové stromy a analýzu opakovatelnosti. Ve druhé části této diplomové práce se zaměřujeme na implementaci programu, který je schopný na základě takového modelu komunikace verifikovat síťový provoz v reálném čase.
|
|
|
Parametric Properties for Log Checker
Mutňanský, Filip ; Kočí, Radek (referee) ; Smrčka, Aleš (advisor)
The goal of this thesis is to implement a tool that based on user defined properties can verify sequences of events in the traces of the program, or the log file. Properties are defined in extended regular expressions. The tool is able to verify parametric properties. User can define relations between parameters of events. Input of this tool is the definition of properties and constraints of parameters. Output of the tool is the report of violated properties with its sequences of events that caused the error.
|
|
|
Syntactic Analysis Based on Special Models
Zámečníková, Eva ; Masařík, Karel (referee) ; Lukáš, Roman (advisor)
This bachelor thesis is dealing with translation based on coupled finite automaton. Coupled finite automaton contains input and output automaton. The input automaton makes syntactic analysis with an input string. Used rules from the input automaton control the output automaton, which generates an output string. Basic topic of this thesis is determinisation of the input automaton without loss of information about rules used in original automaton.
|
|
|
Biautomata
Klouček, Miloš ; Holub, Štěpán (advisor) ; Kozlík, Andrew (referee)
This paper is focused on finite automata and their ability to recognize certain significant classes of regular languages. First of all we define core terms of the theory of finite automata, then we proceed to provide an overview of their properties. Thereafter we focus on extending finite automata into biautomata by equipping them by an extra "backwards" transformation function and on examining properties of such structures. While doing so we especially focus on comparing similar properties of automata and biautomata. In the second part of this paper we demonstrate the utility of biautomata by providing an improved proof of famous Simon's theorem, which characterizes piecewise testable languages. This proof is a slightly modified version of the result of O. Klíma a L. Polák. Powered by TCPDF (www.tcpdf.org)
|
|
|
Synchronization of finite automata
Vorel, Vojtěch ; Koubek, Václav (advisor) ; Pangrác, Ondřej (referee)
The thesis is an introduction to the research of sychronizing words of finite automata and the Černý conjecture. We give an overview of significant results in the field and their proof methods and describe a wide spectrum of unsolved problems. We reproduce also some latest results, namely Trakhtman's upper bound of general synchronizing threshold and Steinberg's tight bound for one-cluster automata with prime length cycle. In the last chapter we focus on subset synchronization and related computational problems. We give a new lower bound of maximal subset synchronizing threshold and partially determine the time complexity of a natural restriction of the PSPACE-complete problem deciding about subset synchronizability.
|
guest ::
