|
|
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.
|
|
|
Construction of Effective Automata for Regex Matching in HW
Frejlach, Jakub ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
This thesis is motivated by the application of REs in domains requiring fast matching such has deep packet inspections. To ensure sufficient speed a HW acceleration is typically employed. During the acceleration, REs are in the form of NFA synthesized on FPGA. Although HW acceleration solves the speed problems, it suffers from increased consumption of the FPGA components, specifically LUT. The goal of this thesis is to design, implement and experimentally evaluate heuristic method for approximation of FA in context of HW accelerated RE matching. The purpose of this approximation is to lower consumption of LUT components during FPGA synthesis. The key idea of the method is to add some transitions allowing to construct a smaller number of character classes and thus to reduce the number of LUT implementing the transition relation while reducing the error by modifying only less significant parts of FA. Proposed method together with evaluation pipeline is implemented in TOFA tool. Technique was evaluated on both synthetic and real data. Results of experiments shows, that transitional approximation works especially well on automatas with large number of equivalence character classes.
|
|
|
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.
|
|
|
Network Protocols Semiautomatic Diagnostics
Svoboda, Ondřej ; Ryšavý, Ondřej (referee) ; Holkovič, Martin (advisor)
This thesis is about semiautomatic network protocol diagnostics and creating protocol description from eavesdropped communication. Several network eavesdropping techniques and some common programs for network analysis are introduced. Well-known network protocols are described, with focus on their communication messages. Some already existing methods for creating models from examples are mentioned and their characteristics defined. Next we design architecture of developed tool and some methods, that create protocol description. After that we explain implementation of this tool and finally the tool is tested and experimented with.
|
|
|
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.
|
|
|
Processing of Turkic Languages
Ciddi, Sibel ; Zeman, Daniel (advisor) ; Hlaváčová, Jaroslava (referee)
Title: Processing of Turkic Languages Author: Sibel Ciddi Department: Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University in Prague Supervisor: RNDr. Daniel Zeman, Ph.D. Abstract: This thesis presents several methods for the morpholog- ical processing of Turkic languages, such as Turkish, which pose a specific set of challenges for natural language processing. In order to alleviate the problems with lack of large language resources, it makes the data sets used for morphological processing and expansion of lex- icons publicly available for further use by researchers. Data sparsity, caused by highly productive and agglutinative morphology in Turkish, imposes difficulties in processing of Turkish text, especially for meth- ods using purely statistical natural language processing. Therefore, we evaluated a publicly available rule-based morphological analyzer, TRmorph, based on finite state methods and technologies. In order to enhance the efficiency of this analyzer, we worked on expansion of lexicons, by employing heuristics-based methods for the extraction of named entities and multi-word expressions. Furthermore, as a prepro- cessing step, we introduced a dictionary-based recognition method for tokenization of multi-word expressions. This method complements...
|
|
|
Three virtual characters in a quarrel: an interactive model
Babor, Petr ; Brom, Cyril (advisor) ; Beneš, Jan (referee)
In computer games, with the ambition to tell a story are often cut-scenes, passages of games, where the player does not play, but only follows a part of the narrated story. This fact distract player from playing. These passages should be integrated as much as possible in the game itself. The goal of our work is to design, implement and test a model for creating cut-scenes with dynamic development and limited user interaction possibilities. We restricted the model to a situation where three characters arguing and we implemented it for the Pogamut platform. We use animations and emoticons as means of expression, characters do not speak by natural language. Movement is ensured by the steering rules from the project Steering Library. Dramaturgy and synchronization of scenes is controlled by a stochastic finite state machine. We made an experiment where the test subjects watched the generated cut-scenes and compared them with hand-made to evaluate the work. The results confirmed the assumption that the quality of generated scenes do not reach handwritten ones. However the test subjects still perceived them positively, because of the ability to influence their development. Implemented parts of the model can be used to create games and educational programs with social theme. Theoretical design of the model can be...
|
|
|
Methods of Automated Model Transformations in Information System Analysis
Tůma, Jakub ; Merunka, Vojtěch (advisor) ; Toman, Prokop (referee)
This doctoral dissertation thesis has impact to holistically development extension of information systems. Thesis has impact to analytical models and its transformation methods.
This thesis is focused on models Business Process Modeling Notation (BPMN) and Business Object Relational Modeling (BORM). Model BPMN is developed since 2000. Model BORM is developed since 1993 and it is older. The thesis general target was extension of holistically development of information systems. The main target was to bridge the gap between BPMN and BORM models.
This thesis was inspired by Finite State Machine (FSM). The state of the art describes approaches to models transformation. In the analytical part the mathematical formula are used to describe transformation. This part is used to base for the implementation part. The implementation part contains transformation algorithm its description and verification on the case studies. Impact of developed transformation method is validated on the comparison with the other approaches.
The targets were aimed and documented automated transformation calculus. The impact of automated BPMN and BORM models connection using transformation method. The result is method of automated transformation from BPMN model to BORM model using algorithm. The transformation method is based on the Mealy automaton.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
guest ::
