# Data-Driven Abstractions for Control Systems

Rudi Coppola  0000-0002-7767-2935 Student, IEEE  Andrea Peruffo
0000-0002-7767-2935 Member, IEEE and Manuel Mazo Jr  0000-0002-5638-5283
Senior Member, IEEE R. Coppola, A. Peruffo and M. Mazo are with Faculty of
Mechanical, Maritime and Materials Engineering, TU Delft, Delft, The
Netherlands<EMAIL_ADDRESS>
###### Abstract

At the intersection of dynamical systems, control theory, and formal methods
lies the construction of symbolic abstractions: these typically represent
simpler, finite-state models whose behaviour mimics the one of an underlying
concrete system but are easier to analyse. Building an abstraction usually
requires an accurate knowledge of the underlying model: this knowledge may be
costly to gather, especially in real-life applications. We aim to bridge this
gap by building abstractions based on sampling finite length trajectories.
Adding the controller degrees of freedom, we newly define the notion of
probabilistic alternating simulation, and provide probably approximately
correct (PAC) guarantees that the constructed abstraction includes all
behaviours of the concrete system and that it is suitable for control design,
for arbitrarily long time horizons, leveraging the scenario theory. Our method
is then tested on several numerical benchmarks.

Abstractions for control, formal methods, probabilistic guarantees, scenario
approach.

##  1 Introduction

Data-driven modeling and analysis is living a new renaissance with the
advances in machine learning and artificial intelligence enabled by
unprecedented computing power. The field of system verification, aiming at
providing formal performance and safety guarantees is not alien to this trend.
Recent work has been focused on the use of collected data from a system to
derive directly (i.e. with no model involved) barrier functions certifying
invariance [2, 25], or finite abstractions to verify and synthesize
controllers [12, 19, 24]. A popular approach is to employ scenario-based
optimization techniques to derive probably approximately correct (PAC)
guarantees on the performance metric of interest. The use of scenario-based
optimization requires independent samples, generated from the probability
distribution that drives the system’s uncertainty. A special case considered
in many works [12, 30, 31] is that of deterministic systems (for which a model
is not available), in which the only uncertainty is their initialization, i.e.
the initial state is drawn from some probability distribution, and the control
policy, usually chosen from a finite set of possible actions, and the samples
consist of individual transitions or, more generally, finite-length
trajectories. In this setting the independence of samples can be derived by
independently sampling the initial state: typically a uniform distribution is
selected for compact initial sets. If the set of initial conditions coincides
with the domain of interest, one can directly sample one-step transitions;
however, the scenario-based approach would provide guarantees for the
satisfaction of _one-step_ properties, provided that transitions are indeed
sampled independently. On the other hand, one is often interested in inferring
long (even infinite) horizon specifications from one-step properties. These
approaches are limited to provide guarantees for the time horizon used to
construct the data set, as for larger horizons nothing can be directly
inferred, unless some additional knowledge of the system is available, as for
example in [18].

Contributions. Addressing this limitation is the main objective of this work.
We consider deterministic systems with unknown dynamics and a random
initialization. Our approach provides a construction of data-driven finite
abstractions, built on the notions of alternating simulation and a particular
class of abstractions known as Strongest Asynchronous $\ell$-complete
Abstractions (or Approximations) (SA$\ell$CAs) [28]. We introduce the notion
of probabilistic alternating simulation, instrumental in describing the
relation between a deterministic (but randomly sampled) model and a transition
system constructed upon the collected system’s behaviours. Leveraging the
scenario theory, we establish PAC guarantees for the inclusion of the concrete
system’s finite behaviours in those of the abstraction. We clarify the role
played by the length of the trajectories used for constructing the
abstraction, and, by laying coarse assumptions on the concrete system’s
dynamics, we reveal how the PAC guarantees can be adapted to retain the
abstraction’s suitability for control over _longer_ trajectory lengths. This
enables the verification of properties, and synthesis of control policies,
over an arbitrarily long time horizon while preserving the PAC guarantees.

Related Work. Abstractions usually entail a model-based technique aimed at
extracting prominent features [29, 4]. The end goal of this process is to
represent the original system with a simpler object, typically with a finite
number of states, to streamline the verification of certain properties of the
original system or the formulation of a policy (or controller) that guarantees
fulfillment of a user-defined requirement. When the model is unknown, one can
opt for model identification, as demonstrated in, for example, [14], and, in a
second step, the identified model can be abstracted using conventional formal
techniques. The main shortcoming of model-based abstractions is that the
necessary computation for their construction rapidly grows with the state and
input dimension and the resolution of their discretization. Alternatively,
When the model is unknown, some recent works have recently proposed a method
to directly synthesize an abstraction from data, with guarantees of
correctness without the need to identify an underlying model. Recently, a
suite of techniques has emerged to build abstractions from data sampled from
unknown models. In [11, 3, 18], a sampled-based interval MDP is created using
the scenario approach to constrain transition probabilities in a stochastic
dynamical model. In [12], a notion of PAC alternating simulation relationship
is defined by sampling one-step state transitions. In [20], PAC over-
approximations of monotone systems are employed to construct models; in [16],
a sample-based growth rate is used to build an abstraction and synthesize a
controller.

At the heart of our work lies a type of abstraction known as SA$\ell$CA, [27,
28] which carries several interesting properties for our purposes and can be
constructed from the _complete_ knowledge of a concrete system’s output
trajectories, rather than its state trajectories. When only _partial_
knowledge is available, as in the case of abstracting the system from sampled
trajectories, certain undesired phenomena may arise. These phenomena, not only
limited to data-driven SA$\ell$CAs, are analyzed in detail in [10]. Further,
in [9] the authors propose the construction of data-driven $\ell$-complete
abstractions for linear autonomous systems; in this work, we extend the
results in [9] to include data-driven SA$\ell$CAs for nonlinear control
systems. these methods find applications also for event-triggered control
models [22, 23]. Recent work [5, 6] proposes the construction of a data-driven
memory-based Markov model for stochastic systems, equipped with an adaptive
method to estimate the size of the needed memory from observations. As we show
throughout this manuscript, memory is a key notion allowing us to use data-
driven SA$\ell$CAs for control.

Organisation This manuscript is organised as follows. Section 2 provides
relevant background information and notation used across this work. In Section
3, we describe transition systems and the systems’ relations, which represent
the main tool allowing us to craft an abstraction-based controller. Next, we
present a data-driven perspective on the construction of abstractions of
unknown systems in Section 4, leveraging scenario theory to provide PAC-type
guarantees. The PAC guarantees hold up until the time horizon used for
sampling the trajectories necessary to construct the abstraction; in Section 5
we outline the assumptions under which the abstraction can be used to extend
the guarantees for greater time horizons. We present experimental results for
these abstractions in Section 6, and we reserve a discussion and conclusion to
Sections 7.

##  2 Notation and Preliminaries

