proofs

# Controlling Golog Programs against MTL Constraints

Till Hofmann1 Stefan Schupp2
1Knowledge-Based Systems Group, RWTH Aachen University, Aachen, Germany
2Cyber-Physical Systems Group, TU Wien, Vienna, Austria
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### 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.

##  1 Introduction

While Golog is an expressive language to describe high-level robot behavior,
it is often tedious to use on real-world robots, as it is challenging to
manage all the low-level details of the system (?; ?). A real-world platform
often poses implicit requirements that must be considered while developing a
robot program. As an example, consider a simple robot that is able to pick up
objects. From a high-level perspective, it is easy to model this, e.g.,
$\mathit{grasp}$ changes the location of the object and requires that the
robot is at the same location as the object. However, on an actual robot, much
more is involved, e.g., before doing $\mathit{grasp}$, the robot’s camera must
have been enabled long enough so the object detection was able to find the
object. Encoding these low-level details quickly results in a bloated robot
program that is difficult to maintain. Furthermore, it requires the awareness
of the developer of low-level details, as the robot’s actions may otherwise
have unexpected consequences, e.g., the robot breaking the object.

In this paper, we propose to make these implicit requirements explicit. by
modelling them as constraints in Metric Temporal Logic (MTL), a temporal logic
that allows timing constraints. Rather than having a single detailed program,
we propose that the high-level program is augmented with a _maintenance
program_ , which takes care of the low-level details and is executed
concurrently. This allows the developer to focus on the high-level behavior
while ensuring that all constraints are satisfied.

Executing such an augmented program poses a _synthesis problem_ : a controller
needs to decide which actions to execute and when to execute them. In this
paper, we investigate this synthesis problem. Given a high-level Golog program
and an MTL specification of undesired behavior, the task is to select those
actions that  (i) are possible successors according to the Golog program,
(ii) ensure that the program eventually terminates, and  (iii) satisfy the
specification.  To solve this synthesis problem, we take inspiration from
_timed automata controller synthesis_ (?), where a timed automaton is
controlled against an MTL specification. We present the following
contributions:  (i) the logic
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$, which extends Golog with clocks and clock constraints to express timing
constraints,  (ii) a theoretical framework for controller synthesis on Golog
programs given an MTL specification,  (iii) and decidability results of the
controller synthesis problem for Golog programs on finite domains.

We start in Section 2 by describing the background and related work, before we
introduce the logic
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$ in Section 3. We summarize results on MTL decidability in Section 4,
define the controller synthesis problem in Section 5 and then describe our
approach in Section 6. We conclude in Section 7.

##  2 Background and Related Work

The situation calculus (?; ?) is a logical formalism for reasoning about
dynamical domains based on first-order logic. World states are represened
explicitly as first-order terms called _situations_ , where _fluents_ describe
(possibly changing) properties of the world and actions are axiomatized in
basic action theorys (BATs). Golog (?; ?) is a programming language based on
the situation calculus that allows to control the high-level behavior of
robots. $\mathcal{E\negthinspace S}$ (?) is a modal variant and epistemic
extension of the situation calculus, where situations are part of the
semantics but do not appear as terms in the language. $\mathcal{E\negthinspace
S\negthinspace G}$ (?) extends $\mathcal{E\negthinspace S}$ with a transition
semantics for Golog programs and temporal formulas to verify the correctness
of Golog programs (?).

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_ , consisting of
sequences of symbol-time pairs. Depending on the choice of the state and time
theory, the satisfiability problem for MTL becomes undecidable (?). However,
for finite words with pointwise semantics, it has been shown to be decidable
(?; ?). We build on top of this result and describe it in more detail in
Section 4.1.

A timed automaton (TA) (?) is an automaton equipped with a finite set of
clocks, whose real-timed values increase uniformly, and where a transition may
reset clocks and have a guard on the clock value. ? (?) describe a synthesis
method where the goal is to reach a certain set of (timed) goal states of a
TA, which can be seen as an _internal_ winning condition. ? (?) synthesize a
timed controller against an _external_ specification, where the undesired
behavior is given as a TA, assuming _fixed resources_ , i.e., a fixed number
of clocks and a fixed resolution in timing constraints. They do so by defining
a _timed game_ , where a winning strategy corresponds to a control strategy,
and then reducing the timed game to a classical game. In a similar fashion, ?
(?) describe a timed game to determine a controller for a TA against an MTL
specification. Our method to find a controller for a Golog program is inspired
by these techniques.

Similar to the proposed approach, ? (?) extend Golog for self-maintenance by
allowing temporal constraints using Allen’s Interval Algebra (?). Related is
also the work by ? (?), who propose a hybrid approach of temporal constraint
reasoning and reasoning about actions based on the situation calculus. Based
on $\mathit{LTL}_{f}$ synthesis (?), ? (?) describe a synthesis method that
controls a robot against uncontrollable environment actions under resource
constraints. In contrast to this work, they do not allow metric temporal
constraints. ? (?) augment a fixed action sequence (e.g., a plan) with
maintenance actions to satisfy a temporal specification with timing
constraints. In contrast to our work, they do not allow Golog programs, and
they use a restricted constraint language. ? (?) convert a Golog program to a
TA, which allows to use MTL controller synthesis to solve the synthesis
problem. Rather than constructing a TA, we synthesize a controller based on a
symbolic execution of the program.

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

We start by describing
$\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace S\negthinspace
G}$, a logic that allows the specification of Golog programs with timing
constraints. It builds on top of $\mathcal{E\negthinspace S\negthinspace G}$
and $\mathcal{E\negthinspace S}$, which in turn are modal variants of the
situation calculus. In contrast to an earlier version of the logic (?), we do
not allow arbitrary expressions referring to time, as this directly leads to
undecidability, even in finite contexts. Instead, inspired by timed automata,
we introduce clocks and we only allow comparisons to clock values as well as
clock resets.

The language has three sorts: _object_ , _action_ , and _clock_. A special
feature inherited from $\mathcal{E\negthinspace S}$ is the use of countably
infinite sets of _standard names_ for those sorts. Standard object and clock
names syntactically look like constants, but are intended to be isomorphic
with the set of all objects (clocks) of the domain. In other words, standard
object (clock) 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 as a subsort. Action standard names are
function symbols of any arity whose arguments are standard object names, e.g.,
$\mathit{grasp}(o)$ for picking up an object. 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.

###  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.

variables of sort object $x_{1},x_{2},\ldots$, action $a,a_{1},a_{2},\ldots$,
and clock $c,c_{1},c_{2},\ldots$,

  2. 2.

standard names of sort object $\mathcal{N}_{O}=\\{o_{1},o_{2},\ldots\\}$,
action $\mathcal{N}_{A}=\\{p_{1},p_{2},\ldots\\}$, and clock
$\mathcal{N}_{C}=\\{q_{1},q_{2},\ldots\\}$,

  3. 3.

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
predicates $\operatorname{Poss}$, $\operatorname{reset}$, and
$\operatorname{g}$, and

  4. 4.

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

######  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 of the corresponding
sort.

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

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

  1. 1.

if $t_{1},\ldots,t_{k}$ are object or action 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 object or action terms, then $(t_{1}=t_{2})$ is a
situation formula,

  3. 3.

if $c$ is a clock term and $r\in\mathbb{N}$111With a finite set of rational
constants used for comparison in constraints, these can be scaled to integer
values., then $c\bowtie r$ is a clock formula, where
$\operatorname{\bowtie}\in\\{<,\leq,=,\geq,>\\}$,

  4. 4.

if $\alpha,\beta$ are clock formulas, then $\square\alpha$ and
$\alpha\wedge\beta$ are clock formulas, and

  5. 5.

if $\alpha$ and $\beta$ are situation formulas, $x$ is a variable, and
$\delta$ is a program expression (defined below), then $\alpha\wedge\beta$,
$\neg\alpha$, $\forall x.\,\alpha$, $\square\alpha$, and $[\delta]\alpha$ are
situation 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$”, and $c<r$ as “the value of clock c is less than r” (analogously for
$\leq,=,\geq,>$).

A situation formula is called static if it contains no $[\cdot]$ or $\square$
operators and fluent if it is static and does not mention
$\operatorname{Poss}$.

Finally, we define the syntax of Golog program expresions referred to by the
operator $[\delta]$:

######  Definition 4 (Program Expressions).

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

where $t$ is an action term and $\alpha$ is a static situation formula. A
program expression consists of actions $t$, tests $\alpha?$, sequences
$\delta_{1};\delta_{2}$, nondeterministic222We leave out the pick operator
$\pi x.\,\delta$, as we later restrict the domain to be finite, where pick can
be expressed with nondeterministic branching. branching
$\delta_{1}|\delta_{2}$, interleaved concurrency $\delta_{1}\|\delta_{2}$, and
nondeterministic iteration $\delta^{*}$.

We also use the abbreviation $\mathit{nil}:=\top?$ for the empty program that
always succeeds.

###  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{N}_{A}\times\mathbb{R}_{\geq 0}$, and for
every $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
$\operatorname{time}(z):=t_{k}$ for $k>0$ and
$\operatorname{time}(\langle\rangle):=0$.

######  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}]$. The set of
all worlds is denoted by $\mathcal{W}$.

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 will allow us to
specify MTL constraints on program execution traces.

To allow the program to keep track of time, we introduce _clocks_ , similarly
to clocks in timed automata. At each point of the program execution, each
clock needs to have a value, which is determined by the _clock valuation_ :

######  Definition 7 (Clock Valuation).

A clock valuation over a finite set of clocks $C$ is a mapping
$\nu:C\rightarrow\mathbb{R}_{\geq 0}$.

We denote the set of all clock valuations over $C$ as $\operatorname{N}_{C}$.
The clock valuation $\vec{0}$ denotes the clock valuation $\nu$ with
$\nu(c)=0$ for all $c\in C$. For every
$\operatorname{\bowtie}\in\\{<,\leq,=,\geq,>\\}$, we write
$\nu\bowtie\nu^{\prime}$ if $\nu(c)\bowtie\nu^{\prime}(c)$ for all $c\in C$.

We continue by define the transitions that a program may take in a given world
$w$. The program transition semantics is based on $\mathcal{E\negthinspace
S\negthinspace G}$ (?) and extended by time and clocks. Here, a program
configuration is a tuple $(z,\nu,\rho)$ consisting of a timed trace $z$, a
clock valuation $\nu$, and the remaining program $\rho$. A program may take a
transition
$(z,\nu,\rho)\xrightarrow{w}(z^{\prime},\nu^{\prime},\rho^{\prime})$ if it can
take a single action that results in the new configuration. In three places,
these refer to the truth of clock and situation formulas (see Definition 10
below).

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

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

  1. 1.

