# Distributed Sequential Receding Horizon Control of Multi-Agent Systems under
Recurring Signal Temporal Logic

Eleftherios E. Vlahakis, Lars Lindemann, and Dimos V. Dimarogonas This work
was supported by the Knut & Alice Wallenberg Foundation (KAW), the Horizon
Europe Grant SymAware and the ERC Consolidator Grant LEAFHOUND.E. E. Vlahakis
and D. V. Dimarogonas are with the Division of Decision and Control Systems,
School of Electrical Engineering and Computer Science, KTH Royal Institute of
Technology, 10044, Stockholm, Sweden. Email<EMAIL_ADDRESS>Lindemann is with the Thomas Lord Department of Computer Science, Viterbi
School of Engineering, University of Southern California, Los Angeles, 90089,
CA, USA. Email<EMAIL_ADDRESS>
###### Abstract

We consider the synthesis problem of a multi-agent system under Signal
Temporal Logic (STL) specifications representing bounded-time tasks that need
to be satisfied recurrently over an infinite horizon. Motivated by the limited
approaches to handling recurring STL systematically, we tackle the infinite-
horizon control problem with a receding horizon scheme equipped with
additional STL constraints that introduce minimal complexity and a backward-
reachability-based terminal condition that is straightforward to construct and
ensures recursive feasibility. Subsequently, assuming a separable performance
index, we decompose the global receding horizon optimization problem defined
at the multi-agent level into local programs at the individual-agent level the
objective of which is to minimize the local cost function subject to local and
joint STL constraints. We propose a scheduling policy that allows individual
agents to sequentially optimize their control actions while maintaining
recursive feasibility. This results in a distributed strategy that can operate
online as a model predictive controller. Last, we illustrate the effectiveness
of our method via a multi-agent system example assigned a surveillance task.

##  I INTRODUCTION

Various applications of multi-agent systems require agents to undertake
recurring tasks that must be executed over an infinite time horizon. Examples
of such tasks include area coverage in surveillance systems, traffic
management in intelligent transportation, smart harvesting in precision
agriculture, and more. Signal Temporal Logic (STL) [1] is an important
formalism for precisely defining, among others, a wide range of such tasks.
STL is equipped with quantitative semantics [2], allowing one to capture the
robustness of a formula, roughly measuring the distance from the space of
falsifying system runs [3]. Although formulation and verification of complex
recurring multi-agent specifications are possible via STL, control synthesis
from STL becomes increasingly challenging as the number of agents and the
planning horizon grow.

A synthesis problem under recurring STL can be formulated as

$\displaystyle\underset{u}{\text{minimize}}\;\;$
$\displaystyle\sum_{t=0}^{\infty}l(x(t),u(t))$ (1a) subject to $\displaystyle
x(t+1)=f(x(t),u(t)),\;x(0)=x_{0}$ (1b) $\displaystyle
x\models\square_{[0,\infty)}\phi$ (1c)

where $l:\mathbb{R}^{n}\times\mathbb{R}^{m}\to\mathbb{R}_{\geq 0}$ is a cost
function, $x=[x(0),x(1),\ldots]$ is an infinite run of the system (1b) that is
required to satisfy the STL formula $\phi$ in (1c) at every time step, with
$\square$ denoting the always operator and $\phi$ a bounded-time STL formula,
and $u=[u(0),u(1),\ldots]$ is the optimization variable denoting an admissible
input trajectory. This problem is computationally challenging and hard to
solve directly due to infinite memory requirements.

Intuitively, by iteratively solving a finite-horizon variant of (1) with a
sufficiently large optimization horizon and tracking past computations, a
feasible input trajectory $u$ can be constructed by collecting the first
element of the optimal solution from each iteration. Such a receding horizon
approach to addressing (1) recursively has been proposed in [4] via mixed-
integer programming (MIP) based on binary encoding of STL constraints. The
soundness and completeness of this approach for STL formulas defined over
linear predicates have resulted in approaches to reactive and robust model
predictive control (MPC) of single-agent systems under STL [5, 6, 7, 8].
However, due to the complexity increase caused by the use of binary variables
[9], MIP-based synthesis methods are problematic when dealing with large or
unbounded STL formulas that require the satisfaction of Lasso conditions. The
underlying control problem becomes even more challenging if applied in the
multi-agent framework.

To bypass complexity issues, the authors in [10] introduce discrete average
space robustness, a new quantitative semantics of STL, that allows the
formulation of tractable optimization problems for control synthesis.
Robustness metrics of STL that fit receding horizon schemes and permit more
tractable solutions have also been proposed in [11, 12]. The appeal of a
receding horizon approach relies on the validity that all iterations yield a
solution. Although recursive feasibility is well explored in MPC literature
[13] for classical control objectives (e.g., closed-loop stability), there
exist only few results in developing terminal conditions to establish
recursive feasibility of receding horizon and MPC schemes under STL [14, 15].
This stems from the challenge to design intuitive and effective terminal
conditions for systems with non-asymptotic control objectives.

In this work, we consider the control synthesis problem (1) of a multi-agent
system under recurring STL. The global specification is defined as a bounded-
time STL formula that needs to be satisfied recurrently over an infinite
horizon, as per (1c). We introduce a receding horizon scheme to attack (1)
iteratively and propose Lasso and terminal constraints that guarantee
recursive feasibility enabling an MPC implementation provided that the
underlying optimizations can be solved in near real-time. Our method is not
limited to MIP setups and is amenable to STL constraint formulation via binary
encoding or tractable STL metrics [10, 12]. Subsequently, assuming a separable
global performance index and an STL formula representing individual and
coupling specifications, we decompose the receding horizon control problem
defined at the multi-agent level into smaller local programs each associated
with an individual agent assigned local and collective tasks. To establish a
valid distributed receding horizon scheme that addresses (1) iteratively based
on the local programs, we propose a scheduling algorithm that preserves
recursive feasibility and allows the agents to optimize their actions
sequentially.

The remainder of the paper is organized as follows. In Section II, notation
and basic notions in STL are introduced. In Section III, we define the multi-
agent system we study, the underlying STL formula, and the induced interaction
graph. The main results, namely, the proposed receding horizon scheme, and the
proposed distributed receding horizon strategy, are in Sections IV and V,
respectively. A numerical example and concluding remarks with future work
directions are in Sections VI and VII, respectively.

##  II Preliminaries

###  II-A Notation

The sets of (non-negative) real numbers and (non-negative) integers are
denoted by ($\mathbb{R}_{\geq 0}$) $\mathbb{R}$ and ($\mathbb{Z}_{\geq 0}$)
$\mathbb{Z}$, respectively. The real $n$-dimensional vector space is
$\mathbb{R}^{n}$, and the set of $n\times m$ real matrices is
$\mathbb{R}^{n\times m}$. The transpose of a vector $\xi$ is $\xi^{T}$. The
all-one vector is $\bm{1}_{n}\in\mathbb{R}^{n}$ and the identity matrix is
$I_{n}\in\mathbb{R}^{n\times n}$. The $j$th row of matrix $A$ and the $j$th
element of vector $a$ are denoted by $(A)_{j}$ and $(a)_{j}$, respectively.
Let $x_{1},\ldots,x_{n}$ be vectors. Then,
$x=(x_{1},\ldots,x_{n})=[x_{1}^{T}\;\cdots\;x_{n}^{T}]^{T}$. Let
$t\in\mathbb{Z}$ and $a,b\in\mathbb{Z}_{\geq 0}$ with $a>b$. Then, $t\in[a,b]$
means that $t=\\{a,a+1,\ldots,b-1,b\\}$. The tuple $[x(a),\ldots,x(b)]$
denotes the trajectory consisting of $x(t)$ for $t\in[a,b]$. Similarly, we
denote by $[x(a:b)]$ a trajectory consisting of successive elements defined
over a time interval $[a,b]$ and by $[x(t)]$ a trajectory originating at
$x(t)$. We denote by $x(\tau|t)$ the prediction of $x(\tau)$ carried out at
time $t$. We also denote by $[x(t+a:t+b|t)]$ the predicted trajectory
$[x(t+a|t),\ldots,x(t+b|t)]$. The half-space representation of a convex
compact polytopic set is $\mathcal{Y}=\\{y:G_{y}y\leq g_{y}\\}$ with the
inequalities applied elementwise. The cardinality of $\mathcal{V}$ is
$|\mathcal{V}|$. The Kronecker product of $A\in\mathbb{R}^{n\times m}$ and
$B\in\mathbb{R}^{p\times q}$ is $A\otimes B\in\mathbb{R}^{np\times mq}$. The
remainder of the division of $a$ by $b$ is $\text{mod}(a,b)$.

