Online control synthesis for uncertain systems under signal temporal logic specifications

Abstract

Signal temporal logic (STL) formulas have been widely used as a formal language to express complex robotic specifications, thanks to their rich expressiveness and explicit time semantics. Existing approaches for STL control synthesis suffer from limited scalability with respect to the task complexity and lack of robustness against the uncertainty, for example, external disturbances. In this paper, we study the online control synthesis problem for uncertain discrete-time systems subject to STL specifications. Different from existing techniques, we propose an approach based on STL, reachability analysis, and temporal logic trees. First, based on a real-time version of STL semantics, we develop the notion of tube-based temporal logic tree (tTLT) and its recursive (offline) construction algorithm. We show that the tTLT is an under-approximation of the STL formula, in the sense that a trajectory satisfying a tTLT also satisfies the corresponding STL formula. Then, an online control synthesis algorithm is designed using the constructed tTLT. It is shown that when the STL formula is robustly satisfiable and the initial state of the system belongs to the initial root node of the tTLT, it is guaranteed that the trajectory generated by the control synthesis algorithm satisfies the STL formula. We validate the effectiveness of the proposed approach by several simulation examples and further demonstrate its practical usability on a hardware experiment. These results show that our approach is able to handle complex STL formulas with long horizons and ensure the robustness against the disturbances, which is beyond the scope of the state-of-the-art STL control synthesis approaches.

1. Introduction

1.1. Motivation

The rapid growth of robotic applications, such as autonomous vehicles and service robots, has stimulated the need for new control synthesis approaches to safely accomplish more complex objectives such as nondeterministic, periodic, or sequential tasks (Kress-Gazit et al., 2018). Temporal logics, such as linear temporal logic (LTL) (Baier and Katoen, 2008), metric interval temporal logic (MITL) (Koymans, 1990), and signal temporal logic (STL) (Maler and Nickovic, 2004), have shown capability in expressing such objectives for dynamical systems. However, traditional control methods (e.g., linear quadratic regulator, model predictive control, and adaptive control) are originally developed for simple control objectives such as stability and set invariance (Baillieul and Samad, 2021), and these methods are restrictive to handle complex temporal logic tasks. Thus, advanced control methods must be developed to fill this gap.

As a more recently developed temporal logic, STL allows the specification of properties over dense-time. This makes it suitable for expressing complex specifications that may involve specific timing requirements or deadlines. Such specifications include time-constrained reachability (e.g., ${\mathrm{F}}_{\left[\mathrm{0,60}\right]}{\mathrm{G}}_{\left[\mathrm{0,20}\right]}A$ : visit region A within 60 s and stay there for another 20 s) and time-constrained surveillance (e.g., $G{F}_{\left[\mathrm{10,50}\right]}A\wedge G{F}_{\left[\mathrm{10,50}\right]}B$ : visit regions A and B every 10–50 s). STL was originally evaluated over continuous-time signals in Maler and Nickovic (2004), and then extended to discrete-time signals in Raman et al. (2015). STL contains predicates as the atomic elements and the truth value of each predicate is evaluated through a predicate function. Due to a number of advantages, such as explicitly treating real-valued signals (Maler and Nickovic, 2004), and admitting robustness semantics (Fainekos and Pappas, 2009), control synthesis under STL specifications has gained popularity and many efforts have been devoted for STL control synthesis in the last few years. Nevertheless, existing approaches usually suffer from limited scalability with respect to the task complexity and lack of robustness to the uncertainties from the robotic systems.

The complexity of STL formulas (e.g., the time horizon or nestedness) is in general crucial in deciding the complexity of control synthesis approaches, for example, optimization-based methods. For example, the number of integer variables in mixed-integer program based approaches grows exponentially with respect to the time horizon. Other popular approaches, for example, barrier function-based methods, only handle a fragment of STL formulas with non-nested temporal operators. On the other hand, robotic systems are usually corrupted by external disturbances and accompanied by modeling errors. These uncertainties make it challenging to reason about STL specifications due to the encoded time semantics. To the best of our knowledge, few control approaches can efficiently handle system uncertainties with robustness guarantees for STL specifications.

1.2. Related work

1.2.1. LTL or MITL control synthesis

LTL focuses on the Boolean satisfaction of properties by given signals while MITL is a continuous-time extension that allows to express temporal constraints. Existing control approaches that use LTL or MITL mainly rely on a finite abstraction of the system dynamics and a language equivalent automata (Gastin and Oddoux, 2001) or timed-automata (Alur et al., 1996) representation of the LTL or MITL specification. The controller is synthesized by solving a game over the product automata (Belta et al., 2007, 2017; Zhou et al., 2016). Other control approaches include optimization-based (Wolff and Murray, 2016; Fu and Topcu, 2015) and sampling-based methods (Vasile and Belta, 2013; Kantaros and Zavlanos, 2019).

One of the most relevant works is Gao et al. (2022). In this paper, the notion of temporal logic tree (TLT) is proposed for LTL specifications and the corresponding TLT-based control synthesis algorithm is developed. Despite some relevance, it is far from straightforward to extend these results to general STL formulas. Some significant differences between our paper and Gao et al. (2022) are highlighted as follows. First, the definitions and semantics of TLT and tTLT are largely different. In particular, the time constraints encoded in STL formulas require a new notion of real-time STL semantics for connecting tTLT and STL. Second, the control synthesis algorithms in this paper are largely different from that in Gao et al. (2022). In order to carefully monitor the time constraint satisfaction in the STL formulas, the online synthesis algorithm needs in an appropriate way to track the set node (Algorithm 7), update the tTLT (Algorithm 8), and update the post set (Algorithm 11).

1.2.2. STL control synthesis

Given the extensive literature studying STL, we restrict our attention to the following STL synthesis approaches.

1.2.2.1. Optimization-based methods

Optimization methods leverage on the fact that STL formulas can be encoded as mixed-integer constraints. Based on this, STL control synthesis can be obtained by solving a series of optimization problems (Raman et al., 2014, 2015). To avoid the complexity of integer-based optimization, smooth approximations have been proposed by using sequential quadratic programming (SQP) (Gilpin et al., 2021) or convex-concave programming (Takayama et al., 2023). Recent work studies how to reduce the integer variables using the property of logic operators (Kurtz and Lin, 2022). However, these results are restricted to deterministic systems.

An extension of the mixed-integer formulation is investigated for linear systems with additive bounded disturbances in Sadraddini and Belta (2015), where the model predictive controller is obtained by solving the optimization problem at each time step in a receding horizon fashion. In Farahani et al. (2019), a model predictive controller in the form of shrinking horizon is developed for linear systems with stochastic disturbances under STL constraints. One drawback of these approaches is the exponential computational complexity which makes it difficult to be applied to STL formulas with long time horizons. In addition, a stochastic gradient decent-based method is developed to optimize the probability that the stochastic system satisfies an STL specification (Scher et al., 2022).

1.2.2.2. Barrier function methods

Barrier function methods are mainly used for continuous-time systems. The idea is to transfer the STL formula into one or several (time-varying) control barrier functions, and then obtain feedback control laws by solving quadratic programs (Lindemann and Dimarogonas, 2019a). This method is computationally efficient. However, as the existence and design of barrier functions are still open problems, it currently mainly applies to deterministic affine systems. In Yang et al. (2020), the authors consider linear cyber-physical systems with continuous-time dynamics and discrete-time controllers. The proposed offline trajectory planner is based on a mixed integer quadratic program that utilizes control barrier functions to generate satisfying trajectories in continuous-time. Other control synthesis approaches include sampling-based (Vasile et al., 2017a; Karlsson et al., 2020) and learning-based methods (Venkataraman et al., 2020; Kapoor et al., 2020). In addition, control synthesis for multi-agent systems and STL specifications is recently considered in Lindemann and Dimarogonas (2019b); Buyukkocak et al. (2021); Sun et al. (2022).

1.2.2.3. Reachability-based methods

Reachability is a fundamental notion in systems and control and reachability analysis has been widely used for simple control objectives, for example, stability and safety (Bertsekas, 1972). In Roehm et al. (2016), a reachability-based method is proposed for STL model checking by converting an STL formula to reachset temporal logic. This method is refined in (Kochdumper and Bak, 2023) for linear deterministic systems by adequately tuning parameters to enforce over-approximation error to zero. Chen et al. (2018b) recognizes the connection between temporal logic operators and reachability, and then exploits Hamilton-Jacobi reachability for STL control synthesis, which has served as an inspiration to our work. Although there exists close relevance between Chen et al. (2018b) and our paper, some remarkable differences should be highlighted.

First, we find that the connection between temporal logic operators and reachability in Chen et al. (2018b) may not hold for nested STL formulas. We improve and extend this point by introducing the new real-time STL semantics, which is beyond Chen et al. (2018b) and motivates the proposal of the tTLTs. Second, while the control design in Chen et al. (2018b) is restricted to non-nested STL formulas, we propose a systemic way to online synthesize the robust controller for more general STL formulas. In our paper, thanks to the semantic relation between the STL formulas and their corresponding tTLTs, we are able to perform control synthesis over the tTLT, instead of the STL formulas, with a correct-by-construction guarantee.

1.2.2.4. Sampling-based/data-driven/learning-based methods

Motivated by the success of sampling-based methods in motion planning, some recent works consider the extension to the STL planing. In Vasile et al. (2017b), an RRT* approach is developed to incrementally construct a tree such that an STL specification is maximally satisfied. Barbosa et al. (2019) uses a cost function to guide exploration for satisfying a restricted fragment of STL formulas. More recent work Ho et al. (2022) integrates automaton theory and sampling-based methods for STL control synthesis of nonlinear deterministic system. When the system model is unknown, a direct data-driven STL synthesis method is studied using behavioral characterization of linear models (Van Huijgevoort et al., 2023).

In addition, learning-based methods have been becoming popular for STL verification and synthesis. For example, neural network-based methods are investigated in Liu et al. (2022); Leung and Pavone (2022); Hashimoto et al. (2022). By generating rewards in proper ways from STL specifications, reinforcement learning-based approaches have been proposed in Venkataraman et al. (2020); Kapoor et al. (2020); Singh and Saha (2023); Hamilton et al. (2022).

1.2.3. Other related work

Beyond the above literature review, the properties of STL formulas have been studied in different contexts or for different purposes. In Leung et al. (2023), a mechanism is proposed to infuse the logical structure of STL specifications into gradient-based methods by translating STL robustness formulas into computation graphs. In Lindemann et al. (2021a), the STL formulas are interpreted over discrete-time stochastic processes using the the induced risk. Based on this, risk-aware STL control is studied in Lindemann et al. (2022).

1.3. Contributions

In this paper, we aim at developing an efficient, robust, and sound control synthesis algorithm for uncertain robotic systems under STL specifications. Different from existing STL synthesis techniques, we propose an approach based on STL, reachability analysis, and temporal logic trees. The new framework is shown in Figure 1. It consists of two phases. In the offline phase, we propose to transform an STL formula into a tube-based temporal logic tree (tTLT) by performing reachability analysis on the dynamic system under consideration. As a fundamental notion in systems and control, reachability captures the evolution of dynamic systems under inputs (e.g., control inputs and uncertainties). In the online phase, the constructed tTLT is further used to guide the control synthesis. The contributions of our paper are as follows: (i) We propose a real-time version of STL semantics and establish a correspondence between STL formulas and tTLTs via reachability analysis. (ii) We develop an algorithm that can automatically and recursively construct the tTLT from the corresponding STL formula. We show that the tTLT is an under-approximation for a broad fragment of STL formulas, i.e., all the trajectories that satisfy the tTLT also satisfy the corresponding STL formula. (iii) We develop an online control synthesis algorithm based on the constructed tTLT. We show that the algorithm is robust and sound. (iv) We validate the effectiveness of the proposed approach by several simulation examples and further demonstrate its practical usability on a hardware experiment.

Figure 1.

The tTLT-based STL control synthesis framework.

It is worth mentioning that reachability analysis is the core to ensure the robustness of the proposed algorithm, since the uncertainties in the system can be explicitly addressed when performing reachability analysis. Over the past decades, there have been remarkable progresses in the computation of reachable sets for different systems. New software tools on reachability analysis facilitate the usability of the approach proposed in our paper.

We further remark that the robustness here refers to the control ability against system uncertainties. That is, we are interested in synthesizing a controller under which the signals satisfy an STL specification despite the underlying uncertainties. This is different from the notion of quantitative robustness which measures how much a signal satisfies or violates an STL specification.

1.4. Organization and notations

The remainder of the paper is organized as follows. In Section 2, preliminaries and the problem under consideration are formulated. In Section 3, definitions of real-time STL semantics and tTLTs are introduced. Section 4 establishes a semantic connection between STL and tTLT. Section 5 deals with the online control synthesis problem. The results are validated by simulations and experiments in Sections 6 and 7. Conclusions are given in Section 8. The notations used in this work are defined in Table 1.

Table 1.

Notations.

$\mathbb{R}$	Set of real numbers
${\mathbb{R}}_{\ge 0}$	Set of nonnegative real numbers
$\mathbb{N}$	Set of natural numbers
${\mathbb{R}}^n$	Euclidean space of dimension n
${\mathbb{R}}^{n\times m}$	Space of n-by-m real matrices
‖x‖	Euclidean norm of vector x
x T	Transpose of real vector x
∅	Empty set
$\overline{S}$	Complement of a set S
2 S	Set of all subsets of S
|S|	Cardinality of a set S
∪	Set union
∩	Set intersection
¬	Negation operator
∧	Logical operator AND
∨	Logical operator OR
⊂ (⊆)	Subset (subset or equivalent to)
⊃ (⊇)	Super-set (super-set or equivalent to)
[a, b]	Closed interval with end points a and b
S1 \ S2	Set difference of two sets S1 and S2

2. Preliminaries and problem Formulation

2.1. Systems dynamics

Consider an uncertain discrete-time control system of the form

$x_{k+1}=f\left(x_k,u_k,w_k\right),$

(1)

where $x_k:=x\left(t_k\right)\in {\mathbb{R}}^n,u_k:=u\left(t_k\right)\in U,w_k:=w\left(t_k\right)\in W,k\mathbb{\in }\mathbb{N}$ are the state, control input, and disturbance at time t _k , respectively. The time sequence {t _k } can be seen as a sequence of sampling instants, which satisfy 0 = t₀ < t₁ < ⋯. The control input is constrained to a compact set $U\subset {\mathbb{R}}^m$ and the disturbance is constrained to a compact set $W\subset {\mathbb{R}}^l$ . In the following, let us define the control policy.

Definition 2.1

A control policy ν = ν₀ν₁…ν _k … is a sequence of maps ${\nu }_k:{\mathbb{R}}^n\to U$ , $\forall k\mathbb{\in }\mathbb{N}$ . Denote by ${\mathcal{U}}_{\ge k}$ the set of all control policies that start from time t _k .

One can see from Definition 2.1 that a control policy ν is a sequence of time-dependent functions ν _k , each of which is a map from ${\mathbb{R}}^n$ (i.e., the state space) to the control set U. Given the control policy ν, one can select control input u _k = ν _k (x _k ) for implementation at time instant t _k .

Definition 2.2

A disturbance signal w = w₀w₁…w _k … is called admissible if $w_k\in W,\forall k\mathbb{\in }\mathbb{N}$ . Denote by ${\mathcal{W}}_{\ge k}$ the set of all admissible disturbance signals that start from time t _k .

The solution of equation (1) is defined as a discrete-time signal x ≔x₀x₁…. We call x a trajectory of equation (1) if there exists a control policy $\mathbf{\nu }\in {\mathcal{U}}_{\ge 0}$ and a disturbance signal $\mathit{w}\in {\mathcal{W}}_{\ge 0}$ satisfying (1), i.e.,

$x_{k+1}=f\left(x_k,{\nu }_k\left(x_k\right),w_k\right),\forall k\mathbb{\in }\mathbb{N}$

We use ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\left(t_k\right)$ to denote the trajectory point reached at time t _k under the control policy ν and the disturbance w from initial state x₀.

The deterministic system is defined by

$x_{k+1}=f_d\left(x_k,u_k\right)$

(2)

