# Verification of Component-based Systems with Recursive Architectures

Marius Bozga<EMAIL_ADDRESS>Radu Iosif  radu.iosif@univ-
grenoble-alpes.fr Joseph Sifakis<EMAIL_ADDRESS>Univ.
Grenoble Alpes, CNRS, Grenoble INP111Institute of Engineering Univ. Grenoble
Alpes, VERIMAG, 38000 Grenoble, France

###### Abstract

We study a sound verification method for parametric component-based systems.
The method uses a resource logic, a new formal specification language for
distributed systems consisting of a finite yet unbounded number of components.
The logic allows the description of architecture configurations coordinating
instances of a finite number of types of components, by means of inductive
definitions similar to the ones used to describe algebraic data types or
recursive data structures. For parametric systems specified in this logic, we
show that decision problems such as reaching deadlock or violating critical
section are undecidable, in general. Despite this negative result, we provide
for these decision problems practical semi-algorithms relying on the automatic
synthesis of structural invariants allowing the proof of general safety
properties. The invariants are defined using the $\mathsf{WS}\kappa{S}$
fragment of the monadic second order logic, known to be decidable by a
classical automata-logic connection, thus reducing a verification problem to
checking satisfiability of a $\mathsf{WS}\kappa{S}$ formula.

###### keywords:

Resource Logic , Component-based Distributed Systems , Parameterized
Verification

††journal: Theoretical Computer Science

##  1 Introduction

Mastering the complexity of a distributed system requires a deep understanding
of its coordination mechanisms. We distinguish between _endogenous_
coordination, that explicitly uses synchronization primitives in the code
describing the behavior of the components (e.g. semaphores, monitors, compare-
and-swap, etc.) and _exogenous_ coordination, that defines global rules
describing how the components interact. These two orthogonal paradigms play
different roles in the design of a system: exogenous coordination is used
during high-level model building, whereas endogenous coordination is
considered at a later stage of development, to implement the model using low-
level synchronization.

In this paper we focus on (high-level) _exogenous coordination of distributed
systems_ , consisting of a finite yet unbounded number of interconnected
components. Communication is assumed to be correct, i.e. we abstract from
packet losses and corruptions. Components behave according to a small set of
finite-state abstractions of sequential programs, whose transitions are
labeled with events. They communicate via interactions (handshaking) modeled
as sets of events that occur simultaneously in multiple components. For
instance, Fig. 1(a) shows a token-ring system, whose components are depicted
by yellow boxes containing state machines that represent their behavior and
whose architecture is the set of connectors between components depicted by
solid lines.

The separation between _behavior_ and _coordination_ is a fundamental
principle in the design of large-scale distributed systems [1]. This modular
view of a distributed system, in which the internal computation and the state
changes of each component are encapsulated in a well defined interface, is key
to scalable design methods that exploit a conceptual hierarchy. For instance,
a ring is a chain whose final output port is connected to the initial input
port, whereas a chain consists of a (head) component linked to a separate
(tail) chain as shown in Fig. 1(b). Moreover, system designers are accustomed
to using architectural patterns, such as rings, pipelines, stars, trees, etc.,
that define interactions between (unboundedly large) sets of components. Such
high-level models of real-life distributed systems are suitable for reasoning
about correctness in the early stages of system design, when details related
to network reliability or the implementation of coordination by means of low-
level synchronization mechanisms (e.g. semaphores, monitors, compare-and-swap,
etc.) are abstracted away.

###  1.1 Running Example

1$\cdots$$\mathit{out}$$\mathit{out}$$\mathit{out}$(a)$\mathit{in}$$\mathit{out}$$\mathit{in}$$\mathit{out}$$\mathfrak{t}$$\mathit{in}$$\mathit{out}$$\mathfrak{t}$$\mathit{in}$$\mathsf{S}[1]$$\mathit{in}$$\mathit{out}$$\mathit{in}$$\mathit{out}$$\mathfrak{t}$$\mathsf{S}[n]$$\mathsf{S}[n-1]$$\mathit{in}$$\mathit{in}$$\mathsf{T}[n-1,n]$$\mathsf{T}[n,1]$$\mathsf{S}[2]$(b)$\mathfrak{n}$$\mathfrak{t}$$\mathfrak{n}$$\mathfrak{n}$$\mathfrak{n}$$\mathsf{T}[1,2]$$\mathsf{S}(y_{1})$$\mathsf{S}(y^{1}_{1})$$\mathit{out}$$\mathit{out}$$\mathit{out}$$\mathit{Ring}()$$\mathit{Chain}(y^{1}_{1},y_{2})$$\mathit{Chain}(y_{1},y_{2})$33$\mathit{Chain}(y^{2}_{1},y_{2})$$\mathit{in}$$\mathit{in}$$\mathsf{T}(y_{1},y^{1}_{1})$$\mathsf{T}(y^{1}_{1},y^{2}_{1})$$\mathit{in}$

Figure 1: Recursive Specification of a Token-Ring System

For starters, we consider the following recursive definition of a token-ring
architecture, composed of a finite but unbounded number of stations that are
instances of the same component type $\mathsf{S}$, connected via transfer
connectors, of interaction type $\mathsf{T}$. The behavior of each station is
a machine with two states, indicating whether the station has a token
($\mathfrak{t}$) or not ($\mathfrak{n}$). The number of tokens is constant and
equal to the number of stations that are initially in state $\mathfrak{t}$.
Each station not having a token may receive a token from the left, via the in
port (that triggers the transition
$\mathfrak{n}\xrightarrow{{\scriptstyle\textit{in}}}\mathfrak{t}$) and send
its token to the right, via the out port (that triggers the transition
$\mathfrak{t}\xrightarrow{{\scriptstyle\textit{out}}}\mathfrak{n}$). We refer
to Fig. 1(a) for a depiction of a token-ring system, defined by the rules:

$\displaystyle\mathit{Ring}()$ $\displaystyle\leftarrow$ $\displaystyle\exists
y_{1}\exists y_{2}~{}.~{}\mathit{Chain}(y_{1},y_{2})*\mathsf{T}(y_{2},y_{1})$
(1) $\displaystyle\mathit{Chain}(x_{1},x_{2})$ $\displaystyle\leftarrow$
$\displaystyle\mathit{Comp}(x_{1})*\mathsf{T}(x_{1},x_{2})*\mathit{Comp}(x_{2})$
(2) $\displaystyle\mathit{Chain}(x_{1},x_{2})$ $\displaystyle\leftarrow$
$\displaystyle\exists
y_{1}~{}.~{}\mathit{Comp}(x_{1})*\mathsf{T}(x_{1},y_{1})*\mathit{Chain}(y_{1},x_{2})$
(3) $\displaystyle\mathit{Comp}(x_{1})$ $\displaystyle\leftarrow$
$\displaystyle\mathsf{S}^{\mathfrak{n}}(x_{1})$ (4)
$\displaystyle\mathit{Comp}(x_{1})$ $\displaystyle\leftarrow$
$\displaystyle\mathsf{S}^{\mathfrak{t}}(x_{1})$ (5)

Intuitively, rule 1 states that a token-ring consists of a chain of components
and an interaction between the out port of the last and the in port of the
first component in the chain. A chain consists of either two components and an
interaction between their out and in ports, respectively (rule 2), or a
component and an interaction between its out port and the in port of the first
component of a distinct chain (3). The rules (4) and (5) intuitively say that
a component has type $\mathsf{S}$ and can be in state $\mathfrak{n}$ or in
state $\mathfrak{t}$, respectively. The star symbol $*$ used in the rules 1-5
is a commutative and associative logical connective that composes sub-systems
with disjoint sets of components and interactions; for instance, in rule 2,
the two components declared as $\mathit{Comp}(x_{1})$ and
$\mathit{Comp}(x_{2})$ are necessarily different, meaning that $x_{1}$ and
$x_{2}$ cannot be mapped to the same value. The rules 2 and 3 correspond to
the base and the inductive case of a recursive definition of finite chains of
length at least two. We refer to Fig. 1(b) for a depiction of the recursive
unfolding of the above rules.

Note that no transfer of tokens is possible if the number of tokens in the
system is either zero (there is no token to be transfered) or equals the
number of components (there is no room to place a token). In this case, we say
that a system is in a _deadlock_. The decision problem “can a token-ring
started in a non-deadlock actually reach a deadlock?” is challenging, because
it requires a proof that holds for systems of _any_ size, i.e. number of
components and interactions. We show that, even if such problems are
undecidable, in general, a large number of instances of these problems can be
handled by the methods developed in this paper.

###  1.2 Contributions of this Work

The parameterized verification method presented in this paper relies on an
idea reported in [2]. In addition to a complete development of the technical
results, previously omitted for space reasons, here we apply the verification
method to a specification language based on a resource logic, that resembles
Separation Logic [3], instead of the recursive term algebra introduced in [2].
An extension of this resource logic has been recently developed for Hoare-
style reasoning about the safety properties of programmed reconfiguration in
distributed systems [4], to which the work presented here provides a push-
button verification back-end. In combination with the proof system reported in
[4], the verification method presented in this paper can automatically prove
the correctness of a distributed system _after the reconfiguration of its
coordinating architecture_. Since various dialects of (Concurrent) Separation
Logic are being commonly used to specify and reason about concurrent systems
[5, 6, 7], we expect this new logic to be easily accepted by the research and
development community. The contribution of this paper is three-fold:

  1. 1.

We introduce a logic-based language, called Configuration Logic (CL), to
describe the sets of configurations (i.e. architectures and local states of
components) of distributed systems parameterized by (i) the number of
components of each type that are active in the system, e.g. a system with $n$
readers and $m$ writers, in which $n$ and $m$ are not known a priori and (ii)
the pattern in which the interactions occur (e.g. a pipeline, ring, star or
more general hypergraph structures). The language uses predicate symbols to
hierarchically break the architecture into specific patterns. The
interpretation of these predicate symbols is defined inductively by rewriting
rules consisting of formulæ that contain predicate atoms, in a way that
recalls the usual definitions of algebraic datatypes [8] or heaps [3].

  2. 2.

We tackle a parametric safety problem concerning systems described in this
language, which is essentially checking that the reachable states of every
instance stays clear of a set of global error configurations, such as
deadlocks or critical section violations. In particular, we show that both the
parametric deadlock freedom and critical section violation problems are
undecidable, even for architectures as simple as a chain of components.

  3. 3.

We develop a verification method that synthesizes parametric invariants from
the syntactic description of the architecture (in CL) and from the behavior of
its components (finite-state machines). The invariants and the set of error
configurations are both described using a decidable fragment of Monadic Second
Order Logic (MSO), that enables the use of off-the-shelf solvers for checking
the resulting verification conditions.

Configuration
Logicpathautomatonflowformulatrap/mutexinvariantsSIDrewritingtreesinitialconfigurationsDeadlockReachabilityformula(e)behaviorMonadic
Second Order LogicFinite-state Machines

Figure 2: The Synthesis of Verification Conditions

The stages of the synthesis of verification conditions are depicted in Fig. 2.
The starting point is a set of inductive definitions and a CL formula
describing the initial configurations of the system, together with a
description of component behavior by finite-state machines. The CL formula
uses inductively defined predicate symbols defined by sets of rewriting trees,
describing the unfoldings of their inductive definitions. In particular, these
rewriting trees describe architectures, up to a permutation of the indices of
components of each type.

We use rewriting trees as the backbones of architecture encoding, from which
we derive a MSO  _flow formula_ , that essentially describes the operational
semantics induced by the interactions of the architecture, relying on (i) a
static description of the profile of the interactions (how they glue component
types), and (ii) the transition systems describing the behavior of component
types in the architecture. The main technical problem in building flow formulæ
is tracking the identities and values of the variables that occur within
predicate symbols, which, in turn, are recursively replaced by their
definitions, in a rewriting tree. For instance, the $y_{2}$ variable
introduced by rule (1) using existential quantification substitutes the
$x_{2}$ variable from the definition of a $\mathit{Chain}$ predicate, in rules
(2) and (3) several times, before the same variable ($y_{2}$) substitutes the
$x_{1}$ variable in rule (4) or (5) (§1.1). This is achieved by defining a
_path automaton_ that traverses the rewriting tree downwards tracking the
introduction of a variable by existential quantification in a rule to the rule
where it is instantiated in a component atom.

The flow formula is subsequently used to define invariants, i.e. over-
approximations of the sets of states reachable from some initial
configuration, in a system defined by some unfolding (rewriting) of the
predicate symbols in CL specifications. In contrast with the classical
approach of invariant inference using, e.g. abstract interpretation [9], our
technique generates invariants as MSO formulæ obtained directly from the flow
formulæ, by a syntactic translation. Analogously, the set of error
configurations (deadlocks and critical section violations) is obtained
directly from the flow formula of the system. The verification condition asks
that the conjunction of the MSO formulæ describing the invariant and error
configurations, respectively, is unsatisfiable; a satisfiable verification
condition might indicate the presence of a spurious error caused by the over-
approximation introduced by the invariant synthesis. Since we represent the
configurations of a system by rewriting trees, we use a decidable fragment of
MSO, interpreted over trees to answer the verification condition
automatically.

The paper is structured as follows. Section 2 introduces the definitions of
component-based systems and their operational semantics, Section 3 describes
the resource logic used to define sets of configurations, Section 4 describes
the parametric decision problems and gives the general undecidability results,
Section 5 defines rewriting trees formally, together with a notion of a
canonical model, induced by a rewriting tree of a logical formula, Section 6
describes the invariant synthesis and the encoding of the verification
conditions in MSO, Section 8 gives concluding remarks and sketches directions
for future work.

##  2 Component-based Systems

###  2.1 Definitions

This section introduces the definitions needed to formally describe our model
of component-based systems. We denote by $\mathbb{N}$ the set of natural
numbers. Given integers $i$ and $j$, we write $[{i},{j}]$ for the set
$\\{{i,i+1,\ldots,j}\\}$, assumed to be empty if $i>j$. For a set $A$ and an
integer $i\geq 1$, we denote by $A^{i}$ the $i$-times Cartesian product of $A$
with itself. By $\mathrm{pow}({A})$ we denote the powerset of $A$. For a
finite set $A$, we denote by $|\\!|{A}|\\!|$ its cardinality.

Let $\mathbb{P}$ be a countable set of _ports_. We consider classes of
component-based systems that share the same _signature_
$\Sigma=(\mathfrak{C},\mathfrak{I},\mathfrak{P})$, where:

  * •

$\mathfrak{C}=\\{{\mathsf{C}_{1},\ldots,\mathsf{C}_{N}}\\}$ is a finite set of
relation symbols of arity one, called _component types_ ,

  * •

$\mathfrak{I}=\\{{\mathsf{I}_{1},\ldots,\mathsf{I}_{M}}\\}$ is a finite set of
relation symbols of arity $\\#(\mathsf{I}_{j})\geq 1$, called _interaction
types_ ,

  * •

