[FKNT10a]
V. Forejt, M. Kwiatkowska, G. Norman and A. Trivedi.
Expected Reachability-Time Games.
In K. Chatterjee and T. Henzinger (editors), Proeedings of 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), volume 6246 of LNCS, pages 122--136, Springer.
September 2010.
[pdf]
[bib]
|
Notes:
See [FKNT16] for a journal version of the paper, with full proofs and several error fixes. An technical report for this conference paper can be found in [FKNT10b].
The original publication is available at link.springer.com.
|
Abstract.
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 ∩ co-NEXPTIME.
|