11institutetext:  University of Siegen, 11email: firstname.lastname@uni-
siegen.de 22institutetext: Knowledge-Based Systems Group, TU Dresden, Dresden,
Germany 22email<EMAIL_ADDRESS>
# Abstract Domains for Database Manipulating Processes

Tobias Schüler 11 0009-0008-1559-133X Stephan Mennicke 22 0000-0002-3293-2940
Malte Lochau 11 0000-0002-8404-753X

###### Abstract

Database manipulating systems (DMS) formalize operations on relational
databases like adding new tuples or deleting existing ones. To ensure
sufficient expressiveness for capturing practical database systems, DMS
operations incorporate as guarding expressions first-order formulas over
countable value domains. Those features impose infinite state, infinitely
branching processes thus making automated reasoning about properties like
reachability of states intractable. Most recent approaches therefore restrict
DMS to obtain decidable fragments. Nevertheless, a comprehensive semantic
framework capturing full DMS, yet incorporating effective notions of data
abstraction and process equivalence is an open issue. In this paper, we
propose DMS process semantics based on principles of abstract interpretation.
The concrete domain consists of all valid databases, whereas the abstract
domain employs different constructions for unifying sets of databases being
semantically equivalent up to particular fragments of the DMS guard language.
The connection between abstract and concrete domain is effectively established
by homomorphic mappings whose properties and restrictions depend on the
expressiveness of the DMS fragment under consideration. We instantiate our
framework for canonical DMS fragments and investigate semantical preservation
of abstractions up to bisimilarity, being one of the strongest equivalence
notions for operational process semantics.

###### Keywords:

database manipulating systems abstract interpretation labeled transition
systems bisimulation equivalence.

##  1 Introduction

Background and Motivation. Modern software systems intensively interact with
diverse environmental components which often includes one or more (relational)
databases. Database manipulating systems [1] (DMS) and similar approaches [7,
8, 4, 22] characterize the operational behavior of (relational) database
systems by formalizing actions consecutively transforming the current state of
databases by adding new tuples or deleting existing ones. The action language
supported by DMS-like formalisms must be sufficiently expressive to capture
crucial behavioral aspects of practical database systems. To this end, those
actions combine set-based add/delete operations with FOL formulas both defined
on databases over (countable) value domains [2]. The FOL part serve as
guarding expressions for actions which, if enabled, have the ability to
further expand and/or narrow the active domain of databases reached in the
subsequent state. However, these distinct features of DMS-like formalisms
impose intrinsically problematic properties on the underlying operational
semantics. For instance, using labeled transitions systems (LTS) [7], the
resulting process model is not only non-regular and infinite-state, but even
infinitely branching as arbitrary fresh data may be added to databases in a
step. Essential correctness properties of DMS processes like reachability of
states are thus not only theoretically undecidable, but also practically
intractable by state-of-the-art reasoning tools. As a pragmatic workaround,
most approaches consider bounded state spaces and/or narrow down
expressiveness of DMS languages to obtain decidable fragments [1].

Contributions. In this paper, we apply the framework of _abstract
interpretation_ [9, 10] to tame the LTS semantics of DMS processes. In the
concrete domain, the set of LTS states corresponds to all valid databases of a
given database schema over infinite value domains. In the abstract domain, LTS
states are constructed by employing different abstraction operators for
unifying subsets of databases. This abstract representation enables us to
effectively connect the abstract and concrete domains by means of homomorphic
mappings. The types of properties of DMS processes being preserved and/or
reflected by abstraction depend on the expressiveness of the DMS fragment used
in DMS actions as well as the notion of process equivalence under
consideration. We instantiate our framework for canonical DMS fragments and
investigate behavior preservation of abstractions up to bisimilarity. As
bisimilarity constitutes one of the strongest equivalence notions for LTS-
based process semantics, our abstraction builds the basis for guaranteeing
preservation of essential semantical properties. In this way, our framework
provides a sound conceptual basis for building effective model-checking tools
for DMS process verification [10].

##  2 Foundations

#### Databases.

We assume a first-order (FO) vocabulary consisting of mutually disjoint
(countably infinite) sets of constants $\mathbf{C}$, variables $\mathbf{V}$,
and predicates $\mathbf{P}$. Each predicate $p\in\mathbf{P}$ has an arity
$\textit{ar}(p)\in\mathbb{N}$. Terms are either constants or variables, and
for a list of terms $\mathbf{t}=t_{1},\ldots,t_{n}$ we denote its length by
$|\mathbf{t}|=n$. An expression $p(\mathbf{t})$ is an atom if $p\in\mathbf{P}$
and $\mathbf{t}$ is a term list, such that $\textit{ar}(p)=|\mathbf{t}|$. An
atom is _grounded_ if it is variable-free and we call a finite set of ground
atoms $\mathcal{D}$ a _database_. The universe of all databases is
$\mathbb{U}^{\mathbf{C}}$. A (possibly infinite) set of ground atoms
$\mathcal{I}$ is an _instance_ with the respective universe
$\mathbb{I}^{\mathbf{C}}$. Note that,
$\mathbb{U}^{\mathbf{C}}\subseteq\mathbb{I}^{\mathbf{C}}$.

#### Guards.

We consider FOL formulas $g$ to serve as guards as follows:

$\begin{array}[]{rcc|c|c|c|c}\Phi&::=&p(\mathbf{t}){}&~{}t=u{}&~{}\neg\Phi{}&~{}\Phi\wedge\Phi{}&~{}\exists
x.\ \Phi\end{array}$ (1)

where $p(\mathbf{t})$ is an atom, $t,u$ are terms, and $x\in\mathbf{V}$. The
terms occurring in guard $g$ being variables are referred to by the set
$\textit{vars}(g)$. A variable $x\in\textit{vars}(g)$ is either _free_ or
_bound_ in $g$, defining the set
$\textit{free}(g)$111$\textit{free}(r(\mathbf{t}))=\mathbf{t}\cap\mathbf{V}$,
$\textit{free}(t=u)=\\{t,u\\}\cap\mathbf{V}$, $\textit{free}(\neg
g)=\textit{free}(g)$,
$\textit{free}(g\wedge\psi)=\textit{free}(g)\cup\textit{free}(\psi)$, and
$\textit{free}(\exists x.\ g)=\textit{free}(g)\setminus\\{x\\}$. of free
variables.

#### Guards as FOL Fragments.

Table 1: Guard fragments, their formula shape, and their abbreviation guard fragment |  abbrv. |  formula
---|---|---
_normal conjuncitve guard_ |  NCG |  $\exists\mathbf{y}.\ a_{1}\wedge\ldots\wedge a_{m}\wedge\neg b_{1}\wedge\ldots\wedge\neg b_{n}$
_projection-free NCG_ |  pf-NCG |  $a_{1}\wedge\ldots\wedge a_{m}\wedge\neg b_{1}\wedge\ldots\wedge\neg b_{n}$
_conjuncitve guard_ |  CG |  $\exists\mathbf{y}.\ a_{1}\wedge\ldots\wedge a_{m}$
_projection-free CG_ |  pf-CG |  $a_{1}\wedge\ldots\wedge a_{m}$
_conjunction of negated atoms_ |  CNA |  $\forall\mathbf{y}.\ \neg a_{1}\wedge\ldots\wedge\neg a_{m}$

A _normal conjunctive guard_ (NCG) is a formula

$\exists\mathbf{y}.\ a_{1}\wedge\ldots\wedge a_{m}\wedge\neg
b_{1}\wedge\ldots\wedge\neg b_{n}$ (2)

where $\mathbf{y}$ is a list of variables occurring in the atoms
$a_{1},\ldots,a_{m},b_{1},\ldots,b_{n}$. For an NCG $g$ of shape (2) we refer
to the positive guard part by $g^{+}=\exists\mathbf{y}.\
a_{1}\wedge\ldots\wedge a_{m}$ and its negated part by
$g^{-}=\exists\mathbf{y}.\ \neg b_{1}\wedge\ldots\wedge\neg b_{n}$,
respectively. Whenever convenient, $g^{+}$ ($g^{-}$, resp.) identifies the set
of atoms occurring within $g$, meaning $g^{+}=\\{a_{1},\ldots,a_{m}\\}$
($g^{-}=\\{b_{1},\ldots,b_{n}\\}$, resp.). An NCG $g$ with $g^{-}=\emptyset$
is a _conjunctive guard_ (CG). An NCG $g$ is _safe_ if
$\textit{vars}(g^{-})\subseteq\textit{vars}(g^{+})$. Similarly, the other
guard fragments are summarized in Table 1.

#### Substitution.

A _substitution_ is a partial function $\sigma:\mathbf{V}\to\mathbf{C}$
mapping variables to constants. The set of all variables for which $\sigma$ is
defined is denoted by $\textit{dom}(\sigma)$. We call $\sigma$ a _substitution
for guard $g$_ if $\textit{vars}(g)\subseteq\textit{dom}(\sigma)$. Such a
substitution replaces variables of a guard by constants and, thereby, forms a
_guard match_. For convenience, we assume for every substitution $\sigma$ and
constant $c\in\mathbf{C}$, $\sigma(c)=c$, extending the signature of $\sigma$
to $\mathbf{V}\cup\mathbf{C}\to\mathbf{C}$. If $\mathbf{t}=t_{1}\dots t_{n}$
is a list of terms and $\sigma$ a substitution defined for all variables in
$\mathbf{t}$, we denote by $\mathbf{t}\sigma$ the term list
$\sigma(t_{1})\dots\sigma(t_{n})$. A substitution $\sigma$ is a _match to
guard $g$ in instance $\mathcal{I}$_ if (a)
$\textit{free}(g)=\textit{dom}(\sigma)$ and (b) $\mathcal{I},\sigma\models g$,
where

  * •

$\mathcal{I},\sigma\models p(\mathbf{t})$ if
$p(\mathbf{t}\sigma)\in\mathcal{I}$,

  * •

$\mathcal{I},\sigma\models t=u$ if $t\sigma=u\sigma$,

  * •

$\mathcal{I},\sigma\models\neg g$ if $\mathcal{I},\sigma\models g$ does not
hold,

  * •

$\mathcal{I},\sigma\models g\wedge g^{\prime}$ if $\mathcal{I},\sigma\models
g$ and $\mathcal{I},\sigma\models g^{\prime}$, and

  * •

$\mathcal{I},\sigma\models\exists x.\ g$ if $\mathcal{I},\sigma[x\mapsto
c]\models g$ for some $c\in\mathbf{C}$.

#### Guard matches.

We denote the set of all matches to guard $g$ in instance $\mathcal{I}$ by
$g(\mathcal{I})$. We may simply write $g$ to identify a guard. A guard match
to NCGs $g=\exists\mathbf{y}.\ \psi$ in $\mathcal{I}$ is tightly connected to
the existence of homomorphisms from $\psi$ (viewed as a set of atoms) to
instance $\mathcal{I}$. A function
$h:\mathbf{C}\cup\mathbf{V}\to\mathbf{C}\cup\mathbf{V}$ is called a
_homomorphism_ from a set of atoms $\mathcal{A}$ into a set of atoms
$\mathcal{B}$ if (a) $h(c)=c$ for all $c\in\mathbf{C}$ and (b)
$p(t_{1},\dots,t_{n})\in\mathcal{A}$ implies
$p(h(t_{1}),\dots,h(t_{n}))\in\mathcal{B}$.

Also NCAs, CGs and their negation have a correspondence to homomorphisms as
follows.

###### Proposition 1

For instance $\mathcal{I}$, CG $g$, and substitution $\sigma$, $\sigma\in
g(\mathcal{I})$ if, and only if, $\textit{free}(g)=\textit{dom}(\sigma)$ and
there is a homomorphism $h:g\to\mathcal{I}$ such that $\sigma\subseteq h$.

###### Proposition 2

For instance $\mathcal{I}$, NCA $g$, and substitution $\sigma$, $\sigma\in
g(\mathcal{I})$ if, and only if, $\textit{free}(g)=\textit{dom}(\sigma)$ and
there is a function $h:\mathbf{C}\cup\mathbf{V}\to\mathbf{C}$, such that (a)
$h(c)=c$ for all $c\in\mathbf{C}$, (b) $h(g)\cap\mathcal{I}=\emptyset$, and
(c) $\sigma\subseteq h$.

This characterizations of guard matches to NCAs and CGs turns out to be quite
useful in proofs of following sections.

#### Guard match, query answer and substitution.

Guards and guard matches are very similar to queries and query answers in
database systems. However, whereas query answers should be _domain
independent_ (i.e., having finitely many possible substitutions [2]), this
does not necessarily hold for guard matches [1]. For instance, query $\neg
P(x)$ would have infinitely many answers and is therefore prohibited, whereas
the corresponding guard simply checks if, for instance, a to-be-added person
is not yet contained in the database.

###### Example 1

We consider a simplified social network (SSN) with two predicates, (1) a unary
predicate $P(\textit{name})$ for _persons_ currently being members of the
network with attributes $name$, and (2) a binary predicate
$F(\textit{name}_{1},\textit{name}_{2})$ for a non-symmetric _friendship_
relation from person $\textit{name}_{1}$ to person $\textit{name}_{2}$. We
assume all possible strings denoting names to be part of $\mathbf{C}$. A
database of our SSN may be
$\mathcal{D}_{e}=\\{P(\text{A}),P(\text{B}),P(\text{C}),F(\text{A},\text{B}),F(\text{B},\text{A}),F(\text{A},\text{C})\\}$
(with A, B and C may be Alice, Bob and Charles). Potential guards are

  * •

a symmetric friendship: $g_{sf}=F(x,y)\wedge F(y,x)$,

  * •

a directed friendship: $g_{df}=F(x,y)\wedge\neg F(y,x)$,

  * •

a friendship from $x$ to someone: $g_{af}=\exists y.F(x,y)$, and

  * •