$\mathfrak{P}:\mathfrak{C}\cup\mathfrak{I}\rightarrow\mathrm{pow}({\mathbb{P}})\cup\bigcup_{i\geq
1}\mathbb{P}^{i}$ is an _interface_ associating each component type
$\mathsf{C}\in\mathfrak{C}$ a finite set of ports
$\mathfrak{P}({\mathsf{C}})\in\mathrm{pow}({\mathbb{P}})$ and each interaction
type $\mathsf{I}\in\mathfrak{I}$ a finite tuple of ports
$\mathfrak{P}({\mathsf{I}})\in\mathbb{P}^{\\#(\mathsf{I})}$.

W.l.o.g., we assume that
$\bigcup_{i=1}^{N}\mathfrak{P}({\mathsf{C}_{i}})=\mathbb{P}$ and
$\mathfrak{P}({\mathsf{C}_{i}})\cap\mathfrak{P}({\mathsf{C}_{j}})=\emptyset$,
for all $1\leq i<j\leq N$, i.e. each port $p$ belongs to the interface of
exactly one component type, denoted by $\mathit{comp}({p})$. We denote by
$\mathfrak{I}^{(k)}$ the subset of interaction types of arity $k$, formally
$\mathfrak{I}^{(k)}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{\mathsf{I}\in\mathfrak{I}~{}|~{}\\#(\mathsf{I})=k\\}$,
for any $k\geq 1$.

######  Example 1 (contd. from §1.1)

The signature for the token-ring example from Fig. 1a is
$\Sigma=\langle{\\{{\mathsf{S}}\\},\\{{\mathsf{T}}\\},\mathfrak{P}}\rangle$,
where $\mathfrak{P}({\mathsf{S}})=\\{{\textit{in},\textit{out}}\\}$ and
$\mathfrak{P}({\mathsf{T}})=\langle{\textit{out},\textit{in}}\rangle$, i.e.
the interaction type $\mathsf{T}$ connects an out port to an in port.
$\blacksquare$

The component and interaction types are interpreted as sets and relations over
a countably infinite _universe_ $\mathbb{U}$ of indices. The particular nature
of indices is not important at this point; we assume that two indices can only
be compared for equality, with no other associated relation or function. An
_architecture_ $\alpha$ over the signature
$\Sigma=(\mathfrak{C},\mathfrak{I},\mathfrak{P})$ associates each component
type $\mathsf{C}_{i}$ a set $\alpha(\mathsf{C}_{i})\subseteq\mathbb{U}$ and
each interaction type $\mathsf{I}_{j}$ a relation
$\alpha(\mathsf{I}_{j})\subseteq\mathbb{U}^{\\#(\mathsf{I}_{j})}$, defining:

  * •

_components_ $\mathsf{C}_{i}[u]$, for some $u\in\alpha(\mathsf{C}_{i})$, and

  * •

_interactions_ $\mathsf{I}_{j}[u_{1},\ldots,u_{\\#(\mathsf{I}_{j})}]$, for
some
$\langle{u_{1},\ldots,u_{\\#(\mathsf{I}_{j})}}\rangle\in\alpha(\mathsf{I}_{j})$.

Intuitively, an architecture is a description of the static structure of a
system. Note that an index $u\in\mathbb{U}$ can refer two (or more) different
components $\mathsf{C}_{1}[u]$ and $\mathsf{C}_{2}[u]$ belonging to different
component types and similarly, a tuple of indices $\mathbf{u}$ can refer two
(or more) different interactions $\mathsf{I}_{1}[\mathbf{u}]$ and
$\mathsf{I}_{2}[\mathbf{u}]$ of different interaction types, with the same
arity; interactions may occur disconnected from components, e.g.
$\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}]$ does not necessarily mean that
each component
$\mathit{comp}({\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{i}})[u_{i}]$, for
all $i\in[{1},{\\#(\mathsf{I})}]$ is present in the structure.

######  Example 2 (contd. from Example 1)

Letting indices be natural numbers, the structure of Fig. 1a is described by
the architecture $\alpha$ over $\Sigma$, such that
$\alpha(\mathsf{S})=[{1},{n}]$ and
$\alpha(\mathsf{T})=\\{\langle{1,2}\rangle,\langle{2,3}\rangle,\ldots,\langle{n,1}\rangle\\}\rangle$,
for some $n\geq 2$. $\blacksquare$

A _behavior_ is described by a finite state machine
$M=(Q,P,\xrightarrow{{\scriptstyle}})$, where $Q$ is a finite set of states,
$P\subseteq\mathbb{P}$ is a finite set of ports and
$\xrightarrow{{\scriptstyle}}\subseteq Q\times P\times Q$ is a transition
relation; we write $q\xrightarrow{{\scriptstyle p}}q^{\prime}$ instead of
$(q,p,q^{\prime})\in\xrightarrow{{\scriptstyle}}$. Let $\mathbb{B}$ be the set
of finite-state machines with ports from $\mathbb{P}$. The _behavior map_
$\beta:\mathfrak{C}\rightarrow\mathbb{B}$ associates each component type
$\mathsf{C}\in\mathfrak{C}$ with a state machine
$\beta({\mathsf{C}})=(Q_{\mathsf{C}},\mathfrak{P}({\mathsf{C}}),\xrightarrow{{\scriptstyle}}_{{\scriptstyle\mathsf{C}}})$,
whose set of states is denoted by
$\mathit{states}_{\beta}({\mathsf{C}})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}Q_{\mathsf{C}}$.
In the following, we consider w.l.o.g. that
$\mathit{states}_{\beta}({\mathsf{C}_{i}})\cap\mathit{states}_{\beta}({\mathsf{C}_{j}})=\emptyset$,
for all $1\leq i<j\leq N$ and define
$\mathcal{Q}_{\beta}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\bigcup_{i=1}^{N}\mathit{states}_{\beta}({\mathsf{C}_{i}})$.

######  Example 3 (contd. from Example 1)

The behavior of the component type $\mathsf{S}$ in Fig. 1a is described by the
state machine
$\beta({\mathsf{S}})=(\\{{\mathfrak{t},\mathfrak{n}}\\},\\{{\textit{in},\textit{out}}\\},\xrightarrow{{\scriptstyle}})$,
with transitions
$\mathfrak{n}\xrightarrow{{\scriptstyle\textit{in}}}\mathfrak{t}$ and
$\mathfrak{t}\xrightarrow{{\scriptstyle\textit{out}}}\mathfrak{n}$.
$\blacksquare$

For a port $p$ we denote by $T_{\beta}{}(p)$ the set of transitions labeled by
$p$ in the finite-state machine associated by $\beta$ to $\mathit{comp}({p})$.
We extend this notation to tuples of ports by taking
$T_{\beta}{}(\langle{p_{1},\ldots,p_{n}}\rangle)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}T_{\beta}{}(p_{1})\times\cdots\times
T_{\beta}{}(p_{n})$. That is, the set
$T_{\beta}{}(\langle{p_{1},\ldots,p_{n}}\rangle)$ contains $n$-tuples of
transitions $\langle{t_{1},\ldots,t_{n}}\rangle$ labeled respectively with
ports $\langle{p_{1},\ldots,p_{n}}\rangle$. For an interaction $\mathsf{I}$ we
use $T_{\beta}{}(\mathsf{I})$ as a shortcut for
$T_{\beta}{}(\mathfrak{P}({\mathsf{I}}))$. In particular,
$T_{\beta}{}(\mathsf{I})$ contains the set of tuples of component’s
transitions that are _synchronizing_ by interaction $\mathsf{I}$.

A _system_ $\mathfrak{S}$ is a tuple $(\Sigma,\alpha,\beta)$, where $\alpha$
is an architecture and $\beta$ is a behavior associated with the signature
$\Sigma$. When $\Sigma$ is clear from the context, we omit it and denote a
system as $(\alpha,\beta)$.

###  2.2 Operational Semantics

We represent the operational semantics of a system as a Petri net, recalled
below for self-containment reasons. A _Petri net_ is a tuple
$\mathsf{N}=(S,T,E)$, where $S$ is a set of _places_ , $T$ is a set of
_transitions_ , $S\cap T=\emptyset$, and $E\subseteq(S\times T)\cup(T\times
S)$ is a set of _edges_. Given $x,y\in S\cup T$, we write
$E(x,y)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}1$ if
$(x,y)\in E$ and
$E(x,y)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}0$,
otherwise. Let
$\text{$\leftidx{{}^{\bullet}}{\text{${x}$}}$}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{y\in
S\cup T\mid E(y,x)=1}\\}$,
${x}^{\bullet}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{y\in
S\cup T\mid E(x,y)=1}\\}$ and lift these definitions to sets of nodes. A
_marking_ of $\mathsf{N}$ is a function $\mathrm{m}:S\rightarrow\mathbb{N}$. A
transition $t$ is _enabled_ in $\mathrm{m}$ if and only if $\mathrm{m}(s)>0$
for each place $s\in\text{$\leftidx{{}^{\bullet}}{\text{${t}$}}$}$. We write
$\mathrm{m}\xrightarrow{{\scriptstyle t}}\mathrm{m}^{\prime}$ whenever $t$ is
enabled in $\mathrm{m}$ and
$\mathrm{m}^{\prime}(s)=\mathrm{m}(s)-E(s,t)+E(t,s)$, for all $s\in S$ and
$t\in T$. A sequence of transitions $\sigma=t_{1},\ldots,t_{n}$ is a _firing
sequence_ , written
$\mathrm{m}\xrightarrow{{\scriptstyle\sigma}}\mathrm{m}^{\prime}$ if and only
if either (i) $n=0$ and $\mathrm{m}=\mathrm{m}^{\prime}$, or (ii) $n\geq 1$
and there exist markings $\mathrm{m}_{1},\ldots,\mathrm{m}_{n-1}$ such that
$\mathrm{m}\xrightarrow{{\scriptstyle
t_{1}}}\mathrm{m}_{1}\ldots\mathrm{m}_{n-1}\xrightarrow{{\scriptstyle
t_{n}}}\mathrm{m}^{\prime}$. A marking $\mathrm{m}$ is a _deadlock_ of a Petri
net $\mathsf{N}=(S,T,E)$ if and only if no transition $t\in T$ is enabled in
$\mathrm{m}$ and let $\mathit{Dead}({\mathsf{N}})$ denote the set of deadlocks
of $\mathsf{N}$.

A _marked Petri net_ is a pair $\mathcal{N}=(\mathsf{N},\mathrm{m}_{0})$,
where $\mathrm{m}_{0}$ is the _initial marking_ of $\mathsf{N}$. A firing
sequence is _initial_ if it starts in $\mathrm{m}_{0}$. A marking $\mathrm{m}$
is _reachable_ in $\mathcal{N}$ if there exists an initial firing sequence
ending in $\mathrm{m}$. Let $\mathit{Reach}({\mathcal{N}})$ (resp.
$\mathit{Step}({\mathcal{N}})$) be the set of markings reachable (in one step)
in $\mathcal{N}$. For simplicity, we write
$\mathit{Reach}({\mathsf{N},\mathrm{m}_{0}})$ and
$\mathit{Step}({\mathsf{N},\mathrm{m}_{0}})$ instead of
$\mathit{Reach}({(\mathsf{N},\mathrm{m}_{0})})$ and
$\mathit{Step}({(\mathsf{N},\mathrm{m}_{0})})$, respectively. A marked Petri
net $\mathcal{N}$ is _boolean_ 222Boolean Petri nets are sometimes called
$1$-safe or $1$-bounded in the literature. if $\mathrm{m}(s)\leq 1$, for each
$s\in S$ and $\mathrm{m}\in\mathit{Reach}({\mathcal{N}})$. All marked Petri
nets considered in the following will be boolean and we blur the distinction
between a marking $\mathrm{m}:S\rightarrow\\{{0,1}\\}$ and the set $\\{{s\in
S\mid\mathrm{m}(s)=1}\\}$, by writing $s\in\mathrm{m}$ (resp.
$s\not\in\mathrm{m}$) instead of $\mathrm{m}(s)=1$ (resp. $\mathrm{m}(s)=0$).

###### Definition 1

The _operational semantics_ of a system $\mathfrak{S}=(\Sigma,\alpha,\beta)$
with signature $\Sigma=(\mathfrak{C},\mathfrak{I},\mathfrak{P})$ is
represented by the Petri net $\mathsf{N}({\mathfrak{S}})=(S,T,E)$, where:

$\begin{array}[]{rcl}S&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\bigcup_{\mathsf{C}\in\mathfrak{C}}\\{{~{}q[u]~{}\mid~{}q\in\mathit{states}_{\beta}({\mathsf{C}}),~{}u\in\alpha(\mathsf{C})~{}}\\}\\\\[8.53581pt]
T&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\bigcup_{\mathsf{I}\in\mathfrak{I}}\\{~{}(\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)~{}\mid~{}\langle{p_{1},\ldots,p_{\\#(\mathsf{I})}}\rangle=\mathfrak{P}({\mathsf{I}}),\\\\[2.84526pt]
&&\hskip
42.67912pt\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in\alpha(\mathsf{I}),~{}\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle\in
T_{\beta}{}(\mathsf{I}),\\\\[2.84526pt] &&\hskip 42.67912pt\forall
i,j\in[{1},{\\#(\mathsf{I})}].~{}i\not=j\Rightarrow u_{i}\not=u_{j}\mbox{ or
}\mathit{comp}({p_{i}})\not=\mathit{comp}({p_{j}})~{}\\}\\\\[8.53581pt]
E&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\bigcup_{\mathsf{I}\in\mathfrak{I}}\\{~{}(q[u_{i}],(\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)),\\\\[2.84526pt]
&&\hskip
28.45274pt((\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle),q^{\prime}[u_{i}])~{}\mid{}\\\\[2.84526pt]
&&\hskip 42.67912ptt_{i}=(q\xrightarrow{{\scriptstyle
p_{i}}}q^{\prime}),~{}i\in[{1},{\\#(\mathsf{I})}]~{}\\}\end{array}$

The places, transitions and edges of $\mathsf{N}({\mathfrak{S}})$ are defined
jointly by the architecture $\alpha$ and the behavior $\beta$. For every
component $\mathsf{C}[u]$ in $\alpha$, the Petri net contains the places
$q[u]$, for each state $q$ in $\mathit{states}_{\beta}({\mathsf{C}})$. For
every interaction $\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}]$ in $\alpha$,
the Petri net contains one transition for every tuple
$\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle$ of transitions of component
types behavior, which are _synchronizing_ according to $\mathsf{I}$, that is,
where their labeling ports $\langle{p_{1},\ldots,p_{\\#(\mathsf{I})}}\rangle$
form the tuple $\mathfrak{P}(\mathsf{I})$. Moreover, a transition
corresponding to an interaction $\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}]$
involves pairwise distinct components; the last condition in the definition of
$T$ above requires that $u_{i}\neq u_{j}$ or
$\mathit{comp}({p_{i}})\neq\mathit{comp}({p_{j}})$. Finally, edges are defined
according to the tuple of synchronizing transitions
$\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle$ and connect to pre- and
post- places, respectively $q[u_{i}]$ and $q^{\prime}[u_{i}]$, for each
involved component $\mathsf{C}[u_{i}]$. For the sake of clarity we omit
writing the tuple $\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle$ when it
is determined by $\mathsf{I}$, namely for those behaviors where a port labels
exactly one transition, in each state machine, as it is the case in the
example below:

######  Example 4 (contd. from Example 3)

$\mathsf{T}[1,2]$$\mathfrak{t}[1]$$\mathfrak{n}[2]$$\mathfrak{t}[2]$$\mathfrak{n}[n]$$\mathfrak{t}[n]$$\mathsf{T}[n-1,n]$$\mathsf{T}[2,3]$$\mathsf{T}[n,1]$$\ldots$$\mathsf{T}[n,1]$$\mathfrak{n}[1]$

Figure 3: The Execution Semantics of a Token-Ring System

The Petri net describing the execution semantics of the token-ring system from
Fig. 1(a) is given in Fig. 3. Consider the marking of this Petri net depicted
in dashed lines. From this marking, the sequence of interactions
$\mathsf{T}[1,2],\mathsf{T}[2,3],\ldots,\mathsf{T}[n-1,n],\mathsf{T}[n,1]$ can
be fired any number of times, in this order. These interactions correspond to
the joint execution of the transitions labeled by the ports $\mathit{out}$ and
$\mathit{in}$, from any two adjacent components $i$ and $(i\mod n)+1$ of the
ring, respectively. $\blacksquare$

The executions of a system $\mathfrak{S}=(\Sigma,\alpha,\beta)$ can be
represented by the firing sequences of a marked Petri net involving only those
boolean markings of $\mathsf{N}(\mathfrak{S})$, that contain exactly one state
$q\in\mathit{states}_{\beta}({\mathsf{C}})$ per component $\mathsf{C}[u]$,
such that $u\in\alpha(\mathsf{C})$. We formalize and prove this fact below:

###### Definition 2

Given a system $\mathfrak{S}=(\Sigma,\alpha,\beta)$ with signature
$\Sigma=(\mathfrak{C},\mathfrak{I},\mathfrak{P})$, a marking $\mathrm{m}$ of
the Petri net $\mathsf{N}(\mathfrak{S})=(S,T,E)$ is _precise_ if and only if,
for each $\mathsf{C}\in\mathfrak{C}$ and each $u\in\alpha(\mathsf{C})$, we
have $|\\!|{\mathrm{m}\cap\\{{q[u]\mid
q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}}|\\!|=1$.

###### Proposition 1

Given a system $\mathfrak{S}$ and a precise initial marking $\mathrm{m}_{0}$
of $\mathsf{N}({\mathfrak{S}})$, every marking
$\mathrm{m}\in\mathit{Reach}({\mathsf{N}({\mathfrak{S}}),\mathrm{m}_{0}})$ is
precise.

_Proof_ : Let $\mathfrak{S}=(\Sigma,\alpha)$ and
$\mathrm{m}^{\prime}\in\mathit{Reach}({\mathsf{N}({\mathfrak{S}}),\mathrm{m}_{0}})$
be a marking. The proof goes by the length $n\geq 0$ of the firing sequence
taking $\mathrm{m}_{0}$ into $\mathrm{m}^{\prime}$. For the base case $n=0$,
we have that $\mathrm{m}^{\prime}=\mathrm{m}_{0}$ is precise, by hypothesis.
For the inductive step $n\geq 1$, let $\mathrm{m}$ be the predecessor of
$\mathrm{m}^{\prime}$ in the sequence, hence $\mathrm{m}$ is precise for
$\mathfrak{S}$, by the inductive hypothesis. Then, by Def. 1, there exists a
transition
$(\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)$
in $T$, such that

$\displaystyle\mathrm{m}^{\prime}=(\mathrm{m}\setminus\\{{q_{1}[u_{1}],\ldots,q_{\\#(\mathsf{I})}[u_{\\#(\mathsf{I})}]}\\})\cup\\{{q_{1}^{\prime}[u_{1}],\ldots,q_{\\#(\mathsf{I})}^{\prime}[u_{\\#(\mathsf{I})}]}\\}$
(6)

where
$\mathfrak{P}({\mathsf{I}})=\langle{p_{1},\ldots,p_{\\#(\mathsf{I})}}\rangle$
and $t_{i}=(q_{i}\xrightarrow{{\scriptstyle
p_{i}}}q^{\prime}_{i})\in\xrightarrow{{\scriptstyle}}_{{\scriptstyle\mathit{comp}({p_{i}})}}$
for all $i\in[{1},{\\#(\mathsf{I})}]$ and moreover $u_{i}\not=u_{j}$ or
$\mathit{comp}({p_{i}})\not=\mathit{comp}({p_{j}})$ for all distinct
$i,j\in[{1},{\\#(\mathsf{I})}]$.

Let $\mathsf{C}\in\mathfrak{C}$ be a component type and let
$u\in\alpha(\mathsf{C})$ be an index. Since $\mathrm{m}$ is precise, we have
$\mathrm{m}\cap\\{{q[u]\mid
q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}=\\{{q^{*}[u]}\\}$, for some
state $q^{*}$. We distinguish the following cases:

  * •

$u=u_{i}$ for some $i\in[{1},{\\#(\mathsf{I})}]$ and $q^{*}=q_{i}$ In this
case, we have:

$\mathrm{m}^{\prime}\cap\\{{q[u]\mid
q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}=\\{{q_{i}^{\prime}[u]}\\}\text{,
by definition of $\mathrm{m}^{\prime}$ in (\ref{eq:amarkprime})}$

  * •

$u=u_{i}$ for some $i\in[{1},{\\#(\mathsf{I})}]$ and $q^{*}\not=q_{i}$. In
this case, as the transition
$(\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{{\\#(\mathsf{I})}}}\rangle)$
fires in $\mathrm{m}$ it follows that $q_{i}[u]\in\mathrm{m}$. But then
$q_{i}[u]\in\mathrm{m}\cap\\{{q[u]\mid
q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}=\\{q^{*}[u]\\}$ implies
$q_{i}=q^{*}$, which is a contradiction.

  * •

$u\not\in\\{{u_{1},\ldots,u_{\\#(\mathsf{I})}}\\}$. In this case, we have:

$\mathrm{m}\cap\\{{q[u]\mid
q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}=\mathrm{m}^{\prime}\cap\\{{q[u]\mid
q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}$

In all non-contradictory cases, we obtain that
$|\\!|{\mathrm{m}\cap\\{{q[u]\mid
q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}}|\\!|=1$. Because
$\mathsf{C}\in\mathfrak{C}$ and $u\in\alpha(\mathsf{C})$ are arbitrary,
$\mathrm{m}$ is precise for $\mathfrak{S}$.

##  3 The Configuration Logic

By _configuration_ of a system, we understand the architecture describing the
components and interactions from the system, together with a snapshot of its
current state. Configurations are used to reason about _parametric_ systems,
that share a common architectural pattern (style) and differ in the number of
instances of a certain component type. For instance, a token-ring (Fig. 1)
applies the same architectural pattern (the output of each component is
connected to its right neighbor in a round-robin fashion) to any number $n\geq
2$ of components.

###### Definition 3

A _configuration_ of a system $\mathfrak{S}=(\Sigma,\alpha,\beta)$ is a pair
$(\alpha,\mathrm{m})$, where $\alpha$ is an architecture over the signature
$\Sigma$ and $\mathrm{m}$ is a precise marking of
$\mathsf{N}({\mathfrak{S}})$.

We aim at describing sets of configurations recursively (i.e. configurations
with more complex structure being obtained by composing simpler ones), using
the following definition of composition:

###### Definition 4

Two architectures $\alpha_{1}$ and $\alpha_{2}$, over the signature
$\Sigma=(\mathfrak{C},\mathfrak{I},\mathfrak{P})$, are _disjoint_ if and only
if $\alpha_{1}(\mathsf{C})\cap\alpha_{2}(\mathsf{C})=\emptyset$, for all
$\mathsf{C}\in\mathfrak{C}$ and
$\alpha_{1}(\mathsf{I})\cap\alpha_{2}(\mathsf{I})=\emptyset$, for all
$\mathsf{I}\in\mathfrak{I}$. If $\alpha_{1}$ and $\alpha_{2}$ are disjoint,
the _composition_ of configurations $(\alpha_{1},\mathrm{m}_{1})$ and
$(\alpha_{2},\mathrm{m}_{2})$ is
$(\alpha_{1},\mathrm{m}_{1})\bullet(\alpha_{2},\mathrm{m}_{2})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}(\alpha_{1}\cup\alpha_{2},\mathrm{m}_{1}\cup\mathrm{m}_{2})$,
where $\alpha_{1}\cup\alpha_{2}$ denotes the pointwise union of the
architectures $\alpha_{1}$ and $\alpha_{2}$:

  * •

$(\alpha_{1}\cup\alpha_{2})(\mathsf{C})=\alpha_{1}(\mathsf{C})\cup\alpha_{2}(\mathsf{C})$,
for each $\mathsf{C}\in\mathfrak{C}$,

  * •

$(\alpha_{1}\cup\alpha_{2})(\mathsf{I})=\alpha_{1}(\mathsf{I})\cup\alpha_{2}(\mathsf{I})$,
for each $\mathsf{I}\in\mathfrak{I}$.

The composition
$(\alpha_{1},\mathrm{m}_{1})\bullet(\alpha_{2},\mathrm{m}_{2})$ is undefined
if $\alpha_{1}$ and $\alpha_{2}$ are not disjoint.

It is easy to check that the composition of configurations
$(\alpha_{1},\mathrm{m}_{1})$ and $(\alpha_{2},\mathrm{m}_{2})$ with disjoint
architectures is again a configuration, in particular
$\mathrm{m}_{1}\cap\mathrm{m}_{2}=\emptyset$ and
$\mathrm{m}_{1}\cup\mathrm{m}_{2}$ is a precise marking of the Petri net
$\mathsf{N}({\Sigma,\alpha_{1}\cup\alpha_{2},\beta})$.

We introduce the _configuration logic_ (CL) to describe (possibly infinite)
sets of configurations, via inductive definitions. Let
$\Sigma=(\mathfrak{C},\mathfrak{I},\mathfrak{P})$ be a signature and
$\beta:\mathfrak{C}\rightarrow\mathbb{B}$ be a behavior map, fixed for the
rest of this section. Let $\mathbb{X}^{1}$ be a set of first-order variables
and $\mathbb{A}$ be a countably infinite set of predicate symbols, where
$\\#(\mathcal{A})\geq 0$ denotes the arity of a predicate symbol
$\mathcal{A}\in\mathbb{A}$. The formulæ of CL are inductively defined by the
following syntax:

$\begin{array}[]{rcl}\phi&::=&\mathsf{emp}\mid\mathsf{C}(x)\mid\mathsf{C}^{q}(x)\mid\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})\mid\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\mid\phi*\phi\mid\exists
x~{}.~{}\phi\end{array}$

where $\mathsf{C}\in\mathfrak{C}$ are component types,
$q\in\mathit{states}_{\beta}({\mathsf{C}})$ are states,
$\mathsf{I}\in\mathfrak{I}$ are interaction types, $\mathcal{A}\in\mathbb{A}$
are predicate symbols and $x_{1},x_{2},\ldots\in\mathbb{X}^{1}$ denote first-
order variables. Atomic formulæ of the form $\mathsf{C}(x)$ or
$\mathsf{C}^{q}(x)$, $\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})$ and
$\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})$ are called _component_ ,
_interaction_ and _predicate atoms_ , respectively. The logical connective $*$
is an associative and commutative _separating conjunction_ operator.

By $\mathrm{fv}({\phi})$ we denote the set of free variables that do not occur
within the scope of a quantifier; $\phi$ is called _quantifier-free_ (q.f.) if
and only if it has no quantifiers and a _sentence_ if and only if
$\mathrm{fv}({\phi})=\emptyset$, respectively. A _substitution_ is a partial
mapping $\theta:\mathbb{X}^{1}\rightarrow\mathbb{X}^{1}$ and $\phi\theta$ is
the formula obtained by replacing each variable
$x\in\mathrm{fv}({\phi})\cap\mathrm{dom}({\theta})$ by $\theta(x)$ in $\phi$,
where
$\mathrm{dom}({\theta})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{x\in\mathbb{X}^{1}\mid\theta\text{
is defined at }x}\\}$. We denote by $[x_{1}/y_{1},\ldots,x_{k}/y_{k}]$ the
substitution that replaces $x_{i}$ with $y_{i}$, for all $i\in[{1},{k}]$ and
is undefined everywhere else. This notation is extended to tuples of variables
of equal length as $[\mathbf{x}/\mathbf{y}]$, where
$\mathbf{x}=\langle{x_{1},\ldots,x_{k}}\rangle$ and
$\mathbf{y}=\langle{y_{1},\ldots,y_{k}}\rangle$.

Intuitively, a formula $\mathsf{emp}$ describes configurations with empty
architecture, $\mathsf{C}(x)$ (resp. $\mathsf{C}^{q}(x)$) describes
configurations with architectures consisting of a single instance of the
component type $\mathsf{C}$, indexed by the value of $x$ (resp. in state $q$),
and $\mathsf{I}(x_{1},\ldots,x_{k})$ describes a single interaction of type
$\mathsf{I}$, between components indexed by $x_{1},\ldots,x_{k}$,
respectively. The formula
$\mathsf{C}^{q_{1}}(x_{1})*\ldots*\mathsf{C}^{q_{k}}(x_{k})*\mathsf{I}(x_{1},\ldots,x_{k})$
describes an architecture consisting of $k$ _pairwise distinct_ instances of
the component type $\mathsf{C}$, in states $q_{1},\ldots,q_{k}$, respectively,
joined by an interaction of type $\mathsf{I}$. The formula
$\mathsf{I}(x_{1},\ldots,x_{k})*\mathsf{I}(x^{\prime}_{1},\ldots,x^{\prime}_{k})$
states the existence of two interactions of type $\mathsf{I}$, with _distinct_
tuples of indices, given by the values of $\langle{x_{1},\ldots,x_{k}}\rangle$
and $\langle{x^{\prime}_{1},\ldots,x^{\prime}_{k}}\rangle$, respectively, i.e.
the values of $x_{i}$ and $x^{\prime}_{i}$ must differ for at least one
$i\in[{1},{k}]$.

The semantics of CL formulæ is given by a satisfaction relation
$\models_{\Delta}^{\mathfrak{s}}$ between configurations and formulæ. This
relation is parameterized by:

  * •

a _store_ $\mathfrak{s}:\mathbb{X}^{1}\rightarrow\mathbb{U}$, i.e. a function
mapping variables to indices, and

  * •

a _set of inductive definitions_ (SID) $\Delta$ consisting of rules of the
form $\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi$, where
$\phi$ is a CL formula such that
$\mathrm{fv}({\phi})=\\{{x_{1},\ldots,x_{\\#(\mathcal{A})}}\\}$.

The satisfaction relation is defined inductively on the structure of the
formulæ:

$\begin{array}[]{rclcl}(\alpha,\mathrm{m})&\models^{\mathfrak{s}}_{\Delta}&\mathsf{emp}&\iff&\alpha(\mathsf{C})=\emptyset\text{,
for all $\mathsf{C}\in\mathfrak{C}$, }\alpha(\mathsf{I})=\emptyset,\\\
&&&&\text{for all $\mathsf{I}\in\mathfrak{I}$ and
$\mathrm{m}=\emptyset$}\\\\[5.69054pt]
(\alpha,\mathrm{m})&\models^{\mathfrak{s}}_{\Delta}&\mathsf{C}(x)&\iff&\alpha(\mathsf{C})=\\{{\mathfrak{s}(x)}\\},~{}\alpha(\mathsf{C}^{\prime})=\emptyset\text{,
for all }\\\
&&&&\mathsf{C}^{\prime}\in\mathfrak{C}\smallsetminus\\{{\mathsf{C}}\\},\alpha(\mathsf{I})=\emptyset\text{,
for all }\mathsf{I}\in\mathfrak{I}\text{ and }\\\
&&&&\mathrm{m}=\\{{q[\mathfrak{s}(x)]}\\}\text{, for some
}q\in\mathit{states}_{\beta}({\mathsf{C}})\\\\[5.69054pt]
(\alpha,\mathrm{m})&\models^{\mathfrak{s}}_{\Delta}&\mathsf{C}^{q}(x)&\iff&\alpha(\mathsf{C})=\\{{\mathfrak{s}(x)}\\},~{}\alpha(\mathsf{C}^{\prime})=\emptyset\text{,
for all }\\\
&&&&\mathsf{C}^{\prime}\in\mathfrak{C}\smallsetminus\\{{\mathsf{C}}\\},\alpha(\mathsf{I})=\emptyset\text{,
for all }\mathsf{I}\in\mathfrak{I}\\\ &&&&\text{ and
}\mathrm{m}=\\{{q[\mathfrak{s}(x)]}\\}\\\\[5.69054pt]
(\alpha,\mathrm{m})&\models^{\mathfrak{s}}_{\Delta}&\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I}_{k})})&\iff&\alpha(\mathsf{C})=\emptyset\text{,
for all
}\mathsf{C}\in\mathfrak{C},~{}\alpha(\mathsf{I})=\\{\langle\mathfrak{s}(x_{1}),\\\
&&&&\ldots,\mathfrak{s}(x_{\\#(\mathsf{I}_{k})})\rangle\\},~{}\alpha(\mathsf{I}^{\prime})=\emptyset\text{,
for all }\\\
&&&&\mathsf{I}^{\prime}\in\mathfrak{I}\smallsetminus\\{{\mathsf{I}}\\}\text{
and }\mathrm{m}=\emptyset\\\\[5.69054pt]
(\alpha,\mathrm{m})&\models^{\mathfrak{s}}_{\Delta}&\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})&\iff&(\alpha,\mathrm{m})\models^{\mathfrak{s}}_{\Delta}\phi[y_{1}/x_{1},\ldots,y_{\\#(\mathcal{A})}/x_{\\#(\mathcal{A})}],\\\
&&&&\text{for some rule
}\mathcal{A}(y_{1},\ldots,y_{\\#(\mathcal{A})})\leftarrow\phi\in\Delta\end{array}$
$\begin{array}[]{rclcl}(\alpha,\mathrm{m})&\models^{\mathfrak{s}}_{\Delta}&\phi_{1}*\phi_{2}&\iff&\text{there
exist configurations
}(\alpha_{1},\mathrm{m}_{1}),(\alpha_{2},\mathrm{m}_{2})\\\ &&&&\text{such
that
}(\alpha,\mathrm{m})=(\alpha_{1},\mathrm{m}_{1})\bullet(\alpha_{2},\mathrm{m}_{2})\text{
and }\\\
&&&&(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}}_{\Delta}\phi_{i}\text{,
for }i=1,2.\\\\[5.69054pt]
(\alpha,\mathrm{m})&\models^{\mathfrak{s}}_{\Delta}&\exists
x~{}.~{}\phi_{1}&\iff&(\alpha,\mathrm{m})\models^{\mathfrak{s}^{\prime}}_{\Delta}\phi_{1}\text{,
for some store }\mathfrak{s}^{\prime}\text{ that agrees}\\\ &&&&\text{with
}\mathfrak{s}\text{ on all variables from
}\mathbb{X}^{1}\smallsetminus\\{{x}\\}\end{array}$

To simplify the notation, we consider that $\Delta$ is fixed and omit the
$\Delta$ subscript in the following. If the formula $\phi$ is a sentence, we
can omit the store $\mathfrak{s}$ from the satisfaction relation
$\models^{\mathfrak{s}}$ and write $(\alpha,\mathrm{m})\models\phi$. In this
case, $(\alpha,\mathrm{m})$ is said to be a _model_ of $\phi$ and denote by
${{\bf[\\![}\phi{\bf]\\!]}}$ the set of models of the sentence $\phi$. For two
sentences $\phi$ and $\psi$, we say that $\phi$ _entails_ $\psi$ if
${{\bf[\\![}\phi{\bf]\\!]}}\subseteq{{\bf[\\![}\psi{\bf]\\!]}}$, written
$\phi\models\psi$.

######  Example 5 (contd. from §1.1)

The SID consisting of the rules 1-5 (§1.1) defines systems with token-ring
architectures. On the other hand, the rules below define chains of
$\mathsf{S}$ and $\mathsf{T}$ components, with at least $n,t\in\mathbb{N}$
components in state $\mathfrak{n}$ and $\mathfrak{t}$, respectively:

$\begin{array}[]{rclcrcl}\mathit{Chain}_{{0},{0}}(x,x)&\leftarrow&\mathsf{S}(x)\\\
\mathit{Chain}_{{0},{1}}(x,x)&\leftarrow&\mathsf{S}^{\mathfrak{t}}(x)&&\mathit{Chain}_{{1},{0}}(x,x)&\leftarrow&\mathsf{S}^{\mathfrak{n}}(x)\end{array}$

$\begin{array}[]{rcl}\mathit{Chain}_{{n},{t}}(x,z)&\leftarrow&\exists
y.~{}\mathsf{S}^{\mathfrak{t}}(x)\ast\mathsf{T}(x,y)\ast\mathit{Chain}_{{n},{t\dot{-}1}}(y,z)\\\
\mathit{Chain}_{{n},{t}}(x,z)&\leftarrow&\exists
y.~{}\mathsf{S}^{\mathfrak{n}}(x)\ast\mathsf{T}(x,y)\ast\mathit{Chain}_{{n\dot{-}1},{t}}(y,z)\end{array}$

where
$k\dot{-}1\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\max(k-1,0)$,
$k\in\mathbb{N}$. $\blacksquare$

Below we show that CL sentences define indeed system configurations.

###### Proposition 2

Given a sentence $\phi$ of CL, if
$(\alpha,\mathrm{m})\in{{\bf[\\![}\phi{\bf]\\!]}}$ then $\mathrm{m}$ is a
precise marking of the Petri net $\mathsf{N}({\Sigma,\alpha,\beta})$.

_Proof_ : We prove a more general statement: for each formula $\phi$ and each
store $\mathfrak{s}$, if $(\alpha,\mathrm{m})\models^{\mathfrak{s}}\phi$ then
$\mathrm{m}$ is a precise marking of $\mathsf{N}({\Sigma,\alpha,\beta})$. The
proof is by induction on the definition of the $\models^{\mathfrak{s}}$
relation, by distinguishing the following cases:

  * •

$\phi\in\\{{\mathsf{emp},\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})}\\}$:
$\mathrm{m}=\emptyset$ and $\alpha(\mathsf{C})=\emptyset$, for all
$\mathsf{C}\in\mathfrak{C}$, thus $\mathrm{m}$ is trivially precise for
$\mathsf{N}({\Sigma,\alpha,\beta})$.

  * •

$\phi=\mathsf{C}(x)$: $\mathrm{m}=\\{{q[\mathfrak{s}(x)]}\\}$, for some
$q\in\mathit{states}_{\beta}({\mathsf{C}})$,
$\alpha(\mathsf{C})=\\{{\mathfrak{s}(x)}\\}$ and
$\alpha(\mathsf{C}^{\prime})=\emptyset$, for all
$\mathsf{C}^{\prime}\in\mathfrak{C}\smallsetminus\\{{\mathsf{C}}\\}$, hence
$\mathrm{m}$ is precise for $\mathsf{N}({\Sigma,\alpha,\beta})$.

  * •

$\phi=\mathsf{C}^{q}(x)$: $\mathrm{m}=\\{{q[\mathfrak{s}(x)]}\\}$,
$\alpha(\mathsf{C})=\\{{\mathfrak{s}(x)}\\}$ and
$\alpha(\mathsf{C}^{\prime})=\emptyset$, for all
$\mathsf{C}^{\prime}\in\mathfrak{C}\smallsetminus\\{{\mathsf{C}}\\}$, hence
$\mathrm{m}$ is precise for $\mathsf{N}({\Sigma,\alpha,\beta})$.

  * •

$\phi=\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})$:
$(\alpha,\mathrm{m})\models^{\mathfrak{s}}\psi[y_{1}/x_{1},\ldots,y_{\\#(\mathcal{A})}/x_{\\#(\mathcal{A})}]$,
for some rule
$\mathcal{A}(y_{1},\ldots,y_{\\#(\mathcal{A})})\leftarrow\psi\in\Delta$ and
apply the inductive hypothesis.

  * •

$\phi=\phi_{1}*\phi_{2}$: if
$(\alpha,\mathrm{m})\models^{\mathfrak{s}}\phi_{1}*\phi_{2}$ then there exists
configurations $(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}}\phi_{i}$,
for $i=1,2$, such that $\alpha_{1}$ and $\alpha_{2}$ are disjoint,
$\alpha=\alpha_{1}\cup\alpha_{2}$ and
$\mathrm{m}=\mathrm{m}_{1}\cup\mathrm{m}_{2}$. By the inductive hypothesis,
$\mathrm{m}_{i}$ is a precise marking of
$\mathsf{N}({\Sigma,\alpha_{i},\beta})$, for $i=1,2$. Let
$\mathsf{C}\in\mathfrak{C}$ be a component type and let
$u\in\alpha(\mathsf{C})$ be an index. Then either $u\in\alpha_{1}(\mathsf{C})$
or $u\in\alpha_{2}(\mathsf{C})$, but not both. Let us consider the case
$u\in\alpha_{1}(\mathsf{C})\smallsetminus\alpha_{2}(\mathsf{C})$, the other
case being symmetric. Then $\mathrm{m}\cap\\{{q[u]\mid
q\in\mathit{states}({\mathsf{C}})}\\}=\mathrm{m}_{1}\cap\\{{q[u]\mid
q\in\mathit{states}({\mathsf{C}})}\\}$, hence
$|\\!|{\mathrm{m}\cap\\{{q[u]\mid
q\in\mathit{states}({\mathsf{C}})}\\}}|\\!|=|\\!|{\mathrm{m}_{1}\cap\\{{q[u]\mid
q\in\mathit{states}({\mathsf{C}})}\\}}|\\!|=1$. Since the choices of
$\mathsf{C}$ and $u$ were arbitrary, we obtain that $\mathrm{m}$ is precise.

  * •

$\phi=\exists x~{}.~{}\phi_{1}$: by an application of the inductive
hypothesis.

##  4 Decision Problems

A decision problem is a class of yes/no queries of the same kind, that differ
only in their input. All decision problems considered in this paper are
parameterized by a given signature
$\Sigma=(\mathfrak{C},\mathfrak{I},\mathfrak{P})$. The queries take as input a
sentence $\phi$, a SID $\Delta$, a behavior map
$\beta:\mathfrak{C}\rightarrow\mathbb{B}$ and a tuple of states
$\langle{q_{1},\ldots,q_{n}}\rangle\in\mathcal{Q}_{\beta}^{n}$ for some
$n\in\mathbb{N}$. They are defined as follows:

  * •

$\mathit{deadlock}(\phi,\Delta,\beta)$: is there a configuration
$(\alpha,\mathrm{m})$, such that $(\alpha,\mathrm{m})\models_{\Delta}\phi$ and
$\mathit{Reach}({\mathsf{N}({\Sigma,\alpha,\beta}),\mathrm{m}})\cap\mathit{Dead}({\mathsf{N}({\Sigma,\alpha,\beta})})\neq\emptyset$
?

  * •

$\mathit{reach}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)$: are
there configurations $(\alpha,\mathrm{m})$, $(\alpha,\mathrm{m}^{\prime})$ and
indices $u_{1},\ldots,u_{k}\in\mathbb{U}$, such that
$(\alpha,\mathrm{m})\models_{\Delta}\phi$,
$\mathrm{m}^{\prime}\in\mathit{Reach}({\mathsf{N}({\Sigma,\alpha,\beta}),\mathrm{m}})$
and $\\{{q_{i}[u_{i}]~{}|~{}i\in[{1},{k}]}\\}\subseteq\mathrm{m}^{\prime}$,
with $q_{1}[u_{1}],\ldots,q_{k}[u_{k}]$ pairwise distinct?

The above queries occur typically as correctness conditions in system
verification. For instance, proving that, in every system described by a
formula $\phi$, no freeze configuration is reachable means showing that
$\mathit{deadlock}(\phi,\Delta,\beta)$ does not hold. Similarly, proving that
each system described by $\phi$ stays clear of a set of error configurations
e.g., at most one component is in some critical state $q_{crit}$ at any time
amounts to proving that
$\mathit{reach}(\phi,\langle{q_{crit},q_{crit}}\rangle,\Delta,\beta)$ does not
hold.

###  4.1 Undecidability Results for Linear Systems

We show that the problems defined by the sets of queries above, taken over all
inputs, but parameterized by a fixed given signature, are undecidable. In
fact, we shall prove stronger results, in which the input formulæ define sets
of configurations with _linear_ architectures.

###### Definition 5

Given a signature $\Sigma=(\\{{\mathsf{C}}\\},\mathfrak{I},\mathfrak{P})$, a
sentence $\phi$, interpreted over a SID $\Delta$, is _linear_ if and only if
$\phi\models_{\Delta\cup\Lambda}\phi_{\mathcal{L}}$, where $\Lambda$ consists
of the rules:

$\begin{array}[]{rcl}\mathcal{L}(x,x)&\leftarrow&\hskip
20.77051pt\mathsf{C}(x)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}^{(1)}}\mathsf{I}(x)\\\
\mathcal{L}(x,y)&\leftarrow&\exists
z~{}.~{}\mathsf{C}(x)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}^{(1)}}\mathsf{I}(x)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}^{(2)}}\mathsf{I}(x,z)*\mathcal{L}(z,y)\end{array}$

where $\mathcal{L}$ is a binary predicate symbol and $\phi_{\mathcal{L}}$ is
the sentence $\exists x\exists y~{}.~{}\mathcal{L}(x,y)$.

For instance, the sentences $\exists x\exists y~{}.~{}\mathit{Chain}(x,y)$
(§1.1) and $\exists x\exists y~{}.~{}\mathit{Chain}_{{n},{t}}(x,y)$ for
$n,t\geq 0$ (Example 5) are linear, when taking
$\mathfrak{C}=\\{{\mathsf{S}}\\}$ and $\mathfrak{I}=\\{{\mathsf{T}}\\}$.

Below we show that undecidability occurs for classes of queries taking linear
sentences as input, over a fixed signature consisting of only one component
type and a fixed set of interaction types, which is not part of the input of a
query.

###### Theorem 1

The following problems are undecidable:

$\begin{array}[]{rcl}\mathit{LinearDeadlock}&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\\{{\mathit{deadlock}(\phi,\Delta,\beta)\mid\phi\models_{\Delta\cup\Lambda}\phi_{\mathcal{L}}}\\}\\\
\mathit{LinearReachability}&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\\{{\mathit{reach}(\phi,\langle{q_{1}}\rangle,\Delta,\beta)\mid\phi\models_{\Delta\cup\Lambda}\phi_{\mathcal{L}}}\\}\\\
\end{array}$

The idea of the proof is to build a component-based system with linear
architecture that simulates the execution of a Post-Turing machine. We present
the construction in §4.2 and complete the proof in §4.3.

###  4.2 Simulation of Post-Turing Machines by Linear Systems

A Post-Turing machine [10, 11] executes sequential deterministic programs $M$
of the form $1:~{}stmt_{1};~{}2:~{}stmt_{2};~{}\ldots;~{}m:~{}stmt_{m}$, where
each statement $stmt_{i}$ is one of following: $\mathsf{write~{}0}$,
$\mathsf{write~{}1}$, $\mathsf{go~{}right}$, $\mathsf{go~{}left}$,
$\mathsf{goto~{}step~{}\mathit{j}~{}if~{}read~{}0}$,
$\mathsf{goto~{}step~{}\mathit{j}~{}if~{}read~{}1}$, $\mathsf{stop}$, for some
$j\in[{1},{m}]$. The machine operates on an infinite tape of zeroes and ones.
Initially, the head is pointing at some position on the tape and the program
control is at the first statement. At any step, the current statement is
executed and the tape content, the head position and control are updated
according to that statement.

We simulate a Post-Turing machine by a component-based system with linear
architecture. Its signature
$\Sigma_{PT}=(\mathfrak{C}_{PT},\mathfrak{I}_{PT},\mathfrak{P}_{PT})$ is
presented in Fig. 4(a) and consists of one component type $\mathsf{C}_{PT}$
and ten interaction types $\mathfrak{I}_{PT}$, with associated ports as
presented in the figure. In particular, the signature does not depend on the
program executed by the machine.

$\mathit{out}\\_write\\_0$$\mathit{out}\\_write\\_1$$\mathit{out}\\_right$$\mathit{out}\\_right!$$\mathit{out}\\_left$$\mathit{out}\\_left!$$\mathit{out}\\_read$$\mathit{in}\\_read\\_0$$\mathit{in}\\_read\\_1$$\mathit{out}\\_err$$\mathit{in}\\_write\\_0$$\mathit{in}\\_write\\_1$$\mathit{in}\\_right$$\mathit{in}\\_right!$$\mathit{in}\\_left!$$\mathit{in}\\_read$$\mathit{out}\\_read\\_0$$\mathit{out}\\_read\\_1$$\mathit{in}\\_left$$\mathsf{C}_{PT}$$\mathit{out}\\_write\\_0$$\mathit{out}\\_write\\_1$$\mathit{out}\\_right$$\mathit{out}\\_right!$$\mathit{out}\\_left$$\mathit{out}\\_left!$$\mathit{out}\\_read$$\mathit{in}\\_read\\_0$$\mathit{in}\\_read\\_1$$\mathit{out}\\_err$$\mathit{in}\\_write\\_0$$\mathit{in}\\_write\\_1$$\mathit{in}\\_right$$\mathit{in}\\_right!$$\mathit{in}\\_left$$\mathit{in}\\_left!$$\mathit{in}\\_read$$\mathit{out}\\_read\\_0$$\mathit{out}\\_read\\_1$$\mathfrak{C}_{PT}$$\mathfrak{I}_{PT}$

(a)

$\gamma_{1},\bot$$\ldots$$\gamma_{k}$$\gamma_{n}$$\ldots$$\ldots$$\ldots$$\gamma_{k},\top$$\gamma_{n},\bot$tapectrltapetapesink$a$$a$$a^{\prime}$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$$a^{\prime}$$\gamma_{1}$$\mathit{out}\\_a$$\mathit{in}\\_a^{\prime}$$\mathit{out}\\_a^{\prime}$$\mathit{in}\\_a$$a$$a^{\prime}$$a$$a^{\prime}$$i:\mathit{stmt}_{i}$$i:\mathit{stmt}_{i}$

(b)

Figure 4: Undecidability of Deadlock and Reachability for Linear Component-
based Systems

The linear system that simulates a Post-Turing machine is depicted in Fig.
4(b). First of all, the machine program $M$ is encoded in the behavior
$\beta_{M}$ of the component type $\mathsf{C}_{PT}$. In particular, this
behavior includes three disjoint state machines, as described in Table 1,
labeled with the same set of ports. Second, in the linear system, each
component plays a different role depending on its position, i.e. it runs
according to one of the three state machines below:

  * •

the leftmost _ctrl_ component behaves according to the _control state machine_
derived from the program $M$: it issues the commands to be executed by the
tape components depending on the current statement, and proceeds further
according to the control flow of $M$. In case of _read_ commands, it goes to
an intermediate state, waiting to receive either _read_0_ or _read_1_ answers.
In case of _left!_ commands, it goes to an error state signaling the overflow
of the tape on the left side. The complete definition is given in Table 1
(top).

  * •

the middle _tape_ components behave according to the _tape state machine_ and
mimic the behavior of a single tape cell: the $k$-th component state records
the $k$-th symbol of the tape $\gamma_{k}$ and the presence ($\top$) or
absence ($\bot$) of the machine head at that cell. They react to commands
(received through $in$-ports) by changing their state and/or further issuing
commands to their neighbors (sent through $out$-ports). The complete
definition is given in Table 1 (middle).

  * •

the rightmost _sink_ component behaves according to the _sink state machine_
and detects the overflow of the tape on the right side and signals it as an
error. This happens when this component receives the _right!_ command. The
complete definition is given in Table 1 (bottom).

$\begin{array}[]{lcl}\lx@intercol\mbox{control state machine with states
}Q_{ctrl}^{M}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{i,(i,\\_)~{}|~{}i\in[{1},{m+1}]\\}\mbox{
represents the program }M\hfil\lx@intercol\\\ \hline\cr
i:~{}\mathsf{write~{}0}&&i\xrightarrow{{\scriptstyle\mathit{out}\\_write\\_0}}i\\!+\\!1\\\
i:~{}\mathsf{write~{}1}&&i\xrightarrow{{\scriptstyle\mathit{out}\\_write\\_1}}i\\!+\\!1\\\
i:~{}\mathsf{go~{}right}&&i\xrightarrow{{\scriptstyle\mathit{out}\\_right}}i\\!+\\!1\\\
i:~{}\mathsf{go~{}left}&&i\xrightarrow{{\scriptstyle\mathit{out}\\_left}}i\\!+\\!1,~{}i\xrightarrow{{\scriptstyle\mathit{out}\\_left!}}(i,\\_),~{}(i,\\_)\xrightarrow{{\scriptstyle\mathit{out}\\_err}}(i,\\_)\\\
i:~{}\mathsf{goto~{}step~{}\mathit{j}~{}if~{}read~{}0}&&i\xrightarrow{{\scriptstyle\mathit{out}\\_read}}(i,\\_),~{}(i,\\_)\xrightarrow{{\scriptstyle\mathit{in}\\_read\\_0}}j,~{}(i,\\_)\xrightarrow{{\scriptstyle\mathit{in}\\_read\\_1}}i\\!+\\!1\\\
i:~{}\mathsf{goto~{}step~{}\mathit{j}~{}if~{}read~{}1}&&i\xrightarrow{{\scriptstyle\mathit{out}\\_read}}(i,\\_),~{}(i,\\_)\xrightarrow{{\scriptstyle\mathit{in}\\_read\\_1}}j,~{}(i,\\_)\xrightarrow{{\scriptstyle\mathit{in}\\_read\\_0}}i\\!+\\!1\\\
i:~{}\mathsf{stop}&&/*nothing*/\\\ \hline\cr\end{array}$

$\begin{array}[]{lcl}\lx@intercol\mbox{tape state machine with states
}Q_{tape}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{(\gamma,\pi),(\gamma,\pi,a)~{}|~{}\gamma\in\\{0,1\\},~{}\pi\in\\{\bot,\top\\},~{}a\in\mathfrak{I}_{PT}\smallsetminus\\{\mathit{err}\\}\\}\hfil\lx@intercol\\\
\hline\cr(\gamma,\bot)\xrightarrow{{\scriptstyle\mathit{in}\\_a}}(\gamma,\bot,a)&&(\gamma,\bot,a)\xrightarrow{{\scriptstyle\mathit{out}\\_a}}(\gamma,\bot)\hskip
28.45274pt\forall a\not=\mathit{right!,left!,err}\\\
(\gamma,\bot)\xrightarrow{{\scriptstyle\mathit{in}\\_right!}}(\gamma,\top)&&(\gamma,\bot,\mathit{left})\xrightarrow{{\scriptstyle\mathit{out}\\_left!}}(\gamma,\top)\\\
(\gamma,\top)\xrightarrow{{\scriptstyle\mathit{in}\\_write\\_\gamma^{\prime}}}(\gamma^{\prime},\top)\\\
(\gamma,\top)\xrightarrow{{\scriptstyle\mathit{in}\\_read}}(\gamma,\top,\mathit{read})&&(\gamma,\top,\mathit{read})\xrightarrow{{\scriptstyle\mathit{out}\\_read\\_\gamma}}(\gamma,\top)\\\
(\gamma,\top)\xrightarrow{{\scriptstyle\mathit{in}\\_right}}(\gamma,\top,\mathit{right})&&(\gamma,\top,\mathit{right})\xrightarrow{{\scriptstyle\mathit{out}\\_right!}}(\gamma,\bot)\\\
(\gamma,\top)\xrightarrow{{\scriptstyle\mathit{in}\\_left!}}(\gamma,\bot)\\\
\hline\cr\end{array}$

$\begin{array}[]{lcl}\lx@intercol\mbox{sink state machine with states
}Q_{sink}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{\mathit{idle},\mathit{busy}\\}\hfil\lx@intercol\\\
\hline\cr\mathit{idle}\xrightarrow{{\scriptstyle\mathit{in}\\_right!}}\mathit{busy}&&\mathit{busy}\xrightarrow{{\scriptstyle\mathit{out}\\_err}}\mathit{busy}\\\
\hline\cr\end{array}$

Table 1: The behavior $\beta_{M}$ of $\mathsf{C}_{PT}$ for a Post-Turing
machine executing a program $M$

###  4.3 Proof of Theorem 1

Let $M$ be the program of a Post-Turing machine and let
$w=\gamma_{1}\gamma_{2}\ldots\gamma_{n}$ be a finite word in $\\{0,1\\}^{n}$,
assuming moreover wlog333$w$ can be augmented with extra zeroes on the right
that $n\geq 2$. Consider the signature $\Sigma_{PT}$ and the behavior
$\beta_{M}$ as defined in the previous section. Furthermore, consider the
following set $\Delta_{w}$ of rules, where
$\mathfrak{I}_{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathfrak{I}_{PT}^{(1)}$,
$\mathfrak{I}_{2}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathfrak{I}_{PT}^{(2)}$:

$\begin{array}[]{rcl}\mathit{Zeroes}(x,x)&\leftarrow&\hskip
20.77051pt\mathsf{C}_{PT}^{(0,\bot)}(z)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(x)\\\
\mathit{Zeroes}(x,y)&\leftarrow&\exists
z~{}.~{}\mathsf{C}_{PT}^{(0,\bot)}(x)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(x)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(x,z)*\mathit{Zeroes}(z,y)\end{array}$
$\begin{array}[]{rcl}\mathit{Word\\_w}(x,y)&\leftarrow&\exists
z_{2}~{}\ldots~{}\exists
z_{n-1}~{}.~{}\mathsf{C}_{PT}^{(\gamma_{1},\top)}(x)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(x)~{}*\\\ &&\hskip
11.38109pt\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(x,z_{2})*\mathsf{C}_{PT}^{(\gamma_{2},\bot)}(z_{2})*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(z_{2})~{}*\\\ &&\hskip
11.38109pt\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(z_{2},z_{3})*\mathsf{C}_{PT}^{(\gamma_{3},\bot)}(z_{3})*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(z_{3})~{}*\\\ &&\hskip
22.76219pt...\\\ &&\hskip
11.38109pt\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(z_{n-1},y)*\mathsf{C}_{PT}^{(\gamma_{n},\bot)}(y)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(y)\\\\[5.69054pt]
\mathit{Tape\\_w}(x,y)&\leftarrow&\exists z_{1}~{}\exists w_{1}~{}\exists
z_{2}~{}\exists w_{2}~{}.~{}\mathit{Zeroes}(x,z_{1})~{}*\\\ &&\hskip
11.38109pt\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(z_{1},w_{1})*\mathit{Word\\_w}(w_{1},w_{2})\\\
&&\hskip
11.38109pt\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(w_{2},z_{2})*\mathit{Zeroes}(z_{2},y)\\\\[5.69054pt]
\mathit{Init\\_w}(x,y)&\leftarrow&\exists z_{1}~{}\exists
z_{2}~{}.~{}\mathsf{C}_{PT}^{1}(x)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(x)\\\ &&\hskip
11.38109pt\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(x,z_{1})*\mathit{Tape\\_w}(z_{1},z_{2})~{}*\\\
&&\hskip
11.38109pt\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{2}}\mathsf{I}(z_{2},y)*\mathsf{C}_{PT}^{idle}(y)*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{\mathsf{I}\in\mathfrak{I}_{1}}\mathsf{I}(y)\end{array}$

and let
$\phi_{w}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\exists
x~{}\exists y~{}.~{}\mathit{Init}_{w}(x,y)$. Intuitively, $\phi_{w}$ is a
linear sentence which defines the valid (initial) configurations of the linear
system encoding the Post-Turing machine, where moreover $w$ is written on the
tape and the machine head is pointing at the beginning $w$. We prove the
following two assertions equivalent:

  1. 1.

the Post-Turing machine running $M$ terminates on input $w$

  2. 2.

the answer to $\mathit{deadlock}(\phi_{w},\Delta_{w},\beta_{M})$ is yes

“1 $\Rightarrow$ 2”: If the machine terminates then it terminates by visiting
finite portions of the tape to the left and to the right, with respect to the
initial placement of $w$ on the tape. Henceforth, if the linear component-
based system is started with the amount of tape cells needed on both sides, it
will run without errors (that is, neither left or right tape overflow) until
termination as well.

“2 $\Rightarrow$ 1”: First of all, if the linear system reaches a deadlock
from its initial configuration, it means that neither left or right overflow
occur (otherwise, the unary $\mathit{err}$ interactions are enabled and run in
an endless loop). Henceforth, the computation of the linear system involved
only the allocated tape components and followed the execution of the
statements in $M$. Moreover, by construction of the linear system, the
relationship between the control and the tape state machines ensures that no
blocking can occur between them: tape cells are continuously ready to receive
the commands from the control and to execute them, in order. Therefore, the
system stops in a deadlock only if no more commands are sent, i.e. when the
control machine reaches a $\mathsf{stop}$ statement and all tape components
are “idle”, that is, no other commands are pending for completion.

The termination problem of Post-Turing machines being undecidable [11], it
implies that the $\mathit{LinearDeadlock}$ problem is also undecidable.
Moreover, we can use a similar argument to show that the
$\mathit{LinearReachability}$ problem is undecidable as well. Actually, we can
restrict without loss of generality to programs $M$ containing a unique
$\mathsf{stop}$ statement moreover occurring as the last statement $m$ in $M$.
Then, for such programs we can prove the equivalence of the previous
assertions to the following one:

  1. 3.

the answer to
$\mathit{reach}(\phi_{w},\langle{m}\rangle,\Delta_{w},\beta_{M})$ is yes

that is, the linear system reaches some configuration where a component is in
state $m$. In fact, by construction, the only component that could reach the
$m$ state is the leftmost control component, and therefore we can map back any
execution of the linear component-based system reaching $m$ in the control
component, to a terminating execution of the Post-Turing machine.

##  5 Translating CL Specifications into Rewriting Trees

The inductive interpretation of predicate symbols in the CL logic, by means of
a finite set of definitions, supports the idea of designing systems
hierarchically (top-down). For instance, in §1.1, we specify a ring system
first by a chain of components, with an interaction between the $\mathit{out}$
port of the last to the $\mathit{in}$ port of the first component (rule 1).
Then a chain consists of one component and an interaction between the
$\mathit{out}$ port of that component and the $\mathit{in}$ port of the first
component of a separate chain (rule 2), or of two components (rule 3).
Intuitively, one can view these stages of the definition as rewriting steps,
in which a predicate atom is replaced by one of the rules defining it. In this
section, we formalize this idea by introducing rewriting trees, i.e. trees
labeled with rules, that define a partial order in which the rules are
applied.

Moreover, the verification method described in §6 uses rewriting trees as
backbones for the encoding of sets of configurations in MSO interpreted over
trees [12]. In particular, the component indices from the set $\mathbb{U}$ are
going to be interpreted as nodes of rewriting trees. As will be shown below,
this interpretation of logical variables loses no generality, because
component indices can only be compared for equality; their particular nature
is of no importance from the point of view of the verification problems
considered. Furthermore, the interpretation of component indices as tree nodes
enables the use of a decidable fragment of MSO, to encode verification
conditions.

The mapping of variables to the nodes of a rewriting tree is uniquely defined
by the occurrences of the component atoms in the tree. More precisely, because
all atomic propositions that occur in the rewriting tree are joined by
separating conjunctions, the variables of all component atoms $\mathsf{C}(x)$
with the same component type $\mathsf{C}$ must be interpreted as different
indices, or else the formula corresponding to the tree would not be
satisfiable. Hence, a rewriting tree uniquely defines an architecture $\alpha$
over a given signature $\Sigma$ and, implicitly, a Petri net
$\mathsf{N}({\Sigma,\alpha,\beta})$, for a given behavior map $\beta$ (Def.
1).

###  5.1 Rewriting Trees

Trees play an important role in the subsequent developments, hence we
introduce a few formal definitions, for self-containment reasons. Let
$\kappa\geq 1$ be an integer constant and let $[{1},{\kappa}]^{*}$ denote the
set of finite sequences of integers between $1$ and $\kappa$, called _nodes_
in the following. We denote the concatenation of nodes
$w,u\in[{1},{\kappa}]^{*}$ as $w\cdot u$ or simply $wu$, when no confusion
arises. A set of nodes $T\subseteq[{1},{\kappa}]^{*}$ is said to be:

  1. 1.

_prefix-closed_ if $wi\in T$, for some $i\in[{1},{\kappa}]$, only if $w\in T$,
and

  2. 2.

_complete_ if $wi\in T$, for some $i\in[{1},{\kappa}]$, only if $wj\in T$, for
all $j\in[{1},{i-1}]$.

A $\kappa$-ary tree $\mathcal{T}$ is a function mapping a complete prefix-
closed set of nodes $\mathrm{nodes}({\mathcal{T}})$ into a finite set of
labels. The _root_ of $\mathcal{T}$ is the empty sequence $\epsilon$, the
children of a node $w\in\mathrm{nodes}({\mathcal{T}})$ are
$\mathrm{childs}_{\scriptscriptstyle{\mathcal{T}}}({w})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{wi\in\mathrm{nodes}({\mathcal{T}})\mid
i\in[{1},{\kappa}]}\\}$ and the parent of a node
$wi\in\mathrm{nodes}({\mathcal{T}})$, where $i\in[{1},{\kappa}]$, is $w$. The
_leaves_ of $\mathcal{T}$ are
$\mathrm{leaves}({\mathcal{T}})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{w\in\mathrm{nodes}({\mathcal{T}})\mid
w\cdot 1\not\in\mathrm{nodes}({\mathcal{T}})}\\}$. The _subtree_ of
$\mathcal{T}$ rooted at $w$ is defined by
$\mathrm{nodes}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{w}}})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{w^{\prime}\mid
ww^{\prime}\in\mathrm{nodes}({\mathcal{T}})\\}$ and
${\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{w}}(w^{\prime})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathcal{T}(ww^{\prime})$,
for all
$w^{\prime}\in\mathrm{nodes}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{w}}})$.
A _prefix_ of a tree $\mathcal{T}$ is the restriction of $\mathcal{T}$ to a
complete prefix-closed subset of $\mathrm{nodes}({\mathcal{T}})$. We say that
$\mathcal{T}$ is finite if $\mathrm{nodes}({\mathcal{T}})$ is finite.

Let $\Delta$ be a fixed SID in the rest of this section. For an arbitrary CL
formula $\phi$, we denote by $\\#_{\mathsf{pred}}({\phi})$ the number of
occurrences of predicate atoms and by $\mathsf{pred}_{i}({\phi})$ the $i$-th
predicate atom from $\phi$, in some predefined total ordering of the symbols
in the syntax tree of $\phi$. A formula $\phi$ is said to be _predicate-free_
if $\\#_{\mathsf{pred}}({\phi})=0$. Without loss of generality, we assume from
now on that $\\#_{\mathsf{pred}}({\phi})\leq\kappa$, for each CL formula
$\phi$ considered in the following. We shall also simplify our technical life
by considering the following assumption:

###### Assumption 1

For each sentence $\phi$, there exists a rule
$\mathcal{A}_{\phi}()\leftarrow\phi$ in $\Delta$, where $\mathcal{A}_{\phi}$
is a predicate symbol of zero arity, not occurring in $\phi$ or elsewhere in
$\Delta$.

This assumption loses no generality because each query in a decision problem
(§4) considers finitely many sentences, for which finitely many rules of the
above form are added to $\Delta$.

###### Definition 6

Given a CL formula $\phi$, a _rewriting tree for $\phi$_ is a tree
$\mathcal{T}$ with labels from $\Delta$, such that
$\mathcal{T}(\epsilon)=\left(\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi\right)$,
for some predicate symbol $\mathcal{A}$ and, for each
$w\in\mathrm{nodes}({\mathcal{T}})$, such that
$\mathcal{T}(w)=\left(\mathcal{A}_{0}(x_{1},\ldots,x_{\\#(\mathcal{A}_{0})})\leftarrow\psi_{0}\right)$,
the following hold:

  1. 1.

for all $i\in[{1},{\\#_{\mathsf{pred}}({\psi_{0}})}]$, if
$\mathsf{pred}_{i}({\psi_{0}})=\mathcal{A}_{i}(y^{i}_{1},\ldots,y^{i}_{\\#(\mathcal{A}_{i})})$,
then $wi\in\mathrm{nodes}({\mathcal{T}})$ and
$\mathcal{T}(wi)=\left(\mathcal{A}_{i}(x_{1},\ldots,x_{\\#(\mathcal{A}_{i})})\leftarrow\psi_{i}\right)$
is a rule from $\Delta$,

  2. 2.

$wi\not\in\mathrm{nodes}({\mathcal{T}})$, for all
$i>\\#_{\mathsf{pred}}({\psi_{i}})$.

We denote by $\mathbb{T}({\phi}){}$ the set of rewriting trees for $\phi$.

By slight abuse of notation, we write
$\phi[\psi_{1}/\varphi_{1}\ldots\psi_{n}/\varphi_{n}]$ for the result of
replacing each subformula $\psi_{i}$ of $\phi$ by the formula $\varphi_{i}$,
for all $i\in[{1},{n}]$. We associate each rewriting tree
$\mathcal{T}\in\mathbb{T}({\phi})$ a _characteristic formula_
$\mathfrak{F}({\mathcal{T}})$, defined inductively on the structure of
$\mathcal{T}$, as follows:

$\mathfrak{F}({\mathcal{T}})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\left\\{\begin{array}[]{l}\phi\text{,
if }\mathrm{nodes}({\mathcal{T}})=\\{{\epsilon}\\}\\\\[5.69054pt]
\phi\left[\mathcal{A}_{1}(\mathbf{y}_{1})/\mathfrak{F}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{1}}})[\mathbf{x}_{1}/\mathbf{y}_{1}]~{}\ldots~{}\mathcal{A}_{n}(\mathbf{y}_{n})/\mathfrak{F}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{n}}})[\mathbf{x}_{n}/\mathbf{y}_{n}]\right],\\\
\text{ if }n=\\#_{\mathsf{pred}}({\phi})\geq 1\text{ and
}\mathsf{pred}_{i}({\phi})=\mathcal{A}_{i}(\mathbf{y}_{i}),\text{ for all
}i\in[{1},{n}]\end{array}\right.$

Intuitively, the characteristic formula of a rewriting tree is the predicate-
free formula obtained by replacing each predicate atom occurring in a node of
the tree by the characteristic formula of its corresponding subtree,
recursively. In the process of building a characteristic formula, the free
variables of the characteristic formulæ of the subtrees are substituted with
the parameters of their corresponding predicate atoms.

###### Example 6

Let
$\Sigma=(\\{{\mathsf{N},\mathsf{L}}\\},\\{{\mathsf{R},\mathsf{I}}\\},\mathfrak{P})$
be a signature, where
$\mathfrak{P}({\mathsf{N}})=\\{{\mathit{req},\mathit{reply}}\\}$,
$\mathfrak{P}({\mathsf{L}})=\\{{\mathit{reply},\mathit{in},\mathit{out}}\\}$,
$\mathfrak{P}({\mathsf{R}})=\langle{\mathit{req},\mathit{reply},\mathit{reply}}\rangle$
and $\mathfrak{P}({\mathsf{I}})=\langle{\mathit{out},\mathit{in}}\rangle$.
Consider a behavior map $\beta$, such that
$\mathit{states}_{\beta}({\mathsf{N}})=\\{{q_{0},q_{1}}\\}$ and
$\mathit{states}_{\beta}({\mathsf{L}})=\\{{s_{0},s_{1},s_{2}}\\}$. The SID
below defines tree-shaped architectures, whose leaves are connected in a token
ring:

$\displaystyle\mathit{Root}()$ $\displaystyle\leftarrow\exists r\exists
n_{1}\exists\ell_{1}\exists r_{1}\exists n_{2}\exists\ell_{2}\exists
r_{2}~{}.~{}\mathsf{N}^{q_{0}}(r)*\mathsf{R}(r,n_{1},n_{2})*\mathsf{I}(r_{1},\ell_{2})*\mathsf{I}(r_{2},\ell_{1})$
$\displaystyle\hskip
110.96556pt*~{}\mathit{Node}(n_{1},\ell_{1},r_{1})*\mathit{Node}(n_{2},\ell_{2},r_{2})$
(7) $\displaystyle\mathit{Node}(n,\ell,r)$ $\displaystyle\leftarrow\exists
n_{1}\exists r_{1}\exists
n_{2}\exists\ell_{2}~{}.~{}\mathsf{N}^{q_{0}}(n)*\mathsf{R}(n,n_{1},n_{2})*\mathsf{I}(r_{1},\ell_{2})$
$\displaystyle\hskip
110.96556pt*~{}\mathit{Node}(n_{1},\ell,r_{1})*\mathit{Node}(n_{2},\ell_{2},r)$
(8) $\displaystyle\mathit{Node}(n,\ell,r)$
$\displaystyle\leftarrow\mathsf{N}^{q_{0}}(n)*\mathsf{R}(n,\ell,r)*\mathit{Leaf}(\ell)*\mathsf{I}(\ell,r)*\mathit{Leaf}(r)$
(9) $\displaystyle\mathit{Leaf}(x)$
$\displaystyle\leftarrow\mathsf{L}^{s_{0}}(x)$ (10)

$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$$\mathsf{N}(r^{\epsilon})$(b)$\mathsf{N}(n^{2}_{1})$$\mathit{Node}(n^{\epsilon}_{2},l^{\epsilon}_{2},r^{\epsilon}_{2})$$\mathit{Node}(n^{1}_{2},l^{1}_{2},r^{\epsilon}_{1})$$\mathit{Node}(n^{1}_{1},l^{\epsilon}_{1},r^{1}_{1})$$\mathit{Node}(n^{\epsilon}_{1},l^{\epsilon}_{1},r^{\epsilon}_{1})$$\mathit{Root}()$$\mathit{out}$$\mathit{out}$$\mathit{out}$$\mathit{out}$$\mathit{out}$$\mathit{out}$$\mathit{out}$$\mathit{req}$$\mathit{reply}$$\mathit{reply}$$\mathit{req}$$\mathit{req}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathit{req}$$\mathit{req}$$\mathit{req}$$\mathit{req}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathit{reply}$$\mathsf{L}(r^{1}_{1})$$\mathsf{L}(l^{1}_{2})$$\mathsf{L}(r^{\epsilon}_{1})$$\mathsf{L}(l^{\epsilon}_{2})$$\mathsf{L}(r^{2}_{1})$$\mathsf{L}(l^{2}_{2})$$\mathsf{L}(r^{\epsilon}_{2})$$\mathsf{N}(n^{\epsilon}_{1})$$\mathsf{N}(n^{\epsilon}_{2})$$\mathsf{N}(n^{1}_{1})$$\mathit{out}$$\mathit{in}$$\mathit{in}$$\mathit{in}$$\mathit{in}$$\mathit{in}$$\mathit{in}$$\mathit{in}$$\mathsf{L}(l^{\epsilon}_{1})$$\mathit{in}$$\mathit{Node}(n^{2}_{2},l^{2}_{2},r^{\epsilon}_{2})$$\mathsf{N}(n^{2}_{2})$$\mathit{Node}(n^{2}_{1},l^{\epsilon}_{2},r^{2}_{1})$$\mathsf{N}(n^{1}_{2})$$\mathit{Node}(n,\ell,r)\leftarrow\exists
n_{1}\exists r_{1}\exists
n_{2}\exists\ell_{2}~{}.~{}\mathsf{N}^{q_{0}}(n)*\mathsf{R}(n,n_{1},n_{2})*\mathsf{I}(r_{1},\ell_{2})$$\mathit{Node}(n,\ell,r)\leftarrow\exists
n_{1}\exists r_{1}\exists
n_{2}\exists\ell_{2}~{}.~{}\mathsf{N}^{q_{0}}(n)*\mathsf{R}(n,n_{1},n_{2})*\mathsf{I}(r_{1},\ell_{2})$$\mathit{Root}()\leftarrow\exists
r\exists n_{1}\exists\ell_{1}\exists r_{1}\exists n_{2}\exists\ell_{2}\exists
r_{2}~{}.~{}\mathsf{N}^{q_{0}}(r)*\mathsf{R}(r,n_{1},n_{2})*\mathsf{I}(r_{1},\ell_{2})*\mathsf{I}(r_{2},\ell_{1})$$\mathit{Node}(n_{1},\ell_{1},r_{1})*\mathit{Node}(n_{2},\ell_{2},r_{2})$$\mathit{Node}(n_{1},\ell,r_{1})*\mathit{Node}(n_{2},\ell_{2},r)$$\mathit{Node}(n_{1},\ell,r_{1})*\mathit{Node}(n_{2},\ell_{2},r)$(a)$\mathit{Node}(n,\ell,r)\leftarrow\mathsf{N}(n)*\mathsf{R}(n,\ell,r)$$\mathit{Node}(n,\ell,r)\leftarrow\mathsf{N}^{q_{0}}(n)*\mathsf{R}(n,\ell,r)$$\mathit{Node}(n,\ell,r)\leftarrow\mathsf{N}(n)*\mathsf{R}(n,\ell,r)$$*\mathit{Leaf}(\ell)*\mathsf{I}(\ell,r)*\mathit{Leaf}(r)$$*\mathit{Leaf}(\ell)*\mathsf{I}(\ell,r)*\mathit{Leaf}(r)$$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$$*\mathit{Leaf}(\ell)*\mathsf{I}(\ell,r)*\mathit{Leaf}(r)$$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$$\mathit{Node}(n,\ell,r)\leftarrow\mathsf{N}^{q_{0}}(n)*\mathsf{R}(n,\ell,r)$$*\mathit{Leaf}(\ell)*\mathsf{I}(\ell,r)*\mathit{Leaf}(r)$$\mathit{Leaf}(x)\leftarrow\mathsf{L}^{s_{0}}(x)$

Figure 5: Trees with Leaves Linked in a Token Ring

Fig. 5(a) shows an unfolding tree for $\phi=\exists r\exists
n_{1}\exists\ell_{1}\exists r_{1}\exists n_{2}\exists\ell_{2}\exists
r_{2}~{}.~{}\mathsf{N}^{q_{0}}(r)*\mathsf{R}(r,n_{1},n_{2})*\mathsf{I}(r_{1},\ell_{2})*\mathsf{I}(r_{2},\ell_{1})*\mathit{Node}(n_{1},\ell_{1},r_{1})*\mathit{Node}(n_{2},\ell_{2},r_{2})$,
with $\mathcal{A}_{\phi}=\mathit{Root}$, and Fig. 5(b) shows a model of the
characteristic formula of this unfolding tree. To avoid name clashes, we
annotate existentially quantified variables in the characteristic formula with
the node of the unfolding tree where they are introduced, for instance
$r^{\epsilon},n_{1}^{\epsilon}$ and $n_{2}^{\epsilon}$ are introduced at the
root, whereas $n_{1}^{1},n_{2}^{1},\ell_{2}^{1},r_{1}^{1}$
($n_{1}^{2},n_{2}^{2},\ell_{2}^{2},r_{1}^{2}$) occur first at the left (right)
child of the root. $\blacksquare$

The following result shows that each model of a sentence is the model of the
characteristic formula of some rewriting tree for that sentence, that
represents the way in which the model is “produced” by unfolding the rules in
$\Delta$. In general, such rewriting trees are not unique, as different
rewriting trees can have equivalent characteristic formulæ.

###### Lemma 1

For each CL sentence $\phi$, we have
${{\bf[\\![}\phi{\bf]\\!]}}=\bigcup_{\mathcal{T}\in\mathbb{T}({\phi}){}}{{\bf[\\![}\mathfrak{F}({\mathcal{T}}){}{\bf]\\!]}}$.

_Proof_ : We prove a slightly more general statement: for each formula $\phi$,
each rule $\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi$ from
$\Delta$, each configuration $(\alpha,\mathrm{m})$ and each store
$\mathfrak{s}$:

$\begin{array}[]{rcl}(\alpha,\mathrm{m})\models^{\mathfrak{s}}\phi&\iff&(\alpha,\mathrm{m})\models^{\mathfrak{s}}\mathfrak{F}({\mathcal{T}})\text{,
for some }\mathcal{T}\in\mathbb{T}({\phi})\text{, such}\\\ &&\text{that
}\mathcal{T}(\epsilon)=\left(\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi\right)\end{array}$

“$\Rightarrow$” By induction on the definition of the satisfaction relation
$\models$, considering the following cases:

  * •

$\phi\in\\{{\mathsf{emp},\mathsf{C}^{q}(x),\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})}\\}$:
we define $\mathcal{T}$ by
$\mathrm{nodes}({\mathcal{T}})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\epsilon}\\}$
and
$\mathcal{T}(\epsilon)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\left(\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi\right)$.
By Def. 6, we have $\mathcal{T}\in\mathbb{T}({\phi})$ and
$\mathfrak{F}({\mathcal{T}})=\phi$, thus
$(\alpha,\mathrm{m})\models^{\mathfrak{s}}\mathfrak{F}({\mathcal{T}})$.

  * •

$\phi=\exists y_{1}\ldots\exists
y_{n}~{}.~{}\phi_{0}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{k}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$,
where $\phi_{0}$ is quantifier- and predicate-free: since
$(\alpha,\mathrm{m})\models^{\mathfrak{s}}\exists y_{1}\ldots\exists
y_{n}~{}.~{}\phi_{0}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{k}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$,
there exists a store $\mathfrak{s}^{\prime}$ that agrees with $\mathfrak{s}$
over $\mathbb{X}^{1}\setminus\\{{y_{1},\ldots,y_{n}}\\}$ and configurations
$(\alpha_{i},\mathrm{m}_{i})$, such that
$(\alpha,\mathrm{m})=(\alpha_{0},\mathrm{m}_{0})\bullet\ldots\bullet(\alpha_{k},\mathrm{m}_{k})$,
$(\alpha_{0},\mathrm{m}_{0})\models^{\mathfrak{s}^{\prime}}\phi_{0}$ and
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$,
for all $i\in[{1},{k}]$. For each $i\in[{1},{k}]$, since
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$,
there exists
$\mathcal{A}_{i}(x_{1},\ldots,x_{\\#(\mathcal{A}_{i})})\leftarrow\psi_{i}$ in
$\Delta$, such that
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}}\psi_{i}[x_{1}/z^{i}_{1},\ldots,x_{\\#(\mathcal{A}_{i})}/z^{i}_{\\#(\mathcal{A}_{i})}]$,
by the definition of $\models$. Let
$\mathfrak{s}^{\prime}_{i}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathfrak{s}^{\prime}\circ[x_{1}/z^{i}_{1},\ldots,x_{\\#(\mathcal{A}_{i})}/z^{i}_{\\#(\mathcal{A}_{i})}]$
be a store. We have
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}_{i}}\psi_{i}$ and,
by the induction hypothesis, there exists a rewriting tree
$\mathcal{T}_{i}\in\mathbb{T}({\psi_{i}})$, such that
$\mathcal{T}_{i}(\epsilon)=\left(\mathcal{A}_{i}(x_{1},\ldots,x_{\\#(\mathcal{A}_{i})})\leftarrow\psi_{i}\right)$
and
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}_{i}}\mathfrak{F}({\mathcal{T}_{i}})$,
hence
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}}\mathfrak{F}({\mathcal{T}_{i}})[x_{1}/z^{i}_{1},\ldots,x_{\\#(\mathcal{A}_{i})}/z^{i}_{\\#(\mathcal{A}_{i})}]$.
We define the rewriting tree $\mathcal{T}$ as:

    * –

$\mathrm{nodes}({\mathcal{T}})=\\{{\epsilon}\\}\cup\bigcup_{i=1}^{k}i\cdot\mathrm{nodes}({\mathcal{T}_{i}})$,

    * –

$\mathcal{T}(\epsilon)=\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi$,

    * –

$\mathcal{T}(iw)=\mathcal{T}_{i}(w)$, for each $i\in[{1},{k}]$ and each
$w\in\mathrm{nodes}({\mathcal{T}_{i}})$.

We obtain $\mathfrak{F}({\mathcal{T}})=\exists y_{1}\ldots\exists
y_{n}~{}.~{}\phi_{0}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{k}\mathfrak{F}({\mathcal{T}_{i}})[x_{1}/z^{i}_{1},\ldots,x_{\\#(\mathcal{A}_{i})}/z^{i}_{\\#(\mathcal{A}_{i})}]$,
leading to
$(\alpha,\mathrm{m})\models^{\mathfrak{s}}\mathfrak{F}({\mathcal{T}})$.

”$\Leftarrow$” By induction on the structure of
$\mathcal{T}\in\mathbb{T}({\phi})$, such that
$\mathcal{T}(\epsilon)=\left(\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi\right)$,
by distinguishing the following cases:

  * •

$\mathrm{nodes}({\mathcal{T}})=\\{{\epsilon}\\}$: since
$\mathcal{T}(\epsilon)=\left(\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi\right)$,
we have $\mathfrak{F}({\mathcal{T}})=\phi$, hence
$(\alpha,\mathrm{m})\models^{\mathfrak{s}}\phi$.

  * •

$\mathrm{childs}_{\scriptscriptstyle{\mathcal{T}}}({\epsilon})=\\{{1,\ldots,k}\\}$,
for some $k\geq 1$: assume w.l.o.g. that $\phi=\exists y_{1}\ldots\exists
y_{n}~{}.~{}\phi_{0}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{k}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$,
where $\phi_{0}$ is a quantifier- and predicate-free formula. By the
definition of characteristic formulæ, we have
$\mathfrak{F}({\mathcal{T}})=\exists y_{1}\ldots\exists
y_{n}~{}.~{}\phi_{0}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{k}\mathfrak{F}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}})[x_{1}/z^{i}_{1},\ldots,x_{\\#(\mathcal{A}_{i})}/z^{i}_{\\#(\mathcal{A}_{i})}]$,
where
$\mathcal{T}(i)=\left(\mathcal{A}_{i}(x_{1},\ldots,x_{\\#(\mathcal{A}_{i})})\leftarrow\psi_{i}\right)$,
hence
${\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}\in\mathbb{T}({\psi_{i}})$.
Since $(\alpha,\mathrm{m})\models^{\mathfrak{s}}\mathfrak{F}({\mathcal{T}})$,
there exists a store $\mathfrak{s}^{\prime}$ that agrees with $\mathfrak{s}$
over $\mathbb{X}^{1}\setminus\\{{y_{1},\ldots,y_{n}}\\}$ and configurations
$(\alpha_{0},\mathrm{m}_{0}),\ldots,(\alpha_{k},\mathrm{m}_{k})$, such that
$(\alpha_{0},\mathrm{m}_{0})\models^{\mathfrak{s}^{\prime}}\phi_{0}$ and
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}}\mathfrak{F}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}})[x_{1}/z^{i}_{1},\ldots,x_{\\#(\mathcal{A}_{i})}/z^{i}_{\\#(\mathcal{A}_{i})}]$,
for all $i\in[{1},{m}]$. Consider an arbitrary index $i\in[{1},{m}]$ and let
$\mathfrak{s}^{\prime}_{i}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\mathfrak{s}^{\prime}\circ[x_{1}/z^{i}_{1},\ldots,x_{\\#(\mathcal{A}_{i})}/z^{i}_{\\#(\mathcal{A}_{i})}]$,
hence
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}_{i}}\mathfrak{F}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}})$.
By the inductive hypothesis, we have
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}_{i}}\psi_{i}$,
hence
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}_{i}}\mathcal{A}_{i}(x_{1},\ldots,x_{\\#(\mathcal{A}_{i})})$
and
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}^{\prime}}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$
follows. Because the above holds for all $i\in[{1},{k}]$, we conclude that
$(\alpha,\mathrm{m})\models^{\mathfrak{s}}\phi$.

###  5.2 Canonical Models

In the following, we shall equate the universe of indices $\mathbb{U}$ with
the set $[{1},{\kappa}]^{*}$ of tree nodes, i.e. finite sequences of integers
between $1$ and $\kappa$. This is without loss of generality, because both
sets are infinitely countable and the nature of indices plays no role in the
interpretation of CL formulæ. In this setting, we define the _canonical model_
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})$ of the characteristic
formula $\mathfrak{F}({\mathcal{T}})$ of a rewriting tree $\mathcal{T}$. In
order to simplify its definition, we proceed under the following assumption:

###### Assumption 2

Each rule of $\Delta$ is of one of the forms:

$\displaystyle\mathcal{A}(x_{1})$ $\displaystyle\leftarrow\phi\text{, such
that }\phi\neq\mathsf{emp}$ (I)
$\displaystyle\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})$
$\displaystyle\leftarrow\exists y_{1}\ldots\exists
y_{n}~{}.~{}\phi~{}*~{}\psi~{}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{p}\mathcal{A}_{i}(z_{1}^{i},\ldots,z_{\\#(\mathcal{A}_{i})}^{i})$
(II)

for some $n,m\geq 0$ and $p\geq 1$, where:

  * •

$\phi\in\\{{\mathsf{C}^{q}(x_{1})\mid\mathsf{C}\in\mathfrak{C},~{}q\in\mathit{states}_{\beta}({\mathsf{C}})}\\}\cup\\{{\mathsf{emp}}\\}$,

  * •

$\psi$ is a separating conjunction of interaction atoms,

  * •

$\bigcup_{i=1}^{p}\\{{z_{1}^{i},\ldots,z_{\\#(\mathcal{A}_{i})}^{i}}\\}=\left(\\{{x_{1},\ldots,x_{\\#(\mathcal{A})}}\\}\setminus\mathrm{fv}({\phi})\right)\cup\\{{y_{1},\ldots,y_{n}}\\}$,
and

  * •

$\\{{z_{1}^{i},\ldots,z_{\\#(\mathcal{A}_{i})}^{i}}\\}\cap\\{{z_{1}^{j},\ldots,z_{\\#(\mathcal{A}_{j})}^{j}}\\}=\emptyset$,
for all $1\leq i<j\leq p$.

The direct consequence of this assumption is that, each variable that occurs
in a characteristic formula of a rewriting tree, occurs in exactly one
component atom, in a rule that labels exactly one node from the rewriting
tree. This fact is proved below:

###### Lemma 2

Let $\phi$ be a CL formula and $\mathcal{T}\in\mathbb{T}({\phi})$ be a
rewriting tree for $\phi$. For each variable $x$, that occurs free or
existentially quantified in $\mathfrak{F}({\mathcal{T}})$, there exists
exactly one node $w\in\mathrm{nodes}({\mathcal{T}})$ and one component atom
$\mathsf{C}^{q}(x)$ in $\mathcal{T}(w)$.

_Proof_ : It is sufficient to prove the statement for the case where $x$
occurs in the label of the root of $\mathcal{T}$. If it is introduced at some
node $w\in\mathrm{nodes}({\mathcal{T}})\setminus\\{{\epsilon}\\}$ by an
existential quantifier, the same proof can be done taking
${\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{w}}$ instead of
$\mathcal{T}$. The proof goes by induction on the structure of $\mathcal{T}$.
For the base case $\mathrm{nodes}({\mathcal{T}})=\\{{\epsilon}\\}$, the only
possibility is that $\mathcal{T}(\epsilon)$ is a rule of the form (I) and the
proof is immediate. For the inductive step, let $\mathcal{T}(\epsilon)$ be the
following rule:

$\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\exists
y_{1}\ldots\exists
y_{n}~{}.~{}\phi~{}*~{}\psi~{}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{p}\mathcal{A}_{i}(v_{1}^{i},\ldots,v_{\\#(\mathcal{A}_{i})}^{i})$

If $\phi$ is of the form $\mathsf{C}^{q}(x_{1})$ and $x=x_{1}$, then
$\epsilon$ is the unique node such that $x$ occurs in a component atom. Else,
$x\in\\{{x_{1},\ldots,x_{\\#(\mathcal{A})}}\\}~{}\cup~{}\\{{y_{1},\ldots,y_{n}}\\}\setminus\mathrm{fv}({\phi})$,
thus $x\in\\{{v_{1}^{i},\ldots,v_{\\#(\mathcal{A}_{i})}^{i}}\\}$, for exactly
one $i\in[{1},{p}]$, by Assumption 2. In this case the inductive hypothesis
applies, thus $x$ occurs in exactly one component atom $\mathsf{C}^{q}(x)$ in
$\mathcal{T}(w)$, for exactly one
$w\in\mathrm{nodes}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}})$.

Note, however, that Assumption 2 is not without loss of generality. For
instance, architectures of the form $\exists z_{1}\ldots\exists
z_{k}~{}.~{}\mathsf{I}(x,z_{1})*\mathsf{C}^{q}(z_{1})*\mathsf{I}(z_{1},z_{2})*\ldots*\mathsf{C}^{q}(z_{k})*\mathsf{I}(z_{k},y)$,
having unconnected (loose) interactions, cannot be defined by SIDs that meet
the requirement of Assumption 2. On the positive side, all examples considered
in this paper can be written using only rules of this form, for instance, the
definition of the $\mathit{Chain}_{{n},{t}}$ predicates, for constant integers
$n,t\geq 0$ (Example 5) or the definition of the $\mathit{Root}$,
$\mathit{Node}$ and $\mathit{Leaf}$ predicates (Example 6).

The canonical model of a characteristic formula $\mathfrak{F}({\mathcal{T}})$
is obtained by instantiating each variable $x$ that occurs free or
existentially quantified in $\mathfrak{F}({\mathcal{T}})$ by the unique node
$w\in\mathrm{nodes}({\mathcal{T}})$, such that $x$ occurs in a single
component atom $\mathsf{C}^{q}(x)$ in $\mathcal{T}(w)$ (Lemma 2). Formally,
let $\phi=\exists y_{1}\ldots\exists
y_{n}~{}.~{}\psi~{}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{p}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$
be a formula, where $\psi$ is quantifier- and predicate-free, and define, for
each rewriting tree $\mathcal{T}\in\mathbb{T}({\phi})$, a store
$\mathfrak{s}^{\epsilon}_{\mathcal{T}}:\mathrm{fv}({\psi})\cup\bigcup_{i=1}^{p}\\{{z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})}}\\}\rightarrow\mathrm{nodes}({\mathcal{T}})$,
as follows:

$\mathfrak{s}^{\epsilon}_{\mathcal{T}}(x)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\left\\{\begin{array}[]{ll}\epsilon&\text{if
$x$ occurs in a component atom from $\psi$}\\\
i\cdot\mathfrak{s}^{\epsilon}_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}}(x_{j})&\text{if
$x=z^{i}_{j}$, for some $j\in[{1},{\\#(\mathcal{A}_{i})}]$, where}\\\
&\mathcal{T}(i)=\big{(}\mathcal{A}_{i}(x_{1},\ldots,x_{\\#(\mathcal{A}_{i})})\leftarrow\varphi_{i}\big{)}\text{,
for all $i\in[{1},{p}]$}\end{array}\right.$

Note that, because the rules of the SID meet the conditions of Assumption 2,
the two cases of the definition of $\mathfrak{s}^{\epsilon}_{\mathcal{T}}$
above are exclusive and, moreover, $\mathfrak{s}^{\epsilon}_{\mathcal{T}}(x)$
is defined for all free variables of the matrix
$\psi~{}*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{p}\mathcal{A}_{i}(z^{i}_{1},\ldots,z^{i}_{\\#(\mathcal{A}_{i})})$
of $\phi$. We extend the store $\mathfrak{s}^{\epsilon}_{\mathcal{T}}$ to a
store
$\mathfrak{s}_{\mathcal{T}}:\mathrm{fv}({\eta})\rightarrow\mathrm{nodes}({\mathcal{T}})$
mapping all variables (free or existentially quantified) that occur in the
characteristic formula $\mathfrak{F}({\mathcal{T}})=\exists z_{1}\ldots\exists
z_{k}~{}.~{}\eta$, where $\eta$ is a quantifier- and predicate-free formula:

$\mathfrak{s}_{\mathcal{T}}(x)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\left\\{\begin{array}[]{ll}\mathfrak{s}^{\epsilon}_{\mathcal{T}}(x)&\text{if
$x\in\mathrm{fv}({\mathfrak{F}({\mathcal{T}})})$}\\\
w\cdot\mathfrak{s}^{\epsilon}_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{w}}}(x)&\text{if
$x$ is existentially quantified at
$w\in\mathrm{nodes}({\mathcal{T}})$}\end{array}\right.$ (11)

In the above definition, we have assumed that all existentially quantified
variables have pairwise distinct names (this is w.l.o.g. as quantified
variables can be $\alpha$-renamed, if necessary). Note that
$\mathfrak{s}_{\mathcal{T}}$ is uniquely defined, for each given rewriting
tree $\mathcal{T}$ and induces a unique _canonical model_ , defined below:

###### Definition 7

The _canonical model_ of a rewriting tree $\mathcal{T}$ is the configuration
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})$, defined as follows:

  * •

$\alpha_{\mathcal{T}}(\mathsf{C})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\mathfrak{s}_{\mathcal{T}}(x)\mid\mathsf{C}^{q}(x)\text{
occurs in }\eta}\\}$,

  * •

$\alpha_{\mathcal{T}}(\mathsf{I})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\langle{\mathfrak{s}_{\mathcal{T}}(x_{1}),\ldots,\mathfrak{s}_{\mathcal{T}}(x_{\\#(\mathsf{I})})}\rangle\mid\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})\text{
occurs in }\eta}\\}$, and

  * •

$\mathrm{m}_{\mathcal{T}}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{q[\mathfrak{s}_{\mathcal{T}}(x)]\mid\mathsf{C}^{q}(x)\text{
occurs in }\eta}\\}$.

###### Lemma 3

Given a sentence $\phi$, for each rewriting tree
$\mathcal{T}\in\mathbb{T}({\phi})$, we have
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models\mathfrak{F}({\mathcal{T}})$.

_Proof_ : Let $\mathfrak{F}({\mathcal{T}})=\exists x_{1}\ldots\exists
x_{n}~{}.~{}\eta$. We prove a more general statement, namely if $\phi$ is a
formula, not necessarily a sentence, then
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models^{\mathfrak{s}_{\mathcal{T}}}\eta$.
The proof goes by induction on the structure of $\mathcal{T}$, distinguishing
the cases below:

  * •

$\mathrm{nodes}({\mathcal{T}})=\\{{\epsilon}\\}$ and
$\mathcal{T}(\epsilon)=\left(\mathcal{A}(x)\leftarrow\mathsf{C}^{q}(x)\right)$
is a rule of type (I): then
$\alpha_{\mathcal{T}}(\mathsf{C})=\\{{\mathfrak{s}_{\mathcal{T}}(x)}\\}=\\{{\epsilon}\\}$,
$\mathrm{m}_{\mathcal{T}}=\\{{q[\mathfrak{s}_{\mathcal{T}}(x)]}\\}=\\{{q[\epsilon]}\\}$,
$\alpha_{\mathcal{T}}(\mathsf{C}^{\prime})=\emptyset$, for all
$\mathsf{C}^{\prime}\in\mathfrak{C}\setminus\\{{\mathsf{C}}\\}$ and
$\alpha_{\mathcal{T}}(\mathsf{I})=\emptyset$, for all
$\mathsf{I}\in\mathfrak{I}$, thus
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models^{\mathfrak{s}_{\mathcal{T}}}\mathsf{C}^{q}(x)$.

  * •

$\mathrm{nodes}({\mathcal{T}})\neq\\{{\epsilon}\\}$ and
$\mathcal{T}(\epsilon)=\big{(}\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\exists
y_{1}\ldots\exists y_{n}~{}.~{}\phi*\psi~{}*$
$\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{p}\mathcal{A}_{i}(z_{1}^{i},\ldots,z_{\\#(\mathcal{A}_{i})}^{i})\big{)}$
is a rule of type (II). Let $\eta_{i}$ be the matrix of the characteristic
formula
$\mathfrak{F}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}})$, for
all $i\in[{1},{p}]$. By the definition of $\mathfrak{s}_{\mathcal{T}}$, we
have
$\mathfrak{s}_{\mathcal{T}}(x)=i\cdot\mathfrak{s}_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}}(x)$,
for all $x\in\eta_{i}$ and $i\in[{1},{p}]$. We define the structures
$(\alpha_{0},\mathrm{m}_{0}),(\alpha_{1},\mathrm{m}_{1}),\ldots,$
$(\alpha_{p},\mathrm{m}_{p})$ as follows:

    * –

$\alpha_{0}(\mathsf{C})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\mathfrak{s}_{\mathcal{T}}(x)}\\}=\\{{\epsilon}\\}$
and
$\mathrm{m}_{0}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{q[\mathfrak{s}_{\mathcal{T}}(x)]}\\}=\\{{q[\epsilon]}\\}$
if $\phi=\mathsf{C}^{q}(x_{1})$, else $\alpha_{0}(\mathsf{C})=\emptyset$ and
$\mathrm{m}_{0}=\emptyset$ and, moreover,
$\alpha_{0}(\mathsf{I})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{\langle{\mathfrak{s}_{\mathcal{T}}(x_{1}),\ldots,\mathfrak{s}_{\mathcal{T}}(x_{\\#(\mathsf{I})})}\rangle\mid\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})\text{
occurs in }\psi\\}$, thus we have
$(\alpha_{0},\mathrm{m}_{0})\models^{\mathfrak{s}_{\mathcal{T}}}\phi*\psi$.

    * –

$\alpha_{i}(\mathsf{C})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\mathfrak{s}_{\mathcal{T}}(x)\mid\mathsf{C}^{q}(x)\text{
occurs in }\eta_{i}}\\}$,
$\mathrm{m}_{i}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{\langle{\mathfrak{s}_{\mathcal{T}}(x_{1}),\ldots,\mathfrak{s}_{\mathcal{T}}(x_{\\#(\mathsf{I})})}\rangle\mid$
$\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})\text{ occurs in }\eta_{i}\\}$,
for each $i\in[{1},{p}]$. Since
$\mathfrak{s}_{\mathcal{T}}(x)=i\cdot\mathfrak{s}_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}}(x)$,
for all $x\in\eta_{i}$ and $i\in[{1},{p}]$, we have
$\alpha_{i}(\mathsf{C})=\\{{i\cdot u\mid
u\in\alpha_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}}(\mathsf{C})}\\}$,
for all $\mathsf{C}\in\mathfrak{C}$, $\mathrm{m}_{i}=\\{{q[i\cdot u]\mid
q[u]\in\mathrm{m}_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}}}\\}$
and $\alpha_{i}(\mathsf{I})=\\{\langle{i\cdot u_{1},\ldots,i\cdot
u_{\\#(\mathsf{I})}}\rangle\mid$
$\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in\alpha_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}}(\mathsf{I})\\}$,
for all $\mathsf{I}\in\mathfrak{I}$. By the inductive hypothesis, we have
$(\alpha_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}},\mathrm{m}_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}})\models^{\mathfrak{s}_{{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}}}\eta_{i}$,
thus
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}_{\mathcal{T}}}\eta_{i}$, for
all $i\in[{1},{p}]$.

