14:00
15:00

[M2F] Julie Parreaux (U. Warsaw) - Weighted Timed Games: Decidability, Randomness and Robustness

Weighted timed games are two-player zero-sum games played in a timed automaton
equipped with integer weights. We consider optimal reachability objectives, in
which one of the players, whom we call Min, wants to reach a target location
while minimising the cumulated weight. While knowing if Min has a
(deterministic) strategy to guarantee a value lower than a given threshold is
known to be undecidable (with two or more clocks), several conditions, one of
them being the divergence or one-clock WTGs with only non-negative weights,
have been given to recover decidability. We, first, extend this list by
considering arbitrary weights by showing that the value function can be
computed in exponential time (if weights are encoded in unary).

Next, in such weighted timed games (like in untimed weighted games in the
presence of negative weights), Min may need finite memory to play (close to)
optimally. This is thus tempting to try to emulate this finite memory with
other strategic capabilities. In particular, we allow the players to use
stochastic decisions, both in the choice of transitions and timing delays. We
give, for the first time, a definition of the expected value in weighted timed
games, overcoming several theoretical challenges. We then show that, in
divergent weighted timed games, the stochastic value is indeed equal to the
classical (deterministic) value, thus proving that Min can guarantee the same
value while only using stochastic choices and no memory.

Finally, even stochastic strategies, almost optimal strategies are not
implementable since they use infinite precision of clocks in the choice of the
delay or in the knowledge about the configurations. Robustness is a known
process to encode the imprecision of delays in strategies: robustness allows to
Max player (the opponent of Min) to lightly modify the delay chosen by Min. In
the literature, two robust semantics exist: conservative semantic checks a
guard after the perturbation, and excessive semantic checks a guard before.
As for deterministic strategies, it was known that if Min has a (robust)
strategy to guarantee a value lower than a given threshold is known to be
undecidable. By adapting the process of value iteration introduced by Alur, we
compute the (robust) value in acyclic WTG under conservative and excessive
semantics.

Amphitheatre du LaBRI