no friendship: $g_{nf}=\neg F(x,y)\wedge\neg F(y,x)$.

On $\mathcal{D}_{e}$ we obtain the following guard matches:

  * •

$g_{sf}(\mathcal{D}_{e})=\\{\\{x\mapsto\text{A},y\mapsto\text{B}\\},\\{x\mapsto\text{B},y\mapsto\text{A}\\}\\}$,

  * •

$g_{df}(\mathcal{D}_{e})=\\{\\{x\mapsto\text{A},y\mapsto\text{C}\\}\\}$,

  * •

$g_{sf}(\mathcal{D}_{e})=\\{\\{x\mapsto\text{A}\\},\\{x\mapsto\text{B}\\}\\}$,
and

  * •

$g_{nf}(\mathcal{D}_{e})=\\{\\{x\mapsto\text{B},y\mapsto\text{C}\\},\\{x\mapsto\text{C},y\mapsto\text{B}\\},\\{x\mapsto\text{A},y\mapsto\text{A}\\},\dots\\}$.

For instance $\mathcal{D}_{e},\\{x\mapsto\text{A},y\mapsto\text{B}\\}\models
g_{sf}$ holds as Alice is a friend of Bob and Bob is a friend of Alice,
whereas $\mathcal{D}_{e},\\{x\mapsto\text{A},y\mapsto\text{B}\\}\models
g_{df}$ does not hold.

#### Database Manipulating Systems.

Database manipulating systems formalize possible sequences of _actions_
consecutively applied to database instances. Syntactically, our formalization
loosely follows the canonical notion of actions used in the DMS formalism by
Abdulla et al. [1]. An action consists of a _guard_ and an _effect_ on the
current instance. A guard specifies on which instances the action is
applicable. The effect might be deletion of atoms from the instance and adding
new atoms to the instance. Formally, the effect comprises two finite sets of
atoms, $\tt Del$ and $\tt Add$, such that $\textit{vars}(\tt
Del)\subseteq\textit{free}(g)$. Atoms in $\tt Del$ are determined by the match
for guard $g$, while $\tt Add$ is a collection of new atoms. Note that $\tt
Del$ and $\tt Add$ may contain variables that will be bound by (a) the guard
matches and (b) by arbitrary constants in case of those variables in
$\textit{vars}(\tt Add)\setminus\textit{free}(g)$. The rationale behind case
(b) is that an action inserting atoms may depend on external stimuli like
sensor data or user input. An action act is a triple $(g,\tt Del,\tt Add)$
which forms the basis of a _database manipulating system_ (DMS).

######  Definition 1 (Database Manipulating System)

A _database manipulating system_ (DMS) is a pair
$\mathcal{S}=(\mathcal{I}_{0},\textsc{Act})$ where $\mathcal{I}_{0}$ is the
_initial instance_ and Act is a finite set of actions.

From $\mathcal{I}_{0}$, any sequence of actions $\textit{act}=(g,\tt Del,\tt
Add)\in\textsc{Act}$ may be performed based on substitutions $\sigma$ due to
matches of guard $g$. Note that $\sigma$ specifies all variables occurring in
$\tt Del$. We denote by $\tt Del\sigma$ the set obtained by replacing all
occurrences of variables $x\in\textit{vars}(\tt Del)$ by $\sigma(x)$. In
general, for a set of atoms $\mathcal{A}$ and substitution $\sigma$,
$\mathcal{A}\sigma$ is the set of atoms in which each variable
$x\in\textit{vars}(\mathcal{A})$ has been replaced by $\sigma(x)$ if it is
defined for $\sigma$. Set $\tt Add$ may contain variables which are not in
$\textit{dom}(\sigma)$ such that $\tt Add\sigma$ is not a proper database . To
facilitate arbitrary external inputs, we expand $\sigma$ to the missing
variables. Substitution $\sigma^{\star}$ extends $\sigma$ to $\tt Add$ if
$\textit{dom}(\sigma^{\star})=\tt Add$ and $\sigma\subseteq\sigma^{\star}$.
Extending $\sigma$ to $\sigma^{\star}$ completes a step by deletions $\tt
Del\sigma^{\star}$ from and additions $\tt Add\sigma^{\star}$ to the current
instance.

######  Definition 2 (DMS Step)

A DMS action $\textit{act}=(g,\tt Del,\tt Add)$ is _enabled under instance
$\mathcal{I}$ and substitution $\sigma$_, denoted
$\mathcal{I}[\textit{act},\sigma\rangle$, if $\sigma\in g(\mathcal{I})$. If
$\mathcal{I}[\textit{act},\sigma\rangle$, then an effect is an extension
$\sigma^{\star}$ of $\sigma$ to $\tt Add$, producing instance
$\mathcal{I}^{\prime}=(\mathcal{I}\setminus\tt Del\sigma^{\star})\cup\tt
Add\sigma^{\star}$. We denote the _DMS step_ from $\mathcal{I}$ to
$\mathcal{I}^{\prime}$ via act and $\sigma$ by
$\mathcal{I}\mathrel{[\textit{act},\sigma^{\star}\rangle}\mathcal{I}^{\prime}$.

###### Example 2

Action $\textit{act}_{\textit{add}}=(\textit{true},\emptyset,\\{P(x)\\})$
(adding a new person) is enabled under each instance even if the person
already exists in that instance. Thus, $\sigma$ is empty and $\sigma^{\star}$
may be, e.g., $\\{x\mapsto\text{A}\\}$. Action
$\textit{act}_{\textit{rev}}=(g_{df},\\{F(x,y)\\},\\{F(y,x)\\})$ checks if a
directed friendship exists between $x$ and $y$, deletes this friendship and
adds the reversed friendship.

The formal semantics of a DMS is defined as a _labeled transition system_
(LTS).

######  Definition 3 (Labeled Transition System)

A _labeled transition system_ (LTS) is a triple
$\mathcal{T}=(Q,\Sigma,\mathrel{\ext@arrow 0359\Rightarrowfill@{}})$ where $q$
is a set of states (processes), $\Sigma$ is a set of transition labels, and
$\mathrel{\ext@arrow 0359\Rightarrowfill@{}}\subseteq Q\times\Sigma\times Q$ a
transition relation. We denote $(q,a,q^{\prime})\in\mathrel{\ext@arrow
0359\Rightarrowfill@{}}$ as $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}$ and write $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}$ if $\exists q^{\prime}\in Q:q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}$ and $q\not\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}$ if not $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}$.

LTS $\mathcal{T}=(Q,\Sigma,\mathrel{\ext@arrow 0359\Rightarrowfill@{}})$ is
(a) _finitely branching_ if for each $q\in Q$, the set $\\{q^{\prime}\in
Q\mid\exists a\in\Sigma:q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}\\}$ is finite,  (b) _image-finite_ if for
each $q\in Q$ and $a\in\Sigma$, the set $\\{q^{\prime}\in Q\mid
q\mathrel{\ext@arrow 0359\Rightarrowfill@{}{a}}q^{\prime}\\}$ is finite,  (c)
_finite-state_ if $Q$ is finite, and  (d) _deterministic_ if for each state
$q\in Q$ and $a\in\Sigma$, $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}$ and $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime\prime}$ implies
$q^{\prime}=q^{\prime\prime}$.  Although LTSs may be directly associated with
directed edge-labeled graphs, comparison relations based on graph
homomorphisms are too strong to capture distinctive features of LTS processes.
Instead, _simulation_ and _bisimulation_ relations on processes are used.
Intuitively, process $q$ simulates $p$ if every action that may be performed
by $p$ can be mimicked by $q$ and the successor states again simulate each
other.

######  Definition 4 ((Bi-)Simulation)

For an LTS $(Q,\Sigma,\mathrel{\ext@arrow 0359\Rightarrowfill@{}})$, a binary
relation $R\subseteq Q\times Q$ is a _simulation_ if for all $(p,q)\in R$ and
$a\in\Sigma$, $p\mathrel{\ext@arrow 0359\Rightarrowfill@{}{a}}p^{\prime}$
implies that $q^{\prime}\in Q$ exists such that $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}$ and $(p^{\prime},q^{\prime})\in R$.
Process $q\in Q$ _simulates_ process $p\in Q$ if there is a simulation $R$
with $(p,q)\in R$. If $p$ simulates $q$ by simulation $R$, and $q$ simulates
$p$ by simulation $R^{\prime}$, then $p$ and $q$ are _similar_. Simulation $R$
is a _bisimulation_ if, and only if, $R^{-1}:=\\{(q,p)\mid(p,q)\in R\\}$ is
also a simulation. If there is a bisimulation $R$, such that $(p,q)\in R$,
then $p$ and $q$ are _bisimilar_.

Note, the witnesses $R$ and $R^{\prime}$ for similarity are not necessarily
bisimulations as possibly $R^{-1}\neq R^{\prime}$.

DMS semantics can be formalized as an LTS
$\textsf{DMS}:=(\mathbb{U}^{\mathbf{C}},\textsc{Act}\Sigma,\mathrel{\ext@arrow
0359\Rightarrowfill@{}})$ where $\mathrel{\ext@arrow 0359\Rightarrowfill@{}}$
is formed by $\mathcal{I}_{1}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{I}_{2}$ if,
and only if,
$\mathcal{I}_{1}\mathrel{[\textit{act},\sigma\rangle}\mathcal{I}_{2}$ (cf.
Def. 2). In general, DMS is infinitely branching, infinite-state, and
deterministic.

DMS builds the basis for investigating desirable properties of all possible
processes defining a DMS. For instance, the _reachability problem_ asks for a
given DMS and a distinguished action $\textit{act}_{x}$, if there is an
instance $\mathcal{I}_{x}$ with $\mathcal{I}_{0}\mathrel{\ext@arrow
0359\Rightarrowfill@{}}\mathcal{I}_{1}\mathrel{\ext@arrow
0359\Rightarrowfill@{}}\dots\mathrel{\ext@arrow
0359\Rightarrowfill@{}}\mathcal{I}_{x}$ such that action $\textit{act}_{x}$ is
enabled under $\mathcal{I}_{x}$. The reachability problem is undecidable for
DMS [1].

###### Example 3

We introduce a new binary predicate $W(w_{1},w_{2})$ with $w_{1}$ and $w_{2}$
being words over $\mathbf{C}^{*}$ where $W(\epsilon,\epsilon)$ holds for the
initial database. For each friendship predicate $F(x,y)$ we consider a set of
DMS actions of the form
$\textit{act}_{F(x,y)}:=(W(w_{1},w_{2}),W(w_{1},w_{2}),W(w_{1}\circ
x,w_{2}\circ y))$ where $\circ$ denotes concatenation. We consider the DMS
action $\textit{act}_{\textit{end}}=(W(w_{1},w_{2})\wedge
w_{1}=w_{2},\emptyset,\emptyset)$. Then, the reachability problem with respect
to $\textit{act}_{\textit{end}}$ is undecidable as it can be reduced to Post’s
correspondence problem.

The next example constitutes a semi-decidable reachability problem.

###### Example 4

Given a predefined set of persons and actions for consecutively adding and
deleting friendships between arbitrary pairs of persons, do we eventually
reach a database containing a triangle friendship between three different
persons (i.e., $x$ a friend of $y$, $y$ a friend of $z$ and $z$ a friend of
$x$)? To this end, we expand the unary predicate $P(\textit{name})$ to a
binary predicate $P(\textit{name},\textit{name})$ and use NCG to define a
guard $P(x,x)\wedge P(y,y)\wedge\neg P(x,y)$. $\neg P(x,y)$ (i.e., ensuring
that $x$ and $y$ match different persons). This is a standard technique to
avoid $\neq$ in first order formulas. Starting from an arbitrary database, we
consider two actions: $\textit{act}_{add}:=(P(x,x)\wedge P(y,y)\wedge\neg
P(x,y),\emptyset,F(x,y))$ (adding a friendship) and
$\textit{act}_{delete}:=(F(x,y),F(x,y),\emptyset)$ (deleting a friendship) and
ask for reachability of the action $\textit{act}_{end}=(\exists
x,y,z.F(x,y)\wedge F(y,z)\wedge F(z,x)\wedge\neg P(x,y)\wedge\neg
P(y,z)\wedge\neg P(z,x),\emptyset,\emptyset)$.

A finite solution to this problem comprises an _abstract LTS_ with four
states, where each of those abstract states contains all subsets of databases
with (1) no friendships, (2) friendship chains of maximum length $\leq 2$, (3)
friendship chains of maximum length $>2$ without any triangles, and (4) at
least one triangle.

In the remainder of this paper, we develop a hierarchy of abstract domains to
characterize semantic-preserving abstractions of states of DMS depending on
the expressiveness of the guard fragment used. Our approach is based on the
formal framework of abstract interpretation.

##  3 Principles of Abstract Interpretation

Before we present our abstract interpretation framework for DMS, we first
describe its basic ingredients. Different processes assembled in
$\mathsf{DMS}$ may share similar behavior in terms of their enabled actions
and subsequent processes. For instance, let us consider a DMS action which
inserts a friendship between Alice and Bob, where the guard of this action
consists of a conjunction of atoms requiring Alice and Bob to exist in the
database. All (i.e., countably infinitely many) _concrete states_ matching
this guard may be aggregated into _one_ single abstract state. The concrete
states aggregated in the subsequent abstract state reached after performing
this action then all share the inserted relationship between Alice and Bob.
The way how the concrete states are aggregated into, and reconstruction from,
such an abstract state clearly depends on the guard fragment used. In
addition, DMS states are infinitely branching due to the ability of DMS
actions to insert any possible new value. However, in many cases, the exact
values are often not relevant for reasoning about the subsequent behavior and
can therefore be aggregated into one representative abstract value. The
following definitions are based on Dams et al. [10] and conceptualize these
observations.

#### Lattice.

Abstract interpretation provides a framework for effectively reasoning about
computational models over infinite semantic domains modeled as lattices. By
$\sqcap$ and $\sqcup$ we denote binary operations on sets $S$. The operators
$\sqcap$ and $\sqcup$ are monotone with respect to a partial order $\leq$ on
$S$ (i.e., $x_{1},x_{2},y_{1},y_{2}\in S$, $x_{1}\leq x_{2}$ and $y_{1}\leq
y_{2}$ implies $x_{1}\sqcap y_{1}\leq x_{2}\sqcap y_{2}$ and $x_{1}\sqcup
y_{1}\leq x_{2}\sqcup y_{2}$).

######  Definition 5 (Lattice)

A _lattice_ is a partially ordered set $(S,\leq)$ such that each two-element
subset $\\{x,y\\}\subseteq S$ has (1) a unique least upper bound in $S$,
denoted by $x\sqcup y$, and (2) a unique greatest lower bound in $S$, denoted
by $x\sqcap y$. A _bounded lattice_ has a unique greatest element $\top$ and a
unique least element $\bot$ such that $\top\geq\bigsqcup_{x\in S}x$,
$\bot\leq\bigsqcap_{x\in S}x$ and $\bot\leq x\leq\top$ for all $x\in S$.
$\top$ and $\bot$ are identities for $\sqcap$ and $\sqcup$.

Bounded lattices are not further deployed in the following but are mentioned
here only for the sake of comprehensibility. Abstract interpretation aims at
establishing connections between lattices modeling different semantic domains.

#### Galois Connection.

By $(\mathbb{C},\sqsubseteq)$ we denote a concrete semantic domain where
$\mathbb{C}=2^{Q}$ comprises the set of all subsets of concrete sets of states
$Q$ of a computational model (here: $\mathsf{DMS}$). By $\sqsubseteq$ we
denotes a partial (semantic) ordering on $\mathbb{C}$ (here: $\subseteq$). By
$(\mathbb{A},\preceq)$ we denote an abstract semantic domain where
$\mathbb{A}$ is a set of abstract states and $\preceq$ a partial (precision)
ordering on $\mathbb{A}$. It is crucial that the elements of the concrete
domain $\mathbb{C}$ are possible _subsets_ of concrete states, whereas the
elements of the abstract domain $\mathbb{A}$ are _singleton_ abstract states.
The mutual connection between concrete and abstract domain is shaped by a pair
of abstraction function $\alpha:\mathbb{C}\to\mathbb{A}$ and a concretization
function $\gamma:\mathbb{A}\to\mathbb{C}$, together forming a _Galois
connection_.

######  Definition 6 (Galois Connection)

The pair
$(\alpha:\mathbb{C}\rightarrow\mathbb{A},\gamma:\mathbb{A}\rightarrow\mathbb{C})$
is a _Galois connection_ between lattices $(\mathbb{C},\sqsubseteq)$ and
$(\mathbb{A},\preceq)$ if (1) $\alpha$ and $\gamma$ are _total_ and _monotone_
, (2) $\forall C\in\mathbb{C}:\gamma\circ\alpha(C)\sqsupseteq C$, and (3)
$\forall a\in\mathbb{A}:\alpha\circ\gamma(a)\preceq a$.

Monotonicity guarantees that more precise abstractions single out fewer
concrete states and, conversely, abstracting larger sets of concrete states
yields less precise abstractions. Furthermore, (2) requires that concrete
states are preserved after reconstruction. Finally, (3) requires a form of
optimality of the abstraction thus not decreasing precision.

#### Bisimulation.

We lift (bi-)simulations to steps $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}C^{\prime}$ between sets of concrete states as
apparent in the concrete domain in two ways: either (1) there is at least one
process $q\in C$ with $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}$ and $q^{\prime}\in C^{\prime}$, or (2)
all processes in $C$ evolve to some process in $C^{\prime}$ by action $a$. We
may refer to case (1) as an $\exists$-step and to case (2) as a
$\forall$-step, and adapt the notions of (bi-)simulation to the these new
types of steps.

