11institutetext: Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000,
France

# Decision Problems in a Logic for Reasoning about ReconfigurableDistributed
Systems

Marius Bozga 11 Lucas Bueri 11 Radu Iosif 11

###### Abstract

We consider a logic used to describe sets of configurations ofdistributed
systems, whose network topologies can be changed atruntime, by reconfiguration
programs. The logic uses inductivedefinitions to describe networks with an
unbounded number ofcomponents and interactions, written using a
multiplicativeconjunction, reminiscent of Bunched Implications
[PymOHearn99]and Separation Logic [Reynolds02]. We study the complexity ofthe
satisfiability and entailment problems for the configurationlogic under
consideration. Additionally, we consider robustness properties, such as
tightness (are all interactionsentirely connected to components?) and degree
boundedness (is every component involved in a boundednumber of interactions?),
the latter being aningredient for decidability of entailments.

##  1 Introduction

Distributed systems are increasingly used as critical parts of
theinfrastructure of our digital society, as in e.g., datacenters,e-banking
and social networking. In order to address maintenance(e.g., replacement of
faulty and obsolete network nodes by new ones)and data traffic issues (e.g.,
managing the traffic inside adatacenter
[DBLP:journals/comsur/Noormohammadpour18]), thedistributed systems community
has recently put massive effort indesigning algorithms for _reconfigurable
systems_ , whose networktopologies change at
runtime[DBLP:journals/sigact/FoersterS19]. However, dynamicreconfiguration is
an important souce of bugs that may result in e.g.,denial of services or even
data
corruption111https://status.cloud.google.com/incident/appengine/19007.This
paper contributes to a logical framework that addresses thetimely problems of
formal _modeling_ and _verification_ ofreconfigurable distributed systems. The
basic building blocks of thisframework are  (i) a Hoare-style program proof
calculus[AhrensBozgaIosifKatoen21] used to write formal proofs ofcorrectness
of reconfiguration programs, and (ii) an invariant synthesis method
[BozgaIosifSifakis21] thatproves the safety (i.e., absence of reachable error
configurations)of the configurations defined by the assertions that annotate
areconfiguration program. These methods are combined to prove that an
initially correctdistributed system cannot reach an error state, following
theexecution of a given reconfiguration sequence.The assertions of the proof
calculus are written in a logic thatdefines infinite sets of configurations,
consisting of _components_ (i.e., processes running on different nodes of
thenetwork) connected by _interactions_ (i.e., multi-party channelsalongside
which messages between components are transfered). Systemsthat share the same
architectural style (e.g., pipeline, ring, star,tree, etc.) and differ by the
number of components and interactionsare described using inductively defined
predicates. Suchconfigurations can be modified either by  (a) adding or
removing components andinteractions (reconfiguration), or (b) changing the
local states of components, byfiring interactions. The assertion logic views
components and interactions as _resources_ , that can be created or deleted,
in the spirit ofresource logics _à la_ Bunched Implications[PymOHearn99], or
Separation Logic [Reynolds02]. The mainadvantage of using resource logics is
their support for _localreasoning_ [CalcagnoOHearnYan07]: reconfiguration
actions arespecified by pre- and postconditions mentioning only the
resourcesinvolved, while framing out the rest of the configuration.The price
to pay for this expressive power is the difficulty ofautomating the reasoning
in these logics. This paper makes severalcontributions in the direction of
proof automation, by studying thecomplexity of the _satisfiability_ and
_entailment_ problems, for the configuration logic underconsideration.
Additionally, we study the complexity of two robustness properties
[JansenKatelaanMathejaNollZuleger17],namely _tightness_ (are all interactions
entirely connected tocomponents?) and _degreeboundedness_ (is every component
involved in a bounded number ofinteractions?). In particular, the latter
problem is used as aprerequisite for defining a fragment with a decidable
entailmentproblem.

###  1.1 Motivating Example

The logic studied in this paper is motivated by the need for anassertion
language that supports reasoning about dynamicreconfigurations in a
distributed system. For instance, consider adistributed system consisting of a
finite (but unknown) number of _components_ (processes) placed in a ring,
executing the samefinite-state program and communicating via _interactions_
thatconnect the _out_ port of a component to the _in_ port ofits right
neighbour, in a round-robin fashion, as inFig. 1 (a). The behavior of a
component is a machine withtwo states, $\mathsf{T}$ and $\mathsf{H}$, denoting
whether thecomponent has a token ($\mathsf{T}$) or not ($\mathsf{H}$). A
component$c_{i}$ without a token may receive one, by executing a
transition$\mathsf{H}\xrightarrow{{\scriptstyle\mathit{in}}}\mathsf{T}$,
simultaneously with itsleft neighbour $c_{j}$, that executes the transition
transition$\mathsf{T}\xrightarrow{{\scriptstyle\mathit{out}}}\mathsf{H}$.
Then, we say that theinteraction $(c_{j},\mathit{out},c_{i},\mathit{in})$ has
fired, movinga token one position to the right in the ring. Note that there
can bemore than one token, moving independently in the system, as long as
notoken overtakes another token.The token ring system is formally specified by
the following inductiverules:

$\displaystyle\mathsf{ring}_{{h},{t}}(x)$ $\displaystyle\leftarrow\exists
y\exists
z~{}.~{}{[{x}]}@{q}*\langle{{x}.\mathit{out},{z}.\mathit{in}}\rangle*\mathsf{chain}_{{h^{\prime}},{t^{\prime}}}(z,y)*\langle{{y}.\mathit{out},{x}.\mathit{in}}\rangle$
$\displaystyle\mathsf{chain}_{{h},{t}}(x,y)$ $\displaystyle\leftarrow\exists
z.~{}{[{x}]}@{q}*\langle{{x}.{\mathit{out}},{z}.{\mathit{in}}}\rangle*\mathsf{chain}_{{h^{\prime}},{t^{\prime}}}(z,y)$
$\displaystyle\mathsf{chain}_{{0},{1}}(x,x)$
$\displaystyle\leftarrow{[{x}]}@{\mathsf{T}}\hskip
22.76219pt\mathsf{chain}_{{1},{0}}(x,x)\leftarrow{[{x}]}@{\mathsf{H}}\hskip
22.76219pt\mathsf{chain}_{{0},{0}}(x,x)\leftarrow[{x}]$
$\displaystyle\text{where }h^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\left\\{\begin{array}[]{ll}\max(h-1,0)&\text{,
if }q=\mathsf{H}\\\ h&\text{, if }q=\mathsf{T}\end{array}\right.\text{ and
}t^{\prime}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\left\\{\begin{array}[]{ll}\max(t-1,0)&\text{,
if }q=\mathsf{T}\\\ t&\text{, if }q=\mathsf{H}\end{array}\right.$

The predicate $\mathsf{ring}_{{h},{t}}(x)$ describes a ring with at least
twocomponents, such that at least $h$ (resp. $t$) components are in
state$\mathsf{H}$ (resp. $\mathsf{T}$). The ring consists of a component $x$in
state $q$, described by the formula ${[{x}]}@{q}$, aninteraction from the
$\mathit{out}$ port of $x$ to the $\mathit{in}$port of another component $z$,
described as$\langle{{x}.\mathit{out},{z}.\mathit{in}}\rangle$, a separate
chain of componentsstretching from $z$ to $y$
($\mathsf{chain}_{{h^{\prime}},{t^{\prime}}}(z,y)$), and an
interactionconnecting the $\mathit{out}$ port of component $y$ to
the$\mathit{in}$ port of component
$x$($\langle{{y}.\mathit{out},{x}.\mathit{in}}\rangle$). Inductively, a chain
consists of acomponent ${[{x}]}@{q}$, an
interaction$\langle{{x}.\mathit{out},{z}.\mathit{in}}\rangle$ and a
separate$\mathsf{chain}_{{h^{\prime}},{t^{\prime}}}(z,y)$. Fig. 1 (b) depicts
the unfoldingof the inductive definition of the token ring, with the
existentiallyquantified variables $z$ from the above rules $\alpha$-renamed
to$z^{1},z^{2},\ldots$ to avoid confusion.

$\mathsf{ring}_{{h},{t}}(x)$$\cdots$$\mathit{out}$$\mathit{out}$$\mathit{out}$(a)$\mathit{in}$$\mathit{out}$$\mathit{in}$$\mathit{out}$$\mathsf{T}$$\mathit{in}$$\mathit{out}$$\mathsf{T}$$\mathit{in}$$\mathit{in}$$\mathit{out}$$\mathit{in}$$\mathit{out}$$\mathsf{T}$$c_{n}$$c_{n-1}$$\mathit{in}$$\mathit{in}$$c_{2}$(b)$\mathsf{H}$$\mathsf{T}$$\mathsf{H}$$\mathsf{H}$$\mathsf{H}$${[{x}]}@{\mathsf{H}}$${[{z^{1}}]}@{\mathsf{T}}$$c_{1}$$\langle{{y}.\mathit{out},{x}.\mathit{in}}\rangle$$\langle{{z^{1}}.\mathit{out},{z^{2}}.\mathit{in}}\rangle$$\mathsf{chain}_{{h-1},{t-1}}(z^{2},y)$$\langle{{x}.\mathit{out},{z^{1}}.\mathit{in}}\rangle$$\mathsf{chain}_{{h-1},{t}}(z^{1},y)$

⬇

$\\{{\ovalbox{${{[{y}]}@{\mathsf{H}}*\langle{{y}.{\mathit{out}},{z}.{\mathit{in}}}\rangle*\mathsf{chain}_{{h-1},{t}}(z,x)}$}*\langle{{x}.{\mathit{out}},{y}.{\mathit{in}}}\rangle}\\}$

disconnect(x.$\mathit{out}$, y.$\mathit{in}$);

$\\{{\ovalbox{${{[{y}]}@{\mathsf{H}}}$}*\langle{{y}.{\mathit{out}},{z}.{\mathit{in}}}\rangle*\ovalbox{${\mathsf{chain}_{{h-t},{t}}(z,x)}$}}\\}$

disconnect(y.$\mathit{out}$, z.$\mathit{in}$);

$\\{{{[{y}]}@{\mathsf{H}}*\ovalbox{${\mathsf{chain}_{{h-1},{t}}(z,x)}$}}\\}$

delete(y);

$\\{{\ovalbox{${\mathsf{chain}_{{h-1},{t}}(z,x)}$}}\\}$

connect(x.$\mathit{out}$, z.$\mathit{in}$)

$\\{{\mathsf{chain}_{{h-1},{t}}(z,x)*\langle{{x}.{\mathit{out}},{z}.{\mathit{in}}}\rangle}\\}$

$\\{{\mathsf{ring}_{{h-1},{t}}(z)}\\}$

(c)

Figure 1: Inductive Specification and Reconfiguration of a Token Ring

A _reconfiguration program_ takes as input a mapping of programvariables to
components and executes a sequence of _basicoperations_ i.e.,
component/interaction creation/deletion, involvingthe components and
interactions denoted by these variables. Forinstance, the reconfiguration
program in Fig. 1 (c) takesas input three adjacent components, mapped to the
variables$\mathtt{x}$, $\mathtt{y}$ and $\mathtt{z}$, respectively, removes
thecomponent $\mathtt{y}$ together with its left and right interactionsand
reconnects $\mathtt{x}$ directly with $\mathtt{z}$.
Programmingreconfigurations is error-prone, because the interleaving
betweenreconfiguration actions and interactions in a distributed system
maylead to bugs that are hard to trace. For instance, if areconfiguration
program removes the last component in state$\mathsf{T}$ (resp. $\mathsf{H}$)
from the system, no token transferinteraction may fire and the system
deadlocks.We prove absence of such errors using a Hoare-style proof
system[AhrensBozgaIosifKatoen21], based on the above logic as
assertionlanguage. For instance, the proof from Fig. 1 (c) showsthat the
reconfiguration sequence applied to a component $\mathtt{y}$in state
$\mathsf{H}$ (i.e., ${[{y}]}@{\mathsf{H}}$) in a ring withat least $h\geq 2$
components in state $\mathsf{H}$ and at least$t\geq 1$ components in state
$\mathsf{T}$ leads to a ring with at least$h-1$ components in state
$\mathsf{H}$ and at least $t$ in state$\mathsf{T}$; note that the states of
the components may change duringthe execution of the reconfiguration program,
as tokens are moved byinteractions.For reasons of proof scalability, a basic
operation is specified onlywith regard to the components and interactions
required to avoidfaulting. For instance
$\\{{{[{x}]}@{q}}\\}~{}\mathsf{\mathsf{delete}(x)}~{}\\{{\mathsf{emp}}\\}$(resp.
$\\{{\langle{{x}.\mathit{out},{y}.\mathit{in}}\rangle}\\}~{}\mathsf{\mathsf{disconnect}(\mathtt{x}.\mathit{out},\mathtt{y}.\mathit{in})}~{}\\{{\mathsf{emp}}\\}$)
means that $\mathsf{delete}$(resp. $\mathsf{disconnect}$) requires a component
(resp. interaction)and returns an empty configuration,
whereas$\\{{\mathsf{emp}}\\}~{}\mathsf{\mathsf{connect}(\mathtt{x}.\mathit{out},\mathtt{y}.\mathit{in})}~{}\\{{\langle{{x}.\mathit{out},{y}.\mathit{in}}\rangle}\\}$means
that $\mathsf{connect}$ requires nothing and creates an interactionbetween the
given ports of the given components. These localspecifications are plugged
into a context described by a frame formula$F$, using the _frame rule_
$\\{{\phi}\\}~{}\mathsf{\mathsf{P}}~{}\\{{\psi}\\}\Rightarrow\\{{\phi*\ovalbox{${F}$}}\\}~{}\mathsf{\mathsf{P}}~{}\\{{\psi*F}\\}$;
forreadability, the frame formulæ (from the preconditions of theconclusion of
the frame rule applications) are enclosed in boxes.The proof also uses the
_consequence rule_
$\\{{\phi}\\}~{}\mathsf{P}~{}\\{{\psi}\\}\Rightarrow\\{{\phi^{\prime}}\\}~{}\mathsf{P}~{}\\{{\psi^{\prime}}\\}$
that applies if $\phi^{\prime}$ isstronger than $\phi$ and $\psi^{\prime}$ is
weaker than $\psi$. The sideconditions of the consequence rule require
checking the validity ofthe entailments
$\mathsf{ring}_{{h},{t}}(y)\models\exists x\exists
z~{}.~{}\langle{{x}.{\mathit{out}},{y}.{\mathit{in}}}\rangle*{[{y}]}@{\mathsf{H}}*\langle{{y}.{\mathit{out}},{z}.{\mathit{in}}}\rangle*\mathsf{chain}_{{h-1},{t}}(z,x)$
and$\mathsf{chain}_{{h-1},{t}}(z,x)*\langle{{x}.{\mathit{out}},{z}.{\mathit{in}}}\rangle\models\mathsf{ring}_{{h-1},{t}}(z)$,
for all $h\geq 2$ and $t\geq 1$. These sideconditions can be automatically
discharged using the results on thedecidability of entailments given in this
paper. Additionally,checking the satisfiability of a precondition is used to
detecttrivially valid Hoare triples.

###  1.2 Related Work

Formal modeling coordinating architectures of component-based systemshas
received lots of attention, with the development of architecturedescription
languages (ADL), such as BIP [basu2006modeling] orREO [Arbab04]. Many such
ADLs have extensions that describeprogrammed reconfiguration, e.g.,[DR-BIP-
STTT, KrauseMaraikarLazovikArbab11], classified accordingto the underlying
formalism used to define their operationalsemantics: _process
algebras_[CavalcanteBO15, magee1996dynamic], _graph
rewriting_[taentzer1998dynamic, DBLP:journals/scp/WermelingerF02,
LeMetayer],_chemical reactions_ [wermelinger1998towards] (see
thesurveys[bradbury2004survey, rumpe2017classification]). Unfortunately,only
few ADLs support formal verification, mainly in the flavour ofruntime
verification[BucchiaroneG08, DormoyKL10, LanoixDK11, DBLP:conf/sac/El-
HokayemBS21]or finite-state model checking [Clarke08].Parameterized
verification of unbounded networks of distributedprocesses uses mostly hard-
coded coordinating architectures
(see[BloemJacobsKhalimovKonnovRubinVeithWidder15] for a survey). Afirst
attempt at specifying architectures by logic is the _interaction logic_ of
Konnov et al. [KonnovKWVBS16], acombination of Presburger arithmetic with
monadic uninterpretedfunction symbols, that can describe cliques, stars and
rings. Morestructured architectures (pipelines and trees) can be described
usinga second-order extension [MavridouBBS17]. However, theseinteraction
logics are undecidable and lack support for automatedreasoning.Specifying
parameterized component-based systems by inductivedefinitions is not new.
_Network grammars_[ShtadlerGrumberg89, LeMetayer, Hirsch] use context-free
grammarrules to describe systems with linear (pipeline, token-
ring)architectures obtained by composition of an unbounded number ofprocesses.
In contrast, we use predicates of unrestricted arities todescribe
architectural styles that are, in general, more complex thantrees. Moreover,
we write inductive definitions using a resourcelogic, suitable also for
writing Hoare logic proofs of reconfigurationprograms, based on local
reasoning [CalcagnoOHearnYan07].Local reasoning about concurrent programs has
been traditionally thefocus of Concurrent Separation Logic (CSL), based on a
parallelcomposition rule [DBLP:journals/tcs/OHearn07], initially with anon-
interfering (race-free) semantics [Brookes:2016] and latercombining ideas of
assume- and rely-guarantee[Owicki1978, DBLP:phd/ethos/Jones81] with local
reasoning[FengFerreiraShao07, Vafeiadis07] and abstract notions of
framing[Dinsdale-Young10, Dinsdale-Young13, Farka21]. However, the body ofwork
on CSL deals almost entirely with shared-memory multithreadingprograms,
instead of distributed systems, which is the aim of ourwork. In contrast, we
develop a resource logic in which the processesdo not just share and own
resources, but become mutable resourcesthemselves.The techniques developed in
this paper are inspired by existingtechniques for similar problems in the
context of Separation Logic(SL) [Reynolds02]. For instance, we use an abstract
domainsimilar to the one defined by Brotherston etal.
[DBLP:conf/csl/BrotherstonFPG14] for checking satisfiabilityof symbolic heaps
in SL and reduce a fragment of the entailmentproblem in our logic to SL
entailment[EchenimIosifPeltier21]. In particular, the use of existingautomated
reasoning techniques for SL has pointed out severaldifferences between the
expressiveness of our logic and that ofSL. First, the configuration logic
describes hypergraphstructures, in which edges are $\ell$-tuples for $\ell\geq
2$, insteadof directed graphs as in SL, where $\ell$ is a parameter of
theproblem: considering $\ell$ to be a constant strictly decreases
thecomplexity of the problem. Second, the degree (number of
hyperedgescontaining a given vertex) is unbounded, unlike in SL, where
thedegree of heaps is constant. Therefore, we dedicate an entire
section(§LABEL:sec:boundedness) to the problem of deciding the existence ofa
bound (and computing a cut-off) on the degree of the models of aformula, used
as a prerequisite for the encoding of the entailmentproblems from the
configuration logic as SL entailments.

##  2 Definitions

We denote by $\mathbb{N}$ the set of positive integers. For a set $A$,
wedefine
$A^{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}A$,
$A^{i+1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}A^{i}\times
A$, for all $i\geq 0$, and $A^{+}=\bigcup_{i\geq 1}A^{i}$, where $\times$
denotes theCartesian product. We denote by $\mathrm{pow}({A})$ the powerset of
$A$ and by$\mathrm{mpow}({A})$ the power-multiset (set of multisets) of $A$.
Thecardinality of a finite set $A$ is denoted as $|\\!|{A}|\\!|$. By
writing$A\subseteq_{\mathit{fin}}B$ we mean that $A$ is a finite subset of
$B$. Givenintegers $i$ and $j$, we write $[{i},{j}]$ for the
set$\\{{i,i+1,\ldots,j}\\}$, assumed to be empty if $i>j$. For a
tuple$\mathbf{t}=\langle{t_{1},\ldots,t_{n}}\rangle$, we define
$|{\mathbf{t}}|\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}n$,
$\and{\mathbf{t}}{i}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}t_{i}$
and$\and{\mathbf{t}}{[{i},{j}]}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\langle{t_{i},\ldots,t_{j}}\rangle$.
Bywriting $x=\mathit{poly}(y)$, for given $x,y\in\mathbb{N}$, we mean that
thereexists a polynomial function $f:\mathbb{N}\rightarrow\mathbb{N}$, such
that $x\leq f(y)$.

