|
Optický rezonátor s nízkou disperzí pro účely délkového senzoru využivající optický frekvenční hřeben
Pravdová, Lenka ; Hucl, Václav ; Lešundák, Adam ; Lazar, Josef ; Číp, Ondřej
Ultra přesná měření délky jsou doménou laserových interferometrů. Na našem pracovišti jsme navrhli a experimentálně ověřili metodu měření s optickým rezonátorem, která využívá širokospektrálního záření optického frekvenčního hřebene. Měřená délka, tj. délka rezonátoru, je pak převedena na hodnotu opakovací frekvence pulsního laseru se synchronizací modů optického frekvenčního hřebene. V našem příspěvku nyní představujeme porovnání absolutní stupnice optického rezonátoru se stupnicí inkrementálního interferometru. Inkrementální interferometr je do sestavy implementován pro provedení požadované verifikace stupnice optického rezonátoru. Dvousvazkový inkrementální interferometr pracuje na vlnové délce 633 nm a měřicí zrcadlo rezonátoru vybavené piezo posuvem je s výhodou použito zároveň i jako zpětný odrážeč pro tento interferometr. Jako markantní chybový signál se zde projevuje periodická nelinearita stupnice inkrementálního interferometru. Relativní rozlišení naší metody tak dosahuje hodnoty až 10-9 při zachování absolutní stupnice měření.\n
|
| |
|
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.
|
|
Grammars with Restricted Derivation Trees
Koutný, Jiří ; Janoušek, Jan (oponent) ; Vojnar, Tomáš (oponent) ; Meduna, Alexandr (vedoucí práce)
This doctoral thesis studies theoretical properties of grammars with restricted derivation trees. After presenting the state of the art concerning this investigation area, the research is focused on the three main kinds of the restrictions placed upon the derivation trees. First, it introduces completely new investigation area represented by cut-based restriction and examines the generative power of the grammars restricted in this way. Second, it investigates several new properties of path-based restriction placed upon the derivation trees. Specifically, it studies the impact of erasing productions on the generative power of grammars with restricted path and introduces two corresponding normal forms. Then, it describes a new relation between grammars with restricted path and some pseudoknots. Next, it presents a counterargument to the generative power of grammars with controlled path that has been considered as well-known so far. Finally, it introduces a generalization of path-based restriction to not just one but several paths. The model generalized in this way is studied, namely its pumping, closure, and parsing properties.
|
|
Formal Systems Based on Automata and Grammars
Čermák, Martin ; Rybička, Jiří (oponent) ; Šaloun, Petr (oponent) ; Meduna, Alexandr (vedoucí práce)
The present thesis continues with study of grammar and automata systems. First of all, it deals with regularly controlled CD grammar systems with phrase-structure grammars as components. Into these systems, three new derivation restrictions are placed and their effect on the generative power of these systems are investigated. Thereafter, this thesis defines two automata counterparts of canonical multi-generative nonterminal and rule synchronized grammar systems, generating vectors of strings, and it shows that these investigated systems are equivalent. Furthermore, this thesis generalizes definitions of these systems and establishes fundamental hierarchy of n-languages (sets of n-tuples of strings). In relation with these mentioned systems, automaton-grammar translating systems based upon finite automaton and context-free grammar are introduced and investigated as a mechanism for direct translating. At the end, in this thesis introduced automata systems are used as the core of parse-method based upon n-path-restricted tree-controlled grammars.
|
|
Navigace mobilních robotů
Rozman, Jaroslav ; Matoušek,, Václav (oponent) ; Šolc, František (oponent) ; Zbořil, František (vedoucí práce)
Mobilní robotika je v posledních letech velice diskutované a rozšířené téma. Souvisí to především se stále se zdokonalující výpočetní technikou, která tak umožňuje vyvíjet stále složitější a dokonalejší roboty. Cílem tohoto snažení je vytvořit robota, schopného se autonomně pohybovat ve zvoleném prostředí. Pro tento úkol je nutné, aby si robot vytvořil mapu, ve které bude svůj pohyb plánovat. V současné době se za standard v mapování považují pravděpodobnostní algoritmy založené na metodě SLAM. Tato disertační práce se zabývá návrhem plánovacího algoritmu právě pro metodu SLAM. Popisuje plánování pohybu pro robota vybaveného dvojicí kamer, tzv. stereokamerou, umístěnou na pohyblivé platformě. Plánování pohybu je navržené s ohledem na použití algoritmů, které budou v obraze ze stereokamery vyhledávat význačné body a z těch pak pomocí triangulace tvořit mapu, nebo také model prostředí. Přínos práce by se dal rozdělit do tří částí. V první je popsán způsob vyznačování plochy, ve které pak bude robot plánovat svůj pohyb. Druhá část se zabývá samotným plánováním pohybu robota v této mapě. Bere při tom v úvahu vlastnosti algoritmu SLAM a snaží se tedy toto plánování navrhnout tak, aby vytvořená mapa byla co nejpřesnější. Ve třetí části je pak popsán pohyb platformy, která nese kamery. V této části se využívá toho, že robot může svými kamerami sledovat i jiná místa, než jsou ta ve směru jeho pohybu. To mu umožní prozkoumat mnohem větší prostor bez přílišné ztráty informace o své přesné poloze.
|
|
Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (oponent) ; Yamamura,, Akihito (oponent) ; Meduna, Alexandr (vedoucí práce)
This doctoral thesis studies synchronous formal systems based on grammars and transducers, investigating both theoretical properties and practical application perspectives. It introduces new concepts and definitions building upon the well-known principles of regulated rewriting and synchronization. An alternate approach to synchronization of context-free grammars is proposed, based on linked rules. This principle is extended to regulated grammars such as scattered context grammars and matrix grammars. Moreover, based on a similar principle, a new type of transducer called the rule-restricted transducer is introduced as a system consisting of a finite automaton and context-free grammar. New theoretical results regarding the generative and accepting power are presented. The last part of the thesis studies linguistically-oriented application perspectives, focusing on natural language translation. The main advantages of the new models are discussed and compared, using select case studies from Czech, English, and Japanese to illustrate.
|
|
Security of Biometric Systems
Lodrová, Dana ; Busch, Christoph (oponent) ; Provazník, Ivo (oponent) ; Drahanský, Martin (vedoucí práce)
The main contributions of this thesis are two novel approaches for the increase of securing of biometric systems based on fingerprint recognition. The first approach is within the liveness detection and prevents the use of various fake fingers and other spoofing techniques during the capturing processes. This patented approach is based on a combination of change of papillary line color and width caused by pressing of a finger against glass plate. The resultant liveness detection unit can be integrated into an optical fingerprint sensor. The second approach is within standardization and it increases the security and interoperability of minutiae extraction and comparison process. For this purposes, I have created the methodology to determine semantic conformance rates of minutiae extractors. The minutiae extracted by the tested extractors are compared against Ground-Truth-Minutiae obtained by clustering of data provided by dactyloscopic/forensic experts. This proposed methodology is included in the ISO/IEC 29109-2 Amd. 2 WD4.
|
|
Optimalizace sledování síťových toků
Žádník, Martin ; Lhotka,, Ladislav (oponent) ; Matoušek, Radomil (oponent) ; Sekanina, Lukáš (vedoucí práce)
Tato disertační práce se zabývá optimalizací sledování síťových toků. Sledování síťových toků spočívá ve sledování jejich stavu a je klíčovou úlohou pro řadu síťových aplikací. S každým příchodem paketu je nutné aktualizovat hodnoty stavu, což zahrnuje přístupy do paměti. Vzhledem k vysoké propustnosti linek a obrovskému množství souběžných toků hraje přístup do paměti kritickou roli ve výkonnosti stavového zpracování síťového provozu. Tento problém se řeší různými technikami. Tyto techniky ale ve výsledku vždy požadují, aby nejblíže zpracování provozu byla nasazena paměť s nízkou odezvou, cache toků, schopná vyřídit všechny přístupy. Cache toků má proto omezenou kapacitu a její efektivní správa má zásadní vliv na výkonnost a výsledky zpracování síťového provozu. Vzhledem ke specifikům síťového provozu nemusí být stávající správy vhodné pro správu cache toků. Disertační práce se proto zabývá automatizovaným vývojem správy cache na základě reálného provozu dané sítě. Automatizace vývoje správy cache toků je realizována pomocí genetického algoritmu. Genetický algoritmus vyvíjí nová řešení a hodnotí je simulací nad vzorkem provozu z různých sítí. Navržený postup je ověřen na vývoji správ pro dva problémy. Prvním problémem je vývoj správy, která bude vykazovat celkově nízký počet výpadků stavů z cache toků. Druhým problémem je vývoj správy, která bude vykazovat velmi nízký počet výpadků u velkých toků. Optimalizace zakódování správy a experimenty s parametry genetického algoritmu ukázují, že je možné nalézt správy cache toků, které jsou optimalizované pro specifika daného nasazení. Nově vyvinuté správy poskytují lepší výsledky než ostatní testované správy. Z hlediska snížení celkového počtu výpadků je vyvinuta správa, která snižuje počet výpadků na konkrétní datové sadě až o deset procent vůči nejlepší porovnávané správě. Z pohledu snížení počtu výpadků u velkých toků je dosaženo vyvinutou správou až dvojnásobného snížení výpadků. Většina velkých toků (více než 90%) nezaznamenala při použití vyvinuté správy dokonce ani jeden výpadek. Rovněž během záplav nových toků, které se v síťovém provozu vyskytují v souvislosti se skenováním sítí a útoky, se ukazují velmi dobré vlastnosti vyvinuté správy. V rámci práce je rovněž navrženo rozšíření správy o využití doplňkové informace ze záhlaví příchozích paketů. Výsledky ukazují, že kombinací této informace lze počet výpadků u správ dále snižovat.
|
|
Čerpadlo s difuzorem s použitím stochastických lopatek (oběžné kolo i difuzor)
Dobšáková, Lenka ; Melichar, Jan (oponent) ; Veselý, Jindřich (oponent) ; Haluza, Miloslav (vedoucí práce)
Tato dizertační práce se zabývá studiem nerovnoměrné lopatkové mříže u odstředivých čerpadel. Vliv nerovnoměrné lopatkové mříže je zkoumána u oběžného i rozváděcího kola. Nerovnoměrné lopatkování kol čerpadla je v této práci zkoumáno z hlediska vlivu na účinnostní charakteristiku. Myšlenkou použití nerovnoměrného lopatkování je získání ploché účinnostní charakteristiky. Odstředivé čerpadlo by pak mohlo být používáno na větším rozsahu výkonů při dosažení dostatečně velké účinnosti. Práce je založena na experimentální měření a numerické simulaci nerovnoměrných hydraulických prvků čerpadla. Nerovnoměrné oběžné kolo a rozvaděč byli pro tento výzkum nově navrženy. Pro měření bylo v rámci této práce potřeba navrhnout a sestavit novou měřící trať malých ponorných čerpadel. Měřeny byly různé sestavy čerpadla s kombinacemi běžných návrhů hydraulik na jeden pracovní bod a hydraulik s nerovnoměrnou lopatkovou mříží. Všechna měření byla vyhodnocena a byly získány charakteristiky účinnosti, dopravní výšky a příkonu pro každou měřenou kombinaci. Část sestav měřených experimentálně byla také numericky vypočtena pomocí programu Ansys Fluent. Z numerických výpočtů byla sbírána data potřebná pro vyhodnocení charakteristiky účinnosti a měrné energie pro každou řešenou sestavu. Teoretické úvahy se týkají vlivu nerovnoměrné mříže u rozvaděče a vzniká tak doporučení, jak by bylo možné významně snížit ztráty v kanálech. Bylo také provedeno teoretické odvození způsobu, jak získat plochou charakteristiku účinnosti oběžného kola.
|
host ::
