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...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2009.
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/99081/fi_d/ |
| Shrnutí: | 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 č. 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. |
|---|---|
| Popis jednotky: | Vedoucí práce: Antonín Kučera. |
| Fyzický popis: | v, 114 s. |