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. In this paper, we establish undecidability for two-clock WTGs making use of non-negative weights, even in a time-bounded setting, closing the last remaining major gap in our algorithmic understanding of WTGs.
翻译:带权定时博弈(WTG)的值问题旨在确定:给定一个具有可达性目标和有理数阈值的双人带权定时博弈,博弈的值是否超过该阈值。大约十年前,该问题已被证明对于使用至少三个时钟的WTG是不可判定的,而对于单时钟WTG则已知是可判定的。本文中,我们证明了即使是在时间有界设定下,使用非负权重的双时钟WTG的值问题也是不可判定的,从而填补了WTG算法理解中最后一个主要空白。