|
|
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.
|
|
|
Reduction of CentOS operating system
Vashkevich, Pavel ; Caha, Tomáš (referee) ; Komosný, Dan (advisor)
The goal of this bachelor's thesis is to perform a reduction of the Linux operating system. For minimalization was entered the Linux distribution CentOS 8, which is created on the basis of open-source code. This code are spread by Red Hat. The theoretical part describes the basic components of the operating system, including the Linux kernel, drivers and graphical interface. The practical part describes the suggestion of a method for minimizing the operating system. This method also includes a comparison of lightweight web browsers. The resulting size after reduction is 731 MB. Minimization automation software is published in the personal repository on GitHub under the MIT license.
|
|
| |
|
| |
|
|
Democratic deficit of the EU: options of evolvement
Tomášová, Tereza ; Šlosarčík, Ivo (advisor) ; Weiss, Tomáš (referee)
Diploma thesis " Democratic deficit of the EU: options of evolvement" deals with democracy and democratic legitimacy of the European Union. It represents a particular concept of the EU's democratic deficit, which is ambiguous term, but generally indicates a lack of democracy- particularly the lack of popular participation in the governance or a lack of democratic legitimacy of EU institutions and decision-making. The aim of my work was, according to the hypotheses to determine what is causing the EU's democratic deficit, whether it is a serious problem that should be addressed at European level, and if so, what are the possibilities for minimizing or further evolvement. To explore this issue further, I examine the theory of democratic legitimacy in the introduction and divide it into the "input and output" legitimacy. Subsequently, I also introduced methodology and the current debate on democratic deficit in the leading periodicals, dealing with the EU and think tanks. The second part deals with the history of the democratic deficit and its various definitions, follows with a presentation of my two hypotheses dealing with the question whether or not the EU's democratic deficit is a problem. In the third part, my two hypotheses are tested on the project of the Single European Sky, which aims to...
|
|
|
Library for Operations over Finite Automata
Bartůněk, Petr ; Puš, Viktor (referee) ; Kaštil, Jan (advisor)
This work deals with two basic operations over finite automata. Determination of nondeterministic finite automata and minimization of deterministic finite automata. For these two operations I proposed sequential algorithms that are parallelizable. I deal mainly with finding the speedup of SSE instructions, or use the OpenMP library. The trend today is mainly in increasing the number of processors, so I propose parallel algorithms for multiple processors. When searching for the optimal solution, I will be to examine other ways to achieve speedup, for example efficient saving of the data structures in memory.
|
|
|
Reduction of the Nondeterministic Finite Automata
Procházka, Lukáš ; Kořenek, Jan (referee) ; Kaštil, Jan (advisor)
Nondeterministic finite automaton is an important tool, which is used to process strings in many different areas of programming. It is important to try to reduce its size for increasing programs' effectiveness. However, this problem is computationally hard, so we need to search for new techniques. Basics of finite automata are described in this work. Some methods for their reduction are then introduced. Usable reduction algorithms are described in greater detail. Then they are implemented and tested. The test results are finally evaluated.
|
|
|
Evolutionary Combinational Circuit Resynthesis
Pták, Ondřej ; Schwarz, Josef (referee) ; Sekanina, Lukáš (advisor)
This project deals with combinational digital circuits and their optimization. First there are presented main levels of abstraction utilized in the design of combinational digital circuits. Afterwards different methods are surveyed for optimization of combinational digital circuits. The next part of this project is mainly devoted to evolutionary algorithms, their common characteristics and branches: genetic algorithms, evolutionary strategies, evolutionary programming and genetic programming. The variant of genetic programming called Cartesian Genetic Programming (CGP) and the use of CGP in various areas, particularly in the synthesis and optimization of combinational logic circuits are described in detail. The project also discusses some modifications of CGP and the scalability problem of evolutionary circuit design. Consequential part of this thesis describes the method for evolution resynthesis of combinational digital circuits. There is description of design, especially the method of splitting circuits into subcircuits, and implementation details. Finally experiments with these method and their results are described.
|
|
|
Design and optimization of hydrostatic pocket space
Minář, Petr ; Pavlík, Jan (referee) ; Blecha, Petr (advisor)
This diploma thesis deals with an optimization of hydrostatic slide of the large-portal gantry machine FRU (TOS Kuřim). First part of the thesis concerns with an analysis of the current practice in hydrostatic guides in the field of heavy gantry machines, an usage of alternative materials for a construction of carrying parts of machines, and possibilities of current simulation methods. Aim of the second part of this thesis is a brief clarification of the principle of mathematical optimization, and creation of general methodology of construction optimization by means of system analysis. Optimization calculations were processed by ANSYS Workbench 11.0. There is achieved adjusted and optimized design of the hydrostatic slide as the result of the thesis. Moreover, the comparison of key deformations was added. Created methodology is applicable in both an area of construction of gantry machines, and a wide spectrum of construction fields.
|
|
|
Optimization of an aircraft wing rib
Kopřiva, Lubomír ; Suchánek, Miroslav (referee) ; Petruška, Jindřich (advisor)
Topology optimization is a method providing new direction in designing of a technical objects. The aim of topology optimization is to find optimal distribution of material in design space. This diploma thesis is focused on optimization of aircraft wing rib num.6 of the airplane EV-55 using a software HW/Optistruct 7.0 implemented in a software package HyperWorks 7.0. The optimization of the rib was calculated under four different load cases. Resulting shapes of the rib were then tested by strenght calculations in software ANSYS 10.0. Finally, the obtained data of weights of optimized ribs were compared with the weight of the original rib.
|
guest ::
