1 Introduction↩︎

Modern control applications, such as safe and reliable operations of robots and unmanned vehicles, demand satisfying complex time-dependent task specifications instead of the traditional stabilization and trajectory tracking problem. Signal Temporal Logic (STL) [1] provides a formal language framework to describe these tasks, such as requiring a robot to transport materials between specified locations within a prescribed time horizon, and avoid time-varying hazardous regions, like areas undergoing scheduled maintenance. Moreover, STL provides a quantitative measure of task satisfaction through robustness metrics [2]. Essentially, STL has become an increasingly popular tool in areas such as deep learning [3], reinforcement learning [4], learning from demonstration [5], planning and control [6], [7]. Despite its wide applicability, control under STL specifications is challenging due to algorithmic and computational issues.

Mixed-Integer Programming (MIP) [8] and gradient-based methods [9] have been used to enforce STL constraints, but because they rely on optimization, they often do not scale well as the STL specifications become more complex or the system dynamics become more complicated. In recent years, Model Predictive Control has been deployed as a promising tool to satisfy STL specifications within a receding-horizon framework [10], but it also often suffers from computational complexity issues for complex tasks. Symbolic control provides formal correctness guarantees but is prone to the curse of dimensionality due to state-space abstraction [11].

An alternative approach to satisfy STL specifications is using the concept of Prescribed Performance Control (PPC), where performance funnels have been enforced on STL robustness metrics [12], [13]. Although computationally efficient, it can handle only a fragment of STL specifications. Control Barrier Function (CBF) [14] enforces safety constraints with formal guarantees, and time-varying CBF has also been used to under-approximate the predicate function [15]. However, it requires accurate system dynamics and is also limited to a fragment of STL specifications.

The Spatiotemporal Tube (STT) framework, which provides a time-varying safe region in the state space, was introduced in [16] and subsequently extended to address the satisfaction of the full class of Signal Temporal Logic (STL) specifications [17]. In these works, the tubes are generated by solving an optimization problem requiring a predefined template of the tubes, which restricts their expressivity and suffers from increased computational complexity for more complex specifications. Moreover, these tubes rely on unbounded control inputs and can not handle the input constraints, making it infeasible for real-world systems.

In recent years, leveraging the universal approximation property of neural networks, several efforts have been made to synthesize safety controllers for STL specifications [3], [18], which often struggle to enforce formal correctness guarantees, require additional computational burden, and can be applied only for some fragment of the STL specification. In addition, these neural network-based methods still rely on extensive state-space data, necessitating access to a black-box or simulator model for generating training samples, which is often difficult to obtain in real-world scenarios.

In this work, we introduce the Physics-informed Neural Spatiotemporal Tube (PINSTT) framework that constructs the STT directly for the full class of STL specifications, without the knowledge of system dynamics and state-space samples. We frame the STL robustness metric [2] as the loss function of the neural network and ensure a positive radius of the tube by forming another loss function. A key contribution of our work is the use of STT with spherical cross-sections, which significantly reduces computational complexity compared to its hyper-rectangle counterparts [16], [17]. The training of the neural network is performed over the collocation points collected over the augmented time horizon. We verify the trained PINSTT over the continuous horizon on the fly using a Lipschitz-based validity condition. Leveraging the automatic differentiation property of the physics-informed neural network [19], we enforce the Lipschitz boundedness of the center and radius of the constructed tube. The Lipschitz bounds are chosen in such a way that the tube moves in conjunction with the input constraints of the system. Then, based on the velocity and torque bounds of the system, we derive feasibility conditions and subsequently provide an approximation-free, closed-form control law to keep the system within the tube, thereby ensuring satisfaction of the STL specification. Finally, the approach is validated over several case studies.

Notations: The symbols \({\mathbb{N}}\), \({\mathbb{R}}\), \({\mathbb{R}}^+\), and \({\mathbb{R}}_0^+\) denote the set of natural, real, positive real, and nonnegative real numbers. The Euclidean norm of a vector is denoted by \(\lVert \cdot \rVert\). For \(a, b \in \mathbb{N}\) with \(a \leq b\), the closed interval in \(\mathbb{N}\) is denoted as \([a; b]\). The set difference between two sets \(\mathcal{A}\) and \(\mathcal{B}\) is defined as \(\mathcal{A}\setminus \mathcal{B}\). A ball centered at \({\mathbf{c}}\in \mathbb{R}^n\) with radius \({\mathbf{r}}\in \mathbb{R}^+\) is defined as \({\mathbb{B}}({\mathbf{c}}, {\mathbf{r}}) := \{ x \in \mathbb{R}^n \mid \|x - {\mathbf{c}}\| \leq {\mathbf{r}}\}\). For all \(x, y \in {\mathbb{R}}^n\), the vector inequality \(x \preceq y\) represents \(x_i \leq y_i\) for all \(i \in [1;n]\). We define the sup norm \(\|\cdot\|_{[a,b]}\) of a signal \(s:{\mathbb{R}}_0^+ \rightarrow {\mathbb{R}}^n\) over time interval \([a,b]\) as \(\|s\|_{[a,b]}:=\min_{t\in [a,b]}\|s(t)\|\). The symbol \(x \odot y\) represents the Hadamard product (elementwise multiplication) of the two vectors of \(x, y \in {\mathbb{R}}^n\). We use \(\mathbf{I}_n\) and \(\mathbf{0}^{n \times m}\) to denote the identity matrix of size \(n \times n\) and the zero matrix of size \(n \times m\), respectively. \(x \uparrow (\downarrow) c\) implies \(x\) approaches \(c\) from the left (right) side.

2 Preliminaries and Problem Formulation↩︎

2.1 System Definition↩︎

Consider an Euler-Lagrange (EL) system \(\mathcal{S}\) given as \[\begin{align} \mathcal{S}: M(x)\Ddot{x} + V(x,\dot{x}) + G(x) = \tau(t) + w(t), \label{eqn:sysdyn} \end{align}\tag{1}\] where \(x(t) = [x_1(t), \ldots, x_n(t)]^\top \in {\mathbf{X}}\subset \mathbb{R}^n\) is the system configuration, \(\tau(t) \in \mathbb{R}^n\) is the control input, and \(w(t) \in \mathbb{R}^n\) is an unknown disturbance. The terms \(M(x) \in \mathbb{R}^{n \times n}\), \(V(x,\dot{x}) \in \mathbb{R}^n\), and \(G(x) \in \mathbb{R}^n\) are the inertia, Coriolis/centrifugal, and gravity components. For brevity, we omit the functional dependence and denote the terms by \(M\), \(V\), \(G\), and \(w\).

For \(\mathcal{S}\), the control input is bounded, i.e., \(|\tau(t)| \preceq \overline{\tau}, \quad \forall t \in {\mathbb{R}}_0^+.\) This induces implicit bounds on the system dynamics [20], [21], [22]. Although the disturbance \(w\) and the system parameters \(M\), \(V\), and \(G\) are unknown, their boundedness can be used for control design. To formalize this, we introduce the following assumptions.

The Assumptions 1-4 provide the bounds on various system parameters, which will be used to derive feasibility conditions ensuring that both the STL and input constraints are satisfied.

2.2 Signal Temporal Logic↩︎

