Copyright (c) 2024 IEEE 1 0 current page.north east -2.5cm -1cm

# Time-Robust Path Planning with
Piece-Wise Linear Trajectory for Signal Temporal Logic Specifications

Nhan-Khanh Le1, Erfaun Noorani2, Sandra Hirche1, and John S. Baras2 1NK. Le
and S. Hirche are with the Chair of Information-oriented Control (ITR), School
of Computation, Information and Technology, Technical University of Munich,
80333 Munich, Germany. Emails: {nhankhanh.le<EMAIL_ADDRESS>Noorani and
J. Baras are with the Department of Electrical and Computer Engineering and
the Institute for Systems Research (ISR) at the University of Maryland,
College Park, MD, USA. Emails<EMAIL_ADDRESS>partially
supported by ONR grant N00014-17-1-2622, by a grant from the Army Research
Lab, by the Clark Foundation, and the European Union’s Horizon Europe
innovation action program under grant agreement No. 101093822, ”SeaClear2.0”.

###### Abstract

Real-world scenarios are characterized by timing uncertainties, e.g., delays,
and disturbances. Algorithms with temporal robustness are crucial in
guaranteeing the successful execution of tasks and missions in such scenarios.
We study time-robust path planning for synthesizing robots’ trajectories that
adhere to spatial-temporal specifications expressed in Signal Temporal Logic
(STL). In contrast to prior approaches that rely on discretized trajectories
with fixed time-steps, we leverage Piece-Wise Linear (PWL) signals for the
synthesis. PWL signals represent a trajectory through a sequence of time-
stamped waypoints. This allows us to encode the STL formula into a Mixed-
Integer Linear Program (MILP) with fewer variables. This reduction is more
pronounced for specifications with a long planning horizon. To that end, we
define time-robustness for PWL signals. Subsequently, we propose quantitative
semantics for PWL signals according to the recursive syntax of STL and prove
their soundness. We then propose an encoding strategy to transform our
semantics into a MILP. Our simulations showcase the soundness and the
performance of our algorithm.

##  I Introduction

Temporal Logic (TL) is a branch of logic equipped with an expressive language
capable of reasoning logical statements with respect to _time_ [1]. TL is used
to express the spatial-temporal behavior of a system unambiguously from
natural languages, e.g., a mission specification “robot $1$ is _eventually_
inside region $A$ and stays there for $5$ time units” can be captured
unambiguously with TL formulas. Using TL allows for synthesizing robots’
trajectories with automated algorithms that meet the expected spatial-temporal
behavior. This is known as the _formal synthesis_ problem.

Signal Temporal Logic (STL) is a variant of TL. It extends its predecessor
temporal logic languages, such as Linear Temporal Logic (LTL), to enable
specifications of continuous-time signals. Its support for signals over the
reals and its quantitative semantics [2] allow evaluating the _robustness_ ,
i.e., _degree of satisfaction_ , of a signal with respect to a specification.
In other words, one can measure how well the system meets or falls short of
meeting a specification. This is essential for practical automated mission
design and synthesis to account for potential uncertainties.

Exploring the robustness with respect to STL formulas involves an assessment
of both spatial and temporal dimensions. Formal STL synthesis with spatial
robustness is well-studied [3, 4, 5]. Here, we focus on the notion of temporal
robustness.

Temporal robustness is essential in practical applications, where assigning
fixed-time missions is challenging and robots frequently encounter delays,
unexpected early starts, or disturbances during execution. The notion of
temporal robustness for STL formulas was introduced in [6]. Following this,
[7, 8, 9] further investigated the notion of temporal robustness in the
context of monitoring and control synthesis.

One approach employed for formal synthesis with STL is to transform (space and
time) robust STL with linear predicates into linear constraints using mixed
binary and continuous variables and construct a Mixed-Integer Linear Program
(MILP). In [8, 9], the authors propose a strategy to encode time robustness
into linear constraints for discretized signals, which allows for time-robust
control synthesis using MILP s. This builds upon prior methods in [10, 3] that
propose the encoding rules using big-M methods [11] to encode space robust STL
with linear predicates into a MILP. This approach does not scale well. The
generated constraints from an STL formula are imposed on _each_ discretized
trajectory instance. This implies that the MILP increases in the number of
binary and continuous variables proportionally to the planning horizon.
Several methods for achieving an efficient optimization-based synthesis have
been proposed, ranging from sequential quadratic programming [4] and gradient-
based [12] methods to using time-varying Control Barrier Function (CBF) and
decomposition [13]. However, these methods are investigated solely for space-
robustness. Since the definition of time-robustness involves time-shifting,
the above-mentioned methods are not applicable [8].

This motivates us to explore a scalable synthesis method that also provides
robustness against timing uncertainties. Our method is inspired by the
hierarchical path-planning method using Piece-Wise Linear (PWL) signals
proposed in [14, 15]. A PWL signal considers a trajectory as a sequence of
waypoints consisting of timestamps and values. As a result, the size of the
constructed MILP does not depend on the time horizon but solely on the number
of waypoints. [14, 15] show that various planning problems can be represented
by a fewer number of waypoints compared to the number of discretized
trajectory instances, especially for long-time-horizon planning problems. The
notion of time-robustness for PWL signals has not been investigated. We
propose and investigate the concept of time-robustness for PWL signals. We
summarize our contribution in detail here:

Contributions & Organization.

  * •

_Definition and Quantitative Semantics of Time-Robust STL for PWL Signals_
(Section III): We define the notion of temporal robustness with respect to an
STL specification for PWL signals. We then propose the quantitative semantics
and prove their soundness. With our semantics, we are able to express time-
robustness directly using the few numbers of waypoints, and evaluate the time-
margin of a PWL signal with respect to a specification.

  * •

_Time-Robust STL Path Planning_ (Section IV): We formulate a hierarchical
time-robust formal synthesis problem using PWL signals. This allows for
synthesizing the waypoints that not only satisfy a specification but also
maximize the time-robustness.

  * •

_MILP Encoding_ (Section V): We propose an encoding strategy to transform our
proposed semantics into a MILP. This allows for direct solutions to our
formulated time-robust path planning problem.

  * •

_Simulation Results_ (Section VI): We implement the synthesis algorithm and
use several different mission specifications with different complexity to
verify the soundness and study the performance of our method.

Mathematical Notation: True and False are denoted by $\top$ and $\perp$,
respectively. We use the set ${\mathbb{B}=\\{\perp,\top\\}=\\{0,1\\}}$ to
denote both sets of boolean and binary values. The set of natural, integer,
and real numbers are denoted by $\mathbb{N},\mathbb{Z},\mathbb{R}$,
respectively. We use $\mathbb{Z}_{\geq 0}$ and $\mathbb{R}_{\geq 0}$ to denote
the set of non-negative integers and real numbers. The set of strict positive
natural index is denoted by ${\mathbb{N}_{K}:=\\{1,2,\cdots,K\\}}$. We use
$\sqcap$ for infimum and $\sqcup$ supremum operators. The assignment operator
is $\Coloneqq$. The Euclidean norm is denoted by ${\left\|.\right\|_{2}}$. The
“equivalence” of expressions is denoted with $\equiv$. Additionally, we define
the sign operator $\text{sgn}(\cdot)$ over boolean variables, i.e.,
$\text{sgn}(x)=1$ when $x=1$ and $\text{sgn}(x)=-1$ when $x=0$.

##  II Preliminaries

We begin by introducing the syntax and qualitative semantics of STL for
continuous signals. Given the inherent computational challenges in handling
continuous signals using the existing solution methods, we opt for PWL signals
as a practical alternative. We present the definition of PWL signals and their
qualitative semantics.

###  II-A STL

We first present the syntax and semantics of STL for continuous signals [6].
Let $\xi(\cdot):\mathbb{T}\xrightarrow{}\mathbb{X}$ be a continuous signal
where $\xi(t)\in\mathbb{X}\subseteq\mathbb{R}^{d}$ denotes the real-valued
signal instance with $d$ dimensions at time instant
$t\in\mathbb{T}\subseteq\mathbb{R}_{\geq 0}$. Within the context of motion
planning for robots, we use the terms _signal_ and _trajectory_
interchangeably.

######  Definition 1 (STL Syntax)

$\displaystyle\phi\Coloneqq{\pi}|\lnot{\pi}|\phi_{1}\wedge\phi_{2}|\phi_{1}\vee\phi_{2}|\Diamond_{I}\phi|\square_{I}\phi|\phi_{1}\mathcal{U}_{I}\phi_{2},$
(1)

where ${\pi}$ and ${\lnot\pi}$ denote an atomic predicate and its negation,
and $\phi_{1}$ and $\phi_{2}$ are formulas of class $\phi$. The logical
operators are conjunction ($\wedge$) and disjunction ($\vee$). Temporal
operators are “Eventually” ($\Diamond$), “Always” ($\square$) and “Until”
($\mathcal{U}$) with the subscript $I$ denoting the time interval
${[a,b],0\leq a\leq b}$.

Similar to [15], we use _Negation Normal Form_ syntax, i.e., negation is
applied only to atomic predicates ${\pi}$. It is not restrictive because we
can express any STL formula using this syntax [15]. We assume that an atomic
predicate can be represented by a linear function. Let
${\mu(\cdot):\mathbb{X}\xrightarrow{}\mathbb{R}}$ be a linear function that
maps a signal instance to a real value. Such function represents an atomic
predicate ${\pi}$ through the relationship ${{\pi}\Coloneqq\mu(\xi(t))\geq
0}$, i.e., ${\pi}$ holds _true_ if and only if $\mu(\xi(t))\geq 0$.

In the following, we introduce the qualitative semantics of STL which define
when a signal satisfies a formula $\phi$ at time $t$. In particular, we write
$(\xi,t)\models\phi$ if $\xi$ satisfies $\phi$ at $t$, and
$(\xi,t)\not\models\phi$ if $\xi$ does not satisfy $\phi$ at $t$. The
semantics are defined _recursively_ for each formula in the syntax (1) below.

######  Definition 2 (Qualitative Semantics of STL formulas)

$\displaystyle(\xi,t)$ $\displaystyle\models{\pi}$
$\displaystyle\Leftrightarrow\mu(\xi(t))\geq 0$ (2) $\displaystyle(\xi,t)$
$\displaystyle\models\lnot{\pi}$
$\displaystyle\Leftrightarrow(\xi,t)\not\models{\pi}$ $\displaystyle(\xi,t)$
$\displaystyle\models\phi_{1}\wedge\phi_{2}$
$\displaystyle\Leftrightarrow(\xi,t)\models\phi_{1}\wedge(\xi,t)\models\phi_{2}$
$\displaystyle(\xi,t)$ $\displaystyle\models\phi_{1}\vee\phi_{2}$
$\displaystyle\Leftrightarrow(\xi,t)\models\phi_{1}\vee(\xi,t)\models\phi_{2}$
$\displaystyle(\xi,t)$ $\displaystyle\models\Diamond_{[a,b]}\phi$
$\displaystyle\Leftrightarrow\exists{{t^{\prime}}\in[t+a,t+b]}~{}(\xi,t^{\prime})\models\phi$
$\displaystyle(\xi,t)$ $\displaystyle\models\square_{[a,b]}\phi$
$\displaystyle\Leftrightarrow\forall{{t^{\prime}}\in[t+a,t+b]}~{}(\xi,t^{\prime})\models\phi$
$\displaystyle(\xi,t)$
$\displaystyle\models\phi_{1}\mathcal{U}_{[a,b]}\phi_{2}$
$\displaystyle\Leftrightarrow\exists
t^{\prime}\in[t+a,t+b],(\xi,t^{\prime})\models\phi_{2}$
$\displaystyle\wedge(\forall
t^{\prime\prime}\in[t,t^{\prime}],(\xi,{t^{\prime\prime}})\models\phi_{1})$

###  II-B PWL Trajectory

Rather than using a continuous signal to represent a robot’s trajectory, one
may use a sequence of timestamped waypoints with the assumption that the path
between each pair of waypoints is linearly connected. We define PWL signal
below.

######  Definition 3 (Waypoint)

A waypoint is a tuple consisting of a timestamp and the signal value

$\displaystyle w=\left<t,p\right>,t\in\mathbb{T}\subseteq\mathbb{R}_{\geq
0},p\in\mathbb{X}\subseteq\mathbb{R}^{d}.$ (3)

######  Definition 4 (Linear Waypoint Segment)

A linear waypoint segment is a pair of a starting and an ending waypoint,
${z}_{i}=\\{w_{i},w_{i+1}\\}\equiv\\{\left<t_{i},p_{i}\right>,\left<t_{i+1},p_{i+1}\right>\\}$
with ${0\leq t_{i}\leq t_{i+1}}$. The value of the piece-wise linear signal at
a given time $t$ can be represented by a linear function
${Z_{i}(\cdot):\mathbb{T}\xrightarrow{}\mathbb{X}}$, i.e.,

$\displaystyle Z_{i}(t)$
$\displaystyle=p_{i}+\frac{p_{i+1}-p_{i}}{t_{i+1}-t_{i}}(t-t_{i}),t\in[t_{i},t_{i+1}].$
(4)

######  Definition 5 (PWL Trajectory)

A piece-wise linear trajectory from $K$ waypoints is a sequence of $K-1$
linear waypoint segments ${\xi_{z_{0}}=\\{z_{0},z_{1},\cdots,z_{K-2}\\}}$.

###  II-C Qualitative STL Semantics for PWL Trajectory

In line with prior research [15], we are only interested in specifications
that indicate the robots to reach and avoid particular regions with the
expected temporal behavior. Therefore, we use atomic predicates ${\pi}$ and
its negation ${\lnot\pi}$ to particularly indicate whether a _linear waypoint
segment_ lies _inside_ or _outside_ a region $\mathcal{P}$. We assume that a
region $\mathcal{P}$ can be approximated by convex polygon
${\mathcal{P}(A,h)=\\{p\in\mathbb{R}^{d}~{}|Ap\leq
h\\},A\in\mathbb{R}^{r\times d},h\in\mathbb{R}^{r}}$.

Let the binary variable $z^{\phi}_{i}$ indicate the statement “segment $z_{i}$
(or _every_ signal instance in $[t_{i},t_{i+1}]$) satisfies the formula
$\phi$”, i.e., ${z^{\phi}_{i}\Coloneqq z_{i}\models\phi}$ and
${z^{\phi}_{i}=\top\Leftrightarrow\text{sgn}(z^{\phi}_{i})=1\Leftrightarrow(\xi,t)\models\phi,\forall
t\in[t_{i},t_{i+1}]}$. Then $\pi$ corresponds to region $\mathcal{P}$, i.e.,
$\pi$ holds true when the trajectory is “inside $\mathcal{P}$” and $\lnot\pi$
when it is “outside $\mathcal{P}$”. From here on, we have $\pi$ and $\lnot\pi$
as the atomic predicates that indicate ${z_{i}^{\pi}\Coloneqq
Z_{i}(t)\in\mathcal{P},\forall t\in[t_{i},t_{i+1}]}$, and
${z_{i}^{\lnot\pi}\Coloneqq Z_{i}(t)\not\in\mathcal{P},\forall
t\in[t_{i},t_{i+1}]}$.

We now show that these “atomic predicates” are constructed from conjunctions
and disjunctions of the aforementioned linear predicate introduced in
Definition 1.

$\displaystyle z_{i}^{{\pi}}\Coloneqq$
$\displaystyle\bigwedge_{j=1}^{r}\bigg{(}\frac{h^{j}-A^{j}p_{i}}{\left\|A^{j}\right\|_{2}}\geq\epsilon\wedge\frac{h^{j}-A^{j}p_{i+1}}{\left\|A^{j}\right\|_{2}}\geq\epsilon\bigg{)},$
(5) $\displaystyle z_{i}^{\lnot{\pi}}\Coloneqq$
$\displaystyle\bigvee_{j=1}^{r}\bigg{(}\frac{A^{j}p_{i}-h^{j}}{\left\|A^{j}\right\|_{2}}\geq\epsilon\wedge\frac{A^{j}p_{i+1}-h^{j}}{\left\|A^{j}\right\|_{2}}\geq\epsilon\bigg{)},$

where $A^{j},h^{j}$ are the coefficients of $j$-th rows of $A$ and $h$, i.e.,
one edge of the polygon. The positive space margin $\epsilon\in\mathbb{R}$ is
used to encounter the uncertain spatial deviation. Note that each term of (5)
is _linear_ in $p_{i}$ or $p_{i+1}$. This is consistent with our assumption of
using linear predicates. The following example explains the notation.

###### Example 1

See Figure 1. ${z_{i}\models\pi\Leftrightarrow Z_{i}(t)\in\mathcal{P},\forall
t\in[t_{i},t_{i+1}]}$, ${z_{i}\models\neg\pi\Leftrightarrow
Z_{i}(t)\not\in\mathcal{P},\forall t\in[t_{i},t_{i+1}]}$. We have
$z_{1}\not\models\pi$, ${z_{1}\models\neg\pi}$, ${z_{2}\models\pi}$,
${z_{2}\not\models\neg\pi}$, ${z_{3}\not\models\pi}$,
${z_{3}\not\models\neg\pi}$, ${z_{4}\not\models\pi}$, and
${z_{4}\not\models\neg\pi}$.

For other operators, [15] proposes the following qualitative semantics:

$\displaystyle z_{i}^{\square_{[a,b]}\phi}$
$\displaystyle\Coloneqq\bigwedge_{j=1}^{K}\left([t_{j},t_{j+1}]\cap[t_{i}+a,t_{i+1}+b]\neq\varnothing\Rightarrow
z_{j}^{\phi}\right).$ (6) $\displaystyle z_{i}^{\Diamond_{[a,b]}\phi}$
$\displaystyle\Coloneqq(t_{i+1}-t_{i}\leq b-a)$
$\displaystyle\wedge\bigvee_{j=1}^{K}\left([t_{j},t_{j+1}]\cap[t_{i+1}+a,t_{i}+b]\neq\varnothing\wedge
z_{j}^{\phi}\right).$ $\displaystyle
z_{i}^{\phi_{1}\mathcal{U}_{[a,b]}\phi_{2}}$
$\displaystyle\Coloneqq(t_{i+1}-t_{i}\leq b-a)\wedge$
$\displaystyle\bigvee_{j=1}^{K}\bigg{(}[t_{j},t_{j+1}]\cap[t_{i+1}+a,t_{i}+b]\neq\varnothing\wedge
z_{j}^{\phi_{2}}$
$\displaystyle\wedge\bigwedge_{l=0}^{j}[t_{l},t_{l+1}]\cap[t_{i},t_{i+1}+b]\neq\varnothing\Rightarrow
z_{l}^{\phi_{1}}\bigg{)}.$

The time-intersection in the above semantics is to guarantee that _every_
instance of a segment $z_{i}$ satisfies the STL formula $\phi$. For example,
consider a formula with the “always” operator $z_{i}^{\square_{[a,b]}\phi}$,
we require the signal at _every_ time-instances ${t_{i}\in[t_{i},t_{i+1}]}$
satisfy $\square_{[a,b]}\phi$, which is equivalent to requiring the signal at
_every_ time-instance between ${[t_{i}+a,t_{i}+b]}$ and
${[t_{i+1}+a,t_{i+1}+b]}$ (or they can be combined into
${[t_{i}+a,t_{i+1}+b]}$) to satisfy $\phi$. A similar explanation is applied
for the other operators. Note that the semantics are stricter than necessary
compared to (2) [15].

##  III Time-Robust STL for PWL Signal

Here, we present the definition of time robustness and its quantitative STL
semantics for PWL signals. The degree of time-robustness, as defined in the
work of Donze et al. [6], quantifies the duration $\theta$ during which a
signal maintains its characteristic with respect to an STL formula. This leads
to two notions of time-robustness: right and left time robustness. These
measure the time margin after and before a specified time instance. In other
words, a signal has $\theta^{\phi}_{+}$ right-time robustness if it satisfies
$\phi$ for _any_ preceding time instance between $[t,t+\theta^{\phi}_{+}]$.
This allows the synthesized signal to encounter _early start_ (left-shifted up
to $\theta^{\phi}_{+}$). Meanwhile, left time-robustness is achieved if the
signal satisfies $\phi$ for _any_ succeeding time instance between
$[t-\theta^{\phi}_{-},t]$. This offers robustness to encounter _delay_ (right-
shifted up to $\theta^{\phi}_{-}$). Similarly, we denote the right/left time
robustness of a linear segment $z_{i}^{\phi}$ with respect to $\phi$ by
$\theta_{\bowtie,{i}}^{\phi}$ where ${\bowtie=\\{+,-\\}}$.

######  Definition 6 (Time-Robust STL for PWL Signal)

For atomic predicates ${\pi}$, the right $\theta_{+,i}$ and left
$\theta_{-,i}$ time robustness of a linear segment $z_{i}$ is defined as

$\displaystyle\theta_{+,i}^{{\pi}}$
$\displaystyle=\text{sgn}(z_{i}^{\pi})\sum_{j=i+1}^{i+k^{+}}(t_{j+1}-t_{j}),$
(7) $\displaystyle\theta_{-,i}^{{\pi}}$
$\displaystyle=\text{sgn}(z_{i}^{\pi})\sum_{j=i-k^{-}}^{i-1}(t_{j+1}-t_{j}),$

where
$k^{+}=\max\\{l\in\mathbb{N}_{K}|~{}\text{sgn}(z_{i}^{\pi})=\text{sgn}(z^{\pi}_{i^{\prime}}),~{}\forall
i^{\prime},i+1\leq i^{\prime}\leq i+l\\}$, and
$k^{-}=\max\\{l\in\mathbb{N}_{K}|~{}\text{sgn}(z_{i}^{\pi})=\text{sgn}(z^{\pi}_{i^{\prime}}),\forall
i^{\prime},i-l\leq i^{\prime}\leq i-1\\}$. For $k=0$, we set
$\theta_{+,i}^{{\pi}}=\theta_{-,i}^{{\pi}}=0$.

For negation, we use a similar definition but replace $z_{i}^{\pi}$ with
$z_{i}^{\neg\pi}$ and $\theta_{\bowtie,{i}}^{{\pi}}$ with
$\theta_{\bowtie,{i}}^{{\lnot\pi}}$. Intuitively, (7) aggregates the time
interval of the succeeding/preceding segments $z_{i^{\prime}}$ as long as both
$z_{i}$ and $z_{i^{\prime}}$ either satisfy $\pi$ or both violate it, i.e.,
${\text{sgn}(z_{i}^{\pi})=\text{sgn}(z^{\pi}_{i^{\prime}})}$.

For logical and temporal operators in the recursive syntax (1), we propose the
following semantics:

$\displaystyle\theta_{\bowtie,{i}}^{\phi_{1}\wedge\phi_{2}}$
$\displaystyle=\theta_{\bowtie,{i}}^{\phi_{1}}\sqcap\theta_{\bowtie,{i}}^{\phi_{2}};~{}\theta_{\bowtie,{i}}^{\phi_{1}\vee\phi_{2}}=\theta_{\bowtie,{i}}^{\phi_{1}}\sqcup\theta_{\bowtie,{i}}^{\phi_{2}}.$
(8) $\displaystyle\theta_{\bowtie,{i}}^{\square_{[a,b]}\phi}$
$\displaystyle=\bigsqcap_{j\in\mathcal{J}^{\cap}}\theta_{\bowtie,{j}}^{\phi},$
(9) $\displaystyle\mathcal{J}^{\cap}$
$\displaystyle=\left\\{j\in\mathbb{N}_{K}|[t_{j},t_{j+1}]\cap[t_{i}+a,t_{i+1}+b]\neq\varnothing\right\\}.$
$\displaystyle\theta_{\bowtie,{i}}^{\Diamond_{[a,b]}\phi}$
$\displaystyle=\bigsqcup_{j\in\mathcal{J}^{\cap}}\theta_{\bowtie,{j}}^{\phi},$
(10) $\displaystyle\mathcal{J}^{\cap}$
$\displaystyle=\left\\{j\in\mathbb{N}_{K}|[t_{j},t_{j+1}]\cap[t_{i+1}+a,t_{i}+b]\neq\varnothing\right\\},$
$\displaystyle t_{i+1}+a$ $\displaystyle\geq t_{i}+b.$
$\displaystyle\theta_{\bowtie,{i}}^{\phi_{1}\mathcal{U}_{[a,b]}\phi_{2}}$
$\displaystyle=\bigsqcup_{j\in\mathcal{J}^{\cap}}\left(\theta_{\bowtie,{j}}^{\phi_{2}}\sqcap\bigsqcap_{l\in\mathcal{L}_{j}^{\cap}}\theta_{\bowtie,{l}}^{\phi_{1}}\right),$
(11) $\displaystyle\mathcal{J}^{\cap}$
$\displaystyle=\left\\{j\in\mathbb{N}_{K}|[t_{j},t_{j+1}]\cap[t_{i+1}+a,t_{i}+b]\neq\varnothing\right\\},$
$\displaystyle\mathcal{L}^{\cap}_{j}$
$\displaystyle=\left\\{l\in\mathbb{N}_{j}|[t_{l},t_{l+1}]\cap[t_{i},t_{i+1}+b]\neq\varnothing\right\\},$
$\displaystyle t_{i+1}+a$ $\displaystyle\geq t_{i}+b.$

Figure 1: The gray area denotes the original polygon $\mathcal{P}$. The
shrunk/bloated polygons by $\epsilon$ distant margin are the inner/outer
dotted lines, respectively. The black line $z_{2}$ represents the line segment
“inside” of the shrunk region and the black line $z_{1}$ represents the line
segment “outside” of the bloated region. The red segments $z_{3},z_{4}$ are
neither “inside” nor “outside” $\mathcal{P}$.

We provide an explanation for the “always” operator (9) similarly to the
qualitative semantics (6), while the other operators can be understood
similarly. The time robustness $\theta_{\bowtie,{i}}^{\square_{[a,b]}\phi}$ is
the minimal (infimum operator) time robustness $\theta_{\bowtie,{j}}^{\phi}$
of _any_ segments $z_{j}$ that intersects with the time interval
${[t_{i}+a,t_{i+1}+b]}$.

The _Soundness_ property of our proposed semantics is formally stated in the
following theorem. If segment $z_{i}$ has positive time robustness with
respect to $\phi$, we know that $z_{i}$ satisfies $\phi$. Inversely, negative
time robustness implies $z_{i}$ does not satisfy $\phi$. The equality case is
inconclusive.

######  Theorem 1 (Soundness)

$\displaystyle\theta_{\bowtie,{i}}^{\phi}$ $\displaystyle>0\Rightarrow
z_{i}^{\phi}=\top$ $\displaystyle\equiv z_{i}\models\phi,$ (12)
$\displaystyle\theta_{\bowtie,{i}}^{\phi}$ $\displaystyle<0\Rightarrow
z_{i}^{\phi}=\perp$ $\displaystyle\equiv z_{i}\not\models\phi.$

###### Proof:

See Appendix A. ∎

Note that there might exist a segment $z_{i}$ that fulfills the specification
$\phi$, but does not guarantee a positive time-robustness, i.e.,
${z_{i}\models\phi\not\Rightarrow\theta_{\bowtie,{i}}^{\phi}>0}$. Also, the
definition of time-robustness for atomic predicates in (7) depends on the
qualitative semantics (5), which is conservative. In particular, there might
exist a PWL segment $z_{i}$ that has both its waypoints outside of a convex
polygon, thus staying outside of the region, but _do not have to fulfill_
$z_{i}^{\lnot{\pi}}=\top$, i.e., ${\exists
z_{i},Z_{i}(t)\not\in\mathcal{P},z_{i}^{\lnot\pi}=\perp}$. This is to show
that the proposed semantics are sound but not complete.

##  IV Problem Formulation

Our goal is to generate robot trajectories that satisfy a spatial-temporal
specification expressed with STL and stay satisfied under time uncertainties.
The direct synthesis from general STL formula is not real-time capable [16,
17]. To mitigate this issue, we adopt a _hierarchical_ planning framework,
which involves an offline high-level planner that synthesizes a reference PWL
signal and a low-level controller for tracking. This control framework is
commonly utilized in various autonomous systems [14, 15].

With the recursive syntax (1), we are able to express the expected temporal
behavior from the time reference $t_{0}=0$, i.e., $z_{o}$. In other words, the
mission $\phi$ is characterized _qualitatively_ by $z_{o}^{\phi}$, and its
time robustness _quantitatively_ by $\theta_{\bowtie,{0}}^{\phi}$. We formally
state our time-robust synthesis problem below.

######  Problem 1 (Time-Robust STL Synthesis)

Given an STL specification $\phi$, find a sequence of $K$ waypoints to
construct a PWL signal ${\xi_{z_{0}}}$ that satisfies $\phi$, and maximize the
trajectory’s time robustness $\theta_{\bowtie,{0}}^{\phi}$.

$\displaystyle\max_{\xi_{z_{0}}}-J(\xi_{z_{0}})$
$\displaystyle+\lambda\theta_{\bowtie,{0}}^{\phi}$ $\displaystyle\textbf{s.t.
~{}~{}~{}~{}}\theta_{\bowtie,{0}}^{\phi}$ $\displaystyle\geq\theta^{*}>0$
$\displaystyle|p_{i+1}-p_{i}|$ $\displaystyle\leq v_{b}(t_{i+1}-t_{i}),\forall
i\in\\{0,\cdots,K-1\\}$

where the strict positive $\theta^{*}$ is the time robustness threshold. The
objective function $J(\xi_{z_{0}})$ expresses the desired path properties,
e.g., minimal path length, or the shortest make-span. The time robustness is
maximized through the term $\theta_{\bowtie,{0}}^{\phi}$. The positive scalar
$\lambda$$>$$0$ is used to trade-off the time-robustness and performance. As
$\lambda$ increases, it gives greater significance to ensuring time-
robustness. The final inequality ensures the feasibility of the synthesized
signal for dynamical systems by constraining the velocity to remain bounded,
where $v_{b}$$>$$0$.

######  Remark 1 (Feasibility)

We assume the existence of a specific _number of waypoints_ $K$ for which the
synthesis problem is _feasible_. Moreover, if the solution exists, Theorem 1
guarantees that it satisfies $\phi$ because $\theta_{\bowtie,{0}}^{\phi}$ is
strictly positive. In practice, $K$ is determined _heuristically_ , i.e.,
either given, or we increase $K$ incrementally until a feasible solution is
obtained.

######  Remark 2 (Advantage of using PWL Signals)

PWL signal represents a robot’s trajectory through a fixed number of $K$
waypoints. The parameter $K$ is _mission dependent_ , e.g., the environments,
the number of reach-avoid regions, the spatial pattern of robots’ trajectory,
etc. To our understanding, $K$ is determined heuristically as there is no
generic method that can pre-define the number of necessary waypoints. However,
[14, 15] show that various expressive planning tasks in practice can be
represented by a small $K$ compared to the _number of instances_ of a
_discretized signal_. Moreover, an advantageous property of PWL signal over
the discretized one is that _$K$ does not directly depend on the planning
horizon_. In particular, imagine that we use a discretized signal for a
mission with a given planning horizon. For a long horizon, the signal, due to
the lower bound of the sampling rate, needs more instances to cover the whole
mission. The results of previous works [17, 16] suggest that the large number
of instances causes the computational burden of Problem 1. On the other hand,
it is not necessary for PWL signal to use more waypoints for a longer planning
horizon. As long as the signal has sufficient waypoints (see Remark 1), we can
directly assign the planning horizon to the timestamp of the last waypoint.
Therefore, we say that the number of waypoints is _invariant_ to the planning
horizon and this is the primary benefit of PWL signals, especially for long-
horizon problems. We provide a more comprehensive complexity analysis in the
next section.

##  V Mixed-Integer Linear Program (MILP)

Problem 1 can not be solved analytically for a general $\phi$ due to the
logical operators. Therefore, we propose an encoding strategy to transform it
into a MILP. Considering the timestamps and the spatial locations as
optimization variables, the encoding uses additional binary and continuous
variables to construct _linear_ constraints that correspond to
$\theta_{\bowtie,{0}}^{\phi}$. This approach is widespread; see [10, 3, 17,
9].

We introduce the general big-M methods that encode the necessary operators. A
detailed explanation of the encoding can be found in [10, 3]. We adapt the
ideas in [9] to encode time-robustness for atomic predicates with PWL signals.
Our contribution is the encoding for our proposed semantics.

###  V-A General MILP Encoding

To transform the STL formula into a MILP, the encoding aims to convert each
operator occurred in the semantics (6), and (8)-(11). We briefly summarize the
necessary encoding that is applied in the previous works [10, 3, 9] as follows

  * •

_Linear predicate:_ Each linear predicate is represented by a linear function
$\mu(\cdot)$. We use linear predicates to indicate whether _a point_ lies in
the inside/outside face of an edge of a convex polygon $\mathcal{P}$ (see
(5)). For instance, let
${\mu(p_{i})=\frac{h^{j}-A^{j}p_{i}}{\left\|A^{j}\right\|_{2}}-\epsilon}$ be a
linear function. If $\mu(p_{i})\geq 0$, $p_{i}$ is on the side of the edge
$(A^{j},h^{j})$ that lies within the polygon (_inside_) $\mathcal{P}$ with
$\epsilon$ space margin. We can capture $\mu(p_{i})\geq 0$ through a binary
variable $b^{\mu}$ as

$\displaystyle-M(1-b^{\mu})$ $\displaystyle\leq{\mu}(p_{i})\leq
Mb^{\mu}-m_{\epsilon},$ (13)

where $M,m_{\epsilon}$ are sufficiently large and small positive numbers,
respectively. If $b^{\mu}=1$, ${\mu}(p_{i})\geq 0$, else ${\mu}(p_{i})<0$. For
the case “ _outside_ $(A^{j},h^{j})$ by $\epsilon$ space margin”, we apply the
same encoding method with
${\mu(p_{i})=\frac{A^{j}p_{i}-h^{j}}{\left\|A^{j}\right\|_{2}}-\epsilon}$.

  * •

_Conjunction_ : To encode $b=\bigwedge_{i=1}^{m}b_{i}$, i.e., conjunction of
$m$ binary variables, we impose the following constraints ${b\leq
b_{i},\forall i\in\mathbb{N}_{m}}$ and  ${b\geq\sum_{i=1}^{m}b_{i}-(m-1).}$

  * •

_Disjunction_ : To encode $b=\bigvee_{i=1}^{m}z_{i}$, we impose ${b\geq
b_{i},\forall i\in\mathbb{N}_{m}}$ and  ${b\leq\sum_{i=1}^{m}b_{i}.}$

  * •

_Infimum and Supremum_ : The infimum of $m$ continuous variables, i.e.,
$\theta=\bigsqcap_{i=1}^{m}\theta_{i}$, is encoded by using $m$ binary
variables $\\{b_{1},\cdots,b_{m}\\}$ and impose the following linear
constraints for $\theta$ as

$\displaystyle\theta_{i}-(1-b_{i})M\leq\theta\leq\theta_{i},\forall
i\in\mathbb{N}_{m},$ (14a) $\displaystyle\sum_{i=1}^{m}b_{i}=1.$ (14b)

Equation (14a) ensures that $\theta$ is smaller than other variables and equal
to any $\theta_{i}$ if and only if $b_{i}=1$. Equation (14b) ensures that the
infimum of the set exists. For supremum, we use similar encoding constraints
as the infimum, but replace (14a) with
${\theta_{i}\leq\theta\leq\theta_{i}+(1-b_{i})M}$.

  * •

_Product of continuous and binary variable_ : To encode
${y=xb,x\in\mathbb{R},b\in\mathbb{B}}$, we impose

$\displaystyle-Mb\leq y\leq Mb,~{}x-M(1-b)\leq y\leq x+M(1-b),$ (15)

where $M>0$ is a sufficiently large upper bound of $x$.

###  V-B Time Robustness Encoding for PWL signal

We use the right-time robustness to explain the encoding. A similar strategy
can be applied for the left time robustness. We first introduce the time
robustness encoding for the atomic predicates, and then for the temporal
operators.

  * •

_Time robustness encoding for ( 7), i.e., for $\pi$ and $\lnot\pi$_: Let
$\theta_{+,{i}}^{{\pi}}$ be the right time robustness of segment $z_{i}$ with
respect to an atomic predicate $\pi$, we adapt the “counting” encoding concept
proposed by [9] to generate linear constraints such that
$\theta_{+,{i}}^{{\pi}}$ corresponds to the right time robustness in (7). To
this end, we introduce two _continuous_ _time-aggregating_ variables $\Delta
t^{1}_{i}$ and $\Delta t^{0}_{i}$ for _each_ segment and encode
$\theta_{+,{i}}^{{\pi}}$

$\displaystyle\Delta t^{1}_{i}$ $\displaystyle=(\Delta t^{1}_{i+1}+\delta
t_{i})z_{i}^{\pi},\Delta t^{0}_{i}=(\Delta t^{0}_{i+1}-\delta
t_{i})(1-z_{i}^{\pi})$ (16) $\displaystyle\theta_{+,{i}}^{{\pi}}$
$\displaystyle=\Delta t^{1}_{i}+\Delta
t^{0}_{i}+\left(-z_{i}^{\pi}\delta_{i}+(1-z_{i}^{\pi})\delta_{i}\right)$ (17)
$\displaystyle=z_{i}^{\pi}\Delta t^{1}_{i+1}+(1-z_{i}^{\pi})\Delta
t^{0}_{i+1},$ (18)

with ${\delta t_{i}=t_{i+1}-t_{i}}$, ${\Delta t^{1}_{K-1}=\Delta
t^{0}_{K-1}=0}$.

According to (7), the constraints depend on $z_{i}^{\pi}$, i.e., the
qualitative value of segment $z_{i}$ with respect to the atomic predicate
$\pi$. As defined in (5), $z_{i}^{\pi}$ indicates whether _a segment_ $z_{i}$
lies inside $\mathcal{P}$, which is constructed through conjunction and
disjunction of linear predicates. Therefore, we apply the encoding techniques
in Section V-A to obtain the constraints for $z_{i}^{\pi}$.

Next, we use $\Delta t^{1}_{i}$ and $\Delta t^{0}_{i}$ to encode the sign
operator in (7). In particular, (16) implies that $\Delta t^{1}_{i}$
aggregates the time interval of the successive segments $z_{i+1}$ if
${z^{\pi}_{i+1}=z^{\pi}_{i}=1}$, while $\Delta t^{0}_{i}$ aggregates the
negative time interval, i.e., $-\delta t_{i}$ if
$\text{sgn}(z^{\pi}_{i+1})=\text{sgn}(z^{\pi}_{i})=0$. Moreover, since (16) is
recursive, the aggregation continues until
$\text{sgn}(z_{i+1})\neq\text{sgn}(z_{i})$. This corresponds to the $\sum$
operator used in (7).

Finally, since these variables are disjunctive, i.e., ${\Delta t^{1}_{i}\neq
0\Rightarrow\Delta t^{0}_{i}=0}$ and vice versa [9], they can be combined into
$\Delta t^{1}_{i}+\Delta t^{0}_{i}$ as shown in (17). The last summand in (17)
is explained by the fact that the time robustness defined in (7) does not
contain the time interval $\delta_{i}$ of the current segment $z_{i}$, so we
have to subtract or add $\delta_{i}$ according to the sign of $z_{i}$. The
encoding for negation $\lnot\pi$ is performed similarly by replacing
$z^{\pi}_{i}$ and $\theta_{+,{i}}^{{\pi}}$ with $z^{\lnot\pi}_{i}$ and
$\theta_{+,{i}}^{{\lnot\pi}}$.

Furthermore, we emphasize that (16) and (18) can be realized with linear
constraints by using the encoding for multiplication of binary and continuous
variables in (15).

  * •

_Time robustness encoding for temporal operators ( 8)-(11)_: We instruct the
encoding for the “eventually” ($\Diamond$), the other operators can be done
similarly. Recall the expression from (10). Let $\theta_{\bowtie}^{*}$ be
$\theta_{\bowtie,{i}}^{\Diamond_{[a,b]}\phi}$. We introduce $K$$-$$1$
additional binary variables $\\{b_{1},\cdots,b_{K-1}\\}$ and impose the
following constraints

$\displaystyle
b_{ij}^{\cap}\Coloneqq(t_{i}+b-t_{j}\geq\epsilon_{t})\wedge(t_{j+1}-(t_{i+1}+a)\geq\epsilon_{t})$
$\displaystyle~{}~{}~{}~{}~{}~{}\wedge\left(t_{i+1}-t_{i}\leq
b-a\right),\forall j\in\mathbb{N}_{K-1};$ (19a)
$\displaystyle\theta_{\bowtie,{j}}^{\phi}-(1-b_{ij}^{\cap})M\leq\theta_{\bowtie}^{*},\forall
j\in\mathbb{N}_{K-1};$ (19b)
$\displaystyle\theta_{\bowtie}^{*}\leq\theta_{\bowtie,{j}}^{\phi}+(1-b_{j})M,\forall
j\in\mathbb{N}_{K-1};$ (19c) $\displaystyle b_{ij}^{\cap}\geq b_{j},\forall
j\in\mathbb{N}_{K-1};\sum_{j=1}^{K}b_{j}=1.$ (19d)

First, in (19a), the binary variable $b^{\cap}_{ij}$ with
$\epsilon_{t}\in\mathbb{R}_{\geq 0}$ indicates whether two time-intervals
$[t_{j},t_{j+1}]$ and ${[t_{i+1}+a,t_{i}+b]}$ intersects. If
$b^{\cap}_{ij}=\top$, they intersect, else they don’t. Equation (19b) implies
that $\theta_{\bowtie}^{*}$ is greater or equal to the time robustness of
_any_ segments that intersect with $[t_{i+1}+a,t_{i}+b]$. Meanwhile, (19c)
guarantees that $\theta_{\bowtie}^{*}$ is bounded by
$\theta_{\bowtie,{j}}^{\phi}$ whenever $b_{j}=1$. Finally, (19d) ensures that
the supremum belongs to the set that intersects the interval, i.e.,
$b_{j}=1\Rightarrow b_{ij}^{\cap}=1$. Besides, $\sum_{j=1}^{K}b_{j}=1$ ensures
that the supremum exists.

###  V-C Complexity Analysis

We analyze the encoding complexity for a PWL signal $\xi_{z_{0}}$ with $K$
waypoints. Atomic predicates (AP) (or negations) are constructed through the
set of $|AP|$ linear predicates, thus we need $\mathcal{O}(|AP|K)$ binary
variables for $\xi_{z_{0}}$. Time robustness for AP requires $\mathcal{O}(1)$
additional continuous variables for each segment as shown in (16), thus
$\mathcal{O}(K)$ for $\xi_{z_{0}}$. For temporal operators, we need additional
variables to encode the time-intersection and infimum/supremum. Each segment
requires $\mathcal{O}(K)$ additional binary and $\mathcal{O}(1)$ continuous
variables, which respectively results in $\mathcal{O}(K^{2})$ and
$\mathcal{O}(K)$ for $\xi_{z_{0}}$. The generalized number of binary and
continuous variables of the MILP is $\mathcal{O}(|\phi|K^{2})$ and
$\mathcal{O}(|\phi|K)$, respectively 111For a formula with _one single
temporal operator_ , e.g., $\Diamond_{[I]}{\pi}$, $\square_{[I]}{\pi}$, we
just impose constraints on the first segment, thus only requiring
$\mathcal{O}(|AP|K)$ binary variables instead of
$\mathcal{O}(|AP|K+|\phi|K^{2})$..

It’s worth highlighting a comparison between our results and the encoding
achieved through discretizing the signal into $T$ instances. The analysis in
[9] shows a complexity of $\mathcal{O}(|AP|T)$ binary and
$\mathcal{O}(|\phi|T)$ continuous variables. Although the number of binary
variables required by PWL signal depends on the quadratic term $K^{2}$,
various path-planning problems can be represented in practice with $K^{2}\ll
T$ [15]. The analysis confirms Remark 2 that the encoding with PWL signal
_does not directly depend on the planning horizon_.

###  V-D Algorithm Overview

We summarize our approach in the following algorithms. We initialize the PWL
signal ${\xi_{z_{0}}}$ as optimization variables. The STL encoding is
performed modularized for each region $\mathcal{P}$ and recursive for temporal
operators (Algorithm 1). Then the algorithm 2 combines the linear constraints
obtained from the encoding of _every_ regions and additionally considers
dynamical constraints to construct a complete MILP. The generated PWL
trajectory/waypoints from an MILP optimizer is then used as a reference for a
low-level tracking controller.

Algorithm 1 Single Region Reach-Avoid Specification

1:Region $\mathcal{P}$, STL Formula $\phi$ for $\mathcal{P}$, number of
waypoints $K$, variables of PWL Trajectory ${\xi_{z_{0}}}$ from Definition 5

2:Set of linear constraints $\mathcal{X}_{\phi}$

3:$\mathcal{X}_{\phi}$$\leftarrow$ {}

4:$A\in\mathbb{R}^{m\times 2},h\in\mathbb{R}^{m}$ $\leftarrow$ Convex
Approximation of $\mathcal{P}$

5:for $j\leftarrow 1$ to $m$ do

6: for $z_{i}^{\pi}\leftarrow z_{0}^{\pi}$ to $z_{K-1}^{\pi}$ do

7: $z_{i}^{\pi}$, $\mathcal{X}$$\leftarrow$ (5), $A^{j},h^{j}$

8: $\mathcal{X}_{\phi}$$\leftarrow$ {$\mathcal{X}_{\phi}$, $\mathcal{X}$}

9: end for

10:end for

11:for $z_{i}^{\pi}\leftarrow z_{0}^{\pi}$ to $z_{K-1}^{\pi}$ do

12: $\theta_{\bowtie,{i}}^{\pi}$, $\mathcal{X}$$\leftarrow$ $z_{i}^{\pi}$,
(18)

13: $\mathcal{X}_{\phi}$$\leftarrow$ {$\mathcal{X}_{\phi}$, $\mathcal{X}$}

14:end for

15:for temporal operators in $\phi$ (backward, recursive) do

16: $\theta_{\bowtie,{i}}^{\phi}$, $\mathcal{X}$$\leftarrow$ Applies Section V
for $\theta_{\bowtie,{i}}^{\pi}$

17: $\mathcal{X}_{\phi}$$\leftarrow$ {$\mathcal{X}_{\phi}$, $\mathcal{X}$}

18:end for

Algorithm 2 Time-Robust Synthesis with MILP

1:STL Formula $\phi$, number of waypoints $K$, maximal velocity $v_{b}>0$,
makespan $T>0$

2:${\xi_{z_{0}}}$

3:Initialize decision variables ${\xi_{z_{0}}}$

4:$\mathcal{X}_{\phi}$$\leftarrow$ {}

5:// STL constraints

6:for each region $\mathcal{P}$ in $\phi$ do

7: $\mathcal{X}$$\leftarrow$ Algorithm 1($\mathcal{P}$, $\phi$, $K$,
$\xi_{z_{0}}$)

8: $\mathcal{X}_{\phi}$$\leftarrow$ {$\mathcal{X}_{\phi}$, $\mathcal{X}$}

9:end for

10:// Dynamic constraints for the waypoints

11:$\mathcal{X}_{\phi}$$\leftarrow$ {$\mathcal{X}_{\phi}$,
$t_{0}=0,t_{K-1}=T$}

12:// Loop over each pair of waypoints
$\left<t_{i},p_{i},t_{i+1},p_{i+1}\right>$

13:for i $\leftarrow$ 0 to $K-1$ do

14: $\mathcal{X}_{\phi}$$\leftarrow$ {$\mathcal{X}_{\phi}$, $t_{i+1}\geq
t_{i},|p_{i+1}-p_{i}|\leq v_{b}(t_{i+1}-t_{i})$}

15:end for

16:// MILP Synthesis

17:${\xi_{z_{0}}}$ $\leftarrow$ GUROBI($\mathcal{X}_{\phi}$,
$J({\xi_{z_{0}}})$)

##  VI Benchmark

[$\phi_{1}$ Multi-Blocks-1 ]

[$\phi_{2}$ Multi-Blocks-2 ]

[$\phi_{3}$ Door-Puzzle-1 ]

[$\phi_{4}$ Door-Puzzle-2 ]

Figure 2: The simulation results of the four scenarios. The blue circles in
the figures are the synthesized waypoints. The PWL signal is the blue piece-
wise linear path connecting the waypoints. The $XY$ plane consists of the
reach (green/dark blue)-avoid (red/yellow) regions. The $Z$ axis denotes the
synthesized time-stamp in seconds. The start and end points are marked as
indicated in the legend.

###  VI-A Setup

To evaluate our method, we benchmark against the method using discretized
signals (Instance-based (IB) method) in [8, 9]. To our knowledge, these are
the sole studies in the synthesis of time-robust STL. We implement both
methods in the same hierarchical path-planning fashion, i.e., we use the
encoding of [8, 9] to synthesize the sequence of discretized robots’
trajectory based on a single-integrator model with velocity constraint. We
opted for a discretization step of $1$ s for the sake of argument simplicity.
This choice aligns the planning horizon $T$ with the number of instances of
the discretized signal. The two algorithms are tested with the same task-
dependant planning time horizon and limited velocity of 1 m/s. For PWL signal,
we increase the number of waypoints $K$ incrementally until a feasible
solution is obtained, and further increase $K$ to evaluate the potential
increase in the objective function as a result of using more waypoints.

We evaluate our method in four example mission scenarios. The missions are
chosen to showcase our algorithm in scenarios with a range of spatial and
temporal complexity. In all the missions, the objective is minimizing the path
length encoded through $-J(\xi_{z_{0}})$ and maximizing the time-robustness
$\theta_{\bowtie,{0}}^{\phi}$ with a trade-off parameter $\lambda=1$ as shown
in 1.

###  VI-B Mission Scenarios

Here, we explain the missions in detail first in plain English and then in STL
language. To simplify the notation, temporal operators without time subscripts
imply the overall time horizon $[0,T]$, e.g.,
${\Diamond\equiv\Diamond_{[0,T]}}$.

In the first mission “Multi-Blocks-1”, the robot needs to visit a region and
stay there for a certain time while avoiding the red regions all the time,
i.e., ${\phi_{1}=\bigwedge_{i=1}^{8}\lnot
A_{i}\wedge\Diamond\square_{[0,5]}R_{1}\wedge\Diamond\square_{[0,5]}R_{2}}$.
The starting and ending positions are given. In the second mission “Multi-
Blocks-2” with a longer mission horizon $T=300~{}s$, the robot must monitor an
additional region within a given time window, i.e.,
$\phi_{2}=\bigwedge_{i=1}^{20}\lnot
A_{i}\wedge\Diamond_{[0,150]}\square_{[0,15]}R_{1}\wedge\Diamond_{[180,260]}\square_{[0,15]}R_{2}\wedge\Diamond_{[50,80]}\square_{[0,15]}R_{3}\wedge\square_{[200,220]}R_{3}$.

The third mission “Door-Puzzle-1” requires the robot to eventually visit
region $R_{1}$ and stay there for a certain time. Region $R_{2}$ must be
eventually visited, but the robot is not allowed to pass through the yellow
gate $G_{1}$ before reaching the charging area $C_{1}$, i.e., ${{\phi_{3}=\neg
G_{1}\mathcal{U}_{[0,30]}C_{1}\wedge\Diamond_{[50,80]}\square_{[0,5]}R_{1}\wedge\Diamond\square_{[0,5]}R_{2}}}$.

The fourth mission “Door-Puzzle-2” is an example taken from [15]. The robot is
not allowed to pass through the gates until the key with a corresponding
number is collected at the green region. The final goal is to reach the blue
region, i.e., ${\phi_{4}=\Diamond G\wedge(\wedge_{i=1}^{5}\square\lnot
A_{i})\wedge\wedge_{i=1}^{5}\lnot D_{i}\mathcal{U}R_{i}}$.

###  VI-C Simulation Results

Table I shows the encoded MILP’s information and the optimization results. The
missions are synthesized with various numbers of waypoints $K$, and the
discretized method (the row corresponding to the planning horizon $T$). We
compare the results _row-wise_ between the PWL method with a fixed $K$ and the
discretized method. Figure 2 depicts the synthesized waypoints and the linear
segments.

  1. 1.

_Soundness_ : Overall, all obtained solutions are sound, i.e., none of them
violate the imposed specification.

  2. 2.

_Model Complexity_ :

     * •

Encoding with PWL signal requires fewer continuous variables (all four
scenarios).

     * •

PWL signal requires more binary variables as observed in $\phi_{1}$ and
$\phi_{3}$. For long planning horizons, e.g., $\phi_{2}$ and $\phi_{4}$, PWL
encoding requires fewer binary variables.

This is explained through the complexity analysis in Section V-C. The number
of binary variables increases proportionally with $K^{2}$
($\mathcal{O}(|\phi|K^{2})$), thus the encoding requires more binary variables
when $T\ll K^{2}$. However, in $\phi_{2}$, PWL encoding uses fewer binary
variables because these specifications are dominated by a large number of
“avoid” sub-formula with only one single temporal operator whose complexity is
linear with $K$ ($\mathcal{O}(|AP|K)$) as explained in the footnote of Section
V-C.

  3. 3.

_Objectives and Sensitivity Analysis_ : The objectives obtained from PWL and
IB methods are approximately equivalent (in all scenarios $\phi_{1},\phi_{2}$,
and $\phi_{3}$). The result of $\phi_{3}$ shows that the objective depends on
the number of waypoints $K$. First, we need at least $K$$=$$23$ to obtain a
feasible solution with a poor time-robustness of 0.2 s. When we increase
$K$$=$$25$, we achieve a better time-robustness (9.7 s). Nevertheless, further
increasing $K$ _does not_ always improve the objective, which is observed when
we further increase $K$$=$$30$, or when we vary $K$ in the experiments
$\phi_{1}$ and $\phi_{2}$. This behavior can be explained by the fact that a
greater number of waypoints expands the solution space and may contain a
better solution.

  4. 4.

_Computation Time_ : The solving time is not solely determined by the number
of constraints and variables. This is observed in all four scenarios. When we
vary $K$, MILP requires a longer time to obtain a feasible solution and in
many cases _much longer time_ to completely terminate the program. We
hypothesize that it is affected by the large feasible solution space. Since we
are maximizing the time robustness directly through the continuous timestamps,
it is hard for the branch-and-bound methods to determine the optimal search
path.

Methods | MILP Info | Time [s]
---|---|---
PWL/IB | # Cstr | # Bin | # Cont | Obj ($L,\theta_{+}$) | GRB
$\phi_{1}$ \- Multi-Blocks-1
K = 23 | 22740 | 7724 | 895 | 44.7, 21.8 | 14*
K = 25 | 25764 | 8810 | 975 | 44.7, 21.8 | 26* - 165
K = 30 | 34024 | 11805 | 1175 | 44.7, 21.8 | 165* - TO
T = 100 | 29214 | 7215 | 2959 | 44.7, 23 | 95*
$\phi_{2}$ \- Multi-Blocks-2
K = 25 | 49677 | 16636 | 1973 | 71.4, 17.7 | 38*
K = 27 | 55371 | 18646 | 2187 | 70, 17.7 | 160* - 195
T = 300 | 192532 | 48275 | 16487 | 70, 17 | 630* - TO
$\phi_{3}$ \- Door-Puzzle-1
K = 23 | 18498 | 6394 | 648 | 75, 0.2 | 6*
K = 25 | 21209 | 7383 | 706 | 76, 9.7 | 27*
K = 30 | 28739 | 10153 | 851 | 76, 9.7 | 149* - TO
T = 100 | 21874 | 5537 | 2358 | 76, 10 | 78* - TO
$\phi_{4}$ \- Door-Puzzle-2
K = 35 | 39337 | 11855 | 2090 | 152, 10 | 251* - 305
K = 40 | 46577 | 14085 | 2395 | 143, 14.2 | 904* - TO
T = 200 | 358929 | 111986 | 8566 | - | TO
TABLE I: Our method is denoted by the number of waypoints with the italic
letter K. Methods using discretized-signals are denoted by the planning
horizon written in the plain text $T$. The MILP complexity is reported through
the number of linear constraints (# Cstr), binary variables (# Bin), and
continuous variables (# Cont), respectively. The objective $(L,\theta_{+})$
indicates the optimized path length and the right time robustness. The last
column depicts the optimization time of the Gurobi solver (in seconds). The
number with the symbol $*$ denotes the time that the objective converges to
the optimal solution. The number behind the hyphen (if exists) is the time
that the solver needs to completely terminate the program. “TO” is the time-
out and is set to $1000$ seconds.

To summarize, our method is _sound_ and the time-robust MILP encoding with PWL
offers a complexity that is invariant to the planning horizon. This is
especially advantageous for problems that can be represented by a few
waypoints.

##  VII Conclusion

We synthesize time-robust trajectories that satisfy spatial-temporal
specifications expressed in STL using PWL signals. To that end, we define a
notion of temporal robustness and propose a sound quantitative STL semantics
for PWL signals. Our encoding strategy leads to a MILP encoding with fewer
binary and continuous variables compared to the existing algorithms. This
reduction in complexity of the constructed MILP is more significant for STL
formulas with long time horizons. Our numerical experiments confirm the
soundness of our semantics and our complexity analysis. Several limitations of
this approach are the conservatism and the incompleteness of the semantics.
Future works focus on analyzing the PWL encoding of the atomic predicates to
reduce the conservatism, as well as investigating the completeness property.

## References

  * [1] C. Baier and J.-P. Katoen, _Principles of Model Checking_. The MIT Press, 2008.
  * [2] O. Maler and D. Nickovic, “Monitoring temporal properties of continuous signals,” in _FORMATS/FTRTFT_ , 2004.
  * [3] V. Raman, A. Donzé, D. Sadigh, R. M. Murray, and S. A. Seshia, “Reactive synthesis from signal temporal logic specifications,” _Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control_ , 2015.
  * [4] Y. V. Pant, H. Abbas, and R. Mangharam, “Smooth operator: Control using the smooth robustness of temporal logic,” in _2017 IEEE Conference on Control Technology and Applications (CCTA)_ , 2017, pp. 1235–1240.
  * [5] L. Lindemann and D. V. Dimarogonas, “Control barrier functions for signal temporal logic tasks,” _IEEE Control Systems Letters_ , vol. 3, pp. 96–101, 2019.
  * [6] A. Donzé and O. Maler, “Robust satisfaction of temporal logic over real-valued signals,” in _Proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems_ , ser. FORMATS’10. Berlin, Heidelberg: Springer-Verlag, 2010, p. 92–106.
  * [7] T. Akazaki and I. Hasuo, “Time robustness in mtl and expressivity in hybrid system falsification (extended version),” 2015.
  * [8] A. Rodionova, L. Lindemann, M. Morari, and G. J. Pappas, “Time-robust control for stl specifications,” in _2021 60th IEEE Conference on Decision and Control (CDC)_ , 2021, pp. 572–579.
  * [9] A. Rodionova, L. Lindemann, M. Morari, and G. Pappas, “Temporal robustness of temporal logic specifications: Analysis and control design,” _ACM Trans. Embed. Comput. Syst._ , vol. 22, no. 1, oct 2022. [Online]. Available: https://doi.org/10.1145/3550072
  * [10] S. Karaman, R. G. Sanfelice, and E. Frazzoli, “Optimal control of mixed logical dynamical systems with ltl specifications,” _2008 47th IEEE Conference on Decision and Control_ , pp. 2117–2122, 2008.
  * [11] I. Griva, S. Nash, and A. Sofer, _Linear and Nonlinear Optimization: Second Edition_ , ser. Other Titles in Applied Mathematics. Society for Industrial and Applied Mathematics (SIAM, 3600 Market Street, Floor 6, Philadelphia, PA 19104), 2009. [Online]. Available: https://books.google.de/books?id=uOJ-Vg1BnKgC
  * [12] K. Leung, N. Aréchiga, and M. Pavone, “Back-propagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods,” _ArXiv_ , vol. abs/2008.00097, 2020.
  * [13] Z. Zhang and S. Haesaert, “Modularized control synthesis for complex signal temporal logic specifications,” 2023.
  * [14] C. Fan, K. Miller, and S. Mitra, “Fast and guaranteed safe controller synthesis for nonlinear vehicle models,” _Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I_ , vol. 12224. [Online]. Available: https://par.nsf.gov/biblio/10180137
  * [15] D. Sun, J. Chen, S. Mitra, and C. Fan, “Multi-agent motion planning from signal temporal logic specifications,” _IEEE Robotics and Automation Letters_ , vol. 7, no. 2, p. 3451 – 3458, 2022, cited by: 2; All Open Access, Green Open Access, Hybrid Gold Open Access.
  * [16] Y. V. Pant, H. Abbas, R. A. Quaye, and R. Mangharam, “Fly-by-logic: Control of multi-drone fleets with temporal logic objectives,” in _2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems (ICCPS)_ , 2018, pp. 186–197.
  * [17] Y. Zhou, D. Maity, and J. S. Baras, “Optimal mission planner with timed temporal logic constraints,” in _2015 European Control Conference (ECC)_ , 2015, pp. 759–764.

##  Appendix A Soundness Proof of Time-robust STL for PWL Signal

We prove Theorem 1 induction hypothesis (IH) for each STL formula in the
recursive syntax (1). We prove the right-time robustness. The left one is
derived similarly.

  * •

Atomic predicate $\pi$ (similar for negation $\lnot\pi$) From (7),
${\theta_{+,{i}}^{\pi}>0\Leftrightarrow\text{sgn}(z_{i}^{\pi})\sum_{j=i+1}^{i+k}(t_{j+1}-t_{j})>0.}$.
Since ${(t_{j+1}-t_{j})\geq 0~{}\forall j}$ and
${\text{sgn}(z_{i}^{\pi})=\text{sgn}(z_{i^{\prime}}^{\pi})\neq 0}$, we have
${\theta_{+,{i}}^{{\pi}}>0\Rightarrow\text{sgn}(z^{\pi})=1\Leftrightarrow
z_{i}^{\pi}=\top.}$

  * •

Conjunction: (8)
${\Rightarrow\theta_{\bowtie,{i}}^{\phi_{1}\wedge\phi_{2}}>0\Rightarrow(\theta_{\bowtie,{i}}^{\phi_{1}}>0\wedge\theta_{\bowtie,{i}}^{\phi_{2}}>0)}$.
From IH, we have $z_{i}^{\phi_{1}}=\top\wedge z_{i}^{\phi_{2}}=\top$
${\Rightarrow z_{i}^{\phi_{1}\wedge\phi_{2}}=\top}.$

  * •

Disjunction: (8)
${\Rightarrow\theta_{\bowtie,{i}}^{\phi_{1}\vee\phi_{2}}>0\Rightarrow(\theta_{\bowtie,{i}}^{\phi_{1}}>0\vee\theta_{\bowtie,{i}}^{\phi_{2}}>0)}$
IH implies $z_{i}^{\phi_{1}}=\top\vee z_{i}^{\phi_{2}}=\top$ ${\Rightarrow
z_{i}^{\phi_{1}\vee\phi_{2}}=\top}.$

  * •

Until: from (11),

${\theta_{\bowtie,{i}}^{\phi_{1}\mathcal{U}_{[a,b]}\phi_{2}}>0}$
${\Rightarrow\exists
j\in\mathcal{J}^{\cap},\left(\theta_{\bowtie,{j}}^{\phi_{2}}\sqcap\bigsqcap_{l\in\mathcal{L}_{j}^{\cap}}\theta_{\bowtie,{l}}^{\phi_{1}}\right)>0}$
${\Rightarrow\exists
j\in\mathcal{J}^{\cap},(\theta_{\bowtie,{j}}^{\phi_{2}}>0)\wedge\left(\forall
l\in\mathcal{L}_{j}^{\cap},\theta_{\bowtie,{l}}^{\phi_{1}}>0\right)}$
${\Rightarrow\exists
j,\bigg{(}[t_{j},t_{j+1}]\cap[t_{i+1}+a,t_{i}+b]\neq\varnothing\wedge(z_{j}\models\phi_{2})\bigg{)}}$
${\wedge\bigg{(}\forall l\leq
j,[t_{l},t_{l+1}]\cap[t_{i},t_{i+1}+b]\neq\varnothing\wedge(z_{l}\models\phi_{1})\bigg{)}}$
${\Rightarrow z_{i}^{\phi_{1}\mathcal{U}_{[a,b]}\phi_{2}}=\top.}$

Again, the second last implication is obtained from the induction rule with
$\theta_{\bowtie,{l}}^{\phi_{1}}>0$ and $\theta_{\bowtie,{j}}^{\phi_{2}}>0$. A
similar proof can be shown for ”eventually” and ”always” operators, and also
for the ”violation” case, i.e., $\theta_{\bowtie,{i}}^{\phi}<0\Rightarrow
z_{i}^{\phi}=\perp$.