You May Delay, but Time Will Not: Timed Games Under Delayed Control

TL;DR

This paper investigates timed games with delayed control actions, showing undecidability in unbounded cases and providing a doubly-exponential algorithm for bounded scenarios, enabling practical verification with existing tools.

Contribution

It introduces a formal model for timed games with delayed actions and offers a reduction-based algorithm for bounded cases, extending verification capabilities.

Findings

Undecidability for unbounded pending actions.

A doubly-exponential algorithm for bounded pending actions.

Practical verification using UPPAAL.

Abstract

Inspired by Martin Fr\"anzle's persistent and influential work on capturing and handling delay inherent to cyber-physical systems in the formal verification of such systems, we study timed games where controllable actions do not take effect immediately, but only after some delay, i.e., they are scheduled for later execution. We show that solving such games is undecidable if an unbounded number of actions can be pending. On the other hand, we present a doubly-exponential time algorithm for games with a bound on the number of pending actions, based on a reduction to classical timed games. This makes timed games under delayed control with bounded schedules solvable with existing tools like UPPAAL.