Signal Temporal Logic (STL) [1] is a formal language used to specify the spatial, temporal, and logical properties of continuous-time signals. The set of STL formulae can be recursively expressed using predicates \(\mathsf{p}\). Consider the predicate function \(h: {\mathbb{R}}^n \rightarrow {\mathbb{R}}\) to be Lipschitz continuous, and \(h(s) \geq 0 \Rightarrow \mathsf{p}:=\textsf{true}\), else \(\mathsf{p}:=\textsf{false}\). An STL formula \(\phi\) is recursively defined using predicates, Boolean logic, and temporal operators: \[\begin{align} \label{eq:STL} \phi:= \textsf{true} \;| \;\textsf{p} \;| \;\neg \phi \;| \phi_1 \land \phi_2 \;| \phi_1 \mathcal{U}_{[a,b]}\phi_2, \end{align}\tag{2}\] where \(\phi_1, \phi_2\) are STL formulae. Boolean operators for negation and conjunction are denoted by \(\neg\) and \(\land\) respectively. \(\mathcal{U}\) represents the temporal until operator in the time interval \([a,b]\) with \(a,b \in {\mathbb{R}}_0^+\) such that \(a \leq b\). The satisfaction relation \((x,t) \models \phi\) denotes a signal \(x : {\mathbb{R}}_{\geq 0} \rightarrow {\mathbb{R}}^n\), a possible state of 1 , satisfies an STL formula \(\phi\) at time \(t\). The STL semantics [1] for a signal \(x\) is recursively given by: \[\begin{align} (x,t) \models \textsf{p} \iff& h(x(t)) \geq 0, \\ (x,t) \models \neg \phi \iff& \neg((x,t) \models \textsf{p}), \\ (x,t) \models \phi_1 \land \phi_2 \iff& (x,t) \models \phi_1 \land (x,t) \models \phi_2, \\ (x,t) \models \phi_1 \mathcal{U}_{[a,b]} \phi_2 \iff& \exists \;t_1 \in [t+a, t+b], (x,t_1) \models \phi_1 \land \forall t_2 \in [t+a, t_1], (x, t_2) \models \phi_2. \end{align}\] The disjunction, eventually and always operator can be derived as \(\phi_1 \lor \phi_2 = \neg(\neg \phi_1 \land \neg \phi_2), \Diamond_{[a,b]}\phi = \textsf{true} \;\mathcal{U}_{[a,b]}\phi\) and \(\square_{[a,b]}\phi = \neg \Diamond_{[a,b]}\neg \phi\). A signal \(x\) satisfies an STL formula \(\phi\), denoted by \(x \models \phi\) if and only if \((x, 0) \models \phi\). The STL robustness metric \(\rho^\phi(x,t)\) [2] quantifies the degree of satisfaction: \(\rho^\phi(x,t) > 0\) implies \((x,t) \models \phi\) and its magnitude reflects the strength of satisfaction or violation. The robustness semantics are defined recursively as: \[\label{eq:stl95sem} \begin{align} &\rho^{\phi}(x,t) = h(x(t)), \\ &\rho^{\neg \phi}(x,t) = -\rho^{\phi}(x,t), \\ &\rho^{\phi_1 \land \phi_2}(x,t) = \min \big(\rho^{\phi_1}(x,t) \land \rho^{\phi_2}(x,t)\big),\\ & \rho^{\Diamond_{[a,b]}\phi}(x,t) = \max_{t_1 \in [t+a, t+b]}\rho^\phi(x, t_1),\\ & \rho^{\square_{[a,b]}\phi}(x,t) = \min_{t_1 \in [t+a, t+b]}\rho^\phi(x, t_1),\\ & \rho^{\phi_1 \;\mathcal{U}_{[a,b]}\phi_2} (x,t) = \max_{t_1 \in [t+a, t+b]}\min \big(\rho^\phi_1(x, t_1), \min_{t_2 \in [t+a, t_1]}\rho^{\phi_2}(x, t_2) \big). \end{align}\tag{3}\] For simplicity, robustness at \(t=0\) is written as \(\rho^\phi(x)\). We consider a finite time horizon \([0, t_f]\) over which the specification \(\phi\) to be realized, i.e., \(x:[0, t_f] \rightarrow {\mathbb{R}}^n\) such that \(x \models \phi\).

2.3 Spatiotemporal Tubes↩︎

To satisfy the STL specification, we leverage Spatiotemporal Tubes [16], [17], defined next.

2.4 Problem Statement↩︎

Given an STL specification \(\phi\) over time \(t \in [0,t_f]\) as in equation 2 , the objective is to synthesize the STTs, as introduced in Definition 1. Then, for the unknown EL system in 1 , the goal is to design a closed-form, approximation-free control law \(\tau(t)\) satisfying the input constraints \(-\bar{\tau} \preceq \tau(t) \preceq \bar{\tau},\) such that the system configuration \(x(t)\) remains constrained within the synthesized STTs for all time \(t \in [0,t_f]\). By guaranteeing the forward invariance of the STTs, the resulting trajectory satisfies the STL specification, i.e., \(x \models \phi\).

The central idea of the proposed framework is to transform STL satisfaction into a geometric constraint satisfaction problem. Rather than reasoning directly over the STL specification, we aim to represent a set of admissible trajectories through a time-varying tube and subsequently design a controller that ensures the system remains within this tube at all times.

3 Neural STT for STL specifications↩︎

The development of the proposed framework begins with the synthesis of STTs associated with the given STL specification. To this end, we first establish sufficient conditions that guarantee a time-varying ball encapsulates a subset of the trajectories satisfying the specification. These conditions form the basis for the neural STT construction presented subsequently.

Proof: The condition ?? being satisfied with \(\eta \leq 0\) implies that the tube radius is always positive, ensuring a feasible safe set of non-zero volume for all time. The condition ?? with \(\eta \leq 0\) ensures that the STL robustness remains strictly positive inside the tube. \({\mathsf{s}}(\theta)\) covers all directions of the unit sphere while \(\lambda \in [0,1]\) scales radially outward from the center of the tube to its boundary. Altogether, they span the complete ball \({\mathbb{B}}({\mathbf{c}}(t), {\mathbf{r}}(t))\) ensuring that any trajectory confined within the STT satisfies the STL specification. \(\square\)

3.1 Sample Collection and Training Procedure↩︎

It is evident that ?? has infinitely many constraints due to the continuous space-time domain, rendering the problem intractable in its original form. To obtain a finite and computationally tractable solution, we sample \(N\) points from the augmented space-time horizon \(\mathcal{W} = [0,2\pi]^{n-1} \times [0,1] \times [0, t_f]\), denoted by \(\mathsf{w}_r = (\theta_r, \lambda_r, t_r)\), \(r\in [1;N]\). We consider a ball \({\mathbb{B}}(\mathsf{w}_r, \varepsilon)\) around each sample \(\mathsf{w}_r\) with radius \(\varepsilon\), such that there exists a \(\mathsf{w}_r\) for all \((\theta, \lambda, t) \in \mathcal{W}\) satisfying \[\begin{align} \label{eq:sample} \lVert (\theta, \lambda, t) - \mathsf{w}_r \rVert \leq \varepsilon. \end{align}\tag{4}\] This ensures that the union of such balls forms a superset of the augmented space-time domain: \(\cup_{r=1}^M {\mathbb{B}}(\mathsf{w}_r, \varepsilon) \supset \mathcal{W}\).

We now seek a functional representation of the STT \(\Gamma(t)\) to satisfy these sampled constraints, \[\tag{5} \begin{align} & \forall t_r \in [0,t_f], r \in [1;M]: -{\mathbf{r}}(t_r) + {\mathbf{r}}_d \leq \eta, \tag{6} \\ & \forall x: [0, t_f] \rightarrow {\mathbb{R}}^n \;\text{s.t.,}\;x(\tau_r) = {\mathbf{c}}(\tau_r) + \lambda {\mathbf{r}}(\tau_r) {\mathsf{s}}(\theta_r), \forall (\theta_r, \lambda_r, t_r) \in \mathcal{W}, r \in [1;M] : -\rho^\phi(x) < \eta.\tag{7} \end{align}\] Since the functional form of the tube center and radius is not known a priori, we model them using a neural network. Although a standard artificial neural network (ANN) can approximate the time-varying ball, training only at discrete samples does not formally guarantee smoothness or inter-sample consistency. This is undesirable because the STT center \({\mathbf{c}}(t)\) and radius \({\mathbf{r}}(t)\) are required to evolve smoothly over time. To overcome the limitation, we use a physics-informed neural network (PINN) framework, namely Physics-informed Neural Spatiotemporal Tube (PINSTT), \[\begin{align} \label{eqn:pinstt} \Gamma (t;\Upsilon) = {\mathbb{B}}({\mathbf{c}}(t;\Upsilon), {\mathbf{r}}(t;\Upsilon)), \end{align}\tag{8}\] with center \({\mathbf{c}}(t;\Upsilon) = [{\mathbf{c}}_1(t;\Upsilon), \ldots, {\mathbf{c}}_n(t;\Upsilon)]^\top \in {\mathbb{R}}^n\), radius \({\mathbf{r}}(t;\Upsilon) \in {\mathbb{R}}\), and the trainable parameters \(\Upsilon\).

