|
|
Redukce nedeterministických konečných automatů
Procházka, Lukáš ; Kořenek, Jan (oponent) ; Kaštil, Jan (vedoucí práce)
Nedeterministický konečný automat je důležitým nástrojem, který se používá pro zpracování řetězců v mnoha různých oblastech programování. V rámci zvýšení efektivity programů je důležité snažit se o zmenšování jeho velikosti. Tento problém je však velmi výpočetně náročný, proto je potřeba hledat nové postupy. V této práci jsou uvedeny základy konečných automatů a poté jsou představeny různé metody zabývající se jejich redukcí. Použitelné redukční algoritmy jsou v práci podrobněji popsány, dále implementovány a otestovány. Nakonec jsou výsledky zhodnoceny.
|
|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (oponent) ; Holík, Lukáš (vedoucí práce)
Nondeterministic finite automata (NFA) are widely used in computer science fields, such as regular languages in formal language theory, high-speed network monitoring, image recognition, hardware modeling, or even in bioinformatic for the detection of the sequence of nucleotide acids in DNA. They are also used in regular mode checking, in string solving, in verification of pointer manipulating programs, for construction of linear arithmetic equations and inequalities, for decision in WS1S and WS2S logic, and many others. Automata minimization is a fundamental technique that helps to decrease resource claims (memory, time, or a number of hardware components) of implemented automata and speed up automata operations. Commonly used minimization techniques, such as state merging, transition pruning, and saturation, can leave potentially minimizable automaton subgraphs with duplicit language information. These fragments consist of a group of states, where the part of language of one state is piecewise covered by the other states in this group. The thesis describes a new minimization approach, which uses SAT solver, which provides information for efficient minimization of these so far nonminimizable automaton parts. Moreover, the newly investigated method, which only uses solver information and state merging, can minimize the automaton similarly and on automata with low transition count faster than a tool RABIT/Reduce, which uses state merging and transition pruning.
|
|
|
Efficient Reduction of Finite Automata
Molnárová, Veronika ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
A finite state automaton is a mathematical model used to describe a machine that performs a computation on the given input over a series of states. In the last century, it has found many uses in different fields of information technology, from video game character behavior to compilers. While each automaton denotes its language, one language can be represented by an infinite number of different automata. As these automata vary in size, to ensure the most efficient work with them, we want to find the smallest one possible. In this thesis, we are going to look at five different types of automata reductions. Firstly, we will talk about three known reduction algorithms, which are the minimization of deterministic automata, the reduction based on a relation of simulation, and the reduction by transformation into a canonical residual automaton. These reductions were implemented in C++ and tested on a sample set of automata to compare their results. Lastly, we looked at the possibility of reducing finite state automata using Boolean satisfiability problem (SAT) and quantified Boolean formula (QBF) solvers. We are presenting a set of rules for each solver for generating a clause in conjunctive normal form (CNF), which can precisely represent the given automaton in Boolean algebra. We used this fact to create a new method of nondeterministic automata reduction.
|
|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (oponent) ; Holík, Lukáš (vedoucí práce)
Nondeterministic finite automata (NFA) are widely used in computer science fields, such as regular languages in formal language theory, high-speed network monitoring, image recognition, hardware modeling, or even in bioinformatic for the detection of the sequence of nucleotide acids in DNA. They are also used in regular mode checking, in string solving, in verification of pointer manipulating programs, for construction of linear arithmetic equations and inequalities, for decision in WS1S and WS2S logic, and many others. Automata minimization is a fundamental technique that helps to decrease resource claims (memory, time, or a number of hardware components) of implemented automata and speed up automata operations. Commonly used minimization techniques, such as state merging, transition pruning, and saturation, can leave potentially minimizable automaton subgraphs with duplicit language information. These fragments consist of a group of states, where the part of language of one state is piecewise covered by the other states in this group. The thesis describes a new minimization approach, which uses SAT solver, which provides information for efficient minimization of these so far nonminimizable automaton parts. Moreover, the newly investigated method, which only uses solver information and state merging, can minimize the automaton similarly and on automata with low transition count faster than a tool RABIT/Reduce, which uses state merging and transition pruning.
|
|
|
Redukce nedeterministických konečných automatů
Procházka, Lukáš ; Kořenek, Jan (oponent) ; Kaštil, Jan (vedoucí práce)
Nedeterministický konečný automat je důležitým nástrojem, který se používá pro zpracování řetězců v mnoha různých oblastech programování. V rámci zvýšení efektivity programů je důležité snažit se o zmenšování jeho velikosti. Tento problém je však velmi výpočetně náročný, proto je potřeba hledat nové postupy. V této práci jsou uvedeny základy konečných automatů a poté jsou představeny různé metody zabývající se jejich redukcí. Použitelné redukční algoritmy jsou v práci podrobněji popsány, dále implementovány a otestovány. Nakonec jsou výsledky zhodnoceny.
|
host ::
RSS.