######  Definition 7 ($\forall$/$\exists$-(bi-)simulation)

For abstract domain $(\mathbb{A},\preceq)$ and concrete domain
$(\mathbb{C},\sqsubseteq)$, a binary relation
$R\subseteq\mathbb{A}\times\mathbb{C}$ is an _$\exists$ -simulation_ if for
all $(\mathcal{A},C)\in R$ and $a\in\textsc{Act}$,
$\mathcal{A}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}\mathcal{A}^{\prime}$ implies that there is a
$C^{\prime}\in\mathbb{C}$ such that (a) $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}C^{\prime}$ with a $q\in C$ for each $q^{\prime}\in
C^{\prime}$ such that $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}$, and (b)
$(\mathcal{A}^{\prime},C^{\prime})\in R$. $R$ is a _$\forall$ -simulation_ if,
additionally to being an $\exists$-simulation, for each $q\in C$ there is a
$q^{\prime}\in C^{\prime}$ with $q\mathrel{\ext@arrow
0359\Rightarrowfill@{}{a}}q^{\prime}$.

If $(\mathcal{A},C)\in R$ and $R$ is a $\forall$/$\exists$-simulation, we say
that $C$ $\forall$/$\exists$-simulates $\mathcal{A}$. By reversing the
conditions of $\forall$/$\exists$-simulations, we get
$\forall$/$\exists$-simulations between the concrete domain and the abstract
domain (i.e., $R\subseteq\mathbb{C}\times\mathbb{A}$). Naturally, a
$\forall$/$\exists$-simulation $R$ is called a
$\forall$/$\exists$-bisimulation if, and only if, $R^{-1}$ is a
$\forall$/$\exists$-simulation. In this paper we restrict our considerations
to $\forall$-bisimulations which preserves reachability properties as in our
running example. Analogously, $\exists$-bisimulation preserve safety
properties and will be considered as a future work.

Please note that the different system types (single instances vs. sets)
introduces a slight asymmetry into the notions of
$\forall$/$\exists$-(bi-)simulations. Although every $\forall$-simulation
$R\subseteq\mathbb{A}\times\mathbb{C}$ is an $\exists$-simulation, a
$\forall$-simulation $R\subseteq\mathbb{C}\times\mathbb{A}$ does not
necessarily adhere to the requirements of an $\exists$-simulation. The reason
is that $(C,\mathcal{A})$ of a $\forall$-simulation
$R\subseteq\mathbb{C}\times\mathbb{A}$ considers only steps
$C\mathrel{\ext@arrow 0359\Rightarrowfill@{}{a}}C^{\prime}$ that are complete
(i.e., every database in $C$ evolves) while if $R$ is viewed as an
$\exists$-simulation, only one database from $C$ may evolve, say to some
singleton set $C^{\prime\prime}$ which is not necessarily captured by $R$.
Therefore, the $\forall$-bisimulation results we obtain throughout the next
section do not entail respective $\exists$-bisimulation results.

#### Abstract Interpretation Framework.

The remainder of this paper is devoted to a hierarchy of concrete domains
$(\mathbf{2}^{\mathbb{U}},\subseteq)$ for DMS processes shaped by different
fragments of FOL as guard language, where the functions $\gamma$ and $\alpha$
are either based on the supremum or infimum of the corresponding abstract
domains. For a guard language $\mathcal{L}$, we call a Galois connection
$(\alpha,\gamma)$ an _abstract interpretation w.r.t. $\mathcal{L}$_ if for
each set of databases $C\subseteq\mathbb{U}$ and set of DMS actions Act using
only guards from $\mathcal{L}$, $\alpha(C)$ and $C$ are $\forall$-bisimilar.

##  4 Abstract Interpretation of DMS

The concrete domain is fixed: $(\mathbf{2}^{\mathbb{U}},\subseteq)$. For
(possibly infinite) sets $C$ of databases, we effectively present six
different abstractions: The first two very basic ones are based on (set) union
and intersection. The third abstraction is a (Cartesian) combination of the
two prior abstractions with the benefit of supporting a more practical guard
fragment. One caveat about these abstractions is that we have to waive
projection (i.e., existential quantification). To gain DMS actions with more
expressive guards, and thereby capture more realistic systems, we devise
abstractions for more general abstract domains. We expand our abstract domain
incorporating so-called _labeled nulls_ as terms in abstract instances. The
order on the abstract domain is then based on homomorphisms. The three
remaining abstractions are complements of the first three, now in the more
abstract domain incorporating labeled nulls. Table 2 summarizes our results.

Table 2: Abstract Domains, Interpretations, and Respective Guard Fragments abstract domain | $\alpha(C)$ | $\gamma(\mathcal{I})$ |  fragment |
---|---|---|---|---
$(\mathbb{I},\subseteq)$ | $\bigcup C$ | $\\{\mathcal{D}\subseteq\mathcal{I}\\}$ | CNA | Theorem 4.1
$(\mathbb{I},\supseteq)$ | $\bigcap C$ | $\\{\mathcal{I}\subseteq\mathcal{D}\\}\ $ | pf-CG | Theorem 4.2
$(\mathbb{I}\times\mathbb{I},\leq)$ | $(\bigcap C,\bigcup C)$ | $\\{\mathcal{I}\subseteq\mathcal{D}\wedge\mathcal{D}\subseteq\mathcal{I}\\}\ $ | pf-NCG | Theorem 4.3
$(\mathbb{I}^{\mathbf{N}},\rightarrow)$ | $\bigsqcup C$ | $\\{\mathcal{D}\to\mathcal{I}\\}$ | CNA | Theorem 4.5
$(\mathbb{I}^{\mathbf{N}},\leftarrow)$ | $\bigsqcap C$ | $\\{\mathcal{I}\to\mathcal{D}\\}$ | CG | Theorem 4.4
$(\mathbb{I}^{\mathbf{N}}\times,\mathbb{I}^{\mathbf{N}},\preceq)$ | $(\bigsqcap C,\bigsqcup C)$ | $\\{\mathcal{I}\to\mathcal{D}\wedge\mathcal{D}\to\mathcal{I}\\}$ | NCG | Theorem 4.6

The rest of this section is structured as follows. First, we introduce a naive
set-based abstraction based on the set union operator on databases together
with a summary of further set-based abstractions. Resolving the issue of
neglecting variable projections in guards we introduce instances with labeled
nulls, on which CGs can be used without losing precision. Finally, we combine
unions and intersections to even support DMS actions with NCGs. Other
abstractions are mentioned. All proofs are attached in the appendix.

###  4.1 Set-Based Abstractions: The Case of Union

As a first and very basic abstraction we study $\bigcup C$ of any set
$C\in\mathbf{2}^{\mathbb{U}}$ of databases. If $C$ is infinite, $\bigcup C$ is
infinite as well, meaning that $\bigcup C$ is captured in $\mathbb{I}$.
Henceforth, we facilitate $\bigcup C$ via the abstraction function
$\alpha_{1}:\mathbf{2}^{\mathbb{U}}\to\mathbb{I}$ with $\alpha_{1}(C)$.

$\displaystyle\alpha_{1}(C):=\bigcup C$
$\displaystyle\gamma_{1}(\mathcal{I}):=\\{\mathcal{D}\subseteq\mathcal{I}\mid\text{$\mathcal{D}$
is a database}\\}$ (3)

The natural choice for the abstract domain is, thus, $(\mathbb{I},\subseteq)$
because the more databases $C$ contains, the bigger the abstract instance is
(cf. Def. 6 item 1). The counterpart concretization function
$\gamma_{1}:\mathbb{I}\to\mathbf{2}^{\mathbb{U}}$ is determined by
$\alpha_{1}$: While $\alpha_{1}$ forms the union of all databases contained in
a set of databases $C$, an abstract instance then describes all databases that
are (finite) subsets of the abstract instance. $\gamma_{1}(\mathcal{I})$ is
defined in (3).

Databases are finite by definition, implying that if $\mathcal{I}$ is
infinite, $\mathcal{D}\subsetneq\mathcal{I}$ for every
$\mathcal{D}\in\gamma_{1}(\mathcal{I})$. The functions in (3) make up for a
Galois connection.

###### Proposition 3

$(\alpha_{1},\gamma_{1})$ is a Galois connection.

For $C\in\mathbf{2}^{\mathbb{U}}$, we are interested in the behavioral
properties of the abstraction $\alpha_{1}(C)$. Therefore, observe that for
every database $\mathcal{D}\in C$, $\mathcal{D}\subseteq\alpha_{1}(C)$. Thus,
guards asking for the absence of atoms will have the same matches on all the
databases in $C$ as well as the abstraction $\alpha_{1}(C)$.

###### Example 5

We analyze two guards $g_{nf}$ (absence of a friendship) and $g_{sf}$
(presence of a symmetric friendship) from example 1 on $C$ and $\mathcal{I}$
with $C=\\{\\{P(\text{A}),$
$P(\text{B}),F(\text{A},\text{B}),F(\text{B},\text{A})\\},\\{P(\text{A}),P(\text{B}),P(\text{C})\\}\\}$
and $\mathcal{I}=\bigcup C=\\{P(\text{A}),P(\text{B}),$
$P(\text{C}),F(\text{A},\text{B}),F(\text{B},\text{A})\\}$. If a friendship is
absent in each database of $C$, this friendship is also absence in
$\mathcal{I}$ (i.e., the union of all databases of $C$). If a friendship is
absent in $\mathcal{I}$ this friendship is also absent in each database of
$C$. In contrast, the presence of a symmetric friendship like
$F(\text{A},\text{B}),F(\text{B},\text{A})$ holds for $\mathcal{I}$ but not
for each database in $C$.

The guard $g_{nf}=\forall y.\neg F(x,y)$ ensures the absence of all
friendships of a person $x$ through the universal quantifier. $g_{nf}$ behaves
similar to $g_{nf}$. The behavior of the existential quantifier is conversely.
For instance, $g_{ex}=\exists x.\neg P(x)$ holds for each database as
databases are finite but the set of all constants is infinite. In contrast, if
set $C$ is infinite and for each constant $c$, $P(c)$ is contained in some
database in $C$, $\mathcal{I}=\bigcup C$ does not satisfy $g_{ex}$.