During training of the PINN, the finite set of constraints in 5 is encoded as physics-based penalties. Specifically, the loss function that is to be minimized is given by \(\mathsf{L}(\Upsilon)\), which only consists of the physics-based sub-losses formulated from the constraints. The sub-loss terms are defined as: \[\label{loss:phys951} \begin{align} \mathsf{L}_1(\Upsilon) &= \sum_{r=1}^M \text{ReLU} \big(-{\mathbf{r}}(t_r; \Upsilon) + {\mathbf{r}}_d - \hat{\eta} \big), \\ \mathsf{L}_2(\Upsilon) &= \sum_{r=1}^M \text{ReLU} \big(-\rho^\phi(y(\mathsf{w}_r)) + \delta - \hat{\eta} \big), \end{align}\tag{9}\] where \(\text{ReLU}(x):= \max(0,x)\), and the choice of \(\hat{\eta}\) is described in the Algorithm 1 while \(\delta \in {\mathbb{R}}^+\) is a small positive quantity to ensure the strict inequality corresponding to condition 7 .

To ensure that the tube varies smoothly over time, we require \({\mathbf{c}}(t; \Upsilon)\) and \({\mathbf{r}}(t; \Upsilon)\) to be Lipschitz continuous, with user-defined bounds \(\mathcal{L}_{{\mathbf{c}}}\) and \(\mathcal{L}_{{\mathbf{r}}}\), respectively. The detailed procedure of choosing the parameters \(\mathcal{L}_c\) and \(\mathcal{L}_r\) will be discussed in Section 4. This assumption is mild in practice, as Lipschitz continuity prevents abrupt temporal changes in the tube and, in turn, leads to smoother control inputs. In addition, neural networks equipped with slope-restricted activation functions are inherently Lipschitz continuous. To enforce these bounds, we use the automatic differentiation property of the PINNs [23] and ensure the derivative of the output is bounded by the user-defined bounds. Accordingly, we introduce two additional sub-loss functions, defined as: \[\label{loss:phys952} \begin{align} \mathsf{L}_3(\Upsilon) &= \sum_{r=1}^M \text{ReLU}(\| \dot{{\mathbf{c}}}(t_r; \Upsilon) \| - \mathcal{L}_c), \\ \mathsf{L}_4(\Upsilon) &= \sum_{r=1}^M \text{ReLU} (| \dot{{\mathbf{r}}}(t_r; \Upsilon) | - \mathcal{L}_r). \end{align}\tag{10}\] Therefore, the combined loss is given by \[\begin{align} \label{eq:loss95phys} \mathsf{L}(\Upsilon) = \sum_{i=1}^4 w_i \mathsf{L}_i(\Upsilon), w_i\in {\mathbb{R}}_0^+, i \in [1;4], \end{align}\tag{11}\] where \(w_i\) are the weights corresponding to the sub-loss terms. Algorithm 1 summarizes the training procedure.

3.2 Formal Verification of the Network↩︎

We now verify that the trained PINSTT captures the STL specification over the entire continuous space-time horizon. From [24], we know that the STL robustness function \(\rho^\phi(x)\) is Lipschitz continuous with respect to signal as all predicate functions are Lipschitz continuous and the signal evolves within the bounded subset \({\mathbf{X}}\) of the state space \({\mathbb{R}}^n\), which means there exists \(\mathcal{L}_\rho \in {\mathbb{R}}^+\) such that for any \(x_1,x_2 : [0, t_f] \rightarrow {\mathbf{X}}\subset {\mathbb{R}}^n\), \[\lVert \rho^\phi(x_1) - \rho^\phi(x_2) \rVert \leq \mathcal{L}_\rho \lVert x_1 - x_2 \rVert_{[0,t_f]}.\] Clearly, in our setting, the signal \(x(t) = {\mathbf{c}}(t;\Upsilon) + \lambda {\mathbf{r}}(t; \Upsilon)\mathsf{s}(\theta)\) is confined within the tube, which is confined within the state-space, it ensures the robustness metric \(\rho^\phi(x)\) admits a finite Lipschitz constant over the domain.

Proof: We first get the Lipschitz constants with respect to the individual parameters \(\theta\) and \(\lambda\), and then combine the results to obtain the overall Lipschitz constant.

From [24], we know that there exists \(\mathcal{L}_\rho \in {\mathbb{R}}^+\) such that \(| \rho^\phi(x_1, \ldots, x_k, \ldots, x_n) - \rho^\phi(\hat{x}_1, \ldots, \hat{x}_k, \ldots, \hat{x}_n)| \leq \mathcal{L}_\rho |x_k -\hat{x}_k|\). \(\lVert\mathsf{s}(\theta)\rVert \leq 1\) for all \(\theta\) with Lipschitz bound \(\mathcal{L}_s\) and \(\Bar{{\mathbf{r}}} = \max_{t \in [0,t_f]}{\mathbf{r}}(t_r; \Upsilon)\) is finite.

• For some fixed \(\lambda \in [0,1]\), for any \(\theta, \hat{\theta} \in [0,2\pi]^{n-1}\), we have \(\lvert \mu(\theta,\lambda) - \mu(\hat{\theta},\lambda) \rvert \leq \mathcal{L}_\rho \Bar{{\mathbf{r}}} \mathcal{L}_s \|\theta - \hat{\theta}\|\).

• For some fixed \(\theta \in [0,2\pi]^{n-1}\), for any \(\lambda, \hat{\lambda} \in [0,1]^n\), we have \(\lvert \mu(\theta,\lambda) - \mu(\theta, \hat{\lambda}) \rvert \leq \mathcal{L}_\rho \Bar{{\mathbf{r}}} |\lambda - \hat{\lambda}|\).

Now combining both of them, for any \((\theta, \lambda), (\hat{\theta}, \hat{\lambda}) \in [0,2\pi]^{n-1} \times [0,1]\), we can have: \[\begin{align} &| \mu(\theta, \lambda) \!-\! \mu(\hat{\theta}, \hat{\lambda})| = \lvert \mu(\theta,\lambda) \!-\! \mu(\hat{\theta},\lambda) \rvert \!+\! \lvert \mu(\hat{\theta},\lambda) \!-\! \mu(\hat{\theta},\hat{\lambda}) \rvert \leq \mathcal{L}_\rho \Bar{{\mathbf{r}}} \mathcal{L}_s\lVert \theta \!-\! \hat{\theta}\rVert + \mathcal{L}_\rho \Bar{{\mathbf{r}}} |\lambda \!-\! \hat{\lambda}| \leq \mathcal{L}_\mu \lVert (\theta, \lambda) \!-\! (\hat{\theta}, \hat{\lambda}) \rVert, \end{align}\] where \(\mathcal{L}_\mu:= \mathcal{L}_\rho \Bar{{\mathbf{r}}} \sqrt{\mathcal{L}_s^2+1}\), which is obtained using Cauchy-Schwarz inequality. This completes the proof. \(\square\)

We now present the main theorem of the section that the PINSTT obtained after training using the sampled points is formally verified to encapsulate the STL specification over the continuous space-time horizon.

