|
|
Implementace jednotky pro vyhledávání vzorů v FPGA
Košař, Vlastimil ; Kořenek, Jan (oponent) ; Kaštil, Jan (vedoucí práce)
Tato práce pojednává o algoritmech pro vyhledávání vzorů používaných v moderních systémech pro detekci nežádoucího provozu, přičemž se zaměřuje na algoritmy umožňující vyhledávání regulárních výrazů. Zabývá se přístupy založenými na deterministických a nedeterministických konečných automatech, hybridními přístupy a přístupem založeným na regulárních výrazech jako programovacím jazyku speciálních procesorů. Dále popisuje návrh implementace jednotek pro vyhledávání vzorů popsaných regulárními výrazy založených na několika z popsaných přístupů včetně metodiky odhadu zabraných zdrojů. V další části je popsán vyvinutý softwarový systém pro generování jednotek. V následující části jsou ukázány a diskutovány dosažené výsledky.
|
|
|
A Library for Computing Simulation Relations over Büchi Automata
Odvárka, Daniel ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
This thesis presents the topic of simulation relations over Büchi automata and the use case of various simulations. The simulation relations are important for reducing a state space of an automaton, or checking the under approximation of language inclusion. There are also parity games, which are important for computing some of the simulation types we introduce. We will go over multiple algorithms that compute these simulation relations. The mentioned algorithms are implemented in programming language C++ and are compared to a tool named RABIT. Our implementation is better only for smaller sized automata.
|
|
| |
|
|
Alternativní transformace jazykových modelů
Havel, Martin ; Beníčková, Zuzana (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce poskytuje ucelený přehled poznatků z oblasti regulárních výrazů, konečných automatů a transformací z regulárního výrazu na konečný automat. Práce navrhuje nové transformace se zaměřením na minimalizaci počtu stavů a počtu pravidel konečných automatů. Koncept alternativních transformací je zpracován do algoritmů a prokázán matematickým důkazy. Cílem práce je obohatit transformace o nové alternativy na poli regulárních výrazů a konečných automatů. Pozornost je především věnována ekonomické stránce finálního konečného automatu. V rámci práce se podařilo sestrojit algoritmy, které jsou schopny transformovat regulární výrazy na konečné automaty. Práce zároveň poskytuje návod k jejich implementaci. Prezentuje obecný koncept transformací, který umožňuje tvořit méně rozsáhlé konečné automaty. Využitím uvedeného přístupu je možné rozšířit řadu transformací o alternativní verze.
|
|
|
Generování Content Adressable Delayed DFA z regulárních výrazů
Hammer, Jan ; Dvořák, Milan (oponent) ; Kaštil, Jan (vedoucí práce)
Práce se zabývá konstrukcí rozšířených typů konečných automatů ze sad regulárních výrazů.Hlavní důraz je na rozšíření CD2FA - Content Addressed Delayed Input DFA, které je navrženo k použití při hloubkové analýze paketů v síti, za účelem snížení paměťové náročnosti a zachování rychlosti výpočtu. Nad takto zkonstruovanými automaty jsou zkoumány statistiky paměťové náročnosti, které ukazují, že CD2FA jsou řádově desetkrát méně paměťově náročné, než původní DFA. Dále jsou prezentovány některá vylepšení procesu konstrukce CD2FA, především vylepšení přípravy adresace stavů za použití perfektního hashování.
|
|
|
Alternativní transformace jazykových modelů
Havel, Martin ; Beníčková, Zuzana (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce poskytuje ucelený přehled poznatků z oblasti regulárních výrazů, konečných automatů a transformací z regulárního výrazu na konečný automat. Práce navrhuje nové transformace se zaměřením na minimalizaci počtu stavů a počtu pravidel konečných automatů. Koncept alternativních transformací je zpracován do algoritmů a prokázán matematickým důkazy. Cílem práce je obohatit transformace o nové alternativy na poli regulárních výrazů a konečných automatů. Pozornost je především věnována ekonomické stránce finálního konečného automatu. V rámci práce se podařilo sestrojit algoritmy, které jsou schopny transformovat regulární výrazy na konečné automaty. Práce zároveň poskytuje návod k jejich implementaci. Prezentuje obecný koncept transformací, který umožňuje tvořit méně rozsáhlé konečné automaty. Využitím uvedeného přístupu je možné rozšířit řadu transformací o alternativní verze.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
|
Morfologický analyzátor pomocí konečných automatů
Bezák, Jakub ; Schwarz, Petr (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem tohoto textu je čtenáři co nejvíc přiblížit problematiku morfologie a morfologické analýzy slovenského jazyka s využitím morfologického analyzátoru a nastínit odlišnost od různých světových jazyků. Text také objasňuje význam hledání základního tvaru slov při analýze slovenských textů. V další části se věnuje optimálnímu uložení rozsáhlých slovníků pomocí konečných automatů s využitím jejich minimalizace. Nakonec jsou srovnáváný různé formy implementace.
|
|
|
Rozhodování WS1S pomocí symbolických automatů
Bednář, Pavel ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
WS1S je druhořádová logika s jednoduchou syntaxí a sémantikou, nabízející velkou stručnost popisu a rozhodnutelnost pomocí konečných automatů. Bohužel složitost rozhodovací procedůry je nonelementary, což na jednu stranu evokuje problém pro praktické aplikace, ale zároveň to představuje určitý prostor pro různé heuristiky a optimalizace. Nejpoužívanější nástroj v této oblasti, Mona, představuje ukázku toho, že konečné automaty s velkými abecedami mohou pracovat efektivně, a to díky BDD kódování přechodů. V této práci představíme novou rozhodovací procedůru pro WS1S, která zkombinuje klasický přístup s Mona přístupem tak, že přechody reprezentované pomocí BDD integrujeme přímo do automatu. Tím dosáhneme efektivity BDD přechodů, ale zároveň flexiblity díky používání čistě jen automatů a navíc oproti BDD můžeme přeskočit více proměnných nebo pracovat s nedeterminismem. Experimenty ukazují, že jsme schopni v některých oblastech konkurovat nástroji Mona a také dokážeme obecně tvořit automaty s méně stavy než Mona.
|
|
|
Ověřování parametrických vlastností nad záznamy běhů programů
Čaládi, Filip ; Fiedor, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Plogchecker 2.0 je nástroj zameraný na verifikáciu užívatelom definovaných vlastností nad sekvenciou udalostí generovaných programom. Implementácia tohoto nástroja stavá hlavne na už implementovanom nástroji Plogchecker. Hlavná mýšlienka týchto nástrojov je, že užívatel musí špecifikovať želané vlastnosti (parametrické alebo neparametrické), sprístupniť záznam behu programu verifikačnému nástroju a konečne prenechať analýzu na tento nástroj. Výstup analýzy je report o porušení špecifikovaných vlastností spolu so sekvenciami udalostí, ktoré spôsobili chybu. Táto práca predstavuje nový algoritmus , ktorý optimalizuje spracovanie sekvenie udalostí nad užívatelom definovanými vlastnosťami. Táto optimalizácia sa zameriava ako na škálovatelnosť tak aj presnosť. Ďalej, je pridaná podpora pre rôzne dátové typy parametrov, ako napríklad reťazec, číslo, dátum a čas. Nakoniec, táto práca ponúka jednoduchší a pohodlnejší spôsob vytvárania parametických vlastností. Počas experimentovania bolo ukázané, že Plogchecker 2.0 je schopný väčšej škálovatelnosti a presnosti.
|
host ::
RSS.