|
|
Turingovy stroje bez návratu na pásce
Surovič, Marek ; Vrábel, Lukáš (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce zavádí omezenou variantu Turingových strojů, které se nemohou pohybovat doleva, tedy se vracet na pásce. Ostatní vlastnosti Turingových strojů (například potenciálně nekonečná páska a schopnost přepisovat symboly na pásce) jsou zachovány. Zavedením tohoto omezení limitujeme vyjadřovací sílu Turingových strojů do té míry, ľe Turingovy stroje bez návratu na pásce jsou ekvivalentní s konečnými automaty a lze je na konečný automat transformovat. Dále je představen a detailně popsán algoritmus, který realizuje tuto transformaci.
|
|
|
Konstrukce zobecněného konečného automatu
Šoka, Martin ; Košař, Vlastimil (oponent) ; Kaštil, Jan (vedoucí práce)
Práce se zabývá vytvořením algoritmu pro konstrukci deterministického zobecněného konečného automatu. Tento automat se od obyčejného deterministického automatu liší tím, že jeho přechody jsou definovány slovy, na základě čeho je možné zredukovat počet stavů obyčejného deterministického automatu. V úvodě jsou vysvětleny základní pojmy, které jsou dále v práci používány. Dále práce popisuje algoritmus samotný, včetně podrobného popisu heuristiky k vyhledání maximálního acyklického podgrafu v grafu atomatu. Popsána je implementace algoritmu a experimentování s algoritmem vytvořenými automaty.
|
|
|
Generic Flow Analysis in Computer Networks
Jančová, Markéta ; Holkovič, Martin (oponent) ; Kolář, Dušan (vedoucí práce)
This diploma thesis focuses on the automatic network traffic description using models of communication. The main aim is at industrial control system protocols, especially IEC 60870-5-104 . We propose a method of characterizing the network state using both communication content and behavior in time viewpoints. These aspects are described using finite state automata , prefix trees , and recurrence analysis. In the second part of this thesis, we focus on the implementation of a program, which is capable to use the obtained model to verify network traffic in real-time.
|
|
| |
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
|
|
|
Generic Flow Analysis in Computer Networks
Jančová, Markéta ; Holkovič, Martin (oponent) ; Kolář, Dušan (vedoucí práce)
This diploma thesis focuses on the automatic network traffic description using models of communication. The main aim is at industrial control system protocols, especially IEC 60870-5-104 . We propose a method of characterizing the network state using both communication content and behavior in time viewpoints. These aspects are described using finite state automata , prefix trees , and recurrence analysis. In the second part of this thesis, we focus on the implementation of a program, which is capable to use the obtained model to verify network traffic in real-time.
|
|
|
Parametric Properties for Log Checker
Mutňanský, Filip ; Kočí, Radek (oponent) ; Smrčka, Aleš (vedoucí práce)
The goal of this thesis is to implement a tool that based on user defined properties can verify sequences of events in the traces of the program, or the log file. Properties are defined in extended regular expressions. The tool is able to verify parametric properties. User can define relations between parameters of events. Input of this tool is the definition of properties and constraints of parameters. Output of the tool is the report of violated properties with its sequences of events that caused the error.
|
|
|
Syntaktická analýza založená na speciálních modelech
Zámečníková, Eva ; Masařík, Karel (oponent) ; Lukáš, Roman (vedoucí práce)
Bakalářká práce se zabývá syntaktickou analýzou pomocí párových automatů. Konečný párový automat obsahuje vstupní a výstupní automat. Vstupní automat provádí syntaktickou analýzu se vstupním řetězcem. Použitá pravidla vstupního automatu řídí výstupní automat, který generuje výstupní řetězec. Hlavním tématem této práce je determinizace vstupního automatu bez ztráty informací o pravidlech použitých v původním automatu.
|
|
|
Dvoustranné automaty
Klouček, Miloš ; Holub, Štěpán (vedoucí práce) ; Kozlík, Andrew (oponent)
Práce se zabývá konečnými automaty a jejich schopností popisovat zajímavé třídy regulárních jazyků. Nejdříve je zavedena základní terminologie konečných automatů a formulovány jejich základní vlastnosti. Poté je pozornost věnována možnosti konečný automat rozšířit na dvoustranný automat přidáním zpětné přechodové funkce a zkoumání vlastností takto rozšířeného automatu. Důraz je kladen především na srovnání obdobných vlastností dvoustranných a konečných automatů. V druhé části práce je užitečnost nabytých poznatků demonstrována v podobě jednoduššího důkazu slavné Simonovy věty charakterizující po částech testovatelné jazyky. Tento důkaz je lehce modifikovaným výsledkem O. Klímy a L. Poláka. Powered by TCPDF (www.tcpdf.org)
|
|
|
Synchronizace konečných automatů
Vorel, Vojtěch ; Koubek, Václav (vedoucí práce) ; Pangrác, Ondřej (oponent)
Práce je úvodem do zkoumání synchronizačních slov konečných automatů a Černého domněnky. Podává přehled o důležitých výsledcích v oboru a metodách jejich dokazování, ale také o širokém spektru dosud nevyřešených otázek. Reprodukuje i důkazy některých nejnovějších výsledků, konkrétně Trakhtmanova horního odhadu obecného sycnhronizačního prahu a Steinbergova těsného odhadu pro jednoklastrové automaty s prvočíselnou délkou cyklu. V poslední kapitole se blíže zaměřujeme na problém synchronizace podmnožin a související výpočetní úlohy. Je zde prezentován nový dolní odhad maximálního synchronizačního prahu podmnožiny. Podařilo se také částečně určit časovou složitost jisté přirozeně omezené varianty PSPACE-úplné úlohy rozhodování o synchronizovanosti podmnožiny.
|
host ::
RSS.