Expected Reachability-Time Games

Warning

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

FOREJT Vojtěch KWIATKOWSKA Marta NORMAN Gethin TRIVEDI Ashutosh

Year of publication 2010
Type Article in Proceedings
Conference Formal Modeling and Analysis of Timed Systems
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-15297-9_11
Field Informatics
Keywords timed automata verification games
Description In an expected reachability-time game (ERTG) two players, Min and Max, move a token along the transitions of a probabilistic timed automaton, so as to minimise and maximise, respectively, the expected time to reach a target. These games are concurrent since at each step of the game both players choose a timed move (a time delay and action under their control), and the transition of the game is determined by the timed move of the player who proposes the shorter delay. A game is turn-based if at any step of the game, all available actions are under the control of precisely one player. We show that while concurrent ERTGs are not always determined, turn-based ERTGs are positionally determined. Using the boundary region graph abstraction, and a generalisation of Asarin and Maler's simple function, we show that the decision problems related to computing the upper/lower values of concurrent ERTGs, and computing the value of turn-based ERTGs are decidable and their complexity is in NEXPTIME intersection co-NEXPTIME.
Related projects:

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