and ${\mathit{x}}_{x_0}^{\mathit{\nu }}\left(t_k\right)$ denotes the solution at time t _k of the deterministic system when the control policy is ν and the initial state is x₀.

2.2. Signal temporal logic

We use STL to concisely specify the desired system behavior. STL (Maler and Nickovic, 2004) is a predicate logic consisting of predicates μ, which are defined through a predicate function $g_{\mu }:{\mathbb{R}}^n\to \mathbb{R}$ as

$\mu :=\{\begin{array}{ll}\top ,& \text{if}\hspace{1em}{g}_{\mu }\left(x\right)\ge 0,\\ \perp ,& \text{if}\hspace{1em}{g}_{\mu }\left(x\right)<0.\end{array}$

The syntax of STL is given by

$\phi ::=\top \mid \mu \mid \neg \phi \mid {\phi }_1\wedge {\phi }_2\mid {\phi }_1{\mathrm{U}}_{\mathrm{I}}{\phi }_2$

(3)

where φ, φ₁, φ₂ are STL formulas and I is a closed interval of $\mathbb{R}$ of the form [a, b] with $a,b\in {\mathbb{R}}_{\ge 0}$ and a ≤ b.

The validity of an STL formula φ is originally defined with respect to a continuous-time signal (Maler and Nickovic, 2004). Later in Raman et al. (2015), the STL semantics with respect to a discrete-time signal has also been proposed. In this work, we study discrete-time control systems. Therefore, we adopt the STL semantics defined in (Raman et al., 2015).

The validity of an STL formula φ with respect to a discrete-time signal x at time t _k , is defined inductively as follows (Raman et al., 2015):

$\begin{array}{l}\left(\mathbf{x},t_k\right)\models \mu \iff g_{\mu }\left(\mathbf{x}\left(t_k\right)\right)\ge 0,\\ \left(\mathbf{x},t_k\right)\models \neg \phi \iff \neg \left(\left(\mathbf{x},t_k\right)\models \phi \right),\\ \left(\mathbf{x},t_k\right)\models {\phi }_1\wedge {\phi }_2\iff \left(\mathbf{x},t_k\right)\models {\phi }_1\wedge \left(\mathbf{x},t_k\right)\models {\phi }_2,\\ \left(\mathbf{x},t_k\right)\models {\phi }_1{\mathrm{U}}_{\left[a,b\right]}{\phi }_2\iff \exists t_{k^{\prime }}\in \left[t_k+a,t_k+b\right]\mathrm{s}.\mathrm{t}.\\ \left(\mathbf{x},t_{k^{\prime }}\right)\models {\phi }_2\wedge \forall t_{k^{″}}\in \left[t_k,t_{k^{\prime }}\right],\\ \left(\mathbf{x},t_{k^{″}}\right)\models {\phi }_1\end{array}$

The signal x = x₀x₁… satisfies φ, denoted by x ⊨ φ if ( x , t₀) ⊨ φ. By using the “negation” operator ¬ and the “conjunction” operator ∧, we can define “disjunction” φ₁ ∨ φ₂ = ¬(¬φ₁ ∧¬φ₂). And by employing the until operator ${\mathrm{U}}_{\mathrm{I}}$ , we can define “eventually” ${\mathrm{F}}_{\mathrm{I}}\phi =\top {\mathrm{U}}_{\mathrm{I}}\phi$ and “always” ${\mathrm{G}}_{\mathrm{I}}\phi =\neg {\mathrm{F}}_{\mathrm{I}}\neg \phi$ .

Definition 2.3

(Dokhanchi et al., 2014) The time horizon ‖φ‖ of an STL formula φ is inductively defined as

$\Vert \phi \Vert =\{\begin{array}{ll}0,& if \phi =\mu ,\\ \Vert {\phi }_1\Vert ,& if \phi =\neg {\phi }_1,\\ \max \left\{\Vert {\phi }_1\Vert ,\Vert {\phi }_2\Vert \right\},& if \phi ={\phi }_1\wedge {\phi }_2,\\ b+\max \left\{\Vert {\phi }_1\Vert ,\Vert {\phi }_2\Vert \right\},& if \phi ={\phi }_1{\mathrm{U}}_{\left[a,b\right]}{\phi }_2.\end{array}$

Definition 2.4

(Robust satisfiability) Consider the uncertain system equation (1) and the STL formula φ. We say φ is robustly satisfiable from the initial state x₀ if there exists a control policy ν such that

${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi ,\forall \mathit{w}\in {\mathcal{W}}_{\ge 0}.$

Definition 2.5

(Satisfiability) Consider the deterministic system equation (2) and the STL formula φ. We say φ is satisfiable from the initial state x₀ if there exists a control policy ν such that

${\mathit{x}}_{x_0}^{\mathit{\nu }}\models \phi .$

Given an STL formula φ, the set of initial states from which φ is (robustly) satisfiable is denoted by

${\mathbb{S}}_{\phi }=\left\{x_0\in {\mathbb{R}}^n\mid \phi \text{is}\left(\text{robustly}\right)\text{satisfiable} \text{from} x_0\right\}.$

(4)

We remark that the computation of the set ${\mathbb{S}}_{\phi }$ is tailored to the dynamic system under consideration. Here we omit it for notation simplicity.

2.3. Reachability operators

In this section, we define two reachability operators. The natural connection between reachability and temporal operators plays an important role in the approach proposed in this paper. The definitions of maximal and minimal reachable tube are given as follows.

Definition 2.6

Consider system equation (1), three sets ${\mathrm{\Omega }}_1,{\mathrm{\Omega }}_2,\mathcal{C}\subseteq {\mathbb{R}}^n$ , and a time interval [a, b]. The maximal reachable tube from Ω₁ to Ω₂ is defined as

$\begin{array}{l}{\mathcal{R}}^M\left({\mathrm{\Omega }}_1,{\mathrm{\Omega }}_2,\mathcal{C},\left[a,b\right],k\right)\\ =\left\{x_k\in {\mathrm{\Omega }}_1|\begin{array}{l}\exists \mathit{\nu }\in {\mathcal{U}}_{\ge k},\forall \mathit{w}\in {\mathcal{W}}_{\ge k},\\ \exists t_{k^{\prime }}\in \left[\max \left\{a,t_k\right\},b\right],{\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{\prime }}\right)\in {\mathrm{\Omega }}_2,\\ \forall t_{k^{″}}\in \left[t_k,t_{k^{\prime }}\right],{\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{″}}\right)\in \mathcal{C}\end{array}\right\}\\ \text{and}{t}_k\in \left[0,b\right].\end{array}$

The set ${\mathcal{R}}^M\left({\mathrm{\Omega }}_1,{\mathrm{\Omega }}_2,\mathcal{C},\left[a,b\right],k\right)$ collects all states in Ω₁ at time t _k from which there exists a control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge k}$ that, despite the worst disturbance signals, drives the system to the target set Ω₂ at some time instant t_k′ ∈ [max{a, t _k }, b] while satisfying constraints defined by $\mathcal{C}$ prior to reaching the target.

Definition 2.7

Consider system equation (1), two sets ${\mathrm{\Omega }}_1,{\mathrm{\Omega }}_2\subseteq {\mathbb{R}}^n$ , and a time interval [a, b]. The minimal reachable tube from Ω₁ to Ω₂ is defined as

$\begin{array}{l}{\mathcal{R}}^m\left({\mathrm{\Omega }}_1,{\mathrm{\Omega }}_2,\left[a,b\right],k\right)\\ =\left\{x_k\in {\mathrm{\Omega }}_1|\begin{array}{l}\forall \mathit{\nu }\in {\mathcal{U}}_{\ge k},\exists \mathit{w}\in {\mathcal{W}}_{\ge k},\\ \exists t_{k^{\prime }}\in \left[\max \left\{a,t_k\right\},b\right],{\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{\prime }}\right)\in {\mathrm{\Omega }}_2\end{array}\right\},\\ \text{and}{t}_k\in \left[0,b\right].\end{array}$

The set ${\mathcal{R}}^m\left({\mathrm{\Omega }}_1,{\mathrm{\Omega }}_2,\left[a,b\right],k\right)$ collects all states in Ω₁ at time t _k from which no matter what control policy ν is applied, there exists a disturbance signal that drives the system to the target set Ω₂ at some time instant t_k′ ∈ [max{a, t _k }, b]. In this definition, the constraint set $\mathcal{C}$ is redundant. The reason is that the minimal reachable tube is used to build a connection with “always” operator ${\mathrm{G}}_{\left[a,b\right]}$ , for which the constraint set is not needed.

2.4. Problem formulation

Consider the following fragment of STL formulas, which is inductively defined as

$\phi ::=\top \mid \mu \mid \neg \mu \mid {\phi }_1\wedge {\phi }_2\mid {\phi }_1\vee {\phi }_2\mid \varphi {\mathrm{U}}_{\mathrm{I}}\phi \mid {\mathrm{F}}_{\mathrm{I}}\phi \mid {\mathrm{G}}_{\mathrm{I}}\varphi$

(5)

where ϕ⩴⊤∣μ∣¬μ∣ϕ₁ ∧ ϕ₂∣ϕ₁ ∨ ϕ₂. Here, ϕ₁, ϕ₂ are formulas of class ϕ and φ₁, φ₂ are formulas of class φ given in equation (5).

Remark 2.1

The STL fragment defined in equation (5) includes nested STL formulas of the form ${\mathrm{F}}_{\left[a_1,b_1\right]}{\mathrm{G}}_{\left[a_2,b_2\right]}\varphi$ and ${\varphi }_1{\mathrm{U}}_{\left[a_1,b_1\right]}\left({\mathrm{G}}_{\left[a_2,b_2\right]}{\varphi }_2\right)$ , while excluding nested STL formulas of the form ${\mathrm{G}}_{\left[a_1,b_1\right]}{\mathrm{F}}_{\left[a_2,b_2\right]}\varphi ,\left({\mathrm{G}}_{\left[a_1,b_1\right]}{\varphi }_1\right){\mathrm{U}}_{\left[a_2,b_2\right]}{\varphi }_2$ . The reason is that according to the semantics of STL, nested STL formulas like ${\mathrm{G}}_{\left[a_1,b_1\right]}{\mathrm{F}}_{\left[a_2,b_2\right]}\varphi$ and $\left({\mathrm{G}}_{\left[a_1,b_1\right]}{\varphi }_1\right){\mathrm{U}}_{\left[a_2,b_2\right]}{\varphi }_2$ require parallel monitoring of their arguments ${\mathrm{F}}_{\left[a_2,b_2\right]}\varphi$ and ${\mathrm{G}}_{\left[a_1,b_1\right]}{\varphi }_1$ within the encoded time intervals of the temporal operators ${\mathrm{G}}_{\left[a_1,b_1\right]}$ and ${\mathrm{U}}_{\left[a_2,b_2\right]}$ , respectively. Nevertheless, we note that the fragment equation (5) is more general than most of the fragments considered in the literature studying online control synthesis, for example, Lindemann and Dimarogonas (2018); Buyukkocak et al. (2022). Such a fragment equation (5) is expressive enough to specify a large number of robotic tasks, e.g., time-constrained reachability, supply-delivery, and safety.

Remark 2.2

It is possible to handle nested STL formulas of the form ${\mathrm{G}}_{\left[a_1,b_1\right]}{\mathrm{F}}_{\left[a_2,b_2\right]}\varphi$ and $\left({\mathrm{G}}_{\left[a_1,b_1\right]}{\varphi }_1\right){\mathrm{U}}_{\left[a_2,b_2\right]}{\varphi }_2$ using the framework proposed in this work. For the formula ${\mathrm{G}}_{\left[a_1,b_1\right]}{\mathrm{F}}_{\left[a_2,b_2\right]}\varphi$ , one can rewrite it as ${\mathrm{F}}_{\left[a_1+a_2,b_1+b_2\right]}{\mathrm{G}}_{\left[0,b_1-a_1\right]}\varphi$ . For the formula $\left({\mathrm{G}}_{\left[a_1,b_1\right]}{\varphi }_1\right){\mathrm{U}}_{\left[a_2,b_2\right]}{\varphi }_2$ , one can rewrite it as ${\mathrm{G}}_{\left[a_1,b_1+b_2\right]}{\varphi }_1\wedge {\mathrm{F}}_{\left[a_2,b_2\right]}{\varphi }_2$ . Since $\mathit{x}\models {\mathrm{F}}_{\left[a_1+a_2,b_1+b_2\right]}{\mathrm{G}}_{\left[0,b_1-a_1\right]}\varphi$ implies $\mathit{x}\models {\mathrm{G}}_{\left[a_1,b_1\right]}{\mathrm{F}}_{\left[a_2,b_2\right]}\varphi$ and $\mathit{x}\models {\mathrm{G}}_{\left[a_1,b_1+b_2\right]}{\varphi }_1\wedge {\mathrm{F}}_{\left[a_2,b_2\right]}{\varphi }_2$ implies $\mathit{x}\models \left({\mathrm{G}}_{\left[a_1,b_1\right]}{\varphi }_1\right){\mathrm{U}}_{\left[a_2,b_2\right]}{\varphi }_2$ , the soundness of the proposed online control synthesis algorithm preserves. However, we note that this approach introduces conservatism due to the fact that the rewritten formula is not equivalent to the original formula.

The problem under consideration is formulated as follows.

Problem 2.1

Online control synthesis. Consider system equation (1) and an STL task φ in equation (5). For an initial state x₀, find, if it exists, a sequence of control inputs ν = ν₀(x₀)ν₁(x₁)…ν _k (x _k )… such that the resulting trajectory x = x₀x₁…x _k … satisfies φ.

Remark 2.3

Note that the objective of Problem 2.1 is not to synthesize a closed-form control policy ν , which is in general computationally intractable for systems with continuous spaces. Instead, we aim at finding online a sequence of feedback control inputs in a way that is similar to receding horizon control.

The key idea to solve Problem 2.1 is as follows. We first transform the STL formula to an alternative tree-based representation, which we call a tube-based temporal logic tree (tTLT), by leveraging reachability analysis as detailed in Section 3. There exists a semantic connection between the STL formula and the corresponding tTLT, thanks to the reachability analysis, which is explained in Section 4. Based on this fact, we can perform control synthesis over the tTLT, instead of the STL formula. An online control synthesis algorithm is provided in Section 5.

3. Real-time STL semantics and tube-based temporal logic tree

In this section, a real-time version of STL semantics and a notion of tTLT are proposed. The real-time STL semantics establish the satisfaction relation between a real-time signal and the STL formula. Based on these real-time semantics, we propose the tTLT using the close connection between STL and reachability analysis.

3.1. Real-time STL semantics

The real-time STL semantics is defined to capture the satisfaction relation between a real-time signal and an STL formula, which is different from the traditional STL semantics defined in Section 2.2. Before proceeding, the following definition is required.

Definition 3.1

Suffix and Completions. Given a discrete-time signal x = x₀x₁…, we say that a partial signal $\mathit{s}=s_l{s}_{l+1}\dots ,l\mathbb{\in }\mathbb{N}$ , is a suffix of the signal x if ∀k′ ≥ l, s_k′ = x_k′. The set of completions of a partial signal s , denoted by C( s ), is given by

$C\left(\mathit{s}\right):=\left\{\mathit{x}:\mathit{s}\text{is} \mathrm{a} \text{suffix} \text{of}\mathit{x}\right\}.$

Given a time instant t _k and a time interval [a, b], define t _k + [a, b]≔[t _k + a, t _k + b]. The real-time STL semantics is defined as follows.

Definition 3.2

Let t _k be the starting time of any STL formula φ to be evaluated. Let t _l ≥ t _k be the starting time of a partial signal s = s _l s_l+1…. The real-time satisfaction of φ with respect to the partial signal s , denoted by ( s , t _k , t _l )∣≍φ, is recursively defined by equation (6).

$\begin{array}{lll}\left(\mathit{s},t_k,t_l\right)\mid \asymp \mu & \iff & g_{\mu }\left(\mathit{s}\left(t_k\right)\right)\ge 0,\hspace{1em}{t}_l=t_k;\end{array}$

(6a)

$\begin{array}{lll}\left(\mathit{s},t_k,t_l\right)\mid \asymp \neg \phi & \iff & \neg \left(\left(\mathit{s},t_k,t_l\right)\mid \asymp \phi \right),t_l\in t_k+\left[0,\Vert \phi \Vert \right];\end{array}$

