Quantitative Formal Methods for High-level Robot Path Planning
Práce se zaměřuje na vybraná teoretická i aplikovaná témata v oblasti verifikace a syntézy řídících strategií. Prvním přínosem práce je vývoj metod pro kvantitativní ověřování modelů systémů s degradující vlastností, jako například elektronická zařízení s degradujícím elektrickým nábojem nebo sítě,...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
Brno :
Masarykova univerzita, Fakulta informatiky,
2013
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/98614/fi_d/ |
| LEADER | 06411ctm a22010577a 4500 | ||
|---|---|---|---|
| 001 | MUB01000858440 | ||
| 003 | CZ BrMU | ||
| 005 | 20240514102359.0 | ||
| 008 | 130511s2013 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2020-08-05 | ||
| 035 | |a (ISMU-VSKP)167108 | ||
| 040 | |a BOD114 |b cze |d BOD018 | ||
| 072 | 7 | |a 004.9 |x Speciální počítačové metody. Počítačová grafika |2 Konspekt |9 23 | |
| 080 | |a 004 |2 MRF | ||
| 080 | |a 004.94 |2 MRF | ||
| 080 | |a 519.217 |2 MRF | ||
| 100 | 1 | |a Tůmová, Jana |% UČO 98614 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Quantitative Formal Methods for High-level Robot Path Planning |y eng |
| 245 | 1 | 0 | |a Quantitative Formal Methods for High-level Robot Path Planning |h [rukopis] / |c Jana Tůmová |
| 260 | |a Brno : |b Masarykova univerzita, Fakulta informatiky, |c 2013 | ||
| 300 | |a x, 164 stran | ||
| 500 | |a Vedoucí práce: Ivana Černá | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2013 | ||
| 520 | 2 | |a Práce se zaměřuje na vybraná teoretická i aplikovaná témata v oblasti verifikace a syntézy řídících strategií. Prvním přínosem práce je vývoj metod pro kvantitativní ověřování modelů systémů s degradující vlastností, jako například elektronická zařízení s degradujícím elektrickým nábojem nebo sítě, v nichž klesá síla nebo kvalita vysílaného signálu. Pro tyto systémy navrhujeme přechodové systémy s degradací jako modelovací formalismus a lineární temporální logiku s degradačními omezeními jako vhodný specifikační jazyk. Představujeme dva různé přístupy k verifikaci a syntéze řídících strategií. První z nich staví na podobnosti systémů s degradací a časových automatů a jeho výsledkem je verifikační metoda s omezenou, i když libovolnou přesností odpovědi. Druhá navrženou technikou verifikace nabízí plnou přesnost a je založena na principech automatového přístupu k verifikaci. Dále zkoumáme vztah mezi přechodovými systémy s degradací a Markovými rozhodovacími procesy a pro tyto ukazujeme, |% cze | |
| 520 | 2 | 9 | |a This thesis addresses selected theoretical and applied topics in quantitative model checking and control strategy synthesis. First, we develop a theoretical framework for quantitative model checking of systems with degradation, which are systems that naturally incorporate a decaying quality, such as electronic devices with degrading electric charge, broadcasting networks with decreasing power or quality of a transmitted signal. We propose transition systems with degradation as a modeling formalism and linear temporal logic with degradation constraints as a suitable specification language. Two different approaches to model checking and control strategy synthesis are proposed. The first one is a limited, yet arbitrary precision method that exploits a resemblance between the systems with degradation and timed automata. The second one is a full precision method that directly builds on principles of automata-based approach.We also investigate the relationship between systems with degradatio |9 eng |
| 650 | 0 | 7 | |a počítačové modelování |7 ph124513 |2 czenas |
| 650 | 0 | 7 | |a výpočetní technika |7 ph137273 |2 czenas |
| 650 | 0 | 7 | |a Markovovy procesy |7 ph117828 |2 czenas |
| 650 | 0 | 9 | |a computer modelling |2 eczenas |
| 650 | 0 | 9 | |a computer science |2 eczenas |
| 650 | 0 | 9 | |a Markov Processes |2 eczenas |
| 655 | 7 | |a disertace |7 fd132024 |2 czenas | |
| 655 | 9 | |a dissertations |2 eczenas | |
| 658 | |a Informatika (čtyřleté) |b Informatika |c FI D-IN4 IN (IN) |2 CZ-BrMU | ||
| 700 | 1 | |a Černá, Ivana, |d 1963- |7 mub2011658599 |% UČO 1419 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Katedra teorie programování |4 dgg | |
| 856 | 4 | 1 | |u http://is.muni.cz/th/98614/fi_d/ |
| CAT | |c 20130511 |l MUB01 |h 0420 | ||
| CAT | |a HANAV |b 02 |c 20130513 |l MUB01 |h 1149 | ||
| CAT | |a POSPEL |b 02 |c 20130530 |l MUB01 |h 0740 | ||
| CAT | |a POSPEL |b 02 |c 20130821 |l MUB01 |h 1021 | ||
| CAT | |a POSPEL |b 02 |c 20140107 |l MUB01 |h 1224 | ||
| CAT | |a POSPEL |b 02 |c 20140218 |l MUB01 |h 0816 | ||
| CAT | |a POSPEL |b 02 |c 20140311 |l MUB01 |h 0732 | ||
| CAT | |a POSPEL |b 02 |c 20140327 |l MUB01 |h 0750 | ||
| CAT | |a POSPEL |b 02 |c 20140327 |l MUB01 |h 0920 | ||
| CAT | |c 20140911 |l MUB01 |h 1611 | ||
| CAT | |c 20140912 |l MUB01 |h 1105 | ||
| CAT | |c 20150901 |l MUB01 |h 1450 | ||
| CAT | |c 20150921 |l MUB01 |h 1411 | ||
| CAT | |a POSPEL |b 02 |c 20151029 |l MUB01 |h 0733 | ||
| CAT | |a HANAV |b 02 |c 20151102 |l MUB01 |h 1302 | ||
| CAT | |a BATCH |b 00 |c 20151226 |l MUB01 |h 0400 | ||
| CAT | |a POSPEL |b 02 |c 20160914 |l MUB01 |h 1427 | ||
| CAT | |a POSPEL |b 02 |c 20160920 |l MUB01 |h 0817 | ||
| CAT | |a POSPEL |b 02 |c 20160927 |l MUB01 |h 0741 | ||
| CAT | |a POSPEL |b 02 |c 20170228 |l MUB01 |h 1036 | ||
| CAT | |a POSPEL |b 02 |c 20170302 |l MUB01 |h 0827 | ||
| CAT | |a POSPEL |b 02 |c 20180314 |l MUB01 |h 0814 | ||
| CAT | |a POSPEL |b 02 |c 20180503 |l MUB01 |h 0729 | ||
| CAT | |a POSPEL |b 02 |c 20180710 |l MUB01 |h 0635 | ||
| CAT | |a VESELA |b 02 |c 20181210 |l MUB01 |h 0904 | ||
| CAT | |a VESELA |b 02 |c 20181210 |l MUB01 |h 0904 | ||
| CAT | |a VESELA |b 02 |c 20181210 |l MUB01 |h 1054 | ||
| CAT | |a VESELA |b 02 |c 20181210 |l MUB01 |h 1058 | ||
| CAT | |a POSPEL |b 02 |c 20190213 |l MUB01 |h 0800 | ||
| CAT | |a POSPEL |b 02 |c 20190924 |l MUB01 |h 0745 | ||
| CAT | |a POSPEL |b 02 |c 20200510 |l MUB01 |h 2306 | ||
| CAT | |c 20200805 |l MUB01 |h 1110 | ||
| CAT | |a POSPEL |b 02 |c 20201212 |l MUB01 |h 2150 | ||
| CAT | |a POSPEL |b 02 |c 20210122 |l MUB01 |h 0054 | ||
| CAT | |a POSPEL |b 02 |c 20210322 |l MUB01 |h 1142 | ||
| CAT | |a POSPEL |b 02 |c 20210327 |l MUB01 |h 0026 | ||
| CAT | |c 20210614 |l MUB01 |h 1004 | ||
| CAT | |c 20210614 |l MUB01 |h 1952 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1220 | ||
| CAT | |a POSPEL |b 02 |c 20210912 |l MUB01 |h 2336 | ||
| CAT | |a POSPEL |b 02 |c 20211010 |l MUB01 |h 2218 | ||
| CAT | |a HANAV |b 02 |c 20211116 |l MUB01 |h 0031 | ||
| CAT | |a POSPEL |b 02 |c 20220629 |l MUB01 |h 0104 | ||
| CAT | |a POSPEL |b 02 |c 20221019 |l MUB01 |h 2326 | ||
| CAT | |a POSPEL |b 02 |c 20221101 |l MUB01 |h 0840 | ||
| CAT | |a POSPEL |b 02 |c 20230629 |l MUB01 |h 0037 | ||
| CAT | |a POSPEL |b 02 |c 20240405 |l MUB01 |h 2123 | ||
| CAT | |a VESELAX |b 02 |c 20240514 |l MUB01 |h 1022 | ||
| CAT | |a VESELAX |b 02 |c 20240514 |l MUB01 |h 1023 | ||
| CAT | |a VESELAX |b 02 |c 20240514 |l MUB01 |h 1023 | ||
| LOW | |a POSLANO DO SKCR |b 2020-08-05 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |3 Diz. práce 2013 |5 42005D2639 |8 20140312 |f 72 |f Týdenní |r 20140312 |
| AVA | |a INF50 |b FI |d Diz. práce 2013 |e available |t K dispozici |f 1 |g 0 |h N |i 0 | ||