real-time system designers

Abstract: 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.

Abstract: An instance of {\sc Pinwheel Packing} is a list of positive integers $a_1,\ldots,a_k$. A feasible schedule assigns one task to every integer time so that every interval of $a_i$ consecutive times contains task $i$. The instance is \emph{dense} when $\sum_i1/a_i=1$. We prove that {\sc Dense Pinwheel Packing} is NP-complete even when every period is encoded in unary and equal periods are listed as distinct tasks. Consequently, the usual binary-encoded problem is strongly NP-complete. Kleinberg and Mishra also prove NP-completeness \cite[Corollary~5.1]{KleinbergMishra2026}, but their reduction uses periods of exponential numerical size and therefore yields only weak NP-hardness. Our proof uses a direct reduction from triangle partition in a sparse tripartite graph. If each of the three parts of the source graph has $n$ vertices, the reduction produces $O(n^4\log^3 n)$ explicitly listed tasks, each with period $O(n^4\log^3 n)$; consequently, its full unary encoding has length $O(n^8\log^6 n)$.