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

Till Hofmann  Gerhard Lakemeyer
Knowledge-Based Systems Group, RWTH Aachen University
{hofmann<EMAIL_ADDRESS>
###### 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.

##  1 Introduction

While Golog (?), an agent programming language based on the Situation Calculus
(?; ?), allows a clear and abstract specification of an agent’s behavior,
executing a Golog program on a real robot often creates additional issues.
Typically, the robot’s platform requires additional constraints that are
ignored when designing a Golog program. As an example, a robot may need to
calibrate its arm before it can use it. One way to deal with such platform
constraints is to split the reasoning into two parts (?): First, an abstract
Golog program specifies the intended behavior of the robot, without taking the
robot platform into account. In a second step, the platform is considered by
transforming the abstract program into a program that is executable on the
particular platform, given a model of the platform and temporal constraints
that connect the platform with the plan.

In this paper, we propose a method for such a transformation: We model the
robot platform with a timed automaton (TA) and formulate constraints with
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$ (?), a modal variant of the Situation Calculus extended with temporal
operators and metric time. We then synthesize a controller that executes the
abstract program, but also inserts additional platform actions to satisfy the
platform constraints. To do so, we restrict the Golog program to a finite
domain, finite traces, and a fully known initial state. This allows us to
reduce the controller synthesis problem to the MTL control problem, which has
been shown to be decidable (?). Furthermore, for the purpose of this paper, we
only use time to formulate temporal constraints on the robot platform and we
restrict programs to untimed programs, i.e., in contrast to programs in (?), a
program may not refer to time and action preconditions and effects are time-
independent. We will revisit these restrictions in the concluding section.

In the following, we first give an overview on the Situation Calculus and
Golog and related work in Section 2 and summarize
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$ in Section 3. In Section 4, we describe timed automata and Metric Temporal
Logic (MTL), before we summarize the MTL synthesis problem. We explain how to
transform a Golog program over a finite domain with a complete initial state
into a TA in Section 5 and how to model a robot platform with a TA and
temporal constraints in Section 6. Both TA and the constraints are then used
in Section 7 to synthesize a controller that executes the program while
satisfying all constraints. We conclude in Section 8.

##  2 Related Work

The Situation Calculus (?; ?) is a first-order logic for representing and
reasoning about actions. Following ?, action preconditions and effects as well
as information about the initial situation are then encoded as so-called
_Basic Action Theories (BATs)_. The action programming language Golog (?) and
its concurrent variant ConGolog (?) are based on the Situation Calculus and
offer imperative programming constructs such as sequences of actions and
iteration as well as non-deterministic branching and non-deterministic choice.
The semantics of Golog and its on-line variant IndiGolog can be specified in
terms of transitions (?). The logic $\mathcal{E\negthinspace S}$ (?) is a
modal variant of the Situation Calculus which gets rid of explicit situation
terms and uses modal operators instead. The logic $\mathcal{E\negthinspace
S\negthinspace G}$ (?; ?) is a temporal extension of $\mathcal{E\negthinspace
S}$ and used for the verification of Golog programs. It specifies program
transition semantics similar to the transition semantics of IndiGolog and
extends $\mathcal{E\negthinspace S}$ with the temporal operators $\mathbf{X}$
(_next_) and $\,\mathbf{U}$ (_until_). The logic
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$ (?) extends $\mathcal{E\negthinspace S\negthinspace G}$ with metric time
and timing constraints on the _until_ operator.

MTL (?) is an extension of Linear Time Logic (LTL) with metric time, which
allows expressions such as $\mathbf{F}_{\leq c}$, meaning _eventually within
time $c$_. In MTL, formulas are interpreted over _timed words_ or _timed state
sequences_ , where each state specifies which propositions are true, and each
state has an associated time value. Depending on the choice of the state and
time theory, the satisfiability problem for MTL becomes undecidable (?).
However, both for finite words and for a pointwise semantics, it has been
shown to be decidable (?; ?).

Similar to the proposed approach, ? (?) extend Golog for self-maintenance by
allowing temporal constraints using Allen’s Interval Algebra (?). Those
constraints are resolved on-line by interleaving the original program with
maintenance actions. Closely related is also the work by ? (?), who propose a
hybrid approach of temporal constraint reasoning and reasoning about actions
based on the Situation Calculus. They also allow constraints based on Allen’s
Interval Algebra, which are translated into a temporal constraint network. ?
describe a synthesis method for LTL and LDL specifications over finite traces
(?). Similar to MTL synthesis, they partition the propositions in controllable
and uncontrollable symbols and use games to synthesize a controller. Based on
$\mathit{LTL}_{f}$ synthesis, ? describe a synthesis method that controls a
robot against uncontrollable environment actions under resource constraints
(?). They model the underlying planning problem as a graph, where each vertex
describes the state of the world and each edge corresponds to an action,
either by the agent or by the environment. In contrast to this work, they do
not allow metric temporal constraints.

##  3 Timed $\mathcal{E\negthinspace S\negthinspace G}$

In this section, we summarize the syntax and semantics of
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$ (?), which is based on $\mathcal{E\negthinspace S\negthinspace G}$ (?) and
$\mathcal{E\negthinspace S}$ (?), modal variants of the Situation Calculus. We
refer to (?) for a more complete description.

The language has two sorts: object and action. A special feature inherited
from $\mathcal{E\negthinspace S}$ is the use of countably infinite sets of
standard names for both sorts. Standard object names syntactically look like
constants, but are intended to be isomorphic with the set of all objects of
the domain. In other words, standard object names can be thought of as
constants that satisfy the unique name assumption and domain closure for
objects. We assume that object standard names include the rational numbers
(including $\infty$) as a subsort. Action standard names are function symbols
of any arity whose arguments are standard object names. Examples are
$\mathit{pick}(o)$ and $\mathit{goto}(l_{1},l_{2})$ for picking up an object
and going from one location to another, respectively. Again, standard action
names range over all actions and satisfy the unique name assumption and domain
closure for actions. One advantage of using standard names is that quantifiers
can be understood substitutionally when defining the semantics. For
simplicity, we do not consider function symbols other than actions. Formally
the language is defined as follows:

###  3.1 Syntax

######  Definition 1 (Symbols of
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$).

The symbols of the language are from the following vocabulary:

  1. 1.

object variables $x_{1},x_{2},x_{3},\ldots,y_{1},\ldots$,

  2. 2.

action variables $a,a_{1},a_{2},a_{3},\ldots$,

  3. 3.

object standard names $\mathcal{N}_{O}=\\{o_{1},o_{2},o_{3},\ldots\\}$,

  4. 4.

action standard names $\mathcal{N}_{A}=\\{p_{1},p_{2},p_{3},\ldots\\}$,

  5. 5.

fluent predicates of arity $k$:
$\mathcal{F}^{k}:\\{F_{1}^{k},F_{2}^{k},\ldots\\}$, e.g.,
$\mathit{Holding(o)}$; we assume this list contains the distinguished
predicate $\mathit{Poss}$

  6. 6.

rigid predicates of arity $k$:
$\mathcal{G}^{k}=\\{G_{1}^{k},G_{2}^{k},\ldots\\}$,

  7. 7.

open, closed, and half-closed intervals, e.g., $[1,2]$, with rational numbers
as interval endpoints,

  8. 8.

connectives and other symbols: $=$, $\wedge$, $\vee$, $\neg$, $\forall$,
$\square$, $[\cdot]$, $\llbracket\cdot\rrbracket$, $\,\mathbf{U}_{I}\,$ (with
interval $I$).

We denote the set of standard names as
$\mathcal{N}=\mathcal{N}_{O}\cup\mathcal{N}_{A}$.

######  Definition 2 (Terms of
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$).

The set of terms of
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$ is the least set such that  (1) every variable is a term of the
corresponding sort,  (2) every standard name is a term.

######  Definition 3 (Formulas).

The _formulas of
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$_, consisting of _situation formulas_ and _trace formulas_ , are the least
set such that

  1. 1.

if $t_{1},\ldots,t_{k}$ are terms and $P$ is a $k$-ary predicate symbol, then
$P(t_{1},\ldots,t_{k})$ is a situation formula,

  2. 2.

if $t_{1}$ and $t_{2}$ are terms, then $(t_{1}=t_{2})$ is a situation formula,

  3. 3.

if $\alpha$ and $\beta$ are situation formulas, $x$ is a variable, $\delta$ is
a program (defined below), and $\phi$ is a trace formula, then
$\alpha\wedge\beta$, $\neg\alpha$, $\forall x.\,\alpha$, $\square\alpha$,
$[\delta]\alpha$, and $\llbracket\delta\rrbracket\phi$ are situation formulas,

  4. 4.

if $\alpha$ is a situation formula, it is also a trace formula,

  5. 5.

if $\phi$ and $\psi$ are trace formulas, $x$ is a variable, and $I$ is an
interval, then $\phi\wedge\psi$, $\neg\phi$, $\forall x.\,\phi$, and
$\phi\,\mathbf{U}_{I}\,\psi$ are also trace formulas.

A predicate symbol with standard names as arguments is called a _primitive
formula_ , and we denote the set of primitive formulas as $\mathcal{P}_{F}$.
We read $\square\alpha$ as “$\alpha$ holds after executing any sequence of
actions”, $[\delta]\alpha$ as “$\alpha$ holds after the execution of program
$\delta$”, $\llbracket\delta\rrbracket\alpha$ as “$\alpha$ holds during the
execution of program $\delta$”, $\phi\,\mathbf{U}_{I}\,\psi$ as “$\phi$ holds
_until_ $\psi$ holds, and $\psi$ holds within interval $I$”.

A formula is called static if it contains no $[\cdot]$, $\square$, or
$\llbracket\cdot\rrbracket$ operators. It is called fluent if it is static and
does not mention $\mathit{Poss}$.