###  2.1 Configurations

We model distributed systems as hypergraphs, whose vertices are _components_
(i.e., the nodes of the network) and hyperedges are _interactions_ (i.e.,
describing the way the componentscommunicate with each other). The components
are taken from acountably infinite set $\mathbb{C}$, called the _universe_.
Weconsider that each component executes its own copy of the same _behavior_ ,
represented as a finite-state
machine$\mathbb{B}=(\mathcal{P},\mathcal{Q},\xrightarrow{{\scriptstyle}})$,
where $\mathcal{P}$ is a finite set of _ports_ , $\mathcal{Q}$ is a finite set
of _states_
and$\xrightarrow{{\scriptstyle}}\subseteq\mathcal{Q}\times\mathcal{P}\times\mathcal{Q}$
is atransition relation. Intuitively, each transition
$q\xrightarrow{{\scriptstyle p}}q^{\prime}$of the behavior is triggerred by a
visible event, represented by theport $p$. For instance, the behavior of the
components of the tokenring system from Fig. 1 (a)
is$\mathbb{B}=(\\{{\mathit{in},\mathit{out}}\\},\\{{\mathsf{H},\mathsf{T}}\\},\\{{\mathsf{H}\xrightarrow{{\scriptstyle\mathit{in}}}\mathsf{T},\mathsf{T}\xrightarrow{{\scriptstyle\mathit{out}}}\mathsf{H}}\\})$.
The universe$\mathbb{C}$ and the behavior
$\mathbb{B}=(\mathcal{P},\mathcal{Q},\xrightarrow{{\scriptstyle}})$
areconsidered fixed in the rest of this paper.We introduce a logic for
describing infinite sets of _configurations_ of distributed systems with
unboundedly manycomponents and interactions. A configuration is a snapshot of
thesystem, describing the topology of the network (i.e., the set ofpresent
components and interactions) together with the local state ofeach component:

###### Definition 1

A _configuration_ is a tuple $\gamma=(\mathcal{C},\mathcal{I},\varrho)$,
where:

  * •

$\mathcal{C}\subseteq_{\mathit{fin}}\mathbb{C}$ is a finite set of
_components_ ,that are present in the configuration,

  * •

$\mathcal{I}\subseteq_{\mathit{fin}}(\mathbb{C}\times\mathcal{P})^{+}$ is a
finiteset of _interactions_ , where each interaction is a
sequence$(c_{1},p_{1},\ldots,c_{n},p_{n})\in(\mathbb{C}\times\mathcal{P})^{n}$that
binds together the ports $p_{1},\ldots,p_{n}$ of the pairwisedistinct
components $c_{1},\ldots,c_{n}$, respectively.

  * •

$\varrho:\mathbb{C}\rightarrow\mathcal{Q}$ is a _statemap_ associating each
(possibly absent) component, a state of thebehavior $\mathbb{B}$, such that
the set $\\{{c\in\mathbb{C}\mid\varrho(c)=q}\\}$ is infinite, for each
$q\in\mathcal{Q}$.

The last condition requires that there is an infinite pool ofcomponents in
each state $q\in\mathcal{Q}$; since $\mathbb{C}$ isinfinite and $\mathcal{Q}$
is finite, this condition is feasible. Forexample, the configurations of the
token ring from Fig. 1(a) are
$(\\{c_{1},\ldots,c_{n}\\},\\{(c_{i},\mathit{out},c_{(i~{}\mathrm{mod}~{}n)+1},\mathit{in})\mid
i\in[{1},{n}]\\},\varrho)$,
where$\varrho:\mathbb{C}\rightarrow\\{{\mathsf{H},\mathsf{T}}\\}$ is a
statemap. The ring topology is described by the set of components
$\\{c_{1},\ldots,c_{n}\\}$ and interactions
$\\{(c_{i},\mathit{out},c_{(i~{}\mathrm{mod}~{}n)+1},\mathit{in})\mid
i\in[{1},{n}]\\}$.Intuitively, an interaction
$(c_{1},p_{1},\ldots,c_{n},p_{n})$synchronizes transitions labeled by the
ports $p_{1},\ldots,p_{n}$ fromthe behaviors (i.e., replicas of the state
machine $\mathbb{B}$) of $c_{1},\ldots,c_{n}$, respectively. The interactions
are classified accordingto their sequence of ports, called the _interaction
type_ and
let$\mathsf{Inter}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathcal{P}^{+}$
be the set of interaction types; aninteraction type models, for instance, the
passing of a certain kindof message (e.g., request, acknowledgement,
etc.).From an operational point of view, two interactions that differ by
apermutation of indices e.g., $(c_{1},p_{1},\ldots,c_{n},p_{n})$
and$(c_{i_{1}},p_{i_{1}},\ldots,c_{i_{n}},p_{i_{n}})$ such that
$\\{{i_{1},\ldots,i_{n}}\\}=[{1},{n}]$, are equivalent, since the set
oftransitions is the same; nevertheless, we chose to distinguish them inthe
following, exclusively for reasons of simplicity.Note that Def. 1 allows
configurations withinteractions that involve absent components (i.e., not from
the set$\mathcal{C}$ of present components in the given configuration).
Thefollowing definition distinguishes such configurations:

###### Definition 2

Let $\gamma=(\mathcal{C},\mathcal{I},\varrho)$ be a configuration.
Aninteraction $(c_{1},p_{1},\ldots,c_{n},p_{n})$ is _loose_ in$\gamma$ if and
only if $c_{i}\not\in\mathcal{C}$, for some $i\in[{1},{n}]$. If $\mathcal{I}$
contains at least one interactionthat is loose in $\gamma$, we say that
$\gamma$ is _loose_. An interaction (resp. configuration) that is not looseis
said to be _tight_.

For instance, every configuration of the system fromFig. 1 (a) is tight and
becomes loose if a component isdeleted. Moreover, the reconfiguration program
fromFig. 1 (c) manipulates tight configurations only. Inparticular, loose
configurations are useful for the definition of acomposition operation, as the
union of disjoint sets of components andinteractions:

###### Definition 3

The composition of two configurations
$\gamma_{i}=(\mathcal{C}_{i},\mathcal{I}_{i},\varrho)$, for $i=1,2$, such that
$\mathcal{C}_{1}\cap\mathcal{C}_{2}=\emptyset$ and
$\mathcal{I}_{1}\cap\mathcal{I}_{2}=\emptyset$, is defined as
$\gamma_{1}\bullet\gamma_{2}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}(\mathcal{C}_{1}\cup\mathcal{C}_{2},\mathcal{I}_{1}\cup\mathcal{I}_{2},\varrho)$.
The composition $\gamma_{1}\bullet\gamma_{2}$ isundefined if
$\mathcal{C}_{1}\cap\mathcal{C}_{2}\neq\emptyset$ or
$\mathcal{I}_{1}\cap\mathcal{I}_{2}\neq\emptyset$.

Note that a tight configuration may be the result of composing twoloose
configurations, whereas the composition of tight configurationsis always
tight. The example below shows that, in most cases, anon-trivial decomposition
of a tight configuration necessarilyinvolves loose configurations:

###### Example 1