(6b)

$\begin{array}{lll}\left(\mathit{s},t_k,t_l\right)\mid \asymp {\phi }_1\wedge {\phi }_2& \iff & \left(\mathit{s},t_k,t_l\right)\mid \asymp {\phi }_1\wedge \left(\mathit{s},t_k,t_l\right)\mid \asymp {\phi }_2,t_l\in t_k+\left[0,\Vert {\phi }_1\wedge {\phi }_2\Vert \right];\end{array}$

(6c)

$\begin{array}{l}\left(\mathit{s},t_k,t_l\right)\mid \asymp {\phi }_1{\mathrm{U}}_{\left[a,b\right]}{\phi }_2\hspace{0.5em}\iff \hspace{0.5em}\\ \{\begin{array}{ll}\exists t_{k^{\prime }}\in \left[\max \left\{t_k+a,t_l\right\},t_k+b\right]\mathrm{s}.\mathrm{t}.\left(\mathit{s},t_{k^{\prime }},t_l\right)\mid \asymp {\phi }_2,& \text{if}\Vert {\phi }_2\Vert =0,\\ \exists t_{k^{\prime }}\in \left[t_k+a,t_k+b\right]\mathrm{s}.\mathrm{t}.\left(\mathit{s},t_{k^{\prime }},t_l\right)\mid \asymp {\phi }_2,& \text{otherwise},\end{array}\\ \wedge \text{if}{t}_l\le t_{k^{\prime }},\forall t_{k^{″}}\in \left[t_l,t_{k^{\prime }}\right],\left(\mathit{s},t_{k^{″}},t_l\right)\mid \asymp {\phi }_1,t_l\in t_k+\left[0,\Vert {\phi }_1{\mathrm{U}}_{\left[a,b\right]}{\phi }_2\Vert \right].\end{array}$

(6d)

The real-time satisfaction relation ( s , t _k , t _l )∣ ≍ φ suggests that the partial signal s is the suffix of a satisfying trajectory that starts from t _k , i.e.,

$\left(\mathit{s},t_k,t_l\right)\mid \asymp \phi \Leftarrow \exists \mathit{x}\in C\left(\mathit{s}\right),\left(\mathit{x},t_k\right)\models \phi .$

Using the induction rule, one can define the real-time STL semantics for “disjunction” φ₁ ∨ φ₂, “eventually” ${\mathrm{F}}_{\left[a,b\right]}\phi$ , and “always” ${\mathrm{G}}_{\left[a,b\right]}\phi$ .

In parallel with Definitions 2.4 and 2.5, we define the STL satisfiability given a partial signal as follows.

Definition 3.3

Consider uncertain system equation (1) and the STL formula φ. We say φ is robustly satisfiable from the state x _k at time t _k if there exists a control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge k}$ such that

$\left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_0,t_k\right)\mid \asymp \phi ,\forall \mathit{w}\in {\mathcal{W}}_{\ge k}.$

Definition 3.4

Consider the deterministic system equation (2) and the STL formula φ. We say φ is satisfiable from the state x _k at time t _k if there exists a control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge k}$ such that

$\left({\mathit{x}}_{x_k}^{\mathit{\nu }},t_0,t_k\right)\mid \asymp \phi .$

Note that when t _k = t₀, Definitions 3.3 and 3.4 reduce to Definitions 2.4 and 2.5, respectively. Given an STL formula φ, the set of states from which φ is robustly satisfiable at t _k is denoted by

$\begin{array}{l}{\mathbb{S}}_{\phi }\left(t_k\right):=\{x_k\in {\mathbb{R}}^n\mid \phi \text{is}\left(\text{robustly}\right)\text{satisfiable}\\ \text{from} x_k \text{at} t_k\}.\end{array}$

(7)

Then, we have the following results.

Proposition 3.1

Consider system equation (1) and predicates μ₁, μ₂. Then, one has

i) ${\mathbb{S}}_{{\mu }_1{\mathrm{U}}_{\left[a,b\right]}{\mu }_2}\left(t_k\right)={\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{S}}_{{\mu }_2},{\mathbb{S}}_{{\mu }_1},\left[a,b\right],k\right)$ ;

ii) ${\mathbb{S}}_{{\mathrm{F}}_{\left[a,b\right]}{\mu }_1}\left(t_k\right)={\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{S}}_{{\mu }_1},{\mathbb{R}}^n,\left[a,b\right],k\right)$ ;

iii) ${\mathbb{S}}_{{\mathrm{G}}_{\left[a,b\right]}{\mu }_1}\left(t_k\right)=\overline{{\mathcal{R}}^m\left({\mathbb{R}}^n,\overline{{\mathbb{S}}_{{\mu }_1}},\left[a,b\right],k\right)}$ , where ${\mathbb{S}}_{{\mu }_1}$ and ${\mathbb{S}}_{{\mu }_2}$ are defined in equation (4).

Proof

First, we prove item i). Assume that $x_k\in {\mathbb{S}}_{{\mu }_1{\mathrm{U}}_{\left[a,b\right]}{\mu }_2}\left(t_k\right)$ . According to the real-time STL semantics, one has that $\exists \mathit{\nu }\in {\mathcal{U}}_{\ge k},\forall \mathit{w}\in {\mathcal{W}}_{\ge k}$ such that

• ∃t_k′ ∈ [max{a, t _k }, b],

$\left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_{k^{\prime }},t_k\right)\mid \asymp {\mu }_2\Rightarrow {\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{\prime }}\right)\in {\mathbb{S}}_{{\mu }_2},$

• • ∀t_k″ ∈ [t _k , t_k′],

$\left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_{k^{″}},t_k\right)\mid \asymp {\mu }_1\Rightarrow {\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{″}}\right)\in {\mathbb{S}}_{{\mu }_1}.$

That is, $x_k\in {\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{S}}_{{\mu }_2},{\mathbb{S}}_{{\phi }_1},\left[a,b\right],k\right)$ .

Now we assume that $x_k\in {\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{S}}_{{\mu }_2},{\mathbb{S}}_{{\mu }_1},\left[a,b\right],k\right)$ . According to Definition 2.6, one has that $\exists \mathit{\nu }\in {\mathcal{U}}_{\ge k},\forall \mathit{w}\in {\mathcal{W}}_{\ge k}$ such that $\exists t_{k^{\prime }}\in \left[\max \left\{a,t_k\right\},b\right],{\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{\prime }}\right)\in {\mathbb{S}}_{{\mu }_2}$ and $\forall t_{k^{″}}\in \left[t_k,t_{k^{\prime }}\right],{\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{″}}\right)\in {\mathbb{S}}_{{\mu }_1}$ . According to equation (7), one can further get that

$\begin{array}{l}{\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{\prime }}\right)\in {\mathbb{S}}_{{\mu }_1}\Rightarrow \left({\mathit{x}}_{x_k}^{\mathbf{\nu },\mathit{w}},t_{k^{\prime }},t_k\right)\mid \asymp {\mu }_1,\\ {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\left(t_{k^{″}}\right)\in {\mathbb{S}}_{{\mu }_2}\Rightarrow \left({\mathbf{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_{k^{″}},t_k\right)\mid \asymp {\mu }_2.\end{array}$

Therefore, $x_k\in {\mathbb{S}}_{{\mu }_1{\mathrm{U}}_{\left[a,b\right]}{\mu }_2}\left(t_k\right)$ .

The proof of item ii) is similar and hence omitted. Next, let us prove item iii).

Assume that $x_k\in {\mathbb{S}}_{{\mathrm{G}}_{\left[a,b\right]}{\mu }_1}\left(t_k\right)$ . According to the real-time STL semantics, one has that $\exists \mathit{\nu }\in {\mathcal{U}}_{\ge k},\forall \mathit{w}\in {\mathcal{W}}_{\ge k}$ such that ∀t_k′ ∈ [max{a, t _k }, b],

$\left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_{k^{\prime }},t_k\right)\mid \asymp {\mu }_1\Rightarrow {\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}}\left(t_{k^{″}}\right)\in {\mathbb{S}}_{{\mu }_1}.$

According to Definition 2.7, ${\mathcal{R}}^m\left({\mathbb{R}}^n,\overline{{\mathbb{S}}_{{\mu }_1}},\left[a,b\right],k\right)$ collects all states in ${\mathbb{R}}^n$ at time t _k from which no matter what control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge k}$ is applied, there exists a disturbance signal $\mathit{w}\in {\mathcal{W}}_{\ge k}$ that drives the system to the set $\overline{{\mathbb{S}}_{{\mu }_1}}$ at some time instant t_k′ ∈ [max{a, t _k }, b]. Therefore, $x_k\in \overline{{\mathcal{R}}^m\left({\mathbb{R}}^n,\overline{{\mathbb{S}}_{{\mu }_1}},\left[a,b\right],k\right)}$ . The other side can be proved similarly. □

In item iii) of Proposition 3.1, the use of the complementary set is motivated by the fact that ${\mathrm{G}}_{\left[a,b\right]}\mu =\neg {\mathrm{F}}_{\left[a,b\right]}\left(\neg \mu \right)$ and ${\mathbb{S}}_{\neg \mu }=\overline{{\mathbb{S}}_{\mu }}$ .

Proposition 3.2

Consider system equation (1) and STL formulas φ₁, φ₂. If φ₁ and φ₂ contain no logical operators ∧ and ∨, then one has

i) ${\mathbb{S}}_{{\phi }_1\wedge {\phi }_2}\left(t_k\right)\subseteq {\mathbb{S}}_{{\phi }_1}\left(t_k\right)\cap {\mathbb{S}}_{{\phi }_2}\left(t_k\right)$ ;

ii) ${\mathbb{S}}_{{\phi }_1\vee {\phi }_2}\left(t_k\right)\supseteq {\mathbb{S}}_{{\phi }_1}\left(t_k\right)\cup {\mathbb{S}}_{{\phi }_2}\left(t_k\right)$ ;

where ${\mathbb{S}}_{{\phi }_1}\left(t_k\right)$ and ${\mathbb{S}}_{{\phi }_2}\left(t_k\right)$ are defined in equation (7).

Proof

Assume that $x_k\in {\mathbb{S}}_{{\phi }_1\wedge {\phi }_2}\left(t_k\right)$ . According to Definition 3.2 and equation (7), one has that there exists a control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge k}$ such that

$\begin{array}{l}\left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_0,t_k\right)\mid \asymp {\phi }_1,\forall \mathit{w}\in {\mathcal{W}}_{\ge k}\\ \wedge \left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_0,t_k\right)\mid \asymp {\phi }_2,\forall \mathit{w}\in {\mathcal{W}}_{\ge k}.\end{array}$

That is, $x_k\in {\mathbb{S}}_{{\phi }_1}\left(t_k\right),x_k\in {\mathbb{S}}_{{\phi }_2}\left(t_k\right)$ . Thus, $x_k\in {\mathbb{S}}_{{\phi }_1\wedge {\phi }_2}\left(t_k\right)\Rightarrow x_k\in {\mathbb{S}}_{{\phi }_1}\left(t_k\right)\cap {\mathbb{S}}_{{\phi }_2}\left(t_k\right)$ . The other direction may not hold because it could happen that for a state x _k , there exist two control policies ${\mathit{\nu }}_1,{\mathit{\nu }}_2\in {\mathcal{U}}_{\ge k}$ such that $\left({\mathit{x}}_{x_k}^{{\mathit{\nu }}_1,\mathit{w}},t_0,t_k\right)\mid \asymp {\phi }_1,\left({\mathit{x}}_{x_k}^{{\mathit{\nu }}_2,\mathbf{w}},t_0,t_k\right)\mid \asymp {\phi }_2,\forall \mathit{w}\in {\mathcal{W}}_{\ge k}$ (i.e., $x_k\in {\mathbb{S}}_{{\phi }_1}\left(t_k\right)\cap {\mathbb{S}}_{{\phi }_2}\left(t_k\right)$ ). However, there is no control policy which ensures the robust satisfaction of φ₁ ∧ φ₂ at t _k .

Assume now that $x_k\in {\mathbb{S}}_{{\phi }_1}\left(t_k\right)$ , then one has that there exists a control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge k}$ such that $\left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_0,t_k\right)\mid \asymp {\phi }_1,\forall \mathit{w}\in {\mathcal{W}}_{\ge k}$ . Moreover, according to STL syntax, one further has $\left({\mathit{x}}_{x_k}^{\mathit{\nu },\mathit{w}},t_0,t_k\right)\mid \asymp {\phi }_1\vee {\phi }_2,\forall \mathit{w}\in {\mathcal{W}}_{\ge k}$ . That is, $x_k\in {\mathbb{S}}_{{\phi }_1}\left(t_k\right)\Rightarrow x_k\in {\mathbb{S}}_{{\phi }_1\vee {\phi }_2}\left(t_k\right)$ . Similarly, one can also get $x_k\in {\mathbb{S}}_{{\phi }_2}\left(t_k\right)\Rightarrow x_k\in {\mathbb{S}}_{{\phi }_1\vee {\phi }_2}\left(t_k\right)$ . Therefore, $x_k\in {\mathbb{S}}_{{\phi }_1}\left(t_k\right)\cup {\mathbb{S}}_{{\phi }_2}\left(t_k\right)\Rightarrow x_k\in {\mathbb{S}}_{{\phi }_1\vee {\phi }_2}\left(t_k\right)$ . The other direction may not hold because it could happen that there exists no state such that either φ₁ or φ₂ is robustly satisfiable from at t _k , i.e., ${\mathbb{S}}_{{\phi }_1}\left(t_k\right)=\varnothing$ , ${\mathbb{S}}_{{\phi }_2}\left(t_k\right)=\varnothing$ and thus ${\mathbb{S}}_{{\phi }_1}\left(t_k\right)\cup {\mathbb{S}}_{{\phi }_2}\left(t_k\right)=\varnothing$ . However, there exists a state $x_k^{*}$ from which there exists a control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge k}$ such that

$\begin{array}{l}\left({\mathit{x}}_{x_k^{*}}^{\mathit{\nu },{\mathit{w}}_1},t_0,t_k\right)\mid \asymp {\phi }_1,\forall {\mathit{w}}_1\in {\mathcal{W}}_1\\ \wedge \left({\mathit{x}}_{x_k^{*}}^{\mathit{\nu },{\mathit{w}}_2},t_0,t_k\right)\mid \asymp {\phi }_2,\forall {\mathit{w}}_2\in {\mathcal{W}}_{\ge k}\setminus {\mathcal{W}}_1\end{array}$

where ${\mathcal{W}}_1\subset {\mathcal{W}}_{\ge k}$ . In this case, one has $x_k^{*}\in {\mathbb{S}}_{{\phi }_1\vee {\phi }_2}\left(t_k\right)$ . □

Propositions 3.1 and 3.2 imply that the real-time satisfiable set of the STL formula can be inferred by set operations and reachability analysis, which makes it reasonable to develop the tTLT, a tree structure consisting of reachable tubes and operators. In the following section, we will detail the definition of tTLT and how to construct a tTLT from a given STL formula using reachability analysis.

3.2. Tube-based temporal logic tree and its construction

In this section, we formally introduce the notion of tTLT and provide its construction algorithm. A tTLT is a variant of the TLT proposed in the recent work (Gao et al., 2022) for LTL formulas. Due to the time-dependent essence of STL formulas, the reachable sets in the TLT are replaced with the reachable tubes in the tTLT, which can explicitly incorporate the time constraints in STL formulas. The intuition of the tTLT is that it indicates how a state trajectory should evolve in order to satisfy the time constraints embedded in an STL formula. In the following, a formal definition of the tTLT is introduced.

Definition 3.5

A tTLT is a tree for which the following holds:

• each node is either a tube node that maps from the nonnegative time axis, i.e., ${\mathbb{R}}_{\ge 0}$ , to a subset of ${\mathbb{R}}^n$ , or an operator node that belongs to $\left\{\wedge ,\vee ,{\mathrm{U}}_{\mathrm{I}},{\mathrm{F}}_{\mathrm{I}},{\mathrm{G}}_{\mathrm{I}}\right\}$ ;