###  II-B Signal Temporal Logic

The formalism adopted here for specifying recurring spatiotemporal properties
of multi-agent systems is Signal Temporal Logic (STL) [1]. We define STL
formulas over discrete-time signals. A recurring STL formula is defined as
follows:

$\psi=\square_{[0,\infty)}\phi$ (2)

with $\phi$ being a bounded-time formula with syntax

$\phi:=\top~{}|~{}p~{}|~{}\lnot
p~{}|~{}\lnot\phi~{}|~{}\phi_{1}\vee\phi_{2}~{}|~{}\phi_{1}\wedge\phi_{2}~{}|~{}\phi_{1}U_{[a,b]}\phi_{2}$
(3)

where $p:=\begin{cases}\top&\text{if\;}\mu(x)\geq 0,\\\
\bot&\text{if\;}\mu(x)<0,\end{cases}$ is a predicate,
$\mu:\mathbb{R}^{n}\to\mathbb{R}$ is predicate function, and $\phi_{1}$,
$\phi_{2}$ are bounded-time STL formulas. Note that with the above syntax we
may define the eventually and always operators as $\lozenge_{[a,b]}\phi=\top
U_{[a,b]}\phi$ and $\square_{[a,b]}\phi=\lnot\lozenge_{[a,b]}\lnot\phi$,
respectively, with $a\geq b$.

Let $N$ be the horizon of formula $\phi$ and $[x(t:t+N)]$ be a trajectory
consisting of $x(t+\tau)$ for $\tau=0,1,\ldots,N$. We denote by
$[x(t:t+N)]\models\phi$ the satisfaction of the formula $\phi$ defined over
the trajectory $[x(t:t+N)]$. For the grammar introduced in (3), the validity
of an STL formula $\phi$ defined over a trajectory $[x(t)]$ originating at
$x(t)$ is formally defined as follows:

$[x(t)]\models p$ | $\Leftrightarrow$ | $\mu(x(t))\geq 0$
---|---|---
$[x(t)]\models\lnot p$ | $\Leftrightarrow$ | $\lnot([x(t)]\models p)$
$[x(t)]\models\phi_{1}\land\phi_{2}$ | $\Leftrightarrow$ | $[x(t)]\models\phi_{1}\land[x(t)]\models\phi_{2}$
$[x(t)]\models\phi_{1}\lor\phi_{2}$ | $\Leftrightarrow$ | $[x(t)]\models\phi_{1}\lor[x(t)]\models\phi_{2}$
$[x(t)]\models\lozenge_{[a,b]}\phi$ | $\Leftrightarrow$ | $\exists\tau\in[t+a,t+b],\;[x(\tau)]\models\phi$
$[x(t)]\models\square_{[a,b]}\phi$ | $\Leftrightarrow$ | $\forall\tau\in[t+a,t+b],\;[x(\tau)]\models\phi$
$[x(t)]\models\phi_{1}U_{[a,b]}\phi_{2}$ | $\Leftrightarrow$ |  $\exists\tau\in[t+a,t+b]$ s.t. $[x(\tau)]\models\phi_{2}$
|  | $\land\forall\tau^{\prime}\in[t,\tau],[x(\tau^{\prime})]\models\phi_{1}$

Based on the semantics introduced above, the horizon of a formula is
recursively defined as [1]: $N^{p}=0$, $N^{\lnot\phi}=N^{\phi}$,
$N^{\phi_{1}\land\phi_{2}}=N^{\phi_{1}\lor\phi_{2}}=\max(N^{\phi_{1}},N^{\phi_{2}})$,
$N^{\square_{[a,b]}\phi}=N^{\lozenge_{[a,b]}\phi}=b+N^{\phi}$,
$N^{\phi_{1}\;U_{[a,b]}\phi_{2}}=b+\max(N^{\phi_{1}},N^{\phi_{2}})$.

STL is endowed with robustness metrics for assessing the robust satisfaction
of a formula [2]. A scalar-valued function
$\rho^{\phi}:\mathbb{R}^{n}\times\cdots\times\mathbb{R}^{n}\to\mathbb{R}$ of a
signal indicates how robustly a signal $[x(t)]$ satisfies a formula $\phi$ at
time $t$. The robustness function is defined recursively as follows

$\displaystyle\rho^{p}([x(t)])=\mu(t),$ $\displaystyle\rho^{\lnot
p}([x(t)])=-\rho^{p}([x(t)]),$
$\displaystyle\rho^{\phi_{1}\land\phi_{2}}([x(t)])=\min(\rho^{\phi_{1}}([x(t)]),\rho^{\phi_{2}}([x(t)])),$
$\displaystyle\rho^{\phi_{1}\lor\phi_{2}}([x(t)])=\max(\rho^{\phi_{1}}([x(t)]),\rho^{\phi_{2}}([x(t)])),$
$\displaystyle\rho^{\square_{[a,b]}\phi}([x(t)])=\min_{\tau\in[t+a,t+b]}\rho^{\phi}([x(t)],\tau),$
$\displaystyle\rho^{\lozenge_{[a,b]}\phi}([x(t)])=\max_{\tau\in[t+a,t+b]}\rho^{\phi}([x(\tau)]),$
$\displaystyle\rho^{\phi_{1}U_{[a,b]}\phi_{2}}([x(t)])=\max_{\tau\in[t+a,t+b]}\big{(}\min(\rho^{\phi_{1}}([x(\tau)]),$
$\displaystyle\hskip
113.81102pt\min_{\tau^{\prime}\in[t,\tau]}\rho^{\phi_{2}}([x(\tau^{\prime})]))\big{)},$
(4)

where $p:=(\mu(x)\geq 0)$ is a predicate, and $\phi$, $\phi_{1}$, and
$\phi_{2}$ are STL formulas.

##  III Multi-agent system

###  III-A MAS and STL description

We consider a multi-agent system (MAS) with discrete-time dynamics written as
in (1b):

$x(t+1)=f(x(t),u(t)),$ (5)

where $x(0)=x_{0}$ is an initial condition,
$x(t)=(x_{1}(t),\ldots,x_{M}(t))\in\mathcal{X}\subset\mathbb{R}^{n}$ and
$u(t)=(u_{1}(t),\ldots,u_{M}(t))\in\mathcal{U}\subset\mathbb{R}^{m}$ are
aggregate state and input vectors, respectively, with
$x_{i}(t)\in\mathcal{X}_{i}\subset\mathbb{R}^{n_{i}}$,
$u_{i}(t)\in\mathcal{U}_{i}\subset\mathbb{R}^{m_{i}}$,
$\mathcal{X}=\mathcal{X}_{1}\times\cdots\times\mathcal{X}_{M}$ and
$\mathcal{U}=\mathcal{U}_{1}\times\cdots\times\mathcal{U}_{M}$, and $M$ is the
number of agents. We assume that the individual agents are open-loop
dynamically decoupled, i.e.,
$f(x(t),u(t))=(f_{1}(x_{1}(t),u_{1}(t)),\ldots,f_{M}(x_{M}(t),u_{M}(t)))$,
with $f(x(t),u(t)):\mathbb{R}^{n}\times\mathbb{R}^{m}\to\mathbb{R}^{n}$ and
$f_{i}(x_{i}(t),u_{i}(t)):\mathbb{R}^{n_{i}}\times\mathbb{R}^{m_{i}}\to\mathbb{R}^{n_{i}}$,
$i=1,\ldots,M$.