Let $\gamma_{i}=(\mathcal{C}_{i},\mathcal{I}_{i},\varrho)$ be
looseconfigurations, where $\mathcal{C}_{i}=\\{{c_{i}}\\}$,
$\mathcal{I}_{i}=\\{{(c_{i},\mathit{out},c_{3-i},\mathit{in})}\\}$, for all
$i=1,2$. Then
$\gamma\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\gamma_{1}\bullet\gamma_{2}$
is thetight configuration
$\gamma=(\\{{c_{1},c_{2}}\\},\\{{(c_{1},\mathit{out},c_{2},\mathit{in}),(c_{2},\mathit{out},c_{1},\mathit{in})}\\},\varrho)$.
The only way of decomposing $\gamma$into two tight subconfigurations
$\gamma^{\prime}_{1}$ and $\gamma^{\prime}_{2}$ istaking
$\gamma^{\prime}_{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\gamma$
and
$\gamma^{\prime}_{2}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}(\emptyset,\emptyset,\varrho)$,
orviceversa. $\blacksquare$

In analogy with graphs, the _degree_ of a configuration isthe maximum number
of interactions from the configuration that involvea (possibly absent)
component:

###### Definition 4

The _degree_ of a configuration $\gamma=(\mathcal{C},\mathcal{I},\varrho)$ is
defined as
$\delta({\gamma})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\max_{c\in\mathbb{C}}\delta_{c}({\gamma})$,
where$\delta_{c}({\gamma})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}|\\!|{\\{(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{I}\mid
c=c_{i},~{}i\in[{1},{n}]\\}}|\\!|$.

For instance, the configuration of the system from Fig. 1(a) has degree two.

###  2.2 Configuration Logic

Let $\mathbb{V}$ and $\mathbb{A}$ be countably infinite sets of _variables_
and _predicates_ , respectively. For eachpredicate $\mathsf{A}\in\mathbb{A}$,
we denote its arity by$\\#{\mathsf{A}}$. The formulæ of the _Configuration
Logic_(CL) are described inductively by the following syntax:

$\phi:=\mathsf{emp}\mid[{x}]\mid\langle{{x_{1}}.\mathit{p_{1}},\ldots,{x_{n}}.\mathit{p_{n}}}\rangle\mid{x}@{q}\mid
x=y\mid x\neq
y\mid\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\mid\phi*\phi\mid\exists
x~{}.~{}\phi$

where $x,y,x_{1},\ldots\in\mathbb{V}$, $q\in\mathcal{Q}$ and
$\mathsf{A}\in\mathbb{A}$. A formula$[{x}]$,
$\langle{{x_{1}}.\mathit{p_{1}},\ldots,{x_{n}}.\mathit{p_{n}}}\rangle$,
${x}@{q}$ and$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$ is called a
_component_ , _interaction_ , _state_ and _predicate_ atom, respectively.
Sometimes, we use the
shorthand${[{x}]}@{q}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}[{x}]*{x}@{q}$.
Intuitively,the formula
${[{x}]}@{q}*{[{y}]}@{q^{\prime}}*\langle{{x}.\mathit{out},{y}.\mathit{in}}\rangle*\langle{{x}.\mathit{in},{y}.\mathit{out}}\rangle$
describes aconfiguration consisting of two distinct components, denoted by
thevalues of $x$ and $y$, in states $q$ and $q^{\prime}$, respectively, and
twointeractions binding the $\mathit{out}$ port of one to the$\mathit{in}$
port of the other component. Forinstance, $\gamma=\gamma_{1}\bullet\gamma_{2}$
from Example1 is such a configuration. A formula is said to be _pure_ if and
only if it consists ofstate atoms, equalities and disequalities. A formula
with nooccurrences of predicate atoms (resp. existential quantifiers) iscalled
_predicate-free_ (resp. _quantifier-free_). Avariable is _free_ if it does not
occur within the scope of anexistential quantifier and let
$\mathrm{fv}({\phi})$ be the set of freevariables of $\phi$. A _sentence_ is a
formula with no freevariables. A _substitution_ $\phi[x_{1}/y_{1}\ldots
x_{n}/y_{n}]$replaces simultaneously every free occurrence of $x_{i}$ by
$y_{i}$ in$\phi$, for all $i\in[{1},{n}]$. Before defining the semanticsof CL
formulæ, we introduce the set of inductive definitionsthat assigns meaning to
predicates:

###### Definition 5

A _set of inductive definitions (SID)_ $\Delta$ consists of _rules_
$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\phi$, where
$x_{1},\ldots,x_{\\#{\mathsf{A}}}$ are pairwisedistinct variables, called
_parameters_ , such that
$\mathrm{fv}({\phi})\subseteq\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}$. The
rule$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\phi$_defines_
$\mathsf{A}$ and we denote by $\mathrm{def}_{\Delta}({\mathsf{A}})$ theset of
rules from $\Delta$ that define $\mathsf{A}$.

