Stochastic Game Logic

BAIER, Christel, Tomáš BRÁZDIL, Marcus GRÖSSER and Antonín KUČERA. Stochastic Game Logic. In Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007). Los Alamitos, Washington, Tokyo: IEEE Computer Society, 2007, p. 227-236. ISBN 0-7695-2883-X.

Basic information

Original name

Stochastic Game Logic

Name in Czech

Logika pro náhodnostní hry

Authors

BAIER, Christel (276 Germany), Tomáš BRÁZDIL (203 Czech Republic), Marcus GRÖSSER (276 Germany) and Antonín KUČERA (203 Czech Republic, guarantor)

Edition

Los Alamitos, Washington, Tokyo, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), p. 227-236, 10 pp. 2007

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/07:00022945

Organization unit

Faculty of Informatics

ISBN

0-7695-2883-X

UT WoS

000305225400001

Keywords in English

stochastic systems; temporal logic; model checking

Tags

Model checking, stochastic systems, temporal logic

Tags

International impact, Reviewed

---

Abstract

V originále

Stochastic game logic (SGL) is a new temporal logic that combines features of alternating temporal logic (to formalize the individual views and cooperation and reaction facilities of agents in a multiplayer game), probabilistic computation tree logic and extended temporal logic (to reason about qualitative and quantitative, linear or branching time winning objectives). The paper presents the syntax and semantics of SGL and discusses its model checking problem. The model checking problem of SGL turns out to be undecidable when the strategies are history-dependent. We show PSPACE completeness for memoryless deterministic strategies and the EXPSPACE upper bound for memoryless randomized strategies. For the qualitative fragment of SGL we show PSPACE completeness for memoryless strategies.

In Czech

Logika pro stochastické hry (SGL) je nová temporální logika, která kombinuje vlastnosti laternující temporální logiky, logiky PCTL, a rozšířené temporální logiky. V článku je zavedena syntaxe a sémantika SGL a rozebrána výpočetní složitost problému ověření platnosti SGL formule v konkrétní struktuře.

---

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