As the examples show, $\alpha_{1}(C)$ may enable DMS actions with conjunctive
guards that are not enabled by some, or any, of the concrete databases in $C$.
Thus, $\alpha_{1}(C)$ captures the behavior of all databases in $C$ if we
choose CNA guards.

###### Theorem 4.1

$(\alpha_{1},\gamma_{1})$ is an abstract interpretation w.r.t. CNA guards.

Similarly, we obtain an abstraction framework based on intersection of all the
databases contained in set $C$ of concrete databases.

###### Theorem 4.2

Galois connection $(\alpha_{2},\gamma_{2})$ with $\alpha_{2}(C):=\bigcap C$
and
$\gamma_{2}(\mathcal{I}):=\\{\mathcal{D}\in\mathbb{U}\mid\mathcal{I}\subseteq\mathcal{D}\\}$
is an abstract interpretation for pf-CGs.

This is a special case of Theorem 4.4 (cf. next subsection). Furthermore,
combining both former abstractions allows us to cover projection-free normal
conjunctive guards in DMS actions. The rationale behind this abstraction is
that for an NCG $g$, $g^{+}$ is evaluated on the intersection component while
$g^{-}$ is simultaneaously evaluated on the union component of the
abstraction.

###### Theorem 4.3

For $\alpha_{3}(C):=(\alpha_{1}(C),\alpha_{2}(C))$ and
$\gamma_{3}((\mathcal{I}^{\cup},\mathcal{I}^{\cap})):=\\{\mathcal{D}\in\mathbb{U}\mid\mathcal{I}^{\cap}\subseteq\mathcal{D}\subseteq\mathcal{I}^{\cup}\\}$,
Galois connection $(\alpha_{3},\gamma_{3})$ is an abstract interpretation for
pf-NCGs.

Next, we consider abstractions allowing for projections (i.e., existentially
quantified variables in DMS action guards) to fully capture NCGs in DMS
actions.

###  4.2 Abstractions with Labeled Nulls: The Case of Intersection

There are two issues with the abstractions discussed so far: (a) limited
expressiveness in guards of DMS actions (no existential quantification) and
(b) (still) infinite branching of abstract states. The reason for the latter
is that abstract instances resemble their concrete counterparts too
explicitly. To resolve both issues we use the well-known _labeled null_
abstraction to get a notion of existence of values contained in a database
whose exact values are irrelevant. Finite branching is a welcome side-effect
of this abstraction as well as a precise abstraction for DMSs using CGs
(including projection via existential quantification).

_Labeled nulls_ are introduced in our framework as a countably infinite set
$\mathbf{N}$ (disjoint from all other term sets). As labeled nulls are proxies
for the existence of values (i.e., constants), a database, in which every
occurrence of a null is replaced by a constant (or other null), is certainly
related to the instance that uses the null. Let us denote the set of all
instances using constants and labeled nulls by $\mathbb{I}^{\mathbf{N}}$
(short for $\mathbb{I}^{\mathbf{C}\cup\mathbf{N}}_{\mathbf{P}}$). The notions
of homomorphisms and guard matches naturally extend to databases containing
nulls (i.e., constants must still map to constants, but nulls may map to nulls
or constants).

Due to the nature of labeled nulls, their identity does not have the same role
as constants have. It is natural to consider $\mathbb{I}^{\mathbf{N}}$ closed
under equivalence up to homomorphisms. This means, instances
$\mathcal{I},\mathcal{J}\in\mathbb{I}^{\mathbf{N}}$ are equal, denoted
$\mathcal{I}\mathbin{\leftrightarrows}\mathcal{J}$, if
$\mathcal{I}\to\mathcal{J}$ and $\mathcal{J}\to\mathcal{I}$. Note, on
$\mathbb{U}$ equivalence up to homomorphisms coincides with set equality. For
instance
$\\{P(\text{A})\\}\leftrightarrows\\{P(\text{A}),P(\mathbf{n}_{0})\\}$ because
we can map $A$ on $A$ and $\mathbf{n}_{0}$ on $A$.
$\\{F(\mathbf{n}_{0},\mathbf{n}_{1})\\}\to\\{F(\mathbf{n}_{0},\mathbf{n}_{0})\\}$
but
$\\{F(\mathbf{n}_{0},\mathbf{n}_{0})\\}\not\to\\{F(\mathbf{n}_{0},\mathbf{n}_{1})\\}$
because we can not map $\mathbf{n}_{0}$ on $\mathbf{n}_{0}$ and
$\mathbf{n}_{0}$ on $\mathbf{n}_{1}$.

$(\mathbb{I}^{\mathbf{N}},\to)$ forms a lattice and, by duality,
$(\mathbb{I}^{\mathbf{N}},\leftarrow)$, too. The join $\sqcup$ of
$(\mathbb{I}^{\mathbf{N}},\to)$ is simply the union of the instances.
Conversely, $\sqcap$ is an intersection of two instances generalizing common
atoms with different constants via null assertions. For instance,
$\mathcal{I}=\\{P(\text{A}),P(\text{B}),F(\mathbf{n}_{0},\mathbf{n}_{1})\\}$
and $\mathcal{J}=\\{P(\text{A}),P(\text{C}),F(\text{A},\text{C})\\}$ have
$\mathcal{I}\sqcup\mathcal{J}=\\{P(\text{A}),P(\text{B}),P(\text{C}),F(\mathbf{n}_{0},\mathbf{n}_{1}),$
$F(\text{A},\text{C})\\}$ as least upper bound and the greatest lower bound is
$\mathcal{I}\sqcap\mathcal{J}=\\{P(\text{A}),F(\mathbf{n}_{0},\mathbf{n}_{1})\\}$.

The next two definitions describe how an action is performed in
$(\mathbb{I}^{\mathbf{N}},\to)$. Let $\mathcal{I}$ be an instance and
$\textit{act}=(g,\tt Del,\tt Add)$ a DMS action. Instead of extending guard
matches $\sigma$ to $\sigma^{\star}$ (involving some constants that are added
to the instance through variables in $\tt Add$), we consider extensions of
$\sigma$ that insert (globally) fresh labeled nulls for all variables in
$\textit{vars}(\tt Add)\setminus\textit{free}(g)$.

###### Definition 8

Let $\textit{act}=(g,\tt Del,\tt Add)$ be a DMS action. For abstract instance
$\mathcal{I}\in\mathbb{I}^{\mathbf{N}}$, if $\sigma\in g(\mathcal{I})$, then
$\mathcal{I}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}(\mathcal{I}\setminus\tt
Del\sigma^{\star})\cup\tt Add\sigma^{\star}$ where
$\sigma\subseteq\sigma^{\star}$ and for each variable $x\in\textit{vars}(\tt
Add)\setminus\textit{free}(g)$, $\sigma^{\star}(x)$ is a fresh labeled null.

###### Example 6

For action $\textit{act}_{\textit{add}}=(\textit{true},\emptyset,\\{P(x)\\})$
from example 2, $\textit{vars}(\tt
Add)\setminus\textit{free}(g)=\\{\mathit{x}\\}\setminus\emptyset=\\{\mathit{x}\\}$
and $\sigma^{\star}(x)=\mathbf{n}$. We obtain $\emptyset\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act}_{\textit{add}},\emptyset\rangle}}\\{P(\mathbf{n})\\}$.

Note that the action label only contains the match $\sigma$ and not its
extension. The reason is that for instances
$\mathcal{I},\mathcal{B}_{1},\mathcal{B}_{2}$ and action-match pair
$\langle\textit{act},\sigma\rangle$, if $\mathcal{I}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{B}_{1}$ and
$\mathcal{I}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{B}_{2}$,
then $\mathcal{B}_{1}\leftrightarrows\mathcal{B}_{2}$. Thus, the different
target instances cannot be distinguished in our abstract domain. This notion
of steps is similar to what the Chase does in existential rule reasoning [13].
Due to the closure of the domain under homomorphisms, it also resembles the
standard chase and the core chase to certain extents [12]. Sets of concrete
instances still proceed as originally defined in Sect. 2. To still guarantee a
resemblance between the action labels in our abstract domain and the labels
used for concrete instances (where no nulls are involved), we introduce a
notion of _compatibility_ of action labels.

###### Definition 9

Action label $\langle\textit{act}_{1},\sigma_{1}\rangle$ is _compatible to_
action label $\langle\textit{act}_{2},\sigma_{2}\rangle$, denoted by
$\langle\textit{act}_{1},\sigma_{1}\rangle\trianglelefteq\langle\textit{act}_{2},\sigma_{2}\rangle$,
if $\textit{act}_{1}=\textit{act}_{2}$ and $\sigma_{1}\subseteq\sigma_{2}$.

Note that we could have reduced the action labeling to include only the guard
matches for concrete instances already. However, this simplification does not
make the branching finite. Even worse, the resulting LTS would become
nondeterministic and looses image-finiteness at the same time.

As before, the abstraction mechanisms we study are based on greatest lower
bounds and least upper bounds of the abstract domain
$(\mathbb{I}^{\mathbf{N}},\to)$. Next, we study the intersection abstraction
of $C\in\mathbf{2}^{\mathbb{U}}$ with $\alpha_{4}(C)$ in (4). Generalizing
from $(\mathbb{I},\supseteq)$ we get $(\mathbb{I}^{\mathbf{N}},\leftarrow)$ as
the less databases $C$ contains, the bigger the abstract instance becomes (cf.
Def. 6 item 1). Conversely, $\gamma_{4}(\mathcal{I})$ in (4) for abstract
instance $\mathcal{I}\in\mathbb{I}^{\mathbf{N}}$.

$\displaystyle\alpha_{4}(C):=\bigsqcap C$
$\displaystyle\gamma_{4}(\mathcal{I}):=\\{\mathcal{D}\in\mathbb{U}\mid\mathcal{I}\to\mathcal{D}\\}\\}$
(4)

###### Proposition 4

$(\alpha_{4},\gamma_{4})$ is a Galois connection.

Using labeled nulls, abstract DMSs using CGs become precise abstractions of
their concrete counterparts.

###### Example 7

We analyze the guard $g_{af}$ (does there exist a friendship from $x$ to
someone) from example 1 on
$C=\\{\\{P(\text{A}),P(\text{B}),F(\text{A},\text{B})\\},\\{P(\text{A}),P(\text{C}),$
$F(\text{A},\text{C})\\}\\}$ and $\mathcal{I}=\bigsqcap
C=\\{P(\text{A}),F(\text{A},\mathbf{n}_{1})\\}$. In contrast to
$\mathcal{I}^{\prime}=\bigcap C=\\{P(\text{A})\\}$, we have a friendship with
nulls in $\mathcal{I}$. Now we get homomorphisms
$h_{\mathcal{I}}:g_{af}\to\mathcal{I}$ and
$h_{\mathcal{D}}:g_{af}\to\mathcal{D}$ for each $\mathcal{D}\in C$.

###### Theorem 4.4

$(\alpha_{4},\gamma_{4})$ is an abstract interpretation for CGs.

Generalizing the Galois connection $(\alpha_{1},\gamma_{1})$ to
$\mathbb{I}^{\mathbf{N}}$ yields $(\alpha_{5},\gamma_{5})$ with
$\alpha_{5}=\alpha_{1}$ and
$\gamma_{5}(\mathcal{A}):=\\{\mathcal{D}\in\mathbb{U}^{\mathbf{N}}\mid\mathcal{D}\to\mathcal{A}\\}$.
As for all databases $\mathcal{D}$ without labeled nulls, the existence of a
homomorphism from $\mathcal{D}$ to $\mathcal{A}$ holds if, and only if,
$\mathcal{D}\subseteq\mathcal{A}$, the new domain generalizes the original
result (i.e., Theorem 4.1) slightly, but without further impact. After all,
labeled nulls are proxies for the existence of constants, whereas CNA guards
account for the absence of atoms.

###### Theorem 4.5

Galois connection $(\alpha_{5},\gamma_{5})$ with $\alpha_{5}(C):=\bigsqcup C$
and
$\gamma_{5}(\mathcal{I}):=\\{\mathcal{D}\in\mathbb{U}\mid\mathcal{D}\to\mathcal{I}\\}$
is an abstract interpretation for CNAs.

###  4.3 Combining Unions and Intersections

Although the former abstractions already capture existentially quantified
variables (i.e., projections), they do not jointly support projections as well
as negation. A corresponding abstraction capturing both is
$\alpha_{6}:\mathbf{2}^{\mathbb{U}}\to\mathbb{I}^{\mathbf{N}}\times\mathbb{I}^{\mathbf{N}}$
with respective concretization
$\gamma_{6}:\mathbb{I}^{\mathbf{N}}\times\mathbb{I}^{\mathbf{N}}\to\mathbf{2}^{\mathbb{U}}$
as defined in (5). The abstract domain is
$(\mathbb{I}^{\mathbf{N}}\times\mathbb{I}^{\mathbf{N}},\preceq)$.
$\mathcal{I}_{1}\preceq\mathcal{I}_{2}$ is defined as
$(\mathcal{I}^{\sqcap}_{1},\mathcal{I}^{\sqcup}_{1})\preceq(\mathcal{I}^{\sqcap}_{2},\mathcal{I}^{\sqcup}_{2})$
if and only if $\mathcal{I}^{\sqcap}_{1}\leftarrow\mathcal{I}^{\sqcap}_{2}$
and $\mathcal{I}^{\sqcup}_{1}\to\mathcal{I}^{\sqcup}_{2}$. The lattice
$(\mathbb{I}^{\mathbf{N}}\times\mathbb{I}^{\mathbf{N}},\preceq)$ is a
combination of the two lattices $(\mathbb{I}^{\mathbf{N}},\leftarrow)$ and
$(\mathbb{I}^{\mathbf{N}},\to)$.

$\displaystyle\alpha_{6}(C):=(\bigsqcap C,\bigsqcup C)$
$\displaystyle\gamma_{6}(\mathcal{I}):=\\{\mathcal{I}^{\sqcap}\to\mathcal{D}\to\mathcal{I}^{\sqcup}\\}$
(5)

###### Proposition 5

$(\alpha_{6},\gamma_{6})$ is a Galois connection.

A substitution $\sigma$ holds for a NCG $g$ and an abstract state
$\mathcal{I}=(\mathcal{I}^{\sqcap},\mathcal{I}^{\sqcup})$ if the following
holds: $\sigma\in g(\mathcal{I})$ if $\sigma\in g^{+}(\mathcal{I}^{\sqcap})$
and $\sigma\in g^{-}(\mathcal{I}^{\sqcup})$.

###### Theorem 4.6

$(\alpha_{6},\gamma_{6})$ is an abstract interpretation for NCG.

###### Example 8

With Galois connection $(\alpha_{6},\gamma_{6})$ the guard $g_{end}:=\exists
x,y,z.F(x,y)$ $\wedge F(y,z)\wedge F(z,x)\wedge\neg P(x,y)\wedge\neg
P(y,z)\wedge\neg P(z,x)$ from action $\textit{act}_{end}$ (example 4) holds in
the abstract and concrete domain.

##  5 Related Work

Reasoning about Database-Manipulating Processes. Most recent works consider
formal process languages for manipulating relational database in the context
of business process modeling [6].

_Data manipulating systems_ (DMS) as considered in this paper are based on
Abdullah et al. [1]. The authors use the formalism to study boundaries of
decidability of (generally undecidable) reachability of state predicates in
DMS processes. Their approach employs a formal semantics of DMS processes
based on Petri nets and counter machines in combination with multiset-based
abstraction of databases. Thereupon, Abdullah et al. impose bounds on database
schemas as well as query evaluation to obtain decidable fragments. Calvanese
et al. [7] also consider a DMS-like language for which they define an _LTS-
based operational semantics_ to support CTL model-checking of such systems.
Similar to Abdullah et al., bounds are imposed on the generally infinite state
space to enable an effective, yet incomplete model-checking procedure.

Cangialosi et al. [8, 11] consider a DMS-like formalism called artifact-
centric (service) language to verify process properties expressed in the
$\mu$-calculus. To obtain an effective verification procedure, the authors
employ, in accordance to our framework, homomorphism equivalence as
abstraction and restrict the process language to conjunctive queries,
respectively. Bagheri et al. [4] extend the work of Cangialosi et al. by
supporting negation within first-order queries serving as preconditions
(guards) of transitions. As a consequence, processes must be restricted to be
weakly acyclic in order to ensure a finite solution.

Other works use _Petri nets_ with data (colored Petri nets) as a DMS-like
formalism. Montali et al. [22] propose DB-nets to integrate data- and process-
related aspects of business processes. In [21], Montali et al. adopt soundness
checks (including reachability) known from workflow nets to DB-nets, where a
finite solution is ensured by employing different notions of boundedness. This
work work has recently been extended by Ghilardi et al. [14, 15] to support
conjunctive queries with atomic negation and existential quantifiers.

To summarize, most works impose bounds on the state space and/or restrictions
of guard/query languages to ensure effective reasoning about semantic
properties of DMS-like processes. However, to the best of our knowledge, none
of these works provide a comprehensive decomposition hierarchy of guard/query
expressions together with a precise characterization of corresponding
semantic-preserving abstractions.

Abstraction Techniques for Databases. Halder et al. [16, 17] apply principles
of _abstract interpretation_ in a more practical setting to define fine-
grained abstractions for SQL query expressions. For approximating query result
sets, query- and database-specific lattice-based abstractions are applied to
value ranges of attribute constraints in selection conditions. In other works,
abstract interpretation is mostly used to formalize the interface between
database languages and programming languages. Baily et al. [5] apply abstract
interpretation for termination analysis for a functional programming language
performing database manipulations. Similar attempts are proposed by Amato et
al. [3] and Toman et al. [25] to reason about the interplay between imperative
programming and database manipulating operations. However, using abstract
interpretation to characterize an implementation-independent hierarchy of
database abstractions as proposed in this paper has not yet been considered.

Besides abstract interpretation, _symbolic execution_ techniques are also
frequently considered to effectively cope with large/infinite state spaces of
database systems. In these approaches, sets of databases instances are
symbolically represented using logical constraints, where most recent works
employ this approach for test-data generation from/for databases [23, 20, 18,
19]. In contrast, elaborating a hierarchy of _symbolic_ abstractions using
different fragments of propositional logics similar to our approach, has not
been investigated so far.

##  6 Conclusion

We proposed a hierarchy of abstract domains for representing (possibly
infinite) sets of databases instances in a final way based on the principles
of abstract interpretation. The resulting hierarchy is semantic-preserving up-
to bisimilarity and is shaped by different fragments of first-order logics
serving as guard language of database-manipulating processes. As a future
work, our framework can be instantiated in different ways to facilitate DMS
model-checking (e.g., considering corresponding fragments of the modal
$\mu$-calculus as specification language). To this end, a purely abstract step
semantics is to be defined which allows us to explore the abstract LTS (e.g.,
starting from all possible initial database instances). We further plan to
enrich DMS by a formal process language like Petri nets and CCS to investigate
effects as induced by constructs like guarded choice and concurrent actions.

#### Acknowledgements.

Stephan Mennicke is partly supported by DFG (German Research Foundation) in
project 389792660 (TRR 248, CPEC), by the BMBF (Federal Ministry of Education
and Research) under project 13GW0552B (KIMEDS), in the Center for Scalable
Data Analytics and Artificial Intelligence (ScaDS.AI), and by BMBF and DAAD
(German Academic Exchange Service) in project 57616814 (SECAI, School of
Embedded and Composite AI).

## References

  * [1] Abdulla, P.A., Aiswarya, C., Atig, M.F., Montali, M., Rezine, O.: Complexity of reachability for data-aware dynamic systems. In: ACSD. pp. 11–20. IEEE (2018)
  * [2] Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases, vol. 8. Addison-Wesley (1995)
  * [3] Amato, G., Giannotti, F., Mainetto, G.: Data sharing analysis for a database programming language via abstract interpretation. In: VLDB. pp. 405–415 (1993)
  * [4] Bagheri Hariri, B., Calvanese, D., De Giacomo, G., De Masellis, R., Felli, P.: Foundations of relational artifacts verification. In: BPM. pp. 379–395. Springer (2011)
  * [5] Bailey, J., Poulovassilis, A.: Abstract interpretation for termination analysis in functional active databases. J. IIS 12, 243–273 (1999)
  * [6] Calvanese, D., De Giacomo, G., Montali, M.: Foundations of data-aware process analysis: A database theory perspective. In: PODS. pp. 1–12. ACM (2013)
  * [7] Calvanese, D., Montali, M., Patrizi, F., Rivkin, A.: Implementing data-centric dynamic systems over a relational dbms. In: FDM. vol. 1378, pp. 209–212. CEUR-WS (2015)
  * [8] Cangialosi, P., De Giacomo, G., De Masellis, R., Rosati, R.: Conjunctive artifact-centric services. In: ICSOC. pp. 318–333. Springer (2010)
  * [9] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. p. 238–252. ACM (1977)
  * [10] Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. TOPLAS 19(2), 253–291 (1997)
  * [11] De Giacomo, G., De Masellis, R., Rosati, R.: Verification of conjunctive artifact-centric services. Intl. J. of CIS 21(02), 111–139 (2012)
  * [12] Deutsch, A., Nash, A., Remmel, J.: The chase revisited. In: PODS. pp. 149–158. ACM (2008)
  * [13] Fagin, R., Kolaitis, P.G., Miller, R.J., Popa, L.: Data exchange: Semantics and query answering. TCS 336(1), 89–124 (2005)
  * [14] Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri nets with parameterised data: Modelling and verification. In: BPM. pp. 55–74. Springer (2020)
  * [15] Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri net-based object-centric processes with read-only data. IS 107, 102011 (2022)
  * [16] Halder, R., Cortesi, A.: Abstract interpretation for sound approximation of database query languages. In: INFOS. pp. 1–10. IEEE (2010)
  * [17] Halder, R., Cortesi, A.: Abstract interpretation of database query languages. CLSS 38(2), 123–157 (2012)
  * [18] Li, C., Csallner, C.: Dynamic symbolic database application testing. In: DBTest (2010)
  * [19] Lo, E., Cheng, N., Hon, W.K.: Generating databases for query workloads. VLDB Endowment 3(1-2), 848–859 (2010)
  * [20] Marcozzi, M., Vanhoof, W., Hainaut, J.L.: A relational symbolic execution algorithm for constraint-based testing of database programs. In: SCAM. pp. 179–188. IEEE (2013)
  * [21] Montali, M., Rivkin, A.: Model checking petri nets with names using data-centric dynamic systems. FAOC 28(4), 615–641 (2016)
  * [22] Montali, M., Rivkin, A.: Db-nets: On the marriage of colored petri nets and relational databases. TOPNOC pp. 91–118 (2017)
  * [23] Pan, K., Wu, X., Xie, T.: Database state generation via dynamic symbolic execution for coverage criteria. In: DBtest. pp. 1–6 (2011)
  * [24] Schüler, T., Mennicke, S., Lochau, M.: Abstract domains for database manipulating processes (2023)
  * [25] Toman, D.: Constraint databases and program analysis using abstract interpretation. In: CDB. pp. 246–262. Springer (1997)

##  Appendix 0.A Domains are Lattices

We start by noticing that we have seven different domains, all of which are
bounded lattices:

  1. (1)

$(\mathbf{2}^{\mathbb{U}},\subseteq)$: the domain of concrete instances;

  2. (2)

$(\mathbb{I},\subseteq)$;

  3. (3)

$(\mathbb{I},\supseteq)$;

  4. (4)

$(\mathbb{I}\times\mathbb{I},\preceq)$;

  5. (5)

$(\mathbb{I}^{\mathbf{N}},\to)$;

  6. (6)

$(\mathbb{I}^{\mathbf{N}},\leftarrow)$;

  7. (7)

$(\mathbb{I}^{\mathbf{N}}\times\mathbb{I},\preceq)$;

###### Proposition 6

$(\mathbf{2}^{\mathbb{U}},\subseteq)$ is a complete, thus, bounded lattice.

###### Proof

Every powerset domain is a bounded lattice with infimum
$\mathcal{D}\cap\mathcal{D}^{\prime}$, supremum
$\mathcal{D}\cup\mathcal{D}^{\prime}$,
$\top=\mathbb{U}=\bigcup_{\mathcal{D}\in\mathbb{U}}\mathcal{D}$ and
$\bot=\emptyset=\bigcap_{\mathcal{D}\in\mathbb{U}}\mathcal{D}$. Furthermore,
it is a complete lattice, meaning that for every subset $X$ of
$\mathbf{2}^{\mathbb{U}}$, greatest lower bound (i.e.,
$\bigcap_{\mathcal{D}\in X}\mathcal{D}$) and least upper bound (i.e.,
$\bigcup_{\mathcal{D}\in X}\mathcal{D}$) exist and are unique.∎

###### Proposition 7

$(\mathbb{I}^{\mathbf{N}},\to)$ is a complete lattice.

###### Proof

Without loss of generality, we assume that instances $\mathcal{I}$ and
$\mathcal{J}$, if any, use distinct nulls.

Supremum:

For $\mathcal{I},\mathcal{J}\in\mathbb{I}^{\mathbf{N}}$, we get the unique
least upper bound $\mathcal{I}\sqcup\mathcal{J}$ by
$\mathcal{I}\cup\mathcal{J}$. Let $\mathcal{U}$ be any other upper bound. Then
there are homomorphisms $h_{1}:\mathcal{I}\to\mathcal{U}$ and
$h_{2}:\mathcal{J}\to\mathcal{U}$, so that $h_{1}\cup h_{2}$ is a homomorphism
$\mathcal{I}\sqcup\mathcal{J}\to\mathcal{U}$.

Infimum:

For $\mathcal{I},\mathcal{J}\in\mathbb{I}^{\mathbf{N}}$, we find that
$\mathcal{I}\cap\mathcal{J}$ is a lower bound of $\mathcal{I}$ and
$\mathcal{J}$. (the respective homomorphism is the identity on
$\mathcal{I}\cap\mathcal{J}$). It remains to be shown that there is a greatest
lower bound of $\mathcal{I}$ and $\mathcal{J}$, denoted
$\mathcal{I}\sqcap\mathcal{J}$, that is unique. To prove it, we use the
observation that if $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ are lower bounds
of $\mathcal{I}$ and $\mathcal{J}$, then
$\mathcal{L}_{1}\sqcup\mathcal{L}_{2}$ is also a lower bound. In that case,
$\mathcal{L}_{1}\sqcup\mathcal{L}_{2}$ is a lower bound greater than
$\mathcal{L}_{1}$ and $\mathcal{L}_{2}$. If $\mathcal{L}_{1}$ and
$\mathcal{L}_{2}$ are distinct greatest lower bounds, then
$\mathcal{L}_{1}\sqcup\mathcal{L}_{2}$ is a lower bound greater than
$\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, contradicting the assumption that
$\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ are greatest lower bounds. Hence, such
a pair of distinct greatest lower bounds $\mathcal{L}_{1}$ and
$\mathcal{L}_{2}$ must not exist, implying there is a unique greatest lower
bound.

For the remainder of the proof, let us assume that $\mathcal{L}_{1}$ and
$\mathcal{L}_{2}$ use distinct labeled nulls. As $\mathcal{L}_{1}$ and
$\mathcal{L}_{2}$ are lower bounds of $\mathcal{I}$ and $\mathcal{J}$, there
are homomorphisms $h_{1}^{X}:\mathcal{L}_{1}\to X$ and
$h_{2}^{X}:\mathcal{L}_{2}\to X$ for $X\in\\{\mathcal{I},\mathcal{J}\\}$. Then
$h_{1}^{X}\cup h_{2}^{X}$ is a homomorphism certifying for
$\mathcal{L}_{1}\sqcup\mathcal{L}_{2}\to X$, showing that
$\mathcal{L}_{1}\sqcup\mathcal{L}_{2}$ is actually a lower bound of
$\mathcal{I}$ and $\mathcal{J}$.

Completeness:

Let $\mathcal{X}\subseteq\mathbb{I}^{\mathbf{N}}$. Least upper bound
$\bigsqcup\mathcal{X}=\bigcup\mathcal{X}$ is defined and is unique. For the
greatest lower bound $\bigsqcap\mathcal{X}$, we get uniqueness by following
similar arguments as in the binary case.

Thus, we get
$\bigsqcup_{\mathcal{I}\in\mathbb{I}^{\mathbf{N}}}\mathcal{I}=\bigcup_{\mathcal{I}\in\mathbb{I}^{\mathbf{N}}}\mathcal{I}=\mathbb{I}^{\mathbf{N}}$
as $\top$ and
$\bigsqcap_{\mathcal{I}\in\mathbb{I}^{\mathbf{N}}}\mathcal{I}=\emptyset$ as
$\bot$. Note that
$\bigcap_{\mathcal{I}\in\mathbb{I}^{\mathbf{N}}}\mathcal{I}\subseteq\bigsqcap_{\mathcal{I}\in\mathbb{I}^{\mathbf{N}}}\mathcal{I}$,
thus $\bot=\emptyset$.∎

###### Corollary 1

(1) $(\mathbb{I}^{\mathbf{N}},\leftarrow)$, (2) $(\mathbb{I},\subseteq)$, and
(3) $(\mathbb{I},\supseteq)$ are complete lattices.

###### Proof

  1. (1)

Follows from duality of Proposition 7.

  2. (2)

Follows as a special case of Proposition 7. Therefore note,
$\mathbb{I}\subsetneq\mathbb{I}^{\mathbf{N}}$ and for each
$\mathcal{I},\mathcal{J}\in\mathbb{I}$, we get
$\mathcal{I}\subseteq\mathcal{J}$ if, and only if,
$\mathcal{I}\to\mathcal{J}$.

  3. (3)

Follows as a special case of (1) (cf. proof of (2)) or by duality of (2).∎

###### Lemma 1

If $(A,\leq_{A})$ and $(B,\leq_{B})$ are complete lattices, then so is
$(A\times B,\preceq)$ with for $(a_{1},b_{1}),(a_{2},b_{2})\in A\times B$, we
get $(a_{1},b_{1})\preceq(a_{2},b_{2})$ if, and only if, $a_{1}\leq_{A}a_{2}$
and $b_{1}\leq_{B}b_{2}$.

###### Proof

As $(A,\leq_{A})$ and $(B,\leq_{B})$ are complete lattices, every subset $X$
of $A$ (or $B$, resp.) has an infimum $\sqcap_{A}X$ ($\sqcap_{B}X$, resp.) and
a supremum $\sqcap_{A}X$ ($\sqcap_{B}X$, resp.). Then for
$(a_{1},b_{1}),(a_{2},b_{2})\in A\times B$,
$(a_{1}\sqcap_{A}a_{2},b_{1}\sqcap_{B}b_{2})$ is the infimum
$(a_{1},b_{1})\sqcap(a_{2},b_{2})$: If $(a_{3},b_{3})\in A\times B$ is a lower
bound of $(a_{1},b_{1})$ and $(a_{2},b_{2})$, then $a_{3}$ is a lower bound
$a_{1}$ and $a_{2}$, and $b_{3}$ is a lower bound of $b_{1}$ and $b_{2}$ (by
definition of $\preceq$). Hence, $a_{3}\leq_{A}a_{1}\sqcap_{A}a_{2}$ and
$b_{3}\leq_{B}b_{1}\sqcap_{B}b_{2}$ since $(A,\leq_{A})$ and $(B,\leq_{B})$
are complete lattices. This means,
$(a_{3},b_{3})\preceq(a_{1},b_{1})\sqcap(a_{2},b_{2})$ (again by definition of
$\preceq$). A similar line of arguments can be taken for the supremum
$(a_{1},b_{1})\sqcup(a_{2},b_{2})$.

The bounds of the lattice are $(\top_{A},\top_{B})=\top$ and
$(\bot_{A},\bot_{B})=\bot$. For every subset $Y$ of $A\times B$, let
$Y_{A}:=\\{a\mid(a,b)\in Y\\}$ and $Y_{B}:=\\{b\mid(a,b)\in Y\\}$. Then we
obtain the infimum of $Y$ by $\bigsqcap
Y:=(\bigsqcap_{A}Y_{A},\bigsqcap_{B}Y_{B})$ and the supremum by $\bigsqcup
Y:=(\bigsqcup_{A}Y_{A},\bigsqcup_{B}Y_{B})$, all justified by the fact that
the input lattices are complete.∎

###### Corollary 2

$(\mathbb{I}\times\mathbb{I},\preceq)$ and
$(\mathbb{I}^{\mathbf{N}}\times\mathbb{I}^{\mathbf{N}},\preceq)$ are complete
lattices.

###### Proof

Follows from Lemma 1 together with Proposition 7 and Corollary 1.∎

##  Appendix 0.B Galois Connections

Instead of proving Propositions 3–5, showing that $(\alpha_{1},\gamma_{1})$,
…, $(\alpha_{6},\gamma_{6})$ are Galois connections, we extract the common
principle from these connections into the following theorem.

###### Theorem 0.B.1

Let $(\mathbb{A},\sqsubseteq)$ be an abstract domain, such that
$\mathbb{U}\subseteq\mathbb{A}$ and $(\mathbf{2}^{\mathbb{U}},\subseteq)$ a
concrete domain, both complete lattices. Then functions
$\alpha:\mathbf{2}^{\mathbb{U}}\to\mathbb{A}$ with $\alpha(C):=\bigsqcup C$
and $\gamma:\mathbb{A}\to\mathbf{2}^{\mathbb{U}}$ with
$\gamma(\mathcal{A})=\\{\mathcal{D}\mid\mathcal{D}\in\mathbb{U}\wedge\mathcal{D}\sqsubseteq\mathcal{A}\\}$
form a Galois connection $(\alpha,\gamma)$.

###### Proof

We need to show that $(\alpha,\gamma)$ satisfies the three properties of a
Galois connection (cf. Definition 6).

Totality/Monotonicity:

Since $(\mathbb{A},\sqsubseteq)$ is a complete lattice, $\alpha$ is total as
it uses the abstract least upper bound of a set of databases, given as input.
Also, $\gamma$ is total since, in the worst case,
$\gamma(\mathcal{A})=\emptyset$ if there is not database being smaller than
$\mathcal{A}$ up to $\sqsubseteq$.

Concretization Preservation:

We need to show that for any $C\in\mathbf{2}^{\mathbb{U}}$,
$C\subseteq\gamma\circ\alpha(C)$. As $\alpha(C)$ is the (abstract) least upper
bound of all the databases in $C$, we get $\mathcal{D}\sqsubseteq\alpha(C)$
for $\mathcal{D}\in C$. Since $\gamma(\alpha(C))$ is the set of all databases
smaller than $\alpha(C)$, we have that $C\subseteq\gamma(\alpha(C))$.

Abstraction Optimality:

We need to show that for any $\mathcal{A}\in\mathbb{A}$,
$\alpha\circ\gamma(\mathcal{A})\sqsubseteq\mathcal{A}$. $\gamma(\mathcal{A})$
is the set of all databases (abstractly) smaller than $\mathcal{A}$. Thus,
$\mathcal{A}$ is an upper bound of $\gamma(\mathcal{A})$. Since
$\alpha(\gamma(\mathcal{A}))$ produces the least upper bound of
$\gamma(\mathcal{A})$, the result follows.∎

Propositions 3–5 follow as corollaries.

##  Appendix 0.C Bisimilarity

###  0.C.1 Proof of Theorem 4.1

The Galois connection we are about to prove to be an abstract interpretation
framework is $(\alpha_{1},\gamma_{1})$ with
$\alpha_{1}(C):=\bigcup_{\mathcal{D}\in C}\mathcal{D}$ and
$\gamma_{1}(\mathcal{A}):=\\{\mathcal{D}\in\mathbb{U}\mid\mathcal{D}\subseteq\mathcal{A}\\}$.
The guard language is CNA and we need to give a $\forall$-bisimulation.

We show that

$R:=\\{(\alpha(C),C)\mid C\in\mathbf{2}^{\mathbb{U}}\\}$

is a $\forall$-bisimulation. Let $(\mathcal{I},C)\in R$ (i.e.,
$\mathcal{I}=\alpha(C)$), $\langle\textit{act},\sigma\rangle$ be an action
such that $\textit{act}=(g,\tt Del,\tt Add)$ and $g=\forall\mathbf{y}.\ \neg
a_{1}\wedge\ldots\wedge\neg a_{m}$ ($m\in\mathbb{N}$) is a CNA.

  1. 1.

If $\mathcal{I}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{I}^{\prime}$
with $\mathcal{I}^{\prime}=(\mathcal{I}\setminus\tt Del\sigma^{\star})\cup\tt
Add\sigma^{\star}$, we need to show that $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}$ for
$C^{\prime}=\\{\mathcal{D}^{\prime}\in\mathbb{U}\mid\exists\mathcal{D}\in
C:\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}\\}$,
such that $\mathcal{D}[\textit{act},\sigma\rangle$ for all $\mathcal{D}\in C$
and $(\mathcal{I}^{\prime},C^{\prime})\in R$ (i.e.,
$\alpha_{1}(C^{\prime})=\mathcal{I}^{\prime}$).

As $\mathcal{I}[\textit{act},\sigma\rangle$, there is no function
$h:\mathbf{C}\cup\mathbf{V}\to\mathbf{C}$ such that $\sigma\subseteq h$ and
$h(g)\cap\mathcal{I}\neq\emptyset$. Let $\mathcal{D}\in C$. Suppose there is a
function $h^{\prime}$ such that $\sigma\subseteq h^{\prime}$ and
$h^{\prime}(g)\cap\mathcal{D}\neq\emptyset$. Then
$h^{\prime}(g)\cap\mathcal{I}\neq\emptyset$ as
$\mathcal{D}\subseteq\mathcal{I}$ (by $\alpha_{1}$), contradicting the
assumption that no such function exists. Thus,
$\mathcal{D}[\textit{act},\sigma\rangle$ which holds for arbitrary
$\mathcal{D}\in C$. Moreover, for every $\mathcal{D}\in C$ there is a
$\mathcal{D}^{\prime}$, such that $\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}$
and $\mathcal{D}^{\prime}=(\mathcal{D}\setminus\tt Del\sigma^{\star})\cup\tt
Add\sigma^{\star}$. The collection of all such $\mathcal{D}^{\prime}$ forms
the set $C^{\prime}$, such that $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}$.
Finally, we get

$\begin{array}[]{rcl}\alpha_{1}(C^{\prime})&=&\bigcup\\{(\mathcal{D}\setminus\tt
Del\sigma^{\star})\cup\tt Add\sigma^{\star}\mid\mathcal{D}\in C\\}\\\
&=&(\bigcup\\{\mathcal{D}\mid\mathcal{D}\in C\\}\setminus\tt
Del\sigma^{\star})\cup\tt Add\sigma^{\star}\\\ &=&(\alpha_{1}(C)\setminus\tt
Del\sigma^{\star})\cup\tt Add\sigma^{\star}\\\ &=&(\mathcal{I}\setminus\tt
Del\sigma^{\star})\cup\tt
Add\sigma^{\star}=\mathcal{I}^{\prime}\text{,}\end{array}$ (6)

proving the fact that $(\mathcal{I}^{\prime},C^{\prime})\in R$.

  2. 2.

If $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}$, then
for every $\mathcal{D}\in C$, $\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}$
such that $\mathcal{D}^{\prime}=(\mathcal{D}\setminus\tt
Del\sigma^{\star})\cup\tt Add\sigma^{\star}$ and $\mathcal{D}^{\prime}\in
C^{\prime}$. It holds that there is no function
$h:\mathbf{C}\cup\mathbf{V}\to\mathbf{C}$, such that $\sigma\subseteq h$ and
$h(g)\cap\mathcal{D}\neq\emptyset$ for every $\mathcal{D}\in C$. Suppose,
there is an $h^{\prime}$ such that $\sigma\subseteq h^{\prime}$ and
$h^{\prime}(g)\cap\mathcal{I}\neq\emptyset$. Then there is an atom $a\in
h^{\prime}(g)\cap\mathcal{I}$ that is also included in some $\mathcal{D}\in C$
(as $\mathcal{I}=\bigcup C$). Hence, $h^{\prime}(g)$ has a non-empty
intersection with that $\mathcal{D}$, contradicting the assumption that
$\mathcal{D}[\textit{act},\sigma\rangle$ for every $\mathcal{D}\in C$.
Therefore, $\mathcal{I}[\textit{act},\sigma\rangle$ and
$\mathcal{I}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}(\mathcal{I}\setminus\tt
Del\sigma^{\star})\cup\tt Add\sigma^{\star}=\mathcal{I}^{\prime}$. By the same
lines as above (cf. (6)), $\alpha_{1}(C^{\prime})=\mathcal{I}^{\prime}$
implying $(\mathcal{I}^{\prime},C^{\prime})\in R$.∎

###  0.C.2 Remark on Theorem 4.5

Note, although the abstract domain is slightly different, the abstraction
function still uses set union as abstraction mechanism. Therefore, and since
the same guard language is conjectured, the theorem directly follows for the
same reasons as given in the proof of Theorem 4.1.

###  0.C.3 Proof of Theorem 4.4

Let $(\mathcal{I},C)\in R$ (i.e., $\mathcal{I}=\alpha(C)$). For some action
$\langle\textit{act},\sigma\rangle$ with $\textit{act}=(g,\tt Del,\tt Add)$,

  1. 1.

$\mathcal{I}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{I}^{\prime}$
with $\mathcal{I}^{\prime}=(\mathcal{I}\setminus\tt Del\sigma^{\star})\cup\tt
Add\sigma^{\star}$ we need to show that $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}$, such
that for all $\mathcal{D}\in C$, there is a $\mathcal{D}^{\prime}\in
C^{\prime}$, such that $\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}$
and $(\mathcal{I}^{\prime},C^{\prime})\in R$.