Note that having distinct parameters in a rule is without loss ofgenerality,
as e.g., a rule $\mathsf{A}(x_{1},x_{1})\leftarrow\phi$ can beequivalently
written as $\mathsf{A}(x_{1},x_{2})\leftarrow x_{1}=x_{2}*\phi$. As a
convention, we shall always use the names $x_{1},\ldots,x_{\\#{\mathsf{A}}}$
for the parameters of a rule that defines$\mathsf{A}$.The semantics of CL
formulæ is defined by a satisfactionrelation
$\gamma\models^{\nu}_{\Delta}\phi$ between configurationsand formulæ. This
relation is parameterized by a _store_ $\nu:\mathbb{V}\rightarrow\mathbb{C}$
mapping the free variables of aformula into components from the universe
(possibly absent from$\gamma$) and an SID $\Delta$. We write $\nu[x\leftarrow
c]$ forthe store that maps $x$ into $c$ and agrees with $\nu$ on allvariables
other than $x$. The definition of the satisfaction relationis by induction on
the structure of formulæ, where $\gamma=(\mathcal{C},\mathcal{I},\varrho)$ is
a configuration(Def. 1):

$\begin{array}[]{rclcl}\gamma&\models^{\nu}_{\Delta}&\mathsf{emp}&\iff&\mathcal{C}=\emptyset\text{
and }\mathcal{I}=\emptyset\\\
\gamma&\models^{\nu}_{\Delta}&[{x}]&\iff&\mathcal{C}=\\{{\nu(x)}\\}\text{ and
}\mathcal{I}=\emptyset\\\
\gamma&\models^{\nu}_{\Delta}&\langle{{x_{1}}.\mathit{p_{1}},\ldots,{x_{n}}.\mathit{p_{n}}}\rangle&\iff&\mathcal{C}=\emptyset\text{
and }\mathcal{I}=\\{{(\nu(x_{1}),p_{1},\ldots,\nu(x_{n}),p_{n})}\\}\\\
\gamma&\models^{\nu}_{\Delta}&{x}@{q}&\iff&\gamma\models^{\nu}_{\Delta}\mathsf{emp}\text{
and }\varrho(\nu(x))=q\\\ \gamma&\models^{\nu}_{\Delta}&x\sim
y&\iff&\gamma\models^{\nu}_{\Delta}\mathsf{emp}\text{ and
}\nu(x)\sim\nu(y)\text{, for all }\sim\in\\{{=,\neq}\\}\\\
\gamma&\models^{\nu}_{\Delta}&\mathsf{A}(y_{1},\ldots,y_{\\#{\mathsf{A}}})&\iff&\gamma\models^{\nu}_{\Delta}\phi[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]\text{,
for some rule }\\\
&&&&\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\phi\text{ from
}\Delta\\\ \gamma&\models^{\nu}_{\Delta}&\phi_{1}*\phi_{2}&\iff&\text{exist
}\gamma_{1},\gamma_{2}\text{, such that
}\gamma=\gamma_{1}\bullet\gamma_{2}\text{ and
}\gamma_{i}\models^{\nu}_{\Delta}\phi_{i}\text{, for }i=1,2\\\
\gamma&\models^{\nu}_{\Delta}&\exists
x~{}.~{}\phi&\iff&\gamma\models^{\nu[x\leftarrow c]}_{\Delta}\phi\text{, for
some }c\in\mathbb{C}\end{array}$

If $\phi$ is a sentence, the satisfaction relation
$\gamma\models^{\nu}_{\Delta}\phi$ does not depend on the store,
written$\gamma\models_{\Delta}\phi$, in which case we say that $\gamma$ isa
_model_ of $\phi$. If $\phi$ is a predicate-free formula, thesatisfaction
relation does not depend on the SID, written $\gamma\models^{\nu}\phi$. A
formula $\phi$ is _satisfiable_ if andonly if the sentence $\exists
x_{1}\ldots\exists x_{n}~{}.~{}\phi$ has amodel, where
$\mathrm{fv}({\phi})=\\{{x_{1},\ldots,x_{n}}\\}$. A formula $\phi$_entails_ a
formula $\psi$, written $\phi\models_{\Delta}\psi$ ifand only if, for any
configuration $\gamma$ and store $\nu$, wehave
$\gamma\models^{\nu}_{\Delta}\phi$ only if $\gamma\models^{\nu}_{\Delta}\psi$.

###  2.3 Separation Logic

Separation Logic (SL) [Reynolds02] will be used in thefollowing to prove
several technical results concerning thedecidability and complexity of certain
decision problems for CL. Forself-containment reasons, we define SL below. The
syntax ofSL formulæ is described by the following grammar:

$\phi:=\mathsf{emp}\mid x_{0}\mapsto(x_{1},\ldots,x_{\mathfrak{K}})\mid
x=y\mid x\neq
y\mid\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\mid\phi*\phi\mid\exists
x~{}.~{}\phi$

where $x,y,x_{0},x_{1},\ldots\in\mathbb{V}$, $\mathsf{A}\in\mathbb{A}$ and
$\mathfrak{K}\geq 1$ is aninteger constant. Formulæ of SL are interpreted over
finitepartial functions
$\mathsf{h}:\mathbb{C}\rightharpoonup_{\scriptscriptstyle\mathit{fin}}\mathbb{C}^{\mathfrak{K}}$,
called _heaps_ 222We use the universe $\mathbb{C}$ here forsimplicity, the
definition works with any countably infinite set., bya satisfaction relation
$\mathsf{h}\Vdash^{\nu}\phi$, definedinductively as follows:

$\begin{array}[]{rclcl}\mathsf{h}&\Vdash^{\nu}_{\Delta}&\mathsf{emp}&\iff&\mathsf{h}=\emptyset\\\
\mathsf{h}&\Vdash^{\nu}_{\Delta}&x_{0}\mapsto(x_{1},\ldots,x_{\mathfrak{K}})&\iff&\mathrm{dom}({\mathsf{h}})=\\{{\nu(x_{0})}\\}\text{
and
}\mathsf{h}(\nu(x_{0}))=\langle{\nu(x_{1}),\ldots,\nu(x_{\mathfrak{K}})}\rangle\\\
\mathsf{h}&\Vdash^{\nu}&\phi_{1}*\phi_{2}&\iff&\text{there exist
}\mathsf{h}_{1},\mathsf{h}_{2}\text{ such that
}\mathrm{dom}({\mathsf{h}_{1}})\cap\mathrm{dom}({\mathsf{h}_{2}})=\emptyset,\\\
&&&&\mathsf{h}=\mathsf{h}_{1}\cup\mathsf{h}_{2}\text{ and
}\mathsf{h}_{i}\Vdash^{\nu}_{\Delta}\phi_{i}\text{, for both }i=1,2\\\
\end{array}$

where
$\mathrm{dom}({\mathsf{h}})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{c\in\mathbb{C}\mid\mathsf{h}(c)\text{
isdefined}}\\}$ is the domain of the heap and (dis-)equalities,predicate atoms
and existential quantifiers are defined same as forCL.

###  2.4 Decision Problems

We define the decision problems that are the focus of the upcomingsections. As
usual, a decision problem is a class of yes/no queriesthat differ only in
their input. In our case, the input consists of anSID and one or two
predicates, written between square brackets.

###### Definition 6

We consider the following problems, for a SID $\Delta$ and
predicates$\mathsf{A},\mathsf{B}\in\mathbb{A}$:

  1. 1.

$\mathsf{Sat}[{\Delta},{\mathsf{A}}]$: is the sentence$\exists
x_{1}\ldots\exists
x_{\\#{\mathsf{A}}}~{}.~{}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$
satisfiable for $\Delta$?

  2. 2.

$\mathsf{Tight}[{\Delta},{\mathsf{A}}]$: is every model$\gamma$ of the
sentence $\exists x_{1}\ldots\exists
x_{\\#{\mathsf{A}}}~{}.~{}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$ a
tight configuration?

  3. 3.

$\mathsf{Bnd}[{\Delta},{\mathsf{A}}]$: is the
set$\\{{\delta({\gamma})\mid\gamma\models_{\Delta}\exists x_{1}\ldots\exists
x_{\\#{\mathsf{A}}}~{}.~{}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})}\\}$
finite?

  4. 4.

$\mathsf{Entl}[{\Delta},{\mathsf{A}},{\mathsf{B}}]$:
does$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\models_{\Delta}\exists
x_{\\#{\mathsf{B}}+1}\ldots\exists
x_{\\#{\mathsf{A}}}~{}.~{}\mathsf{B}(x_{1},\ldots,x_{\\#{\mathsf{B}}})$ hold?

We define the size of a formula $\phi$ as the total number ofoccurrences of
symbols needed to write it down, denoted by$\mathrm{size}({\phi})$. The size
of a SID $\Delta$ is
$\mathrm{size}({\Delta})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\sum_{\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\phi\in\Delta}\mathrm{size}({\phi})+\\#{\mathsf{A}}+1$.
Other parameters of aSID $\Delta$ are its:

  * •

_maximal arity_ , denoted as
$\mathrm{arity}({\Delta})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\max\\{{\\#{\mathsf{A}}\mid\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\phi\in\Delta}\\}$,

  * •

_width_ , denoted as
$\mathrm{width}({\Delta})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\max\\{{\mathrm{size}({\phi})\mid\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\phi\in\Delta}\\}$,

  * •

_maximal interaction size_ , denoted
as$\mathrm{intersize}({\Delta})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\max\\{n\mid\langle{{x_{1}}.\mathit{p_{1}},\ldots,{x_{n}}.\mathit{p_{n}}}\rangle\text{
occurs in }\phi,\\\
\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\phi\in\Delta\\}$.

For each decision problem $\mathsf{P}[{\Delta},{\mathsf{A},\mathsf{B}}]$, we
considerits $(k,\ell)$-bounded
versions$\mathsf{P}^{({k},{\ell})}[{\Delta},{\mathsf{A},\mathsf{B}}]$,
obtained by restricting thepredicates and interaction atoms occurring $\Delta$
to$\mathrm{arity}({\Delta})\leq k$ and
$\mathrm{intersize}({\Delta})\leq\ell$,respectively, where $k$ and $\ell$ are
either positive integers orinfinity. We consider, for each
$\mathsf{P}[{\Delta},{\mathsf{A},\mathsf{B}}]$, thesubproblems
$\mathsf{P}^{({k},{\ell})}[{\Delta},{\mathsf{A},\mathsf{B}}]$ corresponding
tothe three cases  (1) $k<\infty$and$\ell=\infty$,  (2) $k=\infty$and
$\ell<\infty$, and  (3) $k=\infty$and $\ell=\infty$.  As we explain next,this
is because, for the decision problems considered(Def. 6), the complexity for
the case $k<\infty,\ell<\infty$ matches the one for the case
$k<\infty,\ell=\infty$.Moreover, for each problem
$\mathsf{P}[{\Delta},{\mathsf{A}}]$(resp.
$\mathsf{P}[{\Delta},{\mathsf{A},\mathsf{B}}]$), we consider its general
version$\mathsf{P}[{\Delta},{\phi}]$ (resp.
$\mathsf{P}[{\Delta},{\phi,\psi}]$), where $\phi$and $\psi$ are CL formulæ,
whose predicates are interpreted bythe rules in $\Delta$. The generalized
problems $\mathsf{P}[{\Delta},{\phi}]$involving one predicate atom (points 1
and3 of Def. 6) can be reduced totheir restricted versions
$\mathsf{P}[{\Delta},{\mathsf{A}}]$, by introducing afresh predicate
$\mathsf{A}_{\phi}$ (not occurring in $\Delta$), of arity$n\geq 0$ and a rule
$\mathsf{A}_{\phi}(x_{1},\ldots,x_{n})\leftarrow\phi$,where
$\mathrm{fv}({\phi})=\\{{x_{1},\ldots,x_{n}}\\}$. This reduction is linearin
the size of the input and changes none of the following complexityresults.
Concerning the generalized entailment
problem$\mathsf{Entl}[{\Delta},{\phi},{\psi}]$, the reduction to the
problem$\mathsf{Entl}[{\Delta},{\mathsf{A}},{\mathsf{B}}]$ (Def. 64) might
affect its decidability status, which issubject to syntactic restrictions on
the rules in $\Delta$ (detailswill be given in
§LABEL:sec:entailment).Satisfiability (1) and entailment(4) arise naturally
during verification ofreconfiguration programs. For instance,
$\mathsf{Sat}[{\Delta},{\phi}]$ askswhether a specification $\phi$ of a set
configurations (e.g., a pre-,post-condition, or a loop invariant) is empty or
not (e.g., an emptyprecondition typically denotes a vacuous verification
condition),whereas $\mathsf{Entl}[{\Delta},{\phi},{\psi}]$ is used as a side
condition for theHoare rule of consequence, as in e.g., the proof fromFig. 1
(c). Moreover, entailments must be proved whenchecking inductiveness of a
user-provided loop invariant.In contrast, the applications of the tightness
(2)and boundedness (3) problems are less obvious andrequire a few
explanations. The $\mathsf{Tight}[{\Delta},{\phi}]$ problem isrelevant in the
context of compositional verification of distributedsystems. Suppose we have a
distributed system consisting of twointeracting subsystems, whose sets of
initial configurations aredescribed by $\phi_{1}$ and $\phi_{2}$, respectively
i.e., the initialconfigurations of the system are described by
$\phi_{1}*\phi_{2}$. Thecompositional verification of a reconfiguration
program $\mathsf{P}$reduces checking the validity of a Hoare triple
$\\{{\phi_{1}*\phi_{2}}\\}~{}\mathsf{P}~{}\\{{\psi_{1}*\psi_{2}}\\}$ to
checking the validity of the
simpler$\\{{\phi_{i}}\\}~{}\mathsf{P}~{}\\{{\psi_{i}}\\}$, for $i=1,2$.
Unfortunately, thisappealing method faces the problem of _interference_
between thesubsystems described by $\phi_{1}$ and $\phi_{2}$, namely the
looseinteractions of $\phi_{i}$ might connect to present components
of$\phi_{3-i}$ and change their states during the execution. In thiscase, it
is sufficient to infer the sets of cross-boundaryinteractions
$\mathcal{F}_{i,3-i}$, describing those interactions from$\phi_{i}$ that
connect to components from $\phi_{3-i}$, and check thevalidity of the triples
$\\{{\phi_{i}*\mathcal{F}_{3-i,i}}\\}~{}\mathsf{P}~{}\\{{\psi_{i}*\mathcal{F}_{3-i,i}}\\}$,
under arelaxed semantics which considers that the interactions
in$\mathcal{F}_{3-i,i}$ can fire anytime, or according to the orderdescribed
by some regular language. However, if$\mathsf{Tight}[{\Delta},{\phi_{1}}]$
(resp. $\mathsf{Tight}[{\Delta},{\phi_{2}}]$) has a negativeanswer, the set of
cross-boundary interactions may be unbounded, hencenot representable by a
finite separating conjunction of interactionatoms $\mathcal{F}_{1,2}$ (resp.
$\mathcal{F}_{2,1}$). Thus, thetightness problem is important in establishing
necessary conditionsunder which a compositional proof rule can be applied to
checkingcorrectness of reconfigurations in a distributed system.The
$\mathsf{Bnd}[{\Delta},{\phi}]$ problem is used to check a necessarycondition
for the decidability of entailments
i.e.,$\mathsf{Entl}[{\Delta},{\phi},{\psi}]$. If
$\mathsf{Bnd}[{\Delta},{\phi}]$ has a positiveanswer, we can reduce the
problem $\mathsf{Entl}[{\Delta},{\phi},{\psi}]$ to anentailment problem for
SL, which is always interpreted over heapsof bounded degree
[EchenimIosifPeltier21]. Otherwise, thedecidability status of the entailment
problem is open, forconfigurations of unbounded degree, such as the one
described by theexample below.

###### Example 2

The following SID describes star topologies with a centralcontroller connected
to an unbounded number of workers stations:

$\mathit{Star}(x)\leftarrow[{x}]*\mathit{Worker}(x),~{}\mathit{Worker}(x)\leftarrow\mathsf{emp}\mid\exists
y~{}.~{}\langle{{x}.\mathit{out},{y}.\mathit{in}}\rangle*[{y}]*\mathit{Worker}(x)~{}\blacksquare$

##  3 Satisfiability

We show that the satisfiability problem (Def. 6,point 1) is decidable, using a
method similar to theone pioneered by Brotherston etal.
[DBLP:conf/csl/BrotherstonFPG14], for checking satisfiabilityof inductively
defined symbolic heaps in SL. We recall that aformula $\pi$ is _pure_ if and
only if it is a separatingconjunction of equalities, disequalities and state
atoms.

###### Definition 7

The _closure_ $\mathrm{cl}({\pi})$ of a pure formula$\pi$ is the limit of the
sequence $\pi^{0},\pi^{1},\pi^{2},\ldots$ such that $\pi^{0}=\pi$ and, foreach
$i\geq 0$, $\pi^{i+1}$ is obtained by joining (with $*$)all of the following
formulæ to$\pi^{i}$:

  * •

$x=z$, where $x$ and $z$ are the same variable, or $x=y$and $y=z$ both occur
in $\pi^{i}$,

  * •

$x\neq z$, where $x=y$ and $y\neq z$ both occur in$\pi^{i}$, or

  * •

${y}@{q}$, where ${x}@{q}$ and $x=y$ both occurin $\pi^{i}$.

Because only finitely many such formulæ can be added, the sequenceof pure
formulæ from Def. 7 is bound to stabilizeafter polynomially many steps. A pure
formula is satisfiable if andonly if its closure does not contain
contradictory literals i.e., $x=y$ and $x\neq y$, or ${x}@{q}$ and
${x}@{q^{\prime}}$, for $q\neq q^{\prime}\in\mathcal{Q}$. We write
$x\approx_{\pi}y$ (resp. $x~{}{\not\approx}_{\pi}y$) if and only if $x=y$
(resp. $x\neq y$)occurs in $\mathrm{cl}({\pi})$ and
$\mathrm{not}(x\approx_{\pi}y)$(resp.
$\mathrm{not}(x~{}{\not\approx}_{\pi}y)$) whenever $x\approx_{\pi}y$ (resp.
$x{\not\approx}_{\pi}y$) does not hold.Note that e.g.,
$\mathrm{not}(x\approx_{\pi}y)$ is not the same as
$x~{}{\not\approx}_{\pi}y$.A pure formula $\pi$ is satisfiable if and only if
thefollowing hold:

  1. 1.

for all $x,y\in\mathrm{fv}({\pi})$, $x=y$ and $x\neq y$ do notoccur both in
$\mathrm{cl}({\pi})$,

  2. 2.

for all $x\in\mathrm{fv}({\pi})$ and $q\neq r\in\mathcal{Q}$,${x}@{q}$ and
${x}@{r}$ do not occur both in$\mathrm{cl}({\pi})$.

A pure formula $\pi$ is satisfiable if and only if thereexists a store $\nu$
and a configuration $(\emptyset,\emptyset,\varrho)$, such that
$(\emptyset,\emptyset,\varrho)\models^{\nu}\pi$. “$\Leftarrow$” It is easy to
see that$\approx_{\pi}$ is an equivalence relation, for each pureformula
$\pi$. Given any state map $\varrho$, we define$\nu$ by assigning each
equivalence class of $\approx_{\pi}$a distinct component $c$, such that
$\varrho(c)=q$ if${y}@{q}$ occurs in $\pi$, for a variable $y$ in theclass. By
the conditions of the Lemma, $\varrho$ and $\nu$ arewell defined and we have
$(\emptyset,\emptyset,\varrho)\models^{\nu}\pi$, by definition.
“$\Rightarrow$” If$(\emptyset,\emptyset,\varrho)\models^{\nu}\pi$
then$(\emptyset,\emptyset,\varrho)\models^{\nu}\mathrm{cl}({\pi})$, because
each additional formula in$\mathrm{cl}({\pi})$ is a logical consequence
of$\pi$. Since $\mathrm{cl}({\pi})$ is satisfiable, the twoconditions of the
Lemma must hold. ∎ _Base tuples_ constitute the abstract domain used by
thealgorithms for checking satisfiability (point 1 ofDef. 6) and boundedness
(point 3of Def. 6), defined as follows:

###### Definition 8

A _base tuple_ is a triple
$\mathfrak{t}=(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)$, where:

  * •

$\mathcal{C}^{\sharp}\in\mathrm{mpow}({\mathbb{V}})$ is a multiset of
variablesdenoting present components,

  * •

$\mathcal{I}^{\sharp}:\mathsf{Inter}\rightarrow\mathrm{mpow}({\mathbb{V}^{+}})$
mapseach interaction type $\tau\in\mathsf{Inter}$ into a multisetof tuples of
variables of length $|{\tau}|$ each, and

  * •

$\pi$ is a pure formula.

A base tuple is called _satisfiable_ if and only if $\pi$ issatisfiable and
the following hold:

  1. 1.

for all $x,y\in\mathcal{C}^{\sharp}$, $\mathrm{not}(x\approx_{\pi}y)$,

  2. 2.

for all $\tau\in\mathsf{Inter}$,
$\langle{x_{1},\ldots,x_{|{\tau}|}}\rangle,\langle{y_{1},\ldots,y_{|{\tau}|}}\rangle\in\mathcal{I}^{\sharp}(\tau)$,
thereexists $i\in[{1},{|{\tau}|}]$ such
that$\mathrm{not}(x_{i}\approx_{\pi}y_{i})$,

  3. 3.

for all
$\tau\in\mathsf{Inter}$,$\langle{x_{1},\ldots,x_{\\#{\tau}}}\rangle\in\mathcal{I}^{\sharp}(\tau)$
and $1\leq i<j\leq|{\tau}|$, we have $\mathrm{not}(x_{i}\approx_{\pi}x_{j})$.

We denote by $\mathsf{SatBase}$ the set of satisfiable base tuples.

Note that a base tuple $(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)$ is
unsatisfiable if $\mathcal{C}^{\sharp}$($\mathcal{I}^{\sharp}$) contains the
same variable (tuple of variables)twice (for the same interaction type), hence
the use of multisets inthe definition of base tuples. It is easy to see that
checking thesatisfiability of a given base tuple
$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)$ can be done in
time$\mathit{poly}(|\\!|{\mathcal{C}^{\sharp}}|\\!|+\sum_{\tau\in\mathsf{Inter}}|\\!|{\mathcal{I}^{\sharp}(\tau)}|\\!|+\mathrm{size}({\pi}))$.We
define a partial _composition_ operation on satisfiable base tuples, as
follows:

$(\mathcal{C}^{\sharp}_{1},\mathcal{I}^{\sharp}_{1},\pi_{1})\otimes(\mathcal{C}^{\sharp}_{2},\mathcal{I}^{\sharp}_{2},\pi_{2})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}(\mathcal{C}^{\sharp}_{1}\cup\mathcal{C}^{\sharp}_{2},\mathcal{I}^{\sharp}_{1}\cup\mathcal{I}^{\sharp}_{2},\pi_{1}*\pi_{2})$

where the union of multisets is lifted to functions
$\mathsf{Inter}\rightarrow\mathrm{mpow}({\mathbb{V}^{+}})$ in the usual way.
The compositionoperation $\otimes$ is undefined if
$(\mathcal{C}^{\sharp}_{1},\mathcal{I}^{\sharp}_{1},\pi_{1})\otimes(\mathcal{C}^{\sharp}_{2},\mathcal{I}^{\sharp}_{2},\pi_{2})$is
not satisfiable e.g., if
$\mathcal{C}^{\sharp}_{1}\cap\mathcal{C}^{\sharp}_{2}\neq\emptyset$,
$\mathcal{I}^{\sharp}_{1}(\tau)\cap\mathcal{I}^{\sharp}_{2}(\tau)\neq\emptyset$,
for some$\tau\in\mathsf{Inter}$, or $\pi_{1}*\pi_{2}$ is notsatisfiable.Given
a pure formula $\pi$ and a set of variables $X$, theprojection
${\pi}\\!\\!\downarrow_{\scriptscriptstyle{X}}$ removes from $\pi$ all
atomicpropositions $\alpha$, such that $\mathrm{fv}({\alpha})\not\subseteq X$.
The _projection_ of a base
tuple$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)$ on a variable set $X$
isformally defined below:

$\begin{array}[]{rcl}{(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)}\\!\\!\downarrow_{\scriptscriptstyle{X}}&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\left(\mathcal{C}^{\sharp}\cap
X,\lambda\tau~{}.~{}\\{{\langle{x_{1},\ldots,x_{|{\tau}|}}\rangle\in\mathcal{I}^{\sharp}(\tau)\mid
x_{1},\ldots,x_{|{\tau}|}\in
X}\\},{\mathrm{cl}({\mathrm{dist}({\mathcal{I}^{\sharp}})*\pi})}\\!\\!\downarrow_{\scriptscriptstyle{X}}\right)\\\
\text{where
}\mathrm{dist}({\mathcal{I}^{\sharp}})&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\tau\in\mathsf{Inter}}\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\langle{x_{1},\ldots,x_{|{\tau}|}}\rangle\in\mathcal{I}^{\sharp}(\tau)}\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{1\leq i<j\leq|{\tau}|}~{}x_{i}\neq x_{j}\end{array}$

The _substitution_ operation
$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)[x_{1}/y_{1},\ldots,x_{n}/y_{n}]$
replaces simultaneously each$x_{i}$ with $y_{i}$ in $\mathcal{C}^{\sharp}$,
$\mathcal{I}^{\sharp}$ and $\pi$,respectively.For a store $\nu$, we denote by
$\nu[x_{1}/y_{1},\ldots,x_{n}/y_{n}]$ thestore such that
$\nu[x_{1}/y_{1},\ldots,x_{n}/y_{n}](x_{i})=\nu(y_{i})$ andagrees with $\nu$
over $\mathbb{V}\setminus\\{{x_{1},\ldots,x_{n}}\\}$.We lift the composition,
projection and substitution operations tosets of satisfiable base tuples, as
usual.Given a formula $\phi$ and a substitution
$\sigma=[x_{1}/y_{1},\ldots,x_{n}/y_{n}]$, for any configuration
$(\mathcal{C},\mathcal{I},\varrho)$ and store $\nu$,
$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\phi\sigma$ only
if$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu\sigma}\phi$.By induction on
the definition of $\models^{\nu}_{\Delta}$. ∎Next, we define the base tuple
corresponding to a quantifier- andpredicate-free formula $\phi=\psi*\pi$,
where $\psi$consists of component and interaction atoms and $\pi$ is
pure.Since, moreover, we are interested in those components andinteractions
that are visible through a given indexed set ofparameters
$X=\\{{x_{1},\ldots,x_{n}}\\}$, for a variable $y$, we denoteby
${\\{\\!\\!\\{{y}\\}\\!\\!\\}}^{\scriptscriptstyle{X}}_{\pi}$ the parameter
$x_{i}$ with the leastindex, such that $y\approx_{\pi}x_{i}$, or $y$ itself,
if no suchparameter exists. We define the following sets of formulæ:

$\begin{array}[]{rcl}\mathsf{Base}({\phi},{X})&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\left\\{\begin{array}[]{ll}\\{{(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)}\\}&\text{,
if }(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)\text{ is satisfiable}\\\
\emptyset&\text{, otherwise}\end{array}\right.\\\ \text{where
}\mathcal{C}^{\sharp}&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\\{{{\\{\\!\\!\\{{x}\\}\\!\\!\\}}^{\scriptscriptstyle{X}}_{\pi}\mid[{x}]\text{
occurs in }\psi}\\}\\\
\mathcal{I}^{\sharp}&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\lambda\langle{p_{1},\ldots,p_{s}}\rangle.\left\\{{\left\langle{{\\{\\!\\!\\{{y_{1}}\\}\\!\\!\\}}^{\scriptscriptstyle{X}}_{\pi},\ldots,{\\{\\!\\!\\{{y_{s}}\\}\\!\\!\\}}^{\scriptscriptstyle{X}}_{\pi}}\right\rangle\mid\langle{{y_{1}}.\mathit{p_{1}},\ldots,{y_{s}}.\mathit{p_{s}}}\rangle\text{
occurs in }\psi}\right\\}\end{array}$

We consider a tuple of variables $\overrightarrow{\mathcal{X}}$, having a
variable$\mathcal{X}({\mathsf{A}})$ ranging over
$\mathrm{pow}({\mathsf{SatBase}})$, for eachpredicate $\mathsf{A}$ that occurs
in $\Delta$. With these definitions,each rule of $\Delta$:

$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathsf{B}_{1}(z^{1}_{1},\ldots,z^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(z^{h}_{1},\ldots,z^{h}_{\\#{\mathsf{B}_{h}}})$

where $\phi$ is a quantifier- and predicate-free formula, induces
theconstraint:

$\mathcal{X}({\mathsf{A}})\supseteq{\big{(}\mathsf{Base}({\phi},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})\otimes\bigotimes_{\ell=1}^{h}\mathcal{X}({\mathsf{B}_{\ell}})[x_{1}/z^{\ell}_{1},\ldots,x_{\\#{\mathsf{B}_{\ell}}}/z^{\ell}_{\\#{\mathsf{B}_{\ell}}}]\big{)}}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$
(1)

Let $\Delta^{\sharp}$ be the set of suchconstraints, corresponding to the
rules in $\Delta$ and let$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}$ be
the tuple of least solutions of the constraint systemgenerated from $\Delta$,
indexed by the tuple of predicates that occurin $\Delta$, such that
$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})$ denotes the
entry of$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}$ correponding to
$\mathsf{A}$. Since the composition andprojection are monotonic operations,
such a least solution exists andis unique. Moreover, since $\mathsf{SatBase}$
is finite, the leastsolution can be attained in a finite number of steps,
using a standardKleene iteration(see Fig. 2).

input: a SID $\Delta$

output: $\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}$

1:initially
$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}:=\lambda\mathsf{A}~{}.~{}\emptyset$

2:for $\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists y_{m}~{}.~{}\phi\in\Delta$, with $\phi$ quantifier- and
predicate-free do

3:
$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}}):=\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})\cup{\mathsf{Base}({\phi},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$

4:while $\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}$ still change do

5: for
$\mathsf{r}:\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathop{\scalebox{1.9}{\raisebox{-0.77498pt}{$\ast$}}}\hskip
1.0pt_{\ell=1}^{h}\mathsf{B}_{\ell}(z^{\ell}_{1},\ldots,z^{\ell}_{\\#{\mathsf{B}_{\ell}}})\in\Delta$
do

6: if there exist
$\mathfrak{t}_{1}\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{B}_{1}}),\ldots,\mathfrak{t}_{h}\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{B}_{h}})$
then