We also write $<c$, $\leq c$, $=c$, $>c$, and $\geq c$ for the respective
intervals $[0,c)$, $[0,c]$, $[c,c]$, $(c,\infty)$, and $[c,\infty)$. We use
the short-hand notations
$\mathbf{F}_{I}\phi\overset{def}{=}(\top\,\mathbf{U}_{I}\,\phi)$ (_future_)
and $\mathbf{G}_{I}\phi\overset{def}{=}\neg\mathbf{F}_{I}\neg\phi$
(_globally_). For intervals, $c+[s,e]$ denotes the interval $[s+c,e+c]$,
similarly for $c+(s,e)$, $c+[s,e)$, and $c+(s,e]$. We also omit the interval
$I$ if $I=[0,\infty)$, e.g., $\phi\,\mathbf{U}\,\psi$ is short for
$\phi\,\mathbf{U}_{[0,\infty)}\,\psi$.

Finally we define the syntax of Golog programs referred to by the operators
$[\delta]$ and $\llbracket\delta\rrbracket$:

######  Definition 4 (Programs).

$\delta::=t\>\mid\>\alpha?\>\mid\>\delta_{1};\delta_{2}\>\mid\>\delta_{1}|\delta_{2}\>\mid\>\pi
x.\,\delta\>\mid\>\delta_{1}\|\delta_{2}\>\mid\>\delta^{*}$

where $t$ is an action term and $\alpha$ is a static situation formula. A
program consists of actions $t$, tests $\alpha?$, sequences
$\delta_{1};\delta_{2}$, nondeterministic branching $\delta_{1}|\delta_{2}$,
nondeterministic choice of argument $\pi x.\,\delta$, interleaved concurrency
$\delta_{1}\|\delta_{2}$, and nondeterministic iteration $\delta^{*}$.

We also use the abbreviation $\mathit{nil}\overset{def}{=}\top?$ for the empty
program that always succeeds. We remark that the above program constructs are
a proper subset of the original ConGolog (?). We have left out other
constructs such as prioritized concurrency for simplicity.

###  3.2 Semantics

######  Definition 5 (Timed Traces).

A _timed trace_ is a finite timed sequence of action standard names with
monotonically non-decreasing time. Formally, a trace $\pi$ is a mapping
$\pi:\mathbb{N}\rightarrow\mathcal{P}_{A}\times\mathbb{Q}$, and for any
$i,j\in\mathbb{N}$ with $\pi(i)=\left(\sigma_{i},t_{i}\right)$,
$\pi(j)=\left(\sigma_{j},t_{j}\right)$ : If $i<j$, then $t_{i}\leq t_{j}$.

We denote the set of timed traces as $\mathcal{Z}$. For a timed trace
$z=\left(a_{1},t_{1}\right)\ldots\left(a_{k},t_{k}\right)$, we define
$\mathit{time}(z)\overset{def}{=}t_{k}$ for $k>0$ and
$\mathit{time}(\langle\rangle)\overset{def}{=}0$, i.e., $\mathit{time}(z)$ is
the time value of the last action in $z$. We define the timed trace $z^{0}$
where all actions occur at time $0$ as
$z^{0}=\left(a_{1},0\right)\left(a_{2},0\right)\ldots\left(a_{n},0\right)$.

######  Definition 6 (World).

Intuitively, a world $w$ determines the truth of fluent predicates, not just
initially, but after any (timed) sequence of actions. Formally, a world $w$ is
a mapping $\mathcal{P}_{F}\times\mathcal{Z}\rightarrow\\{0,1\\}$. If $G$ is a
rigid predicate symbol, then for all $z$ and $z^{\prime}$ in $\mathcal{Z}$,
$w[G(n_{1},\ldots,n_{k}),z]=w[G(n_{1},\ldots,n_{k}),z^{\prime}]$.

