|
|
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.
|
|
|
Porovnávání jazyků a redukce automatů používaných při filtraci síťového provozu
Havlena, Vojtěch ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se zabývá porovnáváním jazyků automatů a redukcí automatů používaných při monitorování síťového provozu. Je navrženo několik přístupů pro přibližnou redukci automatů (nezachovávající jazyk) a přístup pro porovnávání jejich jazyků. Redukce jsou založeny na podaproximaci jazyka automatu, kdy dochází k odstraňování stavů nebo na nadaproximaci jazyka, kdy dochází k přidávání nových smyček (a odstranění zbytečných stavů později). Navržené metody pro přibližnou redukci a navržená pravděpodobnostní vzdálenost využívají informaci ze síťového provozu. Jsou poskytnuty formální záruky vzhledem k modelu síťového provozu, který je reprezentován pravděpodobnostním automatem. Metody byly implementovány a jejich vlastnosti byly ověřeny na automatech používaných pro filtrování síťového provozu.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulation-based inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.
|
|
|
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 automatů používaných ve filtraci síťového provozu
Semrič, Jakub ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cieľom tejto práce je navrhnúť škálovateľné metódy pre redukciu nedeterministických konečných automatov používaných vo filtrácii paketov. Uvádzame dva prísty redukcie automatov založené na elminácii stavov. Aby sme dosiahli významnú redukciu automatu, používame techniky nezachovávajúce jazyk so zameraním na nad-aproximáciu, keďže redukcie so zachovaním pôvodného jazyka nemusia byť dostatočne účinné. Implementovali sme dané metódy a vyhodnotili presnosť redukovaných automatov na reálnych vzorkoch. Náš prístup neposkytuje žiadne formále záruky vzhľadom na nepoužité dáta, ale može byť hladko použitý na automaty akejkoľvek veľkosti, čo je hlavný problém existujúcich metód, ktoré majú vysokou časovou zložitosťou a nemôžu byť aplikované na veľké automaty.
|
|
|
Přibližné vyhledávání řetězců
Toth, Róbert ; Košař, Vlastimil (oponent) ; Kaštil, Jan (vedoucí práce)
Tato práce se zabývá problémem přibližného vyhledávání řetězců, označovaným též jako vyhledávání s chybami. Nejprve bude definován problém samotný a demonstrována rozmanitost jeho využití, následována krátkým shrnutím rozdílných přístupů k této problematice. Zbývající část práce bude zaměřena na algoritmy založené na využití deterministických konečných automatů. Budou představeny hlavní algoritmy v této oblasti. Ty budou následně implementovány v programovacím jazyku Python a jejich výkonnost důkladně otestována na sérii experimentů.
|
|
|
Efficient Automata Techniques and Their Applications
Havlena, Vojtěch ; Jančar, Petr (oponent) ; Mayr, Richard (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis develops efficient techniques for finite automata and their applications. In particular, we focus on finite automata in network intrusion detection and automata in decision procedures and verification. In the first part of the thesis, we propose techniques of approximate reduction of nondeterministic automata decreasing consumption of resources of hardware-accelerated deep packet inspection. The second part is devoted to automata in decision procedures, in particular, to weak monadic second-order logic of k successors (WSkS) and the theory of strings. We propose a novel decision procedure for WS2S based on automata terms allowing one to effectively prune the state space. Further, we study techniques of WSkS formulae preprocessing intended to reduce the sizes of constructed intermediate automata. Moreover, we employ automata in a decision procedure of the theory of strings for efficient handling of the proof graph. The last part of the thesis then proposes optimizations in rank-based Buchi automata complementation reducing the number of generated states during the construction.
|
|
|
Konstrukce efektivních automatů pro rozpoznávání regulárních výrazů v HW
Frejlach, Jakub ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Motivací této bakalářské práce je užití rozpoznávání regulárních výrazů v aplikačních doménách, kde je vyžadováno rychlé rozpoznávání jako například v hloubkové kontrole paketů. Během akcelerace jsou regulární výrazy ve formě nedeterministických konečných automatů syntetizovány na FPGA. Ačkoliv hardwarová akcelerace řeší rychlostní problémy, tak trpí zvýšenou spotřebou FPGA součástek, konkrétně LUT. Tato práce se zabývá návrhem, implementací a experimentálním vyhodnocením heuristické metody pro aproximaci konečných automatů pro rozpoznávání regulárních výrazů v hardware. Účelem této aproximace je snížení spotřeby LUT součástek při syntéze na FPGA. Princip redukční metody je založen na přidávání nových přechodů, čímž je zajištěna tvorba menšího počtu znakových tříd a je tak dosaženo zredukování spotřeby LUT při implementaci přechodů. Zavedená nepřesnost je minimalizována modifikací pouze méně významných částí automatu. Navržená metoda i s testovacím prostředím je implementována v nástroji TOFA. Technika byla vyhodnocena na syntetických i reálných datech. Výsledky experimentů ukázaly, že přechodová aproximace zvláště dobře funguje na automatech, kde se vyskytuje velký počet znakových tříd.
|
|
| |
|
|
Hledání regulárních výrazů s využitím technologie FPGA
Kubiš, Juraj ; Fukač, Tomáš (oponent) ; Matoušek, Denis (vedoucí práce)
Bakalárska práca sa zaoberá možnosťami hardvérovej akcelerácie vyhľadávania regulárnych výrazov. Obsahom práce je analýza už existujúcich hardvérových architektúr a zhodnotenie ich pozitívnych a negatívnych vlastností. Na základe týchto poznatkov je navrhnutá architektúra. Tá je založená na deterministických konečných automatoch s implicitnými prechodmi (D2FA), je implementovaná v jazyku VHDL a je vykonaná jej syntéza. Výsledky syntézy sú analyzované za účelom zistenia celkovej priepustnosti architektúry. Je navrhnuté programové vybavenie na prevod regulárnych výrazov do podoby D2FA a na optimalizovanie tohoto automatu s cieľom minimalizovania pamäťových nárokov. Implementácia je overená a je zhodnotený prínos jednotlivých optimalizačných techník na redukciu pamäťových nárokov.
|
host ::
RSS.