$\langle z,\nu,a\rangle\xrightarrow{w}\langle
z^{\prime},\nu^{\prime},\mathit{nil}\rangle$, if $z^{\prime}=z\cdot(a,t)$ and
if there is $d\geq 0$ such that

    1. (a)

$t=\operatorname{time}(z)+d$,

    2. (b)

$w,z\models\operatorname{Poss}(a)$,

    3. (c)

$w,z,\nu+d\models\operatorname{g}(a)$, and

    4. (d)

$\nu^{\prime}(c)=\begin{cases}0&\text{ if
}w,z^{\prime}\models\operatorname{reset}(c)\\\ \nu(c)+d&\text{ otherwise
}\end{cases}$

  2. 2.

$\langle z,\nu,\delta_{1};\delta_{2}\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\gamma;\delta_{2}\rangle$
if $\langle z,\nu,\delta_{1}\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\gamma\rangle$,

  3. 3.

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

  4. 4.

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

  5. 5.

$\langle z,\nu,\delta^{*}\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\gamma;\delta^{*}\rangle$ if $\langle
z,\nu,\delta\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\gamma\rangle$,

  6. 6.

$\langle z,\nu,\delta_{1}\|\delta_{2}\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\delta^{\prime}\|\delta_{2}\rangle$
if $\langle z,\nu,\delta_{1}\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\delta^{\prime}\rangle$, and

  7. 7.

$\langle z,\nu,\delta_{1}\|\delta_{2}\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\delta_{1}\|\delta^{\prime}\rangle$
if $\langle z,\nu,\delta_{2}\rangle\xrightarrow{w}\langle z\cdot
p,\nu^{\prime},\delta^{\prime}\rangle$.

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

  1. 1.

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

  2. 2.

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

  3. 3.

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

  4. 4.

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

  5. 5.

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

Intuitively, the program may take a single transition step (Definition 8.1) if
the action is possible to execute and if there is some time increment such
that all clock constraints are satisfied. In the resulting configuration, the
program trace is appended with the new action $a$ and the incremented time
$t$, all clock values are either incremented by the time increment, or reset
if $a$ resets the clock. Also, a program is final if there is no remaining
action and if any test $\alpha?$ is successful.

By following the transitions, we obtain _program traces_ :

######  Definition 9 (Program Traces).

Given a world $w$, a finite trace $z$, and a clock valuation $\nu$, the
_program traces_ of a program expression $\delta$ are defined as follows:

$\displaystyle\operatorname{Succ}_{w}(z,\nu,\delta)$
$\displaystyle=\\{(z^{\prime},\nu^{\prime},\delta^{\prime})\mid\langle
z,\nu,\delta\rangle\xrightarrow{w}\langle
z^{\prime},\nu^{\prime},\delta^{\prime}\rangle\\}$
$\displaystyle\operatorname{Succ}_{w}^{*}(z,\nu,\delta)$
$\displaystyle=\\{(z^{\prime},\nu^{\prime},\delta^{\prime})\mid\langle
z,\nu,\delta\rangle\xrightarrow{w}^{*}\langle
z^{\prime},\nu^{\prime},\delta^{\prime}\rangle\\}$
$\displaystyle\operatorname{Succ}_{w}^{f}(z,\nu,\delta)$
$\displaystyle=\\{(z^{\prime},\nu^{\prime},\delta^{\prime})\mid\langle
z,\nu,\delta\rangle\xrightarrow{w}^{*}\langle
z^{\prime},\nu^{\prime},\delta^{\prime}\rangle$ $\displaystyle\qquad\text{ and
}\langle z^{\prime},\nu^{\prime},\delta^{\prime}\rangle\in\mathcal{F}^{w}\\}$
$\displaystyle\|\delta\|^{z,\nu}_{w}$ $\displaystyle=\\{z^{\prime}\mid(z\cdot
z^{\prime},\nu^{\prime},\delta^{\prime})\in\operatorname{Succ}_{w}^{f}(z,\nu,\delta)\\}$

Intuitively, $\operatorname{Succ}_{w}(z,\nu,\delta)$ describes the direct
successor configurations of a given configuration, while
$\operatorname{Succ}^{*}_{w}(z,\nu,\delta)$ denotes all reachable
configurations from the current configuration, and
$\operatorname{Succ}^{f}_{w}(z,\nu,\delta)$ denotes those sequences ending in
a final configuration. We use $\|\delta\|^{z,\nu}_{w}$ to denote only the
timed traces resulting in a final configuration. We also omit $z$ if
$z=\langle\rangle$ and $\nu$ if $\nu=\vec{0}$. In contrast to
$\mathcal{E\negthinspace S\negthinspace G}$, we are only interested in finite
traces, as MTL is undecidable over infinite traces (?).

Using the program transition semantics, we can now define the truth of a
formula:

######  Definition 10 (Truth of Formulas).

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

  1. 1.

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

  2. 2.

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

  3. 3.

$w,z,\nu\models c\bowtie r$ iff $\nu(c)\bowtie r$,

  4. 4.

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

  5. 5.

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

  6. 6.

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

  7. 7.

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

  8. 8.

$w,z,\nu\models[\delta]\alpha$ iff for all
$(z^{\prime},\nu^{\prime})\in\|\delta\|^{z}_{w}$, $w,z\cdot
z^{\prime},\nu^{\prime}\models\alpha$.

Intuitively, $\square\alpha$ means that in every possible state, $\alpha$ is
true, and $[\delta]\alpha$ means that _after every execution_ of $\delta$,
$\alpha$ is true.

###  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 finite set of clocks
$C$, and 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},C)$ iff
$\Sigma=\Sigma_{0}\cup\Sigma_{\text{pre}}\cup\Sigma_{g}\cup\Sigma_{\text{post}}$,
where $\Sigma$ mentions only fluents in $\mathcal{F}$, clocks in $C$, 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\operatorname{Poss}(a)\equiv\bigvee_{o}\\{\pi_{o}\\}$, with one fluent
formula $\pi_{o}$ with free variable333Free variables are implicitly universal
quantified from the outside. The modality $\Box$ has lower syntactic
precedence than the connectives, and $[\cdot]$ has the highest priority. $a$
for each action type $o$,

  3. 3.

$\Sigma_{g}$ is a set of sentences, one for each action $a$, of the form
$\square\operatorname{g}(a)\,\equiv\;g_{a}$, where $g_{a}$ is a clock formula
over $C$, and

  4. 4.

$\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}$, where $\gamma_{F}$ is a fluent
sentence, and

     * •

one for each clock $c\in C$, of the form
$\square[a]\operatorname{reset}(c)\,\equiv\;\gamma_{c}$, where $\gamma_{c}$ is
a fluent sentence.

The set $\Sigma_{0}$ describes the initial state, $\Sigma_{\text{pre}}$
defines the action preconditions, and $\Sigma_{\text{post}}$ defines action
effects by specifying for each fluent and clock of the domain whether the
fluent is true after doing some action $a$ and whether the respective clock is
reset to zero. The sentences in $\Sigma_{\text{g}}$ use clock formulas to
describe the clock constraints of each action $a$.

We can now define _programs_ :

######  Definition 12 (Program).

A program is a pair $\Delta=(\Sigma,\delta)$ consisting of a BAT $\Sigma$ and
a program expression $\delta$.

We will later refer to the reachable subprograms of some program $\delta$:

######  Definition 13 (Reachable Subprograms).

Given a program $(\Sigma,\delta)$, we define the _reachable subprograms
$\operatorname{sub}(\delta)$ of $\delta$_:

$\operatorname{sub}(\delta)=\\{\delta^{\prime}\>\mid\>\exists
w\models\Sigma,z\in\mathcal{Z}\text{ such that
}\langle\langle\rangle,\delta\rangle\xrightarrow{w}^{*}\langle
z,\delta^{\prime}\rangle\\}$

######  Example 1 (BATs).

We consider a system of a robot that can pick up (_grasp_) an object $o$, with
the following preconditions:

$\displaystyle\Sigma_{\text{pre}}^{\mathit{hi}}=\\{$ $\displaystyle\exists
o,l.\ a=\mathit{start}\\_{\mathit{grasp}(o,l)}$ (1)
$\displaystyle\land\mathit{obj\\_at}(o,l)\land\neg\mathit{grasping}(o)\land\neg\mathit{holding}(o),$
$\displaystyle\exists o,l.\
a=\mathit{end}\\_{\mathit{grasp}(o,l)}\land\mathit{grasping}(o)\\}.$ (2)

To grasp an object $o$ at location $l$, the object needs to be at that
location and the robot cannot already be grasping nor holding the object (1).
Grasping can only end when the robot is currently grasping (2). Here we assume
that the high-level BAT does not specify any operations on clocks, i.e.,
$\Sigma_{g}=\emptyset$. The effects of actions on fluent predicates are
specified by

$\displaystyle\Sigma_{\text{post}}^{\mathit{hi}}=$
$\displaystyle\square[a]\mathit{grasping}(o)\,\equiv\;\exists l.\
a=\mathit{start}\\_{\mathit{grasp}(o,l)}$ (3)
$\displaystyle\lor\mathit{grasping}(o)\land
a\neq\mathit{end}\\_{\mathit{grasp}(o,l)},$
$\displaystyle\square[a]\mathit{holding}(o)\,\equiv\;\exists l.\
a=\mathit{end}\\_{\mathit{grasp}(o,l)}$ (4)
$\displaystyle\lor\mathit{holding}(o)\land\not\exists l^{\prime},o^{\prime}.\
a=\mathit{start}\\_{\mathit{grasp}(o^{\prime},l^{\prime})},$
$\displaystyle\square[a]\mathit{obj\\_at}(o,l)\,\equiv\;\mathit{obj\\_at}(o,l)$
(5) $\displaystyle\land a\neq\mathit{start}\\_{\mathit{grasp}(o,l)}\\}.$

The effects on the fluent predicates are detailed in Equation 3 to Equation 5,
e.g., $\mathit{holding}(o)$ (Equation 4) is satisfied at the end of a grasping
action of an object $o$, or if the robot is currently holding $o$ and does not
start to grasp again. The initial situation, i.e, the initial satisfaction of
the fluent predicates is described by

