Basic model checking problems for stochastic games

Tato práce se zabývá stochastickými tahovými hrami na nekonečných grafech s lineárními výherními podmínkami. Stochastické hry jsou zásadním modelem pro systémy se třemi režimy chování: s náhodnými změnami stavu, nedeterministickými změnami ovládanými operátorem a nedeterministickými změnami způsoben...

Celý popis

Uloženo v:
Podrobná bibliografie
Hlavní autor: Brožek, Václav (Autor práce)
Další autoři: Kučera, Antonín, 1971- (Vedoucí práce)
Typ dokumentu: VŠ práce nebo rukopis
Jazyk:Angličtina
Vydáno: 2009.
Témata:
Markovovy procesy
stochastické procesy
teorie automatů
Markov Processes
stochastic processes
automata theory
disertace
dissertations
On-line přístup:http://is.muni.cz/th/99081/fi_d/
Obálka
LEADER 05409ctm a22008297a 4500
001 MUB01000604721
003 CZ BrMU
005 20240510112656.0
008 091110s2009 xr ||||| |||||||||||eng d
STA |a POSLANO DO SKCR  |b 2019-04-17 
035 |a (ISMU-VSKP)135423 
040 |a BOD114  |b cze  |d BOD018 
072 7 |a 519.1/.8  |x Kombinatorika. Teorie grafů. Matematická statistika. Operační výzkum. Matematické modelování  |2 Konspekt  |9 13 
080 |a 519.713  |2 MRF 
080 |a (043.3)  |2 MRF 
080 |a 519.217  |2 MRF 
080 |a 519.216  |2 MRF 
100 1 |a Brožek, Václav  |% UČO 99081  |* [absolvent FI MU]  |4 dis 
242 1 0 |a Basic model checking problems for stochastic games.  |y eng 
245 1 0 |a Basic model checking problems for stochastic games  |h [rukopis] /  |c Václav Brožek. 
260 |c 2009. 
300 |a v, 114 s. 
500 |a Vedoucí práce: Antonín Kučera. 
502 |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2009. 
520 2 |a Tato práce se zabývá stochastickými tahovými hrami na nekonečných grafech s lineárními výherními podmínkami. Stochastické hry jsou zásadním modelem pro systémy se třemi režimy chování: s náhodnými změnami stavu, nedeterministickými změnami ovládanými operátorem a nedeterministickými změnami způsobenými prostředím. Nedeterministické chování je modelováno pomocí dvou hráčů. Vynecháním jednoho z hráčů dostaneme z těchto her Markovovy rozhodovací procesy, další zásadní model v teoriích pravděpodobnosti a formální verifikace. Pro vygenerování herního grafu se pro hry studované v této práci používají různé podtřídy zásobníkových automatů (PDA), zejména bezstavové PDA (BPA), jednočítačové automaty a celá třída PDA. Zásobníkové automaty odpovídají systémům s rekurzivně se volajícími procedurami, které mají k dispozici lokální i globální proměnné. BPA pak odpovídají takovým z~těchto systémů, kde se nevyskytují globální proměnné. Jednočítačové automaty jsou konečné automaty s jedním neomezeným č.  |% cze 
520 2 9 |a This thesis concerns stochastic turn based games over infinite graphs with linear objectives. Stochastic games are a fundamental model for systems where three modes of behaviour appear: random changes of the state, nondeterministic changes driven by some controller and nondeterministic changes made by en environment. The nondeterminism is modelled by two players. By eliminating one of the players we get a Markov decision process, another fundamental model in probability theory and formal verification. As a game graph generator for the games studied here various subclasses of pushdown automata (PDA) are considered, in particular the class of stateless PDA (BPA), the class of one-counter automata and the whole class of PDA. Pushdown automata correspond to systems with procedures with recursive calls, which use both global and local variables. BPA, where the number of control states is eliminated to 1 model such systems without global variables. One counter automata are finite automata wi.  |9 eng 
650 0 7 |a Markovovy procesy  |7 ph117828  |2 czenas 
650 0 7 |a stochastické procesy  |7 ph116285  |2 czenas 
650 0 7 |a teorie automatů  |7 ph126547  |2 czenas 
650 0 9 |a Markov Processes  |2 eczenas 
650 0 9 |a stochastic processes  |2 eczenas 
650 0 9 |a automata theory  |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 Kučera, Antonín,  |d 1971-  |7 mub2012683133  |% UČO 2508  |4 ths 
710 2 |a Masarykova univerzita.  |b Fakulta informatiky  |7 kn20010709274  |4 dgg 
856 4 1 |u http://is.muni.cz/th/99081/fi_d/ 
CAT |c 20091110  |l MUB01  |h 2229 
CAT |c 20091203  |l MUB01  |h 0241 
CAT |c 20091203  |l MUB01  |h 1923 
CAT |a KOZOVA  |b 02  |c 20100113  |l MUB01  |h 1452 
CAT |a KOZOVA  |b 02  |c 20100113  |l MUB01  |h 1454 
CAT |c 20100428  |l MUB01  |h 1014 
CAT |a BATCH-UPD  |b 00  |c 20100501  |l MUB01  |h 1224 
CAT |a BATCH-UPD  |b 00  |c 20100929  |l MUB01  |h 0336 
CAT |c 20110627  |l MUB01  |h 1917 
CAT |c 20110627  |l MUB01  |h 2326 
CAT |a POSPEL  |b 02  |c 20120207  |l MUB01  |h 1232 
CAT |a batch  |b 00  |c 20120324  |l MUB01  |h 0132 
CAT |a POSPEL  |b 02  |c 20120417  |l MUB01  |h 0740 
CAT |a POSPEL  |b 02  |c 20120626  |l MUB01  |h 0801 
CAT |a BATCH  |b 00  |c 20130304  |l MUB01  |h 1002 
CAT |a POSPEL  |b 02  |c 20130530  |l MUB01  |h 0738 
CAT |a POSPEL  |b 02  |c 20130605  |l MUB01  |h 0736 
CAT |a POSPEL  |b 02  |c 20130822  |l MUB01  |h 1144 
CAT |c 20150901  |l MUB01  |h 1444 
CAT |c 20150921  |l MUB01  |h 1405 
CAT |a BATCH  |b 00  |c 20151226  |l MUB01  |h 0040 
CAT |a HANAV  |b 02  |c 20180503  |l MUB01  |h 1853 
CAT |a VESELA  |b 02  |c 20190109  |l MUB01  |h 1518 
CAT |c 20190417  |l MUB01  |h 0933 
CAT |c 20210614  |l MUB01  |h 0942 
CAT |c 20210614  |l MUB01  |h 1932 
CAT |a BATCH  |b 00  |c 20210724  |l MUB01  |h 1151 
CAT |a VESELAX  |b 02  |c 20240510  |l MUB01  |h 1125 
CAT |a VESELAX  |b 02  |c 20240510  |l MUB01  |h 1126 
CAT |a VESELAX  |b 02  |c 20240510  |l MUB01  |h 1126 
LOW |a POSLANO DO SKCR  |b 2019-04-17 
994 - 1 |l MUB01  |l MUB01  |m VYSPR  |1 FI  |a Fakulta informatiky  |3 Diz. práce 2009  |5 42005D2578  |8 20100113  |f 72  |f Týdenní  |r 20100113 
AVA |a INF50  |b FI  |d Diz. práce 2009  |e available  |t K dispozici  |f 1  |g 0  |h N  |i 0 

Podobné jednotky