Decidability of One-Clock Weighted Timed Games with Arbitrary Weights

TL;DR

This paper proves that one-clock Weighted Timed Games with arbitrary weights are decidable and provides an exponential time algorithm for computing their value function when weights are unary encoded.

Contribution

It establishes the decidability of one-clock WTGs with arbitrary weights, a problem previously unresolved, and offers an exponential time computation method.

Findings

Decidability of one-clock WTGs with arbitrary weights is proven.

Value function can be computed in exponential time with unary weights.

Addresses open problem in weighted timed game theory.

Abstract

Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. Unfortunately, they are notoriously difficult, and undecidable in general. As a consequence, one-clock WTGs have attracted a lot of attention, especially because they are known to be decidable when only non-negative weights are allowed. However, when arbitrary weights are considered, despite several recent works, their decidability status was still unknown. In this paper, we solve this problem positively and show that the value function can be computed in exponential time (if weights are encoded in unary).