$\displaystyle\Sigma_{0}^{\mathit{hi}}=\\{$
$\displaystyle\mathit{obj\\_at}(o,l),\neg\mathit{holding}(o),\neg\mathit{grasping}(o)\\}.$

The correct operation of the gripper requires a camera-module to be
operational before starting to grasp for an object. These low-level operations
are reflected by a secondary BAT over a clock set $C=\\{c\\}$ as follows:

$\displaystyle\Sigma_{\text{pre}}^{\mathit{lo}}=\\{$ $\displaystyle
a=\mathit{start}\\_{\mathit{cam}()}\land\neg\mathit{cam\\_on}(),$
$\displaystyle
a=\mathit{end}\\_{\mathit{cam}()}\land\mathit{cam\\_booting}()\\}.$

Enabling the camera takes one time unit, which is outlined by the constraint

$\displaystyle\Sigma_{g}^{\mathit{lo}}=\\{\square
g[\mathit{end}\\_{\mathit{cam}()]\,\equiv\;c=1}\\}.$

The low-level BAT specifies the following effects of actions:

$\displaystyle\Sigma_{\text{post}}^{\mathit{lo}}=\\{$
$\displaystyle\square[a]\mathit{cam\\_on}()\,\equiv\;a=\mathit{end}\\_{\mathit{cam}()},$
$\displaystyle\square[a]\mathit{cam\\_booting}()\,\equiv\;a=\mathit{start}\\_{\mathit{cam}()}$
$\displaystyle\lor\mathit{cam\\_booting}()\land
a\neq\mathit{end}\\_{\mathit{cam}()},$
$\displaystyle\square[a]\mathit{reset(c)}\,\equiv\;a=\mathit{start}\\_{\mathit{cam}()}\\}.$

Initially,
$\Sigma_{0}^{\mathit{lo}}=\\{\neg\mathit{cam\\_on}(),\neg\mathit{cam\\_booting}()\\}$
holds for the low-level components.

###  3.4 Finite-Domain BATs

As we allow quantification over the infinite set of standard names, a BAT may
generally describe infinite domains and thus also infinitely many fluents.
However, as we later want to specify MTL constraints on the fluents entailed
by some program configuration and MTL requires a finite alphabet, we need to
restrict the BAT to a finite domain. We do this by requiring a restriction on
the quantifiers used in $\Sigma$:

######  Definition 14 (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$_. We denote the set of primitive formulas
restricted to $\Sigma$ as $\mathcal{P}_{\Sigma}$, the action standard names
mentioned in $\Sigma$ as $A_{\Sigma}$, and the clock standard names mentioned
in $\Sigma$ as $C_{\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, where $\exists
x\mathbf{:}\tau_{o}.\phi:=\bigvee_{i=1}^{k}\phi^{x}_{n_{i}}$, $\forall
x\mathbf{:}\tau_{o}.\phi:=\bigwedge_{i=1}^{k}\phi^{x}_{n_{i}}$, and similarly
for action-quantifiers.

We can now define an equivalence relation between worlds, where two worlds are
equivalent if they initially satisfy the same fluents:

######  Definition 15 ($\Sigma_{0}$-equivalent Worlds).

We define the equivalence relation $\equiv_{\Sigma_{0}}$ of worlds wrt
$\Sigma$ such that $w\equiv_{\Sigma_{0}}w^{\prime}$ iff
$w[f,\langle\rangle]=w^{\prime}[f,\langle\rangle]$ for all
$f\in\mathcal{P}_{\Sigma}$.

We use $[w]$ to denote the equivalence class
$[w]=\\{w^{\prime}\in\mathcal{W}\mid w\equiv_{\Sigma_{0}}w^{\prime}\\}$.

As a fd-BAT only refers to finitely many fluents, it also only has finitely
many equivalence classes:

######  Lemma 1.

444Proofs are available in the appendix.

For a fd-BAT $\Sigma$, $\equiv_{\Sigma_{0}}$ has finitely many equivalence
classes.

Furthermore, for each equivalence class, we only need to consider one world:

######  Theorem 1.

Let $\Sigma$ be a fd-BAT and $w,w^{\prime}$ be two worlds with
$w\models\Sigma$, $w^{\prime}\models\Sigma$, and
$w\equiv_{\Sigma_{0}}w^{\prime}$. Then, for every formula $\alpha$ restricted
to $\Sigma$:

$w\models\alpha\text{ iff }w^{\prime}\models\alpha.$

proofs

###### Proof of Theorem 1.

∎

This is an adaption of Lemma 3 from (?). We first show that for any $w$, there
exists a world $w_{\Sigma}$ that is the same as $w$, but satisfies
$\Sigma_{\text{pre}}\cup\Sigma_{g}\cup\Sigma_{\text{post}}$. We define
$w_{\Sigma}$ as the world that satisfies the following conditions:

  1. 1.

For $F\not\in\mathcal{F}$ and for every $z\in\mathcal{Z}$,
$w_{\Sigma}[F(\vec{n}),z]=w[F(\vec{x}),z]$

  2. 2.

For $F\in\mathcal{F}$, $w_{\Sigma}[F(\vec{n}),z]$ is defined inductively:

    1. (a)

$w_{\Sigma}[F(\vec{n}),\langle\rangle]=w[F(\vec{n}),\langle\rangle]$,

    2. (b)

$w_{\Sigma}[F(\vec{n}),z\cdot m]=1$ iff
$w_{\Sigma},z\models(\gamma_{F})^{av_{1}\cdots v_{k}}_{mn_{1}\cdots n_{k}}$,

  3. 3.

$w_{\Sigma}[\operatorname{Poss}(n),z]=1$ iff
$w_{\Sigma},z\models(\pi_{n})^{a}_{n}$.

The argumentation is the same as in (?): $w_{\Sigma}$ clearly exists. The
uniqueness follows from the fact that $\pi$ is a fluent formula and that for
all fluents in $\mathcal{F}$, once their initial values are fixed, then the
values after any number of actions are uniquely determined by
$\Sigma_{\text{post}}$. Note that in particular, $\pi$ and
$\Sigma_{\text{post}}$ may not mention clocks. Therefore, fluent values do not
depend on time.

Now, as each $w_{\Sigma}$ is unique, $w$ and $w^{\prime}$ agree on the fluents
in $\Sigma_{0}$, and $\alpha$ only mentions fluents from $\Sigma$, it follows
that $w,z\models\alpha$ iff $w^{\prime},z\models\alpha$.

Thus, for the sake of simplicity, for a given $\Sigma$, we assume in the
following that we have a single world $w$ with $w\models\Sigma$. To extend
this to fd-BATs, we can apply the proposed method for a world from each
equivalence class.

##  4 Metric Temporal Logic (MTL)

While Section 3 described how we can model Golog programs with BATs, we now
describe how we specify temporal constraints with MTL. MTL (?) extends LTL
with timing constraints on the _Until_ modality, therefore allowing temporal
constraints with interval restrictions, e.g., $\mathbf{F}_{\leq 2}b$ to say
that within the next two timesteps, a $b$ event most occur. One commonly used
semantics for MTL is a _pointwise semantics_ , in which formulas are
interpreted over timed words. We summarize MTL and its pointwise semantics
following the notation by (?). Timed words in MTL are similar to timed traces
in $\operatorname{\mathit{t-}}\negthinspace\mathcal{E\negthinspace
S\negthinspace G}$:

######  Definition 16 (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{R}_{\geq 0}$ such that the
sequence $(\tau_{i})$ is monotonically non-decreasing and non-Zeno. The set of
timed words over $P$ is denoted as $\mathit{TP}^{*}$.

In contrast to the usual definition, we expect each symbol $\sigma_{i}$ to be
a subset (rather than a single element) of the alphabet $P$. We do this
because we later want to define constraints over sets of fluents $F_{i}$ that
are satisfied in some program state.

MTL formulas are constructed as follows:

######  Definition 17 (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$

As an example, the formula
$\mathit{cam\\_on}\,\mathbf{U}_{[1,2]}\,\mathit{grasping}(o)$ says that the
object $o$ must be grasped in the interval $[1,2]$ and until then, the camera
must be on.

We use the abbreviations $\mathbf{F}_{I}\phi:=(\top\,\mathbf{U}_{I}\,\phi)$
(_finally_) and $\mathbf{G}_{I}\phi:=\neg\mathbf{F}_{I}\neg\phi$ (_globally_).

######  Definition 18 (Pointwise Semantics of MTL).

Given a timed word $\rho=\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}$, and

  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
$\mathcal{L}(\phi)=\\{\rho\mid\rho\models\phi\\}$.

Note that we use strict-until, i.e., we require that $i<j$ rather than $i\leq
j$. However, weak-until can be expressed with strict-until
($\phi\textbf{U}_{I}^{\text{weak}}\psi:=\psi\vee\phi\,\mathbf{U}_{I}\,\psi)$,
while strict-until cannot be expressed with weak-until (?).

###  4.1 Alternating Timed Automata

Alternating timed automata (alternating timed automata) (?) are a commonly
used method to decide whether a timed word $\rho$ satisfies an MTL formula
$\phi$. We summarize the construction of an ATA $\mathcal{A}{{}_{\phi}}$ which
accepts a word $\rho$ iff the word satisfies formula $\phi$, i.e., iff
$\rho\in\mathcal{L}(\phi)$. We refer to ? (?) for the full construction.

######  Definition 19.

Let $L$ be a finite set of locations. The set of formulas $\Phi(L)$ is
generated by the following grammar:

$\varphi::=\top\>\mid\>\bot\>\mid\>\varphi_{1}\wedge\varphi_{2}\>\mid\>\varphi_{1}\vee\varphi_{2}\>\mid\>l\>\mid\>x\bowtie
k\>\mid\>x.\varphi$

where $k\in\mathbb{N}$, $\operatorname{\bowtie}\in\\{<,\leq,=,\geq,>\\}$, and
$l\in L$.

######  Definition 20 (ATA).

An alternating timed automaton (ATA) is a tuple
$\mathcal{A}{}=\left(\Sigma_{\mathcal{A}{}},L,l_{0},F,\delta\right)$, where
$\Sigma_{\mathcal{A}{}}$is a finite alphabet,  $L$is a finite set of
locations,  $F\subseteq L$is a set of accepting locations, and
$\delta:L\times\Sigma_{\mathcal{A}{}}\rightarrow\Phi(L)$is the transition
function.

