D 2006

Stochastic Games with Branching-Time Winning Objectives

BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT and Antonín KUČERA

Basic information

Original name

Stochastic Games with Branching-Time Winning Objectives

Name in Czech

Stochastické hry s výherním kritériem určeným formulí větvícího se času

Authors

BRÁZDIL, Tomáš (203 Czech Republic), Václav BROŽEK (203 Czech Republic), Vojtěch FOREJT (203 Czech Republic) and Antonín KUČERA (203 Czech Republic, guarantor)

Edition

Los Alamitos, California, 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, Washington, USA, Proceedings, p. 349-358, 10 pp. 2006

Publisher

IEEE Computer Society

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/06:00017108

Organization unit

Faculty of Informatics

ISBN

0-7695-2631-4

UT WoS

000240899100036

Keywords in English

Stochastic games; branching-time temporal logics

Tags

International impact, Reviewed
Změněno: 22/11/2006 17:28, prof. RNDr. Antonín Kučera, Ph.D.

Abstract

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.

In Czech

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ěť.

Links

MSM0021622419, plan (intention)
Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1M0545, research and development project
Name: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science