Similar to $\mathcal{E\negthinspace S}$ and $\mathcal{E\negthinspace
S\negthinspace G}$, the truth of a fluent after any sequence of actions is
determined by a world $w$. Different from $\mathcal{E\negthinspace S}{}$ and
$\mathcal{E\negthinspace S\negthinspace G}{}$, we require all traces referred
to by a world to contain time values for each action. This also means that in
the same world, a fluent predicate $F(\vec{n})$ may have a different value
after the same sequence of actions if the actions were executed at different
times, i.e., $w[F(\vec{n},\langle\left(a_{1},1\right)\rangle]$ may have a
different value than $w[F(\vec{n},\langle\left(a_{1},2\right)\rangle]$.
However, for simplicity the actions considered in basic action theories (see
Section 3.3) do not make use of this feature.

Next we define the transitions programs may take in a given world $w$. In two
places these refer to the satisfaction of situation formulas (see Definition 9
below).

######  Definition 7 (Program Transition Semantics).

The transition relation $\overset{w}{\rightarrow}$ among configurations, given
a world $w$, is the least set satisfying

  1. 1.

$\langle z,a\rangle\overset{w}{\rightarrow}\langle
z\cdot\left(p,t\right),\mathit{nil}\rangle$, if $t\geq\mathit{time}(z)$, and
$w,z\models\mathit{Poss}(p)$

  2. 2.

$\langle z,\delta_{1};\delta_{2}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\gamma;\delta_{2}\rangle$, if $\langle
z,\delta_{1}\rangle\overset{w}{\rightarrow}\langle z\cdot p,\gamma\rangle$,

  3. 3.

$\langle z,\delta_{1};\delta_{2}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\rangle$ if $\langle z,\delta_{1}\rangle\in\mathcal{F}^{w}$
and $\langle z,\delta_{2}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\rangle$

  4. 4.

$\langle z,\delta_{1}|\delta_{2}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\rangle$ if $\langle
z,\delta_{1}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\rangle$ or $\langle
z,\delta_{2}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\rangle$

  5. 5.

$\langle z,\pi x.\,\delta\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\rangle$, if $\langle
z,\delta^{x}_{n}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\rangle$ for some $n\in\mathcal{N}_{x}$

  6. 6.

$\langle z,\delta^{*}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\gamma;\delta^{*}\rangle$ if $\langle
z,\delta\rangle\overset{w}{\rightarrow}\langle z\cdot p,\gamma\rangle$

  7. 7.

$\langle z,\delta_{1}\|\delta_{2}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta^{\prime}\|\delta_{2}\rangle$ if
$z,\delta_{1}\overset{w}{\rightarrow}\langle z\cdot p,\delta^{\prime}\rangle$

  8. 8.

$\langle z,\delta_{1}\|\delta_{2}\rangle\overset{w}{\rightarrow}\langle z\cdot
p,\delta_{1}\|\delta^{\prime}\rangle$ if
$z,\delta_{2}\overset{w}{\rightarrow}\langle z\cdot p,\delta^{\prime}\rangle$

The set of final configurations $\mathcal{F}^{w}$ is the smallest set such
that

  1. 1.

$\langle z,\alpha?\rangle\in\mathcal{F}^{w}$ if $w,z\models\alpha$,

  2. 2.

$\langle z,\delta_{1};\delta_{2}\rangle\in\mathcal{F}^{w}$ if $\langle
z,\delta_{1}\rangle\in\mathcal{F}^{w}$ and $\langle
z,\delta_{2}\rangle\in\mathcal{F}^{w}$

  3. 3.

$\langle z,\delta_{1}|\delta_{2}\rangle\in\mathcal{F}^{w}$ if $\langle
z,\delta_{1}\rangle\in\mathcal{F}^{w}$, or $\langle
z,\delta_{2}\rangle\in\mathcal{F}^{w}$

  4. 4.

$\langle z,\pi x.\,\delta\rangle\in\mathcal{F}^{w}$ if $\langle
z,\delta^{x}_{n}\rangle\in\mathcal{F}^{w}$ for some $n\in\mathcal{N}_{x}$

  5. 5.

$\langle z,\delta^{*}\rangle\in\mathcal{F}^{w}$

  6. 6.

$\langle z,\delta_{1}\|\delta_{2}\rangle\in\mathcal{F}^{w}$ if $\langle
z,\delta_{1}\rangle\in\mathcal{F}^{w}$ and $\langle
z,\delta_{2}\rangle\in\mathcal{F}^{w}$

The program transition semantics is very similar to the semantics of
$\mathcal{E\negthinspace S\negthinspace G}$. The only difference is in Rule 1,
which has an additional constraint on the time, and which requires the action
to be executable.

######  Definition 8 (Program Traces).

Given a world $w$ and a finite sequence of action standard names $z$, the set
$\|\delta\|^{z}_{w}$ of _finite timed traces of a program $\delta$_ is

$\|\delta\|^{z}_{w}=\\\ \\{z^{\prime}\in\mathcal{Z}\mid\langle
z,\delta\rangle\overset{w}{\rightarrow}^{*}\langle z\cdot
z^{\prime},\delta^{\prime}\rangle\text{ and }\langle z\cdot
z^{\prime},\delta^{\prime}\rangle\in\mathcal{F}^{w}\\}$

######  Definition 9 (Truth of Situation and Trace Formulas).

Given a world $w\in\mathcal{W}$ and a situation formula $\alpha$, we define
$w\models\alpha$ as $w,\langle\rangle\models\alpha$, where for any
$z\in\mathcal{Z}$:

  1. 1.

$w,z\models F(n_{1},\ldots,n_{k})$ iff $w[F(n_{1},\ldots,n_{k}),z]=1$;

  2. 2.

$w,z\models(n_{1}=n_{2})$ iff $n_{1}$ and $n_{2}$ are identical;

  3. 3.

$w,z\models\alpha\wedge\beta$ iff $w,z\models\alpha$ and $w,z\models\beta$;

  4. 4.

$w,z\models\neg\alpha$ iff $w,z\not\models\alpha$;

  5. 5.

$w,z\models\forall x.\,\alpha$ iff $w,z\models\alpha^{x}_{n}$ for every
standard name of the right sort;

  6. 6.

$w,z\models\square\alpha$ iff $w,z\cdot z^{\prime}\models\alpha$ for all
$z^{\prime}\in\mathcal{Z}$;

  7. 7.

$w,z\models[\delta]\alpha$ iff for all finite
$z^{\prime}\in\|\delta\|^{z}_{w}$, $w,z\cdot z^{\prime}\models\alpha$;

  8. 8.

$w,z\models\llbracket\delta\rrbracket\phi$ iff for all
$\tau\in\|\delta\|^{z}_{w}$, $w,z,\tau\models\phi$.

Intuitively, $[\delta]\alpha$ means that _after every execution_ of $\delta$,
the situation formula $\alpha$ is true. $\llbracket\delta\rrbracket\phi$ means
that _during every execution_ of $\delta$, the trace formula $\phi$ is true.

The truth of trace formulas $\phi$ is defined as follows for
$w\in\mathcal{W}$, $z,\tau\in\mathcal{Z}$:

  1. 1.

$w,z,\tau\models\alpha$ iff $w,z\models\alpha$ and $\alpha$ is a situation
formula;

  2. 2.

$w,z,\tau\models\phi\wedge\psi$ iff $w,z,\tau\models\phi$ and
$w,z,\tau\models\psi$;

  3. 3.

$w,z,\tau\models\neg\phi$ iff $w,z,\tau\not\models\phi$;

  4. 4.

$w,z,\tau\models\forall x.\,\phi$ iff $w,z,\tau\models\phi^{x}_{n}$ for all
$n\in\mathcal{N}_{x}$;

  5. 5.

$w,z,\tau\models\phi\,\mathbf{U}_{I}\,\psi$ iff there is a
$z_{1}\neq\langle\rangle$ such that

    1. (a)

$\tau=z_{1}\cdot\tau^{\prime}$,

    2. (b)

$\mathit{time}(z_{1})\in\mathit{time}(z)+I$,

    3. (c)

$w,z\cdot z_{1},\tau^{\prime}\models\psi$,

    4. (d)

for all $z_{2}\neq z_{1}$ with $z_{1}=z_{2}\cdot z_{3}$: $w,z\cdot
z_{2},z_{3}\cdot\tau^{\prime}\models\phi$.

######  Definition 10 (Validity).

A situation formula $\alpha$ is _valid_ (written $\models\alpha$) iff for
every world $w,$ $w\models\alpha$. A trace formula $\phi$ is _valid_
($\models\phi$) iff for every world $w$ and every trace $\tau$,
$w,\langle\rangle,\tau\models\phi$.

###  3.3 Basic Action Theories

A basic action theory (BAT) defines the preconditions and effects of all
actions of the domain, as well as the initial state:

######  Definition 11 (basic action theory).

Given a finite set of fluent predicates $\mathcal{F}$, a set
$\Sigma\subseteq\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace
S\negthinspace G}$ of sentences is called a basic action theory (BAT) over
$\mathcal{F}$ iff
$\Sigma=\Sigma_{0}\cup\Sigma_{\text{pre}}\cup\Sigma_{\text{post}}$, where
$\Sigma$ mentions only fluents in $\mathcal{F}$ and

  1. 1.

$\Sigma_{0}$ is any set of fluent sentences,

  2. 2.

$\Sigma_{\text{pre}}$ consists of a single sentence of the form
$\square\mathit{Poss}(a)\,\equiv\;\pi$, where $\pi$ is a fluent formula with
free variable $a$.111Free variables are implicitly universal quantified from
the outside. The modality $\Box$ has lower syntactic precedence than the
connectives, and $[\cdot]$ has the highest priority.

  3. 3.

$\Sigma_{\text{post}}$ is a set of sentences, one for each fluent predicate
$F\in\mathcal{F}$, of the form $\square[a]F(\vec{x})\,\equiv\;\gamma_{F}$.

The set $\Sigma_{0}$ describes the initial state, $\Sigma_{\text{pre}}$
defines the preconditions of all actions of the domain, and
$\Sigma_{\text{post}}$ defines action effects by specifying for each fluent of
the domain whether the fluent is true after doing some action $a$.

We will also consider BATs restricted to a finite domain of actions and
objects:

######  Definition 12 (Finite-domain BAT).

We call a BAT $\Sigma$ a _ finite-domain basic action theory (fd-BAT)_ iff

  1. 1.

each $\forall$ quantifier in $\Sigma$ occurs as $\forall
x.\,\tau_{i}(x)\supset\phi(x)$, where $\tau_{i}$ is a rigid predicate, $i=o$
if $x$ is of sort object, and $i=a$ if $x$ is of sort action;

  2. 2.

$\Sigma_{0}$ contains axioms

     * •

$\tau_{o}(x)\equiv(x=n_{1}\vee x=n_{2}\vee\ldots\vee x=n_{k})$ and

     * •

$\tau_{a}(a)\equiv(a=m_{1}\vee a=m_{2}\vee\ldots\vee a=m_{l})$

where the $n_{i}$ and $m_{j}$ are object and action standard names,
respectively. Also each $m_{j}$ may only mention object standard names
$n_{i}$.

We call a formula $\alpha$ that only mentions symbols and standard names from
$\Sigma$ _restricted to $\Sigma$_ and we denote the set of primitive formulas
restricted to $\Sigma$ as $\mathcal{P}_{\Sigma}$ and the action standard names
mentioned in $\Sigma$ as $A_{\Sigma}$. We also write $\exists
x\mathbf{:}i.\,\phi$ for $\exists x.\,\tau_{i}(x)\wedge\phi$ and $\forall
x\mathbf{:}i.\,\phi$ for $\forall x.\,\tau_{i}(x)\supset\phi$. Since an fd-BAT
essentially restricts the domain to be finite, quantifiers of type object can
be understood as abbreviations:

$\displaystyle\exists x\mathbf{:}\tau_{o}.\phi$
$\displaystyle\overset{def}{=}\bigvee_{i=1}^{k}\phi^{x}_{n_{i}},$
$\displaystyle\forall x\mathbf{:}\tau_{o}.\phi$
$\displaystyle\overset{def}{=}\bigwedge_{i=1}^{k}\phi^{x}_{n_{i}},$

and similarly for quantifiers of type action.

In addition to a finite domain, we also restrict a BAT such that it completely
determines the initial situation:

######  Definition 13 (determinate BAT).

A fd-BAT $\Sigma$ is _determinate_ iff every for atomic formula $\alpha$
restricted to $\Sigma$, either $\Sigma_{0}\models\alpha$ or
$\Sigma_{0}\models\neg\alpha$.

Next, given a world $w$, we define a world $w_{\Sigma}$ that is consistent
with $\Sigma$:

######  Definition 14.

For any world $w$ and basic action theory $\Sigma$, we define a world
$w_{\Sigma}$ which is like $w$ except that it satisfies the
$\Sigma_{\text{pre}}$ and $\Sigma_{\text{post}}$ sentences of $\Sigma$.

######  Lemma 1 ((?)).

For any $w$, $w_{\Sigma}$ exists and is uniquely defined.

For a determinate BAT over a set of fluent predicates $\mathcal{F}$, we can
show that $\Sigma$ fully determines the truth of every fluent
$f\in\mathcal{F}$, not only initially, but after any sequence of actions:

######  Lemma 2.

Let $\Sigma$ be a determinate BAT over $\mathcal{F}$, $\delta$ a program over
$\Sigma$ and $w,w^{\prime}$ two worlds, and $z\in\mathcal{Z}$ a finite trace
such that
$\langle\langle\rangle,\delta\rangle\overset{w_{\Sigma}}{\longrightarrow^{*}}\langle
z,\delta^{\prime}\rangle$. Then

  1. 1.

$\langle\langle\rangle,\delta\rangle\overset{w^{\prime}_{\Sigma}}{\longrightarrow^{*}}\langle
z,\delta^{\prime}\rangle$,

  2. 2.

for every primitive formula $F\left(\vec{t}\right)$ with $F\in\mathcal{F}$:
$w_{\Sigma}[F(\vec{t}),z]=w^{\prime}_{\Sigma}[F(\vec{t}),z]$

###### Proof.

By induction over the length of $z$.

  * •

Let $z=\langle\rangle$. By definition of a determinate BAT, we know that
$w_{\Sigma}[F(\vec{t}),\langle\rangle]=1\Leftrightarrow
w^{\prime}_{\Sigma}[F(\vec{t}),\langle\rangle]=1$.

  * •

Let $z=z^{\prime}\cdot\left(p,t\right)$. By induction, for each atomic formula
$\alpha$,
$w_{\Sigma}[\alpha,z^{\prime}]=w^{\prime}_{\Sigma}[\alpha,z^{\prime}]$, and
thus, for each fluent situation formula $\gamma$,
$w_{\Sigma},z^{\prime}\models\gamma$ iff
$w^{\prime}_{\Sigma},z^{\prime}\models\gamma$. Furthermore, we know from
$\langle\langle\rangle,\delta\rangle\overset{w_{\Sigma}}{\longrightarrow^{*}}\langle
z,\delta^{\prime}\rangle$ that for some $z^{\prime},\delta^{\prime\prime}$,
$\langle
z^{\prime},\delta^{\prime\prime}\rangle\overset{w_{\Sigma}}{\longrightarrow}\langle
z,\delta^{\prime}\rangle$ and thus
$w_{\Sigma},z^{\prime}\models\mathit{Poss}(p)$. As both $w_{\Sigma}$ and
$w^{\prime}_{\Sigma}$ satisfy $\Sigma_{\text{pre}}$, it follows that
$w^{\prime}_{\Sigma},z^{\prime}\models\mathit{Poss}(p)$ and therefore
$\langle\langle\rangle,\delta\rangle\overset{w^{\prime}_{\Sigma}}{\longrightarrow^{*}}\langle
z,\delta^{\prime}\rangle$. As both $w_{\Sigma}$ and $w^{\prime}_{\Sigma}$
satisfy $\Sigma_{\text{post}}$ and there is a successor state axiom for each
$F$, it follows that $w_{\Sigma}[F(\vec{t}),z]=1$ iff
$w_{\Sigma},z^{\prime}\models\gamma_{F}(\vec{t})$ and
$w^{\prime}_{\Sigma}[F(\vec{t}),z]=1$ iff
$w^{\prime}_{\Sigma},z^{\prime}\models\gamma_{F}(\vec{t})$ and thus
$w_{\Sigma}[F(\vec{t}),z]=1\Leftrightarrow
w^{\prime}_{\Sigma}[F(\vec{t}),z]=1$. ∎

In fact, we can show that $\Sigma$ fully determines possible traces of
$\delta$, as well as the truth of any formula restricted to $\Sigma$:

######  Theorem 1.

Let $\Sigma$ be a determinate BAT, $\delta$ a program over $\Sigma$ and
$w,w^{\prime}$ two worlds, and $z\in\|\delta\|_{w_{\Sigma}}$, $\alpha$ a
situation formula and $\phi$ a trace formula, both restricted to $\Sigma$.
Then:

  1. 1.

$z\in\|\delta\|_{w^{\prime}_{\Sigma}}$

  2. 2.

$w_{\Sigma}\models[\delta]\alpha\Leftrightarrow
w^{\prime}_{\Sigma}\models[\delta]\alpha$

  3. 3.

$w_{\Sigma}\models\llbracket\delta\rrbracket\phi\Leftrightarrow
w^{\prime}_{\Sigma}\models\llbracket\delta\rrbracket\phi$

###### Proof.

Follows from Lemma 2. ∎

For the purpose of this paper and in contrast to (?), we do not have
distinguished function symbols $\mathit{now}$ and $\mathit{time}$ that allow
referring to time in a situation formula. In particular, this means that we
cannot define time-dependent preconditions or effects in a BAT. Thus, time is
only relevant for the truth of trace formulas. Also, a program’s traces are
not restricted with respect to time:

######  Proposition 1.

Given a BAT $\Sigma$, a program $\delta$, and a world $w$. Let
$\tau_{1},\tau_{2}$ be two traces with $\tau_{1}(i)=\left(a_{i},t_{i}\right)$,
$\tau_{2}(i)=\left(a_{i},t^{\prime}_{i}\right)$ for every $i$ (i.e., they
contain the same action symbols but different time points). Then
$\tau_{1}\in\|\delta\|_{w_{\Sigma}}$ iff $\tau_{2}\in\|\delta\|_{w_{\Sigma}}$.

#### A Simple Carrier Bot

With the following determinate fd-BAT, we describe a simple carrier bot that
is able to move to locations and pick up objects:

$\displaystyle\square\mathit{Poss}(a)\equiv$ $\displaystyle\exists
s\mathbf{:}o\exists g\mathbf{:}o.\,a=\mathit{s\\_goto}(s,g)\wedge\neg\exists
a^{\prime}\mathbf{:}a.\,\mathit{Perf}(a^{\prime})$ (1)
$\displaystyle\vee\exists s\mathbf{:}o\exists
g\mathbf{:}o.\,a=\mathit{e\\_goto}(s,g)\wedge\mathit{Perf}(\mathit{goto}(s,g))$
(2) $\displaystyle\vee\exists
o\mathbf{:}o,l\mathbf{:}o.\,a=\mathit{s\\_pick}(o)\wedge\neg\exists
a^{\prime}\mathbf{:}a.\,\mathit{Perf}(a^{\prime})$ (3)
$\displaystyle\quad\wedge\mathit{RAt}(l)\wedge\mathit{At}(o,l)$
$\displaystyle\vee\exists
o\mathbf{:}o.\,a=\mathit{e\\_pick}(o)\wedge\mathit{Perf}(pick(o))$ (4)

The precondition axioms state that it is possible to start the goto action
($\mathit{s\\_goto}$) if the robot is not performing any action (Equation 1),
it can stop the goto action if it is currently performing it (Equation 2).
Furthermore, it can start picking up an object if it is not performing any
other action and it is at the same position as the object (Equation 3).
Finally, it can stop picking if it is currently performing a pick action
(Equation 4).

By splitting actions into start and stop actions, we can execute multiple
actions concurrently. We will later insert platform actions that are executed
in addition and concurrent to the program’s actions. Also, splitting actions
into start and stop actions allows us to model that only the start but not the
end of an action is under the robot’s control. In Section 7, we will let the
environment control all end actions, i.e., the environment will decide when an
action ends.

In addition to the precondition axioms, we also define successor state axioms
for all fluents of the domain:

$\displaystyle\square[a]$ $\displaystyle\mathit{RAt}(l)\,\equiv\;\exists
s\mathbf{:}o.\,a=\mathit{e\\_goto}(s,l))$ (5)
$\displaystyle\quad\vee\mathit{RAt}(l)\wedge\neg\exists
s^{\prime}\mathbf{:}o\,\exists
g^{\prime}\mathbf{:}o.\,a=\mathit{s\\_goto}(s^{\prime},g^{\prime})$
$\displaystyle\square[a]$
$\displaystyle\mathit{At}(p,l)\,\equiv\;\mathit{At}(p,l)\wedge
a\neq\mathit{s\\_pick}(p)$ (6) $\displaystyle\square[a]$
$\displaystyle\mathit{Holding}(p)\,\equiv\;a=\mathit{e\\_pick}(p)\vee\mathit{Holding}(p)$
(7) $\displaystyle\square[a]$
$\displaystyle\mathit{Perf}(a^{\prime})\,\equiv\;$ (8) $\displaystyle\exists
s\mathbf{:}o\exists
g\mathbf{:}o.\,\left[a=\mathit{s\\_goto}(s,g)\right]\vee\exists
o\left[a=\mathit{s\\_pick}(o)\right]$
$\displaystyle\vee\mathit{Perf}(a^{\prime})\wedge\neg\exists
s\mathbf{:}o\exists g\mathbf{:}o\left[a=\mathit{e\\_goto}(s,g)\right]$
$\displaystyle\qquad\wedge\neg\exists
p\mathbf{:}o\left[a=\mathit{e\\_pick}(p)\right]$