7:
$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}}):=\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})~{}\cup~{}{\left(\mathsf{Base}({\phi},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})\otimes\bigotimes_{\ell=1}^{h}\mathfrak{t}_{\ell}[x_{1}/z^{\ell}_{1},\ldots,x_{\\#{\mathsf{B}_{\ell}}}/z^{\ell}_{\\#{\mathsf{B}_{\ell}}}]\right)}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$

Figure 2: Algorithm for the Computation of the Least Solution

Given a base tuple $(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)$ and
astore $\nu$, we define the following sets of components andinteractions,
respectively:

$\displaystyle\nu(\mathcal{C}^{\sharp})$
$\displaystyle\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\nu(x)\mid
x\in\mathcal{C}^{\sharp}}\\}$ $\displaystyle\nu(\mathcal{I}^{\sharp})$
$\displaystyle\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\bigcup_{\langle{p_{1},\ldots,p_{n}}\rangle\in\mathsf{Inter}}\\{{(\nu(x_{1}),p_{1},\ldots,\nu(x_{n}),p_{n})\mid(x_{1},\ldots,x_{n})\in\mathcal{I}^{\sharp}(\langle{p_{1},\ldots,p_{n}}\rangle)}\\}$

We state below the main result leading to an elementary recursivealgorithm for
the satisfiability problem (Thm. 3).Given a base tuple
$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]$,
a state map$\varrho$ and a store $\nu$ such that
$(\emptyset,\emptyset,\varrho)\models^{\nu}\pi$, a set of
components$\mathcal{D}$ disjoint from $\nu(\mathcal{C}^{\sharp})$ and a set
ofinteractions $\mathcal{J}$ disjoint from $\nu(\mathcal{I}^{\sharp})$,there
exists a configuration $(\mathcal{C},\mathcal{I},\varrho)$, suchthat
$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\mathsf{A}(y_{1},\ldots,y_{\\#{\mathsf{A}}})$,
$\mathcal{C}\cap\mathcal{D}=\emptyset$ and
$\mathcal{I}\cap\mathcal{J}=\emptyset$.Let
$\sigma\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]$
be a substitution
and$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})$
be a base pair, such
that$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)=(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})\sigma$.
Since $(\emptyset,\emptyset,\varrho)\models^{\nu}\pi$, we obtain
$(\emptyset,\emptyset,\varrho)\models^{\nu_{0}}\pi_{0}$, by Lemma3, where we
define
$\nu_{0}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\nu\sigma$.
Let

$\mathcal{K}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathcal{D}\cup\\{{c_{i}\mid(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{J},~{}i\in[{1},{n}]}\\}$

The proof is by fixpoint induction on thedefinition of
$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})$. Assume that:

$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})\in{\big{(}\mathsf{Base}({\psi*\pi^{\prime}},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})\otimes\bigotimes_{\ell=2}^{h}\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{B}_{\ell}})[x_{1}/z^{\ell}_{1},\ldots,x_{\\#{\mathsf{B}_{\ell}}}/z^{\ell}_{\\#{\mathsf{B}_{\ell}}}]\big{)}}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$

for a rule $\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\psi*\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}\mathsf{B}_{\ell}(z^{\ell}_{1},\ldots,z^{\ell}_{\\#{\mathsf{B}_{\ell}}})$
of $\Delta$, such that$\psi*\pi^{\prime}$ is quantifier-free, $\psi$ consists
of componentand interaction atoms and $\pi^{\prime}$ is the largest
puresubformula of $\psi*\pi^{\prime}$. Then there exist base
tuples$(\mathcal{C}^{\sharp}_{1},\mathcal{I}^{\sharp}_{1},\pi_{1}),\ldots,(\mathcal{C}^{\sharp}_{h},\mathcal{I}^{\sharp}_{h},\pi_{h})$,
suchthat:

  * •

$(\mathcal{C}^{\sharp}_{1},\mathcal{I}^{\sharp}_{1},\pi_{1})\in\mathsf{Base}({\psi*\pi^{\prime}},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})$,

  * •

$(\mathcal{C}^{\sharp}_{\ell},\mathcal{I}^{\sharp}_{\ell},\pi_{\ell})\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{B}_{\ell}})[x_{1}/z^{\ell}_{1},\ldots,x_{\\#{\mathsf{B}_{\ell}}}/z^{\ell}_{\\#{\mathsf{B}_{\ell}}}]$,
forall $\ell\in[{2},{h}]$,

  * •

$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})={\big{(}(\mathcal{C}^{\sharp}_{1},\mathcal{I}^{\sharp}_{1},\pi_{1})\otimes\ldots\otimes(\mathcal{C}^{\sharp}_{h},\mathcal{I}^{\sharp}_{h},\pi_{h})\big{)}}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$.

From the first and last points, we deduce
$\pi_{0}={\mathrm{cl}({\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}(\mathrm{dist}({\mathcal{I}^{\sharp}_{\ell}})*\pi_{\ell})})}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$.
Let
$\pi^{\prime\prime}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}(\mathrm{dist}({\mathcal{I}^{\sharp}_{\ell}})*\pi_{\ell})$
and define a store $\nu^{\prime}_{0}$, by assigning
each$\approx_{\pi^{\prime\prime}}$-equivalence class the followingcomponent:

  * •

$\nu_{0}(x_{i})$, if $x_{i}$ belongs to the class, for some
$i\in[{1},{\\#{\mathsf{A}}}]$,

  * •

else, if the class is disjoint from $\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}$
and ${y}@{q}$ occurs in $\pi^{\prime}$,for a variable $y$ in the class, we
assign $c\in\mathbb{C}\setminus\mathcal{K}$, such that $\varrho(c)=q$;since
$\pi^{\prime}$ is satisfiable, there are no two state atoms${y}@{q}$ and
${z}@{r}$, such that $y\approx_{\pi^{\prime}}z$ and $q\neq r$ in
$\pi^{\prime}$ and,moreover, chosing $c$ is always possible, by the last point
ofDef. 1,

  * •

otherwise, the class is assigned an arbitrary component
$c\in\mathbb{C}\setminus\mathcal{K}$.

Such a store exists, because $\pi^{\prime\prime}$ is satisfiable and,moreover,
$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\pi^{\prime\prime}$,
hence also
$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\pi_{\ell}$, for
all$\ell\in[{2},{h}]$. We define two sequences of sets ofcomponents
$\mathcal{C}_{1},\ldots,\mathcal{C}_{h}$ and
interactions$\mathcal{I}_{1},\ldots,\mathcal{I}_{h}$, asfollows:

  * •

$\mathcal{C}_{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\nu^{\prime}_{0}(y)\mid[{y}]\text{occurs
in }\psi}\\}$,

  * •

$\mathcal{I}_{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{(\nu^{\prime}_{0}(z_{1}),p_{1},\ldots,\nu^{\prime}_{0}(z_{t}),p_{t})\mid\langle{{z_{1}}.\mathit{p_{1}},\ldots,{z_{t}}.\mathit{p_{t}}}\rangle\text{occurs
in }\psi}\\}$,

  * •