The MAS is subject to a global recurring STL task $\psi$ with syntax as in
(2)-(3) that couples the behavior of the agents. The structure of $\psi$
induces an interaction graph $\mathcal{G}=(\mathcal{V},\mathcal{E})$, where
$\mathcal{V}=\\{1,\ldots,M\\}$ is the set of nodes, with node $i$ representing
the $i$th agent of the MAS, and
$\mathcal{E}\subset\mathcal{V}\times\mathcal{V}$ is the set of edges.
Descriptively, an edge $(i,j)$ indicates a subformula contained in $\psi$
involving at least agents $i$ and $j$. We consider that $\mathcal{G}$ is
undirected, that is, $(i,j)\in\mathcal{E}\iff(j,i)\in\mathcal{E}$. To capture
all the possible interactions between agents involved in $\psi$ beyond one- or
two-agent tasks using the graph $\mathcal{G}$, we recall the definition of
cliques.

###### Definition 1

Let $\mathcal{G}=(\mathcal{V},\mathcal{E})$ be an undirected graph with node
set $\mathcal{V}$, with cardinality $M=|\mathcal{V}|$, and edge set
$\mathcal{E}$. Define $\mathcal{E}_{\mathcal{V}^{\prime}}\subseteq\mathcal{E}$
as the set of edges associated with nodes
$\mathcal{V}^{\prime}\subseteq\mathcal{V}$. Then,
$\mathcal{G}^{\prime}=(\mathcal{V}^{\prime},\mathcal{E}_{\mathcal{V}^{\prime}})$
is a complete subgraph of $\mathcal{G}$, if
$\mathcal{E}_{\mathcal{V}^{\prime}}$ contains all possible edges between the
nodes $\mathcal{V}^{\prime}$. The set of cliques of $\mathcal{G}$ is defined
as

$\displaystyle\mathcal{K}=\\{\nu\subset\mathcal{V}:(\nu,\mathcal{E}_{\nu})\text{
is a complete subgraph of }$ $\displaystyle\mathcal{G}$ $\displaystyle\text{
with }|\nu|\leq$ $\displaystyle M\\}$ (6)

###### Remark 1

The set of cliques of a connected, undirected graph
$\mathcal{G}=(\mathcal{V},\mathcal{E})$ contains all vertices, called one-
vertex cliques, all edges, called two-vertex cliques, and all complete
subgraphs of $\mathcal{G}$ with cardinality greater than two and less than or
equal to $|\mathcal{V}|$.

Let $K_{\psi}\subset\mathcal{K}$ be the set of cliques that are induced by the
structure of the task $\psi$. Then, the global STL task defined at multi-agent
level is

$\displaystyle\psi$ $\displaystyle=\square_{[0,\infty)}\phi$ (7a)
$\displaystyle\phi$ $\displaystyle=\bigwedge_{\nu\in K_{\psi}}\phi_{\nu}.$
(7b)

In words, we can interpret the global bounded-time STL formula (7b) as a
conjunction of subformulas, denoted as $\phi_{\nu}$, each of which involves
individual agents (represented by one-vertex cliques), pairs of agents
(represented by two-vertex cliques), or groups of more than two agents
(indicated by multi-vertex cliques), where $|\nu|=1$, $|\nu|=2$, or
$2<|\nu|\leq M$, respectively. This utilization of cliques allows us to
effectively capture interactions that go beyond the scope of individual and
two-agent tasks, as typically represented in a vertex-edge graph structure.

###### Remark 2

Under the formulation (7), there is no restriction on the number of subtasks
that are associated with a clique $\nu\in K_{\psi}$. For instance, if clique
$\nu$ is associated with the conjunction (disjunction) of two STL tasks, we
may write $\phi_{\nu}=\phi_{\nu}^{1}\land\phi_{\nu}^{2}$
($\phi_{\nu}=\phi_{\nu}^{1}\lor\phi_{\nu}^{2}$). In fact, $\phi_{\nu}$ is
allowed to be any STL formula consistent with the syntax in (3).

###### Assumption 1

We assume that the formulas $\phi_{\nu}$, $\nu\in K_{\psi}$, have identical
horizons which we denote as $N$.

###### Remark 3

Assumption 1 is not restrictive due to the recurring structure of $\psi$. To
see this, let, e.g., $K_{\psi}=\\{q,p\\}$ and write

$\psi=\square_{[0,\infty)}(\phi_{q}\land\phi_{p}).$ (8)

Let also $N_{q}$ and $N_{p}$ be the horizon of $\phi_{q}$ and $\phi_{p}$,
respectively, with $N=\max\\{N_{q},N_{p}\\}$. Then, the satisfaction of $\psi$
may be enforced by satisfying

$\psi^{\prime}=\square_{[0,\infty)}((\square_{[0,N-N_{q}]}\phi_{q})\land(\square_{[0,N-N_{p}]}\phi_{p}))$
(9)

where the horizon of $\square_{[0,N-N_{\nu}]}\phi_{\nu}$ is
$N=N-N_{\nu}+N_{\nu}$, with $\nu=q,p$.

###  III-B Decomposition

To decompose the global formula in (7b) into local formulas each assigned to
an individual agent, say $i$, we need to collect all $\phi_{\nu}$, $\nu\in
K_{\psi}$, involving agent $i$. In other words, we need to construct the set
of teams consisting of neighboring agents to node $i$ involved in the same
tasks:

$\mathcal{T}_{i}=\\{\tau=\nu\setminus i\;|\;\nu\in
K_{\psi}\;\text{and}\;i\cap\nu\neq\emptyset\\}.$ (10)

We are now ready to define the local bounded-time STL formula assigned to node
$i$ as:

$\hat{\phi}_{i}=\phi_{i}\bigwedge_{j\in\mathcal{T}_{i}}\phi_{ij}.$ (11)

###### Remark 4

Comparing (7b) and (11), it is easy to see that
$\phi_{i}\bigwedge_{j\in\mathcal{T}_{i}}\phi_{ij}=\bigwedge_{\begin{subarray}{c}\nu\in
K_{\psi}\\\ \nu\cap i\neq\emptyset\end{subarray}}\phi_{\nu}$. We also note
that the subscripts $ij$ of $\phi_{ij}$ in (11) indicate the set of nodes
involved in it.

We also define the following aggregate vectors. Let $x_{j}(t)$, with
$j\in\mathcal{T}_{i}$, be the aggregate state vector collecting all the states
of the team $j\in\mathcal{T}_{i}$. Then,
$x_{ij}(t)=(x_{i}(t),x_{j\in\mathcal{T}_{i}}(t))$, is the aggregate vector
consisting of the state vectors of the $i$th agent and the team
$j\in\mathcal{T}_{i}$.

##  IV Multi-agent control

###  IV-A Receding horizon optimization

In this section, we propose a receding-horizon variant of (1) defined at the
multi-agent level, where we incorporate additional constraints referred to as
“Lasso constraints” that effectively shape the feasible domain. By enforcing a
terminal condition aligned with the Lasso constraints, the resulting
trajectories exhibit a recurring pattern. Next, we recall the following
definitions.

###### Definition 2

For the system (5), we denote the precursor set to a set
$\mathcal{S}\subset\mathcal{X}$ as follows

$\text{Pre}(\mathcal{S})=\\{x\in\mathbb{R}^{n}\;|\;\exists
u\in\mathcal{U}\;\text{s.t.\;}f(x,u)\in\mathcal{S}\\}$ (12)