Initially, the robot is at $m_{1}$ and object $o_{1}$ is at $m_{2}$. Only
$m_{1}$ is $\mathit{Spacious}$, which we will use in Section 6 as a
requirement for arm calibration:

$\displaystyle\Sigma_{0}=\\{\forall
x\mathbf{:}o.\,\mathit{RAt}(x)\equiv\left(x=m_{1}\right),$ (9)
$\displaystyle\forall x\mathbf{:}o\,\forall
y\mathbf{:}o.\,\mathit{At}(x,y)\equiv\left(x=o_{1}\wedge y=m_{2}\right),$
$\displaystyle\forall
x\mathbf{:}o.\,\mathit{Spacious}(x)\equiv\left(x=m_{1}\right),$
$\displaystyle\tau_{o}(x)\equiv\left(x=m_{1}\vee x=m_{2}\vee x=o_{1}\right),$
$\displaystyle\tau_{a}(a)\equiv\left(a=\mathit{s\\_goto}(m_{1},m_{2})\vee\ldots\vee
a=\mathit{e\\_pick}(o_{1})\right)\\}$

⬇

$\pi l_{r}.\>\mathit{RAt}(l_{r})?;\pi o.\,\pi l_{o}.\,\mathit{At}(o,l_{o})?$;

$\mathit{s\\_goto}(l_{r},l_{o});\mathit{e\\_goto}(l_{r},l_{o});\mathit{s\\_pick}(o);\mathit{e\\_pick}(o);$

Listing 1: An abstract program to fetch an object.

1 shows a simple program that picks up one object.

##  4 MTL Synthesis

Timed automata (TA) (?; ?) are a widely used model for representing real-timed
systems. Their properties are often described with MTL (?), a temporal logic
that extends LTL with metric time. We first summarize timed automata and MTL,
and then define the problem of controlling a TA against an MTL specification,
following (?; ?).

##### MTL

MTL extends LTL with timing constraints on the _Until_ modality. One commonly
used semantics for MTL is a _pointwise semantics_ , in which formulas are
interpreted over timed words.

######  Definition 15 (Timed Words).

A timed word $\rho$ over a finite set of atomic propositions $P$ is a finite
or infinite sequence
$\left(\sigma_{0},\tau_{0}\right)\left(\sigma_{1},\tau_{1}\right)\ldots$ where
$\sigma_{i}\subseteq P$ and $\tau_{i}\in\mathbb{Q}_{+}$ such that the sequence
$(\tau_{i})$ is monotonically non-decreasing and non-Zeno. The set of timed
words over $P$ is denoted as $TP^{*}$.

For a timed word
$\rho=\left(\sigma_{0},t_{0}\right)\left(\sigma_{1},t_{1}\right)\ldots$ and
every $k\in\mathbb{N}$ with $k\leq|\rho|$, we also write $\rho_{k}$ for the
prefix $\left(\sigma_{0},t_{0}\right)\ldots\left(\sigma_{k},t_{k}\right)$.

######  Definition 16 (Formulas of MTL).

Given a set $P$ of atomic propositions, the formulas of MTL are built as
follows:

$\phi::=p\>\mid\>\neg\phi\>\mid\>\phi\wedge\phi\>\mid\>\phi\,\mathbf{U}_{I}\,\phi$

We use the same abbreviations as for
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$, i.e., $\mathbf{F}_{I}\phi\overset{def}{=}(\top\,\mathbf{U}_{I}\,\phi)$
(_future_) and $\mathbf{G}_{I}\phi\overset{def}{=}\neg\mathbf{F}_{I}\neg\phi$
(_globally_). As in
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$, we may omit the interval $I$ if $I=[0,\infty)$. For a given set of atomic
propositions $P$, we denote the language of MTL formulas over $P$ as
$\mathcal{L}_{\text{MTL}}(P)$.

######  Definition 17 (Pointwise semantics of MTL).

Given a timed word
$\rho=\left(\sigma_{0},\tau_{0}\right)\left(\sigma_{1},\tau_{1}\right)\ldots$
over alphabet $P$ and an MTL formula $\phi$, $\rho,i\models\phi$ is defined as
follows:

  1. 1.

$\rho,i\models p$ iff $p\in\sigma_{i}$

  2. 2.

$\rho,i\models\neg\phi$ iff $\rho,i\not\models\phi$

  3. 3.

$\rho,i\models\phi_{1}\wedge\phi_{2}$ iff $\rho_{i}\models\phi_{1}$ and
$\rho_{i}\models\phi_{2}$

  4. 4.

$\rho,i\models\phi_{1}\,\mathbf{U}_{I}\,\phi_{2}$ iff there exists $j$ such
that

    1. (a)

$i<j<|\rho|$,

    2. (b)

$\rho,j\models\phi_{2}$,

    3. (c)

$\tau_{j}-\tau_{i}\in I$,

    4. (d)

and $\rho,k\models\phi_{1}$ for all $k$ with $i<k<j$.

For an MTL formula $\phi$, we also write $\rho\models\phi$ for
$\rho,0\models\phi$ and we define the language of $\phi$ as
$L(\phi)=\\{\rho\mid\rho\models\phi\\}$.

##### Alternative definition of MTL