• the root node and the leaf nodes are tube nodes;

• if a tube node is not a leaf node, its unique child is an operator node;

• the children of any operator node are tube nodes.

Definition 3.6

A complete path p of a tTLT is a path that starts from the root node and ends at a leaf node.

The following result shows how to construct a tTLT for any given STL formula using reachability analysis.

Theorem 3.1

For system equation (1) and every STL formula φ in equation (3), a tTLT, denoted by ${\mathcal{T}}_{\phi }$ , can be constructed from φ through the reachability operators ${\mathcal{R}}^M$ and ${\mathcal{R}}^m$ .

Proof

We follow three steps to construct a tTLT.

Step 1

Rewrite the STL formula φ into the equivalent positive normal form (PNF). It has been proven in Sadraddini and Belta (2015) that each STL formula has an equivalent STL formula in PNF (i.e., negations only occur adjacent to predicates), which can be inductively defined as

$\begin{array}{l}\phi ::=\top \mid \mu \mid \neg \mu \mid {\phi }_1\wedge {\phi }_2\mid {\phi }_1\vee {\phi }_2\\ \mid {\phi }_1{\mathrm{U}}_{\mathrm{I}}{\phi }_2\mid {\mathrm{F}}_{\mathrm{I}}{\phi }_1\mid {\mathrm{G}}_{\mathrm{I}}{\phi }_1\end{array}$

Step 2

For each predicate μ or its negation ¬μ, construct the tTLT with only one tube node ${\mathbb{S}}_{\mu }=\left\{x:g_{\mu }\left(x\right)\ge 0\right\}$ or $\overline{{\mathbb{S}}_{\mu }}$ . The tTLT of ⊤ or ⊥ has only one tube node, which is ${\mathbb{R}}^n$ or ∅.

Step 3

Following the induction rule to construct the tTLT ${\mathcal{T}}_{\phi }$ . More specifically, we will show that given STL formulas φ₁ and φ₂, if the tTLTs can be constructed from φ₁ and φ₂, then the tTLTs can be constructed from φ₁ ∧ φ₂, φ₁ ∨ φ₂, ${\phi }_1{\mathrm{U}}_{\left[a,b\right]}{\phi }_2$ , ${\mathrm{F}}_{\left[a,b\right]}{\phi }_1$ , and ${\mathrm{G}}_{\left[a,b\right]}{\phi }_1$ .

Case 1

Boolean operators ∧ and ∨. Consider two STL formulas φ ₁ , φ ₂ and their corresponding tTLTs ${\mathcal{T}}_{{\phi }_1},{\mathcal{T}}_{{\phi }_2}$ . The root nodes of ${\mathcal{T}}_{{\phi }_1}$ and ${\mathcal{T}}_{{\phi }_2}$ are denoted by ${\mathbb{X}}_{{\phi }_1}\left(t_k\right)$ and ${\mathbb{X}}_{{\phi }_2}\left(t_k\right)$ , respectively. The tTLT ${\mathcal{T}}_{{\phi }_1\wedge {\phi }_2}$ $\left({\mathcal{T}}_{{\phi }_1\vee {\phi }_2}\right)$ can be constructed by connecting ${\mathbb{X}}_{{\phi }_1}\left(t_k\right)$ and ${\mathbb{X}}_{{\phi }_2}\left(t_k\right)$ through the operator node ∧ (∨) and taking the intersection (or union) of the two root nodes, i.e., ${\mathbb{X}}_{{\phi }_1}\left(t_k\right)\cap {\mathbb{X}}_{{\phi }_2}\left(t_k\right)$ $\left({\mathbb{X}}_{{\phi }_1}\left(t_k\right)\cup {\mathbb{X}}_{{\phi }_2}\left(t_k\right)\right)$ , to be the root node. An illustrative diagram for φ ₁ ∧ φ ₂ is given in Figure 2 .

Figure 2.

Illustrative diagram of construction tTLT for φ ₁ ∧ φ ₂ .

Case 2

Until operator $U_{\left[a,b\right]}$ . Consider two STL formulas φ ₁ , φ ₂ and their corresponding tTLTs ${\mathcal{T}}_{{\phi }_1},{\mathcal{T}}_{{\phi }_2}$ . The root nodes of ${\mathcal{T}}_{{\phi }_1}$ and ${\mathcal{T}}_{{\phi }_2}$ are denoted by ${\mathbb{X}}_{{\phi }_1}\left(t_k\right)$ and ${\mathbb{X}}_{{\phi }_2}\left(t_k\right)$ , respectively. In addition, the leaf nodes of ${\mathcal{T}}_{{\phi }_1}$ are denoted by ${\mathbb{Y}}_{{\phi }_1}^1\left(t_k\right),\dots ,{\mathbb{Y}}_{{\phi }_1}^N\left(t_k\right)$ , where N is the total number of leaf nodes of ${\mathcal{T}}_{{\phi }_1}$ . The tTLT ${\mathcal{T}}_{{\phi }_1{U}_{\left[a,b\right]}{\phi }_2}$ can be constructed by the following steps: 1) replace each leaf node ${\mathbb{Y}}_{{\phi }_1}^i\left(t_k\right)$ by ${\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{X}}_{{\phi }_2}\left(t_0\right),{\mathbb{Y}}_{{\phi }_1}^i\left(t_0\right),\left[a,b\right],k\right)$ ; 2) update ${\mathcal{T}}_{{\phi }_1}$ from the leaf nodes to the root node with the new leaf nodes; and 3) connect each leaf node of the updated ${\mathcal{T}}_{{\phi }_1}$ and the root node of ${\mathcal{T}}_{{\phi }_2}$ , i.e., ${\mathbb{X}}_{{\phi }_2}\left(t_k\right)$ , with the operator node U_[a,b] One illustrative diagram for $U_{\left[a,b\right]}$ is given in Figure 3 .

Figure 3.

Illustrative diagram of construction tTLT for ${\phi }_1{U}_{\left[a,b\right]}{\phi }_2$ .

Case 3

Eventually and always operators $F_{\left[a,b\right]}$ and $G_{\left[a,b\right]}$ . Consider an STL formula φ ₁ and its corresponding tTLT ${\mathcal{T}}_{{\phi }_1}$ . The root node of ${\mathcal{T}}_{{\phi }_1}$ is given by ${\mathbb{X}}_{{\phi }_1}\left(t_k\right)$ . The tTLT ${\mathcal{T}}_{F_{\left[a,b\right]}{\phi }_1}$ $\left({\mathcal{T}}_{G_{\left[a,b\right]}{\phi }_1}\right)$ can be constructed by connecting ${\mathbb{X}}_{{\phi }_1}\left(t_k\right)$ through the operator $F_{\left[a,b\right]}$ $\left(G_{\left[a,b\right]}\right)$ and making the tube ${\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{X}}_{{\phi }_1}\left(t_0\right),{\mathbb{R}}^n,\left[a,b\right],k\right)$ $\left(\overline{{\mathcal{R}}^m\left({\mathbb{R}}^n,\overline{{\mathbb{X}}_{{\phi }_1}\left(t_0\right)},\left[a,b\right],k\right)}\right)$ the root node. An illustrative diagram for $G_{\left[a,b\right]}$ is given in Figure 4. □

Based on Theorem 3.1, Algorithm 1 is designed for the construction of tTLT ${\mathcal{T}}_{\mathrm{\phi }}$ . It takes the syntax tree of the STL formula φ as input. For an STL formula, the nodes of its syntax tree are either predicate or operator nodes. More specifically, all the leaf nodes are predicates and all other nodes are operators.

Algorithm 1. tTLTConstruction.

Let us use the following example to show how to construct the tTLT.

Figure 4.

Illustrative diagram of construction tTLT for $G_{\left[a,b\right]}{\phi }_1$ .

Example 3.1

Consider the formula $\phi =F_{\left[a_1,b_1\right]}{G}_{\left[a_2,b_2\right]}{\mu }_1\wedge {\mu }_2{U}_{\left[a_3,b_3\right]}{\mu }_3$ , where μ _i , i = {1, 2, 3} are predicates. The syntax tree of φ is shown on the left-hand side of Figure 5 . The corresponding tTLT for φ (constructed using Algorithm 1) is shown on the right-hand side of Figure 5 , where

$\begin{array}{l}{\mathbb{X}}_4\left(t_k\right)=\overline{{\mathcal{R}}^m\left({\mathbb{R}}^n,\overline{{\mathbb{S}}_{{\mu }_1}},\left[a_2,b_2\right],k\right)},\\ {\mathbb{X}}_3\left(t_k\right)={\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{S}}_{{\mu }_3},{\mathbb{S}}_{{\mu }_2},\left[a_3,b_3\right],k\right),\\ {\mathbb{X}}_2\left(t_k\right)={\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{X}}_4\left(t_0\right),{\mathbb{R}}^n,\left[a_1,b_1\right],k\right),\\ {\mathbb{X}}_1\left(t_k\right)={\mathbb{X}}_2\left(t_k\right)\cap {\mathbb{X}}_3\left(t_k\right)\end{array}$

Figure 5.

Example 3.1: syntax tree (left) and tTLT (right) for $\phi =F_{\left[a_1,b_1\right]}{G}_{\left[a_2,b_2\right]}{\mu }_1\wedge {\mu }_2{U}_{\left[a_3,b_3\right]}{\mu }_3$ . Recall that $F_{\left[a,b\right]}\phi =\top U_{\left[a,b\right]}\phi$ .

Remark 3.1

Given an STL formula φ in PNF, let K denote the number of Boolean operators and L the number of temporal operators contained in φ. Let ${\mathcal{T}}_{\phi }$ be the tTLT corresponding to φ. Then, ${\mathcal{T}}_{\phi }$ has at most 2K complete paths. In addition, each complete path has at most 2(K + L) + 1 nodes, out of which at most K + L are non-root tube nodes. Thus, one can conclude that ${\mathcal{T}}_{\phi }$ contains at most 4K(K + L) + 1 nodes, out of which at most 2K(K + L) + 1 are tube nodes.

4. Semantic connection between STL and tTLT

In this section, the semantic connection between an STL formula and its corresponding tTLT is derived. We define how a given state trajectory satisfies a tTLT and then show that the tTLT is a semantic under-approximation of the STL formula. Before that, let us first define the segment of the complete path.

Definition 4.1

A complete path of a tTLT can be encoded in the form of $\mathit{p}={\mathbb{X}}_0{\Theta }_1{\mathbb{X}}_1{\Theta }_2\dots {\Theta }_{N_f}{\mathbb{X}}_{N_f}$ , where N _f is the number of operator nodes contained in the complete path, ${\mathbb{X}}_i:{\mathbb{R}}_{\ge 0}\to 2^{{\mathbb{R}}^n},\forall i\in \left\{\mathrm{0,1},\dots ,N_f\right\}$ represent tube nodes, and ${\Theta }_j\in \left\{\wedge ,\vee ,U_I,F_I,G_I\right\},\forall j\in \left\{1,\dots ,N_f\right\}$ represent operator nodes. Any subsequence of a complete path is called a segment of the complete path.

Now, we define the maximal temporal segment for a tTLT, which plays an important role when simplifying the tTLT.

Definition 4.2

A maximal temporal segment (MTS) of a complete path of the tTLT is one of the following types of segment:

1) a segment from the root node to the parent of the first Boolean operator node (∧ or ∨);

2) a segment from one child of one Boolean operator node to the parent of the next Boolean operator node;

3) a segment from one child of the last Boolean operator node to the leaf node.

One can conclude from Definition 4.2 that any MTS starts and ends with a tube node and contains no Boolean operator nodes.

Definition 4.3

A time coding of (a complete path of) the tTLT is an assignment of each tube node ${\mathbb{X}}_i$ of (the complete path of) the tTLT an activation time instant $t_{{\kappa }_i},{\kappa }_i\mathbb{\in }\mathbb{N}$ .

Now, we further define the satisfaction relation between a trajectory x and a complete path of the tTLT.

Definition 4.4

Consider a trajectory x ≔x ₀ x ₁ … and a complete path $\mathit{p}={\mathbb{X}}_0{\Theta }_1{\mathbb{X}}_1{\Theta }_2\dots {\Theta }_{N_f}{\mathbb{X}}_{N_f}$ . We say x satisfies p , denoted by x ⊨ p , if there exists a time coding for p such that

i) if Θ _i ∈ {∧, ∨}, then $t_{{\kappa }_i}=t_{{\kappa }_{i-1}}$ ;

ii) if ${\Theta }_i=U_I$ , then $t_{{\kappa }_i}\in t_{{\kappa }_{i-1}}+I$ ;

iii) if ${\Theta }_i=G_I$ , then $t_{{\kappa }_i}=\underset{t_k}{\mathit{argmax}}\left\{t_k\in t_{{\kappa }_{i-1}}+I\right\}$ ;

and

iv) $x_k\in {\mathbb{X}}_i\left(t_{k-{\kappa }_i}\right),\forall k\in \left[{\kappa }_i,{\kappa }_{i+1}\right],i=0,\dots ,N_f-1$ ;

v) $x_{{\kappa }_{N_f}}\in {\mathbb{X}}_{N_f}\left(t_0\right)$ .

Remark 4.1

From items i)-iii) of Definition 4.4, one has that $t_{{\kappa }_0}\le t_{{\kappa }_1}\le \cdots \le t_{{\kappa }_{N_f}}$ . This means that if a trajectory x ⊨ p , it must visit each tube node ${\mathbb{X}}_i$ of the complete path p sequentially. In addition, we can further conclude from items iv)-v) that the trajectory x has to stay in each tube node ${\mathbb{X}}_i$ for sufficiently long time steps.

With Definition 4.4, the satisfaction relation between a trajectory x and a tTLT ${\mathbb{X}}_i$ can be defined as follows.

Definition 4.5

Consider a trajectory x and a tTLT ${\mathcal{T}}_{\phi }$ . We say x satisfies ${\mathcal{T}}_{\phi }$ , denoted by $\mathit{x}\models {\mathcal{T}}_{\phi }$ , if there exists a time coding $\left\{t_{{\kappa }_i}\right\}$ for ${\mathcal{T}}_{\phi }$ such that the output of Algorithm 2 is true.

The central idea of Algorithm 2 is to check the Boolean relation among sub-formulas of a given STL formula φ. For instance, assume $\phi ={\wedge }_{i=1}^n{\phi }_i$ , where each φ _i , ∀i = 1, …, n contains no Boolean operators. Then one can get from Algorithm 1 that ${\mathcal{T}}_{\phi }$ has n complete paths p _i , i = 1, …, n, and each p _i corresponds to a sub-formula φ _i . Then Algorithm 2 dictates that $\mathit{x}\models {\mathcal{T}}_{\phi }$ if and only if x satisfies every complete path of ${\mathcal{T}}_{\phi }$ . Assume now that $\phi ={\vee }_{i=1}^n{\phi }_i$ , then Algorithm 2 dictates that $\mathit{x}\models {\mathcal{T}}_{\phi }$ if and only if x satisfies at least one complete path of ${\mathcal{T}}_{\phi }$ .

Algorithm 2. tTLTSatisfaction.

Algorithm 2 takes as inputs a trajectory x , a tTLT ${\mathcal{T}}_{\phi }$ , and a time coding $\left\{t_{{\kappa }_i}\right\}$ , and outputs true or false. It works as follows. Given a tTLT ${\mathcal{T}}_{\phi }$ , we first compress it via Algorithm 3 (line 1), in this way the resulting compressed tree ${\mathcal{T}}_{\phi }^c$ contains only Boolean operator nodes and tube nodes. Then for each complete path p of ${\mathcal{T}}_{\phi }$ , if x ⊧ p , one sets the corresponding leaf node of p in ${\mathcal{T}}_{\phi }^c$ (note that ${\mathcal{T}}_{\phi }^c$ and ${\mathcal{T}}_{\phi }$ have the same set of leaf nodes) with true. Otherwise, one sets the corresponding leaf node of p in ${\mathcal{T}}_{\phi }^c$ with false (lines 2-8). After that, we set all the non-leaf tube nodes of ${\mathcal{T}}_{\phi }^c$ with false (line 9) and the resulting tree becomes a Boolean tree (a tree with Boolean operator and Boolean variable nodes). Finally, we backtrack the Boolean tree ${\mathcal{T}}_{\phi }^c$ using Algorithm 4, and return the root node (lines 10-11).