An ATA has an implicit single clock $x$. A state of $\mathcal{A}{}$ is a pair
$(l,v)$, where $l\in L$ is the location and $v\in\mathbb{R}_{\geq 0}$ is a
_clock valuation_ of the clock $x$. We denote the set of all possible states
with $Q$. Given a set of states $M\subseteq Q$ and a clock valuation
$v\in\mathbb{R}_{\geq 0}$, the truth of a formula $\varphi\in\Phi(L)$ is
defined as follows:  (1) $(M,v)\models s$iff $s\in M$,  (2) $(M,v)\models
x\bowtie k$iff $v\bowtie k$,  (3) $(M,v)\models x.\varphi$iff
$(M,0)\models\varphi$.  The set of states $M$ is a _minimal model of
$\varphi$_ if $(M,v)\models\varphi$ and there is no proper subset $N\subset M$
with $(N,v)\models\varphi$. A _configuration_ of $\mathcal{A}{}$ is a finite
set of states. The initial configuration is $\\{(l_{0},0)\\}$. A configuration
$G$ is accepting if for all $(l,u)\in G$, $l\in F$.

The language accepted by an ATA is defined in terms of a transition system
$\mathcal{T}_{\mathcal{A}{}}=(2^{Q},\rightsquigarrow,\rightarrow)$ over sets
of configurations: The time-labeled transition relation
$\operatorname{\rightsquigarrow}\subseteq 2^{Q}\times\mathbb{R}_{\geq 0}\times
2^{Q}$ captures the progress of time in so-called _flow steps_ , where
$G\overset{t}{\rightsquigarrow}G^{\prime}$ if
$G^{\prime}=\\{(s,v+t)\mid(s,v)\in G\\}$. The $\Sigma_{\mathcal{A}{}}$-labeled
transition relation $\operatorname{\rightarrow}\subseteq
2^{Q}\times\Sigma_{\mathcal{A}{}}\times 2^{Q}$ describes _edge steps_ ,
instantaneous changes in the locations. With $G=\\{(s_{i},v_{i})\\}_{i\in I}$,
the transition $\rightarrow$ is defined such that
$G\overset{a}{\rightarrow}G^{\prime}$ if $G^{\prime}=\bigcup_{i\in I}M_{i}$,
where $(M_{i},v_{i})$ is some minimal model of $\delta(s_{i},a)$. For a
(finite) timed word $\rho=(\sigma_{0},\tau_{0}),\ldots,(\sigma_{k},\tau_{k})$,
the _run_ of $\mathcal{A}{}$ on $\rho$ is a sequence of alternating edge and
flow steps:

$G_{0}\overset{\sigma_{0}}{\rightarrow}G_{1}\overset{d_{0}}{\rightsquigarrow}G_{2}\ldots\overset{\sigma_{k}}{\rightarrow}G_{2k}\overset{d_{k}}{\rightsquigarrow}G_{2k+1}$

A finite timed word $\sigma$ is accepted by $\mathcal{A}{}$ if there is a run
of $\mathcal{A}{}$ over $\sigma$ leading to an accepting configuration. We
denote by $\mathcal{L}(\mathcal{A}{})$ the set of timed words accepted by
$\mathcal{A}{}$.

######  Theorem 2 ((?)).

Given an MTL formula $\phi$, one can build an ATA $\mathcal{A}{{}_{\phi}}$
with $\mathcal{L}(\phi)=\mathcal{L}(\mathcal{A}{{}_{\phi}})$.

We omit the construction, but instead provide an example:

######  Example 2 (ATA).

Given the MTL formula $\phi_{\mathit{bad}}=\top\,\mathbf{U}_{\leq
1}\,\neg\mathit{cam\\_on}\land\mathit{grasping}$,
$\mathcal{A}{{}_{\phi_{\mathit{bad}}}}$ looks as follows:

$\displaystyle\Sigma_{\mathcal{A}{}}$
$\displaystyle=2^{\\{\mathit{cam\\_on},\mathit{grasping}\\}}$ $\displaystyle
L$ $\displaystyle=\\{\phi_{\mathit{bad}}\\}$ $\displaystyle l_{0}$
$\displaystyle=\phi_{\mathit{bad}}$ $\displaystyle F$ $\displaystyle=\\{\\}$
$\displaystyle\delta$ $\displaystyle=\\{$
$\displaystyle(\phi_{\mathit{bad}},\\{\\})$
$\displaystyle=\phi_{\mathit{bad}},$
$\displaystyle(\phi_{\mathit{bad}},\\{\mathit{cam\\_on}\\})$
$\displaystyle=\phi_{\mathit{bad}},$
$\displaystyle(\phi_{\mathit{bad}},\\{\mathit{grasping}\\})$
$\displaystyle=x\leq 1\vee\phi_{\mathit{bad}},$
$\displaystyle(\phi_{\mathit{bad}},\\{\mathit{cam\\_on},\mathit{grasping}\\})$
$\displaystyle=\phi_{\mathit{bad}}\\}$

##  5 The Control Problem

With the goal to control a Golog program against an MTL specification such
that all execution traces satisfy the specification, we define what we mean by
a _controller_ , as well as what the _control problem_ is:

######  Definition 21 (Controller).

Given a program $\Delta=(\delta,\Sigma)$, a partition $A=A_{E}\dot{\cup}A_{C}$
of possible actions and an MTL formula $\phi$, a controller $\mathit{CR}$ is a
partial function that maps a configuration to a set of successor
configurations, i.e.,
$\mathit{CR}(z,\nu,\delta)=\\{(z_{i},\nu_{i},\delta_{i})_{i\in I}\\}$ such
that

  1. (C1)

For each $z_{i},\nu_{i},\delta_{i}$: $\langle
z,\nu,\delta\rangle\xrightarrow{w}\langle z_{i},\nu_{i},\delta_{i}\rangle$,

  2. (C2)

For each $a_{e}\in A_{E}$, if $\langle z,\delta\rangle\xrightarrow{w}\langle
z\cdot(a_{e},t),\delta^{\prime}\rangle$, then $\langle
z\cdot(a_{e},t),\delta^{\prime}\rangle\in\mathit{CR}(z,\delta)$, and

  3. (C3)

$\mathit{CR}(z,\delta)=\\{\\}$ implies $\langle
z,\delta\rangle\in\mathcal{F}^{w}$.

We demand that it is _non-blocking_ , i.e., it does not add deadlocks, and
only maps to valid successors (C1). Second, we require the controller to be
_non-restrictive_ (C2), i.e., it does not block the environment from executing
its actions and third, we state that the controller may only terminate if a
final configuration has been reached (C3).

If we execute a controller by following its transitions iteratively and
starting with the initial configuration $(\langle\rangle,\delta)$, we obtain a
set of traces $\mathcal{Z}_{\mathit{CR}}$. Formally,
$\mathcal{Z}_{\mathit{CR}}$ is the smallest set such that  (1) for each
$((a_{1},t_{1}),\nu_{1},\rho_{1})\in\mathit{CR}(\langle\rangle,\delta)$, there
is a $z=\langle(a_{1},t_{1}),\ldots\rangle\in\mathcal{Z}_{\mathit{CR}}$,  (2)
for each $z\in\mathcal{Z}_{\mathit{CR}}$ and for each prefix $z_{i}$ of $z$,
if there are $\nu_{i},\rho_{i}$ such that
$(z_{i+1},\nu_{i+1},\rho_{i+1})\in\mathit{CR}(z_{i},\nu_{i},\rho_{i})$, then
there is a $z^{*}$ such that $z_{i+1}\cdot z^{*}\in\mathcal{Z}_{\mathit{CR}}$.

In addition to action traces, we are also interested in the fluent traces
(i.e., the satisfied fluents after each step):

######  Definition 22 (Fluent Trace).

Given a world $w$ and a BAT $\Sigma$, the _fluent trace_ $\psi(z)$
corresponding to a timed trace $z$ is the sequence
$\psi(z)=\langle(F_{0},0),(F_{1},t_{1})\ldots,(F_{n},t_{n})\rangle$ where
$F_{i}=\\{f\in\mathcal{P}_{\Sigma}\mid w,z_{i}\models f\\}$ and
$t_{i}=\operatorname{time}(z_{i})$.

For each $z_{i}$, we also denote the last element $F_{i}$ of $\psi(z_{i})$
with $F(z_{i})$. Furthermore, we denote the set of all fluent traces induced
by the controller as $\Psi_{\mathit{CR}}=\\{\psi(z)\mid
z\in\mathcal{Z}_{\mathit{CR}}\\}$. We can now define the control problem:

######  Definition 23 (Control Problem).

Given a program $\Delta=(\delta,\Sigma)$ and an MTL formula $\phi$, the
control problem is to determine a controller $\mathit{CR}$ such that for each
$\psi\in\Psi_{\mathit{CR}}$: $\psi\models\phi$.

Intuitively, the problem is to determine a controller for the program $\Delta$
such that each execution satisfies the specification $\psi$, which is an MTL
formula over the fluents of $\Sigma$.

##  6 Approach

The goal of this work is to synthesize a controller which orchestrates actions
of a high-level program and a second, low-level program in such a way that a
task is successfully executed while complying with a given specification. In
our scenario, the idea is, among safety requirements, to express platform
requirements as constraints on the high-level program, which can be satisfied
by correct concurrent execution of high- and low-level actions.

Our approach consists of the following steps:  (1) we construct an ATA
$\mathcal{A}{{}_{\phi}}$ from the specification,  (2) we define a labeled
transition system $\mathcal{E}$ that symbolically executes the Golog program,
(3) we combine $\mathcal{A}{{}_{\phi}}$ and $\mathcal{E}$ to obtain a
synchronous product $\mathcal{S}$ (which may have uncountably many states),
(4) we regionalize $\mathcal{S}$ by applying regionalization to the clock
values to obtain $\mathcal{T}_{\sim}$ with countably many states,  (5) we
apply a powerset construction to obtain a deterministic $\mathcal{DT}_{\sim}$,
and  (6) we define a timed game on $\mathcal{DT}_{\sim}$ that results in a
decidable procedure to solve the synthesis problem.

To obtain a transition system of a program $\Delta$ we need to introduce
several notions. First of all, to describe sets of executions symbolically, we
define symbolic traces:

######  Definition 24 (Symbolic Alphabet and Symbolic Traces).