for all $\ell\in[{2},{h}]$, assume that
$\mathcal{C}_{1},\ldots,\mathcal{C}_{\ell-1}$ and
$\mathcal{I}_{1},\ldots,\mathcal{I}_{\ell-1}$ have been defined and let us
define:

$\begin{array}[]{rcl}\mathcal{D}_{\ell}&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\mathcal{D}~{}\cup~{}\bigcup_{j=1}^{\ell-1}\mathcal{C}_{j}~{}\cup~{}\bigcup_{j=\ell+1}^{h}\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{j})\\\
\mathcal{J}_{\ell}&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\mathcal{J}~{}\cup~{}\bigcup_{j=1}^{\ell-1}\mathcal{I}_{j}~{}\cup~{}\bigcup_{j=\ell+1}^{h}\nu^{\prime}_{0}(\mathcal{I}^{\sharp}_{j})\end{array}$

First, we prove that
$\mathcal{D}_{\ell}\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})=\emptyset$
and
$\mathcal{J}_{\ell}\cap\nu^{\prime}_{0}(\mathcal{I}^{\sharp}_{\ell})=\emptyset$
(we prove the firstpoint, the second using a similar argument). Suppose, for
acontradiction, that
$c\in\mathcal{D}_{\ell}\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})$. We
distinguish the followingcases:

    * –

if $c\in\mathcal{D}\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})$,
then$c\in\mathcal{D}\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{0})$,
because$\mathcal{C}^{\sharp}_{\ell}\subseteq\mathcal{C}^{\sharp}_{0}$,
contradiction
with$\mathcal{D}\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{0})=\mathcal{D}\cap\nu(\mathcal{C}^{\sharp})=\emptyset$.

    * –

else, if
$c\in\mathcal{C}_{j}\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})$,for
some $j\in[{1},{\ell-1}]$, then $c\in\mathcal{C}_{j}\cap\mathcal{D}_{j}$,
because
$\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})\subseteq\mathcal{D}_{j}$,
contradiction with the inductive
hypothesis$\mathcal{C}_{j}\cap\mathcal{D}_{j}=\emptyset$.

    * –

otherwise,
$c\in\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{j})\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})$,
hence there exist variables $y_{j}\in\mathcal{C}^{\sharp}_{j}$ and
$y_{\ell}\in\mathcal{C}^{\sharp}_{\ell}$, such
that$y_{j}\approx_{\pi^{\prime\prime}}y_{\ell}$, contradiction with the
factthat
$(\mathcal{C}^{\sharp}_{j},\mathcal{I}^{\sharp}_{j},\pi_{j})\otimes(\mathcal{C}^{\sharp}_{\ell},\mathcal{I}^{\sharp}_{\ell},\pi_{\ell})$
issatisfiable.

Second, we apply the inductive hypothesis to obtain
configurations$(\mathcal{C}_{\ell},\mathcal{I}_{\ell},\varrho)$, such
that$(\mathcal{C}_{\ell},\mathcal{I}_{\ell},\varrho)\models^{\nu^{\prime}_{0}}_{\Delta}\mathsf{B}_{\ell}(t^{\ell}_{1},\ldots,t^{\ell}_{\\#{\mathsf{B}_{\ell}}})$,
$\mathcal{C}_{\ell}\cap\mathcal{D}_{\ell}=\emptyset$ and
$\mathcal{I}_{\ell}\cap\mathcal{J}_{\ell}=\emptyset$, for all
$\ell\in[{2},{h}]$. By the definitions of $\mathcal{D}_{\ell}$
and$\mathcal{J}_{\ell}$, the sets $\mathcal{C}_{\ell}$ and
$\mathcal{I}_{\ell}$are pairwise disjoint, respectively, hence the
composition$(\mathcal{C},\mathcal{I},\varrho)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\scalebox{2.0}{$\bullet$}_{\ell=1}^{h}(\mathcal{C}_{\ell},\mathcal{I}_{\ell},\varrho)$
is defined.
Moreover,$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu^{\prime}_{0}}_{\Delta}\psi*\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}\mathsf{B}_{\ell}(t^{\ell}_{1},\ldots,t^{\ell}_{\\#{\mathsf{B}_{\ell}}})$,
hence
$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu^{\prime}_{0}}_{\Delta}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$,
leading to
$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu}\mathsf{A}(y_{1},\ldots,y_{\\#{\mathsf{A}}})$.Finally,
we are left with proving that $\mathcal{C}\cap\mathcal{D}=\emptyset$ and
$\mathcal{I}\cap\mathcal{J}=\emptyset$ (we provethe first point only, the
second uses a similar reasoning).
Since$\mathcal{C}=\bigcup_{\ell=1}^{h}\mathcal{C}_{\ell}$, this is equivalent
toproving the following:

    * –

$\mathcal{C}_{1}\cap\mathcal{D}=\emptyset$: suppose, for acontradiction, that
$\nu^{\prime}_{0}(y)\in\mathcal{D}$, for avariable $y$, such that $[{y}]$
occurs in $\psi$. By thedefinition of $\nu^{\prime}_{0}$, we have either
$\nu^{\prime}_{0}(y)\in\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{0})$ or
$\nu^{\prime}_{0}(y)\in\mathcal{K}$. Since
$\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{0})\cap\mathcal{D}=\mathcal{K}\cap\mathcal{D}=\emptyset$,
both cases lead to acontradiction.

    * –

$\mathcal{C}_{\ell}\cap\mathcal{D}=\emptyset$, for all $\ell\in[{2},{h}]$:
because $\mathcal{C}_{\ell}\cap\mathcal{D}_{\ell}=\emptyset$ and
$\mathcal{D}\subseteq\mathcal{D}_{\ell}$, bydefinition of
$\mathcal{D}_{\ell}$, for all $\ell\in[{2},{h}]$. ∎

Given a predicate atom $\mathsf{A}(y_{1},\ldots,y_{\\#{\mathsf{A}}})$,a store
$\nu$ and a configuration $(\mathcal{C},\mathcal{I},\varrho)$,such that
$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\mathsf{A}(y_{1},\ldots,y_{\\#{\mathsf{A}}})$,
there exists a basetuple
$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]$,
such that$\nu(\mathcal{C}^{\sharp})\subseteq\mathcal{C}$,
$\nu(\mathcal{I}^{\sharp})\subseteq\mathcal{I}$ and
$(\emptyset,\emptyset,\varrho)\models^{\nu}\pi$.By fixpoint induction on the
definition of the satisfaction relation$\models^{\nu}_{\Delta}$. Since
$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\mathsf{A}(y_{1},\ldots,y_{\\#{\mathsf{A}}})$,
byLemma 3, we have
$(\mathcal{C},\mathcal{I},\varrho)\models^{\nu_{0}}_{\Delta}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$,where
$\nu_{0}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\nu[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]$.
Hence, $\Delta$ has arule
$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\psi*\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}\mathsf{B}_{\ell}(z^{\ell}_{1},\ldots,z^{\ell}_{\\#{\mathsf{B}_{\ell}}})$,
such that $\psi*\pi^{\prime}$ isquantifier-free, $\psi$ consists of component
and interaction atomsand $\pi^{\prime}$ is pure and there exists a store
$\nu^{\prime}_{0}$, thatagrees with $\nu_{0}$ over
$x_{1},\ldots,x_{\\#{\mathsf{A}}}$ andconfigurations
$(\mathcal{C}_{1},\mathcal{I}_{1},\varrho)$,
$\ldots,(\mathcal{C}_{\ell},\mathcal{I}_{\ell},\varrho)$, suchthat:

  * •

$(\mathcal{C}_{1},\mathcal{I}_{1},\varrho)\models^{\nu^{\prime}_{0}}\psi*\pi^{\prime}$,

  * •

$(\mathcal{C}_{\ell},\mathcal{I}_{\ell},\varrho)\models^{\nu^{\prime}_{0}}_{\Delta}\mathsf{B}_{\ell}(z^{\ell}_{1},\ldots,z^{\ell}_{\\#{\mathsf{B}_{\ell}}})$,
for all $\ell\in[{2},{h}]$,and

  * •

$(\mathcal{C},\mathcal{I},\varrho)=(\mathcal{C}_{1},\mathcal{I}_{1},\varrho)\bullet\ldots\bullet(\mathcal{C}_{h},\mathcal{I}_{h},\varrho)$.

We consider the following base tuples:

  * •

$(\mathcal{C}^{\sharp}_{1},\mathcal{I}^{\sharp}_{1},\pi_{1})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathsf{Base}({\psi*\pi^{\prime}},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})$,

  * •

$(\mathcal{C}^{\sharp}_{\ell},\mathcal{I}^{\sharp}_{\ell},\pi_{\ell})\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{B}_{\ell}})[x_{1}/z^{\ell}_{1},\ldots,x_{\\#{\mathsf{B}_{\ell}}}/z^{\ell}_{\\#{\mathsf{B}_{\ell}}}]$,
suchthat
$\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})\subseteq\mathcal{C}_{\ell}$,$\nu^{\prime}_{0}(\mathcal{I}^{\sharp}_{\ell})\subseteq\mathcal{I}_{\ell}$
and$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\pi_{\ell}$, whose
existence is guaranteed by the inductivehypothesis, for all
$\ell\in[{2},{h}]$.

By the definition of
$\mathsf{Base}({\psi*\pi^{\prime}},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})$
and the fact that
$(\mathcal{C}_{1},\mathcal{I}_{1},\varrho)\models^{\nu^{\prime}_{0}}\psi*\pi^{\prime}$,
weobtain $\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{1})=\mathcal{C}_{1}$
and$\nu^{\prime}_{0}(\mathcal{I}^{\sharp}_{1})=\mathcal{I}_{1}$. Since the
composition$\scalebox{2.0}{$\bullet$}_{\ell=1}^{h}(\mathcal{C}_{\ell},\mathcal{I}_{\ell},\varrho)$
isdefined, the sets $\mathcal{C}_{1},\ldots,\mathcal{C}_{h}$ and
$\mathcal{I}_{1},\ldots,\mathcal{I}_{h}$ are pairwise disjoint, respectively.
Since$\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})\subseteq\mathcal{C}_{\ell}$
and$\nu^{\prime}_{0}(\mathcal{I}^{\sharp})\subseteq\mathcal{I}_{\ell}$, for
all $\ell\in[{1},{h}]$, we deduce that
$\bigotimes_{\ell=1}^{h}(\mathcal{C}^{\sharp}_{\ell},\mathcal{I}^{\sharp}_{\ell},\pi_{\ell})$
is satisfiable, because:

  * •

for all $1\leq i<j\leq h$, for any two variables
$y\in\mathcal{C}^{\sharp}_{i}$ and $z\in\mathcal{C}^{\sharp}_{j}$ we have
$\mathrm{not}(y\approx_{\pi^{\prime}}z)$, because
$\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{i})\cap\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{j})=\emptyset$,

  * •

for all $1\leq i<j\leq h$, all $\tau\in\mathsf{Inter}$, for any two tuples
$\langle{y_{1},\ldots,y_{|{\tau}|}}\rangle\in\mathcal{I}^{\sharp}_{i}(\tau)$
and$\langle{z_{1},\ldots,z_{|{\tau}|}}\rangle\in\mathcal{I}^{\sharp}_{j}(\tau)$,
we have $\mathrm{not}(y_{k}\approx_{\pi^{\prime}}z_{k})$, for at least some
$k\in[{1},{|{\tau}|}]$,
because$\nu^{\prime}_{0}(\mathcal{I}^{\sharp}_{i})\cap\nu^{\prime}_{0}(\mathcal{I}^{\sharp}_{j})=\emptyset$,

  * •

for each tuple
$\langle{y_{1},\ldots,y_{|{\tau}|}}\rangle\in\mathcal{I}^{\sharp}_{\ell}(\langle{p_{1},\ldots,p_{n}}\rangle)$,
for $\ell\in[{1},{h}]$, we have
$\mathrm{not}(y_{i}\approx_{\pi^{\prime}}y_{j})$, forall $1\leq i<j\leq n$,
because
$(\nu^{\prime}_{0}(y_{1}),p_{1},\ldots,\nu^{\prime}_{0}(y_{n}),p_{n})\in\mathcal{I}_{\ell}$,
hence $\nu^{\prime}_{0}(y_{1}),\ldots,\nu^{\prime}_{0}(y_{n})$ are pairwise
distinct,

  * •

$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}\pi_{\ell}$,
hence$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}\mathrm{dist}({\mathcal{I}^{\sharp}_{\ell}})*\pi_{\ell}$, by
the previous point.

Then we define
$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}{\left(\bigotimes_{\ell=1}^{h}(\mathcal{C}^{\sharp}_{\ell},\mathcal{I}^{\sharp}_{\ell},\pi_{\ell})\right)}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$
and
$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]$.
By the definition of$\Delta^{\sharp}$, we have:

$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})\supseteq{\big{(}\mathsf{Base}({\psi*\pi^{\prime}},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})\otimes\bigotimes_{\ell=2}^{h}\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{B}_{\ell}})[x_{1}/z^{\ell}_{1},\ldots,x_{\\#{\mathsf{B}_{\ell}}}/z^{\ell}_{\\#{\mathsf{B}_{\ell}}}]\big{)}}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$

and, since, by the construction of
$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})$,

