Publication details

Expected Reachability-Time Games



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

Faculty of Informatics

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.

More info