Given a program $\Delta=(\delta,\Sigma)$, the _symbolic alphabet_ of $\Delta$
is the set $\mathcal{V}_{\Delta}=A_{\Sigma}\times C_{\Sigma}\times
2^{C_{\Sigma}}$. A symbolic trace of $\Delta$ is a sequence
$s=(a_{1},g_{1},Y_{1})\ldots\in\mathcal{V}_{\Delta}^{*}$.

We denote the set of all symbolic traces of $\Delta$ with
$\mathcal{S}_{\Delta}$.

######  Definition 25 (Induced Timed Trace).

A symbolic trace
$s=(a_{1},g_{1},Y_{1})(a_{2},g_{2},Y_{2})\ldots\in\mathcal{S}_{\Delta}$
induces a set of timed traces $\operatorname{tw}(s)$ over
$A_{\Sigma}\times\mathbb{R}_{\geq 0}$, where $z\in\operatorname{tw}(s)$ iff
$|z|=|s|$, $z=(a_{1},t_{1})(a_{2},t_{2})\ldots$ and there is a sequence of
valuations $\nu_{0},\nu_{1},\ldots$ (compatible with $g_{1},\ldots$ and
$Y_{1},\ldots$) and programs $\rho_{i}\in\operatorname{sub}(\delta)$ such that
$\langle\langle\rangle,\nu_{0},\delta\rangle\xrightarrow{w}\langle\langle(a_{1},t_{1})\rangle,\nu_{1},\rho_{1}\rangle\xrightarrow{w}\ldots\xrightarrow{w}\langle
z,\nu_{n},\rho_{n}\rangle$.

Symbolic traces are sufficient to describe the execution of a program, as all
timed traces induced by a symbolic trace end in the same observable trace:

######  Theorem 3.

Let $s$ be a symbolic trace of a program $\Delta$, let $w\models\Sigma$, and
$z,z^{\prime}\in\operatorname{tw}(s)$. Then for every situation formula
$\alpha$: $w,z\models\alpha$ iff $w,z^{\prime}\models\alpha$. proofs

###### Proof of Theorem 3.

∎

First, $|z|=|z^{\prime}|=n$ by definition of $\operatorname{tw}$. We show the
statement by induction over $n$.
Base case. Let $z=\langle\rangle$. Then also $z^{\prime}=\langle\rangle$, and
the statement follows.
Induction step. Let $z=z_{1}\cdot(a,t)$ and
$z^{\prime}=z_{1}^{\prime}\cdot(a^{\prime},t^{\prime})$. By induction,
$w,z\models\alpha$ iff $w,z^{\prime}\models\alpha$. By Definition 25,
$a=a^{\prime}$. As the precondition and successor state axioms may not mention
clock constraints, $w,z_{1}\models[a]\alpha$ iff
$w,z_{1}^{\prime}\models[a]\alpha$. Thus, the statement follows.

We can now define the symbolic execution of a program:

######  Definition 26 (Symbolic Program Execution).

Given a program $\Delta=(\delta,\Sigma)$, the _symbolic execution_ of $\Delta$
is a labeled transition system $\mathcal{E}=(E,e_{0},\xrightarrow[]{})$
defined as follows:

  * •

$E=\mathcal{S}_{\Delta}\times\operatorname{N}_{C}\times\operatorname{sub}(\delta)$,

  * •

$e_{0}=(\langle\rangle,\vec{0},\delta)$,

  * •

$(s,\nu,\rho)\xrightarrow[t]{(a,g,Y)}(s^{\prime},\nu^{\prime},\rho^{\prime})$
if there is $z\in\operatorname{tw}(s)$ and
$z^{\prime}=z\cdot(a,\operatorname{time}(z)+t)$ such that

    1. 1.

$s^{\prime}=s\cdot(a,g,Y)$,

    2. 2.

$\langle z,\nu,\rho\rangle\xrightarrow{w}\langle
z^{\prime},\nu^{\prime},\rho^{\prime}\rangle$,

    3. 3.

$c\in Y$ iff $w,z^{\prime}\models\operatorname{reset}(c)$, and

    4. 4.

$g=g_{a}$, i.e., the guard in $\Sigma$ wrt $a$.

######  Example 3.

The $\mathcal{E}$ of the program $\Delta=(\Sigma^{\text{lo}},\delta)$ with

$\delta=(\mathit{start}\\_{\mathit{cam}()};\mathit{end}\\_{\mathit{cam}()};)\mid\mathit{start}\\_{\mathit{grasp}}$

allows the following transitions:

$e_{0}\xrightarrow[0.5]{\mathit{start}\\_{\mathit{cam}()},\top,\\{c_{\mathit{cam}}\\}}e_{1}\quad
e_{1}\xrightarrow[1]{\mathit{end}\\_{\mathit{cam}()},c_{\mathit{cam}}=1,\\{\\}}e_{2}$

(and more), where

$\displaystyle e_{0}$ $\displaystyle=(\langle\rangle,\vec{0},\delta)$
$\displaystyle e_{1}$
$\displaystyle=(\langle(\mathit{start}\\_{\mathit{cam}()},\top,c_{\mathit{cam}})\rangle,\\{c_{\mathit{cam}}:0\\},$
$\displaystyle\qquad\mathit{end}\\_{\mathit{cam}()}\mid\mathit{start}\\_{\mathit{grasp}})$
$\displaystyle e_{2}$
$\displaystyle=(\langle(\mathit{start}\\_{\mathit{cam}()},\top,c_{\mathit{cam}}),(\mathit{end}\\_{\mathit{cam}()},c_{\mathit{cam}}=1,\emptyset)\rangle,$
$\displaystyle\qquad\\{c_{\mathit{cam}}:1\\},\mathit{start}\\_{\mathit{grasp}})$

For $e=(s,\nu,\rho)$, we also write $\operatorname{tw}(e)$ to mean
$\operatorname{tw}(s)$. For a path
$p=(\langle\rangle,\vec{0},\delta)\xrightarrow[t]{(a_{1},g_{1},Y_{1})}(s_{1},\nu_{1},\rho_{1})\xrightarrow[t]{(a_{2},g_{2},Y_{2})}\ldots\xrightarrow[t]{(a_{n},g_{n},Y_{n})}(s_{n},\nu_{n},\rho_{n})$
of $\mathcal{E}$, we write $\mathcal{Z}(p)=\operatorname{tw}(s_{n})$ for the
timed traces induced by $p$. We say $p$ ends in a final configuration if there
is a $z\in\operatorname{tw}(s_{n})$ such that $\langle
z,\nu_{n},\rho_{n}\rangle\in\mathcal{F}^{w}$. We write
$\mathcal{Z}(\mathcal{E})$ for the set of induced traces of all paths in
$\mathcal{E}$ ending in a final configuration.

######  Lemma 2.

Let $p$ be a path
$p=(\langle\rangle,\vec{0},\delta)\xrightarrow[t]{(a_{1},g_{1},Y_{1})}(s_{1},\nu_{1},\rho_{1})\xrightarrow[t]{(a_{2},g_{2},Y_{2})}\ldots\xrightarrow[t]{(a_{n},g_{n},Y_{n})}(s_{n},\nu_{n},\rho_{n})$
of $\mathcal{E}$ ending in a final configuration. Then for every
$z\in\mathcal{Z}(p)$, $\langle z,\nu_{n},\rho_{n}\rangle\in\mathcal{F}^{w}$.
proofs

###### Proof of Lemma 2.

∎

As $p$ is final, there is a $z_{f}\in\mathcal{Z}(p)$ such that $\langle
z_{f},\nu_{n},\rho_{n}\rangle\in\mathcal{F}^{w}$. Also, by definition of
$\mathcal{Z}(p)$, $z\in\mathcal{Z}(p)$ iff $z\in\operatorname{tw}(s_{n})$.
Thus, by Theorem 3, for every $z\in\mathcal{Z}(p)$ and every situation formula
$\alpha$: $w,z\models\alpha$ iff $w,z_{f}\models\alpha$. Thus, $\langle
z,\nu_{n},\rho_{n}\rangle\in\mathcal{F}^{w}$.

Next, the following theorem establishes the validity of a symbolic execution
with respect to explicit program traces.

######  Theorem 4.

$z\in\mathcal{Z}(\mathcal{E})$ iff $z\in\|\delta\|_{w}$. proofs

###### Proof of Theorem 4.

∎

$\Rightarrow$: Let $z\in\mathcal{Z}(\mathcal{S})$. Then there is a path
$p=(\langle\rangle,\vec{0},\delta)\xrightarrow[t]{(a_{1},g_{1},Y_{1})}(s_{1},\nu_{1},\rho_{1})\xrightarrow[t]{(a_{2},g_{2},Y_{2})}\ldots\xrightarrow[t]{(a_{n},g_{n},Y_{n})}(s_{n},\nu_{n},\rho_{n})$
such that for some $z_{f}\in\operatorname{tw}(s_{n})$, $\langle
z_{f},\nu_{n},\rho_{n}\rangle\in\mathcal{F}^{w}$. By definition of
$\xrightarrow[]{}$ of $\mathcal{E}$,
$\langle\langle\rangle,\vec{0},\delta\rangle\xrightarrow{w}^{*}\langle
z,\nu_{n},\rho_{n}\rangle$. Furthermore, by Lemma 2, $\langle
z,\nu_{n},\rho_{n}\rangle\in\mathcal{F}^{w}$. Therefore, $z\in\|\delta\|_{w}$.
$\Leftarrow$: Let $z\in\|\delta\|_{w}$. Then, by definition of
$\|\cdot\|_{w}$,
$\langle\langle\rangle,\vec{0},\delta\rangle\xrightarrow{w}^{*}\langle
z,\nu_{n},\rho_{n}\rangle$ and $\langle
z,\nu_{n},\rho_{n}\rangle\in\mathcal{F}^{w}$. Now, we show by induction over
the length $i$ of $z$ that
$\langle\langle\rangle,\vec{0},\delta\rangle\xrightarrow{w}^{*}\langle
z,\nu_{i},\rho_{i}\rangle$ implies that there is a path
$p=(\langle\rangle,\vec{0},\delta)\xrightarrow[t_{1}]{(a_{1},g_{1},Y_{1})}(s_{1},\nu_{1},\rho_{1})\xrightarrow[t_{2}]{(a_{2},g_{2},Y_{2})}\ldots\xrightarrow[t_{i}]{(a_{i},g_{i},Y_{i})}(s_{i},\nu_{i},\rho_{i})$
with $z\in\operatorname{tw}(s_{i})$.
Base case. With $i=0$, it follows that $z=\langle\rangle$ and $|p|=0$.
Clearly, $z\in\operatorname{tw}(\langle\rangle)$.
Induction step. Let $|z|=|p|=i$ and $z^{\prime}=z\cdot(a,t)$. By Definition
8.1, $\langle z,\nu_{i},\rho_{i}\rangle\xrightarrow{w}\langle
z^{\prime},\nu_{i+1},\rho_{i+1}\rangle$ and there is a $d\geq 0$ such that

  1. 1.

