D 2007

Stochastic Game Logic

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

Základní údaje

Originální název

Stochastic Game Logic

Název česky

Logika pro náhodnostní hry

Autoři

BAIER, Christel (276 Německo), Tomáš BRÁZDIL (203 Česká republika), Marcus GRÖSSER (276 Německo) a Antonín KUČERA (203 Česká republika, garant)

Vydání

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

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

Organizační jednotka

Fakulta informatiky

ISBN

0-7695-2883-X

UT WoS

000305225400001

Klíčová slova anglicky

stochastic systems; temporal logic; model checking

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 25. 11. 2007 23:27, prof. RNDr. Antonín Kučera, Ph.D.

Anotace

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.

Česky

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.

Návaznosti

MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky