Stochastic Real-Time Games with Qualitative Timed Automata Objectives

BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ, Antonín KUČERA a Vojtěch ŘEHÁK. Stochastic Real-Time Games with Qualitative Timed Automata Objectives. In CONCUR 2010 - Concurrency Theory. Berlin Heidelberg New York: Springer, 2010, s. 207-221. ISBN 978-3-642-15374-7. Dostupné z: https://dx.doi.org/10.1007/978-3-642-15375-4_15.

Základní údaje

Originální název

Stochastic Real-Time Games with Qualitative Timed Automata Objectives

Autoři

BRÁZDIL, Tomáš (203 Česká republika, domácí), Jan KRČÁL (203 Česká republika, domácí), Jan KŘETÍNSKÝ (203 Česká republika, domácí), Antonín KUČERA (203 Česká republika, garant, domácí) a Vojtěch ŘEHÁK (203 Česká republika, domácí)

Vydání

Berlin Heidelberg New York, CONCUR 2010 - Concurrency Theory, od s. 207-221, 15 s. 2010

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/10:00065879

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-15374-7

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-15375-4_15

UT WoS

000285373500015

Klíčová slova anglicky

stochastic games; timed automata

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We consider two-player stochastic games over real-time probabilistic processes where the winning objective is specified by a timed automaton. The goal of player Box is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player Diamond aims at the opposite. We prove that whenever player Box has a winning strategy, then she also has a strategy that can be specified by a timed automaton. The strategy automaton reads the history of a play, and the decisions taken by the strategy depend only on the region of the resulting configuration. We also give an exponential-time algorithm which computes a winning timed automaton strategy if it exists.

Česky

V článku se zkoumají hry nad stochastickými procesy s reálným časem, kde výherní kritérium je určeno časovým automatem. Je dokázáno, že pokud hráč Box má (nějakou) strategii, pomocí které dokáže zajistit svou výhru s pravděpodobností jedna proti libovolné strategii protihráče, pak má také výherní strategii, kterou lze konečně reprezentovat časovým automatem. Tento automat lze navíc algoritmicky sestrojit.

---

Návaznosti

GAP202/10/1469, projekt VaV	Název: Formální metody pro analýzu a verifikaci komplexních systémů Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů
GP201/08/P459, projekt VaV	Název: Nové možnosti automatické verifikace síťových protokolů Investor: Grantová agentura ČR, Nové možnosti automatické verifikace síťových protokolů
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
MUNI/A/0914/2009, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky