|
|
Aproximativní techniky pro Markovovy modely
Andriushchenko, Roman ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Předkládaná práce je zaměřena na popis aproximativních technik pro analýzu Markovských řetězců, konkrétně na metody založené na agregaci nebo ořezávání stavového prostoru. Na začátku je představen postup umožňující aplikaci agregace pro modely diskrétního času s libovolnou strukturou stavového prostoru a je odvozen lepší odhad aproximační chyby. Daný postup je pak propojen s uniformizačními technikami, jak se standardní tak s adaptivní, což umožňuje provádět analýzu řetězců spojitého času spolu s odhadem aproximační chyby. Navržená technika spolu s existujícími metodami založenými na ořezávání byly implementovány v rámci nástroje PRISM. Provedené experimenty potvrzuji, že nově odvozený odhad aproximační chyby vylepšuje přesnost o několik řádů bez zhoršení celkové výkonnosti. Je ukázano, že výsledná agregační metoda je schopna poskytnout validní aproximaci modelu spolu s adekvátními odhady aproximační chyby, a to jak v diskrétním tak i ve spojitém čase. Následně je provedeno porovnání s technikami založenými na ořezávání stavového prostoru a je diskutováno pro které třídy Markovských řetězců je ta či ona metoda použitelnější. Nakonec je demonstrováno úspěšne použití aproximativních technik pro model checking Markovových modelů.
|
|
|
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.
|
|
|
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.
|
|
|
A Haskell Platform for Creating Progressive Web Applications
Zárybnický, Jakub ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
This work attempts to ease developing browser applications in the Haskell programming language by creating a set of components that its library ecosystem so far lacks, especially focusing on the components required for development of Progressive Web Applications, applications that use new technologies like Service Workers. The thesis compares which components are commonly expected from a web framework and which are available in Haskell; describes the implementation of three such components (router, storage, and Service Worker libraries); and implements three applications that demonstrate use of these components.
|
|
|
Konjunkce a disjunkce ve fuzzy logice
Havlena, Vojtěch ; Kunovský, Jiří (oponent) ; Křena, Bohuslav (vedoucí práce)
Tato práce se věnuje triangulárním normám a jejich zobecněním - uninormám, zejména jejich transformacím pomocí jednotkové funkce, a také modelování fuzzy logické konjunkce a disjunkce na základě empirických dat. Byly stanoveny podmínky, při nichž transformací určitých uninorem vznikne opět uninorma. Taktéž byly určeny podmínky invariantnosti transformace pro třídu určitých uninorem. Transformace uninorem rozšiřuje třídu možných spojek a jejich studium nám ulehčilo hledání podmínek při modelování. Byl také nalezen a analyzován algoritmus pro modelování fuzzy logických spojek. Na základě programu implementujícího tento algoritmus byl vyhodnocen experiment, který měl za cíl modelovat fuzzy konjunkci užívanou lidmi.
|
|
|
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.
|
|
|
Automatický theorem prover
Mazánek, Martin ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování.
|
|
|
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.
|
|
|
Just-in-Time Compilation of Dependently-Typed Lambda Calculus
Zárybnický, Jakub ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
A number of programming languages have managed to greatly improve their performance by replacing their custom runtime system with general platforms that use just-in-time optimizing compilers like GraalVM or RPython. This thesis evaluates whether such a transition would also benefit dependently-typed programming languages or theorem provers. This thesis introduces the type-theoretic notion of dependent types and the algorithms involved in working with them, specifies a minimal dependently-typed language on the -calculus, and presents the implementation two interpreters for this language: a simple interpreter written in Kotlin, and a second interpreter, also written in Kotlin, that uses the Truffle language implementation framework on the GraalVM platform, which is a partial evaluation-based just-in-time compiler based on the Java Virtual Machine. The performance of these two interpreters is then compared on a number of normalization and elaboration tasks.The results are strongly negative, however, the influence of JIT compilation is not noticeable given the large overhead of the JVM platform. This thesis concludes with a number of alternative projects that would use the capabilities of Truffle better.
|
|
|
Beyond Register Automata: Pushing the Border of Decidability
Gulčíková, Sabína ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Register automaton (RA) operating over infinite alphabet is one of the great tools for pattern matching with backreferences, runtime verification, or modelling of parallel computation. In case of pattern matching with backreferences, the state-of-the-art matchers make use of backtracking algorithms, whose application causes significant slowdown in case of nondeterministic regular expressions. Since RAs cannot always be determinised, it is an unsuitable model for solution to problems related to inefficient usage of backtracking algorithms. On the other hand, the RA's quality of being equipped by a finite memory serves as a good basis for storing the so-called capture groups used in pattern matching with backreferences. In this work, a formal model called register set automaton (RsA) is proposed. A large class of RAs can be transformed into this deterministic model, which, among other things, allows for fast pattern matching with backreferences. We explore RsA's properties including decidability of emptiness testing, determinisability, closure under Boolean operations and we compare it to other register models in context of their expressive power.
|
host ::
RSS.