Let $\mathcal{D}\in C$. Since $\mathcal{I}=\bigsqcap C$ by $\alpha_{4}$, there
is a homomorphism $id_{\mathcal{I}}:\mathcal{I}\to\mathcal{D}$. From Prop. 1 a
homomorphism $h_{g}:g\rightarrow\mathcal{I}$ exists. Then $h=h_{g}\circ
h_{\mathcal{I}}$ is a homomorphism $g\to\mathcal{D}$ and $\sigma\in
g(\mathcal{D})$ follows. Hence, $\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}(\mathcal{D}\setminus\tt
Del\sigma^{\star})\cup\tt Add\sigma^{\star}$. This argument holds for all
$\mathcal{D}\in C$. Thus $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}=\\{(\mathcal{D}\setminus\tt
Del\sigma^{*})\cup\tt Add\sigma^{\star}\mid\mathcal{D}\in C\\}$.

By construction of $\mathcal{I}^{\prime}$ and all $\mathcal{D}^{\prime}\in
C^{\prime}$, it is clear that $\mathcal{I}^{\prime}$ is a lower bound of each
$\mathcal{D}^{\prime}\in C^{\prime}$. Thus,
$\mathcal{I}^{\prime}\to\alpha_{4}(C^{\prime})=\bigsqcap C^{\prime}$. It
follows $\mathcal{I}^{\prime}\mathbin{\leftrightarrows}\alpha_{4}(C^{\prime})$
and, thus, $(\mathcal{I}^{\prime},C^{\prime})\in R$.

  2. 2.

$C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}$ such
that for every $\mathcal{D}\in C$, $\sigma\in g(\mathcal{D})$,
$\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}$
and $\mathcal{D}^{\prime}\in C^{\prime}$. It follows $\sigma\in g(\sqcap{C})$
and so $\sigma\in g(\mathcal{I})$. Construction of $\mathcal{I}^{\prime}$
according to the definition. Similarities pull out. Thus,
$\alpha(C^{\prime})\mathbin{\leftrightarrows}\mathcal{I}^{\prime}$.∎

###  0.C.4 Remark on Theorem 4.2

Compared to Theorem 4.4, projection-free conjunctive guards constitute the
guard language for this theorem. The reason may be found in the steps
considered on the concrete domain (i.e., item 2 in the proof of Theorem 4.4).
Consider the two databases

$\displaystyle\mathcal{D}_{1}=$ $\displaystyle\\{p(A),p(B),f(A,B)\\}$
$\displaystyle\mathcal{D}_{2}=$ $\displaystyle\\{p(A),p(C),f(A,C)\\}\text{.}$

Then the set intersection (also known as abstraction $\alpha_{2}$) is

$\displaystyle\mathcal{A}=\mathcal{D}_{1}\cap\mathcal{D}_{2}=$
$\displaystyle\\{p(A)\\}\text{,}$

while the abstract intersection in domain
$(\mathbb{I}^{\mathbf{N}},\leftarrow)$ is

$\displaystyle\mathcal{B}=\mathcal{D}_{1}\sqcap\mathcal{D}_{2}=$
$\displaystyle\\{p(A),f(A,n)\\}\text{.}$

In $\mathcal{B}$ the existence of a value $x$ such that $f(A,x)$ is expressed
by the labeled null $n$. Thus, a guard asking for the existence of a value
$x$, such that $f(A,x)$ can be matched on $\mathcal{B}$. On $\mathcal{A}$, on
the other hand, the same guard has no match, although both concrete databases
$\mathcal{D}_{1}$ and $\mathcal{D}_{2}$ list one $f$-atom accounting for the
connection to $A$. Thus, projections are expressed inside the abstract
instances using labeled nulls (e.g., $\mathcal{B}$), but is not present in the
simpler set-based abstractions (e.g., $\mathcal{A}$).

The proof of Theorem 4.2 follows the same lines as the proof of Theorem 4.4,
using $\subseteq$ instead of postulating the existence of
homomorphisms222Note, $\subseteq$ ultimately entails the existence of a
homomorphism, the identity function.. In item 2, $\sigma$ can only be
considered a match on the abstract instance $\mathcal{I}$ if the conjunctive
guard $g$ is projection-free (i.e., does not use existential quantification).

###  0.C.5 Proof of Theorem 4.6

Here we consider Galois connection $(\alpha_{6},\gamma_{6})$ on the abstract
domain $(\mathbb{I}^{\mathbf{N}}\times\mathbb{I}^{\mathbf{N}},\preceq)$ with
$\alpha_{6}(C):=(\bigsqcap C,\bigsqcup C)$ and for
$\mathcal{I}\in\mathbb{I}^{\mathbf{N}}\times\mathbb{I}^{\mathbf{N}}$, we get
if $\mathcal{I}=(\mathcal{I}_{1},\mathcal{I}_{2})$, then
$\mathcal{I}^{\sqcap}=\mathcal{I}_{1}$ and
$\mathcal{I}^{\sqcup}=\mathcal{I}_{2}$. We prove $\forall$-bisimilarity for
DMS using safe normal conjunctive guards.

Towards this goal, we show that

$R=\\{(\alpha_{6}(C),C)\mid C\subseteq\mathbb{U}\\}$

is a $\forall$-bisimulation. For $(\mathcal{I},C)\in R$ and
$\langle\textit{act},\sigma\rangle$,

  1. 1.

if $\mathcal{I}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{I}^{\prime}$,
we need to show that $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}$ such
that (a) for all $\mathcal{D}\in C$, $\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}$
and $\mathcal{D}^{\prime}\in C$, (b) for each $\mathcal{D}^{\prime}\in C$
there is a $\mathcal{D}\in C$ with $\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}$,
(c) $(\mathcal{I}^{\prime},C^{\prime})\in R$. Recall that $\mathcal{I}=()$ and
act uses an NCG guard $g$, such that $\sigma\in g^{+}(\mathcal{I}^{\sqcap})$
and $\sigma\in g^{-}(\mathcal{I}^{\sqcup})$. For $\mathcal{D}\in C$, we have
that $\mathcal{I}^{\sqcap}\to\mathcal{D}$ and
$\mathcal{D}\to\mathcal{I}^{\sqcup}$. By the argumentations in theorem 4.4 and
4.5, we obtain $\sigma\in g^{+}(\mathcal{D})\cup g^{-}(\mathcal{D})$. Thus,
$\mathcal{D}\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}\mathcal{D}^{\prime}$
for all $\mathcal{D}\in C$ and $\mathcal{D}^{\prime}\in C^{\prime}$ such that
$\mathcal{D}^{\prime}=(\mathcal{D}\setminus\tt Del\sigma^{\bullet})\cup\tt
Add\sigma^{\bullet}$ for some extension $\sigma^{\bullet}$ of $\sigma$
(surely, $\sigma$ and $\sigma^{\bullet}$ are compatible as $\sigma^{\bullet}$
extends $\sigma$). Following the arguments of the previous theorems separately
for $\mathcal{I}^{\prime\sqcap}$ and $\mathcal{I}^{\prime\sqcup}$, we obtain
the result that $\mathcal{I}^{\prime}=\alpha(C^{\prime})$, implying
$(\alpha(C^{\prime}),\mathcal{I}^{\prime})\in R$.

  2. 2.

if $C\mathrel{\ext@arrow
0359\Rightarrowfill@{}{\langle\textit{act},\sigma\rangle}}C^{\prime}$, then
the same separation of concerns for $\alpha(C)^{\sqcap}$ and
$\alpha(C)^{\sqcup}$ applies. The necessary arguments can be found in the
proofs of theorems 4.4 and 4.5.∎

###  0.C.6 Remark on Theorem 4.3

Once again, the proof is similar to the proof of the abstraction on the more
general domain. Since the abstraction function here is composed of the
$\alpha_{1}$ and $\alpha_{2}$, we have to stick to projection-freeness of the
guards once more. Otherwise, the proof follows the same lines as the proof of
Theorem 4.6, respecting the notes mentioned in Sect. 0.C.4


# NetROS-5G: Enhancing Personalization through 5G Network Slicing and Edge
Computing in Human-Robot Interactions

Anestis Dalgkitsis<EMAIL_ADDRESS>0000-0001-6838-1768 Research &
Development Department,
Iquadrat InformaticaCarrer del Dr. Rizal, 10BarcelonaSpain08006 and  Christos
Verikoukis<EMAIL_ADDRESS>Computer Engineering & Informatics
Department, University of Patras25is Martiou 7, Kato
KastritsiPatrasGreece26504 Iquadrat InformaticaCarrer del Dr. Rizal,
10BarcelonaSpain08006 ISI/ATHENAArtemidos 6 & EpidavrouAthensGreece15125

###### Abstract.

Robots are increasingly being used in a variety of applications, from
manufacturing and healthcare to education and customer service. However, the
mobility, power, and price points of these robots often dictate that they do
not have sufficient computing power on board to run modern algorithms for
personalization in human-robot interaction at desired rates. This can limit
the effectiveness of the interaction and limit the potential applications for
these robots. 5G connectivity provides a solution to this problem by offering
high data rates, bandwidth, and low latency that can facilitate robotics
services. Additionally, the widespread availability of cloud computing has
made it easy to access almost unlimited computing power at a low cost. Edge
computing, which involves placing compute resources closer to the action, can
offer even lower latency than cloud computing. In this paper, we explore the
potential of combining 5G, edge, and cloud computing to provide improved
personalization in human-robot interaction. We design, develop, and
demonstrate a new framework, entitled NetROS-5G, to show how the performance
gained by utilizing these technologies can overcome network latency and
significantly enhance personalization in robotics. Our results show that the
integration of 5G network slicing, edge computing, and cloud computing can
collectively offer a cost-efficient and superior level of personalization in a
modern human-robot interaction scenario.

5G, edge computing, cloud computing, network slicing, personalized robotics

††conference: ; March 13, 2023; Stockholm, SE

##  1\. Introduction

The incorporation of advanced algorithms in robotics has led to an increasing
demand for more powerful computing resources. However, the onboard computing
capabilities of robots are frequently limited, and may not be able to keep
pace with the rapid advancements in the field. In light of this, cloud
computing has emerged as a viable solution, offering on-demand access to an
abundance of computing resources. Edge computing on the other hand, provides
low latency access to computing resources in close proximity to the robot,
which can reduce the delay in communication between the robots and the
computational resources. The emergence of 5G networks has further enabled the
availability of low-latency access to edge computing resources, leading to
improvements in the overall responsiveness. The integration of cloud
computing, edge computing, and 5G networks has the potential to significantly
expand the capabilities of robots, lower their production price and enhance
the personalization capabilities and naturalness of Human-Robot Interaction
(HRI), via low-latency access to even further computational resources.

5G network slicing is a feature of the 5G networks that allows for the
creation of multiple virtual networks within a physical network, each with its
own specific characteristics and capabilities. Edge computing, on the other
hand, is a method of processing data closer to the source of the data, rather
than sending it to a centralized location for processing. When combined, 5G
network slicing and edge computing can provide improved human-robot
interaction and personalization by allowing for the creation of dedicated
virtual networks specifically designed for each use-case. These virtual
networks can be optimized for low-latency, high-bandwidth communication, which
is crucial for real-time interactions between humans and robots. Additionally,
edge computing can be used to process sensor data from robots in real-time,
allowing them to make more informed decisions and respond to human input more
quickly. This can lead to more natural and intuitive interactions between
humans and robots, as well as more personalized experiences.

Our key idea is that the human-robot interactions could be enhanced by the use
of modern 5G and beyond networking in conjunction with edge and cloud
computing. This presents a business market opportunity for cheaper robots with
better performance, that offer better personalization.

To achieve this, we design and implement a framework based on the functions of
5G network slicing, edge and cloud computing to orchestrate network services
with the end goal of better personalization and performance in HRI. By using
off-the-shelf parts we build a 5G Stand Alone (5G-SA) network with slicing
capabilities in both Radio Access Network (RAN) and computing part. We build
an in situ prototype management software, entitled NetRos-5G, which can
seamlessly extend the capabilities of Robot Operating System 2 (ROS2) between
the robot, remote cloud, and edge computing nodes. The abundance of resources
and capabilities beyond the robot can enhance the personalization capabilities
and HRI.

##  2\. Related work

The utilization of cloud computing in robotics, also known as cloud robotics,
has been previously investigated as a viable approach for offloading tasks or
increasing processing capabilities. Several studies have proposed automated
frameworks for provisioning and deploying ROS 2 nodes on public cloud
computing providers to improve robot performance. Notably, FogROS, FogROS2,
and FogROS G, introduced in (Kaiyuan et al., 2021), (Ichnowski et al., 2022),
and (Chen et al., 2022), respectively, are among the most significant
contributions. FogROS solutions are unique in that they push robot
applications from the robot to the cloud, rather than remotely assisting
tasks. The studies demonstrate the potential performance gains of offloading
ROS 2 nodes to cloud computing. While cloud computing introduces latency, it
can overcome network latency and significantly improve robot performance,
depending on the task.