$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})\in{\big{(}\mathsf{Base}({\psi*\pi^{\prime}},{\\{{x_{1},\ldots,x_{\\#{\mathsf{A}}}}\\}})\otimes\bigotimes_{\ell=2}^{h}\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{B}_{\ell}})[x_{1}/z^{\ell}_{1},\ldots,x_{\\#{\mathsf{B}_{\ell}}}/z^{\ell}_{\\#{\mathsf{B}_{\ell}}}]\big{)}}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$

we obtain
$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})$,
leading to
$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]$.
Next, we check
that$\nu(\mathcal{C}^{\sharp})\subseteq\bigcup_{\ell=1}^{h}\nu^{\prime}_{0}(\mathcal{C}^{\sharp}_{\ell})\subseteq\bigcup_{\ell=1}^{h}\mathcal{C}_{\ell}=\mathcal{C}$
and
$\nu(\mathcal{I}^{\sharp})\subseteq\bigcup_{\ell=1}^{h}\nu^{\prime}_{0}(\mathcal{I}^{\sharp}_{\ell})\subseteq\bigcup_{\ell=1}^{h}\mathcal{I}_{\ell}=\mathcal{I}$.
Finally, the requirement$(\emptyset,\emptyset,\varrho)\models^{\nu}\pi$
followsfrom the following:

  * •

$\pi=\pi_{0}[x_{1}/y_{1},\ldots,x_{\\#{\mathsf{A}}}/y_{\\#{\mathsf{A}}}]$, by
the definition of$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)$,

  * •

$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\pi^{\prime}$ and
$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\pi_{\ell}$, for all
$\ell\in[{2},{h}]$,

  * •

$\pi_{0}={\mathrm{cl}({\pi^{\prime}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\ell=2}^{h}\mathrm{dist}({\mathcal{I}^{\sharp}_{\ell}})*\pi_{\ell}})}\\!\\!\downarrow_{\scriptscriptstyle{x_{1},\ldots,x_{\\#{\mathsf{A}}}}}$,
where$(\emptyset,\emptyset,\varrho)\models^{\nu^{\prime}_{0}}\mathrm{dist}({\mathcal{I}^{\sharp}_{\ell}})$
follows from the satisfiability
of$(\mathcal{C}^{\sharp}_{\ell},\mathcal{I}^{\sharp}_{\ell},\pi_{\ell})$, for
all $\ell\in[{2},{h}]$. ∎

$\mathsf{Sat}[{\Delta},{\mathsf{A}}]$ has a positive answer if and only
if$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})\neq\emptyset$.
“$\Leftarrow$” follows from Lemma 3and “$\Rightarrow$” follows from Lemma3.
∎If the maximal arity of the predicates occurring in $\Delta$ is boundby a
constant $k$, no satisfiable base tuple
$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)$ can have atuple
$\langle{y_{1},\ldots,y_{|{\tau}|}}\rangle\in\mathcal{I}^{\sharp}(\tau)$, for
some $\tau\in\mathsf{Inter}$, suchthat $|{\tau}|>k$, since all variables
$y_{1},\ldots,y_{|{\tau}|}$ are parameters denoting distinct components(point
3 of Def. 8). Hence, theupper bound on the size of a satisfiable base tuple is
constant, inboth the $k<\infty,\ell<\infty$ and $k<\infty,\ell=\infty$
cases,which are, moreover indistinguishable complexity-wise (i.e., both
are$\mathsf{NP}$-complete). In contrast, in the cases $k=\infty,\ell<\infty$
and$k=\infty,\ell=\infty$, the upper bound on the size of satisfiablebase
tuples is polynomial and simply exponential in
$\mathrm{size}({\Delta})$,incurring a complexity gap of one and two
exponentials, respectively.The theorem below states the main result of this
section:$\mathsf{Sat}^{({k},{\infty})}[{\Delta},{\mathsf{A}}]$ is
$\mathsf{NP}$-complete for $k\geq
4$,$\mathsf{Sat}^{({\infty},{\ell})}[{\Delta},{\mathsf{A}}]$ is
$\mathsf{EXP}$-complete and$\mathsf{Sat}[{\Delta},{\mathsf{A}}]$ is in
$2\mathsf{EXP}$._Membership (upper bounds)._ For non-negative integers $m\leq
n$ denote by
$S_{n,m}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\frac{n!}{(n-m)!}$
the number of ordered $m$-element subsets of a$n$-element set.Let
$\alpha=\mathrm{arity}({\Delta})$, $\beta=\mathrm{intersize}({\Delta})$ and
$p=|\\!|{\mathcal{P}}|\\!|$. Themaximum length of a satisfiable base tuple is
$B\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\alpha+(\sum_{j=1}^{\min(\alpha,\beta)}p^{j}\cdot
S_{\alpha,j})+(2\alpha^{2}+\alpha)$, that is, size of the set of
components$\mathcal{C}^{\sharp}$ plus the size of the set of
interactions$\mathcal{I}^{\sharp}$ plus the length of the longest pure
formula$\pi$. In general, for any non-negative integer $j$ thereexists at most
$p^{j}$ interaction types of arity $j$ with ports from$\mathcal{P}$; moreover,
for any such interaction type there exists atmost $S_{\alpha,j}$ interactions
relating distinctcomponents from an $\alpha$-element set. Moreover, no
suchinteraction exists neither if $j>\alpha$ nor $j>\beta$.For any
$u\leq\alpha$ it holds that $\sum_{j=1}^{u}p^{j}\cdot S_{\alpha,j}\leq
p^{u}\alpha^{u}$ (an easy check byinduction on $u$). We use the inequality
above with$u=\min(\alpha,\beta)$ and obtain that $B\leq
2\alpha+2\alpha^{2}+p^{\min(\alpha,\beta)}\alpha^{\min(\alpha,\beta)}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}B^{*}$.
Wedistinguish the three cases:

  1. 1.

$k<\infty$, $\ell=\infty$: since $\alpha\leq k$ then $\alpha$ is constant
and$B^{*}=\mathcal{O}(1)$,

  2. 2.

$k=\infty$, $\ell<\infty$: since $\beta\leq\ell$
and$\alpha=\mathcal{O}(\mathrm{size}({\Delta}))$
then$B^{*}=\mathit{poly}(\mathrm{size}({\Delta}))$,

  3. 3.

$k=\infty$, $\ell=\infty$: since
$\alpha=\mathcal{O}(\mathrm{size}({\Delta}))$then
$B^{*}=2^{\mathit{poly}(\mathrm{size}({\Delta)})}$.

Let
$N\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}2^{B^{*}}$,
that is, (an over-approximation of) thetotal number of base tuples. Clearly,
$N$ is constant in case (1)and respectively
$2^{\mathit{poly}(\mathrm{size}({\Delta)})}$
and$2^{2^{\mathit{poly}(\mathrm{size}({\Delta)})}}$ in cases (2), (3). Let $L$
bethe number of predicates occuring in $\Delta$ and $H$ be the maximumnumber
of predicates used in a term in $\Delta$. Let observe thatboth $L$ and $H$ are
in general $\mathcal{O}(\mathrm{size}({\Delta}))$. Then theleast solution
$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}$ has at most $N$ base tuples
for eachpredicate, hence at most $L\cdot N$ base tuples. Furthermore, foreach
rule of $\Delta$ the time to check and/or produce the base
tuple$(\mathcal{C}^{\sharp}_{0},\mathcal{I}^{\sharp}_{0},\pi_{0})$ with
respect to therule constraint (1) and given
arguments$(\mathcal{C}^{\sharp}_{j},\mathcal{I}^{\sharp}_{j},\pi_{j})_{j=1,h}$
is polynomial$\mathit{poly}(B^{*},\mathrm{size}({\Delta})))$. That is, both
compositionand projection take at most
$(H+1)B^{*}+\mathrm{size}({\Delta})^{3}$ time asthey need to process (union or
scan) at most $H+1$ base tuples oflength $B^{*}$ each plus the closure of pure
formula with at most$\mathrm{size}({\Delta})$ variables.

  1. 1.

$k<\infty$, $\ell=\infty$: We define a non-determinstic algorithm asfollows.
Let $(\Delta,\mathsf{A})$ be the input instance. We guess awitness
$\langle{W_{1},\ldots,W_{K}}\rangle$ for a least solution, where $1\leq K\leq
L\cdot N$ and each $W_{i}$ entry is of the
form$(T_{i},r_{i},e_{i,1},\ldots,e_{i,h_{i}})$, where $T_{i}$ is a base
tuple,$r_{i}$ an index of a rule of $\Delta$ and $e_{i,1},\ldots,e_{i,h}$are
index values from $\\{{i+1,\ldots,K}\\}$ for $0\leq h_{i}\leq H$.The length of
every witness entry is therefore at most
$B^{*}+\lceil\log_{2}(\mathrm{size}({\Delta}))\rceil+H\lceil\log_{2}(L\cdot
N)\rceil$. As $N$ is constant when $k<\infty$, and $L$ and $H$are
$\mathcal{O}(\mathrm{size}({\Delta}))$ it follows that the number of guesses
ispolynomial for building $\langle{W_{1},\ldots,W_{K}}\rangle$. We now
checkthat $\langle{W_{1},\ldots,W_{K}}\rangle$ represents indeed a
validcomputation of a base tuples from the least solution
i.e.,$(\mathcal{C}^{\sharp},\mathcal{I}^{\sharp},\pi)\in\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}({\mathsf{A}})$.
For this, we need to check:(a) every entry is well-formed, that is, the rule
indexed by $r_{i}$instantiates precisely $h_{i}$ predicates; moreover, for
every $1\leq j\leq h_{i}$ the index $e_{i,j}$ designates an entry$W_{e_{i,j}}$
whose rule defines the $j$-th predicate instantiatedby the rule $r_{i}$; (b)
the base tuple of every entry issatisfiable and correctly computed, that is,
$T_{i}$ is the resultof applying the constraint (1) for rule $r_{i}$
withactual arguments $T_{e_{i,1}},\ldots,T_{e_{i,h_{i}}}$ from thereferred
entries; (c) the rule $r_{1}$ of the first entry $W_{1}$defines the predicate
$\mathsf{A}$. Again, as $B^{*}$ and $N$ areconstant in this case, all these
checks are done in polynomialtime. Since both the generation and the checking
of the witnessare polynomial time, this ensures membership in $\mathsf{NP}$.

  2. 2.

$k=\infty$, $\ell<\infty$: Consider the computation of theleast solution
$\mu\overrightarrow{\mathcal{X}}.\Delta^{\sharp}$ using standard Kleene
iteration. Atevery step, a rule of $\Delta$ and a tuple of at most $H$
basetuples arguments are selected to produce a new base tuple. Thus,in the
worst case, at most $\mathrm{size}({\Delta})$ rules in combinationwith at most
$N^{H}$ base tuples need to be selected and evaluated.If no new base tuple is
generated the fixpoint is reached and thealgorithms stops. Since there are at
most $L\cdot N$ base tuplesin the least solution, the total time will be
therefore $L\cdot N\cdot\mathrm{size}({\Delta})\cdot N^{H}\cdot
t(B^{*},\mathrm{size}({\Delta}))$ where$t(B^{*},\mathrm{size}({\Delta}))$ is
the (polynomial) time to process oneselection. It is an easy check that the
above is$2^{\mathit{poly}(\mathrm{size}({\Delta}))}$
since$N=2^{\mathit{poly}(\mathrm{size}({\Delta}))}$ in this case.

  3. 3.

$k=\infty$, $\ell=\infty$: Following the same reasoning as inthe previous case
the complexity is$2^{2^{\mathit{poly}(\mathrm{size}({\Delta)})}}$
as$N=2^{2^{\mathit{poly}(\mathrm{size}({\Delta}))}}$ in this case.

_Hardness (lower bounds)_. The restricted fragment of CL to$*$, $=$, $\not=$
is equisatisfiable to the restricted fragment ofSL restricted to $*$, $=$,
$\not=$. The satisfiability of theabove SL fragment has been proven
respectively $\mathsf{NP}$-hard, ifthe arities of predicates are bounded by a
constant $k\geq 3$[DBLP:conf/csl/BrotherstonFPG14, Theorem 4.9]
and$\mathsf{EXP}$-hard, in general [DBLP:conf/csl/BrotherstonFPG14,
Theorem4.15]. Yet, the reductionsconsidered in these proofs rely on the use of
a predefined _nil_ constant symbol in the SL logic; this constant canbe
nevertheless replaced by a variable consistently propagated alongthe SID, that
is, at the price of increasing the arities of allpredicates by one. Therefore,
it follows immediately that$\mathsf{Sat}^{({k},{\infty})}[{\Delta},{\phi}]$ is
$\mathsf{NP}$-hard for $k\geq 4$
and$\mathsf{Sat}^{({\infty},{\ell})}[{\Delta},{\phi}]$,
$\mathsf{Sat}[{\Delta},{\phi}]$ are both$\mathsf{EXP}$-hard. ∎

###### Example 3

The doubly-exponential upper bound for the algorithm computing theleast
solution of a system of constraints of the form(1) is necessary, in general,
as illustrated by the followingworst-case example. Let $n$ be a fixed
parameter and consider the$n$-arity predicates $A_{1},\ldots,A_{n}$ defined by
the following SID:

$\begin{array}[]{rcll}A_{i}(x_{1},\ldots,x_{n})&\rightarrow&\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{j=0}^{n-i}~{}A_{i+1}(x_{1},\ldots,x_{i-1},[x_{i},\ldots,x_{n}]^{j})&\text{,
for all }i\in[{1},{n-1}]\\\
A_{n}(x_{1},\ldots,x_{n})&\rightarrow&\langle{{x_{1}}.\mathit{p},\ldots,{x_{n}}.\mathit{p}}\rangle\\\
A_{n}(x_{1},\ldots,x_{n})&\rightarrow&\mathsf{emp}\end{array}$

where, for a list of variables $x_{i},\ldots,x_{n}$ and an integer$j\geq 0$,
we write $[x_{i},\ldots,x_{n}]^{j}$ for the list rotated tothe left $j$ times
(e.g.,$[x_{1},x_{2},x_{3},x_{4},x_{5}]^{2}=x_{3},x_{4},x_{5},x_{1},x_{2}$). In
this example,when starting with $A_{1}(x_{1},\ldots,x_{n})$ one eventually
obtainspredicate atoms $A_{n}(x_{i_{1}},\ldots,x_{i_{n}})$, for any
permutation$x_{i_{1}},\ldots,x_{i_{n}}$ of $x_{1},\ldots,x_{n}$. Since $A_{n}$
maychoose to create or not an interaction with that permutation ofvariables,
the total number of base tuples generated for $A_{1}$ is$2^{n!}$. That is, the
fixpoint iteration generates $2^{2^{\mathcal{O}(n\log n)}}$ base tuples,
whereas the size of the input of $\mathsf{Sat}[{\Delta},{\mathsf{A}}]$
is$\mathit{poly}(n)$. $\blacksquare$

