Basic Model Checking Problems for Stochastic Games
Václav Brožek · 2009
Tato prace se zabýva stochastickými tahovými hrami na nekonecných grafech s linearnimi výhernimi podminkami. Stochasticke hry jsou zasadnim modelem pro systemy se třemi režimy chovani: s nahodnými změnami stavu, nedeterministickými změnami ovladanými operatorem a nedeterministickými změnami způsobenými prostředim. Nedeterministicke chovani je modelovano pomoci dvou hraců. Vynechanim jednoho z hraců dostaneme z těchto her Markovovy rozhodovaci procesy, dalsi zasadni model v teoriich pravděpodobnosti a formalni verifikace. Pro vygenerovani herniho grafu se pro hry studovane v teto praci použivaji různe podtřidy zasobnikových automatů (PDA), zejmena bezstavove PDA (BPA), jednocitacove automaty a cela třida PDA. Zasobnikove automaty odpovidaji systemům s rekurzivně se volajicimi procedurami, ktere maji k dispozici lokalni i globalni proměnne. BPA pak odpovidaji takovým z~těchto systemů, kde se nevyskytuji globalni proměnne. Jednocitacove automaty jsou konecne automaty s jednim neomezeným citacem. Jsou schopny modelovat napřiklad frontu s jednim typem uloh, ktera může pracovat ve vice režimech (quasi-birth-death procesy, QBD). Ustředni výherni podminka studovana v teto praci je dosažitelnost. Ta je zadana množinou cilových vrcholů a pravděpodobnostnim limitem. Jeden z~hraců se zde snaži maximalizovat pravděpodobnost dosaženi cile, druhý se ji snaži minimalizovat. Prvni hrac vyhraje, ma-li strategii, ktera zajisti pravděpodobnost (ostře ci neostře) větsi než daný limit, bez ohledu na strategii druheho hrace. Dualně je definovana výhra druheho hrace. Poznamenejme, že z pohledu logiky nejde o negaci podminky pro výhru prvniho hrace. Algoritmicke problemy spojene s dosažitelnosti, ktere zde uvažujeme, zahrnuji rozhodovani vitěze pro daný vrchol hry, pocitani reprezentace množiny vsech výhernich vrcholů daneho hrace, popis výherni strategie, a dale zjisťovani hodnoty hry v danem vrcholu. Studium problemu zaciname na obecne rovině stochastických her na nekonecných grafech s konecným větvenim. Představujeme několik zasadnich výsledků, vcetně (silne) determinovanosti v tom smyslu, že v každem vrcholu vyhrava pravě jeden hrac. Věnujeme se i vztahu mezi obecnými a bezpaměťovými deterministickými strategiemi, a existenci optimalni strategie. Posleze se zužime na připad her generovaných PDA. Uvedeme některe zname výsledky o nerozhodnutelnosti výse zminěných problemů pro tuto třidu a take rozebereme, jaka omezeni teto třidy způsobi rozhodnutelnost. Rovněž ukažeme, že regularita množin výhernich vrcholů uzce souvisi s rozdilem mezi obecnou a kvalitativni výherni podminkou. V kvalitativni podmince může být pravděpodobnostni limit pouze 0 nebo 1, v obecne to může být libovolne racionalni cislo. Dale uvadime rozsahlou diskuzi výse zminěných problemu spolu s netrivialnimi řesenimi pro třidy BPA her a her nad jednocitacovými automaty. Zavěrem se věnujeme Buchiho výherni podmince. Lisi se od dosažitelnosti v~tom, že požaduje nekonecně mnoho navstěv cile namisto aspoň jedne navstěvy požadovane při dosažitelnosti. Uvadime zde několik zakladnich výsledků pro tuto podminku v kontextu BPA her.