Name
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-642-15297-9_11 | FORMATS'10 Proceedings of the 8th international conference on Formal modeling and analysis of timed systems |
Keywords | Field | DocType |
shorter delay,lower value,decision problem,expected reachability-time game,expected time,turn-based ertgs,available action,time delay,concurrent ertgs,boundary region graph abstraction,timed automaton | NEXPTIME,Complexity class,Decision problem,Nondeterministic algorithm,Computer science,Theoretical computer science,Reachability,Timed automaton,Probabilistic logic,Stochastic game | Journal |
Volume | Issue | ISSN |
abs/1604.04435 | C | 0302-9743 |
ISBN | Citations | PageRank |
3-642-15296-1 | 4 | 0.42 |
References | Authors | |
28 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vojtech Forejt | 1 | 302 | 14.69 |
| Marta Z. Kwiatkowska | 2 | 6118 | 322.21 |
| Gethin Norman | 3 | 4163 | 193.68 |
| Ashutosh Trivedi | 4 | 149 | 28.08 |