$t=\operatorname{time}(z)+d$,

  2. 2.

$w,z\models\operatorname{Poss}(a)$,

  3. 3.

$w,z,\nu_{i}+d\models\operatorname{g}(a)$,

  4. 4.

$\nu_{i+1}=0$ if $w,z^{\prime}\models\operatorname{reset}(c)$ and $\nu_{i}+d$
otherwise.

Thus, $z^{\prime}\in\operatorname{tw}(s\cdot(a,g_{a},Y))$, where $c\in Y$ iff
$w,z^{\prime}\models\operatorname{reset}(c)$. Then, by definition of
$\xrightarrow[]{}$ of $\mathcal{E}$,
$(s,\nu_{i},\rho_{i})\xrightarrow[d]{a,g_{a},Y}(s^{\prime},\nu_{i+1},\rho_{i+1})$.

With this symbolic abstraction of the input program, we can now create the
product automaton of the symbolic execution $\mathcal{E}$ and the ATA
$\mathcal{A}{{}_{\phi}}$ which is used to track the satisfaction of the input
specification.

######  Definition 27 (Synchronous Product).

Given a symbolic execution $\mathcal{E}=(E,e_{0},\xrightarrow[]{})$ and an ATA
$\mathcal{A}{{}_{\phi}}$, the synchronous product
$\mathcal{S}=(S,s_{0},\rightarrow)$ is a labeled state transition system,
defined as follows:

  * •

$S=E\times\mathcal{G}$,

  * •

$s_{0}=(e_{0},G_{0})$,

  * •

$(e,G)\xrightarrow{(a,g,Y)}(e^{\prime},G^{\prime})$ if
$e\xrightarrow[t]{(a,g,Y)}e^{\prime}$ and
$G\overset{t}{\rightsquigarrow}G^{*}\overset{F}{\rightarrow}G^{\prime}$ with
$z\in\operatorname{tw}(e)$ and $f\in F$ iff $w[f,z]=1$.

######  Example 4.

The synchronous product $\mathcal{S}$ of $\mathcal{E}$ and
$\mathcal{A}{{}_{\phi_{bad}}}$ (where
$\phi_{\mathit{bad}}=\top\,\mathbf{U}_{\leq 1}\,\neg c\land g$) looks as
follows:

$\displaystyle s_{0}$
$\displaystyle=(e_{0},G_{0})=((\langle\rangle,\vec{0},\delta),\\{(\phi_{\mathit{bad}},0)\\})$
$\displaystyle(e_{0},G_{0})$
$\displaystyle\xrightarrow[0.5]{\mathit{start}\\_{\mathit{cam}()},\top,\\{c_{\mathit{cam}}\\}}(e_{1},\\{(\phi_{\mathit{bad}},0.5)\\})$
$\displaystyle(e_{1},\\{(\phi_{\mathit{bad}},0)\\})$
$\displaystyle\xrightarrow[1]{\mathit{end}\\_{\mathit{cam}()},c=1,\emptyset}(e_{2},\\{(\phi_{\mathit{bad}},1.5)\\})$
$\displaystyle(e_{0},G_{0})$
$\displaystyle\xrightarrow[0.5]{\mathit{start}\\_{\mathit{grasp}},\top,\emptyset}(e_{1},\emptyset)$

The last transition ends in a configuration with an empty ATA configuration,
as $\mathit{grasp}$ causes $\mathit{grasping}$ to be true and therefore
satisfies the specification of bad behavior.

For a symbolic trace $s$, we write $\psi(s)$ for the fluent trace $\psi(z)$
and $F(s)$ for the set of satisfied fluents $F(z)$, where
$z\in\operatorname{tw}(s)$. Note that this is well-defined, as by Theorem 3,
$\psi(z)=\psi(z^{\prime})$ for every $z,z^{\prime}\in\operatorname{tw}(s)$.

######  Theorem 5.

Given a synchronous product $\mathcal{S}$ of $\mathcal{E}$ and
$\mathcal{A}{{}_{\phi}}$, and a timed trace $z$. Then:

  1. 1.

If $z\in\mathcal{Z}(\mathcal{S})$, then there is also a run of
$\mathcal{A}{{}_{\phi}}$ on $F(z)$.

  2. 2.

$z\in\mathcal{Z}(\mathcal{S})$ iff $z\in\|\delta\|_{w}$.

proofs

###### Proof of Theorem 5.

∎

  1. 1.

Follows directly from the fact that $\mathcal{A}{{}_{\phi}}$ is complete.

  2. 2.

Follows by Theorem 4 and because $\mathcal{A}{{}_{\phi}}$ is complete.

###  6.1 Regionalization

We regionalize the states $S$ of $\mathcal{S}$ to obtain a canonical
representation and a finite abstraction for states in $\mathcal{S}$, inspired
by (?; ?; ?). Let $K$ be the greatest constant mentioned in $\phi$. Then
$\text{REG}_{K}$ is a finite set of regions defined for each $0\leq i\leq K$
as follows: $r_{2i}=\\{i\\}$, $r_{2i+1}=(i,i+1)$ and the last region
collecting all values larger than $K$ as $r_{2K+1}=(K,\infty)$. For
$u\in\mathbb{R}_{\geq 0}$, $\operatorname{reg}(u)$ denotes the region in
$\text{REG}_{K}$ containing $u$. For each $\mathcal{S}$-state
$((s,\nu,\rho),G)$, we compute its canonical representation. Let
$\Lambda=2^{(C\cup L)\times\text{REG}_{K}}$ be the alphabet over regionalized
clocks (tuples of name and region) used to represent a regionalized state as
follows:

First, we represent the clock values in $\nu$ as $G_{\nu}=\\{(c,\nu(c))\mid
c\in C\\}$. We partition $G_{\nu}\cup G$ into a sequence of subsets
$G_{1},\ldots,G_{n}$ such that for every $1\leq i\leq j\leq n$, for every pair
$(l_{i},c_{i})\in G_{i}$ and every pair $(l_{j},c_{j})\in G_{j}$, the
following holds: $i\leq j$ iff
$\operatorname{fract}(c_{i})\leq\operatorname{fract}(c_{j})$. For each
$G_{i}$, let
$\operatorname{abs}(G_{i})=\\{(l,\operatorname{reg}(c))\mid(l,c)\in
G_{i}\\}\in\Lambda$. Then, the canonical representation
$H(\nu,G)\in\Lambda^{*}$ of $\nu$ and $G$ is defined as the sequence
$H(\nu,G)=(\operatorname{abs}(G_{1}),\ldots,\operatorname{abs}(G_{n}))$. We
say that two $\mathcal{S}$-configurations $S=(s,\nu,\rho,G)$ and
$S^{\prime}=(s^{\prime},\nu^{\prime},\rho^{\prime},G^{\prime})$ are
equivalent, written $S\sim S^{\prime}$ if
$(s,\rho,H(\nu,G))=(s^{\prime},\rho^{\prime},H(\nu^{\prime},G^{\prime}))$.

######  Proposition 1 ((?)).

The relation $\sim$ is a bisimulation over $\mathcal{S}$, i.e., $S_{1}\sim
S_{1}^{\prime}$ and $S_{1}\xrightarrow{a,g,Y}S_{2}$ implies
$S_{1}^{\prime}\xrightarrow{a,g,Y}S_{2}^{\prime}$ for some $S_{2}^{\prime}$
with $S_{2}\sim S_{2}^{\prime}$.

Using this proposition, we can define a regionalized version of the
synchronous product as follows:

######  Definition 28 (Regionalized Synchronous Product).

Given a synchronous product $\mathcal{S}=(S,s_{0},\xrightarrow{})$. The
_discrete quotient_ $\mathcal{T}_{\sim}$ of $\mathcal{S}$ is a symbolic
transition system (STS)
$\mathcal{T}_{\sim}=(S_{\sim},\sigma_{0},\lhook\joinrel\xrightarrow{})$ with

  * •

$S_{\sim}=\\{(s,\rho,H(\nu,G))\mid((s,\nu,\rho),G)\in S\\}$,

  * •

$\sigma_{0}=(\langle\rangle,\delta,H(\vec{0},G_{0}))$, and

  * •

$(s,\rho,h)\lhook\joinrel\xrightarrow{a,g,Y}(s^{\prime},\rho^{\prime},h^{\prime})$
iff there exists $(\nu,G)\in H^{-1}(h)$ such that such that
$((s,\nu,\rho),G)\xrightarrow{a,g,Y}((s^{\prime},\nu^{\prime},\rho^{\prime}),G^{\prime})$
and $h^{\prime}=H(\nu^{\prime},G^{\prime})$.

######  Example 5.

The regionalization of $\mathcal{S}$ from Example 4 with $K=1$ looks as
follows:

$\displaystyle\sigma_{0}$
$\displaystyle\lhook\joinrel\xrightarrow{\mathit{start}\\_{\mathit{cam}()},\top,\\{c_{\mathit{cam}}\\}}\sigma_{1}$
$\displaystyle\sigma_{1}$
$\displaystyle\lhook\joinrel\xrightarrow{\mathit{end}\\_{\mathit{cam}()},c=1,\emptyset}\sigma_{2}$
$\displaystyle\sigma_{0}$
$\displaystyle\lhook\joinrel\xrightarrow{\mathit{start}\\_{\mathit{grasp}},\top,\emptyset}\sigma_{3}$

where

$\displaystyle\sigma_{0}$
$\displaystyle=(\langle\rangle,\delta,(\\{(c_{\mathit{cam}},0),(\phi_{\mathit{bad}},0)\\}))$
$\displaystyle\sigma_{1}$
$\displaystyle=(\langle(\mathit{start}\\_{\mathit{cam}()},\top,c_{\mathit{cam}})\rangle,\mathit{end}\\_{\mathit{cam}()}\mid\mathit{start}\\_{\mathit{grasp}},$
$\displaystyle\qquad(\\{(c_{\mathit{cam}},0),(\phi_{\mathit{bad}},1)\\}))$
$\displaystyle\sigma_{2}$
$\displaystyle=(\langle\rangle,\mathit{start}\\_{\mathit{grasp}},(\\{(c_{\mathit{cam}},2),(\phi_{\mathit{bad}},3)\\}))$
$\displaystyle\sigma_{3}$
$\displaystyle=(\langle\rangle,\mathit{end}\\_{\mathit{cam}()},(\\{(c_{\mathit{cam}},1)\\}))$