A commonly used alternative definition of MTL, especially in the context of
timed automata, requires the symbols in timed words to be from $P$ instead of
$2^{P}$, i.e., for a timed word
$\rho=\left(\sigma_{0},\tau_{0}\right)\left(\sigma_{1},\tau_{1}\right)\ldots$
over P, we require $\sigma_{i}\in P$ (instead of $\sigma_{i}\subseteq P$).
Also, truth of an atomic formula $p$ is defined as:

  1. 1’.

$\rho,i\models p$ iff $\sigma_{i}=p$.

Intuitively, a timed automaton describes a transition system with actions
leading from one state to the other, where formulas describe the occurrence of
actions, e.g., $\mathbf{G}[a_{1}\supset\mathbf{F}a_{2}]$ says that whenever
action $a_{1}$ occurs, $a_{2}$ will occur afterwards eventually. Here, the set
of atomic propositions $P$ is the set of possible actions. At most one action
may occur at any point in time. Thus, each $\sigma_{i}\in P$ defines the
action that occurs at time $\tau_{i}$.

In our context, formulas describe states of the world, e.g.,
$\mathit{RAt}(m_{1})\wedge\mathit{Holding}(o_{1})$ says that the robot is at
$m_{1}$ and currently holding $o_{1}$. Here, the set of atomic propositions is
the set of primitive formulas describing possible world states and multiple
predicates may be true at the same time. Thus, each $\sigma_{i}\subseteq P$
describes the primitive formulas that are true at time $\tau_{i}$.

Let MTL$\in$ and denote MTL with the alternative semantics and $\models_{\in}$
satisfiability in MTL$\in$. We can define mappings between MTL and MTL$\in$.
The mapping
$\cdot^{*}:\mathcal{L}_{\text{MTL}}(P)\rightarrow\mathcal{L}_{\text{MTL}_{\in}}(2^{P})$
maps a formula of MTL into MTL$\in$, where:

$\displaystyle p^{*}$ $\displaystyle=\bigvee_{\\{Q\subseteq P\mid p\in Q\\}}Q$
$\displaystyle\left(\neg\phi\right)^{*}$ $\displaystyle=\neg\phi^{*}$
$\displaystyle\left(\phi\wedge\psi\right)^{*}$
$\displaystyle=\phi^{*}\wedge\psi^{*}$
$\displaystyle\left(\phi\,\mathbf{U}_{I}\,\psi\right)^{*}$
$\displaystyle=\phi^{*}\,\mathbf{U}_{I}\,\psi^{*}$

Note that if $\phi$ is a formula over $P$, then $\phi^{*}$ is a formula over
$2^{P}$, i.e., the atomic propositions in $\phi^{*}$ are sub-sets of $P$. As
an example, for $P=\\{a,b,c\\}$: $\left(a\wedge
b\right)^{*}=\left(\left\\{a\right\\}\vee\left\\{a,b\right\\}\vee\left\\{a,b,c\right\\}\vee\left\\{a,c\right\\}\right)\wedge\left(\left\\{b\right\\}\vee\left\\{a,b\right\\}\vee\left\\{a,b,c\right\\}\vee\left\\{b,c\right\\}\right)$.

The mapping
$\cdot^{+}:\mathcal{L}_{\text{MTL}_{\in}}(P)\rightarrow\mathcal{L}_{\text{MTL}}(P)$
maps a formula of MTL$\in$ into MTL by enforcing that each $\sigma_{i}$
contains exactly one symbol from $P$:

$\phi^{+}=\phi\wedge\mathbf{G}\bigvee_{p\in P}\left(p\wedge\bigwedge_{q\in
P\setminus\\{p\\}}\neg q\right)$

######  Theorem 2.

For every $\phi\in\mathcal{L}_{\text{MTL}}(P)$ and
$\psi\in\mathcal{L}_{\text{MTL}_{\in}}(P)$:

$\displaystyle{\models}\phi$
$\displaystyle\Leftrightarrow{\models_{\in}}\phi^{*}$
$\displaystyle{\models}\psi^{+}$
$\displaystyle\Leftrightarrow{\models_{\in}}\psi$

In the following, we will use the semantics from Definition 17. However,
related work on MTL synthesis uses the other formalism. In particular, Theorem
4 uses the the alternative MTL semantics from above. With Theorem 2, we can
apply those results while using the semantics from Definition 17.

#####  MTL and $\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace
S\negthinspace G}$

Timed words in MTL are similar to traces in
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$. In fact, $\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace
S\negthinspace G}$ subsumes MTL:

######  Theorem 3 (? (?)).

Let $\phi$ be a sentence of MTL. Then
$\models_{\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace
S\negthinspace G}{}}\phi$ iff $\models_{\text{MTL}}\phi$.

##### Symbolic transition systems and timed automata

Intuitively, a timed automaton is a finite automaton extended with time. More
specifically, a timed automaton has a finite set of clocks; time may pass in
the vertices of the graph, which are also called _locations_. Transitions,
also called switches, are the edges of the graph. They are always
instantaneous, may have clock constraints, and may reset some clocks to zero.
Formally, we first define symbolic transition systems (STSs):

######  Definition 18 (Symbolic Transition Systems and Timed Automata (?)).

Let $X$ be a finite set of variables (called _clocks_). The set
$\mathcal{G}(X)$ of _clock constraints_ $g$ over $X$ is defined by the grammar
$g::=g\wedge g\mid x\bowtie c$, where
$\mathord{\bowtie}\in\\{<,\leq,=,\geq,>\\}$, $x\in X$, and
$c\in\mathbb{Q}_{\geq 0}$. A _valuation_ over $X$ is a mapping
$\nu:X\rightarrow\mathbb{R}_{\geq 0}$. The set of valuations satisfying a
constraint $g$ is denoted as $\llbracket g\rrbracket$. A granularity is
defined by a triple $\mu=\left(X,m,K\right)$, where $X$ is a finite set of
clocks, $m\in\mathbb{N}_{>0}$, and $K\in\mathbb{N}$. A constraint $g$ is
$\mu$-granular if it only uses clocks from $X$ and each constant in $g$ is
$\frac{\alpha}{m}$ with $\alpha\leq K$ and $\alpha\in\mathbb{N}$.

For alphabet $P$ and clocks $X$, a _symbolic alphabet_ $\Gamma$ is a finite
subset of $2^{P}\times\mathcal{G}(X)\times 2^{X}$, where a symbolic action
$\left(p,g,Y\right)\in\Gamma$ is interpreted as action $p$ can happen if the
constraint $g$ is satisfied, with the clocks in $Y$ being reset after the
action. A symbolic word
$\gamma=\left(a_{1},g_{1},Y_{1}\right)\left(a_{2},g_{,}Y_{2}\right)\ldots$
over $\Gamma$ gives rise to a set of timed words $\mathit{tw}(\gamma)$ over
$P$.

A _ symbolic transition system (STS)_ over a symbolic alphabet $\Gamma$ based
on $\left(P,X\right)$ is a tuple
$\mathcal{T}=\left(S,s_{0},\rightarrow,F\right)$, where $S$ is a possibly
infinite set of states, $s_{0}\in S$ is the initial state,
$\mathnormal{\rightarrow}\subseteq S\times\Gamma\times S$ is the transition
relation, and $F\subseteq S$ is a set of accepting state. The _timed language_
accepted by an STS $\mathcal{T}$ is denoted as $L(\mathcal{T})$.

A STS is called _deterministic_ if there are no distinct transitions
$q\overset{a,g_{1},Y_{1}}{\longrightarrow}q_{1}$ and
$q\overset{a,g_{2},Y_{2}}{\longrightarrow}q_{2}$ with $\llbracket
g_{1}\rrbracket\cap\llbracket g_{2}\rrbracket\neq\emptyset$.

A _ timed automaton (TA)_ is an STS with finitely many states.

We also want to compose STSs:

######  Definition 19 (STS Compositions).

For two STS $\mathcal{T}_{1}=\langle
Q_{1},q_{0}^{1},\rightarrow_{1},F_{1}\rangle$ over $\Gamma_{1}$ based on
$\left(P_{1},X_{1}\right)$ and $\mathcal{T}_{2}=\langle
Q_{2},q_{0}^{2},\rightarrow_{2},F_{2}\rangle$ over $\Gamma_{2}$ based on
$\left(P_{2},X_{2}\right)$, the _parallel composition_
$\mathcal{T}_{1}\parallel\mathcal{T}_{2}$ of $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$ is the STS $\langle Q,q_{0},\rightarrow,F\rangle$ where
$Q=Q_{1}\times Q_{2}$, $q_{0}=\left(q_{0}^{1},q_{0}^{2}\right)$,
$F=F_{1}\times F_{2}$ and
$\left(p_{1},p_{2}\right)\overset{a,g,Y}{\longrightarrow}\left(q_{1},q_{2}\right)$
iff $p_{1}\overset{a,g_{1},Y_{1}}{\longrightarrow}q_{1}$ and
$p_{2}\overset{a,g_{2},Y_{2}}{\longrightarrow}q_{2}$ with $g=g_{1}\wedge
g_{2}$ and $Y=Y_{1}\cup Y_{2}$.

If $P_{1}\cap P_{2}=\emptyset$, then the _product STS_
$\mathcal{T}_{1}\times\mathcal{T}_{2}$ is the STS $\langle
Q,q_{0},\rightarrow,F\rangle$ where $Q=Q_{1}\times Q_{2}$,
$q_{0}=\left(q_{0}^{1},q_{0}^{2}\right)$, $F=F_{1}\times F_{2}$ and
$\left(p_{1},p_{2}\right)\overset{a,g,Y}{\longrightarrow}\left(q_{1},q_{2}\right)$
iff $p_{1}\overset{a_{1},g_{1},Y_{1}}{\longrightarrow}q_{1}$,
$p_{2}\overset{a_{2},g_{2},Y_{2}}{\longrightarrow}q_{2}$, and $a=a_{1}\cup
a_{2}$, $g=g_{1}\wedge g_{2}$, and $Y=Y_{1}\cup Y_{2}$.

