image/svg+xml
Title
Title
Nb
/
Nb
Energy Game
Model a ressource
Mean-payoff Game
Model a reward
Timed games
0
-2
3
x > 3, x := 0
x < 2
x > 3, x := 0
Clocks
Reward
e := e+3
de
dt
= 2 , -1, ....
x := 0
dx
dt
= 1
x < 1 , x>3, ...
Optimal Reachability
Proof: encode c1 by
and c2 by
1
2
1
2
y
x
For Eve:
0
0
-1 , x == 0
0 , x<1
For Adam:
0
0
-1 , x==0
0 , x := 0
constraints,
resets, and
time elapsing
Finite abstraction
compatible with :
+ Preserves sequence of
states
- Information about weights
is lost
1
-2
-2
5
2
-2
1
5
2
-2
-2
0
1
-1
she has one in the energy game
if, and only if,
Eve has a winning strategy in the unraveled game
Quasi paths
Winning Condition of the Unraveled Game:
s0
s1
s2
s1
s0
s1
t
t
x
x
Timed Game
Region Game
Unraveling
Consequence: our algorithm is
complete for Robust Games
Complexity: EXPSPACE / EXPTIME-hard
Refinement of the condition
Eve wins
Eve wins
-2
1
5
2
-2
-2
0
1
-1
0
-2
3
x > 3, x := 0
x < 2
x > 3, x := 0
-1
x <1, x := 0
1, x <1
-1
-1
1, x <1
1
1
-2
5
2
0
-2
3
x > 3, x := 0
x < 2
x > 3, x := 0
Link Mean Payoff Energy in Timed Games
Class of games for which the problems are decidable
Value Iteration works for this class