Symbolic Approximation of Weighted Timed Games

TL;DR

This paper extends the class of weighted timed games to include negative weights, demonstrating that their values can be approximated using a symbolic value iteration algorithm, despite the problem's inherent complexity.

Contribution

It introduces an extension to existing classes of weighted timed games to handle negative weights and proposes a symbolic approximation algorithm.

Findings

Negative weights can be incorporated while maintaining approximation complexity.

A symbolic value iteration algorithm effectively approximates game values.

The approach extends analysis capabilities to energy-like models.

Abstract

Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation schema on this class.