We prove that the Value Problem for weighted timed games (WTGs) with two clocks and non-negative integer weights is undecidable – even under a time bound. The Value Problem for weighted timed games (WTGs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. This problem was shown to be undecidable some ten years ago for WTGs making use of at least three clocks, and is known to be decidable for single-clock WTGs. Our reduction encodes a deterministic two-counter machine using two clocks and uses “punishment” gadgets that let the opponent detect and penalize any incorrect simulation. This closes one of the last remaining major gaps in our algorithmic understanding of WTGs.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The Value Problem for Weighted Timed Games with Two Clocks is Undecidable

  • Quentin Guilmant,
  • Joël Ouaknine,
  • Isa Vialard

摘要

We prove that the Value Problem for weighted timed games (WTGs) with two clocks and non-negative integer weights is undecidable – even under a time bound. The Value Problem for weighted timed games (WTGs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. This problem was shown to be undecidable some ten years ago for WTGs making use of at least three clocks, and is known to be decidable for single-clock WTGs. Our reduction encodes a deterministic two-counter machine using two clocks and uses “punishment” gadgets that let the opponent detect and penalize any incorrect simulation. This closes one of the last remaining major gaps in our algorithmic understanding of WTGs.