######  Theorem 6.

  1. 1.

If $z\in\mathcal{Z}(\mathcal{T}_{\sim})$, then there is also a run of
$\mathcal{A}{{}_{\phi}}$ on $F(z)$.

  2. 2.

$z\in\mathcal{Z}(\mathcal{T}_{\sim})$ iff $z\in\mathcal{Z}(\mathcal{S})$.

proofs

###### Proof of Theorem 6.

∎

  1. 1.

Follows directly from the fact that $\mathcal{A}{{}_{\phi}}$ is complete.

  2. 2.

Follows by the definition of $\lhook\joinrel\xrightarrow{}$ and Proposition 1.

With the definition of $\mathcal{T}_{\sim}$ we have obtained a finite
abstraction of the original product automaton of the input program and the
specification. However, the abstraction $\mathcal{T}_{\sim}$ allows several
successors for the same symbolic action $a$, as in $\mathcal{T}_{\sim}$ states
are also distinguished based on the configurations of the ATA. To test whether
a final configuration reachable via a symbolic trace is safe requires to check
all possible successors for all symbolic actions on this trace for safety. To
overcome this, analogous to (?), in the next step we make $\mathcal{T}_{\sim}$
symbol-deterministic.

######  Definition 29 (Deterministic Discrete Quotient).

Given a discrete quotient
$\mathcal{T}_{\sim}=(S_{\sim},\sigma_{0},\lhook\joinrel\xrightarrow{})$, the
deterministic version
$\mathcal{DT}_{\sim}=(\mathit{SW},c_{0},\lhook\joinrel\xrightarrow{}_{D})$ of
$\mathcal{T}_{\sim}$ is defined as follows:

  * •

$\mathit{SW}=\mathcal{S}_{\Delta}\times\operatorname{sub}(\delta)\times
2^{\Lambda^{*}}$,

  * •

$c_{0}=(\langle\rangle,\delta,\\{H(w_{0})\\})$, and

  * •

$(s,\rho,\mathcal{C})\lhook\joinrel\xrightarrow{a,g,Y}_{D}(s^{\prime},\rho^{\prime},\mathcal{C}^{\prime})$
iff $\mathcal{C}^{\prime}=\\{h^{\prime}\mid\exists h\in\mathcal{C}\text{ with
}(s,\rho,h)\lhook\joinrel\xrightarrow{a,g,Y}(s^{\prime},\rho^{\prime},h^{\prime})\\}$.

######  Theorem 7.

  1. 1.

If $z\in\mathcal{Z}(\mathcal{DT}_{\sim})$, then there is also a run of
$\mathcal{A}{{}_{\phi}}$ on $F(z)$.

  2. 2.

$z\in\mathcal{Z}(\mathcal{DT}_{\sim})$ iff
$z\in\mathcal{Z}(\mathcal{T}_{\sim})$.

proofs

###### Proof of Theorem 7.

∎

  1. 1.

Follows from the completeness of $\mathcal{A}{{}_{\phi}}$.

  2. 2.

Follows from the definition of $\lhook\joinrel\xrightarrow{}$ of
$\mathcal{T}_{\sim}$ and Proposition 1: the transition-relation of
$\mathcal{DT}_{\sim}$ combines successor-states of a symbolic action $a,g,Y$,
which per definition agree on the same $s,\rho,\nu$ and only differ in the
ATA-configuration.

###  6.2 Timed Games

We use a variant of _downward closed games_ (?; ?) for the synthesis of a
controller, where a controller exists if there is a safe strategy, i.e., a
trace in the Golog program that leads to an accepting state while the
specification is satisfied. We construct a timed game over
$\mathcal{DT}_{\sim}$, whose states allow to determine safety with respect to
the specification, which enables us to formally describe a _winning strategy_
for the timed game. Formally, a timed game is defined as follows:

######  Definition 30 (Timed Golog Game).

A _timed Golog game_ is a pair $\mathbb{G}=(\Delta,\mathcal{L})$, where
$\Delta$ is a Golog program and $\mathcal{L}\subseteq
T\mathcal{P}_{\Sigma}^{*}$ is a timed language over finite words.

A _validity function_ over $A_{\Sigma}$ is a function
$\operatorname{val}\colon 2^{\mathit{A}_{\Sigma}}\rightarrow
2^{2^{\mathit{A}_{\Sigma}}}$ such that for every set of timed actions
$U\subseteq\mathit{A}_{\Sigma}$ is mapped to a non-empty family of subsets of
$U$. A _strategy_ in $\Delta$ respecting $\operatorname{val}$ is a mapping
that maps each program state to a set of actions such that each of those
actions again results in successor states that are mapped by the strategy.
Formally, it is a mapping $f\colon
D\subseteq\operatorname{Succ}^{*}_{w}(\langle\rangle,\vec{0},\delta)\rightarrow
2^{\mathit{A}_{\Sigma}}$ such that $(\langle\rangle,\vec{0},\delta)\in D$ and
for all $s=(z,\nu,\rho)\in D$,
$f(s)\in\operatorname{val}(\\{a\mid(z\cdot(a,t_{a}),\nu^{\prime},\rho^{\prime})\in\operatorname{Succ}(s)\\})$,
and for all $b\in f(s)$ and every $s^{\prime}$ with
$s^{\prime}=(z\cdot(b,t_{b}),\nu^{\prime},\rho^{\prime})\in\operatorname{Succ}(z,\nu,\rho)$:
$s^{\prime}\in D$. The set of plays of $f$, denoted by
$\operatorname{plays}(f)$, is the set of traces of $\delta$ that are
consistent with the strategy $f$. Formally, $z\in\operatorname{plays}(f)$ iff
for every prefix $z^{\prime}\cdot b$ of $z$, $b\in f(z^{\prime})$.

Let $\operatorname{val}$ be a validity function over $\mathit{A}_{\Sigma}$. A
strategy respecting $\operatorname{val}$ in the timed game
$\mathbb{G}=(\Delta,\mathcal{L})$ is a strategy in $\Delta$ respecting
$\operatorname{val}$. A strategy $f$ is winning with respect to undesired
behavior iff
$(\operatorname{plays}(f)\cap\|\delta\|_{w})\cap\mathcal{L}=\emptyset$.
Intuitively, a state in $\mathcal{DT}_{\sim}$ is bad, if it is final and
contains a bad ATA-configuration. Formally, a $\mathcal{S}$-state
$a=((s,\nu,\rho),G)$ is _bad_ if there exists a $z\in\operatorname{tw}(s)$
with $\langle z,\nu,\rho\rangle\in\mathcal{F}^{w}$ and $G$ is accepting. A
state $(s,\rho,h)$ of $\mathcal{T}_{\sim}$ is _bad_ if there exists
$(\nu,G)\in H^{-1}(h)$ and $((s,\nu,\rho),G)$ is bad. A state
$(s,\rho,\mathcal{C})$ of $\mathcal{DT}_{\sim}$ is _bad_ if there is an
$h\in\mathcal{C}$ such that $(s,\rho,h)$ is bad. A strategy $f$ in
$\mathcal{DT}_{\sim}$ is _safe_ iff for every finite play $z$ of $f$, $z$ does
not end in a bad state of $\mathcal{DT}_{\sim}$.

######  Theorem 8.

There is a winning strategy in $\mathbb{G}$ with respect to _undesired
behavior_ iff there is a safe strategy in $\mathcal{DT}_{\sim}$. proofs

###### Proof of Theorem 8.

∎

By Theorem 5, Theorem 6, and Theorem 7, $z\in\mathcal{Z}(\mathcal{DT}_{\sim})$
iff $z\in\|\delta\|_{w}$ for some $w\models\Sigma$. Therefore, for every
strategy $f$, $f$ is a strategy in $\mathbb{G}$ iff $f$ is a strategy in
$\mathcal{DT}_{\sim}$. If $f$ is a winning strategy in $\mathbb{G}$ with
respect to undesired behavior, then we show that $f$ is safe for
$\mathcal{DT}_{\sim}$: Suppose that $z$ is a bad play in
$\mathcal{DT}_{\sim}$. Then, by definition of $\mathcal{DT}_{\sim}$ and by
Proposition 1, there would be a path in $\mathcal{S}$ from the initial state
to a bad state whose trace is $z$. By construction, this implies
$z\in\|\delta\|_{w}$ for some $w\models\Sigma$ and $z\in\mathcal{L}(\phi)$.
Contradiction to $f$ being a winning strategy in $\mathbb{G}$.

Similarly, if $f$ is safe for $\mathcal{DT}_{\sim}$, then we show that $f$ is
a winning strategy in $\mathbb{G}$ with respect to undesired behavior. Suppose
$f$ is not a winning strategy in $\mathbb{G}$. Then, there is a play
$z\in\operatorname{plays}(f)$ with $z\in\|\delta\|_{w}$ for some
$w\models\Sigma$ and $z\in\mathcal{L}(\phi)$. By definition of
$\mathcal{DT}_{\sim}$ and by Proposition 1, $z$ is a bad play in
$\mathcal{DT}_{\sim}$. Contradiction to $f$ being safe for
$\mathcal{DT}_{\sim}$.

###  6.3 Decidability

With the definition of a timed Golog game from the previous section, we can
design an algorithm, that synthesizes a controller for $\Delta$ with respect
to $\phi$. In the following, we show that the underlying problem of finding a
winning strategy in our game is decidable.

Intuitively, the idea is to show that the search over states of
$\mathcal{DT}_{\sim}$ terminates. We define a reflexive and transitive
relation $\leq$ on states $s_{i}$ of $\mathcal{DT}_{\sim}$, which allows to
state that if $s_{1}\leq s_{2}$ holds and we know that for $s_{1}$ we cannot
find a solution, then we also cannot find a solution for state $s_{2}$. If for
every infinite sequence of states, there exists at least one pair of indices
$i,j,i<j$ such that $s_{i}\leq s_{j}$, we can safely terminate the search when
reaching $s_{j}$. In case $\leq$ fulfills the this property,
$(\mathit{SW},\leq)$ is called a _ well-quasi-ordering (wqo)_.