Given a set $\mathcal{V}$ we denote its $H$-th cartesian product by
$\mathcal{V}^{H}$, and its its power set by $\wp(\mathcal{V})$, unless
otherwise specified. For $v\in\mathcal{V}^{H}$ we denote its $(k+1)$-th
element by $v(k)$ for $k\in[0,H-1]$. We denote the restriction of $v$ to the
interval $I=[k_{1},k_{2}]$, with $k_{1}<k_{2}<H$ by
$v|_{[k_{1},k_{2}]}:=v(k_{1})...v(k_{2})$. Given two sequences
$v\in\mathcal{V}^{H}$ and $v^{\prime}\in\mathcal{V}^{H^{\prime}}$ we denote
their concatenation by $v\cdot v^{\prime}$. Given a relation
$\mathcal{R}\subseteq\mathcal{X}_{a}\times\mathcal{X}_{b}$ and a pair
$(x_{a},x_{b})\in\mathcal{R}$ we denote by
$\mathcal{R}_{\mathcal{X}_{b}}(x_{a}):=\\{x_{b}\in\mathcal{X}_{b}:(x_{a},x_{b})\in\mathcal{R}\\}$.
We denote the inverse relation of $\mathcal{R}$ by $\mathcal{R}^{-1}$, i.e.
$(x_{b},x_{a})\in\mathcal{R}^{-1}$ if and only if
$(x_{a},x_{b})\in\mathcal{R}$. We make extensive use of the sets
$\Delta:=\mathcal{X}\times\mathcal{Y}\times\mathcal{U}\times\mathcal{X}\times\mathcal{Y}$
and $\Gamma:=\mathcal{Y}\times\mathcal{U}\times\mathcal{Y}$, where the sets
$\mathcal{X}$, $\mathcal{Y}$, and $\mathcal{U}$ will be properly defined in
the following. For an integer $H$ we define
$\Delta_{H}:=\mathcal{X}^{H}\times\mathcal{Y}^{H}\times\mathcal{U}^{H}\times\mathcal{X}^{H}\times\mathcal{Y}^{H}$
and $\Gamma_{H}:=\mathcal{Y}^{H}\times\mathcal{U}^{H}\times\mathcal{Y}^{H}$.
Consider an element $i_{H}\in\Delta_{H}$: we equivalently write
$i_{H}=(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in\Delta_{H}$, where
$\xi\in\mathcal{X}^{H}$, $\gamma\in\mathcal{Y}^{H}$ and so on. Finally, for
any $k\in[0,H-1]$ we write
$i_{H}(k)=(\xi(k),\gamma(k),\upsilon(k),\xi^{\prime}(k),\gamma^{\prime}(k))$.
Analogous considerations hold for an element
$w_{H}=(\gamma,\upsilon,\gamma^{\prime})\in\Gamma_{H}$. Denote by
$(\Omega_{i},\mathcal{F}_{i},\mu_{\omega_{i}})$ for $i=1,2$, two probability
spaces, where $\Omega_{i}$ is the sample space, endowed with a
$\sigma$-algebra $\mathcal{F}_{i}$ and a probability measure
$\mu_{\omega_{i}}$. We define the product probability space
$(\mathcal{P},\mathcal{W},\mu_{p})$ where
$\mathcal{P}=\Omega_{1}\times\Omega_{2}$, $\mathcal{W}$ is the product
$\sigma$-algebra denoted $\mathcal{W}=\mathcal{F}_{1}\times\mathcal{F}_{2}$,
and $\mu_{p}$ is the product measure given by
$\mu_{\omega_{1}}\times\mu_{\omega_{2}}$.

###  2.1 Dynamical Models

Consider a time-invariant dynamical system

$\Sigma(x):=\begin{cases}x_{k+1}=f(x_{k},u_{k}),\\\ y_{k}=h(x_{k}),\\\
x_{0}=x,\end{cases}$ (1)

where $x_{k}\in\mathcal{X}\subset\mathbb{R}^{n_{x}}$ is the plant’s state at
time $k\in\mathbb{N}_{+}$, $n_{x}$ is the state-space dimension, $x_{0}$ is
the initial state, $y_{k}\in\mathcal{Y}\subset\mathbb{N}$ is the system output
with $|\mathcal{Y}|<\infty$, $u_{k}\in\mathcal{U}\subset\mathbb{R}^{n_{u}}$ is
the system input at time $k$ with $|\mathcal{U}|<\infty$, $n_{u}$ is the input
dimension. We denote $u_{H}$ as a sequence of control inputs of length $H$.

######  Definition 1 ([7])

Let $(\mathcal{X},d_{X})$ be a complete metric space. Let the map $f$ defined
in (1) satisfy the inequailty

$m_{X}d_{X}(x,y)\leq d_{X}(f(x,u),f(y,u))$ (2)

for $m_{X}>0$ all $x,y\in\mathcal{X}$ and $u\in\mathcal{U}$. The map $f$ is
said to be Lipschitz invertible. $\square$

######  Definition 2 ([7])

Let $(\mathcal{X},d_{X})$ and $(\mathcal{U},d_{U})$ be complete metric spaces.
The map $f$ in (1) is uniformly contracting w.r.t. $x$ if there exists
$0<l_{X}<1$ such that

$d_{X}(f(x,u),f(y,u))\leq l_{X}d_{X}(x,y),$

for all $x,y\in\mathcal{X},\text{ and }u\in\mathcal{U}.$ Similarly, $f$ is
uniformly Lipschitz w.r.t. $u$ if there exists $l_{U}>0$ such that

$d_{X}(f(x,u),f(x,v))\leq l_{U}d_{U}(u,v),$

$\text{ for all }x\in\mathcal{X},\text{ and }u,v\in\mathcal{U}.$ $\square$

###  2.2 Scenario Theory

Let $(\Omega,\mathcal{F},\mu)$ be a probability space, and let $\Omega^{N}$ be
the $N$-Cartesian product of the sample space and with $\mu^{N}$ its product
measure. A point in $(\Omega^{N},\mathcal{F}^{N},\mu^{N})$ is thus a sample
$(\omega_{1},\ldots,\omega_{N})$ of $N$ elements drawn independently from
$\Omega$ according to the same probability $\mu$. Each $\omega_{i}$ is
regarded as an observation, or _scenario_ [8, 13]. Given $N$ samples, we aim
at taking a _decision_ , e.g. construct a classifier, or compute a regression
function, from a set $\Theta$, i.e. the optimization space – no particular
structure is assumed for this set. To every $\omega\in\Omega$ there is
associated a constraint set $\Theta_{\omega}\subseteq\Theta$. The scenario
theory offers a way to compute a solution $\theta_{N}^{*}$ satisfying all the
constraints $\Theta_{\omega_{i}}$ imposed by the set of $N$ i.i.d. samples
while quantifying the probability that a new random sample $\omega\in\Omega$
would result in the pre-computed solution $\theta^{*}_{N}$ violating the new
constraint $\Theta_{\omega}$. Hence, we are interested in evaluating the
generalization power of the solution, i.e. the performance of
$\theta_{N}^{*}$. To this end, we quantify the probability of extracting a
sample resulting in a constraint violated by a $\theta\in\Theta$ as follows.

######  Definition 3 (Violation [8])

The _violation probability_ (or violation for short) of a given
$\theta\in\Theta$ and the _violation set_ are respectively defined as

$V(\theta)=\mu(\,\omega\in\mathcal{V(\theta)}),\quad\mathcal{V(\theta)}=\\{\omega:\theta\notin\Theta_{\omega}\\}.$
(3)

$V(\theta)$ quantifies the probability with which a new randomly selected
constraint $\Theta_{\omega}$ is violated by $\theta$. We say that $\theta$ is
$\epsilon$-robust against constraint violation if $V(\theta)\leq\epsilon$.
$\square$

Notice that in general $V(\theta)$ is not directly computable since $\mu$ is
not known. Under mild assumptions, see [13, Assumption 1], a confidence bound
can be derived:

######  Theorem 1 (PAC bounds [13, Theorem 1])

Given a confidence $\beta\in(0,1)$ and the solution $\theta^{*}_{N}$, it holds

$\mu^{N}(V(\theta^{*}_{N})\leq\epsilon(s^{*}_{N},\beta,N))\geq 1-\beta,$ (4)

where $\epsilon(\cdot)$ is the solution of a polynomial equation (omitted here
for brevity) and $s^{*}_{N}$ is the _complexity_ of the solution – it
represents the cardinality of the smallest subset of the sample set that
yields the same solution $\theta^{*}_{N}$.

###### Remark 1

In this work we consider a discrete sample space $\Omega$, therefore we refer
to the scenario theory for degenerate problems, as per [13, 8].

##  3 Problem formulation and System Description

We adopt the framework of finite-state abstractions in the form of transition
systems.

######  Definition 4 (Transition System (TS))

A transition system $S$ is a tuple
$(\mathcal{X},\mathcal{X}_{0},\mathcal{U},\delta,\mathcal{Y},\mathcal{H})$,
where $\mathcal{X}$ is the set of states,
$\mathcal{X}_{0}\subseteq\mathcal{X}$ is the set of initial states,
$\mathcal{U}$ is the set of inputs, $\mathcal{Y}$ is the set of outputs,
$\delta\subseteq\mathcal{X}\times\mathcal{U}\times\mathcal{X}$ is a transition
relation, and $\mathcal{H}:\mathcal{X}\rightarrow\mathcal{Y}$ is an output
map. $\square$

We denote the set of $u$-successor states of a state $x$ as
$\text{Post}_{u}(x):=\\{x^{\prime}\in\mathcal{X}\ :\
(x,u,x^{\prime})\in\delta\\}$ and the set of admissible inputs at $x$ by
$U_{\delta}(x):=\\{u\in\mathcal{U}\ :\ \text{Post}_{u}(x)\neq\emptyset\\}$.
Given $x\in\mathcal{X}_{0}$ and an $H$-long input sequence
$u_{H}\in\mathcal{U}^{H}$ we define respectively the set of full and external
$H$-behaviour of any transition system $S$ as

$\mathcal{I}_{H}(S,x_{0},u_{H}):=\\{(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in\Delta_{H}\
:\ \xi(0)=x_{0}\ \wedge\\\ \upsilon=u_{H}\wedge\forall j\in[0,H-1]\ .\
(\xi(j),\upsilon(j),\xi^{\prime}(j))\in\delta\ \wedge\\\
\gamma(k)=\mathcal{H}(\xi(k))\wedge\gamma^{\prime}(k)=\mathcal{H}(\xi^{\prime}(k))\wedge\\\
(\xi,\gamma)|_{[1,H-1]}=(\xi^{\prime},\gamma^{\prime})|_{[0,H-2]}\\},$ (5)
$\mathcal{B}_{H}(S,x_{0},u_{H}):=\\{(\gamma,\upsilon,\gamma^{\prime})\in\Gamma_{H}:\\\
\exists\xi,\xi^{\prime}\in\mathcal{X}^{H}\ .\
(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in\mathcal{I}_{H}(S,x_{0},u_{H})\\}.$
(6)

In practical terms, $\mathcal{I}_{H}(S,x_{0},u_{H})$ and
$\mathcal{B}_{H}(S,x_{0},u_{H})$ represent $H$ transitions of system $S$,
starting from $x_{0}$, given the input sequence $u_{H}$; the former includes
information on the state, output, and input, the latter only on the output and
input. We denote by $\mathcal{I}_{H}(S)$ and $\mathcal{B}_{H}(S)$ the set of
all full and external $H$-behaviours originating from any initial condition
$x$ and input sequence $u_{H}$ respectively, that is

$\displaystyle\mathcal{I}_{H}(S)$
$\displaystyle:=\\{i_{H}\in\mathcal{I}_{H}(S,x,u_{H})\ :\
x\in\mathcal{X}_{0},u_{H}\in\mathcal{U}^{H}\\},$
$\displaystyle\mathcal{B}_{H}(S)$
$\displaystyle:=\\{w_{H}\in\mathcal{B}_{H}(S,x,u_{H})\ :\
x\in\mathcal{X}_{0},u_{H}\in\mathcal{U}^{H}\\}.$

The cornerstone of our technique is the notion of $\ell$-sequence, i.e. a
sequence of $\ell$ external behaviours. In particular, we are interested in
drawing a connection between a concrete state $x\in\mathcal{X}$ and every
possible input-output sequence of length $\ell$ that led to that state, i.e.
its recent past or memory. To define the past for initial states
$x\in\mathcal{X}_{0}$ we extend the notation for internal and external
behaviours to negative time indexes using the special symbol $\diamond$, so
that $i_{H}(-1):=(\diamond,\diamond,\diamond,\xi(0),\gamma(0))$ and
$i_{H}(k):=(\diamond,\diamond,\diamond,\diamond,\diamond)$ for $k<-1$.
Similarly, every $w_{H}(-1):=(\diamond,\diamond,\gamma(0))$ and
$w_{H}(k):=(\diamond,\diamond,\diamond)$ for $k<-1$.

Let us now consider the set of external behaviours of length $H$ and consider
a value $\ell$, where $\ell<H$: any behaviour of length $H$ can be split into
subsequences of length $\ell$. We denote the set of all $\ell$-subsequences of
all external behaviours starting from any admissible initial condition and
input sequence by

$\Pi_{\ell,H}:=\bigcup_{w_{H}\in\mathcal{B}_{H}(S)}\bigcup_{k\in[0,H-1]}w_{H}\left|{}_{[k-\ell+1,k]}\right.,$
(7)

Note that, to alleviate the notation, we intentionally leave out the
dependency of $\Pi_{\ell,H}$ on $S$ in the definition above, since the system
under consideration will be evident from the context and always referred to
the concrete system.

Further, let us define the set of external strings of length $\ell$ for a
state $x\in\mathcal{X}$ by

$\mathcal{E}_{\ell,H}(x):=\\{(\alpha,\beta,\alpha^{\prime})\in\Pi_{\ell,H}\
:\exists(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in\mathcal{I}_{H}(S),\\\
\exists j\in\mathbb{N}\ .\
(\alpha,\beta,\alpha^{\prime})=(\gamma,\upsilon,\gamma^{\prime})|_{[j-\ell+1,j]}\wedge\xi^{\prime}(j)=x\\},$
(8)

in words, $\mathcal{E}_{\ell,H}(x)$ is the set of $\ell$-behaviours that the
system can generate immediately before reaching $x$ in at most $H$ transitions
from an initial condition. If a state $x$ can be reached in less than $\ell$
transitions starting from an initial state, one or more corresponding external
strings will include the special symbol $\diamond$. For example, if $\ell=3$
and the state $x^{\prime}$ can be reached in one transition by picking the
control input $u$ from the initial state $x$, then
$((\diamond,\diamond,\diamond),(\diamond,\diamond,\mathcal{H}(x)),(\mathcal{H}(x),u,\mathcal{H}(x^{\prime})))\in\mathcal{E}_{3,H}(x^{\prime})$.
We define the equivalence class of an $\ell$-sequence as

$[w_{\ell}]:=\\{x:w_{\ell}\in\mathcal{E}_{\ell,H}(x)\\},$ (9)

i.e. the set of all states $x$ that share a given external behaviour
$w_{\ell}$.

###### Example 1

Let $S$ be the transition system depicted in Fig. 1, where
$\mathcal{X}=\\{x_{1},x_{2},x_{3}\\}$, $\mathcal{X}_{0}=\\{x_{1}\\}$,
$\mathcal{U}=\\{u_{a},u_{b}\\}$, and $\mathcal{Y}=\\{y_{1},y_{2}\\}$. Consider
a time horizon $H=3$ and the input sequence $u_{3}=u_{a}u_{b}u_{a}$. The
internal and external behaviours initialized from $x_{1}$, are given by

$\displaystyle\mathcal{I}_{3}(S,x_{1},u_{3})$
$\displaystyle=\\{((x_{1},y_{1},u_{a},x_{2},y_{2}),(x_{2},y_{2},u_{b},x_{2},y_{2}),$
$\displaystyle(x_{2},y_{2},u_{a},x_{3},y_{2}))\\},$
$\displaystyle\mathcal{B}_{3}(S,x_{1},u_{3})$
$\displaystyle=\\{((y_{1},u_{a},y_{2}),(y_{2},u_{b},y_{2}),(y_{2},u_{a},y_{2}))\\}.$

Considering $\ell=1$, following (7) we split
$\mathcal{B}_{3}(S,x_{1},u_{3})\in\mathcal{B}_{H}(S)$ in subsequences of
length $1$ and conclude that

$\\{(\diamond,\diamond,y_{1}),(y_{1},u_{a},y_{2}),(y_{2},u_{b},y_{2}),(y_{2},u_{a},y_{2})\\}\subset\Pi_{1,3}.$

Moreover, from (8) we have
$(\diamond,\diamond,y_{1})\in\mathcal{E}_{1,3}(x_{1})$,
$\\{(y_{1},u_{a},y_{2}),(y_{2},u_{b},y_{2})\\}=\mathcal{E}_{1,3}(x_{2})$, and
$(y_{2},u_{a},y_{a})\in\mathcal{E}_{1,3}(x_{3})$. We can repeat these steps
for every input sequence of length $3$ to obtain $\Pi_{1,3}$.

For $\ell=2$, following the same procedure, we obtain
$((\diamond,\diamond,\diamond),(\diamond,\diamond,y_{1}))\in\mathcal{E}_{2,3}(x_{1})$,
$((\diamond,\diamond,y_{1}),(y_{1},u_{a},y_{2}))\in\mathcal{E}_{2,3}(x_{2})$,
$((y_{1},u_{a},y_{2}),(y_{2},u_{b},y_{2}))\in\mathcal{E}_{2,3}(x_{2})$, and
finally
$((y_{2},u_{b},y_{2}),(y_{2},u_{a},y_{2}))\in\mathcal{E}_{2,3}(x_{3})$. Note
that each of these 2-sequences belongs to $\Pi_{2,3}$. $\square$

$x_{1}$ $y_{1}$ ${x_{2}}$ ${y_{2}}$${x_{3}}$
${y_{2}}$$u_{a}$$u_{b}$$u_{b}$$u_{a}$$u_{b}$$u_{a}$$\mathcal{H}(x_{1})=y_{1}$$\text{Post}_{u_{a}}(x_{1})=\\{x_{2}\\}$$\text{Post}_{u_{b}}(x_{1})=\\{x_{3}\\}$$U_{\delta}(x_{1})=\\{u_{A},u_{B}\\}$
Figure 1: Illustration of the transition system of Example 1.

The dynamical system $\Sigma$ defined in $\eqref{eq:deterministic-sys}$ can be
equivalently represented as a TS, possibly with an infinite state space. From
here on, we denote such a TS by $S_{\Sigma}$, we refer to it as the
_embedding_ of $\Sigma$ to a TS, and assume that the concrete system
$S_{\Sigma}$ satisfies the following Assumption 1.

###### Assumption 1

$S_{\Sigma}$ has _free input_ , i.e. $U_{\delta}(x)=\mathcal{U}$ for all $x$,
is _deterministic_ , i.e. $|\text{Post}_{u}(x)|\leq 1$ for every
$x\in\mathcal{X}$ and $u\in\mathcal{U}$, _non-blocking_ , i.e. every state has
at least one successor for every input, and has $\mathcal{X}_{0}=\mathcal{X}$.
In short, $|\text{Post}_{u}(x)|=1$ for every $x\in\mathcal{X}$ and
$u\in\mathcal{U}$.

The assumption that $\mathcal{X}_{0}=\mathcal{X}$ simplifies our notation in
that it implies that the horizon $H$ does not affect the definition of (7) and
(8). In practical terms, every $\ell$-sequence that the system can generate at
any point in time, can also be generated as an initial sequence. Formally, if
$(\alpha,\beta,\alpha^{\prime})\in\mathcal{E}_{\ell,H}(x)$ then there exists
$(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in\mathcal{I}_{H}(S)$ such
that for some $j$ it holds that $\gamma^{\prime}(j)=x$ and
$(\alpha,\beta,\alpha^{\prime})=(\gamma,\upsilon,\gamma^{\prime})|_{[j-\ell+1,j]}$.
But since $\mathcal{X}_{0}=\mathcal{X}$, then
$\xi(j-\ell+1)\in\mathcal{X}_{0}$ which implies that
$(\alpha,\beta,\alpha^{\prime})\in\mathcal{E}_{\ell,\ell+1}(x)$; hence, for
all $x\in\mathcal{X}$ it holds that
$\mathcal{E}_{\ell,\ell+1}(x)=\mathcal{E}_{\ell,H}(x)$ for every $H>\ell$.
Moreover, $\bigcup_{x}\mathcal{E}_{\ell,H}(x)=\Pi_{\ell,H}$. From now on, we
denote the corresponding external strings of a state $x$ simply as
$\mathcal{E}_{\ell}(x)$ and the set of all $\ell$-subsequences of all external
behaviours as $\Pi_{\ell}$. The case that $\mathcal{X}_{0}\neq\mathcal{X}$
follows _mutatis mutandis_ with no conceptual modifications.

###  3.1 Systems’ relations

Let us now introduce two key notions: an _alternating simulation relation_ and
a _simulation relation_. The former is instrumental in refining a policy
synthesised on an abstraction to a controller for the concrete system. For
SA$\ell$CAs, the existence of the latter is equivalent to the existence of an
alternating simulation relation, as shown in the extended version of [28]. We
recall both definitions below. We consider an observation comprising both
input and output, similarly to [28] (contrary to the common definition, see
e.g. [29], where only the output is observed); further, including the input in
the observation allows for the construction of a more refined TS. For
simplicity, we also assume that the abstraction and the concrete system share
the same input space.

######  Definition 5 (Simulation relation [29, Definition 4.7])

Consider two systems $S_{a}$ and $S_{b}$ with
$\mathcal{Y}_{a}=\mathcal{Y}_{b}$, and $\mathcal{U}_{a}=\mathcal{U}_{b}$. A
relation $\mathcal{R}\subseteq\mathcal{X}_{a}\times\mathcal{X}_{b}$ is a
simulation relation from $S_{a}$ to $S_{b}$ w.r.t.
$\mathcal{U}\times\mathcal{Y}$, written
$S_{a}\preceq^{\mathcal{R}}_{S.}S_{b}$, if the following three conditions are
satisfied:

  * •

$\forall x_{a0}\in\mathcal{X}_{a0}\ .\ \exists x_{b0}\in\mathcal{X}_{b0}$ with
$(x_{a0},x_{b0})\in\mathcal{R}$,

  * •

$(x_{a},x_{b})\in\mathcal{R}\implies\mathcal{H}_{a}(x_{a})=\mathcal{H}_{b}(x_{b})$,

  * •

$(x_{a},x_{b})\in\mathcal{R}\implies(\forall u_{a}\in
U_{\delta_{a}}(x_{a}),\exists u_{b}\in U_{\delta_{b}}(x_{b})\ .\ \\\
\forall(x_{a},u_{a},x_{a}^{\prime})\in\delta_{a},\exists
x_{b}^{\prime}\in\mathcal{X}_{b}\ .\
(x_{b},u_{b},x_{b}^{\prime})\in\delta_{b}\wedge(x_{a}^{\prime},x_{b}^{\prime})\in\mathcal{R}\wedge
u_{a}=x_{b})$.

######  Definition 6 (Alternating simulation relation [29, Definition 4.19])

Consider two systems $S_{a}$ and $S_{b}$ with
$\mathcal{Y}_{a}=\mathcal{Y}_{b}$, and $\mathcal{U}_{a}=\mathcal{U}_{b}$. A
relation $\mathcal{R}\subseteq\mathcal{X}_{b}\times\mathcal{X}_{a}$ is an
alternating simulation relation from $S_{b}$ to $S_{a}$ w.r.t.
$\mathcal{U}\times\mathcal{Y}$, written
$S_{b}\preceq_{A.S.}^{\mathcal{R}}S_{a}$, if the following three conditions
are satisfied:

  * •

$\forall x_{b0}\in\mathcal{X}_{b0}\ .\ \exists x_{a0}\in\mathcal{X}_{a0}$ with
$(x_{b0},x_{a0})\in\mathcal{R}$,

  * •

$(x_{b},x_{a})\in\mathcal{R}\implies\mathcal{H}_{a}(x_{b})=\mathcal{H}_{b}(x_{a})$,

  * •

$(x_{b},x_{a})\in\mathcal{R}\implies(\forall u_{b}\in
U_{\delta_{b}}(x_{b}),\exists u_{a}\in U_{\delta_{a}}(x_{a})\ .\ \\\
\forall(x_{a},u_{a},x_{a}^{\prime})\in\delta_{a}\implies\exists
x_{b}^{\prime}\in\mathcal{X}_{b}\ .\
(x_{b},u_{b},x_{b}^{\prime})\in\delta_{b}\wedge(x_{b}^{\prime},x_{a}^{\prime})\in\mathcal{R}\wedge
u_{a}=u_{b})$.

###### Remark 2

Note that if $\ \forall x_{a0}\ .\ \exists x_{b0}$ s.t.
$(x_{b0},x_{a0})\in\mathcal{R}$ and $\forall(x_{b},x_{a})\in\mathcal{R}\ .\
U_{\delta_{a}}(x_{a})=U_{\delta_{b}}(x_{b})$ then the above definition also
defines a _simulation relation_ $\mathcal{R}^{-1}$ from $S_{a}$ to $S_{b}$.
Then, we can formally write

$S_{a}\preceq^{\mathcal{R}^{-1}}_{S.}S_{b}\preceq_{A.S.}^{\mathcal{R}}S_{a}.$

As anticipated, in addition to the standard definition of (alternating)
simulation relation we impose the additional condition $u_{a}=u_{b}$.

###  3.2 Strongest Asynchronous $\ell$-complete Abstractions

In [27, 28] the authors introduce a particular class of abstractions known as
SA$\ell$CA, here adapted and reformulated as a TS. One of the advantages of
the SA$\ell$CA is that for its construction we only require the knowledge of
the external behaviours, i.e. without the knowledge of the internal mechanisms
of the underlying model, motivating our interest in this specific class when
combined with data-driven techniques.

######  Definition 7 (SA$\ell$CA [28])

Let
$S:=(\mathcal{X},\mathcal{X}_{0},\mathcal{U},\delta,\mathcal{Y},\mathcal{H})$
be a TS satisfying Assumption 1, and consider the set of all
$(\ell+1)$-subsequences of all external behaviours starting from any
admissible initial condition $\Pi_{\ell+1}$. Then, the TS
$S_{\ell}:=(\mathcal{X}_{\ell},\mathcal{X}_{\ell
0},\mathcal{U},\delta_{\ell},\mathcal{Y},\mathcal{H}_{\ell})$ is called the
SA$\ell$CA of $S$, where

$\displaystyle\mathcal{X}_{\ell}$ $\displaystyle:=\Pi_{\ell}$
$\displaystyle\mathcal{X}_{\ell 0}$
$\displaystyle:=\\{b_{\ell}\in\Pi_{\ell}:\exists y\in\mathcal{Y}\ .\
b_{\ell}(\ell-1)=(\diamond,\diamond,y)\\}$ $\displaystyle\delta_{\ell}$
$\displaystyle:=\\{(x_{\ell},u,x_{\ell}^{\prime})\ :\
x_{\ell}|_{[1,\ell-1]}=x_{\ell}^{\prime}|_{[0,\ell-2]}\wedge$ $\displaystyle
x_{\ell}^{\prime}(\ell-1)=(y,u,y^{\prime})\Rightarrow
x_{\ell}\cdot(y,u,y^{\prime})\in\Pi_{\ell+1}\\}$ $\displaystyle
H_{\ell}(x_{\ell})$
$\displaystyle:=\\{y^{\prime}\in\mathcal{Y}:(y,u,y^{\prime})=x_{\ell}(\ell-1)\\}$

Note that we implicitly make use of the fact that from $\Pi_{\ell+1}$ is
possible to construct $\Pi_{\ell}$, indeed it is evident that the set of all
$\ell$-subsequences of all external behaviours can be obtained with the same
procedure either from the set of all $\ell+1$-subsequences or, as per (7),
from the set of all external $H$-behaviours.

Referring to Example 1, the corresponding SA$\ell$CA with $\ell=1$ is shown in
Figure 2.

${(\diamond,\diamond,y_{1})}$ ${y_{1}}$start${(y_{1},u_{a},y_{2})}$
${y_{2}}$${(y_{1},u_{b},y_{2})}$ ${y_{2}}$${(y_{2},u_{a},y_{2})}$
${y_{2}}$${(y_{2},u_{a},y_{1})}$ ${y_{1}}$${(y_{2},u_{b},y_{2})}$
${y_{1}}$$u_{a}$$u_{b}$$u_{a}$$u_{b}$$u_{a}$$u_{b}$$u_{a}$$u_{b}$$u_{b}$$u_{a}$$u_{a}$
Figure 2: Illustration of the SA$\ell$CA for the system described in Example 1
for $\ell=1$.

The following three properties motivate our choice of abstracting the system
as a SA$\ell$CA: $(i)$ the relation given by

$\mathcal{R}=\\{(x,x_{\ell})\in\mathcal{X}\times\mathcal{X}_{\ell}:\
x_{\ell}\in\mathcal{E}_{\ell}(x)\\}$ (10)

is a simulation relation from $S$ to $S_{\ell}$ and the inverse relation
$\mathcal{R}^{-1}$ is an alternating simulation relation from $S_{\ell}$ to
$S$ assuming that $S$ has free input, see the extended version of [28]. In
Section 4 we show how to construct a data-driven version of relation (10) and
successively we show that there exists a similar link with the inverse
relation; $(ii.)$ knowledge of the set $\Pi_{\ell+1}$, deriving from all the
external behaviours of $S$, is sufficient to construct the SA$\ell$CA;
$(iii.)$ given the SA$\ell$CA, defining the set of corresponding external
strings based on the _past_ of a state, as in (8), is an arbitrary choice:
indeed, one can define the set of corresponding external strings based on the
_future_ external behaviours following a concrete state – see [28]. Equation
(8) ensures that (10) defines a simulation relation from $S$ to $S_{\ell}$,
and, since the concrete system has free input, $\mathcal{R}^{-1}$ defines an
alternating simulation relation from $S_{\ell}$ to $S$. Moreover, by defining
the corresponding external strings based on the past it is not necessary to
know $\mathcal{R}$ explicitly. In other words, once we construct the
SA$\ell$CA, if $(x,x_{\ell})\in\mathcal{R}$ and by applying input $u$ the
concrete system transitions from $x$ to $x^{\prime}$ leading to the
observation $(\mathcal{H}(x),u,\mathcal{H}(x^{\prime}))$, we automatically
conclude that there exists a transition in $S_{\ell}$ from $x_{\ell}$ to
$x_{\ell}^{\prime}:=x_{\ell}|_{[1,\ell-1]}\cdot(\mathcal{H}(x),u,\mathcal{H}(x^{\prime}))$
such that $(x^{\prime},x_{\ell}^{\prime})\in\mathcal{R}$.

##  4 Data-driven Abstractions

The construction of a SA$\ell$CA implicitly requires the knowledge of all
possible external behaviours of a system of interest. In many practical
applications, this is a costly assumption. To overcome this issue, we aim to
construct an abstraction starting from sampled external behaviours of the
concrete system.

Given a system $S_{a}$, we define the random variable
$i_{u_{H}}^{a}:\mathcal{X}_{0}^{a}\to\wp(\Delta^{a}_{H})$

$i_{u_{H}}^{a}:=\mathcal{I}_{H}(S_{a},x_{0}^{a},u_{H}),$ (11)

where $\Delta^{a}_{H}$ is defined according to
$\Delta^{a}:=\mathcal{X}_{a}\times\mathcal{Y}_{a}\times\mathcal{U}_{a}\times\mathcal{X}_{a}\times\mathcal{Y}_{a}$
and the convention chosen in Section 2. Equation (11) describes the set of
full behaviours of $S_{a}$, for a given $u_{H}$, starting from the randomly
extracted initial condition $x_{0}^{a}$. For deterministic systems,
$i_{u_{H}}^{a}$ is unique, whereas for nondeterministic systems it may
represent a set of behaviours. Given a system $S_{b}$ and a relation
$\mathcal{R}\subseteq\mathcal{X}_{a}\times\mathcal{X}_{b}$ we define the
random variable $i^{b}_{u_{H}}:\mathcal{X}_{a0}\rightarrow\wp(\Delta_{H}^{b})$

$i_{u_{H}}^{b}:=\bigcup_{x_{b0}\in\mathcal{R}_{\mathcal{X}_{b}}(x_{a0})\cap\mathcal{X}_{b0}}\mathcal{I}_{H}(S_{b},x_{b0},u_{H}),$
(12)

which describes the set of full behaviours of $S_{b}$, for a given $u_{H}$,
starting from all the initial conditions that are related to $x_{0}^{a}$
through $\mathcal{R}$.

Considering only _sampled_ behaviours naturally leads to an _approximation_ of
the SA$\ell$CA, i.e. only a subset of $\Pi_{\ell+1}$ is available. We thus
generalize the definition of (alternating) simulation relation to encompass
the case of a randomly sampled initial condition in the concrete system: we
denote this notion as _probabilistic_ (alternating) simulation relation.

######  Definition 8 (Probabilistic simulation relation)

Consider two systems $S_{a}$ and $S_{b}$ with
$\mathcal{Y}_{a}=\mathcal{Y}_{b}$ and
$\mathcal{U}_{a}=\mathcal{U}_{b}=\mathcal{U}$, and a relation
$\mathcal{R}\subseteq\mathcal{X}_{a}\times\mathcal{X}_{b}$. Additionally,
given the probability space $(\mathcal{X}_{a0},\mathcal{G}_{a},\mu_{x_{a}})$,
consider the augmented transition relations $\Delta_{a}$ and $\Delta_{b}$ of
systems $S_{a}$ and $S_{b}$ respectively, for a fixed
$u_{H}\in\mathcal{U}^{H}$, and with $i^{a}_{u_{H}}$ defined as in (11), we say
that $\mathcal{R}$ is a probabilistic simulation relation from $S_{a}$ to
$S_{b}$ with respect to $\mathcal{U}\times\mathcal{Y}$ until horizon $H$ with
probability not less than $1-\epsilon$ if

$\displaystyle\mu_{x_{a}}(x_{a0}\in\mathcal{V}({S_{b}},\mathcal{R},H))<\epsilon,$
(13)

where the violation set $\mathcal{V}({S_{b}},\mathcal{R},H)$ is defined

$\displaystyle\qquad\mathcal{V}({S_{b}},\mathcal{R},H):=\\{x_{a0}:\exists
u_{H}\in\mathcal{U}^{H}\ .\ i_{u_{H}}^{a}\neq\emptyset\ \wedge$
$\displaystyle\quad\exists(\xi_{a},\gamma_{a},\upsilon_{a},\xi^{\prime}_{a},\gamma^{\prime}_{a})\in
i_{u_{H}}^{a},\nexists(\xi_{b},\gamma_{b},\upsilon_{b},\xi^{\prime}_{b},\gamma^{\prime}_{b})\in
i_{u_{H}}^{b}\ .\ $
$\displaystyle(\gamma_{a},\upsilon_{a},\gamma_{a}^{\prime})=(\gamma_{b},\upsilon_{b},\gamma_{b}^{\prime})\wedge\forall
k\geq-1\ .\ (\xi_{a}^{\prime}(k),\xi_{b}^{\prime}(k))\in\mathcal{R}\\}.$ (14)

More compactly, we write

$\mu_{x_{a}}(S_{a}\ {}^{H}{\preceq}_{S.}^{\mathcal{R}}S_{b})<\epsilon,$

where ${}^{H}{\preceq}_{S.}^{\mathcal{R}}$ highlights that the probabilistic
simulation relation is referring to the relation $\mathcal{R}$ and it is
relative to a time horizon $H$. $\square$

######  Definition 9 (Probabilistic alternating simulation relation)

Under the same conditions of Definition 8, we say that
$\mathcal{Z}\subseteq\mathcal{X}_{b}\times\mathcal{X}_{a}$ is a probabilistic
alternating simulation relation from $S_{b}$ to $S_{a}$ with respect to
$\mathcal{U}\times\mathcal{Y}$ until horizon $H$ with probability not less
than $1-\epsilon$ if

$\displaystyle\mu_{x_{a}}(x_{a0}\in\mathcal{Q}({S_{b}},\mathcal{Z},H))<\epsilon,$
(15)

where the violation set $\mathcal{Q}({S_{b}},\mathcal{Z},H)$ is defined

$\displaystyle\mathcal{Q}({S_{b}},\mathcal{Z},H):=\\{x_{a0}:\exists
u_{H}\in\mathcal{U}^{H}\ .\
i_{u_{H}}^{b}\neq\emptyset\wedge(i^{a}_{u_{H}}=\emptyset\vee$
$\displaystyle\quad\exists(\xi_{a},\gamma_{a},\upsilon_{a},\xi^{\prime}_{a},\gamma^{\prime}_{a})\in
i_{u_{H}}^{a},\not\exists(\xi_{b},\gamma_{b},\upsilon_{b},\xi^{\prime}_{b},\gamma^{\prime}_{b})\in
i_{u_{H}}^{b}\ .\ $
$\displaystyle(\gamma_{a},\upsilon_{a},\gamma_{a}^{\prime})=(\gamma_{b},\upsilon_{b},\gamma_{b}^{\prime})\wedge\forall
k\geq-1\ .\ (\xi_{b}^{\prime}(k),\xi_{a}^{\prime}(k))\in\mathcal{Z}\\}\\}.$
(16)

where $i_{u_{H}}^{b}$ is defined as per (12) considering the relation
$\mathcal{Z}^{-1}\subseteq\mathcal{X}_{a}\times\mathcal{X}_{b}$. More
compactly, we write

$\mu_{x_{a}}(S_{b}\ {}^{H}{\preceq}_{A.S.}^{\mathcal{Z}}S_{a})<\epsilon,$

where ${}^{H}{\preceq}_{A.S.}^{\mathcal{Z}}$ highlights that the probabilistic
alternating simulation relation is referring to the relation $\mathcal{Z}$ and
it is relative to a time horizon $H$. $\square$

In words, expressions (13)-(14) describe and bound the probability of drawing
an initial condition $x_{a0}$ for which there exists an input sequence
$u_{H}$, _admissible for $S_{a}$_, generating at least one full $H$-behaviour
$(\xi_{a},\gamma_{a},u_{H},\xi^{\prime}_{a},\gamma^{\prime}_{a})$ that cannot
be related to any
$(\xi_{b},\gamma_{b},u_{H},\xi^{\prime}_{b},\gamma^{\prime}_{b})$ by
$\mathcal{R}$. Expressions (15)-(16) describe and bound the probability of
drawing an initial condition $x_{a0}$ for which there exists an input sequence
$u_{H}$, _admissible for $S_{b}$_, generating either at least one full
$H$-behaviour
$(\xi_{a},\gamma_{a},u_{H},\xi^{\prime}_{a},\gamma^{\prime}_{a})$ that can’t
be related to any
$(\xi_{b},\gamma_{b},u_{H},\xi^{\prime}_{b},\gamma^{\prime}_{b})$ by
$\mathcal{Z}$, or no full $H$-behaviour at all, if $u_{H}$ is inadmissible for
$S_{a}$. Note that the difference between (14) and (16) lies in what makes an
input sequence valid: in the first case, at every time step $k$ the input
$u_{H}(k)$ must belong to the set $U_{a}(\xi_{a}(k))$, hence
$i^{a}_{u_{H}}\neq\emptyset$, in the second case it belongs to
$U_{b}(\xi_{b}(k))$, hence $i^{b}_{u_{H}}\neq\emptyset$. Note that the
condition $i^{a}_{u_{H}}\neq\emptyset$ in (16) ensures that $\mathcal{Q}$
includes those initial conditions $x_{a0}$ for which there exists an input
sequence $u_{H}$ giving at least one full behaviour in $i^{b}_{u_{H}}$ but
none in $i^{a}_{u_{H}}$, meaning that $u_{H}$ is inadmissible for $S_{a}$
starting at $x_{a0}$.

It is easy to check that if for every choice of $H$ it holds that $\epsilon=0$
the definitions above subsume Definition 5 and Definition 6.

###  4.1 Constructing the data-driven abstraction

Consider the probability spaces $(\mathcal{X}_{0},\mathcal{G},\mu_{x})$ and
$(\mathcal{U}^{H},\mathcal{F},\mu_{u_{H}})$: when sampling the system
$S_{\Sigma}$ for $x\in\mathcal{X}_{0}$ and $u_{H}\in\mathcal{U}^{H}$ we assume
to have access only to the external $H$-behaviour of the system, that is
$\mathcal{B}_{H}(S_{\Sigma},x,u_{H})$: note that, by Assumption 1
(determinism), the latter is necessarily a singleton. In order to construct a
data-driven SA$\ell$CA of $S_{\Sigma}$, we draw $N$ pairs $(x^{i},u_{H}^{i})$
according to the product probability measure $\mu_{p}$ and we obtain the set
of sampled external behaviours

$D:=\\{\mathcal{B}_{H}(S_{\Sigma},x^{i},u_{H}^{i})\ :\ i=1,2,...N\\}.$ (17)

For $\ell<H$ we denote by $\hat{\Pi}_{\ell}$ the set of all witnessed
subsequences of length $\ell$, that is

$\hat{\Pi}_{\ell}:=\bigcup_{b_{H}\in
D}\bigcup_{k\in[0,H-1]}b_{H}|_{[k-\ell+1,k]}.$ (18)

From now on we use the symbol $\hat{\cdot}$ as shown above to denote the
quantities depending on the $N$ samples drawn according to $\mu_{p}$. We are
now ready to define the data-driven SA$\ell$CA.

######  Definition 10 (Data-driven SA$\ell$-CA)

Given $\hat{\Pi}_{\ell+1}$, the transition system
$\hat{S}_{\ell}=(\hat{\mathcal{X}}_{\ell},\hat{\mathcal{X}}_{\ell,0},\mathcal{U},\hat{\delta}_{\ell},\mathcal{Y},\mathcal{H}_{\ell})$
is called the data-driven (strongest asynchronous) $\ell$-complete abstraction
(SA$\ell$CA) of $S_{\Sigma}$, where the transition relation is given by

$\displaystyle\hat{\mathcal{X}}_{\ell}$ $\displaystyle:=\hat{\Pi}_{\ell}$
$\displaystyle\hat{\mathcal{X}}_{\ell,0}$
$\displaystyle:=\\{b_{\ell}\in\hat{\Pi}_{\ell}:\exists y\in\mathcal{Y}\ .\
b_{\ell}(\ell-1)=(\diamond,\diamond,y)\\}$ $\displaystyle\hat{\delta}_{\ell}$
$\displaystyle:=\\{(x_{\ell},u,x_{\ell}^{\prime})\ :\
x_{\ell}|_{[1,\ell-1]}=x_{\ell}^{\prime}|_{[0,\ell-2]}\wedge$ $\displaystyle
x_{\ell}^{\prime}(\ell-1)=(y,u,y^{\prime})\Rightarrow
x_{\ell}\cdot(y,u,y^{\prime})\in\hat{\Pi}_{\ell+1}\\}.$

Trivially, $\hat{\Pi}_{\ell+1}\subseteq\Pi_{\ell+1}$. In the following, we
show how to derive a probabilistic alternating simulation relation from
$\hat{S}_{\ell}$ to $S_{\Sigma}$ until horizon $H$ with probability not lower
than $1-\epsilon$ up to some confidence $\beta$.

###### Remark 3

Constructing the SA$\ell$CA using the set of sampled behaviours $D$ entails
solving a scenario program. Its complexity $s^{*}_{N}$ is the cardinality of
the smallest subset of $D$ (17) which would result in the construction of the
same set of all witnessed $(\ell+1)$-sequences $\hat{\Pi}_{\ell+1}$. One may
use Theorem 1 using an upper bound of $s^{*}_{N}$; a close estimate of its
value can be obtained using a greedy set cover algorithm. For practical
purposes, one may use the value $|\hat{\Pi}_{\ell+1}|$, resulting in a more
conservative estimate of $\epsilon$. $\square$

The following two lemmas are simple consequences of the definition above, and
their proof is omitted.

###### Lemma 1

Consider $S_{\Sigma}$, its data-driven SA$\ell$CA $\hat{S}_{\ell}$ constructed
from the set $\hat{\Pi}_{\ell+1}$ and the relation

$\hat{\mathcal{R}}:=\\{(x,x_{\ell})\in\mathcal{X}\times\hat{\mathcal{X}}_{\ell}:\
x_{\ell}\in\mathcal{E}_{\ell}(x)\\}.$ (19)

If $(x,x_{\ell})\in\hat{\mathcal{R}}$ and $(x,u,x^{\prime})\in\delta$ with
$\mathcal{H}(x^{\prime})=y$ then there exists a transition
$(x_{\ell},u,x_{\ell}^{\prime})\in\hat{\delta}_{\ell}$ with
$\mathcal{H}(x_{\ell}^{\prime})=y$ and
$(x^{\prime},x_{\ell}^{\prime})\in\hat{\mathcal{R}}$ if and only if
$x_{\ell}\cdot(u,y)\in\hat{\Pi}_{\ell+1}$. $\square$

Lemma 1 implies that, when using $\hat{\mathcal{R}}$, if a state trajectory of
the concrete system results in the same external behaviour of a state
trajectory of the SA$\ell$CA we know that at every time step the pair given by
the state of the former and the state of the latter belong to
$\hat{\mathcal{R}}$.

###### Lemma 2

Consider $S_{\Sigma}$, a confidence $\beta$ and the data-driven SA$\ell$CA
constructed from $\hat{\Pi}_{\ell+1}$. It holds that

$\displaystyle\quad\mu_{p}^{N}(\mu_{p}((x,u_{H})\in\mathcal{T}(\hat{S}_{\ell},H))<\epsilon)>1-\beta,$
(20)

where the violation set $\mathcal{T}(\hat{S}_{\ell},H)$ is defined

$\displaystyle\mathcal{T}(\hat{S}_{\ell},H):=\\{(x,u_{H}):\mathcal{B}_{H}(S_{\Sigma},x,u_{H})\notin\mathcal{B}_{H}(\hat{S}_{\ell})\\},$

where $\epsilon:=\epsilon(s^{*}_{N},\beta,N)$ as defined in Theorem 1.
$\square$

In practical terms, Lemma 2 provides an upper bound on the probability of
sampling a behaviour in the concrete system that does not belong to the set of
behaviours of the data-driven SA$\ell$CA. This concept is related to the
notion of _behavioural inclusion_ [29]: given two systems, if the set of all
behaviours of one system includes the set of all behaviours of the other, we
say that the first system behaviourally includes the second. If (20) holds,
according to [10], we say that $\hat{S}_{\ell}$ behaviourally includes
$S_{\Sigma}$ until horizon $H$ with probability greater or equal to
$1-\epsilon$.

Lemma 2 is a consequence of [8, Section V.C.], where the authors draw $N$
samples from a countable alphabet, determine which and how many unique symbols
were collected and bound the probability measure of the set of unseen symbols,
that is, those that were not among the $N$ samples. If $\ell+1=H$ the
construction of the data-driven SA$\ell$CA corresponds essentially to the
situation just described, where the alphabet is given by $\Gamma_{H}$. In
general, we construct a data-driven SA$\ell$CA using (18), i.e. we draw
samples belonging to $\Gamma^{\ell+1}$ which may arise in the first $H$ time
instants of the system’s time evolution.

Intuitively, reducing the size of the alphabet by reducing $\ell$ reduces the
complexity $s^{*}_{N}$, which in turn tightens the scenario bounds; on the
other hand, reducing $\ell$ also increases the number of behaviours that the
data-driven SA$\ell$CA can generate, leading to a coarser abstraction.

Let us consider the relation (19) between $S_{\Sigma}$ and $\hat{S}_{\ell}$;
we combine Lemma 1 with Lemma 2 to assign a probability measure to the pairs
$(x,u_{H})$ resulting in a full behaviour in the concrete system which cannot
be related by $\hat{\mathcal{R}}$ with a full behaviour in the abstract
system. This is formally stated in the following proposition.

###### Proposition 1

Consider $S_{\Sigma}$ , the product probability space
$(\mathcal{P},\mathcal{W},\mu_{p})$ obtained from
$(\mathcal{X},\mathcal{G},\mu_{x})$ and
$(\mathcal{U}^{H},\mathcal{F},\mu_{u_{H}})$ as defined in Section 2, and the
data-driven SA$\ell$CA $\hat{S}_{\ell}$ obtained from the set
$\hat{\Pi}_{\ell+1}$. Given a confidence parameter $\beta$, it holds that

$\mu_{p}^{N}(\mu_{p}((x,u_{H})\in\overline{\mathcal{V}}(\hat{S}_{\ell},\hat{\mathcal{R}},H))<\epsilon)>1-\beta$
(21)

where $\epsilon:=\epsilon(s^{*}_{N},\beta,N)$ as defined in (4), and

$\overline{\mathcal{V}}(\hat{S}_{\ell},\hat{\mathcal{R}},H):=\\{(x,u_{H}):\exists(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in
i_{u_{H}},\\\
\not\exists(\xi_{\ell},\gamma_{\ell},\upsilon_{\ell},\xi^{\prime}_{\ell},\gamma^{\prime}_{\ell})\in
i_{u_{H}}^{\ell}\ .\
(\gamma,\upsilon,\gamma^{\prime})=(\gamma_{\ell},\upsilon_{\ell},\gamma_{\ell}^{\prime})\wedge\\\
\forall k\geq-1\ .\
(\xi^{\prime}(k),\xi_{\ell}^{\prime}(k))\in\hat{\mathcal{R}}\\}$ (22)

######  Proof 4.2.

First, we show that the probability of drawing a pair $(x,u_{H})$ resulting in
an external $H$-behaviour not contained in the set of all external
$H$-behaviours of $\hat{S}_{\ell}$ is bounded by $\epsilon$ with confidence
$1-\beta$. Consider the random variable
$w_{x,u_{H}}:\mathcal{X}\times\mathcal{U}^{H}\rightarrow\Gamma_{H}$ defined as
$w_{x,u_{H}}:=\mathcal{B}_{H}(S,x,u_{H})$. From Lemma 2

$\mu_{p}^{N}(\mu_{p}((x,u_{H})\
:w_{x,u_{H}}\notin\mathcal{B}_{H}(\hat{S}_{\ell}))<\epsilon)>1-\beta.$

Now, consider
$\hat{\mathcal{R}}=\\{(x,x_{\ell})\in\hat{\mathcal{X}}_{\ell}\times\mathcal{X}:\
x_{\ell}\in\mathcal{E}_{\ell}(x)\\}$. Suppose that
$(x,u_{H})\in\overline{\mathcal{V}}(\hat{S}_{\ell},\hat{\mathcal{R}},H)$111We
use Lemma 1 to show that if a trajectory in the abstract system is relatable
through $\hat{\mathcal{R}}$ to another trajectory in the concrete system, it
automatically implies that the external behaviour of the two matches: by Lemma
1, this implies that

$w_{x,u_{H}}\notin\mathcal{B}_{H}(\hat{S}_{\ell}).$

Since the negation of the latter holds with probability greater than
$1-\epsilon$ then the negation of the former holds with at least the same
probability, up to a confidence of at least $1-\beta$.

The difference between the sets
$\overline{\mathcal{V}}(\hat{S}_{\ell},\hat{\mathcal{R}},H)$ and
$\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H)$, as defined in (14)
(considering $S_{b}=\hat{S}_{\ell}$) is subtle but important. The first one
encompasses the _pairs_ $(x,u_{H})$ which would result in an external
behaviour of the concrete system that does not exist in the data-driven
SA$\ell$CA. The second one encompasses the _states_ $x$ for which there
_exists_ an input sequence $u_{H}$ which would cause the display of an
external behaviour in the concrete system that does not exist in the data-
driven SA$\ell$CA. For the guarantees provided by Proposition 1 to hold,
however, we are forced to draw the pairs $(x,u_{H})$ according to the product
measure $\mu_{p}$: this means that not only the initial condition $x$ must be
drawn randomly, but also the input sequence $u_{H}$. Since we are interested
in generating an abstraction suitable for control we need to be able to select
the inputs arbitrarily once we have constructed the data-driven SA$\ell$CA,
rather than constricted by the probability distribution $\mu_{u_{H}}$. In
practice, once we construct the data-driven SA$\ell$CA we are interested in
designing a controller, possibly deterministic. To this end, we expand the
result of Proposition 1 to encompass control sequences chosen arbitrarily.

######  Proposition 4.3.

Consider $S_{\Sigma}$, the product probability space
$(\mathcal{P},\mathcal{W},\mu_{p})$ obtained from
$(\mathcal{X},\mathcal{G},\mu_{x})$ and
$(\mathcal{U}^{H},\mathcal{F},\mu_{u_{H}})$, and the data-driven SA$\ell$CA
$\hat{S}_{\ell}$ obtained from the set $\hat{\Pi}_{\ell+1}$. If $\mu_{u_{H}}$
is the uniform probability measure, given a confidence parameter $\beta$ with
$\overline{\epsilon}=\epsilon|\mathcal{U}^{H}|$ it holds that

$\mu_{p}^{N}(\mu_{x}(S_{\Sigma}\
{}^{H}{\preceq}_{S.}^{\hat{\mathcal{R}}}\hat{S}_{\ell})<\overline{\epsilon})>1-\beta.$
(23)

######  Proof 4.4.

For brevity, let us denote by $\mathcal{V}$ and $\overline{\mathcal{V}}$ the
sets $\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H)$, defined according to
$\eqref{eq:sim-vio-set}$, and
$\overline{\mathcal{V}}(\hat{S}_{\ell},\hat{\mathcal{R}},H)$, defined as in
(22). In Proposition 1 we have shown that
$\mu_{p}^{N}(\mu_{p}((x,u_{H})\in\overline{\mathcal{V}})<\epsilon)>1-\beta.$
We define the set
$J(x):=\\{u_{H}\in\mathcal{U}^{H}:(x,u_{H})\in\overline{\mathcal{V}}\\}.$ Let
$b$, $c$, and $z$ be the densities of $\mu_{p}$, $\mu_{x}$, and $\mu_{u_{H}}$
respectively. Then,

$\displaystyle\mu_{p}$
$\displaystyle((x,u_{H})\in\overline{\mathcal{V}})=\int_{\overline{\mathcal{V}}}b(x,u_{H})dxdu_{H}$
(24)
$\displaystyle=\int_{\mathcal{V}}c(x)\int_{J(x)}z(u_{H})du_{H}dx=\int_{\mathcal{V}}c(x)\frac{|J(x)|}{|\mathcal{U}^{H}|}dx$
(25)
$\displaystyle\geq\frac{1}{|\mathcal{U}^{H}|}\int_{\mathcal{V}}c(x)dx=\frac{1}{|\mathcal{U}^{H}|}\mu_{x}(x\in\mathcal{V}),$
(26)

from which follows the thesis

$\mu_{x}(x\in\mathcal{V})<\epsilon|\mathcal{U}^{H}|,$

holding with a probability of at least $1-\beta$.

Proposition 4.3 states that the probability of drawing an initial condition in
the concrete system in $\mathcal{V}$, that is, such that there _exists_ an
input $u_{H}$ which would generate an external behaviour that can not be
related by $\hat{\mathcal{R}}$ to an external behaviour of the SA$\ell$CA, is
bounded by a probability proportional to the cardinality of the input sequence
set, up to a given confidence. In other words, once we have sampled $N$
independent $H$-long external behaviours according to
$\mu_{p}=\mu_{x}\times\mu_{u_{H}}$ to construct $\hat{S}_{\ell}$, Proposition
4.3 establishes a probabilistic simulation relation from the concrete system
to the abstraction, up to some confidence. If the initial condition $x$ does
not belong to $\mathcal{V}$, any arbitrary input sequence $u_{H}$ will
generate an external behaviour that exists in the (data-driven) SA$\ell$CA;
hence, once we have constructed the abstraction, we are free to pick control
actions arbitrarily, not according to the uniform distribution $\mu_{u_{H}}$,
while knowing that the probability of drawing an initial condition $x$ in
$\mathcal{V}$ is bounded by $\epsilon|\mathcal{U}|^{H}$. This property will be
instrumental in the next step, as we will show that we can pick control
actions using the SA$\ell$CA itself once we establish a probabilistic
alternating simulation relation from the SA$\ell$CA to the concrete system.

######  Remark 4.5.

To derive Proposition 4.3 we laid the assumption that $\mu_{u_{H}}$ is the
uniform probability measure. The same reasoning carries through for different
measures, as long as we know the smallest non-zero probability assigned to an
element of $\mathcal{U}^{H}$. However, if $\mu_{u_{H}}$ can be chosen
arbitrarily, the bound obtained from equations (25)-(26) is the tightest for
the uniform probability measure. $\square$

Next, we claim that $\hat{\mathcal{Z}}:=(\hat{\mathcal{R}})^{-1}$ defines a
probabilistic alternating simulation relation.

######  Corollary 4.6.

Under the assumptions of Proposition 4.3, $\hat{\mathcal{Z}}$ defines a
probabilistic alternating simulation relation from $\hat{S}_{\ell}$ to
$S_{\Sigma}$ with respect to $\mathcal{U}\times\mathcal{Y}$ until horizon $H$
with probability not less than $1-\overline{\epsilon}$, with
$\overline{\epsilon}=\epsilon|\mathcal{U}^{H}|$, with confidence greater than
$1-\beta$, that is

$\mu_{p}^{N}(\mu_{x}(\hat{S}_{\ell}\
{}^{H}{\preceq}_{A.S.}^{\hat{\mathcal{Z}}}S_{\Sigma})<\overline{\epsilon})>1-\beta.$
(27)

######  Proof 4.7.

From Proposition 4.3 we know with confidence $1-\beta$ that
$\mu_{x}(x\in\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H))<\epsilon|\mathcal{U}|^{H}$.
Hence, it is sufficient to show that
$\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H)\supseteq\mathcal{Q}(\hat{S}_{\ell},\hat{\mathcal{Z}},H)$.
Suppose that $x\in\mathcal{Q}(\hat{S}_{\ell},\hat{\mathcal{Z}},H)$: since
$S_{\Sigma}$ has free input, any $u_{H}$ satisfying the first line of (16) is
an admissible sequence of inputs for $S_{\Sigma}$, hence
$i_{u_{H}}\neq\emptyset$, which implies that
$x\in\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H)$.

Once the we have established the probabilistic alternating simulation relation
between the data-driven SA$\ell$CA and the concrete system, we can adopt
classical synthesis methods to design a controller enforcing a desired
specification, see e.g. [29].

##  5 Beyond The Sampling Horizon

Let us further elaborate the implications of
$\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H)\neq\emptyset$. Recall that
$\hat{\mathcal{R}}\subseteq\mathcal{X}\times\hat{\mathcal{X}}_{\ell}\subseteq\mathcal{X}\times\mathcal{X}_{\ell}$.
If $\hat{\Pi}_{\ell+1}=\Pi_{\ell+1}$ then, as stated in Section 3.2, it holds
that $\hat{\mathcal{X}}_{\ell}=\mathcal{X}_{\ell}$,
$\hat{\mathcal{R}}=\mathcal{R}$ and $\mathcal{V}=\emptyset$, since the data-
driven SA$\ell$CA coincides with the (complete) SA$\ell$CA. The converse also
holds. We can alternatively express the set $\mathcal{V}$ in terms of the
union of the equivalence classes of the _missing_ $\ell+1$-sequences, i.e.
those belonging to the set difference given by
$\Pi_{\ell+1}\setminus\hat{\Pi}_{\ell+1}$