In the parallel composition $\mathcal{T}_{1}\parallel\mathcal{T}_{2}$, both
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ take a transition for the same input
simultaneously. The product $\mathcal{T}_{1}\times\mathcal{T}_{2}$ takes a
transition on a symbol $a$ if $a$ is the union $a=a_{1}\cup a_{2}$ of two
input symbols $a_{1}$ and $a_{2}$, such that $\mathcal{T}_{1}$
($\mathcal{T}_{2}$) can take a transition on $a_{1}$ ($a_{2}$).

#####  MTL Control Problem

Finally, we define the MTL control problem. Intuitively, the goal is to
synthesize a controller $\mathcal{C}$ that _controls_ a _plant_ $\mathcal{P}$
against a specification of desired behaviors $\Phi$ such that all resulting
traces satisfy the specification $\Phi$ without blocking the plant
$\mathcal{P}$. In this context, _control_ means that $\mathcal{C}$ has control
over some actions, while the environment controls the remaining actions.
Formally:

######  Definition 20 (MTL Control Problem (?)).

Let $P=P_{C}\cup P_{E}$ be an alphabet partitioned into a set of
_controllable_ actions $P_{C}$ and a set of _environment_ actions $P_{E}$. A
_plant_ $\mathcal{P}$ over $P$ is a deterministic TA. Let the clocks used in
$\mathcal{P}$ be $X_{\mathcal{P}}$ and $\mu=\left(X_{\mathcal{P}}\cup
X_{\mathcal{C}},m,K\right)$ be a granularity finer than that of the plant.
Then, a $\mu$-controller for $\mathcal{P}$ is a deterministic STS
$\mathcal{C}$ over a symbolic alphabet based on $\left(P,X_{\mathcal{P}}\cup
X_{\mathcal{C}}\right)$ having granularity $\mu$ and satisfying:

  1. 1.

$\mathcal{C}$ does not reset the clocks of the plant:
$q_{\mathcal{C}}\overset{a,g,Y}{\longrightarrow}q^{\prime}_{\mathcal{C}}$
implies $Y\subset X_{\mathcal{C}}$,

  2. 2.

$\mathcal{C}$ does not restrict environment actions: if $\sigma\in
L(\mathcal{P}\parallel\mathcal{C})$ and $\sigma\left(e,t\right)\in
L(\mathcal{P})$ with $e\in P_{E}$, then $\sigma\cdot\left(e,t\right)\in
L(\mathcal{P}\parallel\mathcal{C})$

  3. 3.

$\mathcal{C}$ is non-blocking: if $\sigma\in
L(\mathcal{P}\parallel\mathcal{C})$ and $\sigma\left(a,t\right)\in
L(\mathcal{P})$ and $\sigma\cdot\left(a,t\right)\in L(\mathcal{P})$, then
$\sigma\cdot\left(b,t^{\prime}\right)\in\mathcal{L}^{*}(\mathcal{P}\parallel\mathcal{C})$
for some $b\in P$ and $t^{\prime}\in\mathbb{Q}$

  4. 4.

all states of $\mathcal{C}$ are accepting.

For a timed language $\mathcal{L}\subseteq TP^{*}$, we say that a
$\mu$-controller $\mathcal{C}$ _controls_ $\mathcal{P}$ against the
specification of desired behaviors $\Phi$ iff
$L(\mathcal{P}\parallel\mathcal{C})\subseteq L(\Phi)$. The control problem
with fixed resources against desired behaviors is to decide, given a plant
$\mathcal{P}$, a set of formulas $\Phi$, and a granularity $\mu$ finer than
that of $\mathcal{P}$, whether there exists a $\mu$-controller $\mathcal{C}$
which controls $\mathcal{P}$ against the specification of desired behaviors
$\Phi$.

? showed that the synthesis problem is decidable, with some restrictions:

######  Theorem 4 (? (?)).

The control problem for fixed resources against MTL specifications over finite
words representing desired behaviors is decidable. Moreover, if there exists a
controller, then one can effectively construct a finite-state one.

We will use this result by constructing a TA $\mathit{PTA}(\Sigma,\delta)$
from a determinate fd-BAT $\Sigma$ and program $\delta$, modelling the
platform as another TA $\mathcal{R}$, and synthesizing a controller
$\mathcal{C}$ that controls the TA
$\mathcal{T}=\mathit{PTA}(\Sigma,\delta)\times\mathcal{R}$ against the
platform constraints $\Phi$.

##  5 Constructing a TA from a Program

We describe how to construct a TA from a program $\delta$ over a determinate
fd-BAT $\Sigma$. We do this by using $P=\mathcal{P}_{\Sigma}\cup A_{\Sigma}$
as alphabet for the TA $\mathit{PTA}(\Sigma,\delta)$, i.e., the alphabet $P$
consists of all primitive formulas and action standard names from $\Sigma$. In
each transition, we encode the occurring action and the resulting situation,
such that $p\overset{\sigma,\emptyset,\emptyset}{\rightarrow}q$ for
$\sigma=\\{f_{1},\ldots,f_{k},a\\}$ if after doing action
$a\in\mathcal{A}_{\Sigma}$ in the corresponding situation, exactly the
primitive formulas $\\{f_{1},\ldots,f_{k}\\}\subseteq\mathcal{P}_{\Sigma}$ are
true. By doing so, we obtain a correspondence of traces of the program
$\delta$ with traces in the TA.

We assume that $\Sigma$ is a determinate finite-domain basic action theory and
$\delta$ is a program over $\Sigma$. We need to restrict $\Sigma$ to be a
determinate BAT as in the resulting timed automaton, each transition encodes
which primitive formulas are true in the respective situation. In particular,
the transition $q_{0}\rightarrow S_{0}$ will encode the primitive formulas
that are true in the initial situation. As we cannot encode disjunctions in
such a transition, we need $\Sigma_{0}$ to determine the truth for each
primitive formula $f_{i}$. Also, as each transition can only contain finitely
many symbols, $\Sigma$ needs to be restricted to a finite domain. Furthermore,
we assume that $\delta$ is terminating, i.e., it only induces finite traces,
which is necessary to guarantee that the resulting transition system indeed
has a finite number of states. We will further discuss those restrictions in
Section 8.

$q_{0}$$S_{0}$$\begin{Bmatrix}\mathit{RAt}(m_{1})\\\
\mathit{At}(o_{1},m_{2})\end{Bmatrix}$ $\begin{Bmatrix}\mathit{RAt}(m_{1})\\\
\mathit{At}(o_{1},m_{2})\end{Bmatrix}$
$S_{1}$$\begin{Bmatrix}\mathit{At}(o_{1},m_{2})]\\\
\mathit{Perf}(\mathit{goto}(m_{1},m_{2}))\end{Bmatrix}$
$\begin{Bmatrix}\mathit{At}(o_{1},m_{2})\\\
\mathit{Perf}(\mathit{goto}(m_{1},m_{2}))\\\
\mathit{s\\_goto}(m_{1},m_{2})\end{Bmatrix}$
$S_{2}$$\begin{Bmatrix}\mathit{RAt}(m_{1})\\\
\mathit{At}(o_{1},m_{2})\end{Bmatrix}$ $\begin{Bmatrix}\mathit{RAt}(m_{2})\\\
\mathit{At}(o_{1},m_{2})\\\ \mathit{e\\_goto}(m_{1},m_{2})\end{Bmatrix}$
$S_{3}$$\begin{Bmatrix}\mathit{RAt}(m_{2})\\\
\mathit{Perf}(\mathit{pick}(o_{1}))\end{Bmatrix}$
$\begin{Bmatrix}\mathit{RAt}(m_{2})\\\ \mathit{Perf}(\mathit{pick}(o_{1}))\\\
\mathit{s\\_pick}(o_{1})\end{Bmatrix}$
$S_{4}$$\begin{Bmatrix}\mathit{RAt}(m_{2})\\\
\mathit{Holding}(o_{1})\end{Bmatrix}$ $\begin{Bmatrix}\mathit{RAt}(m_{2})\\\
\mathit{Holding}(o_{1})\\\ \mathit{e\\_pick}(o_{1})\end{Bmatrix}$ Figure 1:
The TA for the program from 1 and the initial situation from Equation 9. The
dashed edges are controlled by the environment.

######  Definition 21 (Program Timed Automata).

Given a program $\delta$ over a determinate fd-BAT $\Sigma$. We define the
timed automaton
$\mathit{PTA}(\Sigma,\delta)=\left(S,q_{0},\rightarrow,F\right)$ as follows:

  1. 1.

$q_{0}\overset{P,\emptyset,\emptyset}{\longrightarrow}\left(\langle\rangle,\delta\right)$
with $P=\\{f_{i}\in\mathcal{P}_{\Sigma}\mid
w_{\Sigma}[f_{i},\langle\rangle]=1\\}$

  2. 2.

$\left(z,\delta\right)\overset{P\cup\\{a\\},\emptyset,\emptyset}{\longrightarrow}\left(z\cdot
a,\delta^{\prime}\right)$ iff
$\left(z^{0},\delta\right)\overset{w_{\Sigma}}{\rightarrow}\left(\left(z\cdot
a\right)^{0},\delta^{\prime}\right)$ and
$P=\\{f_{i}\in\mathcal{P}_{\Sigma}\mid w_{\Sigma}[f_{i},\left(z\cdot
a\right)^{0}]=1\\}$

  3. 3.

$\left(z,\delta\right)\overset{P,\emptyset,\emptyset}{\longrightarrow}\left(z,\delta\right)$
with $P=\\{f_{i}\in\mathcal{P}_{\Sigma}\mid w_{\Sigma}[f_{i},z]=1\\}$

  4. 4.

$\left(z,\delta\right)\in F$ iff $\langle
z^{0},\delta\rangle\in\mathcal{F}^{w_{\Sigma}}$

A word $\rho$ of the TA $\mathit{PTA}(\Sigma,\delta)$ corresponds to a trace
$\tau\in\|\delta\|_{w_{\Sigma}}$. We can map $\rho$ to $\tau$:

######  Definition 22 (Induced action trace).

Given a word $\rho\in\mathit{PTA}(\Sigma,\delta)$, we define the _(action)
trace $\mu(\rho)$ induced by $\rho$_ inductively:

  * •

If $\rho=\langle\rangle$, then $\mu(\rho)=\langle\rangle$

  * •