Proof: From 4 , for every \(t \in [0,t_f]\), there exists a sampled point \(t_r\) such that \(|t - t_r| \leq \varepsilon.\) Therefore, for all \(t \in [0,t_f], \;-{\mathbf{r}}(t; \Upsilon) + {\mathbf{r}}_d \leq -{\mathbf{r}}(t; \Upsilon) + {\mathbf{r}}(t_r; \Upsilon) - {\mathbf{r}}(t_r; \Upsilon) + {\mathbf{r}}_d \leq \hat{\eta} + \mathcal{L}_r \varepsilon \leq \hat{\eta} + \mathcal{L} \varepsilon \leq 0\).

Similarly, from 4 , for every \(\mathsf{w} \!=\! (\theta,\lambda,\tau) \in \mathcal{W}\), there exists \(\mathsf{w}_r \!=\! (\theta_r,\lambda_r,t_r)\), s.t., \(\|(\theta,\lambda,t) \!-\! (\theta_r,\lambda_r,t_r)\| \!\leq\! \varepsilon\). Define \(y, \hat{y}\) as \(y(\mathsf{w}) = {\mathbf{c}}(\tau; \Upsilon) + \lambda {\mathbf{r}}(t; \Upsilon)\mathsf{s}(\theta), \hat{y}(\mathsf{w}_r) = {\mathbf{c}}(t_r; \Upsilon) + \lambda_r {\mathbf{r}}(t_r; \Upsilon)\mathsf{s}(\theta_r)\). Let, \(\bar{y}:[0,t_f] \rightarrow {\mathbb{R}}^n\) be the ZOH reconstruction of \(\hat{y}\) over the sampled points. Then, \[\begin{align} - \rho^\phi(y) &= - \rho^\phi(y) - \rho^\phi(\bar{y}) + \rho^\phi(\bar{y}) - \rho^\phi(\hat{y}) + \rho^\phi(\hat{y}) \\ & \leq \| \mu(\theta, \lambda) - \mu(\theta_r, \lambda_r) \| + \hat{\eta} + \max_{t \in [0,t_f], |t - t_r| \leq \varepsilon} \mathcal{L}_\rho \|\bar{y}_r(t) - {y}_r(t_r)\| \\ & \leq \hat{\eta} + \mathcal{L}_\mu \lVert (\theta, \lambda) - (\theta_r, \lambda_r) \rVert + \mathcal{L}_\rho(\mathcal{L}_c + \mathcal{L}_r)|t -t_r| \; \leq \hat{\eta} + \sqrt{\mathcal{L}_\mu^2 + \mathcal{L}_\rho^2(\mathcal{L}_c + \mathcal{L}_r)^2}\varepsilon \leq \hat{\eta} + \mathcal{L}\varepsilon \leq 0. \end{align}\] Therefore, \(\rho^\phi(y) > 0\) for all \(y:[0,t_f] \rightarrow {\mathbb{R}}^n\), such that \(y(t) \in {\mathbb{B}}({\mathbf{c}}(t; \Upsilon), {\mathbf{r}}(t; \Upsilon))\) for all \(t \in [0, t_f]\). This satisfies the conditions of Definition 1, completing the proof. \(\square\)

4 Controller Synthesis↩︎

The controller is developed using a two-step procedure inspired by a backstepping-like design. First, a reference velocity is designed to guide the system configuration within the tubes. Then, an acceleration-level controller is constructed to track this reference while respecting input constraints. For convenience, the EL system 1 is rewritten as \[\begin{align} \dot{x} &= v, \tag{12} \\ \dot{v} &= V_M(x,v) + M(x)^{-1}\tau + M(x)^{-1}d, \tag{13} V_M(x,v) = -M(x)^{-1}(V(x,v)+G(x)). \end{align}\]

Stage I: Velocity-level Control↩︎

The goal of this stage is to design a reference velocity \(v_r(t)\) that ensures the system configuration remains within the prescribed STT.

To enforce the system remains within the ball-shaped STTs \(\Gamma(t)\) for all time \(t \in [0;t_f]\), the reference velocity vector \(v_r(x,t)\) is considered as \[\label{eqn:bdvelcon95ball} v_r(t) = -\frac{x(t) - {\mathbf{c}}(t)}{\|x(t) - {\mathbf{c}}(t)\|} \Psi(e_x) \overline{v}, \quad \overline{v} \in {\mathbb{R}}^+\tag{14}\] where \(e_x(x,t) := (\|x(t) - {\mathbf{c}}(t)\|) / {\mathbf{r}}(t)\) is the normalized position error.

Stage II: Acceleration-level Control↩︎

In this stage, the objective is to track the reference velocity \(v_{r}(t)\) from Stage I, while ensuring that the control input remains bounded. To achieve this, the velocity tracking error \(e_v(t) = v(t) - v_{r}(t)\) is constrained within exponentially decaying funnel constraints \(\gamma_v: {\mathbb{R}}_0^+ \rightarrow {\mathbb{R}}^n\) \[\label{eqn:rhov} \gamma_v(t) = e^{-\mu_v t}(p_v-q_v) + q_v,\tag{15}\] as \[\label{eqn:fun2} -\gamma_v(t) \prec e_v(t) \prec \gamma_v(t).\tag{16}\] Here \(p_v \in {\mathbb{R}}^n\) is the initial funnel width, with \(|e_v(0)| \preceq p_v\), \(q_v \in {\mathbb{R}}^n\) is the steady state limit, with \(0^{n \times 1} \prec q_v \prec p_v\), and \(\mu_v \succeq \boldsymbol{0}^{n \times n}\) determines the funnel decay rate.

This leads to the acceleration-level control input \(\tau(t)\) \[\label{eqn:bdcontrol} \tau(t) = -\text{diag}(\Psi(\varepsilon_v))\overline{\tau},\tag{17}\] where \(\varepsilon_v(t) = \text{diag}(\gamma_{v})^{-1}e_v(t)\) is the normalized velocity error and \(\Psi\) is the same bounded transformation function, defined in [26], and \(\overline{\tau} \in {\mathbb{R}}^n\) is the maximum permissible torque.

We now derive feasibility conditions under which the system remains within the synthesized STT under the available actuator limits.

Feasibility Condition↩︎

We now derive feasibility conditions under which the velocity tracking error remains within the prescribed funnel bounds while ensuring that the synthesized STT is trackable under the available actuator limits. Since the tube center and radius evolve over time with rates bounded by \(L_c\) and \(L_r\), the system must possess sufficient velocity and actuation authority to follow this evolution. Therefore, the allowable values of \(L_c\) and \(L_r\) are fundamentally coupled with the velocity and input constraints, giving rise to the following feasibility conditions.

Stage I: From Section 3, we have already ensured that \(\|\dot{{\mathbf{c}}}(t)\|\) and \(|\dot{{\mathbf{r}}}(t)|\) is upper bounded by \(\mathcal{L}_c\) and \(\mathcal{L}_r\). We define \(\overline{\Gamma}:=\mathcal{L}_c + \mathcal{L}_r\) as the upper bound on the rate of variation of the tube over time, which dictates the maximum permissible velocity \(\overline{v}\) given by \[\label{eqn:feas1} \overline{v} \geq \overline{\Gamma} + \|p_v\|,\tag{18}\] where \(p_v \in {\mathbb{R}}^+\) is the starting position of the upper curve of the funnel. This guarantees that the system possesses sufficient actuation capacity to track the evolving tube boundaries \(\overline{\Gamma}\) while rejecting the worst-case perturbation (\(|e_v| \prec p_v\)). It is evident that using the maximum permissible velocity \(\bar{v}\), one can choose \(\mathcal{L}_c\) and \(\mathcal{L}_r\) such that 18 holds.

Stage II: Given the funnel constraint \[\gamma_v(t) = e^{-\mu_vt}(p_v-q_v)+q_v,\] and system dynamics in 1 with Assumptions 1-4, the maximum permissible torque \(\overline{\tau}\) should adhere to the following constraint: \[\label{eqn:feas2} \overline{\tau} \succeq \frac{1}{\underline{m}} \left( \max(-\underline{V_M}, \overline{V_M}) + \underline{m}_i\overline{w} + \mu_v(p_v-q_v) + \overline{a}_r \right),\tag{19}\] where given the bounded transformation function, in [26], we select an upper bound \(\overline{a}_r \in {\mathbb{R}}^n\), such that \(|\dot{v}_r| \preceq \overline{a}_r\).

The following theorem formally summarizes the input-constrained approximation-free feedback controller.

Proof: The proof is divided into two stages. For the first stage, we show that the reference velocity vector \(v_r(t)\) in Equation 14 enforces the system state \(x(t)\) to be confined within the STT \(\Gamma(t)\), \(\forall t \in {\mathbb{R}}_0^+\). In stage II, we prove that the control law \(\tau(t)\) in 17 keeps the velocity tracking error \(e_v(t)\) within the funnel \([-\gamma_v(t), \gamma_v(t)]\) for all \(t \in {\mathbb{R}}_0^+\) 16 . In both stages, we will show the result using the contradiction method.

Stage 1: Let the first time instance when the system state \(x(t)\) exits the STT \(\Gamma(t)\) due to the applied velocity input \(v_r(t)\) as of 14 is denoted by \({t_{\times}}\). Then, \[\begin{gather} \label{Eq:inqe95tx95ball} \|x(t) - {\mathbf{c}}(t)\| < {\mathbf{r}}(t), \text{ for all } t \in [0, {t_{\times}}). \end{gather}\tag{20}\] As the \(x(t)\) approaches the STT boundary, \(\|x(t) - {\mathbf{c}}(t)\| \rightarrow {\mathbf{r}}(t)\). For crossing the boundary, we have the following implications: \[\begin{align} &\|x(t) - {\mathbf{c}}(t)\| < {\mathbf{r}}(t) \Rightarrow \|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t) \\ \Rightarrow & \lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} \frac{d}{dt} \|x(t) - {\mathbf{c}}(t)\| > \dot{{\mathbf{r}}}(t) \\ \Rightarrow &\lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} (x(t) - {\mathbf{c}}(t))^\top (\dot{x}(t) - \dot{{\mathbf{c}}}(t)) > \dot{{\mathbf{r}}}(t)\|x(t)-{\mathbf{c}}(t)\| \\ \Rightarrow &\lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} (x(t) - {\mathbf{c}}(t))^\top \dot{x}(t) > \lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)}(x(t) - {\mathbf{c}}(t))^\top \dot{{\mathbf{c}}}(t) + \dot{{\mathbf{r}}}(t)\|x(t) - {\mathbf{c}}(t)\|. \end{align}\] Substituting the dynamics from Equation 12 with velocity input from 14 , \[\begin{align} &\lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} (x(t) - {\mathbf{c}}(t))^\top v > \lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)}(x(t) - {\mathbf{c}}(t))^\top \dot{{\mathbf{c}}}(t)+\dot{{\mathbf{r}}}(t)\|x(t) - {\mathbf{c}}(t)\|\\ \Rightarrow &\lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} \!\!(x(t) \!-\! {\mathbf{c}}(t))^\top \Bigg(-\frac{(x(t) \!-\! {\mathbf{c}}(t))}{\|x(t) \!-\! {\mathbf{c}}(t)\|} \|\bar{v}\|+e_v\Bigg) \!> \lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} \!\!(x(t) \!-\! {\mathbf{c}}(t))^\top \dot{{\mathbf{c}}}(t)+\dot{{\mathbf{r}}}(t)\|x(t) \!-\! {\mathbf{c}}(t)\| \\ \Rightarrow &\lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} \|x(t) - {\mathbf{c}}(t)\| (-\|\bar{v}\| + \|p_v\|) > \lim_{\|x(t) - {\mathbf{c}}(t)\| \uparrow {\mathbf{r}}(t)} \|x(t) - {\mathbf{c}}(t)\|(\|\dot{{\mathbf{c}}}(t)\| + \dot{{\mathbf{r}}}(t)) \\ \Rightarrow &\|\bar{v}\| < \overline{\Gamma} + \|p_v\|. \end{align}\] However, this contradicts the feasibility constraint in Equation 18 . Hence, \(\|x(t) - {\mathbf{c}}(t)\| \nrightarrow {\mathbf{r}}(t), \forall t \in [0,{t_{\times}})\), i.e., \(x(t)\) never approaches the STT boundary over \(t \in [0,{t_{\times}})\). Consequently, due to the continuity of \(x(t)\), it can be concluded that there is no \({t_{\times}}\) at which \(x(t)\) crosses the STT boundary.

Therefore, the reference velocity vector \(v_r\) in 14 constrains \(x(t)\) within the STT, \(\|x(t) - {\mathbf{c}}(t)\| < {\mathbf{r}}(t), \forall t \in {\mathbb{R}}^+_0.\)

Stage 2: Let \({t_{\times}}\) be the first time instance when the velocity error \(e_v(t)\), on the application of input \(\tau(t)\) as in 17 , violates 16 , i.e., \(\exists i \in [1;n]\), \[e_{v,i}({t_{\times}}) \leq -\gamma_{v,i}({t_{\times}}) \text{ or } e_{v,i}({t_{\times}}) \geq \gamma_{v,i}({t_{\times}}).\] Then, for all \((t,i) \in [0, {t_{\times}}) \times [1;n],\) \[\begin{gather} \label{Eq:inqe95tv} -\gamma_{v,i}(t) < e_{v,i}(t) < \gamma_{v,i}(t). \end{gather}\tag{21}\] We will consider the following two cases for \(t \in [0,{t_{\times}})\).

Case I. For some \(i \in [1;n]\), \(e_{v,i}(t)\) approaches the upper funnel constraint, i.e., \(e_{v,i}(t) \rightarrow \gamma_{v,i}(t) \Rightarrow e_{v,i}(t) - \gamma_{v,i}(t) =: \overline{\delta}_{v,i} \rightarrow 0\). Following 21 : \[\begin{align} &e_{v,i}(t) < \gamma_{v,i}(t) \Rightarrow \overline{\delta}_{v,i} \uparrow 0 \Rightarrow \lim_{\overline{\delta}_{v,i} \uparrow 0} \frac{d}{dt} \overline{\delta}_{v,i} > 0 \\ \Rightarrow &\lim_{\overline{\delta}_{v,i} \uparrow 0} \dot{e}_{v,i}(t) > \lim_{\overline{\delta}_{v,i} \uparrow 0} \dot{\gamma}_{v,i}(t) > -\mu_{v,i}(p_{v,i}-q_{v,i}) \\ \Rightarrow &\lim_{\overline{\delta}_{v,i} \uparrow 0} \dot{v}_{i}(t) > -\mu_{v,i}(p_{v,i}-q_{v,i}) + \dot{v}_{r,i}(t) > -\mu_{v,i}(p_{v,i}-q_{v,i}) - \overline{a}_{r,i}. \end{align}\] Therefore, there exists \(i \in [1;n]\), such that \[\begin{gather} \label{eqn:dv95b1} \lim_{\overline{\delta}_{v,i} \uparrow 0} \dot{v}_{i}(t) > -\mu_{v,i}(p_{v,i}-q_{v,i}) - \overline{a}_{r,i}. \end{gather}\tag{22}\] Since, \(\lim_{\overline{\delta}_{v,i} \uparrow 0} \varepsilon_{v,i}(t) = 1\), we obtain \(\lim_{\overline{\delta}_{v,i} \uparrow 0} \tau_{i}(t) = -\overline{\tau}_{i}\). Using the dynamics 13 and feasibility condition 19 \[\begin{align} \lim_{\overline{\delta}_{v,i} \uparrow 0} \dot{v}_{i}(t) \leq \overline{V}_{M,i} - \underline{m} \overline{\tau}_i + \underline{m}_i\overline{d}_i \leq -\mu_{v,i}(p_{v,i} - q_{v,i}) - \overline{a}_{r,i} \end{align}\] which contradicts 22 . Hence, \(e_{v,i}(t) \nrightarrow \gamma_{v,i}(t), \forall (t,i) \in [0,{t_{\times}}) \times [1;n]\), i.e., the velocity error \(e_v(t)\) never approaches the upper funnel constraint over \(t \in [0,{t_{\times}})\) in any dimension.

