Stochastic Real-Time Games with Qualitative Timed Automata Objectives

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

Basic information

Original name

Stochastic Real-Time Games with Qualitative Timed Automata Objectives

Authors

BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), Jan KRČÁL (203 Czech Republic, belonging to the institution), Jan KŘETÍNSKÝ (203 Czech Republic, belonging to the institution), Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution) and Vojtěch ŘEHÁK (203 Czech Republic, belonging to the institution)

Edition

Berlin Heidelberg New York, CONCUR 2010 - Concurrency Theory, p. 207-221, 15 pp. 2010

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/10:00065879

Organization unit

Faculty of Informatics

ISBN

978-3-642-15374-7

ISSN

DOI

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

UT WoS

000285373500015

Keywords in English

stochastic games; timed automata

Tags

International impact, Reviewed

---

Abstract

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.

In Czech

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.

---

Links

GAP202/10/1469, research and development project	Name: Formální metody pro analýzu a verifikaci komplexních systémů Investor: Czech Science Foundation
GP201/08/P459, research and development project	Name: Nové možnosti automatické verifikace síťových protokolů Investor: Czech Science Foundation, New possibilities in automatic verification of network protocols
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
MUNI/A/0914/2009, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV) Investor: Masaryk University, Category A
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science