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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
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 0302-9743
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
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 30/4/2014 04:35.
Abstract
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.
Abstract (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 projectName: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Czech Science Foundation
GP201/08/P459, research and development projectName: 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 MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)
Investor: Masaryk University, Category A
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science
PrintDisplayed: 25/4/2024 15:43