2006
Stochastic Games with Branching-Time Winning Objectives
BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT a Antonín KUČERAZákladní údaje
Originální název
Stochastic Games with Branching-Time Winning Objectives
Název česky
Stochastické hry s výherním kritériem určeným formulí větvícího se času
Autoři
BRÁZDIL, Tomáš (203 Česká republika), Václav BROŽEK (203 Česká republika), Vojtěch FOREJT (203 Česká republika) a Antonín KUČERA (203 Česká republika, garant)
Vydání
Los Alamitos, California, 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, Washington, USA, Proceedings, od s. 349-358, 10 s. 2006
Nakladatel
IEEE Computer Society
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Spojené státy
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/06:00017108
Organizační jednotka
Fakulta informatiky
ISBN
0-7695-2631-4
UT WoS
000240899100036
Klíčová slova anglicky
Stochastic games; branching-time temporal logics
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 17:28, prof. RNDr. Antonín Kučera, Ph.D.
V originále
We consider stochastic turn-based games where the winning objectives are given by formulae of the branching-time logic PCTL. These games are generally not determined and winning strategies may require memory and/or randomization. Our main results concern history-dependent strategies. In particular, we show that the problem whether there exists a history-dependent winning strategy in 1.5-player games is highly undecidable, even for objectives formulated in the L(F^{=5/8},F^{=1},F^{>0},G^{=1}) fragment of PCTL. On the other hand, we show that the problem becomes decidable (and in fact EXPTIME-complete) for the L(F{=1},F^{>0},G^{=1}) fragment of PCTL, where winning strategies require only finite memory. This result is tight in the sense that winning strategies for L(F^{=1},F^{>0},G^{=1},G^{>0}) objectives may already require infinite memory.
Česky
V článku se zkoumají vlastnosti třídy stochastických her, kde je výherní kritérium určeno danou formulí temporální logiky PCTL. Tyto hry obecně nejsou determinované a výherní strategie mohou vyžadovat paměť a/nebo náhodnostní tahy. Hlavní prezentované výsledky se týkají strategií závisejících na historii hry. Zejména je dokázáno, že problém existence výherní strategie závislé na historii je vysoce nerozhodnutelný pro hry s 1.5 hráči, kde výherním kritériem je formule fragmentu L(F^{=5/8},F^{=1},F^{>0},G^{=1}) logiky PCTL. Rovněž je dokázáno, že tento problém je rozhodnutelný (a EXPTIME-úplný) pro fragment L(F{=1},F^{>0},G^{=1}), kde výherní strategie vyžadují pouze konečnou paměť.
Návaznosti
| MSM0021622419, záměr |
| ||
| 1M0545, projekt VaV |
|