If $\rho=\left(\\{\ldots,a_{i}\\},t_{i}\right)\cdot\rho^{\prime}$ for some
action standard name $a_{i}\in A_{\Sigma}$, then
$\mu(\rho)=\left(a_{i},t_{i}\right)\cdot\mu(\rho^{\prime})$

  * •

Otherwise, if $\rho=\left(\sigma_{i},t_{i}\right)\cdot\rho^{\prime}$ and
$\sigma_{i}\cap A_{\Sigma}=\emptyset$ (i.e., $\sigma_{i}$ contains no action
from $\Sigma$), then $\mu(\rho)=\mu(\rho^{\prime})$

The trace $\mu(\rho)$ induced by an MTL word
$\rho\in\mathit{PTA}(\Sigma,\delta)$ is indeed a trace of the program:

######  Lemma 3.

Given a program $\delta$ over a determinate fd-BAT $\Sigma$. Then:

  1. 1.

For every $\rho\in L(\mathit{PTA}(\Sigma,\delta))$:
$\mu(\rho)\in\|\delta\|_{w_{\Sigma}}$.

  2. 2.

For every $\tau\in\|\delta\|_{w_{\Sigma}}$, there is a $\rho\in
L(\mathit{PTA}(\Sigma,\delta))$ such that $\mu(\rho)=\tau$.

###### Proof.

Follows directly from the construction of $\mathit{PTA}(\Sigma,\delta)$ and
Proposition 1. ∎

Furthermore, we can show that the MTL word $\rho$ and the trace $\mu(\rho)$
entail the same fluent state formulas at every point in time:

######  Theorem 5.

Given a program $\delta$ over a determinate fd-BAT $\Sigma$. Then:

  1. 1.

For every $\rho\in L(\mathit{PTA}(\Sigma,\delta))$ and every $k\leq|\rho|$,
there is a $\tau=z\cdot\tau^{\prime}\in\|\delta\|_{w_{\Sigma}}$ such that
$\mu(\rho_{k})=z$ and

$w_{\Sigma},z\models\alpha\Leftrightarrow\rho_{k}\models\alpha$

  2. 2.

For every $\tau\in\|\delta\|_{w_{\Sigma}}$ and every $z$ with
$\tau=z\cdot\tau^{\prime}$, there is a $\rho\in
L(\mathit{PTA}(\Sigma,\delta))$ such that for some $i\leq|\rho|$,
$\mu(\rho_{k})=z$ and

$w_{\Sigma},z\models\alpha\Leftrightarrow\rho_{k}\models\alpha$

###### Proof.

  1. 1.

Let $\rho\in L(\mathit{PTA}(\Sigma,\delta))$. By Lemma 3, we know that
$\tau\left(\rho\right)\in\|\delta\|_{w_{\Sigma}}$. It remains to be shown that
for every $k\leq|\rho|$, there is a $z,\tau^{\prime}$ such that
$\tau=z\cdot\tau^{\prime}$ and $\mu(\rho_{k})=z$. We show the existence of
$z,\tau^{\prime}$ by induction over $k$:

    1. (a)

Let $k=0$. Thus $\rho_{k}=\left(\sigma_{0},t_{0}\right)$. By definition of
$\mathit{PTA}(\Sigma,\delta)$, we know that $\sigma_{0}=\Sigma_{0}$. For
$z=\langle\rangle$, it follows that $\mu(\rho_{k})=z$ and
$w_{\Sigma},z\models\alpha\Leftrightarrow
w_{\Sigma}\models\alpha\Leftrightarrow\Sigma_{0}\models\alpha\Leftrightarrow\rho^{\prime}\models\alpha$.

    2. (b)

Let $k=l+1$. By induction, there is a $z^{\prime}$ such that
$\tau=z^{\prime}\cdot\tau^{\prime}$, $z^{\prime}=\mu(\rho_{l})$, and
$w_{\Sigma},z^{\prime}\models\alpha\Leftrightarrow\rho_{l}\models\alpha$. Now,
we have two cases:

      1. i.

There is some action symbol $a\in\sigma_{k}$. Then, by definition of
$\mathit{PTA}(\Sigma,\delta)$, for $z=z^{\prime}\cdot\left(a,t_{k}\right)$,
$w_{\Sigma},z\models\alpha\Leftrightarrow\rho_{k}\models\alpha$.

      2. ii.

There is no action symbol in $\sigma_{k}$. Then, by definition of
$\mathit{PTA}(\Sigma,\delta)$, $\sigma_{k}=\\{f_{i}\mid
w_{\Sigma}[f_{i},z^{\prime}]=1\\}$ and thus, for $z=z^{\prime}$, it follows
that $w_{\Sigma},z\models\alpha\Leftrightarrow\rho_{k}\models\alpha$.

  2. 2.

Let $\tau\in\|\delta\|_{w_{\Sigma}}$. By Lemma 3, we know that there is a
$\rho\in L(\mathit{PTA}(\Sigma,\delta))$. It remains to be shown that for
every $z$ with $\tau=z\cdot\tau^{\prime}$, $\mu(\rho_{k})=z$ and
$w_{\Sigma},z\models\alpha\Leftrightarrow\rho_{k}\models\alpha$. By induction
over the length $i$ of $z$:

    1. (a)

Let $i=0$, i.e., $z=\langle\rangle$, and thus $w_{\Sigma},z\models\alpha$ iff
$\Sigma_{0}\models\alpha$. By definition of $\mathit{PTA}(\Sigma,\delta)$,
$\rho_{0}=\left(\Sigma_{0},t_{0}\right)$ for some $t_{0}$. Thus,
$\mu(\rho_{0})=\langle\rangle$ and $\rho_{0}\models\alpha$ iff
$\Sigma_{0}\models\alpha$.

    2. (b)

Let $i=j+1$, i.e., $z=z^{\prime}\cdot\left(a_{i},t_{i}\right)$. By induction,
$z^{\prime}=\mu(\rho_{l})$ for some $l$ and
$w_{\Sigma},z^{\prime}\models\alpha\Leftrightarrow\rho_{l}\models\alpha$. By
definition of $\mathit{PTA}(\Sigma,\delta)$:

$\rho=\overbrace{\underbrace{\left(\sigma_{0},t_{0}\right)\ldots\left(\sigma_{l},t_{l}\right)}_{\rho_{l}}\left(\sigma_{l+1},t_{l+1}\right)\ldots(\underbrace{\\{\ldots,a_{i}\\}}_{\sigma_{k}},t_{k}\\})}^{\rho_{k}}$

where none of $\sigma_{l+1},\ldots,\sigma_{k-1}$ contains any action symbol.
Then, by definition of $\mathit{PTA}(\Sigma,\delta)$, $\sigma_{k}=\\{f\mid
w_{\Sigma}[f,z]=1\\}$, and thus
$w_{\Sigma},z\models\alpha\Leftrightarrow\rho_{k}\models\alpha$.

∎

##  6 Platform Models

$\mathit{Init}$$\\{\mathit{Ready}\\}$$\mathit{Calibrating}$$\\{\mathit{Calibrating}\\}$$\mathit{Calibrated}$$\\{\mathit{Calibrated}\\}$
$\begin{Bmatrix}\mathit{Calibrating}\\\ \mathit{s\\_calibrate}\end{Bmatrix}$
$t_{p}:=0$ $\begin{Bmatrix}\mathit{Calibrated}\\\
\mathit{e\\_calibrate}\end{Bmatrix}$ $t_{p}=5$
$\begin{Bmatrix}\mathit{Calibrating}\\\ \mathit{s\\_calibrate}\end{Bmatrix}$
$t_{p}:=0$ Figure 2: The platform model of a robot arm.

We model the robot platform with timed automata, an example is shown in Figure
2. Similar to PTAs, we expect a platform model to use an alphabet with symbols
of the form $\\{f_{1},\ldots f_{k},a\\}$, where $a\in\mathcal{N}_{A}\setminus
A_{\Sigma}$ is a platform action and
$f_{i}\in\mathcal{P}_{F}\setminus\mathcal{P}_{\Sigma}$ are exactly those
primitive formulas that are true after executing the action. We expect $f_{i}$
and $a$ to be from a different alphabet than the BAT, i.e., the platform does
not have any effects on the abstract program and vice versa. Further, to
guarantee that the platform model does not block the PTA, we expect it to
contain self loops, similar to the self loops of a PTA, and as shown in Figure
2.

##### Platform Constraints

Given a determinate fd-BAT $\Sigma$ and a platform model $\mathcal{R}$, we can
formulate constraints over $\Sigma$ and $\mathcal{R}$:

$\displaystyle\mathbf{G}\neg\mathit{Calibrated}\supset\neg\mathbf{F}_{\leq
10}\exists p\mathbf{:}o.\,\mathit{Perf}(\mathit{pick}(p))$ (10)
$\displaystyle\mathbf{G}\mathit{Calibrating}\supset\exists
l\mathbf{:}o.\,\mathit{RAt}(l)\wedge\mathit{Spacious}(l)$ (11)

The first constraint states that if the robot’s arm is not calibrated, it must
not perform a pick action in the next 10 seconds, i.e., it must calibrate the
arm before doing pick. The second constraint says that if the robot is
calibrating its arm, it must be at a location that provides enough space for
doing so, i.e., a $\mathit{Spacious}$ location.

##  7 Synthesizing a Controller

$\begin{Bmatrix}\mathit{RAt}(m_{1})\\\ \mathit{At}(o_{1},m_{2})\\\
\mathit{Calibrating}\\\ \mathit{s\\_calibrate}\end{Bmatrix}$
$\begin{Bmatrix}\mathit{RAt}(m_{1})\\\ \mathit{At}(o_{1},m_{2})\\\
\mathit{Calibrated}\\\ \mathit{e\\_calibrate}\end{Bmatrix}$ $t_{c}:=0$
$\begin{Bmatrix}\mathit{At}(o_{1},m_{2})\\\ \mathit{s\\_goto}(m_{1},m_{2})\\\
\mathit{Calibrated}\end{Bmatrix}$ $\begin{Bmatrix}\mathit{RAt}(m_{2})\\\
\mathit{At}(o_{1},m_{2})\\\ \mathit{e\\_goto}(m_{1},m_{2})\\\
\mathit{Calibrated}\end{Bmatrix}$ * $\begin{Bmatrix}\mathit{RAt}(m_{2})\\\
\mathit{At}(o_{1},m_{2})\\\ \mathit{Perf}(\mathit{pick}(o_{1}))\\\
\mathit{s\\_pick}(o_{1})\\\ \mathit{Calibrated}\end{Bmatrix}$ $t_{c}>10$
Figure 3: A possible controller that controls the program from Figure 1 and
the platform from Figure 2 against the constraints from Equations 10 and 11.
The dashed edges are controlled by the environment.