Recently the focus has shifted from cloud computing to the new promising edge
computing that provides less computing capabilities, but with lower latency.
Giovanni Toffetti et al. in (Toffetti et al., 2022) discuss the main
advantages combining the use of a Kubernetes and real, heterogeneous, robotic
hardware, the main shortcomings we encountered with networking and sharing
GPUs to support deep learning workloads. More specifically, Peng Huang et al.
in (Huang et al., 2021) propose RecSLAM, a multi-robot laser Simultaneous
Localization and Mapping (SLAM) built upon the Robot-edge-cloud architecture
to allow for low-latency response. RecSLAM develops a hierarchical map fusion
technique that directs robot raw data to edge servers for real-time fusion and
then sends to the cloud for global merging. Their evaluations show RecSLAM can
achieve up to 39.31% processing latency reduction over the state-of-the-art.

The integration of edge and cloud computing has begun to emerge as a topic of
interest in recent literature. Authors in (Zhang et al., 2022) list several
recent works that leverage the Edge-Cloud Continuum with ROS 2 and Kubernetes.

The integration of 5G technologies in robotics is a relatively novel field of
study and has the potential to serve as a foundation for the development of
new systems in which modern robotics can rely on. This can be achieved by
combining 5G with edge and cloud computing. The authors in (Gu et al., 2022)
propose a real-time cloud robotics application by offloading robot navigation
engine over to 5G Mobile Edge Computing (MEC) sever. Robot engines are
containerized based on micro-service architecture and have been deployed using
Kubernetes. They successfully demonstrated that mobile robots are able to
avoid obstacles in real-time when the engines are remotely running in 5G MEC
server.

In contrast, the proposed approach utilizes 5G technologies to selectively
access a portion of the entire networking and computing infrastructure via 5G
network slicing, specifically tailored for each individual task or scenario.
This has shown to yield superior performance compared to other solution and
enhance the HRI.

##  3\. Methodology & Design

We consider an autonomous robot robot equipped with audiovisual capabilities,
including a camera, microphone, and display, to assist travelers in navigating
an airport. The robot must possess the ability to comprehend spoken commands,
verbally communicate, display directions, gather sensor data, and navigate
while avoiding obstacles. The objective of this system is to aid travelers in
reaching their designated departure gates efficiently.

###  3.1. System Model Architecture

The robot is connected to a local 5G Base Station (BS) though a 5G-enabled
modem that is connected via a 10GE to the robot. A server with limited
computing capabilities is connected to the BS through a switch via a 10GE, all
located in close proximity to the robot in a range less than 1 km. This
computing setup close to the robot is defined as a Mobile Edge Computing (MEC)
node. The MEC node has access through the Internet (via the land network) to a
public cloud provider that offers virtually unlimited computing resources. The
studied architecture can be seen in the Fig. 1.

Figure 1. Architecture overview of the studied scenario. The robot is able to
access the edge and cloud computing resources via the 5G network.

###  3.2. Network Slice Framework

All aforementioned entities belong in a 5G networking slice that extends from
the robot, to the edge and cloud computing nodes. All robot ROS 2 nodes were
containerized based on the modern micro-service architecture and deployed
using Kubernetes (Kubernetes, 2023) to provide scalability and load balancing
functions. A shared Cyclone DDS Messaging Bus (Robotics, 2023a) ensures fault-
tolerant data exchange. The dedicated network slice confers security and
isolation from the rest of the network, thereby mitigating the risk of
potential attacks. The computational and network slice architecture can be
seen in the Fig. 2.

Figure 2. Overview of the network slice architecture. The network slice
ensures the security and isolation of the robot functionality from the rest of
the network, while also providing controlled network and computing resources.

##  4\. Practical Evaluation

In this section, we present the examined scenario and results during the
experimental evaluation of our case study.

###  4.1. Experimental Setting

In this study, the experimental evaluation takes place in a laboratory
environment with physical 5G and computing equipment. The robot of choice, the
TurtleBot3 (Robotis, 2023), was simulated in an x86 mini-computer with the
GAZEBO robot simulator (Robotics, 2023b), as the delivery of the actual robot
was delayed due to supply-chain disruptions. The robot was connected through
an Ethernet link to a 5G-modem, branded Teltonika TRB500 (Teltonika, 2023). An
Amarisoft Callbox Mini (Amarisoft, 2023) 5G BS was connected to a server
cluster, used as an edge computing node.

The Amarisoft Callbox BS is single-cell 5G NR standalone or Long-Term
Evolution (LTE) cells. It is composed of a PCIe Software-Defined Radio (SDR)
card, 2x2 Multiple-Input Multiple-Output (MIMO), up to 500 devices with 2
slices. The Amarisoft Callbox BS comes with its own proprietary 5G Core
software which is disabled in this setup, as a custom Open5Gs (Project, 2023)
Core setup is used in the Server Cluster and MECs, to enable low-latency
communication scenarios.

The edge computing node server cluster comprises of two identical servers with
off-the-shelf parts that each contain a 26 Core, 56 Thread Intel Xeon Gold
6230R CPU @ 2.10GHz, 256 GB Error-Correcting Code (ECC) memory and a GeForce
RTX 2080 SUPER GPU dedicated for AI/ML capabilities.

For a cloud computing node, the Amazon Web Services (AWS) Paris node from the
public cloud provider amazon was chosen as the closest cloud server to the
site of evaluation in Barcelona, Spain. The robot, edge and cloud nodes were
all a part of the same 5G network slice for the evaluation of the proposed
NetROS-5G solution, as depicted in Fig. 2. Local, edge and cloud
configurations were also studied.

###  4.2. Examined Scenario

The effectiveness of the proposed framework NetROS-5G was assessed by
conducting a use-case study involving an autonomous robot located in an
airport, guiding the travelers to their designated departure gates. The robot
is scanning the faces of the travelers, matching it with the database entry
and responding with a personalized message before navigating to the correct
gate of the terminal.

###  4.3. Examination Results

First, we examine the End-to-End (E2E) slice latency, between the robot and
the furthest container dedicated to navigation, for all different settings. To
test this Key Performance Indicator (KPI) we use teleoperation to measure the
latency from the node that hosts the navigation container to the robot. This
will allow measuring the network performance during remote operation. For this
scenario, we take 1000 samples at 1Hz for all 4 different scenarios at the
same time. As we can see in Fig. 3, we observe that the overall latency when
using only a cloud node for navigation can be as high as 199.832% more than
running it local at 38 ms average, compared to 0.016 ms average. The NetROS-5G
framework is utilizing the Edge computing node for all navigation tasks,
offloading data-related tasks on the cloud. As expected the response can be
183.548% faster than this of the cloud for both settings.

Figure 3. End-to-end latency difference measured between the robot and the
final destination, with 1000 samples.

Second, we examine the computing load yielded by the personalization
functionality hosted in the nodes. For this KPI, we instantiate a Face-
Recognition script, developed with Python and OpenCV, to showcase the
computational load of a robot task that is used for personalization,
recognizing the person that the robot interacts with. Table 1 shows the
computing load ranges that were measured during the same 1000 samples. Using a
cloud node for the personalization task uses minimal resources. Similarly,
using an edge node as NetROS-5G to outsource the personalization task yields a
lower load than performing the task locally in the onboard computer of the
robot. It is apparent that a combination of edge and cloud computing is the
best middle-ground between latency, computing capability, and cost.

Device | Robot CPU Usage | Memory Usage
---|---|---
NetROS-5G | 12%-18% | 0.51 GB
Robot On-board | 65%-80% | 1.82 GB
5G-SA + Edge | 28%-35% | 0.95 GB
5G-SA + Cloud | 12%-17% | 0.51 GB

Table 1. Average computational load per scenario. 1000 Samples during test.

Finally, we examine the response time of the personalization task, measuring
the time elapsed from the detection of a face that belongs to a traveler to
the response in the local display. In order to perform this task in our
laboratory environment with the simulated robot, we measured and compared the
timestamps of the face detection and the response from the container that
encapsulates the personalization app. According to the scenario, the robot is
searching for the faces of the travelers, matching them to their photos in the
database, and returning a personalized response as an action. Specifically,
Table 2 shows how prolonged the execution of the personalization task is
locally on the onboard computer, almost 110.792% slower than using the edge or
the cloud node, making the networking delay insignificant for such tasks.
Again, similar to the NetROS-5G, a fusion of the edge and cloud is the perfect
middle-ground.

Device | Face recognition | Response time
---|---|---
NetROS-5G | 657 sec | 698 sec
Robot On-board | 2354 ms | 2383 sec
5G-SA + Edge | 596 sec | 615 sec
5G-SA + Cloud | 587 sec | 684 sec

Table 2. Face recognition response time. 1000 Samples during test.

###  4.4. Discussion

The performance of hardware and the reduction of network latency both
contribute to the enhancement of personalization in Human-Robot Interaction
(HRI) by enabling the robot to respond swiftly and precisely to inputs. Low
network latency is a critical aspect for real-time communication and task
offloading in a remote host, as well as for the transmission of data used for
personalization and analysis. It is a key factor in the efficient and accurate
operation of real-time systems, as well as in the effective utilization of
data for personalization and analysis. This highlights the importance of
minimizing network latency in order to achieve optimal performance in real-
time communication and the time required for data analysis and response.

##  5\. Conclusion

In this paper, we have designed and developed a framework called NetROS-5G, to
demonstrate the performance that can be exploited by utilizing network slicing
in 5G networks, edge and cloud computing to overcome network latency and
enhance the performance in personalization tasks in robotics.

As a next step in our research, we plan to conduct experiments utilizing
Simultaneous Localization And Mapping (SLAM) navigation and planning
techniques with a physical TurtleBot 4 robot, and further automating the
NetROS-5G framework. The purpose of these additional experiments is to further
evaluate the performance of the network and computational resources
orchestration component.

###### Acknowledgements.

This work was supported by the European research project 5G-ERA (101016681).

## References

  * (1)
  * Amarisoft (2023) Amarisoft. 2023.  Amarisoft Callbox Series.  https://www.amarisoft.com/products/test-measurements/amari-lte-callbox/ Accessed: 14/01/2023.
  * Chen et al. (2022) Kaiyuan Chen, Jiachen Yuan, Nikhil Jha, Jeffrey Ichnowski, John Kubiatowicz, and Ken Goldberg. 2022.  FogROS G: Enabling Secure, Connected and Mobile Fog Robotics with Global Addressability.  https://doi.org/10.48550/ARXIV.2210.11691
  * Gu et al. (2022) Sewan Gu, Sungkyu Kang, Wonhong Jeong, Hyungil Moon, Hyunseok Yang, and Youngjae Kim. 2022.  Validation of Cloud Robotics System in 5G MEC for Remote Execution of Robot Engines.  _The Journal of Korea Robotics Society_ 17, 2 (2022), 118–123.
  * Huang et al. (2021) Peng Huang, Liekang Zeng, Xu Chen, Ke Luo, Zhi Zhou, and Shuai Yu. 2021.  Edge Robotics: Edge-Computing-Accelerated Multi-Robot Simultaneous Localization and Mapping.  https://doi.org/10.48550/ARXIV.2112.13222
  * Ichnowski et al. (2022) Jeffrey Ichnowski, Kaiyuan Chen, Karthik Dharmarajan, Simeon Adebola, Michael Danielczuk, Vıctor Mayoral-Vilches, Nikhil Jha, Hugo Zhan, Edith LLontop, Derek Xu, John Kubiatowicz, Ion Stoica, Joseph Gonzalez, and Ken Goldberg. 2022.  FogROS2: An Adaptive Platform for Cloud and Fog Robotics Using ROS 2.  https://doi.org/10.48550/ARXIV.2205.09778
  * Kaiyuan et al. (2021) Kaiyuan, Chen, Yafei Liang, Nikhil Jha, Jeffrey Ichnowski, Michael Danielczuk, Joseph Gonzalez, John Kubiatowicz, and Ken Goldberg. 2021.  FogROS: An Adaptive Framework for Automating Fog Robotics Deployment.  https://doi.org/10.48550/ARXIV.2108.11355
  * Kubernetes (2023) Kubernetes. 2023.  Kubernetes.  https://kubernetes.io Accessed: 14/01/2023.
  * Project (2023) Open5GS Project. 2023.  Open5GS.  https://open5gs.org/ Accessed: [Insert date accessed].
  * Robotics (2023a) Open Robotics. 2023a.  Cyclone DDS.  https://github.com/ros2/cyclonedds Accessed: 14/01/2023.
  * Robotics (2023b) Open Robotics. 2023b.  Gazebo.  http://gazebosim.org/ Accessed: 14/01/2023.
  * Robotis (2023) Robotis. 2023.  TurtleBot3.  http://turtlebot3.robotis.com/ Accessed: 14/01/2023.
  * Teltonika (2023) Teltonika. 2023.  Teltonika TRB500.  https://teltonika-networks.com/product/trb500/ Accessed: 14/01/2023.
  * Toffetti et al. (2022) Giovanni Toffetti, Leonardo Militano, Seán Murphy, Remo Maurer, and Mark Straub. 2022.  Cloud Native Robotic Applications with GPU Sharing on Kubernetes.  https://doi.org/10.48550/ARXIV.2210.03936
  * Zhang et al. (2022) Jiaqiang Zhang, Farhad Keramat, Xianjia Yu, Daniel Montero Hern, Jorge Peña Queralta, and Tomi Westerlund. 2022.  Distributed Robotic Systems in the Edge-Cloud Continuum with ROS 2: a Review on Novel Architectures and Technology Readiness.  https://doi.org/10.48550/ARXIV.2211.00985