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

TL;DR

This work investigates real-time controller synthesis when control actions are subject to execution delays. The authors introduce timed games under delayed control, where a controller schedules actions to occur after a delay and where intervening actions may alter the system state before execution. They prove undecidability for the unbounded-pending-actions setting, and show a doubly-exponential-time decision procedure for the bounded-schedule case by reducing to classical timed games, making the problem amenable to existing tools like UPPAAL. Additionally, they establish that timed games under delayed control are a conservative extension of standard timed games, preserving ExpTime-hardness, thereby linking the new model to established theory while providing a practical pathway for analysis in bounded cases.

Abstract

Inspired by Martin Fränzle'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.

Figures (2)

• Figure 1: LEGO Mindstorm Production System.
• Figure 2: The production system ${\cal P}$ (top) and the scheduler ${\cal S}$ (bottom).