D 2007

Stochastic Game Logic

BAIER, Christel, Tomáš BRÁZDIL, Marcus GRÖSSER and Antonín KUČERA

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
Změněno: 25/11/2007 23:27, prof. RNDr. Antonín Kučera, Ph.D.

Abstract

ORIG CZ

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
Displayed: 4/11/2024 16:09