Národní úložiště šedé literatury Nalezeno 13,130 záznamů.  1 - 10dalšíkonec  přejít na záznam: Hledání trvalo 1.13 vteřin. 

An Algorithm for Formal Safety Verification of Complex Heterogeneous Systems
Ratschan, Stefan
Modern technical systems are heterogeneous in the sense that they tightly integrate computational elements into physical surroundings. Computational elements usually require discrete, and physical systems continuous modeling. In this paper, we present an modeling formalism and safety verification algorithm for such heterogeneous systems.

Modelling, parameter estimation, optimisation and control of transport and reaction processes in bioreactors.
ŠTUMBAUER, Václav
With the significant potential of microalgae as a major biofuel source of the future, a considerable scientific attention is attracted towards the field of biotechnology and bioprocess engineering. Nevertheless the current photobioreactor (PBR) design methods are still too empirical. With this work I would like to promote the idea of designing a production system, such as a PBR, completely \emph{in silico}, thus allowing for the in silico optimization and optimal control determination. The thesis deals with the PBR modeling and simulation. It addresses two crucial issues in the current state-of-the-art PBR modeling. The first issue relevant to the deficiency of the currently available models - the incorrect or insufficient treatment of either the transport process modeling, the reaction modeling or the coupling between these two models. A correct treatment of both the transport and the reaction phenomena is proposed in the thesis - in the form of a unified modeling framework consisting of three interconnected parts - (i) the state system, (ii) the fluid-dynamic model and (iii) optimal control determination. The proposed model structure allows prediction of the PBR performance with respect to the modelled PBR size, geometry, operating conditions or a particular microalgae strain. The proposed unified modeling approach is applied to the case of the Couette-Taylor photobioreactor (CTBR) where it is used for the optimal control solution. The PBR represents a complex multiscale problem and especially in the case of the production scale systems, the associated computational costs are paramount. This is the second crucial issue addressed in the thesis. With respect to the computational complexity, the fluid dynamics simulation is the most costly part of the PBR simulation. To model the fluid flow with the classical CFD (Computational Fluid Dynamics) methods inside a production scale PBR leads to an enormous grid size. This usually requires a parallel implementation of the solver but in the parallelization of the classical methods lies another relevant issue - that of the amount of data the individual nodes must interchange with each other. The thesis addresses the performance relevant issues by proposing and evaluation alternative approaches to the fluid flow simulation. These approaches are more suitable to the parallel implementation than the classical methods because of their rather local character in comparison to the classical methods - namely the Lattice Boltzmann Method (LBM) for fluid flow, which is the primary focus of the thesis in this regard and alternatively also the discrete random walk based method (DRW). As the outcome of the thesis I have developed and validated a new Lagrangian general modeling approach to the transport and reaction processes in PBR - a framework based on the Lattice Boltzmann method (LBM) and the model of the Photosynthetic Factory (PSF) that models correctly the transport and reaction processes and their coupling. Further I have implemented a software prototype based on the proposed modeling approach and validated this prototype on the case of the Coutte-Taylor PBR. I have also demonstrated that the modeling approach has a significant potential from the computational costs point of view by implementing and validating the software prototype on the parallel architecture of CUDA (Compute Unified Device Architecture). The current parallel implementation is approximately 20 times faster than the unparallized one and decreases thus significantly the iteration cycle of the PBR design process.

Role of Psb28 proteins in the biogenesis of the Photosystem II complex in the cyanobacterium Synechocystis sp. PCC 6803
BEČKOVÁ, Martina
The thesis focuses on the role of Psb28 proteins, namely the Psb28-1 and its homolog Psb28-2, in the biogenesis of the Photosystem II complex (PSII) in the cyanobacterium Synechocystis PCC 6803. The aims of this work were to localize the proteins within the cells, and to determine their function. A fraction of both Psb28 proteins was identified in the monomeric PSII core complexes but most proteins were found in the unassembled protein fraction associated with thylakoid membranes. Psb28-1 was mostly detected as a dimer while Psb28-2 as a monomer. Psb28-1 also differed from Psb28-2 by its higher affinity to the PSII core complex lacking CP43 antenna. Characterization of Psb28-less mutants suggested regulatory function of the proteins in PSII biogenesis in connection with chlorophyll biosynthetic pathway. Analysis of preparations isolated using FLAG-tagged versions of Psb28 proteins showed their association with Photosystem II - Photosystem I supercomplexes, especially under increased irradiance, and supported a role of Photosystem I in the PSII biogenesis.

Alban Berg: "Vojcek" - komplexní scénografický projekt
Ermakova, Olga ; ZÁBRODSKÁ, Dana (vedoucí práce) ; DAVID, Milan (oponent)
Tématem mé bakalářské práce je zpracování komplexního scénografického projektu k opeře Vojcek. V první části je obsažen životopis dramatika Georga Büchnera, autora hry a skladatele Albana Berga, autora hudby. Následuje popis děje Vojcka a analýza alternativních zpracování Vojcka. V závěru práce představuji koncept k teoretické části mého bakalářského projektu. Součástí konceptu jsou obrázky mé scény a kostýmů. V přílohách jsou obsaženy i fotky kostýmů v reálném prostředí.

Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating

