Stochastic Real-Time Games with Qualitative Timed Automata Objectives

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRÁZDIL Tomáš KRČÁL Jan KŘETÍNSKÝ Jan KUČERA Antonín ŘEHÁK Vojtěch

Year of publication 2010
Type Article in Proceedings
Conference CONCUR 2010 - Concurrency Theory
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-15375-4_15
Field Informatics
Keywords stochastic games; timed automata
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.