######  Definition 3 (one-Step Controllable Set)

For the admissible set $\mathcal{X}$ and a given target set
$\mathcal{S}\subseteq\mathcal{X}$ the one-step controllable set
$\mathcal{C}_{1}(\mathcal{S})$ of the system (5) is defined as

$\mathcal{C}_{1}(\mathcal{S})=\text{Pre}(\mathcal{S})\cap\mathcal{X}$ (13)

The set $\mathcal{C}_{1}(\mathcal{S})$ collects all the states of (5) that can
be driven to the target set $\mathcal{S}$ in one step. We will now introduce a
receding horizon version of (1) and state its recursive feasibility property.
At time $t\geq 0$,

$\displaystyle\underset{u(t:t+N|t)}{\text{minimize}}\;\
\sum_{k=t}^{t+N}\sum_{i=1}^{M}l_{i}(x_{i}(k|t),u_{i}(k|t))$ (14a) s.t.
$\displaystyle x(k+1|t)=f(x(k|t),u(k|t)),\;k=t:t+N$ (14b)
$\displaystyle[x(t-N+1:t-1),x(t:t+1|t)]\models\phi$ (14c)
$\displaystyle\vdots$ $\displaystyle[x(t-1),x(t:t+N-1|t)]\models\phi$ (14d)
$\displaystyle[x(t:t+N|t)]\models\phi$ (14e)
$\displaystyle[x(t+1:t+N+1|t)]\models\phi$ (14f) $\displaystyle\vdots$
$\displaystyle[x(t+N+1|t),x(t+1:t+N|t)]\models\phi$ (14g)
$\displaystyle[x(t+1:t+N|t),x(t|t)]\models\phi$ (14h)
$\displaystyle[x(t+2:t+N|t),x(t:t+1|t)]\models\phi$ (14i)
$\displaystyle\vdots$ $\displaystyle[x(t+N|t),x(t:t+N-1|t)]\models\phi$ (14j)
$\displaystyle x(t|t)=x(t)$ (14k) $\displaystyle
x(k|t)\in\mathcal{X},\;u(k|t)\in\mathcal{U},\;k=t:t+N$ (14l) $\displaystyle
x(t+N|t)\in\mathcal{C}_{1}(x(t))$ (14m)

where the cost function in (1a) is decomposed as
$\sum_{i=1}^{M}l_{i}(x_{i}(k|t),u_{i}(k|t))$, with
$l_{i}:\mathbb{R}^{n_{i}}\times\mathbb{R}^{m_{i}}\to\mathbb{R}_{\geq 0}$, the
aggregate state $x(t)=(x_{1}(t),\ldots,x_{M}(t))$, the bounded-time STL
formula $\phi=\bigwedge_{\nu\in K_{\psi}}\phi_{\nu}$, $N$ is the horizon of
all formulas $\phi_{\nu}$, $\nu\in K_{\psi}$, and, hence, of $\phi$, and
$\mathcal{C}_{1}(x(t))$ in (14m) is the one-step controllable set of system
(5). The constraints in (14c)-(14d) consider trajectories composed of
historical data, the current state and predicted states. The constraint in
(14e) considers a trajectory originating at the current state $x(t)$, whereas
the Lasso constraints in (14f)-(14j) enforce that any trajectory consisting of
$N+1$ successive elements of $[x(t+1:t+N+1|t),x(t+1:t+N+1|t)]$ satisfies
$\phi$. The terminal condition in (14m) enforces recursive feasibility shown
in Theorem 1. Last, constraints in (14l) enforce safety and input capacity
constraints.

###### Remark 5

If a binary encoding as in [4] is employed to formulate the STL constraints in
(14), the constraints in (14f)-(14j) require the introduction of $2N$
additional binary variables.

###### Theorem 1

Let the optimization problem (14) be feasible at $t=0$. Then, it is feasible
for all $t\geq 0$.

###### Proof.

See Appendix A ∎

An immediate consequence of Theorem 1 is stated next.

###### Corollary 1

Let the problem (14) with time-varying terminal constraint
$x(t+N)\in\mathcal{C}_{1}(x(t))$ be feasible at time $t=0$. Then, by applying
$u(t)=u^{*}(t|t)$ to (5), any portion of the closed-loop trajectory $[x(t)]$
consisting of $N+1$ successive elements satisfies the formula $\phi$, that is,
$x(t:t+N)\models\phi$, for all $t\geq 0$. Thus, the infinite run of the
closed-loop system, $x^{\infty}=[x(0),x(1),x(2),\ldots]$, satisfies
$\square_{[0,\infty)}\phi$, that is, $x^{\infty}\models\psi$.

###### Remark 6

Constructing $\mathcal{C}_{1}(x(t))$ is challenging for nonlinear systems. As
a remedy, we can replace the terminal condition in (14m) with
$x(t+N+1|t)=x(t)$ and eliminate the redundant Lasso constraints in
(14h)-(14j). This modification comes at the cost of a more restricted single-
point reachability condition, but it maintains recursive feasibility. In the
case of linear systems, $\mathcal{C}_{1}(x(t))$ can be efficiently computed,
using standard computational geometry software [16], by representing the
target set in halfspace representation as
$S=\\{x\in\mathbb{R}^{n}\;|\;C_{x}x\leq d_{x}\\}$ where
$C_{x}=\begin{bmatrix}I&-I\end{bmatrix}^{T}$ and $d_{x}=(x(t),-x(t))$ [17,
18].

##  V Distributed Control

###  V-A Distributed receding horizon optimization

In this section, we will show how to decompose the receding horizon
optimization problem (14), defined at multi-agent level, into smaller local
problems while preserving recursive feasibility. Our decomposition approach
relies on the following assumption.

###### Assumption 2

The optimization problem (14) is feasible at $t=0$. Additionally, a feasible
(not necessarily optimal) input sequence $[u(0:N|0)]$ is known.

We are now ready to formulate the following smaller optimization problems,
each associated with an individual node:

$\displaystyle\underset{u_{i}(t:t+N|t)}{\text{minimize}}\;\
\sum_{k=t}^{t+N}l_{i}(x_{i}(k|t),u_{i}(k|t))$ (15a) s.t. $\displaystyle
x_{i}(k+1|t)=f_{i}(x_{i}(k|t),u_{i}(k|t)),\;k=t:t+N$ (15b)
$\displaystyle[x_{q}(t-N+1:t-1),x_{q}(t:t+1|t)\models\phi_{q}$ (15c)
$\displaystyle\vdots$
$\displaystyle[x_{q}(t-1),x_{q}(t:t+N-1|t)]\models\phi_{q}$ (15d)
$\displaystyle[x_{q}(t:t+N|t)]\models\phi_{q}$ (15e)
$\displaystyle[x_{q}(t+1:t+N+1|t)]\models\phi_{q}$ (15f) $\displaystyle\vdots$
$\displaystyle[x_{q}(t+N+1|t),x_{q}(t+1:t+N|t)]\models\phi_{q}$ (15g)
$\displaystyle[x_{q}(t+1:t+N|t),x_{q}(t|t)]\models\phi_{q}$ (15h)
$\displaystyle[x_{q}(t+2:t+N|t),x_{q}(t:t+1|t)]\models\phi_{q}$ (15i)
$\displaystyle\vdots$
$\displaystyle[x_{q}(t+N|t),x_{q}(t:t+N-1|t)]\models\phi_{q}$ (15j)
$\displaystyle\forall q\in i\cup\\{ij\\}_{j\in\mathcal{T}_{i}}$ $\displaystyle
x_{i}(t|t)=x_{i}(t)$ (15k) $\displaystyle
x_{i}(k|t)\in\mathcal{X}_{i},\;u_{i}(k|t)\in\mathcal{U}_{i},\;k=t:t+N$ (15l)
$\displaystyle x_{i}(t+N|t)\in\mathcal{C}_{1}(x_{i}(t))$ (15m)

with $i=1,\ldots,M$.

The main idea for introducing (15) is to attack the global receding horizon
scheme (14) in a distributed fashion while preserving recursive feasibility by
handling smaller problems at the agent level.

###### Lemma 1

Let Assumption 2 hold. Then, there is always an admissible input sequence that
renders (15) feasible for all $t\geq 0$ and for all nodes $i=1,\ldots,M$.

###### Proof.

Let $[u(0:N|0)]=([u_{1}(0:N|0)],\ldots,[u_{M}(0:N|0)])$ be known at $t=0$,
with $[u_{i}(0:N|0)]=[u_{i}(0|0),u_{i}(1|0),\ldots,u_{i}(N|0)]$,
$i=1,\ldots,M$, inducing a known feasible state trajectory
$[x_{i}(0:N+1|0)]=[x_{i}(0|0),x_{i}(1|0),\ldots,x_{i}(N|0),x_{i}(N+1|0)]$,
$i=1,\ldots,M$. By feasibility of (14) at $t=0$, there always exist inputs
$\hat{u}_{i}(N)$ such that $f_{i}(x_{i}(N|0),\hat{u}_{i}(N))=x(0|0)$,
$i=1,\ldots,M$ (cf. proof of Theorem 1). One can then see that there are
always $N+1$ successive elements in the sequence
$[u_{i}(0|0),u_{i}(1|0),\ldots,\hat{u}_{i}(N),u_{i}(0|0),u_{i}(1|0),\ldots,\hat{u}_{i}(N)]$
that lie in the feasible domain of (15) for all $i=1,\ldots,M$. ∎

Lemma 1 states that the recursive feasibility property of the global
optimization problem is preserved even if we decompose (14) into $M$ smaller
problems. However, when agents belong to the same cliques within the
underlying graph, indicating shared tasks, solving (15) in parallel becomes
problematic. This is due to the inconsistencies arising in the formulation of
the underlying coupling constraints. As a remedy, we propose a scheduling
algorithm whereby only a subset of agents can optimize their control inputs
while the remaining peers regress a feasible solution from past iterations.
This sequential scheduling enables the implementation of a distributed
receding horizon control policy while underpinning recursive feasibility.

###  V-B Sequential scheduling and distributed model predictive control

Let $\mathcal{O}(t)$ be a time-varying set consisting of the nodes of
$\mathcal{G}$ that can solve their local problem (15) (potentially optimally)
at time $t\geq 0$. We define

$\mathcal{O}(t)=\\{q\in\mathcal{V}\;|\;\forall
q^{\prime}\in\mathcal{V},\;q\neq
q^{\prime},\;(q,q^{\prime})\notin\mathcal{E}\\},$ (16)

where $\mathcal{V}$ and $\mathcal{E}$ are the sets of nodes and edges of the
graph $\mathcal{G}$, respectively. Intuitively, $\mathcal{O}(t)$ collects a
set of agents that are not involved in the same tasks. Obviously, the set
$\mathcal{O}(t)$ is not unique. We construct $\mathcal{O}(t)$ as follows. At
each time $t\geq 0$, we initialize $\mathcal{O}(t)$ by a node
$v(t)\in\mathcal{V}$, where

$v(t)=\text{mod}(v(t-1),M)+1,$ (17)

with $M=|\mathcal{V}|$. The time dependence in $v(t)$ signifies the choice of
a node from the set $\mathcal{V}$ at time $t$. For instance, if
$\mathcal{V}={1,2,3}$ and we begin with $v(0)=1$, according to (17), $v(1)=2$,
$v(2)=3$, $v(3)=1$, $v(4)=2$, and so forth. Then, by going through the
remaining $M-1$ nodes of $\mathcal{G}$, following a lexicographic order, we
add a node $q\in\mathcal{V}$ to $\mathcal{O}(t)$ if
$(q,q^{\prime})\notin\mathcal{E}$ for all $q^{\prime}\in\mathcal{O}(t)$. This
procedure is summarized in Algorithm 1.

Algorithm 1 Computation of $\mathcal{O}(t)$

1:Data: $\mathcal{G}=(\mathcal{V},\mathcal{E})$, $v(t-1)$

2:Initialize: $v(t)\leftarrow\text{mod}(v(t-1),M)+1$

3:Set: $\mathcal{O}(t)\leftarrow v(t)$

4:for $i$ in $1:M-1$ do

5: $q\leftarrow\text{mod}(v(t),M)+i$

6: if $(q,q^{\prime})\notin\mathcal{E}\;\forall q^{\prime}\in\mathcal{O}(t)$
then

7: $\mathcal{O}(t)\leftarrow q\cup\mathcal{O}(t)$

8: end if

9:end for

###### Procedure 1

Problem (15) is solved (potentially optimally) at time $t>0$ if
$i\in\mathcal{O}(t)$. If $i\notin\mathcal{O}(t)$ at time $t$ then Problem (15)
is solved by a feasible solution constructed by the previous iteration (cf.
proof of Lemma 1).

Based on the sequential scheduling induced by the construction of the set
$\mathcal{O}(t)$, we are in a position to state the following result and its
immediate consequence.

###### Theorem 2

Consider Procedure 1 and let Assumption 2 hold. Then, (15) is recursively
feasible for all $i\in\mathcal{V}$.

###### Proof.

The result relies on the definition of the set $\mathcal{O}(t)$. In fact, an
optimal input sequence $[u_{i}^{*}(t:t+N|t)]$ attained by node-$i$, provided
that $i\in\mathcal{O}(t)$ at time $t$, does not violate the feasibility of any
local problem corresponding to neighboring nodes $j\in\mathcal{T}_{i}$. Then,
recursive feasibility follows from Lemma 1. ∎

###### Corollary 2

Consider Procedure 1 and let Assumption 2 hold. Then, there are always
admissible local inputs $u_{i}(t|t)$, $i=1,\ldots,M$ at each time $t\geq 0$
synthesizing a multi-agent input $u(t|t)=(u_{1}(t|t),\ldots,u_{M}(t|t))$ that
drives the MAS (5) giving rise to a multi-agent state trajectory $[x(t)]$ that
satisfies $\phi$ for all $t\geq 0$, that is, the underlying infinite run of
the MAS $x^{\infty}\models\psi$.

The following procedure defines the iterative implementation of a distributed
sequential MPC scheme based on the scheduling algorithm induced by the set
$\mathcal{O}(t)$ and the solution of the problems (15). We denote the
minimizer of (15) by $[u_{i}^{*}(t:t+N|t)]$. At time $t$:

  1. (S1)

Agent $i$ measures its local state and exchanges predictions on the receding-
horizon state trajectories with its neighboring agents as computed in the
previous time step.

  2. (S2)

If $i\in\mathcal{O}(t)$, agent $i$ computes the minimizer
$[u_{i}^{*}(t:t+N|t)]$ of (15), and implements the first component of
$[u_{i}^{*}(t:t+N|t)]$, that is, $u_{i}(t)=u_{i}^{\ast}(t|t)$. Otherwise, if
$i\notin\mathcal{O}(t)$, agent $i$ implements $u_{i}(t)=u_{i}(t|t-1)$.

  3. (S3)

At time $t+1$, agent $i$ updates the local and neighboring state information
and repeats steps (S1) and (S2).

In the following section, we illustrate our distributed control strategy via a
numerical example.

##  VI Numerical Example

We will demonstrate the effectiveness of our control strategy by using the MAS
example considered in [10, Section 6]. Therein, a centralized model predictive
control approach was proposed to solve the synthesis problem under recurring
STL specifications. Here, we augment the STL formula considered in [10] with
collision avoidance between the agents.

The MAS consists of three identical agents $\mathcal{V}=\\{1,2,3\\}$ with
global dynamics $x(t+1)=Ax(t)+Bu(t)$, where
$x(t)=(x_{1}(t),x_{2}(t),x_{3}(t))\in\mathbb{R}^{12}$,
$u(t)=(u_{1}(t),u_{2}(t),u_{3}(t))\in\mathbb{R}^{6}$, with
$x_{i}(t)\in\mathbb{R}^{4}$ and $u_{i}(t)\in\mathbb{R}^{2}$, $i=1,2,3$,
$A=I_{6}\otimes\begin{bmatrix}1&0.1\\\ 0&1\end{bmatrix}$, and
$B=I_{6}\otimes\begin{bmatrix}0.005\\\ 1\end{bmatrix}$. The vector
$((x_{i})_{1},(x_{i})_{3})\in\mathcal{X}$ denotes the position of agent $i$ in
the two-dimensional space, where
$\mathcal{X}=\\{\xi\in\mathbb{R}^{2}:\begin{bmatrix}I_{2}&-I_{2}\end{bmatrix}^{T}\xi\leq(10,10,0,0)\\}$,
and $((x_{i})_{2},(x_{i})_{4})$ collects the respective velocities. The vector
$((u_{i})_{1},(u_{i})_{2})$ collects the constrained accelerations of agent
$i$ in the two directions, where $-20\leq(u_{i})_{j}\leq 20$, with $j=1,2$ and
$i=1,2,3$.

The MAS is tasked with surveilling the area denoted as
$\mathcal{X}\subset\mathbb{R}^{2}_{\geq 0}$. This specification is expressed
through a recurring STL formula $\psi=\square_{[0,\infty)}\phi$, where
$\phi=\phi^{1}\wedge\phi^{2}\wedge\phi^{3}$, with
$\phi^{1}=\phi^{11}\wedge\phi^{12}\wedge\phi^{13}$,
$\phi^{2}=\phi^{21}\wedge\phi^{22}\wedge\phi^{23}$, and
$\phi^{3}=\phi^{31}\wedge\phi^{32}$. The underlying subformulas are listed in
(19). Specifically, $\phi^{1}$ defines the admissible workspace of the multi-
agent system, $\phi^{2}$ specifies the surveillance task, and $\phi^{3}$
specifies collision avoidance. The infinity-norm-based constraints in (19) can
be expressed as conjunctions and disjunctions of linear inequalities on linear
predicates; For example, $\|(\xi_{1},\xi_{2})-(y_{1},y_{2})\|_{\infty}\leq 1$
can be expressed as $(\mu^{1}(\xi)\geq 0)\wedge(\mu^{2}(\xi)\geq
0)\wedge(\mu^{3}(\xi)\geq 0)\wedge(\mu^{4}(\xi)\geq 0)$, with
$\mu^{1}(\xi)=-\xi_{1}+y_{1}+1$, $\mu^{2}(\xi)=-\xi_{2}+y_{2}+1$,
$\mu^{3}(\xi)=\xi_{1}-y_{1}+1$, $\mu^{4}(\xi)=\xi_{2}-y_{2}+1$, whereas
$\|(\xi_{1},\xi_{2})-(y_{1},y_{2})\|_{\infty}\geq 1$ can be represented as
$\left((\mu^{1}(\xi)\geq 0)\lor(\mu^{3}(\xi)\geq
0)\right)\wedge\left((\mu^{2}(\xi)\geq 0)\lor(\mu^{4}(\xi)\geq 0)\right)$,
with $\mu^{1}(\xi)=\xi_{1}-y_{1}-1$, $\mu^{3}(\xi)=-\xi_{1}+y_{1}-1$,
$\mu^{2}(\xi)=\xi_{2}-y_{2}-1$, $\mu^{4}(\xi)=-\xi_{2}+y_{2}-1$.

We employ binary encoding to formulate conjunctions and disjunctions between
linear inequalities on linear predicates. This is an attempt to extend the
important MIP-based approach introduced in [4] in the multi-agent framework,
and test our method computationally. We refer the readers to [4, 6] for a
detailed description of the binary encoding approach. Indicatively,
$\mu(\xi(t))\geq 0$ is formulated as

$\displaystyle\begin{bmatrix}1&-K\\\
-1&K\end{bmatrix}\begin{bmatrix}\mu(\xi(t))\\\
z^{\mu}(t)\end{bmatrix}\leq\begin{bmatrix}0\\\ K\end{bmatrix}$ (18)

where $0\leq z^{\mu}(t)\leq 1$, and $K>0$ is a large positive scalar,
conjunctions $\varphi=\wedge_{k=1}^{r}\varphi_{k}$, and disjunctions
$\varphi^{\prime}=\lor_{k=1}^{r}\varphi^{\prime}_{k}$ are formulated as
$z^{\varphi}\leq z^{\varphi_{k}},\forall k,\text{ and }\;z^{\varphi}\geq
1-r+\sum_{k=1}^{r}z^{\varphi_{k}}$, and $z^{\varphi^{\prime}}\geq
z^{\varphi^{\prime}_{k}},\forall k,\text{ and
}\;z^{\varphi^{\prime}}\leq\sum_{k=1}^{r}z^{\varphi^{\prime}_{k}}$,
respectively, where $\varphi$, $\varphi^{\prime}$, $\varphi_{k}$,
$\varphi^{\prime}_{k}$, $k=1,\ldots,r$, are Boolean formulas, and
$z^{\varphi}\in\\{0,1\\}$, $z^{\varphi^{\prime}}\in\\{0,1\\}$,
$z^{\varphi_{k}}\in\\{0,1\\}$, $z^{\varphi^{\prime}_{k}}\in\\{0,1\\}$,
$k=1,\ldots,r$, are binary variables.

###### Remark 7

$K$ in (18) must be selected at least greater than the maximum admissible
value of $\mu(\xi)$. By choosing a sufficiently large $K$, $z^{\mu}(t)$ will
be constrained in ${0,1}$, and hence, it can be defined as a continuous
variable, effectively reducing the underlying computational overhead.

To decompose the formula $\phi$ into a conjunction of local formulas and
formulate the local receding horizon problems (15), we need the interaction
graph, which, by the coupling constraints introduced in $\phi^{3}$, is
$\mathcal{G}=(\mathcal{V},\mathcal{E})$, where $\mathcal{V}=\\{1,2,3\\}$ and
$\mathcal{E}=\\{(1,2),(2,3)\\}$. Obviously, the set of cliques is
$K_{\psi}=\\{1,2,3,(1,2),(2,3)\\}$ from which the teams corresponding to each
agents are $\mathcal{T}_{1}=\\{2\\}$, $\mathcal{T}_{2}=\\{1,3\\}$, and
$\mathcal{T}_{3}=\\{2\\}$. We are now ready to construct the local formulas
defined in (11) as $\hat{\phi}_{1}=\phi_{1}\wedge\phi_{12}$,
$\hat{\phi}_{2}=\phi_{2}\wedge(\phi_{21}\wedge\phi_{23})$, and
$\hat{\phi}_{3}=\phi_{3}\wedge\phi_{32}$, where,
$\phi_{1}=\phi^{11}\wedge\phi^{21}$, $\phi_{12}=\phi^{31}$,
$\phi_{2}=\phi^{21}\wedge\phi^{22}$, $\phi_{21}=\phi^{31}$,
$\phi_{23}=\phi^{32}$, and $\phi_{3}=\phi^{13}\wedge\phi^{23}$,
$\phi_{32}=\phi^{32}$.

In our simulations, we select $l=\|u(t)\|_{1}$ and $l_{i}=\|u_{i}(t)\|_{1}$ as
global and local performance criteria, respectively. We initiate the process
by solving (14) for one iteration and subsequently execute the distributed
receding horizon procedure (S1)-(S3), as detailed in the previous section.
Following the initial iteration, an optimization is performed by either agent
2 alone or agents 1 and 3, determined by the set
$\mathcal{O}(t)\in\mathcal{O}_{1}\cup\mathcal{O}_{2}$, for $t>0$, where
$\mathcal{O}_{1}=2$ and $\mathcal{O}_{2}=\\{1,3\\}$. The underlying mixed-
integer linear programs were formulated using the YALMIP toolbox in MATLAB
[19] and solved using the GUROBI solver [20].

Starting from the chosen initial conditions, our distributed control strategy
guides the MAS along a trajectory that satisfies the recurring STL formula
$\psi$, while respecting input constraints, as shown in Fig. 2. Histograms in
Fig. 1 illustrate the computation time distributions for the initial
centralized iteration and the subsequent distributed iterations, demonstrating
the benefits of our approach. To assess the robustness of our method, we
conducted simulations by introducing velocity perturbations to the MAS for an
80-time-step duration. Even with these perturbations, the MAS effectively
remains within the permissible workspace, successfully fulfilling its
surveillance task, as depicted in Fig. 3. To verify both simulations, we
employed the robustness function detailed in Section II-B, which remained
nonnegative for most of the simulation period. In addition, we performed
simulations in which we omitted the proposed terminal constraint. The outcomes
reveal that, given the chosen input constraints, the MAS cannot successfully
accomplish the surveillance task. This underscores the key role of the
terminal condition in our control design.

(a) Centralized scheme.

(b) Distributed scheme.

Figure 1: Times of computations performed on Laptop with CPU: 11th Gen
Intel(R) Core(TM) i7-1185G7 at 3.00GHz.

(a) Horizontal positions.

(b) Vertical positions.

(c) Horizontal accelerations.

(d) Vertical accelerations.

Figure 2: Position and acceleration over a 13-second time horizon under the
distributed receding horizon control scheme.

(a) Nominal trajectories.

(b) Perturbed trajectories.

(c) Horizontal accelerations.

(d) Vertical accelerations.

Figure 3: Left: Nominal and perturbed trajectories. Right: Accelerations under
random perturbations in the velocity terms.

##  VII Conclusion

We have proposed a receding horizon control strategy to address the infinite-
horizon synthesis problem of a multi-agent system under recurring STL
specification. To ensure recursive feasibility and guarantee the integrity of
the proposed control scheme we have introduced Lasso and terminal constraints
that are easy to construct and intuitive for schemes under recurring tasks. By
decomposing the global optimization problem into local programs we implement a
scheduling policy that enables individual agents to optimize their control
actions sequentially. This approach yields a distributed control strategy that
enables online operation, while preserving recursive feasibility. Our method
hinges on the feasibility of an initial iteration carried out at the multi-
agent level. Inspired by the proposed sequential scheduling algorithm and the
decomposition approach, we aim to tackle the problem in a fully distributed
manner in future work.

##  Appendix A Proof of Theorem 1

We will show recursive feasibility for $t=0$ and $t>N$. The proof for $0<t<N$
follows similar lines. 1) Problem (14) being feasible at $t=0$ implies that
there exists an optimal input sequence $[u^{*}(0:N|0)]$ inducing an optimal
state trajectory $[x^{*}(0:N+1|0)]$. By applying input $u(0)=u^{*}(0|0)$ to
(5), the MAS evolves to $x(1)=f(x(0),u(0))=f(x(0),u^{*}(0|0))=x^{*}(1|0)$.
Since $x^{*}(N|0)\in\mathcal{C}_{1}(x(0))$, there is an admissible input
$\hat{u}(N)$ s.t. $f(x^{*}(N|0),\hat{u}(N))=x(0)$. Then, at $t=1$, we design
the (not necessarily optimal) admissible input sequence
$[u(1:N+1|1)]=[u^{*}(1|0),u^{*}(2|0),\ldots,\hat{u}(N),u^{*}(0|0)]$, which
yields a state sequence $[x(1:N+2|1)]$ the elements of which are computed
recursively starting from $x(1|1)$ resulting in
$[x(1:N+2|1)]=[x(1),x^{*}(2|0),\ldots,x^{*}(N|0),x(0),x(1)]$, which we check
for feasibility. From constraints (14c)-(14d), we only need to check (14d),
since there are no historical data for the rest. Indeed,
$[x(0),x^{*}(1|1),\ldots,x^{*}(N-1|0),x^{*}(N|0)]\models\phi$ is feasible by
the feasibility of (14e) at $t=0$. Constraint (14e) for $t=1$, which is
written as $[x(1),x^{*}(2|0),x^{*}(3|0),\ldots,x^{*}(N|0),x(0)]\models\phi$,
is feasible due to feasibility of (14h) at $t=0$. Constraints in (14f)-(14g)
for $t=1$, which are written as
$[x^{*}(2|0),x^{*}(3|0),\ldots,x^{*}(N|0),x(0),x(1)]\models\phi$,
$[x^{*}(3|0),x^{*}(4|0),\ldots,x^{*}(N|0),x(0),x(1),x^{*}(2|0)]\models\phi$,
$\ldots$, $[x(1),x^{*}(2|0),\ldots,x^{*}(N-1|0),x^{*}(N|0),x(0)]\models\phi$,
are feasible since they are identical to (14f)-(14g) at $t=0$. Note that due
to the choice $x(N+1|1)=x(0)$, constraints in (14h)-(14j) for $t=1$ are
identical to the first $N$ constraints in (14f)-(14g) and, hence, are
feasible. Finally, since $x(N+2|1)=x(1)$, $x(N+1|1)\in\mathcal{C}_{1}(x(1))$,
and thus, (14m) is feasible. 2) Suppose now that (14) is feasible at time
$t>N$, with optimal input sequence $[u^{*}(t:t+N|t)]$ inducing the optimal
trajectory $[x^{*}(t:t+N+1|t)]$. By applying $u(t)=u^{*}(t|t)$, the MAS is
driven to $x(t+1)=f(x(t),u(t))=x^{*}(t+1|t)$. Since
$x^{*}(t+N|t)\in\mathcal{C}_{1}(x(t))$, there is an admissible input, say
$\hat{u}(t+N)$, such that $f(x^{*}(t+N|t),\hat{u}(t+N))=x(t)$. Then, at time
$t+1$, we design the (not necessarily optimal) admissible input sequence
$[u(t+1:t+N+1|t+1)]=[u^{*}(t+1:t+N-1|t),\hat{u}(t+N),u^{*}(t|t)]$, which
yields a state sequence $[x(t+1:t+N+2|t+1)]$ the elements of which are
computed recursively starting from $x(t+1|t+1)$ resulting in
$[x(t+1:t+N+2|t+1)]=[x(t+1),x^{*}(t+2|t),x^{*}(t+3|t),\ldots,x^{*}(t+N|t),x(t),x(t+1)]$,
which we check for feasibility. First, we verify history-related constraints
(14c)-(14d), which, for time $t+1$, are written as
$[x(t-N+2),x(t-N+3),\ldots,x^{*}(t+1|t),x^{*}(t+2|t)]\models\phi$,
$[x(t-N+3),x(t-N+4),\ldots,x^{*}(t+2|t),x^{*}(t+3|t)]\models\phi$, $\ldots$,
$[x(t),x^{*}(t+1|t),\ldots,x^{*}(t+N-1|t),x^{*}(t+N|t)]\models\phi$, by
constraints (14c)-(14e) corresponding to the (previous) time step $t$.
Constraint (14e) for time $t+1$, namely,
$[x(t+1|t+1),x(t+2|t+1),\ldots,x(t+N+1|t+1)]\models\phi$, which is written as
$[x^{*}(t+1|t),x^{*}(t+2|t),\ldots,x^{*}(t+N|t),x(t)]\models\phi$, is
identical to constraint (14h) at time $t$ and, hence, is feasible. Constraints
in (14f)-(14g) at time $t+1$ are written as
$[x^{*}(t+2:t+N+1|t),x^{*}(t+1|t)]\models\phi$,
$[x^{*}(t+3:t+N+1|t),x^{*}(t+1|t),x^{*}(t+2|t)]\models\phi$, $\ldots$,
$[x^{*}(t+1:t+N+1|t)]\models\phi$, which are identical to constraints
(14f)-(14g) at time $t$, with a slight different order. Also, due to the
choice of $x(t+N+1|t+1)=x(t)$, constraints in (14h)-(14j) for the time step
$t+1$ are identical to constraints (14f)-(14g) at time $t+1$ and, hence, are
feasible. Lastly, since $x(t+N+2|t+1)=x(t+1)$, we have
$x(t+N+1)\in\mathcal{C}_{1}(x(t+1))$, and hence constraint (14m) is feasible.
This completes the proof.