Since the sets of indices of $\alpha_{0},\ldots,\alpha_{p}$ and
$\mathrm{m}_{0},\ldots,\mathrm{m}_{p}$ are pairwise disjoint, their
composition is defined and, moreover, we have
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})=(\alpha_{0},\mathrm{m}_{0})\bullet\ldots\bullet(\alpha_{p},\mathrm{m}_{p})$.
Consequently, we obtain
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models^{\mathfrak{s}_{\mathcal{T}}}\phi*\psi*\mathop{\scalebox{1.9}{\raisebox{-0.86108pt}{$\ast$}}}\hskip
1.0pt_{i=1}^{p}\mathcal{A}_{i}(z_{1}^{i},\ldots,z_{\\#(\mathcal{A}_{i})}^{i})$,
as required.

###### Example 7

Since $\mathcal{T}$ is a rewriting tree for a sentence, each variable occurs
bound in $\mathfrak{F}({\mathcal{T}})$ and is mapped by the store
$\mathfrak{s}_{\mathcal{T}}$ into the unique node of $\mathcal{T}$ that
contains a unique component atom in which that variable occurs:

$\begin{array}[]{llll}\mathfrak{s}_{\mathcal{T}}(r^{\epsilon})=\epsilon&\mathfrak{s}_{\mathcal{T}}(n^{\epsilon}_{1})=1&\mathfrak{s}_{\mathcal{T}}(n^{\epsilon}_{2})=2\\\
\mathfrak{s}_{\mathcal{T}}(n^{1}_{1})=11&\mathfrak{s}_{\mathcal{T}}(n^{1}_{2})=12&\mathfrak{s}_{\mathcal{T}}(n^{2}_{1})=21&\mathfrak{s}_{\mathcal{T}}(n^{2}_{2})=22\\\
\mathfrak{s}_{\mathcal{T}}(\ell^{\epsilon}_{1})=111&\mathfrak{s}_{\mathcal{T}}(r^{1}_{1})=112&\mathfrak{s}_{\mathcal{T}}(\ell^{1}_{2})=121&\mathfrak{s}_{\mathcal{T}}(r^{\epsilon}_{1})=122\\\
\mathfrak{s}_{\mathcal{T}}(\ell^{\epsilon}_{2})=211&\mathfrak{s}_{\mathcal{T}}(r^{2}_{1})=212&\mathfrak{s}_{\mathcal{T}}(\ell^{2}_{2})=221&\mathfrak{s}_{\mathcal{T}}(r^{\epsilon}_{2})=222\end{array}$

The configuration $(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})$
corresponding to the rewriting tree $\mathcal{T}$ from Fig. 5(a) is given
below:

$\begin{array}[]{rll}\alpha_{\mathcal{T}}(\mathsf{N})&=&\\{{\epsilon,1,2,11,12,21,22}\\}\\\
\alpha_{\mathcal{T}}(\mathsf{L})&=&\\{{111,112,121,122,211,212,221,222}\\}\\\
\alpha_{\mathcal{T}}(\mathsf{R})&=&\\{{\langle{\epsilon,1,2}\rangle,\langle{1,11,12}\rangle,\langle{11,111,112}\rangle,\langle{12,121,122}\rangle,\langle{21,211,212}\rangle,\langle{22,221,222}\rangle}\\}\\\
\alpha_{\mathcal{T}}(\mathsf{I})&=&\\{{\langle{111,112}\rangle,\langle{112,121}\rangle,\langle{121,122}\rangle,\langle{211,212}\rangle,\langle{212,221}\rangle,\langle{221,222}\rangle,\langle{222,111}\rangle}\\}\\\
\mathrm{m}_{\mathcal{T}}&=&\\{q_{0}[\epsilon],q_{0}[1],q_{0}[2],q_{0}[11],q_{0}[12],q_{0}[21],q_{0}[22],s_{0}[111],s_{0}[112],s_{0}[121],s_{0}[122],\\\
&&s_{0}[211],s_{0}[212],s_{0}[221],s_{0}[222]\\}\hfill\blacksquare\end{array}$

###  5.3 Symmetry Reduction

As shown in Lemma 1, each model of a sentence is a model of the characteristic
formula of some rewriting tree for that sentence. In this section, we prove a
symmetry property of the models of a characteristic formula corresponding to a
given rewriting tree, that makes them indistinguishable from the point of view
of the decision problems considered previously (§4). Let us fix a signature
$\Sigma$, with component types
$\mathfrak{C}=\\{{\mathsf{C}_{1},\ldots,\mathsf{C}_{N}}\\}$ and interaction
types $\mathfrak{I}=\\{{\mathsf{I}_{1},\ldots,\mathsf{I}_{M}}\\}$, and a
behavior map $\beta$, in the rest of this section.

Intuitively, two architectures are symmetric if they differ only by a renaming
of indices used to interpret the component and interaction types. For
instance, the architectures $\alpha_{1}$ and $\alpha_{2}$, where
$\alpha_{1}(\mathsf{C}_{1})=\alpha_{1}(\mathsf{C}_{2})=\\{{1}\\}$,
$\alpha_{1}(\mathsf{I}_{1})=\\{{\langle{1,1}\rangle}\\}$ and
$\alpha_{2}(\mathsf{C}_{1})=\\{{1}\\}$,
$\alpha_{2}(\mathsf{C}_{2})=\\{{2}\\}$,
$\alpha_{2}(\mathsf{I}_{1})=\\{{\langle{1,2}\rangle}\\}$ have the same shape
(assuming $N=2$ and $M=1$). However, this isomorphism cannot be captured by a
global permutation of indices, as it is usually the case444Typically, global
permutations suffice when only one component type is considered. in the
literature [13], because the sets
$\alpha_{1}(\mathsf{C}_{1})\cup\alpha_{1}(\mathsf{C}_{2})$ and
$\alpha_{2}(\mathsf{C}_{1})\cup\alpha_{2}(\mathsf{C}_{2})$ have different
cardinalities. For this reason, our definition of symmetry considers one
permutation per component type.

Formally, given an architecture $\alpha$ over $\Sigma$ and a tuple of
bijections $\mathbf{f}=\langle{f_{1},\ldots,f_{N}}\rangle$, where each
$f_{i}:\mathbb{U}\rightarrow\mathbb{U}$ renames the indices of the component
type $\mathsf{C}_{i}$, for all $i\in[{1},{N}]$, we define:

$\begin{array}[]{rcl}(\mathbf{f}(\alpha))(\mathsf{C}_{i})&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&f_{i}(\alpha(\mathsf{C}_{i}))\text{,
for all $i\in[{1},{N}]$}\\\
(\mathbf{f}(\alpha))(\mathsf{I})&\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}&\\{\langle{f_{i_{1}}(u_{1}),\ldots,f_{i_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})}\rangle\mid\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in\alpha(\mathsf{I}),{}\\\
&&\hskip 113.81102pt\forall
k\in[{1},{\\#(\mathsf{I})}]~{}.~{}\mathit{comp}({\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}})=\mathsf{C}_{i_{k}}\\}\end{array}$

For a marking $\mathrm{m}$ of the Petri net
$\mathsf{N}({\Sigma,\alpha,\beta})$, we define, moreover:

$\mathbf{f}(\mathrm{m})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{q[f_{i}(u)]\mid
q[u]\in\mathrm{m},~{}q\in\mathit{states}_{\beta}({\mathsf{C}_{i}}),~{}i\in[{1},{N}]\\}$

Since the sets $\mathit{states}_{\beta}({\mathsf{C}_{i}})$, for
$i\in[{1},{N}]$, are assumed to be pairwise disjoint, for each state $q$ there
is exactly one component type $\mathsf{C}_{i}$, such that
$q\in\mathit{states}_{\beta}({\mathsf{C}_{i}})$.

###### Definition 8

Two configurations are _symmetric_ , denoted
$(\alpha_{1},\mathrm{m}_{1})\sim(\alpha_{2},\mathrm{m}_{2})$, if and only if
there exists a tuple of bijections
$\mathbf{f}=\langle{f_{1},\ldots,f_{N}}\rangle$, where
$f_{i}:\mathbb{U}\rightarrow\mathbb{U}$, for all $i\in[{1},{N}]$, such that
$\mathbf{f}(\alpha_{1})=\alpha_{2}$ and
$\mathbf{f}(\mathrm{m}_{1})=\mathrm{m}_{2}$.

The main idea of using symmetries is to prove that models of the same
characteristic formula $\mathfrak{F}({\mathcal{T}})$ of some rewriting tree
$\mathcal{T}$ are symmetric and, in particular, symmetric with the canonical
model $(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})$. This proof is greatly
simplified by considering only those architectures in which all interactions
are _tightly connected_ to components, in the following sense:

###### Definition 9

An architecture $\alpha$ is _tight_ if and only if, for each interaction
$\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}]$ from $\alpha$ and each
$k\in[{1},{\\#(\mathsf{I})}]$, we have $u_{k}\in\alpha(\mathsf{C})$, where
$\mathsf{C}\in\mathfrak{C}$ is the unique component type such that
$\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}\in\mathfrak{P}({\mathsf{C}})$.

Note that interactions from an architecture $\alpha$, having unconnected
ports, cannot fire in the Petri net $\mathsf{N}({\Sigma,\alpha,\beta})$ (Def.
1), thus having no impact on the answer of a decision problem (deadlock,
reachability). Nevertheless, the CL logic is redundant in this respect, as it
allows to specify architectures with loose interactions. We get rid of this
redundancy and assume a syntactic restriction on formulæ, which guarantees the
tightness of models:

###### Definition 10

A _profile_ is a function $\lambda:\mathbb{A}\rightarrow\bigcup_{i\geq
1}\mathfrak{C}^{i}$, that associates each predicate symbol
$\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})$ of non-zero arity with a
tuple of component types of length $\\#(\mathcal{A})\geq 1$. A formula $\phi$
is _tight for a profile $\lambda$_ if and only if it contains, for each
interaction atom $\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})$ and each
$k\in[{1},{\\#(\mathsf{I})}]$:

  * •

a component atom $\mathsf{C}^{q}(x_{k})$, such that
$\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}\in\mathfrak{P}({\mathsf{C}})$,
or

  * •

a predicate atom $\mathcal{A}(y_{1},\ldots,y_{\\#(\mathcal{A})})$, such that
$x_{k}=y_{\ell}$ and
$\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}\in\mathfrak{P}({\langle{\lambda({\mathcal{A}})}\rangle_{\ell}})$,
for some $\ell\in[{1},{\\#(\mathcal{A})}]$.

A SID $\Delta$ is _tight_ if and only if there exists a profile
$\lambda_{\Delta}$, such that, for each rule
$\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\phi$ from $\Delta$,
the formula $\phi$ is tight for $\lambda_{\Delta}$ and contains, for each
$k\in[{1},{\\#(\mathcal{A})}]$:

  * •

a component atom $\mathsf{C}^{q}(x_{k})$, such that
$\langle{\lambda_{\Delta}(\mathcal{A})}\rangle_{k}=\mathsf{C}$, or

  * •

a predicate atom $\mathcal{B}(y_{1},\ldots,y_{\\#(\mathcal{A})})$, such that
$x_{k}=y_{\ell}$ and
$\langle{\lambda_{\Delta}(\mathcal{A})}\rangle_{k}=\langle{\lambda_{\Delta}(\mathcal{B})}\rangle_{\ell}$,
for some $\ell\in[{1},{\\#(\mathcal{B})}]$.

A formula $\phi$, interpreted over a tight SID $\Delta$, is _tight_ if and
only if it is tight for the profile $\lambda_{\Delta}$.

For instance, one can check that the predicate atoms
$\mathit{Chain}_{{n},{t}}(x,y)$ are tight, by taking the profile
$\lambda_{\Delta}(\mathit{Chain}_{{n},{t}})=\langle{\mathsf{S},\mathsf{S}}\rangle$,
for all constants $n,t\geq 0$ (Example 5). Analogously, the predicate atoms
$\mathit{Node}(n,\ell,r)$ are tight, by taking the profile
$\lambda_{\Delta}(\mathit{Node})=\langle{\mathsf{N},\mathsf{L},\mathsf{L}}\rangle$
and $\lambda_{\Delta}(\mathit{Leaf})=\langle{\mathsf{L}}\rangle$ (Example 6).
The above conditions guarantee the tightness of architectures described by
tight formulæ:

###### Lemma 4

For each model $(\alpha,\mathrm{m})$ of a tight sentence, the architecture
$\alpha$ is tight.

_Proof_ : Let $\phi$ be a tight sentence, such that
$(\alpha,\mathrm{m})\models\phi$. By Lemma 1, there exists a rewriting tree
$\mathcal{T}\in\mathbb{T}({\phi})$, such that
$(\alpha,\mathrm{m})\models\mathfrak{F}({\mathcal{T}})$. Let
$\mathsf{I}(z_{1},\ldots,z_{\\#(\mathsf{I})})$ be an interaction atom from
$\mathfrak{F}({\mathcal{T}})$ and $k\in[{1},{\\#(\mathsf{I})}]$. Also, let
$w\in\mathrm{nodes}({\mathcal{T}})$ be the node where this interaction atom
was introduced, such that
$\mathcal{T}(w)=\left(\mathcal{A}(x_{1},\ldots,x_{\\#(\mathcal{A})})\leftarrow\varphi\right)$
and $\mathsf{I}(y_{1},\ldots,y_{\\#(\mathsf{I})})$ occurs in $\varphi$, where
$y_{1},\ldots,y_{\\#(\mathsf{I})}$ are substituted by
$z_{1},\ldots,z_{\\#(\mathcal{A})}$, respectively, during the construction of
$\mathfrak{F}({\mathcal{T}})$. Since the SID $\Delta$, that interprets the
formula $\phi$, is tight, the rule body $\varphi$ is tight, hence one of the
following holds:

  * •

there exists a component atom $\mathsf{C}^{q}(y_{k})$ in $\varphi$, such that
$\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}=\mathsf{C}$, or

  * •

there exists a predicate atom
$\mathcal{B}(\xi_{1},\ldots,\xi_{\\#(\mathcal{B})})$ in $\varphi$, such that
$y_{k}=\xi_{\ell}$ and
$\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}=\langle{\lambda_{\Delta}(\mathcal{B})}\rangle_{\ell}$,
where $\lambda_{\Delta}$ is the profile from Def. 10. In this case, we apply
induction to prove the existence of a component atom $\mathsf{C}^{q}(\xi_{k})$
in $\mathfrak{F}({{\mathcal{T}}\\!\\!\downarrow_{\scriptscriptstyle{i}}})$,
such that $\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}=\mathsf{C}$, where
$i\in[{1},{\\#_{\mathsf{pred}}({\varphi})}]$ is the child of $w$ corresponding
to $\mathcal{B}(\xi_{1},\ldots,\xi_{\\#(\mathcal{B})})$ in $\mathcal{T}$.

In both cases, $\mathfrak{F}({\mathcal{T}})$ contains a component atom
$\mathsf{C}^{q}(z_{k})$, such that
$\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}=\mathsf{C}$, hence
$(\alpha,\mathrm{m})$ is tight, by Def. 9.

The next result proves that each model of a tight sentence is necessarily
symmetric to a canonical model of that sentence:

###### Lemma 5

Given a tight sentence $\phi$, for each $\mathcal{T}\in\mathbb{T}({\phi})$, if
$(\alpha,\mathrm{m})\models\mathfrak{F}({\mathcal{T}})$, then
$(\alpha,\mathrm{m})\sim{}(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})$.

_Proof_ : Since
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models\mathfrak{F}({\mathcal{T}})$,
by Lemma 3, it is sufficient to prove that
$(\alpha_{1},\mathrm{m}_{1})\sim{}(\alpha_{2},\mathrm{m}_{2})$, for any two
configurations $(\alpha_{i},\mathrm{m}_{i})$, such that
$(\alpha_{i},\mathrm{m}_{i})\models\mathfrak{F}({\mathcal{T}})$. Let
$\mathfrak{F}({\mathcal{T}})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\exists
x_{1}\ldots\exists x_{n}~{}.~{}\eta$, where $\eta$ is a quantifier- and
predicate-free formula. Then
$(\alpha_{i},\mathrm{m}_{i})\models\mathfrak{F}({\mathcal{T}})$ if and only if
there exist stores $\mathfrak{s}_{i}$, such that
$(\alpha_{i},\mathrm{m}_{i})\models^{\mathfrak{s}_{i}}\eta$, for $i=1,2$. We
define the sets
$U^{i}_{j}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\\{{\mathfrak{s}_{i}(x)\mid\mathsf{C}^{q}_{j}(x)\text{
occurs in }\eta}\\}$ and the bijections $f_{j}:U^{1}_{j}\rightarrow U^{2}_{j}$
as $f_{j}(\mathfrak{s}_{1}(x))=\mathfrak{s}_{2}(x)$, for all variables $x$,
such that $\mathsf{C}^{q}_{j}(x)$ occurs in $\eta$. These bijections are
extended to bijections $\overline{f}_{j}:\mathbb{U}\rightarrow\mathbb{U}$, by
the following fact:

###### Fact 1

Given finite sets $U_{1},U_{2}\subseteq\mathbb{U}$, such that
$f:U_{1}\rightarrow U_{2}$ is a bijection, there exists a bijection
$\overline{f}:\mathbb{U}\rightarrow\mathbb{U}$, such that
$\overline{f}(u)=f(u)$, for all $u\in U_{1}$.

_Proof_ : Since $f$ is a bijection, we have
$|\\!|{U_{1}}|\\!|=|\\!|{U_{2}}|\\!|$ and, since
$|\\!|{U_{i}}|\\!|=|\\!|{U_{i}\setminus U_{3-i}}|\\!|+|\\!|{U_{1}\cap
U_{2}}|\\!|$, for $i=1,2$, we obtain $|\\!|{U_{1}\setminus
U_{2}}|\\!|=|\\!|{U_{2}\setminus U_{1}}|\\!|$. Hence there exists a bijection
$\overline{f}:\mathbb{U}\rightarrow\mathbb{U}$, such that
$\overline{f}(u)=f(u)$, for all $u\in U_{1}$, $\overline{f}(U_{2}\setminus
U_{1})=U_{1}\setminus U_{2}$ and $\overline{f}(\mathbb{U}\setminus(U_{1}\cup
U_{2}))=f(\mathbb{U}\setminus(U_{1}\cup U_{2}))$.

For
$\mathbf{f}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{=}}\langle{\overline{f}_{1},\ldots,\overline{f}_{N}}\rangle$,
we prove the following points:

  * •

$\mathbf{f}(\alpha_{1})=\alpha_{2}$: by the definition of $\overline{f}_{j}$,
we have
$\overline{f}_{j}(\alpha_{1}(\mathsf{C}_{j}))=\alpha_{2}(\mathsf{C}_{j})$, for
all $j\in[{1},{N}]$. Let $\mathsf{I}\in\mathfrak{I}$ and we prove
$\alpha_{2}(\mathsf{I})=\\{\langle{\overline{f}_{i_{1}}(u_{1}),\ldots,\overline{f}_{i_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})}\rangle\mid\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in\alpha_{1}(\mathsf{I}),~{}\forall
k\in[{1},{\\#(\mathsf{I})}]~{}.~{}\mathit{comp}({\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}})=\mathsf{C}_{i_{k}}\\}$.
“$\subseteq$” Let
$\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in\alpha_{2}(\mathsf{I})$.
Then there exists an interaction atom
$\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})$ in $\eta$, such that
$u_{i}=\mathfrak{s}_{2}(x_{i})$, for $i\in[{1},{\\#(\mathsf{I})}]$. Since
$\phi$ is a tight sentence and $(\alpha_{2},\mathrm{m}_{2})\models\phi$, by
Lemma 4, the architecture $\alpha_{2}$ is tight (Def. 9). Then, for each
$k\in[{1},{\\#(\mathsf{I})}]$, we have
$u_{k}\in\alpha_{2}(\mathsf{C}_{i_{k}})$, where
$\mathsf{C}_{i_{k}}\in\mathfrak{C}$ is the unique component type such that
$\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}\in\mathfrak{P}({\mathsf{C}_{i_{k}}})$.
By the previous point, there exists
$u^{\prime}_{k}\in\alpha_{1}(\mathsf{C}_{i_{k}})$, such that
$\overline{f}_{i_{k}}(u^{\prime}_{k})=u_{k}=\mathfrak{s}_{2}(x_{k})$. By the
definition of $\overline{f}_{i_{k}}$, we have
$u^{\prime}_{k}=\mathfrak{s}_{1}(x_{k})$, hence
$\langle{u^{\prime}_{1},\ldots,u^{\prime}_{\\#(\mathsf{I})}}\rangle\in\alpha_{1}(\mathsf{I})$.
“$\supseteq$” Let
$\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in\alpha_{1}(\mathsf{I})$,
such that
$\mathit{comp}({\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{k}})=\mathsf{C}_{i_{k}}$,
for all $k\in[{1},{\\#(\mathsf{I})}]$. Then there exists an interaction atom
$\mathsf{I}(x_{1},\ldots,x_{\\#(\mathsf{I})})$ in $\eta$, such that
$u_{k}=\mathfrak{s}_{1}(x_{k})$, for all $k\in[{1},{\\#(\mathsf{I})}]$. Since
$\phi$ is a tight sentence and $(\alpha_{1},\mathrm{m}_{1})\models\phi$, by
Lemma 4, the architecture $\alpha_{1}$ is tight, thus
$\mathfrak{s}_{1}(x_{k})=u_{k}\in\alpha_{1}(\mathsf{C}_{i_{k}})$. By the
definition of $\overline{f}_{i_{k}}$, we have
$\mathfrak{s}_{2}(x_{k})=\overline{f}_{i_{k}}(u_{k})$, for all
$k\in[{1},{\\#(\mathsf{I})}]$, hence
$\langle{\overline{f}_{i_{1}}(u_{1}),\ldots,\overline{f}_{i_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})}\rangle\in\alpha_{2}(\mathsf{I})$.

  * •

$\mathbf{f}(\mathrm{m}_{1})=\mathrm{m}_{2}$: we prove
$\mathrm{m}_{2}=\\{{q[\overline{f}_{i}(u)]\mid
q[u]\in\mathrm{m}_{1},q\in\mathit{states}_{\beta}({\mathsf{C}_{i}}),i\in[{1},{N}]}\\}$.
“$\subseteq$” Let $q[u]\in\mathrm{m}_{2}$. Since
$(\alpha_{2},\mathrm{m}_{2})\models^{\mathfrak{s}_{2}}\eta$, there exists a
component atom $\mathsf{C}_{i}^{q}(x)$ in $\eta$, such that
$u=\mathfrak{s}_{2}(x)\in\alpha_{2}(\mathsf{C}_{i})$ and $\mathsf{C}_{i}$ is
the unique component type, such that
$q\in\mathit{states}_{\beta}({\mathsf{C}_{i}})$. By the definition of
$\overline{f}_{i}$, we have $\mathfrak{s}_{1}(x)\in\alpha_{1}(\mathsf{C}_{i})$
and $\mathfrak{s}_{2}(x)=\overline{f}_{i}(\mathfrak{s}_{1}(x))$. Moreover,
since $(\alpha_{1},\mathrm{m}_{1})\models^{\mathfrak{s}_{1}}\eta$, we have
$q[\mathfrak{s}_{1}(x)]\in\mathrm{m}_{1}$. “$\supseteq$” Let
$q[u]\in\mathrm{m}_{1}$ and $q\in\mathit{states}_{\beta}({\mathsf{C}_{i}})$,
for some $i\in[{1},{N}]$. Since
$(\alpha_{1},\mathrm{m}_{1})\models^{\mathfrak{s}_{1}}\eta$, there exists a
component atom $\mathsf{C}^{q}(x)$ in $\eta$, such that
$u=\mathfrak{s}_{1}(x)$. By the definition of $\overline{f}_{i}$, we have
$\overline{f}_{i}(\mathfrak{s}_{1}(x))=\mathfrak{s}_{2}(x)$, hence
$q[\overline{f}_{i}(u)]=q[\mathfrak{s}_{2}(x)]\in\mathrm{m}_{2}$, since
$(\alpha_{2},\mathrm{m}_{2})\models^{\mathfrak{s}_{2}}\eta$.

Moreover, the symmetry relation is preserved by the Petri net describing the
operational semantics of the system (Def. 1):

###### Lemma 6

Given a tight architecture $\alpha$ and a behavior $\beta$, over a signature
$\Sigma=(\\{{\mathsf{C}_{1},\ldots,\mathsf{C}_{N}}\\},\mathfrak{I},\mathfrak{P})$,
for any tuple of bijections $\mathbf{f}=\langle{f_{1},\ldots,f_{N}}\rangle$,
where $f_{i}:\mathbb{U}\rightarrow\mathbb{U}$, for all $i\in[{1},{N}]$, the
following hold:

  1. 1.

$\mathrm{m}^{\prime}\in\mathit{Reach}({\mathsf{N}({\Sigma,\alpha,\beta}),\mathrm{m}})\iff\mathbf{f}(\mathrm{m}^{\prime})\in\mathit{Reach}({\mathsf{N}({\Sigma,\mathbf{f}(\alpha),\beta}),\mathbf{f}(\mathrm{m})})$,

  2. 2.

$\mathrm{m}\in\mathit{Dead}({\mathsf{N}({\Sigma,\alpha,\beta})})\iff\mathbf{f}(\mathrm{m})\in\mathit{Dead}({\mathsf{N}({\Sigma,\mathbf{f}(\alpha),\beta})})$,

for any two markings $\mathrm{m},\mathrm{m}^{\prime}$ of the Petri net
$\mathsf{N}({\Sigma,\alpha,\beta})$.

_Proof_ : By Def. 1, let $\mathsf{N}({\Sigma,\mathbf{f}(\alpha),\beta})$ be
the Petri net $(S^{\mathbf{f}},T^{\mathbf{f}},E^{\mathbf{f}})$, where:

$\begin{array}[]{rcl}S^{\mathbf{f}}&=&\bigcup_{i=1}^{N}\\{{q[u]\mid
q\in\mathit{states}({\mathsf{C}_{i}}),~{}u\in(\mathbf{f}(\alpha))(\mathsf{C}_{i})}\\}\\\\[2.84526pt]
&=&\bigcup_{i=1}^{N}\\{{q[f_{i}(u)]\mid
q\in\mathit{states}({\mathsf{C}_{i}}),~{}u\in\alpha(\mathsf{C}_{i})}\\}\\\\[5.69054pt]
T^{\mathbf{f}}&=&\bigcup_{\mathsf{I}\in\mathfrak{I}}\\{~{}(\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)~{}\mid~{}\langle{p_{1},\ldots,p_{\\#(\mathsf{I})}}\rangle=\mathfrak{P}({\mathsf{I}}),\\\\[2.84526pt]
&&\hskip
34.14322pt\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in(\mathbf{f}(\alpha))(\mathsf{I}),~{}\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle\in
T_{\beta}{}(\mathsf{I}),\\\\[2.84526pt] &&\hskip 34.14322pt\forall
i,j\in[{1},{\\#(\mathsf{I})}].~{}i\not=j\Rightarrow u_{i}\not=u_{j}\mbox{ or
}\mathit{comp}({p_{i}})\not=\mathit{comp}({p_{j}})~{}\\}\\\\[5.69054pt]
&=&\bigcup_{\mathsf{I}\in\mathfrak{I}}\\{~{}(\mathsf{I}[f_{k_{1}}(u_{1}),\ldots,f_{k_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)~{}\mid~{}\langle{p_{1},\ldots,p_{\\#(\mathsf{I})}}\rangle=\mathfrak{P}({\mathsf{I}}),\\\\[2.84526pt]
&&\hskip
34.14322pt\langle{\mathsf{C}_{k_{1}},\ldots\mathsf{C}_{k_{\\#(\mathsf{I})}}}\rangle=\langle{\mathit{comp}({p_{1}}),\dots,\mathit{comp}({p_{\\#(\mathsf{I})}})}\rangle,\\\\[2.84526pt]
&&\hskip
34.14322pt\langle{u_{1},\ldots,u_{\\#(\mathsf{I})}}\rangle\in\alpha(\mathsf{I}),~{}\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle\in
T_{\beta}{}(\mathsf{I}),\\\\[2.84526pt] &&\hskip 34.14322pt\forall
i,j\in[{1},{\\#(\mathsf{I})}].~{}i\not=j\Rightarrow
f_{k_{i}}(u_{i})\not=f_{k_{j}}(u_{j})\mbox{ or
}\mathit{comp}({p_{i}})\not=\mathit{comp}({p_{j}})~{}\\}\end{array}$
$\begin{array}[]{rcl}E^{\mathbf{f}}&=&\bigcup_{\mathsf{I}\in\mathfrak{I}}\\{~{}(q[f_{k_{i}}(u_{i})],(\mathsf{I}[f_{k_{1}}(u_{1}),\ldots,f_{k_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)),\\\\[2.84526pt]
&&\hskip
28.45274pt((\mathsf{I}[f_{k_{1}}(u_{1}),\ldots,f_{k_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle),q^{\prime}[f_{k_{i}}(u_{i})])~{}\mid{}\\\\[2.84526pt]
&&\hskip 34.14322ptt_{i}=(q\xrightarrow{{\scriptstyle
p_{i}}}_{{\scriptstyle\mathit{comp}({p_{i}})}}q^{\prime}),~{}i\in[{1},{\\#(\mathsf{I})}]~{}\\}\end{array}$

We obtain the following equivalence:

$\begin{array}[]{c}\mathrm{m}\xrightarrow{{\scriptstyle(\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)}}\mathrm{m}^{\prime}\text{
in $\mathsf{N}({\Sigma,\alpha,\beta})$}\\\ \iff\\\
\mathbf{f}(\mathrm{m})\xrightarrow{{\scriptstyle(\mathsf{I}[f_{k_{1}}(u_{1}),\ldots,f_{k_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)}}\mathbf{f}(\mathrm{m}^{\prime})\text{
in $\mathsf{N}({\Sigma,\mathbf{f}(\alpha),\beta})$}\end{array}$

where $k_{1},\ldots,k_{\\#(\mathsf{I})}\in[{1},{N}]$ are such that
$\mathsf{C}_{k_{i}}=\mathit{comp}({\langle{\mathfrak{P}({\mathsf{I}})}\rangle_{i}})$,
for all $i\in[{1},{\\#(\mathsf{I})}]$. Point (1) uses this fact inductively,
on the length of the firing sequence leading from $\mathrm{m}$ to
$\mathrm{m}^{\prime}$. For point (2) we use, moreover, that
$q[u]\in\mathrm{m}\iff q[f_{i}(u)]\in\mathbf{f}(\mathrm{m})$ and
$q[u]\in\text{$\leftidx{{}^{\bullet}}{\text{${(\mathsf{I}[u_{1},\ldots,u_{\\#(\mathsf{I})}],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)}$}}$}\iff
q[f_{i}(u)]\in\text{$\leftidx{{}^{\bullet}}{\text{${(\mathsf{I}[f_{k_{1}}(u_{1}),\ldots,f_{k_{\\#(\mathsf{I})}}(u_{\\#(\mathsf{I})})],\langle{t_{1},\ldots,t_{\\#(\mathsf{I})}}\rangle)}$}}$}$,
where $\mathsf{C}_{i}$ is the unique component type such that
$q\in\mathit{states}_{\beta}({\mathsf{C}_{i}})$.

###### Theorem 2

Given a tight sentence $\phi$, interpreted over a SID $\Delta$, a behavior map
$\beta$ and a tuple of states $\langle{q_{1},\ldots,q_{k}}\rangle$, the
following equivalences hold:

$\begin{array}[]{rcl}\mathit{deadlock}_{t}(\phi,\Delta,\beta)&\iff&\mathit{deadlock}(\phi,\Delta,\beta)\\\
\mathit{reach}_{t}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)&\iff&\mathit{reach}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)\end{array}$

where $\mathit{deadlock}_{t}(\phi,\Delta,\beta)$ and
$\mathit{reach}_{t}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)$ are
defined below:

  * •

$\mathit{deadlock}_{t}(\phi,\Delta,\beta)$: does there exist rewriting tree
$\mathcal{T}\in\mathbb{T}({\phi})$, such that
$\mathit{Reach}({\mathsf{N}({\Sigma,\alpha_{\mathcal{T}},\beta}),\mathrm{m}_{\mathcal{T}}})\cap\mathit{Dead}({\mathsf{N}({\Sigma,\alpha_{\mathcal{T}},\beta})})\neq\emptyset$?

  * •

$\mathit{reach}_{t}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)$:
does there exist a rewriting tree $\mathcal{T}\in\mathbb{T}({\phi})$ and a
configuration
$(\alpha_{\mathcal{T}},\mathrm{m})\in\mathit{Reach}({\mathsf{N}({\Sigma,\alpha_{\mathcal{T}},\beta}),\mathrm{m}_{\mathcal{T}}})$,
such that $\\{q_{i}[u_{i}]$ $\mid i\in[{1},{k}]\\}\subseteq\mathrm{m}$, with
$q_{1}[u_{1}],\ldots,q_{k}[u_{k}]$ pairwise distinct?

_Proof_ : We prove the following points:

  * •

$\mathit{deadlock}_{t}(\phi,\Delta,\beta)\Rightarrow\mathit{deadlock}(\phi,\Delta,\beta)$:
assume that $\mathit{deadlock}_{t}(\phi,\Delta,\beta)$ has a positive answer
and let $\mathcal{T}\in\mathbb{T}({\phi})$ be a rewriting tree, such that
$\mathit{Reach}({\mathsf{N}({\Sigma,\alpha_{\mathcal{T}},\beta}),\mathrm{m}_{\mathcal{T}}})\cap\mathit{Dead}({\mathsf{N}({\Sigma,\alpha_{\mathcal{T}},\beta})})\neq\emptyset$,
the existence of which is stated by
$\mathit{deadlock}_{t}(\phi,\Delta,\beta)$. By Lemma 3,
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models\mathfrak{F}({\mathcal{T}})$
and, by Lemma 1, we obtain
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models\phi$, thus
$\mathit{deadlock}(\phi,\Delta,\beta)$ has a positive answer.

  * •

$\mathit{deadlock}(\phi,\Delta,\beta)\Rightarrow\mathit{deadlock}_{t}(\phi,\Delta,\beta)$:
assume that $\mathit{deadlock}(\phi,\Delta,\beta)$ has a positive answer and
let $(\alpha,\mathrm{m})$ be a model of $\phi$ and $\mathrm{m}^{\prime}$ be a
marking such that
$\mathrm{m}^{\prime}\in\mathit{Reach}({\mathsf{N}({\Sigma,\alpha,\beta}),\mathrm{m}})\cap\mathit{Dead}({\mathsf{N}({\Sigma,\alpha,\beta})})$.
By Lemma 1, there exists a rewriting tree $\mathcal{T}\in\mathbb{T}({\phi})$,
such that $(\alpha,\mathrm{m})\models\mathfrak{F}({\mathcal{T}})$. By Lemma 5,
since $\phi$ is a tight sentence, we obtain that
$(\alpha,\mathrm{m})\sim{}(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})$ and
let $\mathbf{f}=\langle{f_{1},\ldots,f_{N}}\rangle$ be the bijections from
Def. 8, such that
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})=(\mathbf{f}(\alpha),\mathbf{f}(\mathrm{m}))$.
By Lemma 6, we obtain that
$\mathbf{f}(\mathrm{m}^{\prime})\in\mathit{Reach}({\mathsf{N}({\Sigma,\mathbf{f}(\alpha),\beta}),\mathbf{f}(\mathrm{m})})\cap\mathit{Dead}({\mathsf{N}({\Sigma,\mathbf{f}(\alpha),\beta})})$,
thus $\mathit{deadlock}_{t}(\phi,\Delta,\beta)$ has a positive answer.

  * •

$\mathit{reach}_{t}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)\Rightarrow\mathit{reach}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)$:
assume that
$\mathit{reach}_{t}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)$ has
a positive answer and let $\mathcal{T}\in\mathbb{T}({\phi})$ be a rewriting
tree and $\mathrm{m}$ be a marking of
$\mathsf{N}({\Sigma,\alpha_{\mathcal{T}},\beta})$, such that
$(\alpha_{\mathcal{T}},\mathrm{m})\in\mathit{Reach}({\mathsf{N}({\Sigma,\alpha_{\mathcal{T}},\beta}),\mathrm{m}_{\mathcal{T}}})$
and $\\{{q_{i}[u_{i}]~{}|~{}i\in[{1},{k}]}\\}\subseteq\mathrm{m}$, where
$q_{1}[u_{1}],\ldots,q_{k}[u_{k}]$ are pairwise distinct places. By Lemma 3,
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models\mathfrak{F}({\mathcal{T}})$
and, by Lemma 1, we obtain
$(\alpha_{\mathcal{T}},\mathrm{m}_{\mathcal{T}})\models\phi$, thus
$\mathit{reach}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)$ has a
positive answer.

  * •

$\mathit{reach}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)\Rightarrow\mathit{reach}_{t}(\phi,\langle{q_{1},\ldots,q_{k}}\rangle,\Delta,\beta)$:
assume that