Towards Bridging the Gap between High-Level Reasoning and Execution on Robots
Till Hofmann
TL;DR
The work addresses the gap between high-level planning and real-time robot execution under uncertainty. It introduces t-ESG, a metric-time extension of ESG/Golog, and shows how robot self-models can be represented as timed automata, enabling MTL-based specifications and synthesis. It establishes decidability results for finite-domain settings, outlines offline and online plan-transformation pipelines, and develops a region-based, WSTS-enabled synthesis framework using ATA/MTL translations and timed games. The framework supports verification and controller synthesis, with practical applicability to real robotic platforms while carefully avoiding undecidability through clock-restriction strategies and abstraction mechanisms. Overall, the approach provides a principled pathway to guarantee timing-constrained behaviors in autonomous robots through formal logic, automata, and game-theoretic synthesis.
Abstract
When reasoning about actions, e.g., by means of task planning or agent programming with Golog, the robot's actions are typically modeled on an abstract level, where complex actions such as picking up an object are treated as atomic primitives with deterministic effects and preconditions that only depend on the current state. However, when executing such an action on a robot it can no longer be seen as a primitive. Instead, action execution is a complex task involving multiple steps with additional temporal preconditions and timing constraints. Furthermore, the action may be noisy, e.g., producing erroneous sensing results and not always having the desired effects. While these aspects are typically ignored in reasoning tasks, they need to be dealt with during execution. In this thesis, we propose several approaches towards closing this gap.