Basic Model Checking Problems for Stochastic Games
| Autoři | |
|---|---|
| Rok publikování | 2009 |
| Druh | Účelové publikace |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | 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 čítačem. Jsou schopny modelovat například frontu s jedním typem úloh, která může pracovat ve více režimech (quasi-birth-death procesy, QBD). Ústřední výherní podmínka studovaná v této práci je dosažitelnost. Ta je zadána množinou cílových vrcholů a pravděpodobnostním limitem. Jeden z~hráčů se zde snaží maximalizovat pravděpodobnost dosažení cíle, druhý se ji snaží minimalizovat. První hráč vyhraje, má-li strategii, která zajistí pravděpodobnost (ostře či neostře) větší než daný limit, bez ohledu na strategii druhého hráče. Duálně je definovaná výhra druhého hráče. Poznamenejme, že z pohledu logiky nejde o negaci podmínky pro výhru prvního hráče. Algoritmické problémy spojené s dosažitelností, které zde uvažujeme, zahrnují rozhodování vítěze pro daný vrchol hry, počítání reprezentace množiny všech výherních vrcholů daného hráče, popis výherní strategie, a dále zjišťování hodnoty hry v daném vrcholu. Studium problému začínáme na obecné rovině stochastických her na nekonečných grafech s konečným větvením. Představujeme několik zásadních výsledků, včetně (silné) determinovanosti v tom smyslu, že v každém vrcholu vyhrává právě jeden hráč. Věnujeme se i vztahu mezi obecnými a bezpaměťovými deterministickými strategiemi, a existenci optimální strategie. Posléze se zúžíme na případ her generovaných PDA. Uvedeme některé známé výsledky o nerozhodnutelnosti výše zmíněných problémů pro tuto třídu a také rozebereme, jaká omezení této třídy způsobí rozhodnutelnost. Rovněž ukážeme, že regularita množin výherních vrcholů úzce souvisí s rozdílem mezi obecnou a kvalitativní výherní podmínkou. V kvalitativní podmínce může být pravděpodobnostní limit pouze 0 nebo 1, v obecné to může být libovolné racionální číslo. Dále uvádíme rozsáhlou diskuzi výše zmíněných problému spolu s netriviálními řešeními pro třídy BPA her a her nad jednočítačovými automaty. Závěrem se věnujeme Büchiho výherní podmínce. Liší se od dosažitelnosti v~tom, že požaduje nekonečně mnoho návštěv cíle namísto aspoň jedné návštěvy požadované při dosažitelnosti. Uvádíme zde několik základních výsledků pro tuto podmínku v kontextu BPA her. |
| Související projekty: |