|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (referee) ; Holík, Lukáš (advisor)
Nedeterministické konečné automaty (NKA) jsou široce využívány v počítačové vědě, například v oblasti formálních jazyků pro reprezentaci regulárních jazyků, k monitorování vysokorychlostních sítí, rozpoznávání obrazu, modelování hardware, nebo dokonce v bioinformatice pro vyhledávání sekvencí nukleotidových kyselin v DNA. NKA jsou také používány v abstraktním regulárním model checkingu, dále ve verifikaci programů manupulujících s řetězci, ve verifikaci programů využívajících ukazatele, pro konstrukci lineárních rovnic a nerovnic, v rozhodovacích procedurách WS1S a WS2S logiky a mnohých dalších. Minimalizace automatů je základní technikou, která pomáhá snižovat nároky na zdroje (paměť, čas nebo množství hardwarových komponentů) a urychlovat operace prováděné na automatech. Běžně používané minimalizační techniky, jakými jsou slučování stavů, odstraňování hran přechodů nebo saturace, mohou v automatech zanechat potenciální minimalizovatelné podgrafy obsahující duplicitní jazykovou informaci. Tyto fragmenty sestávají ze skupiny stavů, kde je již část jazyka jednoho stavu pokryta jazyky ostatních stavů z této skupiny. Tato práce popisuje novou techniku využívající SAT solver, který poskytuje informaci umožňující minimalizovat tyto doposud neminimalizovatelné části automatů. Nově vyvíjená metoda, která využívá pouze informaci od SAT solveru a slučování stavů minimalizuje automaty podobně efektivně, a v případě automatů s nízkým počtem přechodů dokonce rychleji než nástroj RABIT/Reduce, který využívá slučování stavů a odstraňování hran.
|
|
|
Development of Dataster Tool
Vlach, Martin ; Holík, Lukáš (referee) ; Smrčka, Aleš (advisor)
This bachelor thesis deals with expansion of existing web application Dataster in Testos platform. This application serves as a user interface for dbgenx tool from the same platform. The main purpose of Dataster is a user-friendly generation of randomized structured data which are used as a database test content. The first goal of this bachelor thesis was, in particular, to extend dbgenx tool with the possibility of generating test data according to the coverage criteria of combinatorial testing. An existing tool Combine from Testos platform has been selected for this purpose. The other part of the thesis deals with a number of small adjustments and expansion of Dataster web application, for a improvement of usability and overall user-friendliness of this application.
|
|
|
Incremental Inductive Coverability for Alternating Finite Automata
Vargovčík, Pavol ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
In this work, we propose a specialization of the inductive incremental coverability algorithm that solves alternating finite automata emptiness problem. We experiment with various design decisions, analyze them and prove their correctness. Even though the problem itself is PSpace-complete, we are focusing on making the decision of emptiness computationally feasible for some practical classes of applications. We have obtained interesting comparative results against state-of-the-art algorithms, especially in comparison with antichain-based algorithms.
|
|
|
Cooperative Project Planning in Getting Things GNOME
Matušov, Izidor ; Holík, Lukáš (referee) ; Smrčka, Aleš (advisor)
This work dicusses the extension for Getting Things GNOME which makes it possible to use it for planning and managment of cooperative projects. Reader is introduced to basics of project planning and project management and selected methods. The target audience and their needs for the extension were identified and their solutions were proposed. This work includes a walkthrough the extension of the user interface in the form of wireframes. The proposed extension was implemented and tested.
|
|
|
Living in the suburbs
Holík, Lukáš ; Klimecký, Martin (referee) ; Gerö, Jiří (advisor) ; Pěnčík, Jan (advisor)
The aim of this bachelor's thesis was to create a low-energy / passive building located on the suburbs of the city Brno and which would serve for permanent housing. The land on which the building is to be located is currently mostly green. The ratio of the green area did not change from a bird's eye view, it only moved to other height levels. The majority of the proposed area is therefore greenery, in the form of green roofs. The resulting design consists of two two-storey buildings, which are separated by a green roof of garages located below ground level. However, it is one complex building, in which there are a total of 8 independent housing units of various sizes with gardens and terraces. The southern sides of the facades of both buildings form mainly glazed areas facing the gardens of the individual housing units. At the same time, large glass areas use as much southern light as possible, as both eastern and western in the design cannot be sufficiently used. This bachelor's thesis is based on the subject of studio work from the second year.
|
|
|
Translation of LTL with Bounded Repetition to Automata with Counters
Slezáková, Alexandra ; Smrčka, Aleš (referee) ; Holík, Lukáš (advisor)
This work solves translation of LTL with bounded repetition (temporal operators that have limited validity for a certain number of steps) to automaton with counters. Using classical methods, the automaton representation of such formulas is large, because the size of automaton may be exponential to the upper limit of the bounded repetition. We present a construction that creates the automaton independent from repetition. The work represents a solution to the problem using the Büchi automaton with counters. The counters ensure that similar states and transitions are not created, which leads to a reduction in the size of the automaton. Our method is implemented and experimentally verified. We reduce the number of states of the automaton for formulas with large bound of operators several times in comparison to classical methods.
|
|
|
Business Plan
Holík, Lukáš ; Novák, Zdeněk (referee) ; Rompotl, Jaroslav (advisor)
The goal of this dissertation is to create a business plan for mr. David Mokrý - owner of café Blue Queen in Boskovice. In a short time he would like to make his business bigger and found another café - pub (Black King).The needed data for creating a project of new successful restaurant, which should become the most popular in selected location, I'm going to get by many market analyses, respective by analyses of internal and external neighborhood.
|
|
|
Advanced Methods for Synthesis of Probabilistic Programs
Stupinský, Šimon ; Holík, Lukáš (referee) ; Češka, Milan (advisor)
Pravdepodobnostné programy zohrávajú rozhodujúcu úlohu v rôznych technických doménach, ako napríklad počítačové siete, vstavané systémy, stratégie riadenia spotreby energie alebo softvérové produčkné linky. PAYNT je nástroj na automatizovanú syntézu pravdepodobnostných programov vyhovujúcich zadaným špecifikáciam. V tejto práci rozširujeme tento nástroj predovšetkým o podporu optimálnej syntézy a syntézy viacerých špecifikácií. Ďalej sme navrhli a implementovali novú metódu, ktorá dokáže efektívne syntetizovať parametre so spojitým definičným oborom ovplyvňujúce pravdepodobnostné prechody popri syntéze topológie programov, t.j., podporu pre syntézu topológie aj parametrov súčasne. Demonštrujeme užitočnosť a výkonnosť nástroja PAYNT na širokej škále prípadových štúdií z rôznych aplikačných domén ktoré majú uplatnenie v reálnom svete. Pri náročných problémoch syntézy môže PAYNT výrazne znížiť dobu behu až z dní na minúty a zároveň zaistiť úplnosť procesu syntézy.
|
|
|
A BDD Library
Troška, Karol ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Binary decision program is a data structure used in many areas of information technology. This thesis describes BDD as a mathematical formalism and proposes possible representation of BDD in a computer. The propose is focused mainly on a reduction speed of number of memory allocation and on a simplicity and an intuitive system of using a library. There are several examples of a library usage and warnings which programmer should avoid of in the thesis. Proposed representation was implemented in C language.
|
|
|
Simulation for Symbolic Automata
Síč, Juraj ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Symbolic automata are similar to classical automata with one big difference: transitions are labelled with predicates defined in separate logical theory. This allows usage of large alphabets while taking less space. In this work we are interested in computing simulation (a binary relation on states that language inclusion) for these automata. This can be then used for reducing the size of automata without the need to determinize them first. There exist few algorithms for computing simulation over Kripke structures, which were then altered to work over labeled transition systems and classical automata. We show how one of these algorithms can be modified for symbolic automata by using the partition of the alphabet domain that is compatible with the predicates labelling transitions and by using the possibilities of the alphabet theory.
|
guest ::
RSS feed.