Case II. For some \(i \in [1;n]\), \(e_{v,i}(t)\) approaches the lower funnel constraint, i.e., \(e_{v,i}(t) \rightarrow -\gamma_{v,i}(t) \Rightarrow e_{v,i}(t)+\gamma_{v,i}(t) =: \underline{\delta}_{v,i} \rightarrow 0\). Following 21 : \[\begin{align} &e_{v,i}(t) > -\gamma_{v,i}(t) \Rightarrow \underline{\delta}_{v,i} \downarrow 0 \Rightarrow \lim_{\underline{\delta}_{v,i} \downarrow 0} \frac{d}{dt} \underline{\delta}_{v,i} < 0 \\ \Rightarrow &\lim_{\underline{\delta}_{v,i} \downarrow 0} \dot{e}_{v,i}(t) < \lim_{\underline{\delta}_{v,i} \downarrow 0} -\dot{\gamma}_{v,i}(t) < \mu_{v,i}(p_{v,i}-q_{v,i}) \\ \Rightarrow &\lim_{\underline{\delta}_{v,i} \uparrow 0} \dot{v}_{i}(t) < \mu_{v,i}(p_{v,i}-q_{v,i}) + \dot{v}_{r,i}(t) < \mu_{v,i}(p_{v,i}-q_{v,i}) + \overline{a}_{r,i}. \end{align}\] Therefore, there exists \(i \in [1;n]\), such that \[\begin{gather} \label{eqn:dv95b2} \lim_{\underline{\delta}_{v,i} \uparrow 0} \dot{v}_{i}(t) < \mu_{v,i}(p_{v,i}-q_{v,i}) + \overline{a}_{r,i}. \end{gather}\tag{23}\] Since, \(\lim_{\underline{\delta}_{v,i} \downarrow 0} \varepsilon_{v,i}(t) = -1\), we obtain \(\lim_{\underline{\delta}_{v,i} \downarrow 0} \tau_{i}(t) = \overline{\tau}_i.\) Using dynamics 13 and feasibility condition 19 \[\begin{align} \lim_{\underline{\delta}_{v,i} \downarrow 0} \dot{v}_{i}(t) \geq \underline{V}_{M,i} + \underline{m} \overline{\tau}_i - \underline{m}_i\overline{d}_i \geq \mu_{v,i}(p_{v,i} - q_{v,i}) + \overline{a}_{r,i} \end{align}\] which contradicts 23 . Hence, \(e_{v,i}(t) \nrightarrow -\gamma_{v,i}(t), \forall (t,i) \in [0,{t_{\times}}) \times [1;n]\), i.e., the velocity error \(e_v(t)\) never approaches the lower funnel constraint over \(t \in [0,{t_{\times}})\) in any dimension.

Thus, over \(t \in [0, {t_{\times}}])\), \(e_{v,i}(t)\) never approaches the funnel constraints \(-\gamma_{v,i}(t)\) and \(\gamma_{v,i}(t)\) for all \(i \in [1;n]\). Consequently, due to the continuity of \(e_v(t)\), it can be concluded that there is no \({t_{\times}}\) at which \(e_{v,i}(t)\) violates the funnel constraints \(-\gamma_{v,i}(t)\) and \(\gamma_{v,i}(t)\) for all \(i \in [1;n]\).

Therefore, combining Stages I and II, the bounded control input \(\tau(t)\) in 17 , under feasibility conditions 18 and 19 , ensures that the system state \(x(t)\) evolves within the STTs \(\Gamma(t)\). This concludes the proof. \(\square\)

5 Case Study↩︎

To validate the effectiveness of the proposed approach, we present three different case studies: a 2D mobile robot, a 3D UAV, a \(7\) DOF Manipulator, and a multi-agent setup. All experiments were conducted in PyTorch (Python 3.10) on a Windows machine with an Intel Core i7-14700 CPU, 32 GB RAM, and an NVIDIA GeForce RTX 3080 Ti GPU. All the videos can be found here ².

In case studies, each region \(M\) is a hyperrectangle with center \(\mathrm{center}(M)\) and size \(d_M\), and is represented by the predicate \(\tilde{M} := |x - \mathrm{center}(M)|_\infty < d_M\).

5.1 Omnidirectional Robot↩︎

For the first case study, we consider the omnidirectional robot whose dynamics is given by: \[\label{eq:omni} \begin{align} \begin{bmatrix} \dot{x} & \dot{y} \end{bmatrix} &= \begin{bmatrix} v_x & v_y \end{bmatrix} + d_1(t), \\ \begin{bmatrix} \dot{v}_x & \dot{v}_y \end{bmatrix} &= \begin{bmatrix} a_x & a_y \end{bmatrix} + d_2(t). \end{align}\tag{24}\]

We consider the velocity and acceleration limits in each dimension are set to \(0.15 \;m/s\) and \(0.5 \;m/s^2\), respectively. We consider \(\mathcal{L}_c = 0.08\) and \(\mathcal{L}_r = 0.01\), satisfying condition 18 . Now, for the robot, we define the following STL task: \[\begin{align} \psi &= \square_{[0, 280]} \big((\tilde{{\mathbf{S}}} \Rightarrow \Diamond_{[60, 80]}\tilde{{\mathbf{T}}}_1) \land (\tilde{{\mathbf{T}}}_1 \Rightarrow \Diamond_{[60, 80]}\tilde{{\mathbf{T}}}_2) \land (\tilde{{\mathbf{T}}}_2 \Rightarrow \Diamond_{[60, 80]}\tilde{{\mathbf{T}}}_1) \big) \land \Diamond_{[345, 355]} \square_{[0, 10]}\tilde{{\mathbf{G}}} \land \square_{[0, 360]} \neg \tilde{{\mathcal{O}}}, \end{align}\] with \({\mathbf{S}}= {\mathbb{B}}([0.5,0.5],0.15), {\mathbf{T}}_1 = {\mathbb{B}}([2.5, 1.5],0.15), {\mathbf{T}}_2 = {\mathbb{B}}([0.5,2.5], 0.15), {\mathbf{G}}= {\mathbb{B}}([2.75, 2.75],0.15)\) and \({\mathcal{O}}= {\mathbb{B}}([1.25, 0.5], 0.15) \cup {\mathbb{B}}([1.5, 1],0.25) \cup {\mathbb{B}}([1, 2],0.25) \cup {\mathbb{B}}([2, 2.5], 0.15)\). This specification captures a surveillance task in which the omnibot, starting from the initial region \({\mathbf{S}}\), must repeatedly visit the targets \({\mathbf{T}}_1\) and \({\mathbf{T}}_2\) in sequence every \(60-80\) seconds until \(280\) seconds have elapsed. After completing this, the robot must reach the goal G between \(345\) and \(355\) seconds, while avoiding the obstacles \({\mathcal{O}}\) throughout the \(360\)-second mission. To test the robustness of our approach, we also introduce unknown but bounded disturbances. We first collect samples from the augmented state-space as described in 4 and apply Algorithm 1 to obtain the PINSTT that encapsulates the STL specification. Then, start the robot inside the tube and apply 14 and 17 to the robot such that it remains within the tube and moves along it to satisfy the STL specification.

The offline computation time to obtain the STT through the training of PINN is 51.410 seconds, while the per step online control synthesis time is \(3.17 \;\mu\)sec.