## Appendix B

$\displaystyle\phi^{11}$
$\displaystyle=\square_{[0,30]}\|((x_{1})_{1},(x_{1})_{3})-5\bm{1}_{2}\|_{\infty}\leq
5$ (19a) $\displaystyle\phi^{12}$
$\displaystyle=\square_{[0,30]}\|((x_{2})_{1},(x_{2})_{3})-5\bm{1}_{2}\|_{\infty}\leq
5$ (19b) $\displaystyle\phi^{13}$
$\displaystyle=\square_{[0,30]}\|((x_{3})_{1},(x_{3})_{3})-5\bm{1}_{2}\|_{\infty}\leq
5$ (19c) $\displaystyle\phi^{21}$
$\displaystyle=\left(\lozenge_{[10,30]}\|((x_{1})_{1},(x_{1})_{3})-\begin{bmatrix}5&9\end{bmatrix}^{T}\|_{\infty}\leq
1\right)$
$\displaystyle\wedge\left(\lozenge_{[10,30]}\|((x_{1})_{1},(x_{1})_{3})-\begin{bmatrix}1&5\end{bmatrix}^{T}\|_{\infty}\leq
1\right)$ (19d) $\displaystyle\phi^{22}$
$\displaystyle=\left(\lozenge_{[10,30]}\|((x_{2})_{1},(x_{2})_{3})-\begin{bmatrix}8&8\end{bmatrix}^{T}\|_{\infty}\leq
1\right)$
$\displaystyle\wedge\left(\lozenge_{[10,30]}\|((x_{2})_{1},(x_{2})_{3})-\begin{bmatrix}2&2\end{bmatrix}^{T}\|_{\infty}\leq
1\right)$ (19e) $\displaystyle\phi^{23}$
$\displaystyle=\left(\lozenge_{[10,30]}\|((x_{3})_{1},(x_{3})_{3})-\begin{bmatrix}9&5\end{bmatrix}^{T}\|_{\infty}\leq
1\right)$
$\displaystyle\wedge\left(\lozenge_{[10,30]}\|((x_{3})_{1},(x_{3})_{3})-\begin{bmatrix}5&1\end{bmatrix}^{T}\|_{\infty}\leq
1\right)$ (19f) $\displaystyle\phi^{31}$
$\displaystyle=\square_{[0,30]}\|((x_{1})_{1},(x_{1})_{3})-((x_{2})_{1},(x_{2})_{3})\|_{\infty}\geq
0.1$ (19g) $\displaystyle\phi^{32}$
$\displaystyle=\square_{[0,30]}\|((x_{2})_{1},(x_{2})_{3})-((x_{3})_{1},(x_{3})_{3})\|_{\infty}\geq
0.1$ (19h)