We further detail the Compression algorithm (Algorithm 3) and the Backtracking algorithm (Algorithm 4) in the following. Algorithm 3 aims at obtaining a simplified tree with Boolean operator nodes and tube nodes only. To do so, we first encode each MTS in the form of ${\mathbb{X}}_1{\mathrm{\Theta }}_1\dots {\mathrm{\Theta }}_{{\mathrm{N}}_{\mathrm{f}}-1}{\mathbb{X}}_{{\mathrm{N}}_{\mathrm{f}}}$ (line 3), and then replace it with one tube node (line 4). Algorithm 4 takes the compressed tree ${\mathcal{T}}_{\mathrm{\phi }}^{\mathrm{c}}$ as an input, and then update the parent of each Boolean operator node through a bottom-up traversal. In Algorithm 4, PA(Θ) and CH₁(Θ), CH₂(Θ) represent the parent node and the two children of the Boolean operator node Θ ∈ {∧, ∨}, respectively.

Algorithm 3. Compression.

Algorithm 4. Backtracking.

Example 4.1

Let us continue with Example 3.1. The tTLT ${\mathcal{T}}_{\phi }$ (right of Figure 5 ) contains 2 complete paths, i.e.,

${\mathit{p}}_1:={\mathbb{X}}_1\wedge {\mathbb{X}}_2{U}_{\left[a_1,b_1\right]}{\mathbb{X}}_4{G}_{\left[a_2,b_2\right]}{\mathbb{S}}_{{\mu }_1}$

And

${\mathit{p}}_2:={\mathbb{X}}_1\wedge {\mathbb{X}}_3{U}_{\left[a_3,b_3\right]}{\mathbb{S}}_{{\mu }_3}$

Let

$\left\{t_{{\kappa }_1},t_{{\kappa }_2},t_{{\kappa }_4},t_{{\kappa }_5}\right\}$

Be the time coding of the complete path p ₁ , where $t_{{\kappa }_1},t_{{\kappa }_2},t_{{\kappa }_4}$ , and $t_{{\kappa }_5}$ are the activation time instants of the tube nodes ${\mathbb{X}}_1,{\mathbb{X}}_2,{\mathbb{X}}_4$ , and ${\mathbb{X}}_5:={\mathbb{S}}_{{\mu }_1}$ , respectively. Then, we have according to Definition 4.4 that a trajectory x ⊨ p ₁ if i) $t_{{\kappa }_1}=t_{{\kappa }_2}$ ; ii) $t_{{\kappa }_4}\in t_{{\kappa }_2}+\left[a_1,b_1\right]$ ; iii) $t_{{\kappa }_4}\in t_{{\kappa }_2}+\left[a_1,b_1\right]$ ; iv) $x_0\in {\mathbb{X}}_1\left(t_0\right)$ , $x_k\in {\mathbb{X}}_2\left(t_{k-{\kappa }_2}\right),\forall k\in \left[{\kappa }_2,{\kappa }_4\right]$ , $x_k\in {\mathbb{X}}_4\left(t_{k-{\kappa }_4}\right),\forall k\in \left[{\kappa }_4,{\kappa }_5\right]$ , and v) $x_{{\kappa }_5}\in {\mathbb{X}}_5$ .

In addition, the tTLT ${\mathcal{T}}_{\phi }$ contains 3 MTSs, i.e., ${\mathbb{X}}_1$ , ${\mathbb{X}}_2{U}_{\left[a_1,b_1\right]}{\mathbb{X}}_4{G}_{\left[a_2,b_2\right]}{\mathbb{S}}_{{\mu }_1}$ , and ${\mathbb{X}}_3{U}_{\left[a_3,b_3\right]}{\mathbb{S}}_{{\mu }_3}$ . The compressed tree ${\mathcal{T}}_{\phi }^c$ is shown in Figure 6 . If a trajectory x satisfies both of the complete paths p ₁ and p ₂ , the output of Algorithm 2 is true, otherwise, the output is false.

Figure 6.

Example 4.1: compressed tree ${\mathcal{T}}_{\phi }^c$ , where ${\mathcal{T}}_{\phi }$ is plotted in Figure 5.

Definition 4.6

(Robustly satisfiable tTLT) A tTLT is called robustly satisfiable for system equation (1) with initial state x ₀ if there exists a control policy $\mathit{\nu }\in {\mathcal{U}}_{\ge 0}$ such that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi },\forall \mathit{w}\in {\mathcal{W}}_{\ge 0}$ .

The following theorem provides a formally semantic relation between the STL formula fragment in equation (5) and the corresponding tTLTs.

Theorem 4.1

Consider the uncertain system equation (1) with initial state x ₀ and an STL formula φ in equation (5). Let ${\mathcal{T}}_{\phi }$ be the tTLT corresponding to φ. Then, φ is robustly satisfiable for equation (1) if ${\mathcal{T}}_{\phi }$ is robustly satisfiable for equation (1).

Proof

From Definitions 2.4 and 4.6, one has that to prove Theorem 4.1, it is equivalent to prove ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi },\forall \mathit{w}\in {\mathcal{W}}_{\ge 0}\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi ,\forall \mathit{w}\in {\mathcal{W}}_{\ge 0}$ . Given one instance of disturbance signal w , if one has ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ , then it implies ${\mathit{x}}_{x_0}^{\mathit{\nu }}\models {\mathcal{T}}_{\phi },\forall \mathit{w}\in {\mathcal{W}}_{\ge 0}\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi ,\forall \mathit{w}\in {\mathcal{W}}_{\ge 0}$ . Therefore, it is sufficient to prove ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ .

In the following, we will first prove ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\iff {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ for

i) ⊤, predicates μ, ¬μ, and μ ₁ ∧ μ ₂ , μ ₁ ∨ μ ₂ ,

ii) ${\mu }_1{\mathrm{U}}_{\left[a,b\right]}{\mu }_2$ , ${\mathrm{F}}_{\left[a,b\right]}{\mu }_1$ , and ${\mathrm{G}}_{\left[a,b\right]}{\mu }_1$ ;

iii) ${{\mu }_1\mathrm{U}}_{\left[a_1,b_1\right]}{\mathrm{G}}_{\left[a_2,b_2\right]}{\mu }_2$ and ${\mathrm{F}}_{\left[a_1,b_1\right]}{\mathrm{G}}_{\left[a_2,b_2\right]}{\mu }_1$ ;

iv) ${\phi }_1\wedge {\phi }_2$ ;

where φ₁ and φ₂ in item iv) are STL formulas belong to items ii) or iii).

Case i): For ⊤, predicates μ, ¬μ, and μ ₁ ∧ μ ₂ , μ ₁ ∨ μ ₂ , it is trivial to verify that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\iff {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ .

Case ii): We note that the proofs of the three are similar, therefore, in the following, we only consider the case $\phi ={\mu }_1{U}_{\left[a,b\right]}{\mu }_2$ . The tTLT $S_j\left(t_k\right)=Post\left(S_i\left(t_k\right)\right)$ can be constructed via Algorithm 1, which is shown in Figure 7.

Assume that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }$ , then one has from Definition 4.4 that $\exists t_{{\kappa }_1}\in t_0+\left[a,b\right],x_{{\kappa }_1}\in {\mathbb{S}}_{{\mu }_2}$ and $\forall k\in \left[0,{\kappa }_1\right],x_k\in {\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{S}}_{{\mu }_2},{\mathbb{S}}_{{\mu }_1},\left[a,b\right],k\right)\subseteq {\mathbb{S}}_{{\mu }_1}$ , which implies ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ . That is, $\mathbb{U}\left(x_k,t_k\right)$ . Assume now that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ . Then, one has from STL semantics that i) $\exists t_{k^{\prime }}\in t_0+\left[a,b\right],x_{k^{\prime }}\in {\mathbb{S}}_{{\phi }_2}$ and ii) $\forall t_{k^{″}}\in \left[t_0,t_{k^{\prime }}\right],x_{k^{″}}\in {\mathbb{S}}_{{\phi }_1}$ . Moreover, from Definition 2.6, one has that i) and ii) together implies $\forall t_{k^{″}}\in \left[t_0,t_{k^{\prime }}\right],x_{k^{″}}\in {\mathcal{R}}^M\left({\mathbb{R}}^n,{\mathbb{S}}_{{\mu }_2},{\mathbb{S}}_{{\mu }_1},\left[a,b\right],k^{″}\right)$ . Therefore, ${\mathcal{T}}_u^c\left(t_k\right)$ .

Case iii): We note that the proofs of the two are similar. In the following, we consider the case $\mathit{min} \backslash nolimits\_{\nu }_k\mathbb{\in }\mathbb{U}\left(x_k,t_k\right)\left\{\Vert {\nu }_k\Vert \right\}$ . The tTLT $Post\left(B\left(x_k,t_k\right)\right)$ can be constructed via Algorithm 1, which is shown in Figure 8.

Assume that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }$ , then one has from Definition 4.4 that $Post\left(B\left(x_k,t_k\right)\right)$ . In addition, $\forall k\in \left[{\kappa }_1,{\kappa }_2\right],x_k\in \overline{{\mathcal{R}}^m\left({\mathbb{R}}^n,\overline{{\mathbb{S}}_{{\mu }_1}},\left[a_2,b_2\right],k-{\kappa }_1\right)}$ , which implies $x_k\in {\mathbb{S}}_{{\mu }_1},\forall k\in \left[{\kappa }_1,{\kappa }_2\right]$ . That is, ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi \Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu }}\models {\mathcal{T}}_{\phi }$ . Assume now that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ . Then, one has from STL semantics that ∃t _k′ ∈ t ₀ + [a ₁ , b ₁ ] such that $x_{k^{″}}\in {\mathbb{S}}_{{\mu }_1},\forall t_{k^{″}}\in t_{k^{\prime }}+\left[a_2,b_2\right]$ , which implies $\forall t_{k^{″}}\in t_{k^{\prime }}+\left[a_2,b_2\right],x_{k^{″}}\in \overline{{\mathcal{R}}^m\left({\mathbb{R}}^n,\overline{{\mathbb{S}}_{{\mu }_1}},\left[a_2,b_2\right],k^{″}-k^{\prime }\right)}$ . Therefore, ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi \Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu }}\models {\mathcal{T}}_{\phi }$ .

Case iv): φ = φ ₁ ∧ φ ₂ . Assume that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }$ , then one has from Definition 4.4 that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{{\phi }_1}$ and ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{{\phi }_2}$ . Moreover, since φ ₁ and φ ₂ belong to items ii) or iii), then one can conclude from Case ii) and Case iii) that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{{\phi }_i}\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\phi }_i,i=\left\{\mathrm{1,2}\right\}$ , which implies ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\phi }_1\wedge {\phi }_2$ . That is, ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ . The proof of the other direction is similar and hence omitted.

Then, we prove ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ for

v) φ ₁ ∨ φ ₂ , where φ₁ and φ₂ are STL formulas belong to items ii) or iii).

Case v): φ = φ ₁ ∨ φ ₂ . The proof of ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ is similar to Case iv). The other direction does not hold because for an uncertain system, it is possible that there exists a trajectory ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}$ such that ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ , however, the initial state $x_0\notin {\mathbb{X}}_{root}^{\phi }\left(t_0\right)$ (due to Proposition 3.2), where ${\mathbb{X}}_{root}^{\phi }$ denotes the root node of ${\mathcal{T}}_{\phi }$ . In this case, ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}$ does not satisfy ${\mathcal{T}}_{\phi }$ .

The proof of ${\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models {\mathcal{T}}_{\phi }\Rightarrow {\mathit{x}}_{x_0}^{\mathit{\nu },\mathit{w}}\models \phi$ for other STL formulas φ in equation (5) can be completed inductively by combining Cases i)-v). Therefore, the conclusion follows. □

Thanks to the semantic relation between the STL formulas in equation (5) and their corresponding tTLTs, we are able to perform control synthesis over the tTLT, instead of the STL formulas, with correct-by-construction guarantees. The details of this control synthesis are provided in the next section.

Figure 7.

tTLTs ${\mathcal{T}}_{\phi }$ for $\phi ={\mu }_1{U}_{\left[a,b\right]}{\mu }_2$ .

Figure 8.

tTLTs for $\phi =F_{\left[a_1,b_1\right]}{G}_{\left[a_2,b_2\right]}{\mu }_1$ .

5. Online control synthesis

In this section, we study the STL control synthesis problem in Problem 2.1. In the following, an online control synthesis algorithm and its sub-algorithms are designed over the tTLT such that the tTLT ${\mathcal{T}}_{\phi }$ is satisfied (in the sense of Definitions 4.4 and 4.5). From Theorem 4.1, one can see that to guarantee the satisfaction of the STL formula φ in equation (5), it is sufficient to find a control policy ν that guarantees the (robust) satisfaction of the corresponding tTLT ${\mathcal{T}}_{\phi }$ . To this end, the tTLT-based control synthesis approach is sound.

5.1. Definitions and notations

Before proceeding, the following definitions and notations are needed.

Definition 5.1

The time horizon |Θ| of an STL operator $\Theta \in \left\{\wedge ,\vee ,U_{\left[a,b\right]},F_{\left[a,b\right]},G_{\left[a,b\right]}\right\}$ is defined as