We experimentally validated the approach using a hardware setup with an Agile LIMO robot. To test the robustness of our approach, we have performed experiments with nominal control and payload-variation control by attaching a 1 kg payload on top of the robot. The hardware video is available at Video Link with snapshots of the robot with the learned STT is shown in Figure 2 while the control inputs are shown in Figure 3. The control effort occasionally spikes within the prescribed limits due to wheel slip near the tube boundary.

5.2 Quadrotor↩︎

We next evaluate the framework on a Quadrotor operating in a 3D environment with second-order dynamics [27]: \[\label{eq:drone} \begin{align*} \begin{bmatrix} \dot{x} & \dot{y} & \dot{z} \end{bmatrix} &= \begin{bmatrix} v_x & v_y & v_z \end{bmatrix} + d_1(t), \\ \begin{bmatrix} \dot{v}_x & \dot{v}_y & \dot{v}_z \end{bmatrix} &= \begin{bmatrix} a_x & a_y & a_z \end{bmatrix} + d_2(t). \end{align*}\tag{25}\]

For the drone, the velocity and acceleration limits are set as \(2 \;m/s\) and \(4 \;m/s^2\) in each dimension respectively. Therefore, we have considered \(\mathcal{L}_c = 1\) and \(\mathcal{L}_r = 0.5\) and the funnel as \(\gamma_v(t) = (0.4-0.002)e^{-2t} + 0.002\). So, the feasibility condition 18 has been satisfied as \(\overline{v} = 2 > \bar{\Gamma} + p_v = 1+0.5+0.4 = 1.9\). We consider the transformation function \(\Psi(x)\) to be \(\tanh(5x^3)\). Therefore, with the choice of \(\bar{a}_r = 2.5\), the feasibility condition 19 is satisfied with some bounded disturbance. Now STL specification is given as: \[\begin{align} \psi = \tilde{{\mathbf{S}}} \Rightarrow \Diamond_{[0, 10]}(\tilde{{\mathbf{T}}}_1 \lor \tilde{{\mathbf{T}}}_2) \land \Diamond_{[19, 20]} \tilde{{\mathbf{G}}} \land \square_{[0, 20]} \neg \tilde{{\mathcal{O}}}, \end{align}\] where \({\mathbf{S}}= {\mathbb{B}}([1, 1, 1], 0.5), {\mathbf{T}}_1 = {\mathbb{B}}([8, 2, 2], 0.5), {\mathbf{T}}_2 = {\mathbb{B}}([4, 4, 4], 0.5), {\mathbf{G}}= {\mathbb{B}}([8, 8, 8], 0.5)\). The unsafe set \({\mathcal{O}}\) is a union of multiple static cylindrical obstacles centered at \([2,2.5], [6,3], [6,6], [3,5]\) with radius \(0.5\). This STL formula specifies a sequential temporal task where the drone, starting from the initial region \({\mathbf{S}}\), must eventually reach either region \({\mathbf{T}}_1\) or \({\mathbf{T}}_2\) within 0-10 seconds, and subsequently proceed to the goal region \({\mathbf{G}}\) within \(19-20\) seconds, while always avoiding the obstacles \({\mathcal{O}}\). Figure 4 shows the quadrotor trajectory satisfying the given STL specification while the control input and velocity are bounded within the specified bounds. The simulation video is available in the Video Link. The offline PINSTT computation time is 5.284 seconds, while the per-step online control synthesis time is \(3.41 \;\mu\)sec.

5.3 7 DOF Franka Research 3 Manipulator↩︎

