Source-linked AI summary
Approximating the Value of Time-Bounded Weighted Timed Games
Isa Vialard, Joël Ouaknine
TL;DR
The Value problem and the Approximation problem for weighted timed games face undecidability, motivating the search for a tractable setting. The paper uses value iteration in the time-bounded setting and proves that arbitrarily precise approximation is decidable in 4-ExpTime.
Problem
The Value problem asks whether a weighted timed game's value is at most a threshold, while Approximation is undecidable for weighted timed games in general.
Source: §1 · p. 1Method
The paper proves that the value function is Lipschitz-continuous for time-bounded games, implying convergence of classical value iteration.
Source: §1 · p. 2Results
4-ExpTime decidability is established for computing arbitrarily precise approximations of the value in time-bounded weighted timed games.
Source: §1 · p. 2, Conclusion · p. 12Takeaways & Limitations
Time-boundedness is a practically motivated setting for real-time systems, whose executions are limited to finite observation windows.
Source: §1 · p. 2Decidability of Approximation for weighted timed games with non-negative weights only remains an open problem.
Source: Conclusion · p. 12
Abstract
from arXiv · showhide
The Value Problem for weighted timed games, an extension of timed automata with weights and adversity, consists in determining, given a weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. This problem is known to be undecidable for weighted timed games, i.e., there is no algorithm that can compute the value exactly. A natural alternative is to approximate the value; however, the Approximation problem is also undecidable in general. In this paper, we prove that the Approximation problem is decidable in 4-ExpTime for weighted timed games whose executions are time-bounded.
1 Introduction
Weighted timed games combine timed automata with weights and opposing players, but both deciding their value and approximating it face undecidability results. This paper proves that approximation is decidable under time-boundedness, a setting motivated by real-time systems.
1 Introduction
- Weighted timed games extend timed automata with integer weights and a game structure in which Min minimizes the cost of reaching a target against Max.Location weights are rates applied to time delays, while transition weights are instantaneous.Source: §1 · p. 1
- The Value problem asks whether Min can guarantee a cost at most a threshold; it is undecidable for two-clock games even with time-boundedness.The supplied passage also reports undecidability for games with three or more clocks, even under almost-divergence and nonnegative weights.Source: §1 · p. 1
- Approximation asks whether the game's value can be computed within a given error; it is undecidable for weighted timed games in general.Prior approximation algorithms cited in the introduction address almost-divergent games, first with nonnegative weights and later with arbitrary weights.Source: §1 · pp. 1–2
- The Approximation problem is decidable for weighted timed games under a time-boundedness constraint, a setting motivated by finite observation windows in real-time systems.The chosen time bound is typically of the same order of magnitude as the model's timing constraints.Source: §1 · p. 2
- Lipschitz continuity of the value function in the time-bounded setting implies that value iteration converges, yielding a 4-ExpTime algorithm for arbitrarily precise approximations.The paper also gives an explicit upper bound on the convergence rate.Source: §1 · p. 2
- Time-boundedness is orthogonal to almost-divergence and is naturally satisfied in real-time systems, unlike the more constraining almost-divergence condition.The paper identifies the earlier decidability result for Approximation as concerning almost-divergent games [6].Source: §1 · p. 2
2 Definitions
Weighted timed games combine clocks, discrete transitions, weights, and opposing players in a reachability game; the section defines their value and approximation problems and introduces region-based value iteration.
2.1 Weighted timed games
- A weighted timed game adds integer location and transition weights to clock-constrained timed automata, with Min seeking a low-cost goal-reaching play against Max.A play’s cumulative weight includes elapsed-time costs in locations and discrete-transition weights; time-boundedness means every play from a zero-clock configuration lasts at most some integer T.Source: §2.1 · pp. 2–3
2.2 Min-cost reachability games
- Min-cost reachability games remove clocks, clock constraints, and location weights from weighted timed games, yielding a subclass whose Value problem is decidable [5].Source: §2.2 · p. 4
2.3 Region construction and [0, 1)-wtgs
- Bounded-clock weighted timed games can be transformed into equivalent [0, 1)-games and region games, with the same location complexity as the classical region construction.Trimming removes inaccessible transitions and unnecessary guards without changing value, allowing analysis on trimmed region games.Source: §2.3 · pp. 5–6
2.4 Value iteration algorithm
- Value iteration computes the game value under a restriction that Min reach a goal within k transitions, but it need not terminate or even converge in general.For the illustrated game, the value is −1 although opt_k(0, 0) remains 0 for every k; when iteration stabilizes at the value function, plays of bounded length suffice.Source: §2.4 · pp. 6–7, Figure 1 · p. 7
3 Continuity and slope of the Value function in bounded time
For time-bounded region weighted timed games, the Value function is Lipschitz-continuous, with a slope bound determined by the time bound, weights, and number of clocks. This yields convergence of value iteration and permits strict guards to be relaxed without changing value.
3 Continuity and slope of the Value function in bounded time
- The Value function is Lipschitz-continuous with slope at most 2T wmax d for a time-bounded region [0, 1)-game.Here T is the time bound, wmax the maximal difference between 0 and a location weight, and d the number of clocks.Source: §3 · p. 7
- Lipschitz continuity implies that value iteration converges toward the Value function.The paper notes that its explicit convergence-rate bound also implies convergence.Source: §3 · p. 8
- For a trimmed region game with a time bound, replacing strict guards by strict-or-equal guards does not change the value.The result extends the Value function continuously to the closure of regions.Source: §3 · p. 8
4 Convergence speed of value iteration
The paper bounds how many value-iteration steps suffice for an ε-approximation, first within a strongly connected component and then across the graph. These bounds yield a 4-ExpTime approximation algorithm for time-bounded weighted timed games.
4 Convergence speed of value iteration
- The convergence analysis applies after transforming the game and eliminating non-goal transition weights, using at most m′·(4(m′W + wmax T) + 1) locations.The transformation preserves time-boundedness; accumulated transition weight is stored in locations and paid on reaching a goal.Source: §4 · pp. 8–9
4.1 Zooming in on a strongly connected component
- opt_Nε is an ε-approximation in an SCC, with Nε defined by the inductive convergence bound.For the transformed game, the corresponding global bound gives opt_N′ε as an ε-approximation of its value.Source: §4 · p. 9, §4.1 · p. 10
- The SCC bound unfolds the game around repeated events, limiting how often a player spends positive time in a minimum-weight location.An error budget controls the modified strategy; in an up-driven [0,1)-wtg, at most one time unit can be spent, bounding occurrences of that event.Source: §4.1 · p. 10
4.2 Zooming out
- For the SCC graph, convergence is bounded by N(ε_n, n, n), applied from sink components; each path has length at most n.The components are handled from sinks toward the rest of the graph.Source: §4.2 · p. 10
4.3 Complexity
- Time-boundedness can be decided in exponential time by transforming to a trimmed region [0,1)-wtg and checking whether every SCC is up-driven.The transformation and SCC check are polynomial in input size for unary guards, hence exponential for binary guards.Source: §4.3 · p. 11
Approximation Algorithm
- The algorithm transforms the game, checks time-boundedness, and then uses value iteration to compute the requested approximation or return the exact value when applicable.The longest path in the transformed graph provides an upper bound on the time bound.Source: Approximation Algorithm · p. 11
- 4-ExpTime suffices for the approximation problem: Steps 1–3 are exponential, while Step 4 is quadruple-exponential.Step 4 uses a triple-exponential convergence horizon, with each value-iteration step exponential in the relevant parameters.Source: Approximation Algorithm · pp. 11–12
4.3 Complexity
- The convergence-rate bound is not tight: accounting for time-sharing still gives a triple-exponential convergence rate.The stated bound assumes one time unit in each unfolded copy, although the time bound actually concerns the set of copies.Source: Approximation Algorithm · p. 12
Conclusion
For time-bounded weighted timed games, value iteration converges and its convergence rate is bounded, yielding a 4-ExpTime decision procedure for approximation. Decidability of approximation for games with non-negative weights remains open.
Conclusion
- The value-iteration algorithm converges for time-bounded weighted timed games, with a 3ExpTime-bounded convergence speed and a 4-ExpTime approximation procedure.The paper’s result concerns turn-based time-bounded weighted timed games.Source: Conclusion · p. 12
- Decidability of Approximation for weighted timed games with non-negative weights remains open.The authors note that their techniques may provide insights; with non-negative weights, time in positive-weight locations is bounded by a greedy upper bound on the value.Source: Conclusion · p. 12
A Proofs of Section 3
The appendix proves that the value function is Lipschitz-continuous in time-bounded region games and that relaxing strict guards preserves value. The proofs use bisimulation relations that control how matching plays differ.
A Proofs of Section 3
- The proof compares ε-neighbouring valuations using a bisimulation that keeps matching transition times equal and brings upper-clock values closer.The resulting bound on play-weight differences yields the Lipschitz bound on the value function.Source: A Proofs of Section 3 · pp. 15–16
- For a time-bounded region [0,1)-wtg, the value function is Lipschitz-continuous with slope at most 2T wmax d.Here T is the time bound, wmax the maximal difference between location weights and zero, and d the number of clocks.Source: A Proofs of Section 3 · p. 16
- Relaxing strict guards in a trimmed, time-bounded region game does not change its value.The relaxed game’s value corresponds to the original value function extended continuously to the closure of regions.Source: A Proofs of Section 3 · p. 17
- The guard-relaxation proof bounds play-weight differences by ε·T wmax d + 2εwmax, including a convergent contribution from singleton-region delays.The first term reflects delays that bring clocks together; the second reflects the sum of delay differences at singleton-region locations.Source: A Proofs of Section 3 · p. 17
B.1 Proof of Lemma 19
The proof of Lemma 19 bounds accumulated transition weights along relevant plays, then incorporates those costs into an equivalent game’s locations. The construction preserves the value function at corresponding locations.
B.1 Proof of Lemma 19
- For relevant runs, the accumulated cost is bounded, so it can be stored inside locations; therefore, an equivalent weighted timed game G′ can be constructed.Source: §B.1 · p. 18
- For every location ℓ, the original value function equals the transformed game’s value function at (ℓ, 0).The construction adds a bounded accumulated-cost component to locations and assigns value ±∞ to designated locations.Source: §B.1 · p. 18
B.2 Proof of Theorem 23
The proof unfolds a game around a minimum-weight non-urgent location into copies, reducing the number of non-urgent locations while controlling the value difference. Induction yields an acyclic game that approximates the original and a bounded-length near-optimal strategy.
B.2 Proof of Theorem 23
- Unfolding a minimum-weight non-urgent location into Kη + 1 copies reduces the non-urgent-location count by one and changes the value by at most η.The copies count and bound Min’s positive-delay visits at that location.Source: §B.2 · pp. 18, 23
- The construction limits Max’s delays in ℓ to either 0 or at least η/(2smax); the additional limitation in G′′′ versus G′ comes from non-integer guards between copies, not their number.Source: §B.2 · p. 21
- For any η > 0, an acyclic WTG G′′ approximates G′ within η · n in value, with tree depth N(η, n, m).The approximation is measured by ∥ValG′(ℓ′0, ·) − ValG′′(ℓ′′0, ·)∥∞.Source: §B.2 · p. 22
- The acyclic construction induces an η·n-optimal Min strategy in G′ whose plays have length at most N(η, n, m).The length bound carries over when the copies are folded back together.Source: §B.2 · p. 23
B.3 Proof of Remark 24
Remark 24 bounds the convergence rate by over-approximating and repeatedly unfolding the inductive recurrence for N.
B.3 Proof of Remark 24
- For d ≥ 2, the remark over-approximates the inductive formula for N to bound the convergence rate.The recurrence is then repeatedly unfolded.Source: §B.3 · p. 23
- One displayed expression in the recurrence expansion is (Kxk + 1) · n.Source: §B.3 · p. 23
- The derivation uses Kxk + 1 = xk xk+1 by definition of xk+1.Source: §B.3 · p. 23