Controlling Golog Programs against MTL Constraints

TL;DR

This paper introduces a method to integrate Metric Temporal Logic (MTL) constraints into Golog programs, enabling automatic synthesis of controllers that manage high-level robot behaviors alongside low-level platform operations.

Contribution

It extends Golog with clocks and MTL constraints, providing a formal framework for concurrent execution and controller synthesis to satisfy temporal specifications.

Findings

Decidability of the extended Golog with MTL constraints

A synthesis method for controllers managing high and low-level actions

Theoretical foundations for the integration of clocks and MTL in Golog

Abstract

While Golog is an expressive programming language to control the high-level behavior of a robot, it is often tedious to use on a real robotic system. On an actual robot, the user needs to consider low-level details, such as enabling and disabling hardware components, e.g., a camera to detect objects for grasping. In other words, high-level actions usually pose implicit temporal constraints on the low-level platform, which are typically independent of the concrete program to be executed. In this paper, we propose to make these constraints explicit by modeling them as MTL formulas, which enforce the execution of certain low-level platform operations in addition to the main program. Based on results from timed automata controller synthesis, we describe a method to synthesize a controller that executes both the high-level program and the low-level platform operations concurrently in order to satisfy the MTL specification. This allows the user to focus on the high-level behavior without the need to consider low-level operations. We present an extension to Golog by clocks together with the required theoretical foundations as well as decidability results.