$\left|\Theta \right|=\{\begin{array}{ll}0,& if \Theta =\left\{\wedge ,\vee \right\},\\ \widehat{b},& if\Theta \in \left\{U_{\left[a,b\right]},F_{\left[a,b\right]},G_{\left[a,b\right]}\right\},\end{array}$

where $\widehat{b}=\underset{t_k}{\mathrm{argmax}}\left\{a\le t_k\le b\right\}$ .

Definition 5.2

A segment of a complete path of a tTLT is called a Boolean segment if it starts and ends with a tube node and contains only Boolean operator nodes. We say a tube node ${\mathbb{X}}_j$ is reachable from ${\mathbb{X}}_i$ by a Boolean segment if there exists a Boolean segment that starts with ${\mathbb{X}}_i$ and ends with ${\mathbb{X}}_j$ .

Definition 5.3

If each node of a tree is either a set node that is a subset of U or an operator node that belongs to $\left\{\wedge ,\vee ,U_I,F_I,G_I\right\}$ , then the tree is called a control tree.

Each tube node ${\mathbb{X}}_i$ of the tTLT ${\mathcal{T}}_{\phi }$ is characterized by the following two parameters:

• $t_a\left({\mathbb{X}}_i\right)$ : the activation time of ${\mathbb{X}}_i$ ,

• $t_h\left({\mathbb{X}}_i\right)$ : the time horizon of ${\mathbb{X}}_i$ , i.e., the time that ${\mathbb{X}}_i$ is deactivated.

Denote by $T_{\phi }\left(tk\right)$ the resulting tree of $T_{\phi }$ at time instant tk. It is obtained by fixing the value of each tube node ${\mathbb{X}}_i$ according to the activation time $t_a\left({\mathbb{X}}_i\right)$ (i.e., $T_{\phi }\left(t_k\right)$ contains either set nodes or operator nodes). Let $S_i\left(t_k\right)$ be the i-th set node of $T_{\phi }\left(t_k\right)$ , where $S_i\left(t_k\right)$ corresponds to the tube node ${\mathbb{X}}_i$ . The relationship between $S_i\left(t_k\right)$ and ${\mathbb{X}}_i$ can be described as follows:

$S_i\left(t_k\right)=\{\begin{array}{l}{\mathbb{X}}_i\left(t_0\right),\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}if\hspace{0.17em}{t}_k\le t_a\left({\mathbb{X}}_i\right)\\ {\mathbb{X}}_i\left(t_k-t_a\left({\mathbb{X}}_i\right)\right),if\hspace{0.17em}{t}_k\le t_a\left({\mathbb{X}}_i\right)\end{array}$

(8)

Moreover, one has that

$t_a\left(S_i\left(t_k\right)\right)=t_a\left({\mathbb{X}}_i\right),t_h\left(S_i\left(t_k\right)\right)=t_h\left({\mathbb{X}}_i\right),\forall k\ge 0$

At each time instant t _k , ${\mathcal{T}}_{\phi }\left(t_k\right)$ is characterized by

• P(t _k ): the set which collects all the set nodes of, i.e., P(t _k ) = ∪ _i S _i (t _k ),

• Θ: the set which collects all the operator nodes of ${\mathcal{T}}_{\phi }\left(t_k\right)$ , which is time invariant.

For a node N _i (t _k ) ∈ P(t _k ) ∪ Θ, define

• CH(N _i (t _k )): the set of children of node N _i (t _k ),

• PA(N _i (t _k )): the set of parents of node N _i (t _k ),

• $\text{Post}\left(N_i\left(t_k\right)\right)≔\text{CH}\left(\text{CH}\left(N_i\left(t_k\right)\right)\right)$ ,

• $\text{Pre}\left(N_i\left(t_k\right)\right)≔\text{PA}\left(\text{PA}\left(N_i\left(t_k\right)\right)\right)$ .

Given a state-time pair (x _k , t _k ), define $L:{\mathbb{R}}^n\times {\mathbb{R}}_{\ge 0}\to 2^{P\left(t_k\right)}$ as the labelling function, given by

$$L\left(x_k,t_k\right)=\left\{S_i\left(t_k\right)\in P\left(t_k\right){:x}_k\in S_i\left(t_k\right),t_k\le t_h\left(S_i\left(t_k\right)\right)\right\},$$

(9)

which maps (x _k , t _k ) to a subset of P(t _k ). Moreover, define the function $B:{\mathbb{R}}^n\times {\mathbb{R}}_{\ge 0}\to 2^{P\left(t_k\right)}$ , which maps (x _k , t _k ) to a set of valid set nodes in P(t _k ). The function L(x _k , t _k ) computes the subset of set nodes of P(t _k ) that contains x _k at time t _k (without the consideration of history trajectory) while the function B(x _k , t _k ) is further introduced to capture the fact that given the history trajectory, not all set nodes in L(x _k , t _k ) are valid at time t _k . A rule for determining B(x _k , t _k ) given L(x _k , t _k ) is detailed in Algorithm 7 in the next subsection.

5.2. Online control synthesis

In the following, we present the online control synthesis algorithm (and its sub-algorithms), and then present an example to further explain how each sub-algorithm works.

Algorithm 5. onlineControlSynthesis.

Algorithm 6. Initialization.

Algorithm 7. trackingSetNode.

The online control synthesis algorithm is outlined in Algorithm 5. Before implementation, an initialization process (line 1) is required, which is outlined in Algorithm 6. Here, t _a and t _h are two functions that map each tube node ${\mathbb{X}}_i$ to its activation time and time horizon, respectively. If $t_a\left({\mathbb{X}}_i\right)$ or $t_h\left({\mathbb{X}}_i\right)$ is unknown for ${\mathbb{X}}_i$ , its value will be set as ⋈. Then, at each time instant t _k , a feasible control set $\mathbb{U}\left(x_k,t_k\right)$ is synthesized (lines 2-11). This process contains the following steps: 1) find the subset of set nodes in P(t _k ) that are valid at time t _k , i.e., B(x _k , t _k ), via Algorithm 7 (line 2); 2) determine the activation time of ${\mathbb{X}}_i$ , whose corresponding set node S _i (t _k ) ∈ B(x _k , t _k ) (if $t_a\left({\mathbb{X}}_i\right)$ is unknown, i.e., being visited for the first time, it is set as t _k ; otherwise, i.e., being visited before, it is unchanged) (lines 3-7); 3) calculate ${\mathcal{T}}_{\phi }\left(t_{k+1}\right)$ via Algorithm 8 (line 8); 4) build a control tree ${\mathcal{T}}_u\left(t_k\right)$ (Definition 5.3) via Algorithm 9 (line 9), compress it via Algorithm 3 (line 10), and then the feasible control set $\mathbb{U}\left(x_k,t_k\right)$ is given by backtracking the compressed control tree ${\mathcal{T}}_u^c\left(t_k\right)$ via Algorithm 10 (line 11). If the obtained feasible control set ${\mathcal{T}}_u^c\left(t_k\right)$ , the control synthesis process stops and returns NExis (lines 12-13); otherwise, the control input ν _k can be chosen as any element of $\mathbb{U}\left(x_k,t_k\right)$ (one example is to choose ν _k as ${\mathit{min}}_{{\nu }_k\mathbb{\in }\mathbb{U}\left(x_k,t_k\right)}\left\{\Vert {\nu }_k\Vert \right\}$ ) (line 15). Then, we implement the chosen ν _k , measure x _k+1 (line 16), and finally compute the subset of set nodes that are possibly available at the next time instant t _k+1 , i.e., $Post\left(B\left(x_k,t_k\right)\right)$ , via Algorithm 11 (line 17).

Algorithm 8. updatetTLT.

We further detail Algorithms 6–11 in the following.

• Algorithm 6 calculates the functions t _a and t _h (lines 1-7) and $Post\left(B\left(x_{-1},t_{-1}\right)\right)$ (lines 8-12).

• Algorithm 7 outlines the procedure of finding the subset of set nodes in P(t _k ) that are valid at time t _k , i.e., B(x _k , t _k ). This is the most important step of the control synthesis, and it relates to Algorithm 11 postSet. Firstly, one needs to compute the subset of set nodes of P(t _k ) that contains x _k at time t _k , i.e., L(x _k , t _k ) (line 1). Then, one has from Definition 4.4 that if a trajectory x satisfies one complete path of the tTLT, it must i) visit each tube node of the complete path sequentially and ii) stay in each tube node for sufficiently long time steps (Remark 4.1). Based on these two requirements, Algorithm 11 is designed to predict the subset of set nodes that are possibly available at the next time instant, i.e., $Post\left(B\left(x_{k-1},t_{k-1}\right)\right)$ . Note that B(x _k , t _k ) must belong to L(x _k , t _k ) and $Post\left(B\left(x_{k-1},t_{k-1}\right)\right)$ at the same time. Therefore, we let $B\left(x_k,t_k\right)\leftarrow L\left(x_k,t_k\right)\cap Post\left(B\left(x_{k-1},t_{k-1}\right)\right)$ (line 2). The rest of Algorithm 7 (lines 3-7) guarantees that B(x _k , t _k ) contains at most one set node for each complete path of ${\mathcal{T}}_{\phi }\left(t_k\right)$ .

• Algorithm 8 outlines the procedure of calculating ${\mathcal{T}}_{\phi }\left(t_{k+1}\right)$ , given ${\mathcal{T}}_{\phi }\left(t_k\right)$ , t _a and B(x _k , t _k ). It is designed based on equation (8).

• Algorithm 9 outlines the procedure of building a control tree ${\mathcal{T}}_u\left(t_k\right)$ , which is then used for control set synthesis. It is initialized as ${\mathcal{T}}_{\phi }\left(t_k\right)$ (line 1). Then, for those set nodes S _i (t _k ) that belongs to B(x _k , t _k ), it is replaced with the feasible control set (lines 2–8), otherwise, it is replaced with ∅ (lines 9–11).

• Algorithm 10 is similar to Algorithm 4, which outlines the procedure of backtracking a compressed tree.

• Algorithm 11 outlines the procedure of finding the subset of set nodes that are possibly available at the next time instant t _k+1 given B(x _k , t _k ), t _a and ${\mathcal{T}}_{\phi }\left(t_{k+1}\right)$ . It is designed based on Definition 4.4, where the three cases (lines 4–8, 9–12, 13–16) correspond to items i)–iii) of Definition 4.4, respectively. It guarantees that the resulting trajectory visits each tube node of ${\mathcal{T}}_{\phi }$ sequentially and stays in each tube node for sufficiently long time steps (as we discussed in Algorithm 7).

Algorithm 9. buildControlTree.

Algorithm 10. Backtracking*.

Algorithm 11. postSet.

Next, an example is given to illustrate one iteration of the control synthesis algorithm (Algorithm 5).

Example 5.1

Consider the single-integrator control system $\dot{x}=u+w$ with a sampling period of one second. The corresponding discrete-time system is given by

$x_{k+1}=x_k+u_k+w_k$

where $x_k\in {\mathbb{R}}^2,u_k\in U:=\left\{u:\Vert u\Vert \le 1\right\}\subset {\mathbb{R}}^2,w_k\in W:=\left\{w:\Vert w\Vert \le 0.1\right\}\subset {\mathbb{R}}^2,\forall k\mathbb{\in }\mathbb{N}$ . The task specification φ is given in Example 3.1, i.e., $\phi =F_{\left[a_1,b_1\right]}{G}_{\left[a_2,b_2\right]}{\mu }_1\wedge {\mu }_2{U}_{\left[a_3,b_3\right]}{\mu }_3$ , where [a ₁ , b ₁ ] = [5, 10], [a ₂ , b ₂ ] = [0, 10], [a ₃ , b ₃ ] = [0, 8], $g_{{\mu }_1}\left(x\right)=1-\Vert x\Vert$ , $g_{{\mu }_2}\left(x\right)=5-\Vert x-{\left[\mathrm{4,4}\right]}^T\Vert$ , and $g_{{\mu }_3}\left(x\right)=1-\Vert x-{\left[\mathrm{3,5}\right]}^T\Vert$ . Then, one has

$\begin{array}{l}{\mathbb{S}}_{{\mu }_1}=\left\{x_0:\Vert x_0\Vert \le 1\right\},\\ {\mathbb{S}}_{{\mu }_2}=\left\{x_0:\Vert x_0-{\left[\mathrm{4,4}\right]}^T\Vert \le 5\right\},\\ {\mathbb{S}}_{{\mu }_3}=\left\{x_0:\Vert x_0-{\left[\mathrm{3,5}\right]}^T\Vert \le 1\right\}.\end{array}$

The tTLT that corresponds to φ is plotted in Figure 5 . Using Definitions 2.6 and 2.7, one can calculate that

$\begin{array}{l}{\mathbb{X}}_4\left(t_k\right)=\left\{x_k:\Vert x_k\Vert \le 0.9\right\},\\ {\mathbb{X}}_3\left(t_k\right)=\{x_k:\Vert x_k-{\left[\mathrm{3,5}\right]}^T\Vert \le 8.1-k\\ \wedge \Vert x_k-{\left[\mathrm{4,4}\right]}^T\Vert \le 5\},\\ {\mathbb{X}}_2\left(t_k\right)=\left\{x_k:\Vert x_k\Vert \le 9.9-k\right\},\\ {\mathbb{X}}_1\left(t_k\right)={\mathbb{X}}_2\left(t_k\right)\cap {\mathbb{X}}_3\left(t_k\right).\end{array}$

The initial state x ₀ = [0.5,0.8] ^T , for which $x_0\in {\mathbb{X}}_{root}^{\phi }\left(t_0\right)$ . Firstly, an initialization process is required, and one can get from Algorithm 6 that

$\begin{array}{l}{t}_h\left({\mathbb{X}}_1\right)=0,t_h\left({\mathbb{X}}_2\right)=10,t_h\left({\mathbb{X}}_3\right)=8,\\ t_h\left({\mathbb{X}}_4\right)=20,t_h\left({\mathbb{S}}_{{\mu }_1}\right)=\infty ,t_h\left({\mathbb{S}}_{{\mu }_3}\right)=\infty ,\end{array}$

And

$Post\left(B\left(x_{-1},t_{-1}\right)\right)=\left\{{\mathbb{X}}_1\left(t_0\right),{\mathbb{X}}_2\left(t_0\right),{\mathbb{X}}_3\left(t_0\right)\right\}.$

Now, let us see how the feasible control set $\mathbb{U}\left(x_0,t_0\right)$ is synthesized at time instant t ₀ .

1) Find B(x ₀ , t ₀ ) via Algorithm 7. First, L(x ₀ , t ₀ ) is computed according to equation (9),

$$L\left(x_0,t_0\right)=\left\{{\mathbb{X}}_1\left(t_0\right),{\mathbb{X}}_2\left(t_0\right),{\mathbb{X}}_3\left(t_0\right),{\mathbb{X}}_4\left(t_0\right),{\mathbb{S}}_{{\mu }_1}\right\}$$

Then, after running lines 2-7, one has

$B\left(x_0,t_0\right)=\left\{S_2\left(t_0\right),S_3\left(t_0\right)\right\}$

• 2) Determine the activation time. Initially, both $t_a\left({\mathbb{X}}_2\right)$ and $t_a\left({\mathbb{X}}_3\right)$ are unknown, therefore, $t_a\left({\mathbb{X}}_2\right)=t_a\left({\mathbb{X}}_3\right)=t_0$ .

• 3) Update the TLT (thus obtain ${\mathcal{T}}_{\phi }\left(t_1\right)$ ) via Algorithm 8. The output ${\mathcal{T}}_{\phi }\left(t_1\right)$ is given by

$\begin{array}{l}{S}_1\left(t_1\right)={\mathbb{X}}_1\left(t_0\right),S_2\left(t_1\right)={\mathbb{X}}_2\left(t_1\right),\\ S_3\left(t_1\right)={\mathbb{X}}_3\left(t_1\right),S_4\left(t_1\right)={\mathbb{X}}_4\left(t_0\right),\end{array}$

and the leaf nodes ${\mathbb{S}}_{{\mu }_1}$ and ${\mathbb{S}}_{{\mu }_3}$ are unchanged.

• 4) Build the control tree ${\mathcal{T}}_u\left(t_0\right)$ , compress it to obtain ${\mathcal{T}}_u^c\left(t_0\right)$ , and then get $\mathbb{U}\left(x_0,t_0\right)$ . This process is illustrated in Figure 9, and $\mathbb{U}\left(x_0,t_0\right)=\mathbb{U}\left(S_2\left(t_0\right)\right)\mathbb{\cap }\mathbb{U}\left(S_3\left(t_0\right)\right)$ .

Since $\mathbb{U}\left(x_0,t_0\right)\ne \varnothing$ , the online control synthesis continues, and we can further compute $Post\left(B\left(x_0,t_0\right)\right)$ via Algorithm 11, which gives

$Post\left(B\left(x_0,t_0\right)\right)=\left\{S_2\left(t_1\right),S_3\left(t_1\right),{\mathbb{S}}_{{\mu }_3}\right\}.$

The following theorem shows the applicability and soundness of Algorithm 5.

Figure 9.

Left: $\mathbb{U}\left(x_0,t_0\right)$ , Middle: ${\mathcal{T}}_u^c\left(t_0\right)$ , Right: root node of ${\mathcal{T}}_u^c\left(t_0\right)$ after implementing Algorithm 10, where $\mathbb{U}\left(S_2\left(t_0\right)\right)=U=\left\{u:\Vert u\Vert \le 1\right\},\mathbb{U}\left(S_3\left(t_0\right)\right)=U\cap \left\{u:\Vert u-{\left[\mathrm{3.4,3.1}\right]}^T\Vert \le 5\right\}$ .

Theorem 5.1

Consider uncertain system equation (1) with initial state x ₀ and an STL formula φ in equation (5). Assume that φ is robustly satisfiable for equation (1) and $x_0\in {\mathcal{T}}_{root}^{\phi }\left(t_0\right)$ . Then, implementing the online control synthesis algorithm (Algorithm 5) guarantees that

(i) the control set $\mathbb{U}\left(x_k,t_k\right)$ is nonempty for all $k\mathbb{\in }\mathbb{N}$ ;

(ii) the resulting trajectory $x\models \phi$ .

Proof

The proof follows from the construction of tTLT and Algorithms 5-11. The existence of a controller ν _k at each time step t _k , is guaranteed by the definition of maximal and minimal reachable sets (Definitions 2.6 and 2.7), and the construction of tTLT (Propoition 3.1, Theorem 3.1 and Algorithm 1). Moreover, the design of Algorithms 5-11 guarantees that the resulting trajectory x satisfies the tTLT ${\mathcal{T}}_{\phi }$ , i.e., $\mathit{x}\models {\mathcal{T}}_{\phi }$ , which implies x ⊨ φ as proven in Theorem 4.1.

Remark 5.1

