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. |
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 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 |
PrintDisplayed: 26/8/2024 07:11