To be able to relate two states $(s,\rho,\mathcal{C})$ and
$(s^{\prime},\rho^{\prime},\mathcal{C}^{\prime})$ of $\mathcal{DT}_{\sim}$, we
need to be able to relate the sets of regionalized configurations
$\mathcal{C},\mathcal{C}^{\prime}$, which can be achieved via an induced
_monotone domination order_.

######  Definition 31 (Monotone Domination Order).

Given a quasi-ordering (qo) $(S,\leq)$, the _monotone domination order_ is the
qo $(S^{*},\leq^{*})$ over the set $S^{*}$ of finite words over $S$ such that
$x_{1},\ldots,x_{m}\leq^{*}y_{1},\ldots,y_{n}$ iff there is a strictly
monotone injection $h:\\{1,\ldots,m\\}\rightarrow\\{1,\ldots,n\\}$ such that
$x_{i}\leq y_{h(i)}$ for all $1\leq i\leq m$.

######  Example 6 (Monotone Domination).

Consider the two finite sequences of sets of natural numbers
$s_{1}=(\\{1\\},\\{2\\})$ and $s_{2}=(\\{1\\},\\{1,2\\},\\{3\\})$. Using the
monotone domination order $(2^{\mathbb{N}*},\preccurlyeq)$ induced by the qo
$(2^{\mathbb{N}},\subseteq)$, we can see that $s_{1}\preccurlyeq s_{2}$ since
$\\{1\\}\subseteq\\{1\\}$ and $\\{2\\}\subseteq\\{1,2\\}$.

Here, we will use the qo $(\Lambda,\subseteq)$ to induce a monotonic
domination order for $\mathcal{C}$.

We use results by (?) which relate different orderings to state that the
induced monotonic domination order here is a wqo.

######  Proposition 2 ((?)).

(1) Each better-quasi-ordering (bqo) is a wqo.  (2) If $S$ is finite,
$(2^{S}\subseteq)$ is a bqo.  (3) If $(S,\leq)$ is a bqo, then
$(S^{*},\leq^{*})$ is a bqo.  (4) If $(S,\leq)$ is a bqo, then
$(2^{S},\sqsubseteq)$ is a bqo.

It follows that while in general a monotonic domination order is a qo, here it
is a wqo:

######  Lemma 3.

  * •

The monotone domination order $(\Lambda^{*},\preccurlyeq)$ induced by the qo
$(\Lambda,\subseteq)$ is a bqo.

  * •

The powerset ordering $(2^{\Lambda^{*}},\sqsubseteq)$ induced by
$(\preccurlyeq,\Lambda^{*})$ is a bqo.

proofs

###### Proof of Lemma 3.

∎

$S\cup L\cup\text{REG}_{K}$ is finite, thus, by Proposition 2,
$(\Lambda,\subseteq)$ is a bqo. Again by Proposition 2,
$(\Lambda^{*},\preccurlyeq)$ is a bqo. Also, again by Proposition 2,
$(2^{\Lambda^{*}},\sqsubseteq)$ is also a bqo.

Until now, we have synthesized a wqo for the configurations $\mathcal{C}$ of a
state $(s,\rho,\mathcal{C})$ of $\mathcal{DT}_{\sim}$, which is a Cartesian
product of a symbolic trace $s$, the remaining program $\rho$ and the set of
regionalized configurations $\mathcal{C}$. We use the following lemma to state
that wqos are closed under finite Cartesian products.

######  Lemma 4 ((?)).

The Cartesian product of a finite number of wqos is a wqo.

It remains to establish a wqo over symbolic traces and remaining programs to
establish an wqo over states of $\mathcal{DT}_{\sim}$:

######  Definition 32.

The ordering $(\mathit{SW},\leq_{d})$ between states of $\mathcal{DT}_{\sim}$
is defined as follows:
$(s,\rho,\mathcal{C})\leq_{d}(s^{\prime},\rho^{\prime},\mathcal{C}^{\prime})$
iff  (1) $F(\operatorname{tw}(s))=F(\operatorname{tw}(s^{\prime}))$,  (2)
$\rho=\rho^{\prime}$, and  (3) $\mathcal{C}\sqsubseteq\mathcal{C}^{\prime}$.

######  Theorem 9.

$(\mathit{SW},\leq_{d})$ is a wqo. proofs

###### Proof of Theorem 9.

∎

For $F(s)=F(s^{\prime})$ as well as $\rho=\rho^{\prime}$, note that the sets
$\mathcal{P}_{\Sigma}$ and $\operatorname{sub}(\delta)$ are finite. Thus, by
Proposition 2, the orderings $(2^{\mathcal{P}_{\Sigma}},\subseteq)$ and
$(2^{\operatorname{sub}(\delta)},\subseteq)$ and thus also
$(2^{\mathcal{P}_{\Sigma}},=)$ and $(2^{\operatorname{sub}(\delta)},=)$ are
bqos. Furthermore, by Lemma 3, $(2^{\Lambda^{*}},\sqsubseteq)$ is a bqo. Thus,
by Lemma 4 and because each bqo is also a wqo, $\leq_{d}$ is a wqo.

With this theorem, we have defined a wqo over states of $\mathcal{DT}_{\sim}$.
This allows us to traverse $\mathcal{DT}_{\sim}$ and stop expanding a branch
whenever we found a node $(s,\rho,h)$ with an ancestor
$(s^{\prime},\rho^{\prime},h^{\prime})$ such that
$(s^{\prime},\rho^{\prime},h^{\prime})\leq_{d}(s,\rho,h)$. As
$(\mathcal{DT}_{\sim},\leq_{d})$ is a wqo, each sub-branch will only be
expanded finitely many times. Thus:

######  Theorem 10.

The Golog controller synthesis problem for MTL constraints (as defined in
Definition 23) is decidable. proofs

###### Proof Sketch for Theorem 10.

∎

Following the approach presented in (?), we explore the search tree over
configurations of $\mathcal{DT}_{\sim}$, starting from the initial
configuration $c_{0}$ (see Definition 29) to determine safe strategy in
$\mathcal{DT}_{\sim}$. Leaf nodes in the tree are labeled _bad_ if they
contain a bad configuration and otherwise marked as being _good_. Intermediate
nodes $(s,\rho,h)$ are expanded if they do not have a predecessor
$(s^{\prime},\rho^{\prime},h^{\prime})$ in the tree where
$(s^{\prime},\rho^{\prime},h^{\prime})\leq_{d}(s,\rho,h)$, in which case they
are labeled as _good_. Labels for intermediate, expanded nodes are determined
based on the labels of their child nodes: if all child-nodes are labelled
_good_ , the node is labelled as _good_ , otherwise it is labelled as _bad_. A
safe strategy in $\mathcal{DT}_{\sim}$ exists if the root node is labelled
_good_. Each path in the resulting search tree is finite, as we would
otherwise obtain an infinite anti-chain wrt $(\mathcal{DT}_{\sim},\leq_{d})$,
a contradiction to $(\mathcal{DT}_{\sim},\leq_{d})$ being a wqo. With Theorem
8, we obtain a decidable procedure for the controller synthesis problem.

##  7 Conclusion

High-level control of robots is challenging, as the developer needs to take
care both of the high-level behavior and the low-level details of the robot
platform, which often poses implicit constraints on the program. To alleviate
this issue, we proposed to make those constraints explicit as a Metric
Temporal Logic (MTL) specification. We have presented a theoretical framework
to synthesize a Golog controller that ensures that the given specification is
satisfied. Based on an extension of Golog with clocks and adapting well-known
results from timed automaton synthesis, we have described an effective
synthesis algorithm that is guaranteed to terminate.

For future work, we plan to extend our MTL synthesis tool TACoS (?) to Golog
programs. Additionally, while MTL over infinite words is generally
undecidable, it may be interesting to restrict the specification to _Safety
MTL_, which is decidable on infinite words and thus may allow controller
synthesis for non-terminating Golog programs.

## References

  * Abdulla and Nylén 2001 Abdulla, P. A., and Nylén, A.  2001\.  Timed Petri Nets and BQOs.  In Applications and Theory of Petri Nets 2001, 53–70.  Springer.
  * Abdulla, Bouajjani, and d’Orso 2003 Abdulla, P. A.; Bouajjani, A.; and d’Orso, J.  2003\.  Deciding Monotonic Games.  In Computer Science Logic, 1–14.  Springer.
  * 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.
  * Asarin et al. 1998 Asarin, E.; Maler, O.; Pnueli, A.; and Sifakis, J.  1998\.  Controller Synthesis for Timed Automata.  IFAC Proceedings Volumes 31(18):447–452.
  * 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, 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\.
  * D’souza and Madhusudan 2002 D’souza, D., and Madhusudan, P.  2002\.  Timed Control Synthesis for External Specifications.  In Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS), 571–582.  Springer.
  * 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.
  * Henzinger 1998 Henzinger, T. A.  1998\.  It’s about time: Real-time logics reviewed.  In CONCUR’98 Concurrency Theory, 439–454.  Springer.
  * 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 and Lakemeyer 2021 Hofmann, T., and Lakemeyer, G.  2021\.  Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints.  arXiv:2102.09837.
  * Hofmann and Schupp 2021 Hofmann, T., and Schupp, S.  2021\.  TACoS: A tool for MTL controller synthesis.  In Proceedings of the 19th International Conference on Software Engineering and Formal Methods.
  * 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.
  * Kruskal 1960 Kruskal, J. B.  1960\.  Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi’s Conjecture.  Transactions of the American Mathematical Society 95(2):210–225.
  * 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).
  * 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.
  * Viehmann, Hofmann, and Lakemeyer 2021 Viehmann, T.; Hofmann, T.; and Lakemeyer, G.  2021\.  Transforming robotic plans with timed automata to solve temporal platform constraints.  In Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI).

## Proofs

proofs

  *[MTL]: Metric Temporal Logic
  *[BATs]: basic action theory
  *[LTL]: Linear Time Logic
  *[TA]: timed automaton
  *[BAT]: basic action theory
  *[fd-BAT]: finite-domain basic action theory
  *[fd-BATs]: finite-domain basic action theory
  *[ATA]: alternating timed automaton
  *[STS]: symbolic transition system
  *[wqo]: well-quasi-ordering
  *[qo]: quasi-ordering
  *[bqo]: better-quasi-ordering
  *[wqos]: well-quasi-ordering
  *[ MTL]: Metric Temporal Logic