The tTLT construction relies on the computation of backward reachable tubes. Over the past decade, new approaches (e.g., decomposition-based approach (Chen et al., 2018a) and learning-based approaches (Allen et al., 2014; Bansal and Tomlin, 2021)) and software tools (e.g., Hamilton-Jacobi Toolbox (Mitchell and Templeton, 2005) and CORA Toolbox (Althoff, 2015)), have been developed for improving the efficiency of computing backward reachable tubes. Moreover, we remark that the computation of reachable tubes in our work for constructing of the tTLT can be performed offline, which may mitigate the online computational burden. On the other hand, although the exact computation of backward reachable sets/tubes is in general nontrivial for high-dimensional nonlinear systems, efficient algorithms exist for linear systems with polygonal input and disturbance sets (Kurzhanski and Pravin, 2014).

Remark 5.2

The online control synthesis algorithm (Algorithm 5) contains 7 sub-algorithms, i.e., Algorithm 3 and Algorithms 6-11. The computational complexity is determined by Algorithm 9, in which one-step feasible control sets need to be computed. The computational complexity of Algorithms 3, 6, 7, 8, 10, 11 is $\mathcal{O}\left(1\right)$ . Note that in Algorithm 8, the computation of reachable sets, which is required for set node update, is done offline when constructing the tTLT.

Remark 5.3

Different from the mixed-integer programming formulation for STL control synthesis (Raman et al., 2014, 2015), where an entire control policy has to be synthesized at each time step, the control synthesis in our work is reactive in the sense that only the control input at the current time step is generated at each time step.

6. Numerical simulations

In this section, two examples illustrating the theoretical results are provided. We first perform a numerical simulation for car overtaking. We then apply our algorithms to motion planning of a mobile robot over a group of STL specifications and test the scalability of our algorithms with respect to the growing STL complexity.

6.1. Car overtaking example

We first consider a car overtaking example. This example will specify an overtaking task as an STL formula and then show how to synthesize an overtaking controller with safety guarantees.

As shown in Figure 10, we consider a scenario where an automated vehicle Veh₁ plans to move to a target set ${\mathbb{S}}_{{\mu }_1}$ within 80 s. Since there is a broken vehicle Veh₂ in front of Veh₁ and there is another vehicle Veh₃ that moves in an opposite direction in the other lane, Veh₁ must overtake Veh₂ for reaching ${\mathbb{S}}_{{\mu }_1}$ and avoid Veh₃ for safety.

Figure 10.

Scenario illustration: an automated vehicle plans to reach a target set ${\mathbb{S}}_{{\mu }_1}$ while overtaking a broken vehicle Veh ₂ in front of it in the same lane and avoiding Veh ₃ moving in an opposite direction in the other lane.

We describe the dynamics of the vehicle Veh₁ as in Murgovski and Sjöberg (2015):

$x_{k+1}=\underset{A}{\underbrace{\left[\begin{array}{lll}1& 0& \delta \\ 0& 1& 0\\ 0& 0& 1\end{array}\right]}}{x}_k+\underset{B}{\underbrace{\left[\begin{array}{ll}0& 0\\ \delta & 0\\ 0& \delta \end{array}\right]}}{u}_k+w_k,$

where $x_k={\left[p^x\left(k\right),p^y\left(k\right),v^x\left(k\right)\right]}^T$ , $u_k={\left[v^y\left(k\right),a^x\left(k\right)\right]}^T$ , and δ is the sampling period. The working space is $X=\left\{z\in {\mathbb{R}}^3\mid {\left[0,-5,-3\right]}^T\le z\le {\left[\mathrm{120,5,3}\right]}^T\right\}$ , the control constraint set is $U=\left\{z\in {\mathbb{R}}^2\mid {\left[-1,-1\right]}^T\le z\le {\left[\mathrm{1,1}\right]}^T\right\}$ , the disturbance set is $W=\left\{z\in {\mathbb{R}}^3\mid {\left[-0.05,-0.05,-0.05\right]}^T\le z\le {\left[\mathrm{0.05,0.05,0.05}\right]}^T\right\}$ , and the target region is ${\mathbb{S}}_{{\mu }_1}=\left\{z\in {\mathbb{R}}^2\mid {\left[115,-\mathrm{5,0.5}\right]}^T\le z\le {\left[\mathrm{120,0,0.5}\right]}^T\right\}$ .

We use ${\mathbb{S}}_{{\mu }_2}=\left\{z\in {\mathbb{R}}^3\mid {\left[45,-5,-\infty \right]}^T\le z\le {\left[\mathrm{50,0},\infty \right]}^T\right\}$ to denote the state set that contains the occupancy of Veh₂. We describe the dynamics of the vehicle Veh₃ as

${\overline{x}}_{k+1}=\underset{\overline{A}}{\underbrace{\left[\begin{array}{ll}1& 0\\ 0& 1\end{array}\right]}}{x}_k+\underset{\overline{B}}{\underbrace{\left[\begin{array}{ll}\delta & 0\\ 0& \delta \end{array}\right]}}{\overline{u}}_k,$

where $x_k={\left[{\overline{p}}^x\left(k\right),{\overline{p}}^y\left(k\right)\right]}^T$ , ${\overline{u}}_k={\left[{\overline{v}}^x\left(k\right),{\overline{v}}^y\left(k\right)\right]}^T$ , We assume that it moves at a constant velocity ${\overline{u}}_k={\left[{\overline{v}}^x,0\right]}^T$ . The initial state of Veh₃ is ${\overline{x}}_0={\left[{\overline{p}}_{ini}^x,2.5\right]}^T$ . Then, we have that its position of x-axis is ${\overline{p}}_k^x={\overline{p}}_{ini}^x+\delta \times \left(k-1\right)\times {\overline{v}}^x$ .

To formulate the overtaking task, we define the following three sets as shown in Figure 10: ${\mathbb{S}}_{{\mu }_3}=\left\{z\in {\mathbb{R}}^3\mid {\left[0,-5,-3\right]}^T\le z\le {\left[\mathrm{35,0,3}\right]}^T\right\}$ , ${\mathbb{S}}_{{\mu }_4}=\left\{z\in {\mathbb{R}}^3\mid {\left[35,-5,-3\right]}^T\le z\le {\left[\mathrm{60,5,3}\right]}^T\right\}$ , and ${\mathbb{S}}_{{\mu }_5}=\left\{z\in {\mathbb{R}}^3\mid {\left[60,-5,-3\right]}^T\le z\le {\left[\mathrm{120,0,3}\right]}^T\right\}$ .

Let us choose the sampling period as δ = 0.2s(seconds). To respect the time constraint and the input constraint for Veh₁, we consider two possible solutions to the previous reachability problem: (1) fast overtaking: overtake Veh₂ before Veh₃ passes Veh₂; (2) slow overtaking: wait until Veh₃ passes Veh₂ and then overtake Veh₂. The fast overtaking can be encoded into an STL formula:

$\begin{array}{l}{\phi }_{fast\_overtake}={\mu }_3{U}_{\left[\mathrm{0,16}\right]}{\mu }_4\wedge \left({\mu }_3\vee {\mu }_4\right)U_{\left[\mathrm{0,30}\right]}{\mu }_5\\ \wedge \left({\mu }_3\vee {\mu }_4\vee {\mu }_5\right)U_{\left[\mathrm{0,80}\right]}{G}_{\left[\mathrm{0,2}\right]}{\mu }_1\wedge G_{\left[\mathrm{0,80}\right]}\neg \left({\mu }_2\vee {\mu }_6\right),\end{array}$

where ${\mathbb{S}}_{{\mu }_6}=\left\{z\in {\mathbb{R}}^6\mid {\left[{\overline{p}}^x\left(16\right),0,-\infty \right]}^T\le z\le {\left[{\overline{p}}^x\left(0\right),5,\infty \right]}^T\right\}$ . Note that ${\mathbb{S}}_{{\mu }_6}$ denotes the reachable set for the vehicle Veh₃ within the time interval [0,16] seconds and 16 (that corresponds to the sampling index k = 80) is the maximal time instant that the vehicle Veh₁ can reach the set ${\mathbb{S}}_{{\mu }_5}$ in the sprit of φ₁. Using Algorithm 1, one can construct the tTLT ${\mathcal{T}}_{{\phi }_{fast\_overtake}}$ (see Figure 11), where

$\begin{array}{l}{\mathbb{X}}_6\left(t_k\right)={\mathcal{R}}^M\left(X,{\mathbb{S}}_{{\mu }_4},{\mathbb{S}}_{{\mu }_3},\left[\mathrm{0,16}\right],k\right),\\ {\mathbb{X}}_7\left(t_k\right)={\mathcal{R}}^M\left(X,{\mathbb{S}}_{{\mu }_5},{\mathbb{S}}_{{\mu }_3}\cup {\mathbb{S}}_{{\mu }_4},\left[\mathrm{0,30}\right],k\right),\\ {\mathbb{X}}_8\left(t_k\right)=\overline{{\mathcal{R}}^m\left(X,\overline{{\mathbb{S}}_{{\mu }_1}},\left[\mathrm{0,2}\right],k\right)},\\ {\mathbb{X}}_4\left(t_k\right)={\mathbb{X}}_6\left(t_k\right)\cap {\mathbb{X}}_7\left(t_k\right),\\ {\mathbb{X}}_5\left(t_k\right)={\mathcal{R}}^M\left(X,{\mathbb{X}}_8\left(t_0\right),{\mathbb{S}}_{{\mu }_3}\cup {\mathbb{S}}_{{\mu }_4}\cap {\mathbb{S}}_{{\mu }_5},\left[\mathrm{0,80}\right],k\right),\\ {\mathbb{X}}_2\left(t_k\right)={\mathbb{X}}_4\left(t_k\right)\cap {\mathbb{X}}_5\left(t_k\right),\\ {\mathbb{X}}_3\left(t_k\right)=\overline{{\mathcal{R}}^m\left(X,{\mathbb{S}}_{{\mu }_2}\cap {\mathbb{S}}_{{\mu }_6},\left[\mathrm{0,80}\right],k\right)},and\\ {\mathbb{X}}_1\left(t_k\right)={\mathbb{X}}_2\left(t_k\right)\cup {\mathbb{X}}_3\left(t_k\right).\end{array}$

Figure 11.

The constructed tTLT $T_{\phi \text{fast}\_\text{overtake}}$ .

The slow overtaking can be encoded into an STL formula

$\begin{array}{l}{\phi }_{slow\_overtake}={\mu }_3{U}_{\left[\mathrm{16,32}\right]}{\mu }_4\wedge \left({\mu }_3\vee {\mu }_4\right)U_{\left[\mathrm{0,45}\right]}{\mu }_5\\ \wedge \left({\mu }_3\vee {\mu }_4\vee {\mu }_5\right)U_{\left[\mathrm{0,80}\right]}{G}_{\left[\mathrm{0,2}\right]}{\mu }_1\wedge G_{\left[\mathrm{0,80}\right]}\neg \left({\mu }_2\vee {\mu }_7\right)\end{array}$

where ${\mathbb{S}}_{{\mu }_7}=\left\{z\in {\mathbb{R}}^2\mid {\left[-\infty ,0,-\infty \right]}^T\le z\le {\left[{\overline{p}}^x\left(16\right),5,\infty \right]}^T\right\}$ . Note that ${\mathbb{S}}_{{\mu }_7}$ denotes the reachable set for the vehicle Veh₃ within the time interval $[16,+\infty )$ and 16 (that corresponds to the sampling index k = 80) is the minimal time instant that the vehicle Veh₁ can reach the set ${\mathbb{S}}_{{\mu }_4}$ in the sprit of φ₂. The tTLT ${\mathcal{T}}_{{\phi }_{slow\_overtake}}$ can be constructed similar to ${\mathcal{T}}_{{\phi }_{fast\_overtake}}$ .

In the following, two simulation cases are considered and the online control synthesis algorithm is implemented. In the fast overtaking, we choose the initial position ${\overline{p}}_{ini}^x=95$ and the moving velocity ${\overline{v}}^x=-2$ for the vehicle Veh₃ and the initial position x₀ = [0.5,−2.5,2]^T for Veh₁. One can verify that the specification φ_{slow_overtake} is infeasible in this case. Figure 12(a) shows the position trajectories, from which we can see that the whole specification is fulfilled. The blue region denotes the set ${\mathbb{S}}_{{\mu }_6}$ . Figure 12(b) shows the velocity trajectory of v ^x and Figure 12(c) and (d) show the corresponding control inputs, where the dashed lines denote the control bounds. The cyan regions represent the synthesized control sets and the blue lines are the control trajectories. In the slow overtaking, we choose the initial position ${\overline{p}}_{ini}^x=80$ and the moving velocity ${\overline{v}}^x=-3$ for the vehicle Veh₃ and the same initial position x₀ = [0.5,−2.5]^T for Veh₁. In this case one can verify that φ_{fast_overtake} is infeasible. Figure 13(a) shows the position trajectories, from which we can see that the whole specification is fulfilled. The blue region denotes the intersection between the set X and the set ${\mathbb{S}}_{{\mu }_7}$ . Figure 13(b) shows the velocity trajectory of v ^x and Figure 13(c) and (d) show the corresponding control input trajectories of a ^x and v ^y .

Figure 12.

Trajectories for one realization of disturbance signal in the fast overtaking: (a) position trajectory; (b) velocity trajectory of x-axis; (c) control trajectory of x-axis; (d) control trajectory of y-axis.

Figure 13.

Trajectories for one realization of disturbance signal in the slow overtaking: (a) position trajectory; (b) velocity trajectory of x-axis; (c) control trajectory of x-axis; (d) control trajectory of y-axis.

To highlight the effect of disturbances, we compare the trajectories with and without disturbances in the fast overtaking, which are shown in Figure 14(a)–(e). In Figure 14(a), we show the evolution of the x-axis position along the time. We use k ₁ , k ₂ , and k ₃ (or $k_1^{\prime }$ , $k_2^{\prime }$ , and $k_3^{\prime }$ ) to denote the minimal time instants that Veh₁ reaches the sets ${\mathbb{S}}_{{\mu }_4}$ , ${\mathbb{S}}_{{\mu }_5}$ , and ${\mathbb{S}}_{{\mu }_1}$ for the noisy scenario (or for the deterministic scenario). We can see that the disturbances slightly delay the reaching time, while both two position trajectories satisfy the time intervals encoded in φ ₁ . The differences of the velocity trajectory of v ^x and the corresponding control input trajectories of a ^x and v ^y are highlighted in Figure 13(c)–(d), respectively. The disturance realizations of w _k are shown in Figure 13(e). In the deterministic scenario, the controller is aggressive in the sense that the velocity can actively reach the maximum velocity. As a comparison, the controller in the noisy scenario is more cautious in the sense that some gaps always exist between the actual velocity and the maximum velocity. In order to reject the disturbance, more frequent changing of the control inputs occurs in the noisy scenario. Similar observations are applied to the slow overtaking, whose comparisons are shown in Figure 15. Furthermore, in order to show the robustness, we run 100 realizations of the disturbance trajectories in the fast overtaking and in the slow overtaking, respectively. The position trajectories for such 100 realizations of two cases are shown in Figure 16.

Figure 14.

Comparison of robust control with noise and deterministic control without disturbance signal in the fast overtaking: (a) position-time trajectory; (b) velocity trajectory of x-axis; (c) control trajectory of x-axis; (d) control trajectory of y-axis; (e) disturbance signals.

Figure 15.

Comparison of robust control with noise and deterministic control without disturbance signal in the ast overtaking in the slow overtaking: (a) position-time trajectory; (b) velocity trajectory of x-axis; (c) control trajectory of x-axis; (d) control trajectory of y-axis; (e) disturbance signals.

Figure 16.

Position trajectories for 100 realizations of disturbance signals. (a) Position trajectories for 100 realizations of disturbance signals in the fast overtaking. (b) Position trajectories for 100 realizations of disturbance signals in the slow overtaking.

Finally, we report the computation time of this example, which was run in Matlab R2016a with MPT toolbox (Herceg et al., 2013) on a Dell laptop with Windows 7, Intel i7-6600U CPU 2.80 GHz and 16.0 GB RAM. We perform reachability analysis for constructing the tTLT offline, which takes 59.10 s. For online control synthesis, the minimal computation time at a single time step over 100 realizations is 0.23 s, while the maximal computation time is 1.07 s. The average time of each time step is 0.31 s. We remark that the mixed-integer formulation is difficult to implement in this example. This is because the computational complexity of mixed-integer programming grows exponentially with the horizon of the STL formula, which in this example reaches up to 400 sampling instants, much longer than the horizons considered in the simulation examples of Raman et al. (2015, 2014); Sadraddini and Belta (2015).