Using the TA $\mathit{PTA}(\Sigma,\delta)$ that represents the program
$\delta$, the TA $\mathcal{R}$ for the platform, and constraints $\Phi$, we
can use MTL synthesis to synthesize a controller that executes $\delta$ while
satisfying the platform constraints. Specifically, we use

  1. 1.

the plant $\mathcal{P}=\mathit{PTA}(\Sigma,\delta)\times\mathcal{R}$,

  2. 2.

as controllable actions $P_{C}$ all symbols that contain start actions of the
program or the platform model, i.e., $P_{C}=\\{S\mid S\in
P,\mathit{s\\_a}(\vec{t})\in S\text{ for some }a(\vec{t})\\}$,

  3. 3.

as environment actions $P_{E}$ all symbols that contain end actions of the
program or the platform model, i.e., $P_{E}=\\{E\mid E\in
P,\mathit{e\\_a}(\vec{t})\in E\\}$ for some $a(\vec{t})$,

  4. 4.

a fixed granularity $\mu$, e.g., based on the robot platform’s time resolution

  5. 5.

the set of MTL formulas $\Phi$ as specification of desired behaviors.

Figure 3 shows a possible controller for our example program from 1, the
platform from Figure 2, and the constraints from Section 6.

We can show that  (1) the resulting controller indeed satisfies the
constraints and  (2) each of its traces is equivalent to some trace of the
original program, i.e., the resulting controller satisfies the same situation
formulas as the original program at any point of the execution:

######  Theorem 6.

Let $\Sigma$ be a determinate fd-BAT, $\delta$ a program over $\Sigma$ that
only induces finite traces, $\mathcal{R}$ a platform model with symbols
disjunct with the symbols from $\Sigma$, and let the constraints $\Phi$ be a
set of MTL formulas. Let $\mathcal{C}$ be the synthesized MTL controller with
$\mathcal{L}=L\left(\left(\mathit{PTA}(\Sigma,\delta)\times\mathcal{R}\right)\parallel\mathcal{C}\right)$.
Then:

  1. 1.

$\mathcal{L}\subseteq L(\Phi)$, i.e., all constraints are satisfied.

  2. 2.

For every $\rho=\rho^{\prime}\cdot\rho^{\prime\prime}\in\mathcal{L}$,
$\mu(\rho)\in\|\delta\|_{w_{\Sigma}}$, and for every fluent state formula
restricted to $\Sigma$:

$\rho^{\prime}\models\alpha\Leftrightarrow
w_{\Sigma},\mu(\rho^{\prime})\models\alpha$

###### Proof.

  1. 1.

Follows directly from Theorem 4.

  2. 2.

First, note that $\mathcal{L}\subseteq
L(\mathit{PTA}(\Sigma,\delta)\times\mathcal{R})$. Second, as $\mathcal{R}$
does not contain any action standard name from $\Sigma$, for every
$\rho\in\mathcal{L}$, there is a $\rho^{\prime}\in\mathit{PTA}(\Sigma,\delta)$
such that $\mu(\rho)=\mu(\rho^{\prime})$. By Theorem 5, for every
$\rho^{\prime}\in\mathit{PTA}(\Sigma,\delta)$,
$\mu(\rho^{\prime})\in\|\delta\|_{w_{\Sigma}}$ and
$\rho^{\prime}\models\alpha$ iff $w_{\Sigma},\mu(\rho^{\prime})\models\alpha$.
∎

Thus, the resulting controller preserves the program’s original effects while
satisfying all platform constraints.

##  8 Conclusion

In this paper, we have described how to synthesize a controller that controls
a Golog program over a finite domain against a robot platform with metric
temporal constraints. We did so by reducing the problem to the MTL synthesis
problem, assuming that the initial state is completely known, the original
program does not refer to time and only induces finite traces. For this
reduction, we generated a timed automaton (TA) from the initial situation
$\Sigma_{0}$, the program $\delta$ and the platform model $\mathcal{R}$, where
each transition describes all the fluents that are true in the respective
situation. We then synthesized an MTL controller that controls the generated
TA against a set of MTL constraints $\Phi$. By doing so, we obtain a decidable
procedure to control an abstract program against a platform model with metric
temporal constraints.

For future work, we plan to implement the proposed synthesis method based on
(?).

While the restriction to a finite domain is fundamental for the described
synthesis method, in future work, we may want to allow programs that allow
infinite traces. This is possible if we restrict the constraints to Safety MTL
but requires modifications to the TA representation of the program, as the
resulting TA must not have infinitely many states. Furthermore, we may want to
allow programs that refer to time, e.g., by defining equivalence classes of
traces that may refer to different points in time but imply the same situation
formulas. Lastly, it would be interesting to go beyond determinate BATs to
allow some form of incompleteness, for example, by considering sets of
literals under the open world assumption (?).

## References

  * Allen 1983 Allen, J. F.  1983\.  Maintaining Knowledge about Temporal Intervals.  Communications of the ACM 26(11):832–843.

  * Alur and Dill 1994 Alur, R., and Dill, D. L.  1994\.  A theory of timed automata.  Theoretical Computer Science 126(2):183–235.
  * Alur and Henzinger 1993 Alur, R., and Henzinger, T.  1993\.  Real-Time Logics: Complexity and Expressiveness.  Information and Computation 104(1):35–77.
  * Alur 1999 Alur, R.  1999\.  Timed Automata.  In Computer Aided Verification, 8–22.  Springer.
  * Bouyer, Bozzelli, and Chevalier 2006 Bouyer, P.; Bozzelli, L.; and Chevalier, F.  2006\.  Controller Synthesis for MTL Specifications.  In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR), 450–464.  Springer Berlin Heidelberg.
  * Claßen and Lakemeyer 2008 Claßen, J., and Lakemeyer, G.  2008\.  A Logic for Non-Terminating Golog Programs.  In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR), 589–599.
  * Claßen 2013 Claßen, J.  2013\.  Planning and Verification in the Agent Language Golog.  Ph.D. Dissertation, RWTH Aachen University.
  * De Giacomo and Vardi 2015 De Giacomo, G., and Vardi, M. Y.  2015\.  Synthesis for LTL and LDL on Finite Traces.  In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI), 1558–1564.  AAAI Press.
  * De Giacomo et al. 2009 De Giacomo, G.; Lespérance, Y.; Levesque, H. J.; and Sardina, S.  2009\.  IndiGolog: A high-level programming language for embedded reasoning agents.  In Multi-Agent Programming. Springer.
  * De Giacomo, Lespérance, and Levesque 2000 De Giacomo, G.; Lespérance, Y.; and Levesque, H. J.  2000\.  ConGolog, a concurrent programming language based on the situation calculus.  Artificial Intelligence 121\.
  * Finzi and Pirri 2005 Finzi, A., and Pirri, F.  2005\.  Representing flexible temporal behaviors in the situation calculus.  In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), 436–441.
  * He et al. 2017 He, K.; Lahijanian, M.; Kavraki, L. E.; and Vardi, M. Y.  2017\.  Reactive synthesis for finite tasks under resource constraints.  In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 5326–5332.
  * Hofmann and Lakemeyer 2018 Hofmann, T., and Lakemeyer, G.  2018\.  A logic for specifying metric temporal constraints for Golog programs.  In Proceedings of the 11th Cognitive Robotics Workshop 2018 (CogRob).
  * Hofmann et al. 2018 Hofmann, T.; Mataré, V.; Schiffer, S.; Ferrein, A.; and Lakemeyer, G.  2018\.  Constraint-based online transformation of abstract plans into executable robot actions.  In AAAI Spring Symposium: Integrating Representation, Reasoning, Learning, and Execution for Goal Directed Autonomy.
  * Koymans 1990 Koymans, R.  1990\.  Specifying real-time properties with metric temporal logic.  Real-Time Systems 2(4):255–299.
  * Lakemeyer and Levesque 2011 Lakemeyer, G., and Levesque, H. J.  2011\.  A semantic characterization of a useful fragment of the situation calculus with knowledge.  Artificial Intelligence 175(1):142–164.
  * Levesque et al. 1997 Levesque, H. J.; Reiter, R.; Lesperance, Y.; Lin, F.; and Scherl, R. B.  1997\.  GOLOG: A logic programming language for dynamic domains.  Journal of Logic Programming 31(1-3).
  * Levesque 1998 Levesque, H. J.  1998\.  A completeness result for reasoning with incomplete first-order knowledge bases.  In Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning, 14–23.  Morgan Kaufmann Publishers Inc.
  * McCarthy 1963 McCarthy, J.  1963\.  Situations, actions, and causal laws.  Technical report, Stanford University.
  * Ouaknine and Worrell 2005 Ouaknine, J., and Worrell, J.  2005\.  On the decidability of metric temporal logic.  In 20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05), 188–197.
  * Ouaknine and Worrell 2008 Ouaknine, J., and Worrell, J.  2008\.  Some recent results in metric temporal logic.  Lecture Notes in Computer Science 5215 LNCS:1–13.
  * Reiter 2001 Reiter, R.  2001\.  Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems.  MIT Press.
  * Schiffer, Wortmann, and Lakemeyer 2010 Schiffer, S.; Wortmann, A.; and Lakemeyer, G.  2010\.  Self-Maintenance for Autonomous Robots controlled by ReadyLog.  In Proceedings of the 7th IARP Workshop on Technical Challenges for Dependable Robots.

  *[TA]: timed automaton
  *[MTL]: Metric Temporal Logic
  *[LTL]: Linear Time Logic
  *[BAT]: basic action theory
  *[fd-BAT]: finite-domain basic action theory
  *[STSs]: symbolic transition system
  *[STS]: symbolic transition system
  *[ STS]: symbolic transition system
  *[BATs]: basic action theory