$\displaystyle\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H)=\\{x_{0}\in\mathcal{X}:\exists
u_{H}\in\mathcal{U}^{H},\exists(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in$
$\displaystyle\qquad\qquad\qquad\mathcal{I}_{H}(S,x,u_{H}),\exists k\geq-1\ .\
\xi^{\prime}(k)\in\mathcal{K}\\},$ (28)
$\displaystyle\qquad\qquad\mathcal{K}:=\bigcup_{w_{\ell+1}\in\Pi_{\ell+1}\setminus\hat{\Pi}_{\ell+1}}[w_{\ell+1}].$
(29)

So far we have argued that the probability measure assigned by $\mu_{x}$ to
the set of initial conditions visiting an equivalence class $[w_{\ell+1}]$
_within_ time $H$ not acquired during the sampling, i.e.
$[w_{\ell+1}]\notin\hat{\Pi}_{\ell+1}$, is bounded by
$\epsilon|\mathcal{U}^{H}|$. Let us now consider the probability measure of
the set of initial conditions visiting an equivalence class
$[w_{\ell+1}]\notin\hat{\Pi}_{\ell+1}$ _within time_ $H^{\prime}$, with
$H^{\prime}>H$. In order to answer this we analyze the change in measure of a
set under the time-reversed dynamics of the system. To this end, we enunciate
the following lemma, proved in the Appendix A.1.

######  Lemma 5.8.

Given a compact set $\mathcal{X}\subset\mathbb{R}^{n}$, the $p$-norm
$||\cdot||_{p}:\mathcal{X}\rightarrow\mathbb{R}$, and a function
$g:\mathcal{X}\rightarrow\mathcal{X}$ such that $||g(x)-g(y)||_{p}\leq
L||x-y||_{p}$, if for constants $c,q>0$ it holds that
$q^{-1}||x-y||_{p}\leq||x-y||_{2}\leq c||x-y||_{p}$ for all
$x,y\in\mathcal{X}$, then for any Riemann integrable set
$\Sigma\subseteq\mathcal{X}$ it holds that
$\int_{g(\Sigma)}dV\leq(cLq)^{n}\int_{\Sigma}dV$.

###### Assumption 2

The function $f$ defined in (1) satisfies $\eqref{eq:Lipschitz-inv}$, where
the distance is induced by the $p$-norm on $\mathcal{X}$.

######  Proposition 5.9.

Let $\mu_{x}$ and $\mu_{u_{H}}$ be the uniform probability measures on
$(\mathcal{X},\mathcal{G})$ and $(\mathcal{U}^{H},\mathcal{F})$ respectively.
Consider $S_{\Sigma}$ with $\Sigma$ satisfying Assumption 2, and the data-
driven SA$\ell$CA $\hat{S}_{\ell}$ obtained from $\hat{\Pi}_{\ell+1}$. For any
positive integer $T$ it holds that

$\mu_{x}(S_{\Sigma}\
{}^{T+H}{\preceq}_{S.}^{\hat{\mathcal{R}}}\hat{S}_{\ell})\leq\nu\mu_{x}(S_{\Sigma}\
{}^{H}{\preceq}_{S.}^{\hat{\mathcal{R}}}\hat{S}_{\ell})$ (30)

where

$\nu:=\left(1+\lambda^{T}\sum_{i=0}^{\tau-1}\lambda^{-i(H+1)}\right),$
$\tau=\lceil(H+T+1)/(H+1)\rceil-1,$
$\lambda=|\mathcal{U}|\left(\frac{cq}{m_{X}}\right)^{n},$

and $c$, $q$ and $m_{X}^{-1}=L$ are defined as in Lemma 5.8.

Proposition 5.9, proved in Appendix A.2, relates the probability of drawing an
initial condition such that there exists a sequence of inputs that will
produce a new behaviour, i.e. not present in $\hat{S}_{\ell}$, within the time
horizon $H$ selected to construct the data-driven SA$\ell$CA, with the
probability of that happening over a horizon _larger_ than $H$. Note that
Assumption 2 is not tied to a notion of stability of $\Sigma$ and it is
satisfied by a broad set of nonlinear stable/unstable systems.

###  5.1 Contracting Systems

For the class of contracting systems, it is possible to show that there exists
a time $H$ after which they always produce the same output.

###### Assumption 3

The map $f$ of the dynamical system $\Sigma$ described in (1), is uniformly
contracting w.r.t. $x$ with constant $l_{X}$, uniformly Lipschitz w.r.t. $u$
with constant $l_{U}$, as per Definition 2, and there exist
$x^{*}\in\mathcal{X}$ and $u^{*}\in\mathbb{R}^{n_{u}}$ s.t.
$f(x^{*},u^{*})=x^{*}$. $\square$

For instance, contractive control-affine systems [26] satisfy Assumption 3
($f(x,u)$ depends linearly on $u$ for a fixed $x$).

######  Lemma 5.10.

Suppose that $f$ is uniformly contracting w.r.t. $x$ with constant $l_{X}$ and
uniformly Lipschitz w.r.t. $u$ with constant $l_{U}$. Then

$d(x_{k},y_{k})\leq l_{X}^{k}d(x_{0},y_{0})+\frac{l_{U}}{1-l_{X}}\max_{0\leq
i<k}\\{d(u_{i},v_{i})\\}$ (31)

where $x_{i+1}=f(x_{i},u_{i})$ and $y_{i+1}=f(y_{i},v_{i})$ for $i\in[0,k-1]$.

######  Corollary 5.11.

If $f$ satisfies Assumption 3, then

$d(x_{k},x^{*})\leq l_{X}^{k}d(x_{0},x^{*})+\frac{l_{U}}{1-l_{X}}\max_{0\leq
i<k}\\{d(u_{i},u^{*})\\},$ (32)

where $x_{i+1}=f(x_{i},u_{i})$.

######  Proposition 5.12.

Consider a dynamical system $\Sigma$ satisfying Assumption 3, its embedding to
a TS $S_{\Sigma}$, and the data-driven SA$\ell$CA $\hat{S}_{\ell}$ obtained
from $\hat{\Pi}_{\ell+1}$. If there exist a $y\in\mathcal{Y}$ and $r>\rho$
s.t. for all $x\in B(x^{*},r)$ it holds that $h(x_{k})=y^{*}$ then for any
$H\geq\overline{k}$ it holds that

$\mu_{x}(S\ {}^{H}{\preceq}_{S.}^{\hat{\mathcal{R}}}\hat{S}_{\ell})=\mu_{x}(S\
{}^{\overline{k}}{\preceq}_{S.}^{\hat{\mathcal{R}}}\hat{S}_{\ell})$ (33)

where

$\overline{k}=\lceil\log_{l_{X}}\left(r-\rho\right)-\log_{l_{X}}\theta\rceil$
$\theta=\sup_{x\in\mathcal{D}}d(x,x^{*})\qquad\rho=\frac{l_{U}}{1-l_{X}}\sup_{u\in\mathcal{U}}d(u,0).$

######  Proof 5.13.

After $\overline{k}$ time steps the distance of any trajectory’s state $x_{k}$
from $x^{*}$ is smaller than $r$, by Corollary 5.11 we know that $x_{i}$ will
remain within that distance for all $u\in\mathcal{U}$. Moreover, by assumption
of the proposition we have $h(x_{k})=y^{*}$ for all such $x$’s. Thus, the next
input-output pairs are $(u,y^{*})$ for all $u\in\mathcal{U}$. Note that, if
one wants to have a non-blocking data-driven SA$\ell$CA obtained from a set of
external behaviours
$D:=\\{\mathcal{B}_{\overline{k}}(S_{\Sigma},x^{i},u_{\overline{k}}^{i})\ :\
i=1,2,...N\\}$ it may be necessary to artificially extend the external
behaviours according to the result of this proposition. That is, construct the
data-driven SA$\ell$CA from $\hat{\Pi}_{\ell}$ obtained as (18) using the set
of (extended) behaviours

$\widetilde{D}:=\\{b_{\overline{k}}\cdot b_{\ell}:b_{\overline{k}}\in D\wedge
b_{\ell}\in(\\{y^{*}\\}\times\mathcal{U}\times\\{y^{*}\\})^{\ell}\\}.$

instead of $D$.

The proposition assures that, if there exists a sufficiently large ball around
the fixed point of $f$, where all points have the same output, then by
contractivity of the flow $f$ we can compute the time instant in which all
trajectories enter the ball. Hence, if an initial condition does not belong to
the violation set defined in the right-hand side of (33), then neither will it
belong to the violation set defined in the left-hand side. Note that if
$\Sigma$ satisfies Assumption 2 and 3 then the map $f$ is a (contracting)
_lipeomorphism_ , sometimes also referred to as bi-Lipschitz.

###  5.2 Autonomous Systems

In [10] the authors provide a framework for the construction of the data-
driven SA$\ell$CA of an autonomous system, which, for example, can be utilized
for verifying whether a linear temporal logic formula holds, where the
guarantees derive from the scenario optimization. Obviously, (1) is autonomous
if it can be rewritten as $u_{k}:=u(x)$ where $u$ is some state feedback law.
This is equivalent to having a dynamical system where $|\mathcal{U}|=1$. In
this special case, through Proposition 1 we obtain a guarantee that
$\hat{\mathcal{R}}$ is a probabilistic simulation relation from $S_{\Sigma}$
to $\hat{S}_{\ell}$ with respect to $\mathcal{U}\times\mathcal{Y}$ until
horizon $H$ with probability not less than $1-\epsilon=1-\overline{\epsilon}$
(with confidence $\beta$). By Lemma 2 we know that this implies that
$\hat{S}_{\ell}$ behaviourally includes $S_{\Sigma}$ until horizon $H$ with
the same probability, as defined in [10, Definition 4]. In summary, we recover
the same guarantees provided by [10, Proposition 2].

##  6 Experimental Evaluation

### A Linear System

Let us consider the linear system $x_{k+1}=Ax_{k}+Bu_{k}$ characterised by
matrices

$A=\frac{1}{4}\begin{bmatrix}1&2\\\ -1.8&1\end{bmatrix},\quad
B=\begin{bmatrix}0\\\ 1\end{bmatrix}.$ (34)

The input space is composed of 3 possible input signals, i.e.
$\mathcal{U}=\\{-0.3,0,0.3\\}$, whilst the state space
$\mathcal{D}=[-3,3]^{2}$ is partitioned into 9 regions by a uniform grid, each
uniquely labeled, implicitly defining the output set $\mathcal{Y}$.

We sample $N=2\cdot 10^{6}$ initial conditions $(x_{0},u_{H})$ from the
uniform distribution, with $H=4$ and $\ell=2$. The sampling process returns
$\hat{\Pi}_{\ell+1}$, containing 342 sequences, and we construct the
corresponding abstraction. Setting $\beta=10^{-6}$, we compute the scenario
bounds according to Proposition 1,

$\epsilon(s^{*},\beta,N)=1.51\cdot 10^{-4}$

To verify these bounds empirically, we sample in addition $M=10^{6}$ initial
conditions and get an empirical violation probability $\hat{V}=0$.
Additionally, by Corollary 4.6, with confidence at least $1-\beta$,
$\hat{\mathcal{Z}}$ defines a probabilistic alternating simulation relation
from the abstraction to the concrete system with respect to
$\mathcal{U}\times\mathcal{Y}$ until horizon $H$ with probability not less
than $1-\overline{\epsilon}$, where
$\overline{\epsilon}:=\epsilon(s^{*},\beta,N)|\mathcal{U}^{H}|=1.23\cdot
10^{-2}$. These results are summarised in Table 1.

In order to extend the guarantees from horizon $H=4$ to any finite horizon we
employ Proposition 5.12. We use parameters $l_{X}\simeq 0.56$, $\theta\simeq
4.24$, $l_{U}=1$, $\rho\simeq 0.68$, $r=1$, which give $\overline{k}=5$.
Hence, we construct a new abstraction after collecting $N=10^{6}$ trajectories
with horizon $H^{\prime}=5$. In line with the discussion in Section 5, we
conclude that $\hat{\mathcal{Z}}$ defines a probabilistic alternating
simulation relation from the abstraction to the concrete system until horizon
$H^{\prime}$, and hence any horizon, with probability not less than
$1-\overline{\epsilon}^{\prime}$, where
$\overline{\epsilon}^{\prime}=6.18\cdot 10^{-2}$, and confidence $1-\beta$.
Instead of resampling, alternatively, we could have leveraged Proposition 5.9
and used the abstraction constructed with the trajectories of length $H=4$; we
can extend the guarantee of probabilistic alternating simulation relation from
the abstraction to the concrete system until horizon $H$ with probability not
less than $1-\overline{\epsilon}=1-1.23\cdot 10^{-2}$ to horizon $H^{\prime}$
with probability not less than $1-\nu\overline{\epsilon}=1-1.41\cdot 10^{-1}$,
where we have used (30) with $T=1$ to compute the correcting factor
$\nu=11.4$. We can observe that Proposition 5.12 provides tighter bounds using
half of the samples compared to Proposition 5.9.

Benchmark | $N$ | $H$ | $\ell$ | $\hat{\Pi}_{\ell+1}$ | $s^{*}_{N}$ | $\epsilon$ | $\overline{\epsilon}$ | $\hat{V}$
---|---|---|---|---|---|---|---|---
Linear | $2\cdot 10^{6}$ | 3 | 2 | 342 | 169 | $1.51\cdot 10^{-4}$ | $1.23\cdot 10^{-2}$ | 0
SIR | $10^{6}$ | 6 | 2 | 7593 | 2726 | $3.04\cdot 10^{-3}$ | $1.95\cdot 10^{-1}$ | $1.1\cdot 10^{-4}$
Car | $10^{6}$ | 5 | 3 | 1611 | 984 | $1.18\cdot 10^{-3}$ | $3.77\cdot 10^{-2}$ | $1.40\cdot 10^{-4}$
TCL | $10^{4}$ | 50 | 5 | 273 | 44 | $9.18\cdot 10^{-3}$ | – | 0
Table 1: For each benchmark, we sample $N$ trajectories of length $H$ and
split them into $\ell$-sequences. We report the total number of sequences and
the corresponding scenario complexity $s^{*}_{N}$. Considering
$\beta=10^{-6}$, we compute the $\epsilon$ bound as per Theorem 1, and finally
get the bound for the alternating simulation relation $\bar{\epsilon}$ as per
Proposition 4.3. Finally, we perform a second sampling and compute the
empirical violation $\hat{V}$, which lies always below the probability bounds.

### Infectious Diseases Model

The SIR model of infectious diseases considers a population that can be
divided into Susceptible (S), Infected (I), and Recovered (R). The portion of
each class at time $t$ is denoted by $x_{1}(t)$, $x_{2}(t)$ and
$x_{3}(t)=1-x_{1}(t)-x_{2}(t)$, respectively. The model postulates that each
infected individual is in contact with an average number of $\lambda$ a given
number of individuals per unit time, and that infects only those who are
susceptible ($S\to I$ transition), generating new infections at an average
rate $\lambda x(t)$. Each infected individual recovers at a rate $\eta$ ($I\to
R$ transition). The recovered population is assumed to no longer infect others
and cannot be reinfected. Finally, we denote the basic reproduction number
$\sigma$ by $\sigma=\lambda/\eta$. Let us assume that $\sigma$ is our control
variable, and thus can be varied over time, i.e.
$\sigma\in\\{\sigma_{s},\sigma_{n}\\}$, corresponding to a strict, and no
quarantine measures, respectively. In practical terms, $\sigma(t)$ captures
measures such as social distancing, and the lockdown of businesses and
institutions. Formally, the model [15] can be written as:

$\begin{cases}\dot{x}_{1}(t)=-\eta\cdot\sigma\cdot x_{1}(t)\cdot x_{2}(t),\\\
\dot{x}_{2}(t)=\eta\cdot\sigma\cdot x_{1}(t)\cdot x_{2}(t)-\eta\cdot
x_{2}(t),\end{cases}$ (35)

where $\eta=0.1$ is the recovery rate, $\sigma_{s}=0.3$, and $\sigma_{n}=2.2$.
The state space is defined $\mathcal{D}=[0,1]^{2}$ and is partitioned into 400
regions. The system is translated into discrete time via the Euler method,
with $\tau=0.1$. Further, we use a zero-order hold control input over $T=15$
time steps, and we observe the system’s output accordingly every $T$ steps.
This follows a real-life rationale, where quarantine policies should not be
changed too frequently.

We sample $N=10^{6}$ pairs of initial conditions and input sequences from the
uniform distribution, we collect trajectories of length $H=6$ and set
$\ell=2$. We obtain the set $\hat{\Pi}_{\ell+1}$, containing $7593$ sequences,
a complexity $s^{*}_{N}=2726$, and we construct the corresponding abstraction.
Setting $\beta=10^{-6}$, Proposition 1 returns a bound on the violation
probability for a randomly extracted pair of initial condition and input
sequence of

$\epsilon:=\epsilon(s^{*},\beta,N)=3.04\cdot 10^{-3}.$ (36)

Again, to verify these bounds empirically, we sample additionally $M=10^{5}$
initial conditions, getting an empirical violation $\hat{V}=1.10\cdot
10^{-4}$, well below the scenario bounds. Next, by Proposition 4.3 and
Corollary 4.6 we can establish a probabilistic alternating simulation relation
from the abstraction to the concrete system until horizon $H$ with probability
not less than $1-\overline{\epsilon}$ where,

$\overline{\epsilon}:=\epsilon|\mathcal{U}|^{H}=1.95\cdot 10^{-1}.$ (37)

Controller Synthesis for Reachability Specification.  We use the resulting
abstraction to compute a policy. Let us consider an initial state where the
population is divided into 10% infected, 87% susceptible, and a target state
of 80% susceptible and 10% infected. Further, we give each state and each
control action a weight: states have a score equal to the sum of the portion
of infected and susceptible population; control actions have a score of 0 for
$\sigma_{n}$, and 1 for $\sigma_{s}$. By solving the reachability game on the
abstraction (see [29] for a detailed description), we find the optimal policy
for the given abstraction, which corresponds to a strategy that applies a
strict quarantine, leading to the target state in 45 steps.

### Mountain Car

We consider the mountain car benchmark, originally outlined in [21], as it is
presented in the Gymnasium library [1]. The mountain car is a deterministic
model consisting of a car with two actions, representing a fixed positive or
negative acceleration along the $x$ axis, with the goal of reaching the top of
the hill. The goal of the car is to reach the top of the hill, located on the
right of the domain. The variables are the position and the velocity of the
car, whilst the state space domain is
$\mathcal{D}=[-1.2,0.6]\times[-0.07,0.07]$, partitioned into 4 regions,
corresponding to the position within [-1.2, -0.5], (-0.5, 0.], (0, 0.5), and
[0.5, 0.6], labeled $R_{1}$, $R_{2}$, $R_{3}$ and $G$ respectively; the
initial velocity can be any value in the admissible domain. To prevent the car
from switching too often between accelerating to the left and to the right we
impose a zero-order hold control input over $T=50$ time steps, and observe the
system’s output accordingly every $T$ steps. We sample $N=10^{6}$ initial
conditions from the entire domain $\mathcal{D}$ and create a SA$\ell$CA; we
report the probability bounds, the empirical violation (over $10^{5}$
samples), along with the other simulation parameters, in Table 1.

We sample $N=10^{6}$ pairs of initial conditions and input sequences from a
uniform distribution, we collect trajectories of length $H=5$ and set
$\ell=3$. We obtain the set $\hat{\Pi}_{\ell+1}$, containing $1611$ sequences,
and a complexity of $s^{*}_{N}=984$. Proposition 1 returns a bound on the
violation probability for a randomly extracted pair of initial conditions and
input sequences of

$\epsilon:=\epsilon(s^{*},\beta,N)=1.18\cdot 10^{-3}$ (38)

We then sample additional $M=10^{5}$ trajectories, in order to empirically
verify the scenario guarantees with different initial conditions, and obtain
an empirical violation of $\hat{V}=1.40\cdot 10^{-4}$. By Proposition 4.3 and
Corollary 4.6, with confidence at least $1-\beta=1-10^{-6}$, we can establish
a probabilistic alternating simulation relation from the abstraction to the
concrete system until horizon $H$ with probability not less than
$1-\overline{\epsilon}$ where,

$\overline{\epsilon}:=\epsilon|\mathcal{U}|^{H}=3.77\cdot 10^{-2}.$ (39)

Controller Synthesis for Reach Specification and Refinement.  Let us
synthesize a controller to push the car uphill, to the [0.5,0.6] interval. We
frame this as a reachability game on the data-driven abstraction [29]. we
define as goal states all the $\ell$-sequences where the last symbol is $G$,
i.e. the car is in the goal set. The solution of the reachability game returns
a set of abstract states and actions that are guaranteed to drive the car to
the goal set222By limiting the number of iterations of the reachability
algorithm to $H$, we ensure that every state included in the solution reaches
the goal set in no more than $H$ actions., modulo the correctness of the
abstraction. We observe that among the returned states, there are all four
$\ell$-sequences of the form
$((\diamond,\diamond,\diamond),\ldots,(\diamond,\diamond,y))$, where $y$ is
$R_{1}$, $R_{2}$, $R_{3}$ or $G$. We conclude that we can refine the
controller to drive the car to the goal set from every initial state, as long
as no new behaviours are observed. We are now interested in providing a
guarantee for the reach specification for the closed-loop system. We then use
the newly found policy, and sample $N=10^{6}$ new initial conditions uniformly
on the closed-loop model. We obtain an empirical violation
$\hat{V}^{\prime}=0$, i.e. no new behaviours are sampled and all reach the
goal set. As explained in Section 5.2 we can use these new trajectories to
construct a new data-driven SA$\ell$CA (with the same $\ell$) for the closed-
loop concrete system. By Lemma 2, the probability of drawing an initial
condition that, under the synthesised controller, generates a new behaviour
not contained in the data-driven SA$\ell$CA (and hence fails to reach the
target set) is smaller than $\epsilon=1.02\cdot 10^{-4}$, with confidence of
at least $1-10^{-6}$.

### Thermostatically Controlled Load

Figure 3: Example of 100 TCL trajectories, all remaining within the domain
[19.25, 20.75].

Let us consider a thermostatically controlled load benchmark, as outlined in
[17]. Let us describe a deterministic version of a room temperature evolution
model, as

$\theta_{k+1}=a\cdot\theta_{k}+(1-a)\cdot(\theta_{amb}-m_{k}\cdot T_{r}\cdot
P),$ (40)

where $a$ is the TCL thermal characteristic, $\theta$ represent the
temperature of the room at time $k$, $\theta_{amb}$ is the external
temperature, $m$ is a binary variable indicating the status of the TCL (ON or
OFF), $T_{r}$ is the thermal resistance, and $P$ is the TCL’s rated power. The
temperature setpoint is $20^{\circ}$ Celsius, and the binary controller $m$
acts according to an hysteresis law with dead-band width of $0.5^{\circ}C$.
The state space is $\mathcal{D}=[19.25,20.75]$, partitioned uniformly into 20
regions. An example of 100 trajectories is presented in Fig. 3. We construct
the SA$\ell$CA by sampling $N=10^{4}$ trajectories of length $H=50$ and set
$\ell=5$. We summarise the results of the benchmark in Table 1, also reported
here for completeness. We obtain the set $\hat{\Pi}_{\ell+1}$, containing
$273$ sequences, resulting in a complexity $s^{*}_{N}=44$. By setting
$\beta=10^{-6}$ we obtain a probabilistic bound

$\epsilon(s^{*},N,\beta)=9.18\cdot 10^{-3}.$ (41)

Note that, as highlighted in Section 5.2, since this is an autonomous system,
we conclude that the abstraction behaviourally includes the concrete system
until horizon $H$ with probability not less than $1-\epsilon$. Using the
abstraction we verify that the system satisfies the safety property, i.e. the
temperature never exits the range $[19.25,20.75]$, with the aforementioned
probability bounds. The bounds are empirically checked, by sampling additional
$10^{4}$ initial conditions, getting 0 new behaviours, suggesting both that
the prediction intervals are correct and that the abstraction is indeed a
valid model representation for the underlying system.

##  7 Discussion and Concluding Remarks

We have proposed a fully data-driven framework to construct an abstraction
suitable for controlling a discrete-time deterministic control system, by
introducing the notion of probabilistic alternating simulation. The data-
driven SA$\ell$CA does not require any reachability analysis, which is
typically considered a bottleneck for model-based abstractions. Since the
data-driven SA$\ell$CA is constructed from sampled behaviours the number of
transitions in the abstraction $\hat{\Pi}_{\ell+1}$, and hence the number of
states, will automatically adjust based on the dynamics of the system.
Moreover, $\ell$ is a tuneable parameter and can be increased or decreased to
return a more or less refined abstraction respectively, see [10]. Importantly,
the resulting abstraction is independent of the control objective, that is,
one can use the same abstraction to synthesize controllers solving different
problems, without the need to resample and reconstruct the abstraction when
the design objective is changed.

On the other hand, we can observe that the scenario bounds derived in the
examples according to Proposition 1, which in turn is a direct application of
Theorem 1, when compared to the empirical violation, can be conservative by an
order of magnitude. This is because effectively we draw samples from a
discrete event space $\Gamma_{H}$ (the $H$-long behaviours), making the
construction of the abstraction a so-called degenerate problem, as mentioned
in Remark 1. Note that Equations (24)-(25) are not conservative since the
inequality is an equality if every violating initial condition has _exactly_
one input sequence out of the possible $|\mathcal{U}^{H}|$ which produce an
unregistered behaviour. However, this event is highly unlikely; hence, when
closing the loop in the mountain car example we observe a considerably smaller
empirical violation (no violations over $10^{6}$ new samples) compared to the
guaranteed upper bound $\overline{\epsilon}$.

In conclusion, for a fixed number of samples, if the control objective is
known and fixed, synthesizing a controller with a technique suitable for
black-box models as reinforcement learning, and successively verifying the
design might result in tighter bounds, since, as argued Section 5.2 and
experimentally observed in the Mountain Car example, for the closed-loop
system the correcting factor of $|\mathcal{U}^{H}|$ equals 1.

We further prove that we can provide guarantees for a horizon larger than the
sampling one, under additional conditions on the concrete model. Future work
includes the construction of abstractions for systems with noise.

## References

## References

  * [1] Mountaimn car environment.  https://gymnasium.farama.org/environments/classic_control/mountain_car/.  Accessed: 2023-09-30.
  * [2] P. Akella and A. D. Ames.  A barrier-based scenario approach to verifying safety-critical systems.  IEEE Robotics and Automation Letters, 7(4):11062–11069, 2022.
  * [3] T. Badings, L. Romao, A. Abate, D. Parker, H. A. Poonawala, M. Stoelinga, and N. Jansen.  Robust control for dynamical systems with non-gaussian noise via formal abstractions.  Journal of Artificial Intelligence Research, 76:341–391, 2023.
  * [4] C. Baier and J.-P. Katoen.  Principles of model checking.  MIT press, 2008.
  * [5] A. Banse, L. Romao, A. Abate, and R. Jungers.  Data-driven memory-dependent abstractions of dynamical systems.  In Learning for Dynamics and Control Conference, pages 891–902. PMLR, 2023.
  * [6] A. Banse, L. Romao, A. Abate, and R. M. Jungers.  Data-driven abstractions via adaptive refinements and a kantorovich metric.  In 2023 62nd IEEE Conference on Decision and Control (CDC), pages 6038–6043, 2023.
  * [7] F. Bullo.  Contraction Theory for Dynamical Systems.  Kindle Direct Publishing, 1.1 edition, 2023.
  * [8] M. C. Campi, S. Garatti, and F. A. Ramponi.  A general scenario theory for nonconvex optimization and decision making.  IEEE Transactions on Automatic Control, 63(12):4067–4078, 2018.
  * [9] R. Coppola, A. Peruffo, and M. Mazo.  Data-driven abstractions for verification of linear systems.  IEEE Control Systems Letters, 2023.
  * [10] R. Coppola, A. Peruffo, and M. Mazo Jr.  Data-driven abstractions for verification of deterministic systems.  arXiv preprint arXiv:2211.01793, 2022.
  * [11] M. Cubuktepe, N. Jansen, S. Junges, J.-P. Katoen, and U. Topcu.  Scenario-based verification of uncertain mdps.  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 287–305. Springer, 2020.
  * [12] A. Devonport, A. Saoud, and M. Arcak.  Symbolic abstractions from data: A pac learning approach.  In 2021 60th IEEE Conference on Decision and Control (CDC), pages 599–604, 2021.
  * [13] S. Garatti and M. C. Campi.  The risk of making decisions from data through the lens of the scenario approach.  IFAC-PapersOnLine, 54(7):607–612, 2021.
  * [14] S. Haesaert, P. M. Van den Hof, and A. Abate.  Data-driven and model-based verification via bayesian identification and reachability analysis.  Automatica, 79:115–126, 2017.
  * [15] H. W. Hethcote.  The mathematics of infectious diseases.  SIAM review, 42(4):599–653, 2000.
  * [16] M. Kazemi, R. Majumdar, M. Salamati, S. Soudjani, and B. Wooding.  Data-driven abstraction-based control synthesis.  arXiv preprint arXiv:2206.08069, 2022.
  * [17] S. Koch, J. L. Mathieu, D. S. Callaway, et al.  Modeling and control of aggregated heterogeneous thermostatically controlled loads for ancillary services.  In Proc. PSCC, pages 1–7. Citeseer, 2011.
  * [18] A. Lavaei, S. Soudjani, E. Frazzoli, and M. Zamani.  Constructing mdp abstractions using data with formal guarantees.  IEEE Control Systems Letters, 2022.
  * [19] R. Majumdar, N. Ozay, and A.-K. Schmuck.  On abstraction-based controller design with output feedback.  In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, pages 1–11, 2020.
  * [20] A. Makdesi, A. Girard, and L. Fribourg.  Data-driven models of monotone systems.  IEEE Transactions on Automatic Control, 2023.
  * [21] A. W. Moore.  Efficient memory-based learning for robot control.  Technical report, University of Cambridge, 1990.
  * [22] A. Peruffo and M. Mazo.  Data-driven abstractions with probabilistic guarantees for linear petc systems.  IEEE Control Systems Letters, 2022.
  * [23] A. Peruffo and M. Mazo.  Sampling performance of periodic event-triggered control systems: a data-driven approach.  IEEE Transactions on Control of Networked Systems, to appear, 2023.
  * [24] S. Sadraddini and C. Belta.  Formal guarantees in data-driven model identification and control synthesis.  In Proceedings of the 21st HSCC (part of CPS Week), pages 147–156, 2018.
  * [25] A. Salamati, A. Lavaei, S. Soudjani, and M. Zamani.  Data-driven safety verification of stochastic systems via barrier certificates.  IFAC-PapersOnLine, 54(5):7–12, 2021.  7th IFAC Conference ADHS 2021.
  * [26] S. Sastry.  Nonlinear systems: analysis, stability, and control, volume 10.  Springer Science & Business Media, 2013.
  * [27] A.-K. Schmuck and J. Raisch.  Asynchronous l-complete approximations.  Systems & Control Letters, 73:67–75, 2014.
  * [28] A.-K. Schmuck, P. Tabuada, and J. Raisch.  Comparing asynchronous l-complete approximations and quotient based abstractions.  In 2015 54th IEEE Conference on Decision and Control (CDC), pages 6823–6829. IEEE, 2015.
  * [29] P. Tabuada.  Verification and control of hybrid systems: a symbolic approach.  Springer Science & Business Media, 2009.
  * [30] Z. Wang and R. M. Jungers.  A data-driven method for computing polyhedral invariant sets of black-box switched linear systems.  IEEE Control Systems Letters, 2020.
  * [31] Z. Wang and R. M. Jungers.  Scenario-based set invariance verification for black-box nonlinear systems.  IEEE Control Systems Letters, 5(1):193–198, 2021.
  * [32] C. Wu, I. Kanevskiy, and M. Margaliot.  k-contraction: Theory and applications.  Automatica, 136:110048, 2022.

[]Rudi Coppola is a PhD candidate at the Delft Center for Systems and Control.
He obtained a BSc in Electronic Engineering cum laude at Univerisity of Pisa
in 2019 and a MSc in Electrical Engineering at King Abdullah University of
Science and Technology in 2021.

[]Andrea Peruffo is a postdoc at the Delft Center for Systems and Control. He
obtained the DPhil in Computer Science at the University of Oxford. He
received a Laurea in Information Engineering in 2012 and an MS in 2015 in
Automation Engineering, both from the University of Padova (IT). He worked as
a research engineer at Inria Rennes in 2016 and visited the Erato MMSD Group
at NII, Tokyo, in 2020. His research interests include hybrid systems, formal
verification and control theory.

[]Manuel Mazo Jr. is an Associate Professor at the Delft Center for Systems
and Control. He obtained an MSc and PhD in Electrical Engineering from the
University of California, Los Angeles (UCLA) in 2007 and 2010 respectively. He
also holds a Telecommunications Engineering degree from the Polytechnic
University of Madrid (UPM) and an Electrical Engineering degree from the Royal
Institute of Technology (KTH) in Stockholm, awarded under a TIME double degree
program in 2003. Prior to joining TU Delft, he spent two years as a
postdoctoral researcher at INCAS3 and the University of Groningen.

##  Appendix A Proofs

###  A.1 Proof of Lemma 5.8

Consider the parallelotope defined by

$Q(x_{1},...,x_{k})=\left\\{\sum_{i=1}^{k}r_{i}x_{i}\ :\
r_{i}\in[0,1]\right\\}.$

Its volume can be recursively computed as

$\text{vol}(Q(x_{1},...,x_{k})):=\text{vol}(Q(x_{1},...,x_{k-1}))h$

where $h$ is the Euclidean distance of $x_{k}$ from the subspace
$\text{span}(x_{1},...,x_{k-1})$, see [32]. We denote by $de_{i}$ the vector
of value $dx_{i}$ at the $i$-th component and 0 elsewhere. Trivially, the
infinitesimal element of volume shifted by $x$ can be described by
$x+Q(de_{1},...,de_{n})$ and
$\text{vol}(x+Q(de_{1},...,de_{n}))=\text{vol}(Q(de_{1},...,de_{n}))=\prod_{i=1}^{n}dx_{i}$.
Then, in first approximation, the shifted hypercube $x+Q(de_{1},...,de_{n})$
is transformed into the shifted parallelotope given by
$g(x)+Q(g(x+de_{1})-g(x),...,g(x+de_{n})-g(x))$. Let
$Q_{g}^{n}:=Q(g(x+de_{1})-g(x),...,g(x+de_{n})-g(x))$. It follows directly
that we can upper bound its volume as

$\text{vol}(Q_{g}^{n})\leq\text{vol}(Q_{g}^{n-1})||g(x+de_{n})-g(x))||_{2}\\\
\leq\prod_{i=1}^{n}||g(x+de_{i})-g(x))||_{2}.$