For the third case study, we use a 7-DOF Franka Emika Research 3 robot with joint limits \(\overline{v} = 2.5 \;rad/s\) for all the joints and \(\overline{\tau} = [10, 10, 10, 10, 5, 5, 2]^\top \;N/m\). We define a sequential reachability task for the manipulator, defined by the following STL logic in its task-space: \[\begin{align} \psi &= \square_{[0, 120]}\big((\tilde{{\mathbf{S}}} \Rightarrow \Diamond_{[18,23]} \tilde{{\mathbf{T}}}_1 \land (\tilde{{\mathbf{T}}}_1 \Rightarrow \Diamond_{[18,23]} \tilde{{\mathbf{T}}}_2) \land (\tilde{{\mathbf{T}}}_2 \Rightarrow \Diamond_{[18,23]} \tilde{{\mathbf{T}}}_3) \land (\tilde{{\mathbf{T}}}_3 \Rightarrow \Diamond_{[18,23]} \tilde{{\mathbf{T}}}_1) \land (\tilde{{\mathbf{T}}}_1 \Rightarrow \Diamond_{[18,23]} \tilde{{\mathbf{S}}}) \big). \end{align}\] To ensure the feasibility conditions, we have chosen \(\mathcal{L}_c = 1.5\) and \(\mathcal{L}_r = 0.5\). The end-effector positions are chosen in a way such that the joint configuration adheres to their respective bounds. We have tested our algorithm in three different categories: (a) nominal sequential reachability, (b) payload variation (attaching a water bottle to one of the links) to illustrate robustness to unknown dynamics, and (c) external disturbances. Figure 5 (b) shows that the control inputs (applied joint torques) for all the cases are bounded within the prescribed limits for each joint, while the experiment video can be found in the Video Link. The offline PINSTT computation takes roughly one minute, while the per-step online control synthesis time is \(5.42\;\mu\)sec.

Additional planning and control mechanisms are required to guarantee STL satisfaction, prescribed-time reachability, and robustness against bounded disturbances.

6 Comparison↩︎

6.1 Qualitative Comparison↩︎

To further highlight the strengths of the proposed framework, we qualitatively compare it with representative STL planning and control approaches. While sampling-based planners such as RRT* [28] can generate collision-free paths, they require an additional tracking controller to execute the planned trajectory and do not provide formal guarantees. MPC-based methods [10] can accommodate full STL specifications while explicitly handling input constraints and bounded disturbances; however, they require an accurate system model and rely on computationally intensive online optimization. Similarly, CBF-based approaches [29] provide formal safety guarantees and can incorporate actuator limits and bounded disturbances through optimization-based formulations, but they require known system dynamics and are generally limited to a fragment of STL specifications. PPC-based approaches [12] admit closed-form controllers and can handle unknown dynamics and bounded disturbances, but are again applicable only to restricted STL fragments. Likewise, MILP-based approaches [8] can express the full STL language, but require known system dynamics and computationally expensive online optimization. Our previous STT framework [17] supports the full class of STL specifications for unknown systems under bounded disturbances through a closed-form controller; however, it does not explicitly account for actuator limits during tube synthesis or controller design. In contrast, the proposed PINSTT framework simultaneously supports the full class of STL specifications, unknown dynamics, bounded disturbances, and prescribed input constraints through a bounded closed-form controller, while avoiding online optimization. A qualitative comparison is summarized in Table 1.

6.2 Quantitative Comparison↩︎

We evaluate the proposed framework on two benchmark STL tasks, stlcg-1 and stlcg-2, introduced in [6], together with their simplified STL fragment counterparts considered in [30]: \[\begin{align} &\text{stlcg-1:} (\Diamond_{[0, 15]}\square_{[0,5]}\tilde{\mathbf{R}}) \land (\Diamond_{[0, 15]}\square_{[0,5]}\tilde{\mathbf{G}}) \land (\square_{[0,15]}\neg \tilde{\mathbf{B}}) \\ &\text{stlcg-2:}(\Diamond_{[0, 15]}\square_{[0,5]}\tilde{\mathbf{Y}}) \land (\square_{[0,15]}\neg \tilde{\mathbf{G}}) \land (\square_{[0,15]}\neg \tilde{\mathbf{B}}) \\ &\text{stlfrag-1:} (\Diamond_{[0, 15]}\square_{[0,5]}\tilde{\mathbf{R}}) \land (\Diamond_{[0, 15]}\square_{[0,5]}\tilde{\mathbf{G}}) \\ &\text{stlfrag-2:}(\Diamond_{[0, 15]}\square_{[0,5]}\tilde{\mathbf{Y}}). \end{align}\] Figure 6 illustrates the resulting trajectories obtained using a simulation time step of \(0.01\) s.

6.2.1 Computation Time comparison↩︎

Table 2 compares the computation time of the proposed method with existing approaches. For the STT-based methods, the first term denotes the offline tube synthesis time, while the second denotes the online control synthesis time. Although the previous STT approach [17] is faster for simple STL fragments, its offline computation increases significantly with the complexity of the STL specification due to the underlying SMT solver. In contrast, the proposed PINN-based tube synthesis scales better for complex specifications. Furthermore, the proposed bounded transformation function results in a lower online control synthesis time than the earlier STT controller, which relied on an unbounded transformation function. Compared with MILP [8], MPC [10], and CBF-based methods [29], the proposed framework also achieves significantly lower online computation by avoiding online optimization.

6.2.2 Input Comparison↩︎

Table 3 compares the maximum control input for the benchmark tasks stlcg-1 and stlfrag-1. The proposed controller respects the prescribed input limit of \(0.75\) throughout the task, both under nominal and perturbed conditions. In contrast, the previous STT controller [17] requires substantially larger control inputs, especially under model perturbation, since it does not explicitly consider actuator limits. CBF- and MILP-based approaches also require larger control efforts under nominal conditions and are not evaluated under perturbations, since model inaccuracies can lead to violation of the STL specification.

7 Extension to Multi-Agent Systems↩︎

To extend the approach for a multi-agent scenario, we define the robustness metric of the complete cascaded formulation of individual agents and apply a similar strategy to generate the PINSTT for all the agents by defining a robustness metric for the overall cascaded system. Then we apply a similar control strategy for individual agents to satisfy the specification. We validate the effectiveness of the proposed approach in multi-agent scenarios using a team of omnidirectional robots, whose dynamics is given in 24 . We perform in simulation, a group of agents navigating in a bounded 2D workspace with static circular obstacles while maintaining a prescribed formation.

We evaluate a formation-preserving navigation task featuring four agents initialized in a diamond configuration. The objective is to translate the formation diagonally across the workspace while navigating obstacles. This scenario presents significant coupling challenges: agents must simultaneously avoid environmental collisions, maintain safe inter-agent separation, and preserve the global formation structure. Because deviations by any single agent propagate through the collective, coordinated motion is essential.

The task is formally defined using Signal Temporal Logic as a conjunction of local and global specifications: \[\begin{align} \psi = \; \underbrace{ \left( \wedge_{i=1}^{4} \tilde{{\mathbf{S}}}_i \right) }_{\text{Initial condition}}\; & \land\; \underbrace{ \square_{[0,120]} \left( \wedge_{i=1}^{4} \neg \tilde{{\mathcal{O}}}_i \right) \;\land\; \wedge_{i=1}^{4} \left( \Diamond_{[0,120]} \tilde{\boldsymbol{G}}_i \right) }_{\text{Local specifications}} \land \; \underbrace{ \left(\square_{[0,120]} \tilde{\boldsymbol{F}}_{\text{form}}\right) \;\land\; \square_{[0,120]} \left( \wedge_{i=1}^{4} \neg \tilde{\boldsymbol{X}}_i \right) }_{\text{Global specification}} \end{align}\] where \(\tilde{{\mathcal{O}}}_i\) represents unsafe regions, \(\tilde{\mathbf{F}}_{\text{form}}\) encodes leader-relative distance and bearing constraints, and \(\tilde{\mathbf{G}}_i\) denotes target goal regions for the \(i^{\text{th}}\) agent, \(i=\{1,2,3,4\}\). Also, \({\mathbf{S}}_1 = {\mathbb{B}}([\sqrt{2},0],0.3)\), \({\mathbf{S}}_2 = {\mathbb{B}}([0,\sqrt{2}],0.3)\), \({\mathbf{S}}_3 = {\mathbb{B}}([-\sqrt{2},0],0.3)\), \({\mathbf{S}}_4 = {\mathbb{B}}([0,-\sqrt{2}],0.3)\), \(\mathbf{G}_1 = {\mathbb{B}}([13+\sqrt{2},13],0.3)\), \(\mathbf{G}_2 = {\mathbb{B}}([13,13+\sqrt{2}],0.3)\), \(\mathcal{G}_3 = {\mathbb{B}}([13-\sqrt{2},13],0.3)\), \(\mathbf{G}_4 = {\mathbb{B}}([13,13-\sqrt{2}],0.3)\), \({\mathcal{O}}= {\mathbb{B}}([5,2],1.25) \cup {\mathbb{B}}([2,5],1.25) \cup {\mathbb{B}}([8,8],1.75)\), representing static obstacles, and \(\tilde{\mathbf{X}}_i = \bigcup_{\substack{j=1 \\ j \neq i}}^{4} {\mathbb{B}}([x_j,y_j],0.1),\) representing agents acting as dynamic obstacles to agent \(i\). The desired formation is specified relative to the leader agent through nominal inter-agent distances proportional to \([2, 2\sqrt{2}, 2]\) and relative bearings \({\mathbb{B}}\left(\frac{3\pi}{4}, 0.1\right)\), \({\mathbb{B}}\left(\pi, 0.1\right)\), \({\mathbb{B}}\left(-\frac{3\pi}{4}, 0.1\right)\).

The velocity and acceleration limits in each dimension are set to \(0.5 \;\text{m/s}\) and \(1.0 \;\text{m/s}^2\), respectively. To satisfy the feasibility conditions in 18 , we select Lipschitz constants for the tube parameters as \(\mathcal{L}_c = 0.4\) and \(\mathcal{L}_r = 0.05\). Formation integrity is maintained via distance and bearing constraints relative to a designated leader. A formation consistency objective penalizes geometric deviations while permitting uniform scaling, allowing the formation to adapt to constrained environments without compromising its structural identity.

The offline training of the PINN requires \(59.5\) seconds while the per-step online control synthesis time is \(3.17 \;\mu\text{s}\). Figure 7 illustrates the resulting trajectories in 3D space-time and top-down projections. The learned STTs generate smooth, feasible trajectories that successfully navigate obstacles while maintaining formation throughout the mission horizon. Velocity and acceleration profiles remain strictly within prescribed bounds. The simulation video can be found in the Video Link.

8 Conclusion and Future Work↩︎

This paper presented a physics informed neural spatiotemporal tube (PINSTT) framework for satisfying Signal Temporal Logic (STL) specifications for unknown Euler–Lagrange systems subject to input constraints. The proposed approach parameterizes the time-varying center and radius of the tube using a physics-informed neural network, where the STL robustness metric is directly incorporated into the training objective. To provide formal guarantees over the continuous time horizon, Lipschitz continuity of the tube parameters is enforced through physics-informed loss functions using automatic differentiation, and a verification condition is derived to certify the validity of the synthesized tube. Subsequently, a closed-form, approximation-free, model-free control law is developed to ensure that the system trajectory remains within the synthesized tube while respecting prescribed input bounds. The proposed framework combines several desirable properties within a single architecture: support for the full class of STL specifications, applicability to unknown Euler-Lagrange systems, bounded closed-form control inputs, and microsecond-level online control synthesis. The effectiveness of the approach has been demonstrated through both simulation and hardware experiments involving single-agent and multi-agent scenarios.

Future work will focus on extending the framework to stochastic systems and probabilistic settings, incorporating dynamic environments, and developing distributed tube synthesis and control strategies for large-scale multi-agent systems.

References↩︎

---

1. The work of Ratnangshu Das is supported by the Prime Minister’s Research Fellowship from the Ministry of Education, Government of India.↩︎

2. https://l1nk.dev/a4xbr9y↩︎