6.2. Motion planning example

In this section, we consider the motion planning of a mobile robot in an environment, as shown in Figure 17, under a group of STL specifications with growing complexity. We describe the underlying continuous dynamics of the automated vehicle as:

$f\left(x,u,w\right)=\left[\begin{array}{l}{\dot{p}}^x\\ {\dot{p}}^y\\ \stackrel{.}{\theta }\end{array}\right]=\left[\begin{array}{l}v\hspace{0.17em}\mathit{cos}\hspace{0.17em}\theta \\ v\hspace{0.17em}\mathit{sin}\hspace{0.17em}\theta \\ \sigma \end{array}\right]+w,$

where $x={\left[p^x,p^y,\theta \right]}^T$ is the vehicle’s x position, y position, and heading, respectively. The control input is u = [v,σ] ^T , where v is the vehicle’s velocity and σ is the angular velocity. The working space is $X=\left\{z\in {\mathbb{R}}^3\mid {\left[-5,-5,-\pi \right]}^T\le z\le {\left[-\mathrm{5,5},\pi \right]}^T\right\}$ , the control set is $U=\left\{z\in {\mathbb{R}}^2\mid {\left[-0.5,-\pi /5\right]}^T\le z\le {\left[0.5,\pi /5\right]}^T\right\}$ , and the disturbance set is $W=\left\{z\in {\mathbb{R}}^3\mid {\left[-0.1,-0.1,-0.1\right]}^T\le z\le {\left[\mathrm{0.1,0.1,0.1}\right]}^T\right\}$ . For constructing the tTLT, we discretize the above dynamics using a simple zero-order hold estimation. Let Δ be the sampling period, then we describe the discrete dynamics of the automated vehicle as

$x_{k+1}=x_k+f\left(x_k,u_k,w_k\right)\mathrm{\Delta }.$

We set Δ = 0.05s.

We consider the following five STL formulas φ _i , i = 1, …, 5, as defined in equations (10a)–(10e). These five formulas have increasing complexity, e.g., longer horizon and more operators. We report the computation time of this example, which was run in Matlab R2022b with the Level Set Method Toolbox (Mitchell and Templeton, 2005). The offline computation time for constructing the tTLT and the online computation time for synthesizing the controller are summarized in Table 2. As expected, the offline computation time typically increases with respect to the complexity of STL formulas. Note that the formulas φ ₃ and φ ₄ have the same computation time (134.49 s) since the computation of reachable sets for ϕ ₃ can be directly reused to construct the tTLT of ϕ ₄ , despite that ϕ ₄ looks more complex than ϕ ₃ . On the other hand, the online computation for control synthesis, measured by the computation time per time step, is very efficient for all the formulas. The position trajectories are plotted in Figure 18, where the initial position is indicated by the star and the end position is the circle. The time information over the trajectories is illustrated by the color map.

${\phi }_1=\left({\mu }_0\wedge \neg \left({\mu }_1\vee {\mu }_2\vee {\mu }_3\right)\right)U_{\left[\mathrm{0,30}\right]}{G}_{\left[\mathrm{0,2}\right]}{\mu }_4$

(10a)

${\phi }_2={\varphi }_{21}\wedge {\varphi }_{22}$

(10b)

$\begin{array}{l}{\varphi }_{21}=\left({\mu }_0\wedge \neg \left({\mu }_1\vee {\mu }_2\vee {\mu }_3\vee {\mu }_4\vee {\mu }_5\right)\right)U_{\left[\mathrm{0,20}\right]}{G}_{\left[\mathrm{0,2}\right]}{\mu }_6\\ {\varphi }_{22}=\left(\left({\mu }_0\wedge \neg \left({\mu }_1\vee {\mu }_2\vee {\mu }_3\right)\right)U_{\left[\mathrm{0,35}\right]}{G}_{\left[\mathrm{0,2}\right]}{\mu }_4\right)\\ {\phi }_3=\left({\varphi }_{21}\vee {\varphi }_{31}\right)\wedge {\varphi }_{22}\end{array}$

(10c)

$\begin{array}{l}{\varphi }_{31}=\left({\mu }_0\wedge \neg \left({\mu }_1\vee {\mu }_2\vee {\mu }_3\vee {\mu }_4\vee {\mu }_5\right)\right)U_{\left[\mathrm{0,20}\right]}{G}_{\left[\mathrm{0,3}\right]}{\mu }_7\\ {\phi }_4=\left({\varphi }_{21}\wedge {\varphi }_{22}\wedge {\varphi }_{41}\right)\vee \left({\varphi }_{31}\wedge {\varphi }_{22}\wedge {\varphi }_{42}\right)\end{array}$

(10d)

$\begin{array}{l}{\varphi }_{41}=\left({\mu }_0\wedge \neg \left({\mu }_1\vee {\mu }_2\vee {\mu }_3\vee {\mu }_5\right)\right)U_{\left[\mathrm{35,55}\right]}{G}_{\left[\mathrm{0,2}\right]}{\mu }_6\\ {\varphi }_{42}=\left({\mu }_0\wedge \neg \left({\mu }_1\vee {\mu }_2\vee {\mu }_3\vee {\mu }_5\right)\right)U_{\left[\mathrm{35,55}\right]}{G}_{\left[\mathrm{0,3}\right]}{\mu }_7\\ {\phi }_5={\phi }_4\wedge {\varphi }_{51}\end{array}$

(10e)

${\varphi }_{51}=\left({\mu }_0\wedge \neg \left({\mu }_1\vee {\mu }_2\vee {\mu }_3\vee {\mu }_5\right)\right)U_{\left[\mathrm{55,75}\right]}{G}_{\left[\mathrm{0,2}\right]}{\mu }_8$

Figure 17.

Scenario illustration: an automated vehicle needs to enter into the parking lot, park in the designated parking spot (blue), and leave the parking lot, while avoiding any collisions.

Table 2.

Computation time under different STL formulas.

STL formula	Offline com. time	Online com. time
	(tTLT construction)(s)	(Control synthesis)(s)
φ1 in equation (10a)	71.60	0.0180
φ2 in equation (10b)	82.70	0.0178
φ3 in equation (10c)	134.49	0.0193
φ4 in equation (10d)	134.49	0.0159
φ5 in equation (10e)	187.81	0.0164

Figure 18.

The position trajectories that fulfill the STL formulas φ _i , i = 1, …, 5. The time information is indicated using different colors. (a) A position trajectory that fulfill φ ₁ (b) a position trajectory that fulfills φ ₂ (c) two position trajectories that fulfills φ ₃ (d) two position trajectories that fulfills φ ₄ (e) two position trajectories that fulfills φ ₅ .

7. Car parking experiment

In this section, we consider a car parking example. This example will specify a parking task as an STL formula and then show how our algorithms perform on real hardware. We will first perform reachability analysis for constructing the tTLT offline and then we use the tTLT to synthesize a parking controller for the Small-Vehicles-for-Autonomoy (SVEA) platform (Jiang et al., 2022).

As shown in Figure 19, we consider a scenario where an automated vehicle must enter the parking lot ${\mathbb{S}}_{{\mu }_1}$ , park in the designated parking spot ${\mathbb{S}}_{{\mu }_2}$ , and leave the parking lot through the exit ${\mathbb{S}}_{{\mu }_4}$ , where each step of the scenario has a specific deadline. Additionally, throughout the scenario, the vehicle must stay safe and avoid collisions with the parking lot walls and parked vehicles ${\mathbb{S}}_{{\mu }_3}$ .

Figure 19.

Scenario illustration: an automated vehicle needs to enter into the parking lot, park in the designated parking spot (blue), and leave the parking lot, while avoiding any collisions.

We describe the underlying continuous dynamics of the automated vehicle as:

$f\left(x,u,w\right)=\left[\begin{array}{l}{\dot{p}}^x\\ {\dot{p}}^y\\ \stackrel{.}{\theta }\\ \dot{v}\end{array}\right]=\left[\begin{array}{c}v\hspace{0.17em}\mathit{cos}\hspace{0.17em}\theta \\ v\hspace{0.17em}\mathit{sin}\hspace{0.17em}\theta \\ \frac{v\hspace{0.17em}\mathit{tan}\hspace{0.17em}\delta }{L}\\ a\end{array}\right]+w$

(11)

where $x={\left[p^x,p^y,\theta ,v\right]}^T$ is the vehicle’s x position, y position, heading, and velocity, respectively. u = [δ,a] ^T is the vehicle’s steering and acceleration inputs. The working space is $X=\left\{z\in {\mathbb{R}}^4\mid {\left[-2,-3,-\pi ,-0.6\right]}^T\le z\le {\left[\mathrm{2,2},\pi ,0.6\right]}^T\right\}$ , the control set is $U=\left\{z\in {\mathbb{R}}^2\mid {\left[-\pi /5,-0.5\right]}^T\le z\le {\left[\pi /\mathrm{5,0.5}\right]}^T\right\}$ , and the disturbance set is $W=\left\{z\in {\mathbb{R}}^4\mid {\left[-0.01,-0.01,-\pi /72,-0.01\right]}^T\le z\le {\left[\mathrm{0.01,0.01},\pi /\mathrm{72,0.01}\right]}^T\right\}$ . For constructing the tTLT, we discretize (11) using a simple zero-order hold estimation. Let δ be the sampling period, then we describe the discrete dynamics of the automated vehicle as

$x_{k+1}=x_k+f\left(x_k,u_k,w_k\right)\mathrm{\Delta }$

For the parking task, we set Δ = 0.05s. We define the state sets in Figure 19 as ${\mathbb{S}}_{{\mu }_1}=\left\{z\in {\mathbb{R}}^4\mid {\left[-2,-3,-\pi ,-0.6\right]}^T\le z\le {\left[\mathrm{2,0},\pi ,0.6\right]}^T\right\}$ , ${\mathbb{S}}_{{\mu }_2}=\left\{z\in {\mathbb{R}}^4\mid {\left[1.3,-2,-\pi ,-0.6\right]}^T\le z\le {\left[2,-1.5,\pi ,0.6\right]}^T\right\}$ , ${\mathbb{S}}_{{\mu }_4}=\left\{z\in {\mathbb{R}}^4\mid {\left[\mathrm{0.5,0},-\pi ,-0.6\right]}^T\le z\le {\left[\mathrm{1,1},\pi ,0.6\right]}^T\right\}$ , and ${\mathbb{S}}_{{\mu }_3}={\mathbb{S}}_{{\mu }_{\mathrm{3,1}}}\cup {\mathbb{S}}_{{\mu }_{\mathrm{3,2}}}\cup {\mathbb{S}}_{{\mu }_{\mathrm{3,3}}}$ , where ${\mathbb{S}}_{{\mu }_{\mathrm{3,1}}}=\left\{z\in {\mathbb{R}}^4\mid {\left[-2,-3,-\pi ,-0.6\right]}^T\le z\le {\left[-\mathrm{1.3,0},\pi ,0.6\right]}^T\right\}$ , ${\mathbb{S}}_{{\mu }_{\mathrm{3,1}}}=\left\{z\in {\mathbb{R}}^4\mid {\left[-2,-3,-\pi ,-0.6\right]}^T\le z\le {\left[-\mathrm{1.3,0},\pi ,0.6\right]}^T\right\}$ , ${\mathbb{S}}_{{\mu }_{\mathrm{3,3}}}=\left\{z\in {\mathbb{R}}^4\mid {\left[1.3,-3,-\pi ,-0.6\right]}^T\le z\le {\left[2,-2,\pi ,0.6\right]}^T\right\}$ .

We let the full scenario be 60 s long and specify that the vehicle needs to enter the parking lot, park in the designated spot, and leave the parking lot within 10 s, 40 s, and 60 s, respectively. Then, this parking task can be encoded into the following STL formula:

$\begin{array}{l}{\phi }_{parking}=G_{\left[\mathrm{0,60}\right]}\neg {\mu }_3\wedge F_{\left[\mathrm{0,10}\right]}{G}_{\left[\mathrm{0,30}\right]}{\mu }_1\wedge F_{\left[\mathrm{10,40}\right]}{\mu }_2\\ \wedge F_{\left[\mathrm{40,60}\right]}{\mu }_4\end{array}$

First, we use Algorithm 1 to construct the corresponding tTLT ${\mathcal{T}}_{{\phi }_{parking}}$ (see Figure 20), where the tube nodes ${\mathbb{X}}_i,i=1,\dots ,8$ are computed in a bottom-up manner as in the previous example. Then, we implement the online control synthesis algorithm (Algorithm 5) on a SVEA vehicle using ${\mathcal{T}}_{{\phi }_{parking}}$ . For choosing a control policy within the constraints of the synthesized control sets, we apply the same approach as described in Section IV.C of Jiang et al. (2020).

Figure 20.

The constructed tTLT ${\mathcal{T}}_{{\phi }_{parking}}$ .

For our evaluation, we initialize the SVEA vehicle with the initial state of x ₀ = [1, 1.75, − π, 0]. At this initial state, φ ₃ is robustly satisfiable. Figure 21 shows the position trajectory, where one can see that the specification is fulfilled. In Figure 22, we show the control input trajectories for acceleration and steering. We use k ₁ , k ₂ , k ₃ to denote the minimal time instants that the automated vehicle reaches sets ${\mathbb{S}}_{{\mu }_1}$ , ${\mathbb{S}}_{{\mu }_2}$ , and ${\mathbb{S}}_{{\mu }_4}$ . Using the synthesized controller, the SVEA vehicle realized k ₁ = 8.0, k ₂ = 18.7, and k ₃ = 48.7, as illustrated in both Figures 21 and 22, confirming the satisfaction of φ_parking. For our evaluation, we initialize the SVEA vehicle with the initial state of x ₀ = [1, 1.75, − π, 0]. At this initial state, φ ₃ is robustly satisfiable. Figure 21 shows the position trajectory, where one can see that the specification is fulfilled. In Figure 22, we show the control input trajectories for acceleration and steering. We use k ₁ , k ₂ , k ₃ to denote the minimal time instants that the automated vehicle reaches sets ${\mathbb{S}}_{{\mu }_1}$ , ${\mathbb{S}}_{{\mu }_2}$ , and ${\mathbb{S}}_{{\mu }_4}$ . Using the synthesized controller, the SVEA vehicle realized k ₁ = 8.0, k ₂ = 18.7, and k = 48.7, as illustrated in both Figures 21 and 22, confirming the satisfaction of φ_parking.

Figure 21.

The position trajectory of a SVEA vehicle performing the parking task φ _parking .

Figure 22.

The velocity and heading trajectories in response to the acceleration and steering inputs throughout the parking task φ _parking .

Finally, we report the computation time of this example, which was run in Matlab R2022b with the Level Set Method Toolbox (Mitchell and Templeton, 2005). We perform reachability analysis for constructing the tTLT offline on a Dell laptop with Ubuntu 20.04, Intel i7-4600U CPU 2.10 GHz and 8.0 GB RAM, which takes 2371.81 s. We note that the offline computation time for constructing the tTLT can be significantly reduced by using the python implementation (Bui et al., 2022). Throughout the parking task, we perform the online control synthesis on an NVIDIA Jetson TX2 embedded computer onboard the SVEA vehicle. The average time step of the online control synthesis is 0.001 s. A video demonstration of this experiment can be found at https://bit.ly/STL-TLT.

8. Conclusion

A novel approach for the online control synthesis of uncertain discrete-time systems under STL specifications was proposed in this paper. First, a real-time version of STL semantics and a notion of tTLT were introduced. Then the formal semantic connection between an STL formula and its corresponding tTLT was derived, i.e., a trajectory satisfying a tTLT also satisfies the corresponding STL formula. Finally, an online control synthesis algorithm was designed for the uncertain systems based on the connection between STL and tTLT. For the fragment of STL formulas under consideration, the soundness of the algorithm was proven. In the future, the control synthesis for multi-agent systems under local and/or global STL specifications is of interest.