Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints

TL;DR

This paper presents a method for synthesizing controllers for Golog programs over finite domains with metric temporal constraints by reducing the problem to MTL synthesis, ensuring the execution respects platform-specific constraints.

Contribution

It introduces a novel approach to formulate and synthesize controllers for Golog programs with temporal constraints using timed automata and MTL, ensuring correctness and platform compatibility.

Findings

Controller synthesis reduces to MTL synthesis for finite domain Golog programs.

Constructed timed automata accurately represent program and platform constraints.

Synthesized controllers guarantee execution traces match original program effects.

Abstract

Executing a Golog program on an actual robot typically requires additional steps to account for hardware or software details of the robot platform, which can be formulated as constraints on the program. Such constraints are often temporal, refer to metric time, and require modifications to the abstract Golog program. We describe how to formulate such constraints based on a modal variant of the Situation Calculus. These constraints connect the abstract program with the platform models, which we describe using timed automata. We show that for programs over finite domains and with fully known initial state, the problem of synthesizing a controller that satisfies the constraints while preserving the effects of the original program can be reduced to MTL synthesis. We do this by constructing a timed automaton from the abstract program and synthesizing an MTL controller from this automaton, the platform models, and the constraints. We prove that the synthesized controller results in execution traces which are the same as those of the original program, possibly interleaved with platform-dependent actions, that they satisfy all constraints, and that they have the same effects as the traces of the original program. By doing so, we obtain a decidable procedure to synthesize a controller that satisfies the specification while preserving the original program.