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/ |
| Shrnutí: | 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, 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 |
|---|---|
| Popis jednotky: | Vedoucí práce: Ivana Černá |
| Fyzický popis: | x, 164 stran |