|
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
|
| |
|
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.
|
|
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.
|
|
Extensions to Probabilistic Linear Discriminant Analysis for Speaker Recognition
Plchot, Oldřich ; Fousek, Petr (referee) ; McCree,, Alan (referee) ; Burget, Lukáš (advisor)
Tato práce se zabývá pravděpodobnostními modely pro automatické rozpoznávání řečníka. Podrobně analyzuje zejména pravděpodobnostní lineární diskriminační analýzu (PLDA), která modeluje nízkodimenzionální reprezentace promluv ve formě \acronym{i--vektorů}. Práce navrhuje dvě rozšíření v současnosti požívaného PLDA modelu. Nově navržený PLDA model s plným posteriorním rozložením modeluje neurčitost při generování i--vektorů. Práce také navrhuje nový diskriminativní přístup k trénování systému pro verifikaci řečníka, který je založený na PLDA. Pokud srovnáváme původní PLDA s modelem rozšířeným o modelování neurčitosti i--vektorů, výsledky dosažené s rozšířeným modelem dosahují až 20% relativního zlepšení při testech s krátkými nahrávkami. Pro delší testovací segmenty (více než jedna minuta) je zisk v přesnosti menší, nicméně přesnost nového modelu není nikdy menší než přesnost výchozího systému. Trénovací data jsou ale obvykle dostupná ve formě dostatečně dlouhých segmentů, proto v těchto případech použití nového modelu neposkytuje žádné výhody při trénování. Při trénování může být použit původní PLDA model a jeho rozšířená verze může být využita pro získání skóre v případě, kdy se bude provádět testování na krátkých segmentech řeči. Diskriminativní model je založen na klasifikaci dvojic i--vektorů do dvou tříd představujících oprávněný a neoprávněný soud (target a non-target trial). Funkcionální forma pro získání skóre pro každý pár je odvozena z PLDA a trénování je založeno na logistické regresi, která minimalizuje vzájemnou entropii mezi správným označením všech soudů a pravděpodobnostním označením soudů, které navrhuje systém. Výsledky dosažené s diskriminativně trénovaným klasifikátorem jsou podobné výsledkům generativního PLDA, ale diskriminativní systém prokazuje schopnost produkovat lépe kalibrované skóre. Tato schopnost vede k lepší skutečné přesnosti na neviděné evaluační sadě, což je důležitá vlastnost pro reálné použití.
|
guest ::
