Stochastic real-time games with qualitative timed automata objectives

Tomáš Brázdil; Jan Krčál; Jan Křetínský; Antonín Kučera; Vojtěch Řehák

doi:10.1007/978-3-642-15375-4_15

Stochastic real-time games with qualitative timed automata objectives

Tomáš Brázdil, Jan Krčál, Jan Křetínský, Antonín Kučera, Vojtěch Řehák

Informatics 7 - Associate Professorship of Formal Methods for Software Reliability

Masaryk University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

14 Scopus citations

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 □ is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player ◇ aims at the opposite. We prove that whenever player □ 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.

Original language	English
Title of host publication	CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings
Pages	207-221
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-15375-4_15
State	Published - 2010
Event	21st Conference on Concurrency Theory, CONCUR 2010 - Paris, France Duration: 31 Aug 2010 → 3 Sep 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6269 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st Conference on Concurrency Theory, CONCUR 2010
Country/Territory	France
City	Paris
Period	31/08/10 → 3/09/10

Access to Document

10.1007/978-3-642-15375-4_15

Cite this

Brázdil, T., Krčál, J., Křetínský, J., Kučera, A., & Řehák, V. (2010). Stochastic real-time games with qualitative timed automata objectives. In CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings (pp. 207-221). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6269 LNCS). https://doi.org/10.1007/978-3-642-15375-4_15

Brázdil, Tomáš ; Krčál, Jan ; Křetínský, Jan et al. / Stochastic real-time games with qualitative timed automata objectives. CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings. 2010. pp. 207-221 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{908734bb02534efdacc6954061de6737,

title = "Stochastic real-time games with qualitative timed automata objectives",

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 □ is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player ◇ aims at the opposite. We prove that whenever player □ 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.",

author = "Tom{\'a}{\v s} Br{\'a}zdil and Jan Kr{\v c}{\'a}l and Jan K{\v r}et{\'i}nsk{\'y} and Anton{\'i}n Ku{\v c}era and Vojt{\v e}ch {\v R}eh{\'a}k",

year = "2010",

doi = "10.1007/978-3-642-15375-4_15",

language = "English",

isbn = "3642153747",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "207--221",

booktitle = "CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings",

note = "21st Conference on Concurrency Theory, CONCUR 2010 ; Conference date: 31-08-2010 Through 03-09-2010",

}

Brázdil, T, Krčál, J, Křetínský, J, Kučera, A & Řehák, V 2010, Stochastic real-time games with qualitative timed automata objectives. in CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6269 LNCS, pp. 207-221, 21st Conference on Concurrency Theory, CONCUR 2010, Paris, France, 31/08/10. https://doi.org/10.1007/978-3-642-15375-4_15

Stochastic real-time games with qualitative timed automata objectives. / Brázdil, Tomáš; Krčál, Jan; Křetínský, Jan et al.
CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings. 2010. p. 207-221 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6269 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Stochastic real-time games with qualitative timed automata objectives

AU - Brázdil, Tomáš

AU - Krčál, Jan

AU - Křetínský, Jan

AU - Kučera, Antonín

AU - Řehák, Vojtěch

PY - 2010

Y1 - 2010

N2 - 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 □ is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player ◇ aims at the opposite. We prove that whenever player □ 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.

AB - 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 □ is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player ◇ aims at the opposite. We prove that whenever player □ 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.

UR - http://www.scopus.com/inward/record.url?scp=78249287523&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-15375-4_15

DO - 10.1007/978-3-642-15375-4_15

M3 - Conference contribution

AN - SCOPUS:78249287523

SN - 3642153747

SN - 9783642153747

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 207

EP - 221

BT - CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings

T2 - 21st Conference on Concurrency Theory, CONCUR 2010

Y2 - 31 August 2010 through 3 September 2010

ER -

Brázdil T, Krčál J, Křetínský J, Kučera A, Řehák V. Stochastic real-time games with qualitative timed automata objectives. In CONCUR 2010 - Concurrency Theory - 21st International Conference, CONCUR 2010, Proceedings. 2010. p. 207-221. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-15375-4_15

Stochastic real-time games with qualitative timed automata objectives

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this