Additionally, by assumption

$\prod_{i=1}^{n}||g(x+de_{i})-g(x))||_{2}\leq\prod_{i=1}^{n}c||g(x+de_{i})-g(x))||_{p}\leq\\\
\prod_{i=1}^{n}cLq||de_{i}||_{2}=(cLq)^{n}\prod_{i=1}^{n}dx_{i}$

We conclude that for the infinitesimal volume it holds that
$\text{vol}(Q(g(x+de_{1})-g(x),...,g(x+de_{n})-g(x)))\leq(cLq)^{n}\text{vol}(Q(de_{1},...,de_{n}))$.
This relation extends to a general domain as long as it is Riemann integrable.

###  A.2 Proof of Proposition 5.9

Consider any set in $Q\subseteq\mathcal{D}$ and let us define the following
operations:

$\displaystyle{\rm Phys.~{}Rev.~{}E}{u}{Q}{}$
$\displaystyle:=\\{x\in\mathcal{X}:f(x,u)\in Q\\},$ $\displaystyle{\rm
Phys.~{}Rev.~{}E}{*}{Q}{k}$ $\displaystyle:=\\{x\in\mathcal{X}:\exists
u_{k}\in\mathcal{U}^{k},$
$\displaystyle\exists(\xi,\gamma,\upsilon,\xi^{\prime},\gamma^{\prime})\in\mathcal{I}_{H}(S,x,u_{k})\
.\ \xi^{\prime}(k-1)\in Q\\},$ (42) $\displaystyle{\rm
Phys.~{}Rev.~{}E}{*}{Q}{0}$ $\displaystyle:=Q,$ $\displaystyle\mu_{p}^{k}(Q)$
$\displaystyle:=\mu_{x}\left(\bigcup_{i=p}^{k}{\rm
Phys.~{}Rev.~{}E}{*}{Q}{k}\right).$ (43)

