|
Partial Report IV / 2016 - Rating of the deformation stress monitoring the state of the rock mass during mining coal seam 30 (634) within the trial operation of mining method corridor - a pillar in OPJ ČSM - NORTH
Waclawik, Petr ; Ptáček, Jiří ; Kukutsch, Radovan ; Kajzar, Vlastimil ; Koníček, Petr ; Souček, Kamil ; Staš, Lubomír
Monitoring of the deformation stress state of the rock mass is a prerequisite for the verification of unapproved new mining methods hall-pillar and its further application in the Czech part of the Upper Silesian coal basin. This mining method is designed on the basis of experiences and practices that are verified in different natural conditions and depths below the surface and is therefore essential for the verification of conditions for the Czech part of the Upper Silesian Basin based on geotechnical monitoring. The present report is prepared on the basis of a contract no. 942/50/10, where the Institute of Geonics, v.v agrees to make periodic evaluation of monitoring data napěťodeformačního state of the rock mass. In accordance with the aforementioned agreement, the message is processed in the six-month period and continues in the interim report III / 2015 (Waclawik et al. 2015) passed buyers in April this year. Interim results of the geotechnical monitoring, such as the experience gained during the first conquest dobývky V show specifics of natural conditions in trial operation unapproved new mining methods hall-pillar.
Fulltext: content.csg -  PDF
Plný tet: UGN_0464907 - PDF
|
|
Optical fiber sensors and optical fiber splicing
Jelínek, Michal ; Mikel, Břetislav
We present development of new methods and techniques of the splicing and shaping optical fibers. We developed new techniques of splicing for standard Single Mode (SM) and Multimode (MM) optical fibers and optical fibers with different diameters. Together with development these techniques we prepared other techniques to splicing hollow core Photonic Crystal Fiber (PCF) and theirs cross splicing methods.Development of these new techniques and methods of the optical fibers splicing are made with respect to using these fibers to another research and development in the field of optical fibers sensors.
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
Subspace Modeling of Prosodic Features for Speaker Verification
Kockmann, Marcel ; Kenny, Patrick (referee) ; Nöth, Elmar (referee) ; Černocký, Jan (advisor)
Předložená disertační práce se zabývá ověřováním mluvčího pomocí prozodických příznaků zahrnujících hodnoty základního tónu, energie a délek řečových úseků. Studovali jsme dvě rozdílné techniky pro parametrizaci: první vede k dobře definované sadě menšího počtu příznaků, druhá k vysoko-dimenzionální sadě heterogenních prozodických příznaků. První část práce se věnuje vývoji příznaků reprezentujících prozodické kontury, zde jsme vyvinuli a ověřili několik modelovacích technik, s důrazem na modelování v reprezentativních podprostorech. Druhá část práce se zaměřuje na nové pod-prostorové modelovací techniky pro heterogenní prozodické parametry s velkou dimenzionalitou. Model je teoreticky odvozen a experimentálně ověřen na oficiálních datech z NIST evaluací ověřování mluvčího (NIST Speaker Recognition Evaluation). Ve srovnání s ostatními současnými prozodickými jsme dosáhli podstatně lepších výsledků. Na konci práce presentujeme také novou techniku pro elegantní kombinaci dvou prozodických systémů. Tato technika může být použita rovněž pro fúzi prozodického systému se standardním přesným cepstrálním systémem, což vede k dalšímu podstatnému zvýšení úspěšnosti verifikace.
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.
|
|
Grammars with Restricted Derivation Trees
Koutný, Jiří ; Janoušek, Jan (referee) ; Vojnar, Tomáš (referee) ; Meduna, Alexandr (advisor)
V této disertační práci jsou studovány teoretické vlastnosti gramatik s omezenými derivačními stromy. Po uvedení současného stavu poznání v této oblasti je výzkum zaměřen na tři základní typy omezení derivačních stromů. Nejprve je představeno zcela nové téma, které je založeno na omezení řezů a je zkoumána vyjadřovací síla takto omezené gramatiky. Poté je zkoumáno několik nových vlastností omezení kladeného na cestu derivačních stromů. Zejména je studován vliv vymazávacích pravidel na vyjadřovací sílu gramatik s omezenou cestou a pro tyto gramatiky jsou zavedeny dvě normální formy. Následně je popsána nová souvislost mezi gramatikami s omezenou cestou a některými pseudouzly. Dále je prezentován protiargument k vyjadřovací síle tohoto modelu, která byla dosud považována za dobře známou vlastnost. Nakonec je zavedeno zobecnění modelu s omezenou cestou na ne jednu, ale několik cest. Tento model je následně studován zejména z hlediska vlastností vkládání, uzávěrových vlastností a vlastností syntaktické analýzy.
|
|
Evolutionary Approach to Synthesis and Optimization of Ordinary and Polymorphic Circuits
Gajda, Zbyšek ; Schmidt, Jan (referee) ; Zelinka,, Ivan (referee) ; Sekanina, Lukáš (advisor)
Tato disertační práce se zabývá evolučním návrhem a optimalizací jak běžných, tak polymorfních digitálních obvodů. V práci jsou uvedena a vyhodnocena nová rozšíření kartézského genetického programování (Cartesian Genetic Programming, CGP), která umožňují zkrácení výpočetního času a získávání kompaktnějších obvodů. Další část práce se zaměřuje na nové metody syntézy polymorfních obvodů. Uvedené metody založené na polymorfních binárních rozhodovacích diagramech a polymorfním multiplexovaní rozšiřují běžné reprezentace digitálních obvodů, a to s ohledem na začlenění polymorfních hradel. Z důvodu snížení počtu hradel v obvodech syntetizovaných uvedenými metodami je provedena evoluční optimalizace založená na CGP. Implementované polymorfní obvody, které jsou optimalizovány s využitím CGP, reprezentují nejlepší známá řešení, jestliže je jako cílové kritérium brán počet hradel obvodu.
|
|
Test Application Methodology Based On the Identification of Testable blocks
Herrman, Tomáš ; Plíva, Zdeněk (referee) ; Racek, Stanislav (referee) ; Kotásek, Zdeněk (advisor)
The PhD thesis deals with the analysis of digital systems described on RT level. The methodology of data paths analysis is decribed, the data path controller analysis is not solved in the thesis. The methodology is built on the concept of Testable Block (TB) which allows to divide digital component to such segments which can be tested through their inputs/outputs, border registers and primary inputs/outputs are used for this purpose. As a result, lower number of registers is needed to be included into scan chain - border registers are the only ones which are scanned. The segmentation allows also to reduce the volume of test vectors, tests are generated for segments, not for the complete component. To identify TBs, two evolutionary algorithms are used, they operate on TB formal model which is also defined in the thesis.
|
|
On-line Data Analysis Based on Visual Codebooks
Beran, Vítězslav ; Honec, Jozef (referee) ; Sojka, Eduard (referee) ; Zemčík, Pavel (advisor)
Práce představuje novou adaptabilní metodu pro on-line vyhledávání videa v reálném čase pomocí vizuálních slovníků. Nová metoda se zaměřuje na nízkou výpočetní náročnost a přesnost vyhledání při on-line použití. Metoda vychází z technik využitých u statických vizuálních slovníků. Tyto běžné techniky jsou upraveny tak, aby byly schopné se adaptovat na proměnlivá data. Postupy, které toto u nové metody řeší, jsou - dynamická inverzní frekvence dokumentů, adaptabilní vizuální slovník a proměnlivý invertovaný index. Navržený postup byl vyhodnocen na úloze vyhledávání videa a prezentované výsledky ukazují, jaké vlastnosti má adaptabilní metoda ve srovnání se statickým přístupem. Nová adaptabilní metoda je založena na konceptu plovoucího okna, který definuje, jakým způsobem se vybírají data pro adaptaci a ke zpracování. Společně s konceptem je definován i matematický aparát, který umožňuje vyhodnotit, jak koncept nejlépe využít pro různé metody zpracování videa. Praktické využití adaptabilní metody je konkrétně u systémů pro zpracování videa, kde se očekává změna v charakteru vizuálních dat nebo tam, kde není předem známo, jakého charakteru vizuální data budou.
|
|
Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (referee) ; Yamamura,, Akihito (referee) ; Meduna, Alexandr (advisor)
Tato disertační práce studuje synchronní formální systémy založené na gramatikách a převodnících a zkoumá jak jejich teoretické vlastnosti, tak i perspektivy praktických aplikací. Práce představuje nové koncepty a definice vycházející ze známých principů řízeného přepisování a synchronizace. Navrhuje alternativní způsob synchronizace bezkontextových gramatik, založený na propojení pravidel. Tento princip rozšiřuje také na řízené gramatiky, konkrétně gramatiky s rozptýleným kontextem a maticové gramatiky. Dále je představen na podobném principu založený nový druh převodníku, tzv. pravidlově omezený převodník. Jedná se o systém složený z konečného automatu a bezkontextové gramatiky. Práce prezentuje nové teoretické výsledky ohledně generativní a přijímajicí síly. Poslední část práce zkoumá možnosti lingvisticky orientovaných aplikací se zameřením na překlad přirozeného jazyka. Diskutuje a srovnává hlavní výhody nových modelů s využitím vybraných případových studií z českého, anglického a japonského jazyka pro ilustraci.
|
guest ::
