  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.