By Assumption 2 and Lemma 5.8, we bound the measure of the pre-image of a set
$Q$ by the measure of the set itself multiplied by a constant factor, i.e. it
holds that

$\mu_{x}({\rm Phys.~{}Rev.~{}E}{u}{Q}{})\leq\eta\mu_{x}(Q),$

where $\eta=\left(\frac{cu}{m_{X}}\right)^{n}$. As a result, by the union
bound, we can write that

$\mu_{0}^{1}(Q)\leq\bigcup_{u\in\mathcal{U}}\mu({\rm
Phys.~{}Rev.~{}E}{u}{Q}{})+\mu_{x}(Q)\leq(1+\lambda)\mu(Q)$

where $\lambda=|\mathcal{U}|\eta$. Note that ${\rm
Phys.~{}Rev.~{}E}{*}{Q}{k+1}={\rm Phys.~{}Rev.~{}E}{*}{{\rm
Phys.~{}Rev.~{}E}{*}{Q}{k}}{1}$. With this in mind, for
$\tau=\lceil(H+T+1)/(H+1)\rceil-1$, we can express

$\bigcup_{i=0}^{H+T}\text{Pre}_{\mathcal{D}}^{i}(Q)=\bigcup_{i=0}^{\tau-1}\left(\bigcup_{j=T-i(H+1)}^{H+T-i\cdot(H+1)}\text{Pre}_{\mathcal{D}}^{j}(Q)\right)\cup\bigcup_{j=0}^{H}\text{Pre}_{\mathcal{D}}^{j}(Q).$

Hence we derive the following bound

$\mu_{0}^{H+T}(Q)\leq\mu_{0}^{H}(Q)\left(1+\lambda^{T}\sum_{i=0}^{\tau-1}\lambda^{-i(H+1)}\right).$
(44)

Recall (29) and choose $Q=\mathcal{K}$. By combining (28) with (42) and (43)
we obtain that

$\mu_{x}(\mathcal{V}(\hat{S}_{\ell},\hat{\mathcal{R}},H))=\mu_{0}^{H}(\mathcal{K})$
(45)

By combining Equation (44), with the equation above we conclude that

$\mu_{0}^{H+T}(Q)\leq\mu_{0}^{H}(Q)\left(1+\lambda^{T}\sum_{i=0}^{\tau-1}\lambda^{-i(H+1)}\right).$
(46)