Acceleration of Object Detection Using Classifiers
Juránek, Roman ; Kälviäinen, Heikki (oponent) ; Sojka, Eduard (oponent) ; Zemčík, Pavel (vedoucí práce)
Detection of objects in computer vision is a complex task. One of most popular and well explored  approaches is the use of statistical classifiers and scanning windows. In this approach, classifiers learned by AdaBoost algorithm (or some modification) are often used as they achieve low error rates, high detection rates and they are suitable for detection in real-time applications. Object detection run-time which uses such classifiers can be implemented by various methods and properties of underlying architecture can be used for speed-up of the detection.  For the purpose of acceleration, graphics hardware, multi-core architectures, SIMD or other means can be used. The detection is often implemented on programmable hardware.  The contribution of this thesis is to introduce an optimization technique which enhances object detection performance with respect to an user defined cost function. The optimization balances computations of previously learned classifiers between two or more run-time implementations in order to minimize the cost function.  The optimization method is verified on a basic example -- division of a classifier to a pre-processing unit implemented in FPGA, and a post-processing unit in standard PC.

Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which nonterminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs.

Acceleration Methods for Evolutionary Design of Digital Circuits
Vašíček, Zdeněk ; Miller, Julian (oponent) ; Zelinka,, Ivan (oponent) ; Sekanina, Lukáš (vedoucí práce)
Although many examples showing the merits of evolutionary design over conventional design techniques utilized in the field of digital circuits design have been published, the evolutionary approaches are usually hardly applicable in practice due to the various so-called scalability problems. The scalability problem represents a general problem that refers to a situation in which the evolutionary algorithm is able to provide a solution to a small problem instances only. For example, the scalability of evaluation of a candidate digital circuit represents a serious issue because the time needed to evaluate a candidate solution grows exponentially with the increasing number of primary inputs. In this thesis, the scalability problem of evaluation of a candidate digital circuit is addressed. Three different approaches to overcoming this problem are proposed. Our goal is to demonstrate that the evolutionary design approach can produce interesting and human competitive solutions when the problem of scalability is reduced and thus a sufficient number of generations can be utilized. In order to increase the performance of the evolutionary design of image filters, a domain specific FPGA-based accelerator has been designed. The evolutionary design of image filters is a kind of regression problem which requires to evaluate a large number of training vectors as well as generations in order to find a satisfactory solution. By means of the proposed FPGA accelerator, very efficient nonlinear image filters have been discovered. One of the discovered implementations of an impulse noise filter consisting of four evolutionary designed filters is protected by the Czech utility model. A different approach has been introduced in the area of logic synthesis. A method combining formal verification techniques with evolutionary design that allows a significant acceleration of the fitness evaluation procedure was proposed. The proposed system can produce complex and simultaneously innovative designs, overcoming thus the major bottleneck of the evolutionary synthesis at gate level. The proposed method has been evaluated using a set of benchmark circuits and compared with conventional academia as well as commercial synthesis tools. In comparison with the conventional synthesis tools, the average improvement in terms of the number of gates provided by our system is approximately 25%. Finally, the problem of the multiple constant multiplier design, which belongs to the class of problems where a candidate solution can be perfectly evaluated in a short time, has been investigated. We have demonstrated that there exists a class of circuits that can be evaluated efficiently if a domain knowledge is utilized (in this case the linearity of components).

High-Quality Shadow Rendering from Complex Light Sources
Navrátil, Jan ; Sochor, Jiří (oponent) ; Navrátil, Jan (oponent) ; Zemčík, Pavel (vedoucí práce)
In interactive applications, shadows are traditionally rendered using the shadow mapping algorithm. The disadvantage of the algorithm is limited resolution of depth texture which may lead to unpleasant visual artifacts on shadow edges. This work introduces an approach that is based on the improved texture warping. It allows for rendering a scene with the complex light sources, reduce the artifacts on the shadow boundaries and also improve the quality of the shadows regardless of the type of the scene and its configuration.

Hydrobiologie poříčních tůní dolního Podyjí v souvislosti s obnovou hydrologického režimu lužního lesa
Heteša, Jiří ; Keršner, Vladimír ; Marvan, Petr ; Sukop, I.
Poříční tůně dolního Podyjí byly výrazně ovlivněny regulací řeky a výstavbou tří mělkých nádrží v 70. a 80. letech. V důsledku poklesu hladiny spodní vody zaniklo mnoho periodických tůní a byla ohrožena existence mnoha živočišných i rostlinných druhů a s nimi i celého komplexu lužního lesa. Na druhé straně našly na mnohých lokalitách se zvýšenou koncentrací elektrolytů slanomilné rozsivky. Dotace vody z řeky Dyje do těchto tůní je však spojena s rizikem snížení původní biodiverzity a zavlečení nežádoucích druhů, zejména sinic.