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. Online. 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. [citováno 2024-04-24]
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 0302-9743
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
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 30. 4. 2014 04:35.
Anotace
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.
Anotace č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 VaVNá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 VaVNá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ěrNá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 MUNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 24. 4. 2024 06:09