## References

  * [1] O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,” in _Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems_ , Y. Lakhnech and S. Yovine, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 152–166.
  * [2] A. Donzé and O. Maler, “Robust Satisfaction of Temporal Logic over Real-Valued Signals,” in _8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS, 2010_ , Klosterneuburg, Austria, 2010, pp. 92–106.
  * [3] G. E. Fainekos and G. J. Pappas, “Robustness of temporal logic specifications for continuous-time signals,” _Theoretical Computer Science_ , vol. 410, no. 42, pp. 4262–4291, 2009.
  * [4] V. Raman, M. Maasoumy, A. Donze, R. M. Murray, A. Sangiovanni-Vincentelli, and S. A. Seshia, “Model predictive control with signal temporal logic specifications,” in _Proceedings of the IEEE Conference on Decision and Control_. IEEE, 2014, pp. 81–87.
  * [5] S. S. Farahani, V. Raman, and R. M. Murray, “Robust Model Predictive Control for Signal Temporal Logic Synthesis,” _IFAC Proceedings Volumes (IFAC-PapersOnline)_ , vol. 48, no. 27, pp. 323–328, 2015.
  * [6] S. Sadraddini and C. Belta, “Robust temporal logic model predictive control,” in _53rd Annual Allerton Conference on Communication, Control, and Computing_. IEEE, 2015, pp. 772–779.
  * [7] V. Raman, A. Donzé, D. Sadigh, R. M. Murray, and S. A. Seshia, “Reactive Synthesis from Signal Temporal Logic Specifications,” in _Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control_ , ser. HSCC ’15. New York, NY, USA: ACM, 2015, pp. 239–248.
  * [8] S. Ghosh, D. Sadigh, P. Nuzzo, V. Raman, A. Donzé, A. L. Sangiovanni-Vincentelli, S. S. Sastry, and S. A. Seshia, “Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications,” in _Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control_ , ser. HSCC ’16. New York, NY, USA: ACM, 2016, pp. 31–40.
  * [9] V. Kurtz and H. Lin, “Mixed-Integer Programming for Signal Temporal Logic With Fewer Binary Variables,” _IEEE Control Systems Letters_ , vol. 6, pp. 2635–2640, 2022.
  * [10] L. Lindemann and D. V. Dimarogonas, “Robust control for signal temporal logic specifications using discrete average space robustness,” _Automatica_ , vol. 101, pp. 377–387, 2019.
  * [11] Y. V. Pant, H. Abbas, and R. Mangharam, “Smooth operator: Control using the smooth robustness of temporal logic,” in _2017 IEEE Conference on Control Technol. and Applic. (CCTA)_ , 2017, pp. 1235–1240.
  * [12] N. Mehdipour, C.-I. Vasile, and C. Belta, “Arithmetic-geometric mean robustness for control from signal temporal logic specifications,” in _2019 American Control Conference (ACC)_ , 2019, pp. 1690–1695.
  * [13] D. Q. Mayne, J. B. Rawlings, C. V. Rao, and P. O. Scokaert, “Constrained model predictive control: Stability and optimality,” _Automatica_ , vol. 36, no. 6, pp. 789–814, 2000.
  * [14] S. Sadraddini and C. Belta, “Formal synthesis of control strategies for positive monotone systems,” _IEEE Trans. Automat. Contr._ , vol. 64, no. 2, pp. 480–495, 2019.
  * [15] M. Charitidou and D. V. Dimarogonas, “Receding horizon control with online barrier function design under signal temporal logic specifications,” _IEEE Trans. Automat. Contr._ , vol. 68, no. 6, pp. 3545–3556, 2023.
  * [16] M. Herceg, M. Kvasnica, C. Jones, and M. Morari, “Multi-Parametric Toolbox 3.0,” in _Proc. of the European Control Conference_ , Zürich, Switzerland, July 17–19 2013, pp. 502–510.
  * [17] F. Borrelli, A. Bemporad, and M. Morari, _Predictive Control for Linear and Hybrid Systems_. Cambridge University Press, 2017.
  * [18] F. Blanchini and S. Miani, _Set-Theoretic Methods in Control_ , ser. Systems & Control: Foundations & Applications. Birkhäuser, 2015.
  * [19] J. Löfberg, “Yalmip : A toolbox for modeling and optimization in matlab,” in _In Proceedings of the CACSD Conference_ , Taiwan, 2004.
  * [20] “Gurobi optimizer,” https://www.gurobi.com, 2023.