##  4 Tightness

The tightness problem (Def. 6, point2) is the complement of a problem slightly
strongerthan satisfiability (1): given a SID $\Delta$ and aformula $\phi$,
such that $\mathrm{fv}({\phi})=\\{{x_{1},\ldots,x_{n}}\\}$, the _looseness
problem_ $\mathsf{Loose}[{\Delta},{\mathsf{A}}]$ asks for theexistence of a
loose configuration $\gamma$(Def. 2), such that $\gamma\models_{\Delta}\exists
x_{1}\ldots\exists x_{n}~{}.~{}\phi$. We establish upper and lower boundsfor
the complexity of the looseness problem by a reduction to and fromthe
satisfiability problem. The bounds for the tightness problemfollow by standard
complementation of the complexity classes for thelooseness problem.

#### From Looseness to Satisfiability.

Let $\Delta$ be a given SID and $\mathsf{A}$ be a predicate. For eachpredicate
$\mathsf{B}$ that occurs in $\Delta$, we consider a freshpredicate
${\mathsf{B}^{\prime}}$, not occurring in $\Delta$, such
that$\\#{{\mathsf{B}^{\prime}}}=\\#{\mathsf{B}}+1$. The SID
${\widetilde{\Delta}}$ consists of$\Delta$ and, for each rule of $\Delta$ of
the form:

$\mathsf{B}_{0}(x_{1},\ldots,x_{\\#{\mathsf{B}_{0}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$

where $\phi$ is aquantifier- and predicate-free formula,
${\widetilde{\Delta}}$ has the followingrules:

${\mathsf{B}^{\prime}}_{0}(x_{1},\ldots,x_{\\#{\mathsf{B}_{0}}+1})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi~{}*~{}x_{\\#{\mathsf{B}_{0}}+1}=z~{}*~{}\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})~{}*\ldots*~{}\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$

if $z$ occurs in an interaction atom from $\phi$, and:

$\begin{array}[]{rcl}{\mathsf{B}^{\prime}}_{0}(x_{1},\ldots,x_{\\#{\mathsf{B}_{0}}+1})&\leftarrow&\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*{\mathsf{B}^{\prime}}_{i}(t^{i}_{1},\ldots,t^{i}_{\\#{\mathsf{B}_{i}}},x_{\\#{\mathsf{B}_{0}}+1})\\\
&&\hskip
56.9055pt*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})\end{array}$

for some $i\in[{1},{h}]$, if $h\geq 1$. Moreover, for each rule of$\Delta$ of
the form above, with no predicate atoms (i.e., $h=0$),${\widetilde{\Delta}}$
contains the rule:

$\begin{array}[]{rcll}{\mathsf{B}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{B}}+1})&\leftarrow&\exists
y_{1}\ldots\exists y_{m}~{}.~{}\phi*[{x_{\\#{\mathsf{B}_{0}}+1}}]\end{array}$

if and only if $\phi$ contains no predicate atoms. Finally, there is afresh
predicate $\widetilde{\mathsf{A}}$, of arity $\\#{\mathsf{A}}$, witha rule:

$\widetilde{\mathsf{A}}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y~{}.~{}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}},y)*[{y}]$

Intuitively, the last parameter of a ${\mathsf{B}^{\prime}}$ predicate binds
to anarbitrary variable of an interaction atom. A configuration $\gamma$is
loose if and only if the value (component) of some variableoccurring in an
interaction atom is absent, in which case thecomponent can be added to
$\gamma$ (without clashing with a presentcomponent of $\gamma$) by the last
rule. The reduction ispolynomial, since the number of rules in
${\widetilde{\Delta}}$ is linear in thenumber of rules in $\Delta$ and the
size of each newly added rule isincreased by a constant. The following lemma
states the correctness ofthe reduction:

###### Lemma 1

Given a SID $\Delta$ and a predicate $\mathsf{A}$, the
problem$\mathsf{Loose}[{\Delta},{\mathsf{A}}]$ has a positive answer if and
only if theproblem
$\mathsf{Sat}[{{\widetilde{\Delta}}},{\widetilde{\mathsf{A}}}]$ has a positive
answer.

###### Proof

“$\Rightarrow$” Let
$\gamma\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}(\mathcal{C},\mathcal{I},\varrho)$
bea loose configuration, such that
$\gamma\models^{\nu}_{\Delta}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$,
for some store$\nu$. Since $\gamma$ is loose, there exists an
interaction$(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{I}$, such that
$c_{i}\not\in\mathcal{C}$, for some $i\in[{1},{n}]$. We prove that
$\gamma\models_{{\widetilde{\Delta}}}^{\nu[y\leftarrow
c_{i}]}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}},y)$, by fixpoint
induction on the definition
of$\gamma\models^{\nu}_{\Delta}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$.
This is sufficient, because then we
obtain$(\mathcal{C}\cup\\{{c_{i}}\\},\mathcal{I},\varrho)\models_{{\widetilde{\Delta}}}^{\nu}\widetilde{\mathsf{A}}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$,
thus$\mathsf{Sat}[{{\widetilde{\Delta}}},{\widetilde{\mathsf{A}}}]$ has a
positive answer. Consider therule of $\Delta$:

$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$

where $\phi$ isquantifier- and predicate-free and
$c^{\prime}_{1},\ldots,c^{\prime}_{m}\in\mathbb{C}$are components, such that
$(\mathcal{C},\mathcal{I},\varrho)\models_{\Delta}^{\nu^{\prime}}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$,
where
$\nu^{\prime}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\nu[y_{1}\leftarrow
c^{\prime}_{1},\ldots,y_{m}\leftarrow c^{\prime}_{m}]$. We distinguish
thefollowing cases:

  * •

if $(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{I}$ because of aninteraction
atom $\langle{{z_{1}}.\mathit{p_{1}},\ldots,{z_{n}}.\mathit{p_{n}}}\rangle$
from $\phi$, suchthat $\nu^{\prime}(z_{i})=c_{i}$, for all $i\in[{1},{n}]$,
then$(\mathcal{C},\mathcal{I},\varrho)\models_{{\widetilde{\Delta}}}^{\nu^{\prime}[y\leftarrow
c_{i}]}\phi*y=z_{i}*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$,
hence
$(\mathcal{C},\mathcal{I},\varrho)\models_{{\widetilde{\Delta}}}^{\nu[y\leftarrow
c_{i}]}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}},y)$, by the
definition of ${\widetilde{\Delta}}$.

  * •

else $(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{I}$ because of
aconfiguration $\gamma^{\prime}$, such that
$\gamma=\gamma^{\prime}\bullet\gamma^{\prime\prime}$, for some configuration
$\gamma^{\prime\prime}$, and
$\gamma^{\prime}\models^{\nu^{\prime}}_{\Delta}\mathsf{B}_{i}(t^{i}_{1},\ldots,t^{i}_{\\#{\mathsf{B}_{i}}})$.
By the inductive hypothesis, we
obtain$\gamma^{\prime}\models^{\nu^{\prime}[y\leftarrow
c_{i}]}_{\Delta}{\mathsf{B}^{\prime}}_{i}(t^{i}_{1},\ldots,t^{i}_{\\#{\mathsf{B}_{i}}},y)$,
hence$\gamma\models^{\nu[y\leftarrow
c_{i}]}_{\Delta}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}},y)$,
because ${\widetilde{\Delta}}$ contains the rule:

$\begin{array}[]{rcl}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}+1})&\leftarrow&\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*{\mathsf{B}^{\prime}}_{i}(t^{i}_{1},\ldots,t^{i}_{\\#{\mathsf{B}_{i}}},x_{\\#{\mathsf{A}}+1})\\\
&&\hskip
56.9055pt*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})\end{array}$

and
$\gamma^{\prime\prime}\models^{\nu^{\prime}}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*{\mathsf{B}^{\prime}}_{i-1}(t^{i-1}_{1},\ldots,t^{i-1}_{\\#{\mathsf{B}_{i-1}}})*{\mathsf{B}^{\prime}}_{i+1}(t^{i+1}_{1},\ldots,t^{i+1}_{\\#{\mathsf{B}_{i+1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$
follows from $\gamma=\gamma^{\prime}\bullet\gamma^{\prime\prime}$.

”$\Leftarrow$” Let
$\gamma\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}(\mathcal{C},\mathcal{I},\varrho)$
be a configuration and $\nu$ be astore, such that
$\gamma\models^{\nu}_{{\widetilde{\Delta}}}\widetilde{\mathsf{A}}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$.
Since the onlyrule of ${\widetilde{\Delta}}$ that defines
$\widetilde{\mathsf{A}}$ is:

$\widetilde{\mathsf{A}}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y~{}.~{}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}},y)*[{y}]$

there exists a component $c\in\mathcal{C}$, such
that$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu[y\leftarrow
c]}_{\widetilde{\Delta}}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}},y)$.
We prove the following:

  * •

there exists an interaction $(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{I}$,
such that $c_{i}=c$, and

  * •

$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$,

by fixpoint induction on the definition
of$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu[y\leftarrow
c]}_{\widetilde{\Delta}}{\mathsf{A}^{\prime}}(x_{1},\ldots,x_{\\#{\mathsf{A}}},y)$.
Based on the definition of ${\widetilde{\Delta}}$, we distinguish the
followingcases, where $\phi$ is quantifier- and predicate-free,
$c^{\prime}_{1},\ldots,c^{\prime}_{m}\in\mathbb{C}$ are components and
$\nu^{\prime}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\nu[y_{1}\leftarrow
c^{\prime}_{1},\ldots,y_{m}\leftarrow c^{\prime}_{m}]$:

  * •

$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu^{\prime}[y\leftarrow
c]}_{\widetilde{\Delta}}\phi~{}*~{}y=z~{}*~{}\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})~{}*\ldots*~{}\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$,
where $z$ occurs in an interaction atomfrom $\phi$. In this case, there exists
an interaction $(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{I}$, such that
$c=c_{i}$, for some $i\in[{1},{n}]$.
Moreover,$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$,
because $\Delta$ has arule:

$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$

such
that$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})~{}*\ldots*~{}\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$.

  * •

$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu^{\prime}[y\leftarrow
c]}_{\widetilde{\Delta}}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*{\mathsf{B}^{\prime}}_{i}(t^{i}_{1},\ldots,t^{i}_{\\#{\mathsf{B}_{i}}},y)*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$.
In this case, there existsconfigurations $\gamma^{\prime}$ and
$\gamma^{\prime\prime}$, such
that$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)=\gamma^{\prime}\bullet\gamma^{\prime\prime}$,
$\gamma^{\prime}\models^{\nu^{\prime}[y\leftarrow
c]}_{\widetilde{\Delta}}{\mathsf{B}^{\prime}}_{i}(t^{i}_{1},\ldots,t^{i}_{\\#{\mathsf{B}_{i}}},y)$
and$\gamma^{\prime\prime}\models^{\nu}_{\Delta}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$.
By the inductive hypothesis, thereexists an interaction
$(c_{1},p_{1},\ldots,c_{n},p_{n})$ in $\gamma^{\prime}$,such that $c=c_{i}$,
for some $i\in[{1},{n}]$ and
$\gamma^{\prime}\models^{\nu}_{\Delta}\mathsf{B}_{i}(t^{i}_{1},\ldots,t^{i}_{\\#{\mathsf{B}_{i}}})$.
Then $(c_{1},p_{1},\ldots,c_{n},p_{n})\in\mathcal{I}$ and
$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu}_{\Delta}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$,
since $\Delta$ has a rule:

$\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\ldots\exists
y_{m}~{}.~{}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})*\ldots*\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$

such
that$\gamma^{\prime}\bullet\gamma^{\prime\prime}\models^{\nu^{\prime}}_{\Delta}\phi*\mathsf{B}_{1}(t^{1}_{1},\ldots,t^{1}_{\\#{\mathsf{B}_{1}}})~{}*\ldots*~{}\mathsf{B}_{h}(t^{h}_{1},\ldots,t^{h}_{\\#{\mathsf{B}_{h}}})$.

  * •

$(\mathcal{C}\setminus\\{{c}\\},\mathcal{I},\varrho)\models^{\nu^{\prime}[y\leftarrow
c]}_{\widetilde{\Delta}}\phi*[{y}]$ this case contradicts thesemantics of CL.
∎

#### From Satisfiability to Looseness.

Given a SID $\Delta$ and a predicate $\mathsf{A}$, we build a SID
${\widetilde{\Delta}}$that defines a predicate $\widetilde{\mathsf{A}}$, of
equal arity, notoccurring in $\Delta$, such that
$\mathsf{Sat}[{\Delta},{\mathsf{A}}]$ has a positiveanswer if and only if
there exists a loose configuration $\gamma$and a store $\nu$, such that
$\gamma\models^{\nu}_{\widetilde{\Delta}}\widetilde{\mathsf{A}}(x_{1},\ldots,x_{\\#{\mathsf{A}}})$.
The rules of${\widetilde{\Delta}}$ are the rules of $\Delta$, to which the
following rule isadded, for some ports $p_{1},p_{2}\in\mathcal{P}$:

$\widetilde{\mathsf{A}}(x_{1},\ldots,x_{\\#{\mathsf{A}}})\leftarrow\exists
y_{1}\exists
y_{2}~{}.~{}\mathsf{A}(x_{1},\ldots,x_{\\#{\mathsf{A}}})*\langle{{y_{1}}.\mathit{p_{1}},{y_{2}}.\mathit{p_{2}}}\rangle$

This reduction is polynomial,because we add one rule, of size linear on
$\\#{\mathsf{A}}$.The following lemma states the correctness of the reduction:

###### Lemma 2

Given a SID $\Delta$ and a predicate $\mathsf{A}$, the
problem$\mathsf{Sat}[{\Delta},{\mathsf{A}}]$ has a positive answer if and only
if theproblem
$\mathsf{Loose}[{{\widetilde{\Delta}}},{\widetilde{\mathsf{A}}}]$ has a
positive answer.