# Abstract Interpretation of Temporal Concurrent Constraint Programs 111This
paper has been accepted for publication in Theory and Practice of Logic
Programming (TPLP), Cambridge University Press.

MORENO FALASCHI
Dipartimento di Ingegneria dell’Informazione e Scienze Matematiche
Università di Siena  Italy
E-mail<EMAIL_ADDRESS>CARLOS OLARTE
Departamento de Electrónica y Ciencias de la Computación
Pontificia Universidad Javeriana-Cali  Colombia
E-mail<EMAIL_ADDRESS>CATUSCIA PALAMIDESSI
INRIA and LIX
Ecole Polytechnique  France
E-mail<EMAIL_ADDRESS>
(15 May 2013; 3 December 2013)

###### Abstract

Timed Concurrent Constraint Programming (tcc) is a declarative model for
concurrency offering a logic for specifying reactive systems, i.e. systems
that continuously interact with the environment. The universal tcc formalism
(utcc) is an extension of tcc with the ability to express mobility. Here
mobility is understood as communication of private names as typically done for
mobile systems and security protocols. In this paper we consider the
denotational semantics for tcc, and we extend it to a “collecting” semantics
for utcc based on closure operators over sequences of constraints. Relying on
this semantics, we formalize a general framework for data flow analyses of tcc
and utcc programs by abstract interpretation techniques. The concrete and
abstract semantics we propose are compositional, thus allowing us to reduce
the complexity of data flow analyses. We show that our method is sound and
parametric with respect to the abstract domain. Thus, different analyses can
be performed by instantiating the framework. We illustrate how it is possible
to reuse abstract domains previously defined for logic programming to perform,
for instance, a groundness analysis for tcc programs. We show the
applicability of this analysis in the context of reactive systems.
Furthermore, we make also use of the abstract semantics to exhibit a secrecy
flaw in a security protocol. We also show how it is possible to make an
analysis which may show that tcc programs are suspension free. This can be
useful for several purposes, such as for optimizing compilation or for
debugging.

###### keywords:

Timed Concurrent Constraint Programming, Process Calculi, Abstract
Interpretation, Denotational Semantics, Reactive Systems

##  1 Introduction

Concurrent Constraint Programming (ccp) [Saraswat et al. (1991), Saraswat
(1993)] has emerged as a simple but powerful paradigm for concurrency tied to
logic that extends and subsumes both concurrent logic programming [Shapiro
(1989)] and constraint logic programming [Jaffar and Lassez (1987)]. The ccp
model combines the traditional operational view of process calculi with a
_declarative_ one based upon logic. This combination allows ccp to benefit
from the large body of reasoning techniques of both process calculi and logic.
In fact, ccp-based calculi have successfully been used in the modeling and
verification of several concurrent scenarios such as biological, security,
timed, reactive and stochastic systems [Saraswat et al. (1991), Olarte and
Valencia (2008b), Nielsen et al. (2002a), Saraswat et al. (1994), Jagadeesan
et al. (2005)] (see a survey in [Olarte et al. (2013)]).

In the ccp model, agents interact by _telling_ and _asking_ pieces of
information (_constraints_) on a shared store of partial information. The type
of constraints that agents can tell and ask is parametric in an underlying
constraint system. This makes ccp a flexible model able to adapt to different
application domains.

The ccp model has been extended to consider the execution of processes along
time intervals or time-units. In tccp [de Boer et al. (2000)], the notion of
time is identified with the time needed to ask and tell information to the
store. In this model, the information in the store is carried through the
time-units. On the other hand, in Timed ccp (tcc) [Saraswat et al. (1994)],
stores are not automatically transferred between time-units. This way,
computations during a time-unit proceed monotonically but outputs of two
different time-units are not supposed to be related to each other. More
precisely, computations in tcc take place in bursts of activity at a rate
controlled by the environment. In this model, the environment provides a
stimulus (input) in the form of a constraint. Then the system, after a finite
number of internal reductions, outputs the final store (a constraint) and
waits for the next interaction with the environment. This view of _reactive
computation_ is akin to synchronous languages such as Esterel [Berry and
Gonthier (1992)] where the system reacts continuously with the environment at
a rate controlled by the environment. Hence, these languages allow to program
safety critical applications as control systems, for which it is fundamental
to provide tools aiming at helping to develop correct, secure, and efficient
programs.

Universal tcc [Olarte and Valencia (2008b)] (utcc), adds to tcc the
expressiveness needed for _mobility_. Here we understand mobility as the
ability to communicate private names (or variables) much like in the
$\pi$-calculus [Milner et al. (1992)]. Roughly, a tcc  _ask_ process
$\mathbf{when}\ c\ \mathbf{do}\ P$ executes the process $P$ only if the
constraint $c$ can be entailed from the store. This idea is generalized in
utcc by a parametric ask that executes $P[\vec{t}/\vec{x}]$ when the
constraint $c[\vec{t}/\vec{x}]$ is entailed from the store. Hence the
variables in $\vec{x}$ act as formal parameters of the ask operator. This
simple change allowed to widen the spectrum of application of ccp-based
languages to scenarios such as verification of security protocols [Olarte and
Valencia (2008b)] and service oriented computing [López et al. (2009)].

Several domains and frameworks (e.g., [Cousot and Cousot (1992), Armstrong et
al. (1998), Codish et al. (1999)] ) have been proposed for the analysis of
logic programs. The particular characteristics of timed ccp programs pose
additional difficulties for the development of such tools in this language.
Namely, the concurrent, timed nature of the language, and the synchronization
mechanisms based on entailment of constraints (blocking asks). Aiming at
statically analyzing utcc as well as tcc programs, we have to consider the
additional technical issues due to the infinite internal computations
generated by parametric asks as we shall explain later.

We develop here a _compositional_ semantics for tcc and utcc that allows us to
describe the behavior of programs and collects all concrete information needed
to properly abstract the properties of interest. This semantics is based on
closure operators over sequences of constraints along the lines of [Saraswat
et al. (1994)]. We show that parametric asks in utcc of the form
$(\mathbf{abs}\ \vec{x};c)\,P$ can be neatly characterized as closure
operators. This characterization is shown to be somehow dual to the semantics
for the local operator $(\mathbf{local}\,\vec{x})\,P$ that restricts the
variables in $\vec{x}$ to be local to $P$. We prove the semantics to be fully
abstract w.r.t. the operational semantics for a significant fragment of the
calculus.

We also propose an abstract semantics which approximates the concrete one. Our
framework is formalized by abstract interpretation techniques and is
parametric w.r.t. the abstract domain. It allows us to exploit the work done
for developing abstract domains for logic programs. Moreover, we can make new
analyses for reactive and mobile systems, thus widening the reasoning
techniques available for tcc and utcc, such as type systems [Hildebrandt and
López (2009)], logical characterizations [Mendler et al. (1995), Nielsen et
al. (2002a), Olarte and Valencia (2008b)] and semantics [Saraswat et al.
(1994), de Boer et al. (1995), Nielsen et al. (2002a)].

The abstraction we propose proceeds in two-levels. First, we approximate the
constraint system leading to an abstract constraint system. We give the
sufficient conditions which have to be satisfied for ensuring the soundness of
the abstraction. Next, to obtain efficient analyses, we abstract the infinite
sequences of (abstract) constraints obtained from the previous step. Our
semantics is then computable and compositional. Thus, it allows us to master
the complexity of the data-flow analyses. Moreover, the abstraction _over-
approximates_ the concrete semantics, thus preserving safety properties.

To the best of our knowledge, this is the first attempt to propose a
compositional semantics and an abstract interpretation framework for a
language adhering to the above-mentioned characteristics of utcc. Hence we can
develop analyses for several applications of utcc or its sub-calculus tcc (see
e.g., [Olarte et al. (2013)]). In particular, we instantiate our framework in
three different scenarios. The first one presents an abstraction of a
cryptographic constraint system. We use the abstract semantics to bound the
number of messages that a spy may generate, in order to exhibit a secrecy flaw
in a security protocol written in utcc. The second one tailors an abstract
domain for groundness and type dependency analysis in logic programming to
perform a groundness analysis of a tcc program. This analysis is proven useful
to derive a property of a control system specified in tcc. Finally, we present
an analysis that may show that a tcc program is suspension free. This analysis
can be used later for optimizing compilation or for debugging purposes.

The ideas of this paper stem mainly from the works of the authors in [de Boer
et al. (1995), Falaschi et al. (1997a), Falaschi et al. (1997b), Nielsen et
al. (2002a), Olarte and Valencia (2008a)] to give semantic characterization of
ccp calculi and from the works in [Falaschi et al. (1993), Codish et al.
(1994), Falaschi et al. (1997a), Zaffanella et al. (1997), Falaschi et al.
(2007)] to provide abstract interpretation frameworks to analyze concurrent
logic-based languages. A preliminary short version of this paper without
proofs was published in [Falaschi et al. (2009)]. In this paper we give many
more examples and explanations. We also refine several technical details and
present full proofs. Furthermore, we develop a new application for analyzing
suspension-free tcc programs.

The rest of the paper is organized as follows. Section 2 recalls the notion of
constraint system and the operational semantics of tcc and utcc. In Section 3
we develop the denotational semantics based on sequences of constraints. Next,
in Section 4, we study the abstract interpretation framework for tcc and utcc
programs. The three instances and the applications of the framework are
presented in Section 5. Section 6 concludes.

##  2 Preliminaries

Process calculi based on the ccp paradigm are parametric in a _constraint
system_ specifying the basic constraints agents can tell and ask. These
constraints represent a piece of (partial) information upon which processes
may act. The constraint system hence provides a signature from which
constraints can be built. Furthermore, the constraint system provides an
_entailment_ relation ($\vdash$) specifying inter-dependencies between
constraints. Intuitively, $c\vdash d$ means that the information $d$ can be
deduced from the information represented by $c$. For example, $x>60\vdash
x>42$.

Here we consider an abstract definition of constraint systems as cylindric
algebras as in [de Boer et al. (1995)]. The notion of constraint system as
first-order formulas [Smolka (1994), Nielsen et al. (2002a), Olarte and
Valencia (2008b)] can be seen as an instance of this definition. All results
of this paper still hold, of course, when more concrete systems are
considered.

######  Definition 1 (Constraint System)

A cylindric constraint system is a structure
${\mathbf{C}}=\langle\mathcal{C},\leq,\sqcup,\operatorname{\textup{{t}}},\operatorname{\textup{{f}}},{\mathit{V}ar},\exists,D\rangle$
s.t.
\-
$\langle\mathcal{C},\leq,\sqcup,\operatorname{\textup{{t}}},\operatorname{\textup{{f}}}\rangle$
is a lattice with $\sqcup$ the $\mathit{l}ub$ operation (representing the
logical _and_), and $\operatorname{\textup{{t}}}$,
$\operatorname{\textup{{f}}}$ the least and the greatest elements in
$\mathcal{C}$ respectively (representing true and false). Elements in
$\mathcal{C}$ are called _constraints_ with typical elements
$c,c^{\prime},d,d^{\prime}...$. If $c\leq d$ and $d\leq c$ we write $c\cong
d$. If $c\leq d$ and $c\not\cong d$, we write $c<d$.
-${\mathit{V}ar}$ is a denumerable set of variables and for each $x\in{\mathit{V}ar}$ the function $\exists x:\mathcal{C}\to\mathcal{C}$ is a cylindrification operator satisfying: (1) $\exists x(c)\leq c$. (2) If $c\leq d$ then $\exists x(c)\leq\exists x(d)$. (3) $\exists x(c\sqcup\exists x(d))\cong\exists x(c)\sqcup\exists x(d)$. (4) $\exists x\exists y(c)\cong\exists y\exists x(c)$. (5) For an increasing chain $c_{1}<c_{2}<c_{3}...$, $\exists x\bigsqcup_{i}c_{i}\cong\bigsqcup_{i}\exists x(c_{i})$.
\- For each $x,y\in{\mathit{V}ar}$, the constraint $d_{xy}\in D$ is a
_diagonal element_ and it satisfies: (1)
$d_{xx}\cong\operatorname{\textup{{t}}}$. (2) If $z$ is different from $x,y$
then $d_{xy}\cong\exists z(d_{xz}\sqcup d_{zy})$. (3) If $x$ is different from
$y$ then $c\leq d_{xy}\sqcup\exists x(c\sqcup d_{xy})$.

The cylindrification operators model a sort of existential quantification,
helpful for hiding information. We shall use ${\mathit{f}v}(c)=\\{x\in Var\ |\
\exists x(c)\not\cong c\\}$ to denote the set of free variables that occur in
$c$. If $x$ occurs in $c$ and $x\not\in{\mathit{f}v}(c)$, we say that $x$ is
bound in $c$. We use ${\mathit{b}v}(c)$ to denote the set of bound variables
in $c$.

Properties (1) to (4) are standard. Property (5) is shown to be required in
[de Boer et al. (1995)] to establish the semantic adequacy of ccp languages
when infinite computations are considered. Here, the continuity of the
semantic operator in Section 3 relies on the continuity of $\exists$ (see
Proposition 3.8). Below we give some examples on the requirements to satisfy
this property in the context of different constraint systems.

The diagonal element $d_{xy}$ can be thought of as the equality $x=y$.
Properties (1) to (3) are standard and they allow us to define substitutions
of the form $[t/x]$ required, for instance, to represent the substitution of
formal and actual parameters in procedure call. We shall give a formal
definition of them in Notation 2.

Let us give some examples of constraint systems. The finite domain constraint
system (FD) [Hentenryck et al. (1998)] assumes variables to range over finite
domains and, in addition to equality, one may have predicates that restrict
the possible values of a variable to some finite set, for instance $x<42$.

The Herbrand constraint system $\mathcal{H}$ consists of a first-order
language with equality. The entailment relation is the one we expect from
equality, for instance, $f(x,y)=f(g(a),z)$ must entail $x=g(a)$ and $y=z$.
$\mathcal{H}$ may contain non-compact elements to represent the limit of
infinite chains. To see this, let $s$ be the successor constructor, $\exists
y(x=s(s^{n}(y)))$ be denoted as the constraint $\texttt{gt}(x,n)$ (i.e.,
$x>n$) and $\\{\texttt{gt}(x,n)\\}_{n}$ be the ascending chain
$\texttt{gt}(x,0)<\texttt{gt}(x,1)<\cdots$. We note that $\exists
x(\texttt{gt}(x,n))=\operatorname{\textup{{t}}}$ for any $n$ and then,
$\bigsqcup\\{\exists x(\texttt{gt}(x,n))\\}_{n}=\operatorname{\textup{{t}}}$.
Property (5) in Definition 1 dictates that $\exists
x\bigsqcup\\{\texttt{gt}(x,n)\\}_{n}$ must be equal to
$\operatorname{\textup{{t}}}$ (i.e., there exists an $x$ which is greater than
any $n$). For that, we need a constraint, e.g., $\texttt{inf}(x)$ (a non-
compact element), to be the limit $\bigsqcup\\{\texttt{gt}(x,n)\\}_{n}$. We
know that $\texttt{inf}(x)\vdash\texttt{gt}(x,n)$ for any $n$ and then,
$\bigsqcup\\{\texttt{gt}(x,n)\\}_{n}=\texttt{inf}(x)$ and $\exists
x(\texttt{inf}(x))=\operatorname{\textup{{t}}}$ as wanted. A similar
phenomenon arises in the definition of constraint system as Scott information
systems in [Saraswat et al. (1991)]. There, constraints are represented as
finite subsets of _tokens_ (elementary constraints) built from a given set
$D$. The entailment is similar to that in Definition 1 but restricted to
compact elements, i.e., a constraint can be entailed only from a finite set of
elementary constraints. Moreover, $\exists$ is extended to be a continuous
function, thus satisfying Property (5) in Definition 1. Hence, the Herbrand
constraint system in [Saraswat et al. (1991)] considers also a non-compact
element (different from $\operatorname{\textup{{f}}}$) to be the limit of the
chain $\\{\texttt{gt}(x,n)\\}_{n}$.

Now consider the Kahn constraint system underlying data-flow languages where
equality is assumed along with the constant $\operatorname{\mathit{nil}}$ (the
empty list), the predicate $\texttt{nempty}(x)$ ($x$ is not
$\operatorname{\mathit{nil}}$), and the functions $\texttt{first}(x)$ (the
first element of $x$), $\texttt{rest}(x)$ ($x$ without its first element) and
$\texttt{cons}(x,y)$ (the concatenation of $x$ and $y$). If we consider the
Kahn constraint system in [Saraswat et al. (1991)], the constraint $c$ defined
as
$\\{\texttt{first}(\texttt{tail}^{n}(x))=\texttt{first}(\texttt{tail}^{n}(y))\mid
n\geq 0\\}$ does not entail $\\{x=y\\}$ since the entailment relation is
defined only on compact elements. In Definition 1, we are free to decide if
$c$ is different or not from $x=y$. If we equate them, the constraint $x=y$ is
not longer a compact element and then, one has to be careful to only use a
compact version of “$=$” in programs (see Definition 2). A similar situation
occurs with the Rational Interval Constraint System [Saraswat et al. (1991)]
and the constraints $\\{x\in[0,1+1/n]\mid n\geq 0\\}$ and $x\in[0,1]$.

All in all many different constraint systems satisfy Definition 1.
Nevertheless, one has to be careful since the constraint systems might not be
the same as what is naively expected due to the presence of non-compact
elements.

We conclude this section by setting some notation and conventions about terms,
sequences of constraints, substitutions and diagonal elements. We first lift
the relation $\leq$ and the cylindrification operator to sequences of
constraints.

######  Notation 1 (Sequences of Constraints)

We denote by $\mathcal{C}^{\omega}$ (resp. $\mathcal{C}^{*})$ the set of
infinite (resp. finite) sequences of constraints with typical elements
$w,w^{\prime},s,s^{\prime},...$. We use $W,W^{\prime},S,S^{\prime}$ to range
over subsets of $\mathcal{C}^{\omega}$ or $\mathcal{C}^{*}$. We use
$c^{\omega}$ to denote the sequence $c.c.c...$. The length of $s$ is denoted
by $|s|$ and the empty sequence by $\epsilon$. The $i$-th element in $s$ is
denoted by $s(i)$. We write $s\leq s^{\prime}$ iff $|s|\leq|s^{\prime}|$ and
for all $i\in\\{1,\ldots,|s|\\}$, $s^{\prime}(i)\vdash s(i)$. If
$|s|=|s^{\prime}|$ and for all $i\in\\{1,...,|s|\\}$ it holds $s(i)\cong
s^{\prime}(i)$, we shall write $s\cong s^{\prime}$. Given a sequence of
variables $\vec{x}$, with $\exists\vec{x}(c)$ we mean $\exists x_{1}\exists
x_{2}...\exists x_{n}(c)$ and with $\exists\vec{x}(s)$ we mean the pointwise
application of the cylindrification operator to the constraints in $s$.

We shall assume that the diagonal element $d_{xy}$ is interpreted as the
equality $x=y$. Furthermore, following [Giacobazzi et al. (1995)], we extend
the use of $d_{xy}$ to consider terms as in $d_{xt}$. More precisely,

######  Convention 1 (Diagonal elements)

We assume that the constraint system under consideration contains an equality
theory. Then, diagonal elements $d_{xy}$ can be thought of as formulas of the
form $x=y$. We shall use indistinguishably both notations. Given a variable
$x$ and a term $t$ (i.e., a variable, constant or $n$-place function of $n$
terms symbol), we shall use $d_{xt}$ to denote the equality $x=t$. Similarly,
given a sequence of distinct variables $\vec{x}$ and a sequence of terms
$\vec{t}$, if $|\vec{x}|=|\vec{t}|=n$ then $d_{\vec{x}\vec{t}}$ denotes the
constraint $\bigsqcup\limits_{1\leq i\leq n}x_{i}=t_{i}$. If
$|\vec{x}|=|\vec{t}|=0$ then $d_{\vec{x}\vec{t}}=\operatorname{\textup{{t}}}$.
Given a set of diagonal elements $E$, we shall write $E\Vdash
d_{\vec{x}\vec{t}}$ whenever $d_{i}\vdash d_{\vec{x}\vec{t}}$ for some
$d_{i}\in E$. Otherwise, we write $E\not\Vdash d_{\vec{x}\vec{t}}$.

Finally, we set the notation for substitutions.

######  Notation 2 (Admissible substitutions)

Let $\vec{x}$ be a sequence of pairwise distinct variables and $\vec{t}$ be a
sequence of terms s.t. $|\vec{t}|=|\vec{x}|$. We denote by
$c[\vec{t}/\vec{x}]$ the constraint $\exists\vec{x}(c\sqcup
d_{\vec{x}\vec{t}})$ which represents abstractly the constraint obtained from
$c$ by replacing the variables $\vec{x}$ by $\vec{t}$. We say that $\vec{t}$
is admissible for $\vec{x}$, notation $adm(\vec{x},\vec{t})$, if the variables
in $\vec{t}$ are different from those in $\vec{x}$. If $|\vec{x}|=|\vec{t}|=0$
then trivially $adm(\vec{x},\vec{t})$. Similarly, we say that the substitution
$[\vec{t}/\vec{x}]$ is admissible iff $adm(\vec{x},\vec{t})$. Given an
admissible substitution $[\vec{t}/\vec{x}]$, from Property (3) of diagonal
elements in Definition 1, we note that $c[\vec{t}/\vec{x}]\sqcup
d_{\vec{x}\vec{t}}\vdash c$.

###  2.1 Reactive Systems and Timed CCP

Reactive systems [Berry and Gonthier (1992)] are those that react continuously
with their environment at a rate controlled by the environment. For example, a
controller or a signal-processing system, receives a stimulus (input) from the
environment. It computes an output and then, waits for the next interaction
with the environment.

In the ccp model, the shared store of constraints grows monotonically, i.e.,
agents cannot drop information (constraints) from it. Then, a system that
changes the state of a variable as in “${\mathit{s}ignal=on}$” and
“${\mathit{s}ignal=off}"$ leads to an inconsistent store.

Timed ccp (tcc) [Saraswat et al. (1994)] extends ccp for reactive systems.
Time is conceptually divided into _time intervals_(or _time-units_). In a
particular time interval, a ccp process $P$ gets an input $c$ from the
environment, it executes with this input as the initial _store_ , and when it
reaches its resting point, it _outputs_ the resulting store $d$ to the
environment. The resting point determines also a residual process $Q$ which is
then executed in the next time-unit. The resulting store $d$ is not
automatically transferred to the next time-unit. This way, computations during
a time-unit proceed monotonically but outputs of two different time-units are
not supposed to be related to each other. Therefore, the variable
${\mathit{s}ignal}$ in the example above may change its value when passing
from one time-unit to the next one.

######  Definition 2 (tcc Processes)

The set $Proc$ of tcc processes is built from the syntax

$\begin{array}[]{lll}P,Q&:=&\mathbf{skip}\ \ |\ \ \mathbf{tell}(c)\ \ |\
\mathbf{when}\ c\ \mathbf{do}\ P\ \ |\ \ P\parallel Q\ \ |\ \
(\mathbf{local}\,\vec{x})\,P\ \ |\\\ &&\mathbf{next}\,P\ \ |\ \
\mathbf{unless}\ c\ \mathbf{next}\,P\ \ |\ \ p(\vec{t})\end{array}$

where $c$ is a compact element of the underlying constraint system. Let
$\mathcal{D}$ be a set of process declarations of the form
$p(\vec{x})\operatorname{:\\!--}P$. A tcc program takes the form
$\mathcal{D}.P$. We assume $\mathcal{D}$ to have a unique process definition
for every process name, and recursive calls to be guarded by a
${\mathbf{n}ext}$ process.

The process $\mathbf{skip}$ does nothing thus representing inaction. The
process $\mathbf{tell}(c)$ adds $c$ to the store in the current time interval
making it available to the other processes. The process $\mathbf{when}\ c\
\mathbf{do}\ P$ _asks_ if $c$ can be deduced from the store. If so, it behaves
as $P$. In other case, it remains blocked until the store contains at least as
much information as $c$. The parallel composition of $P$ and $Q$ is denoted by
$P\,\parallel\,Q$. Given a set of indexes $I=\\{1,...,n\\}$, we shall use
$\prod\limits_{i\in I}P_{i}$ to denote the parallel composition
$P_{1}\parallel...\parallel P_{n}$. The process $(\mathbf{local}\,\vec{x})\,P$
_binds_ $\vec{x}$ in $P$ by declaring it private to $P$. It behaves like $P$,
except that all the information on the variables $\vec{x}$ produced by $P$ can
only be seen by $P$ and the information on the global variables in $\vec{x}$
produced by other processes cannot be seen by $P$.

The process $\mathbf{next}\,P$ is a _unit-delay_ that executes $P$ in the next
time-unit. The _time-out_ $\mathbf{unless}\ c\ \mathbf{next}\,P$ is also a
unit-delay, but $P$ is executed in the next time-unit if and only if $c$ is
not entailed by the final store at the current time interval. We use
$\mathbf{next}^{n}P$ as a shorthand for $\mathbf{next}\dots\mathbf{next}\,P$,
with $\mathbf{next}$ repeated $n$ times.

We extend the definition of free variables to processes as follows:
${\mathit{f}v}(\mathbf{skip})=\emptyset$;
${\mathit{f}v}(\mathbf{tell}(c))={\mathit{f}v}(c)$;
${\mathit{f}v}(\mathbf{when}\ c\ \mathbf{do}\
Q)={\mathit{f}v}(c)\cup{\mathit{f}v}(Q)$; ${\mathit{f}v}(\mathbf{unless}\ c\
\mathbf{next}\,Q)={\mathit{f}v}(c)\cup{\mathit{f}v}(Q)$;
${\mathit{f}v}(Q\parallel
Q^{\prime})={\mathit{f}v}(Q)\cup{\mathit{f}v}(Q^{\prime})$;
${\mathit{f}v}((\mathbf{local}\,\vec{x})\,Q)={\mathit{f}v}(Q)\setminus\vec{x}$;
${\mathit{f}v}(\mathbf{next}\,Q)={\mathit{f}v}(Q)$;
${\mathit{f}v}(p(\vec{t}))=vars(\vec{t})$ where $vars(\vec{t})$ is the set of
variables occurring in $\vec{t}$. A variable $x$ is bound in $P$ if $x$ occurs
in $P$ and $x\notin{\mathit{f}v}(P)$. We use ${\mathit{b}v}(P)$ to denote the
set of bound variables in $P$.

Assume a (recursive) process definition $\ \ p(\vec{x})\operatorname{:\\!--}P\
\ $ where ${\mathit{f}v}(P)\subseteq\vec{x}$. The call $p(\vec{t})$ reduces to
$P[\vec{t}/\vec{x}]$. Recursive calls in $P$ are assumed to be guarded by a
$\mathbf{next}\,$ process to avoid non-terminating sequences of recursive
calls during a time-unit (see [Saraswat et al. (1994), Nielsen et al.
(2002a)]).

In the forthcoming sections we shall use the idiom $!\,P$ defined as follows:

######  Notation 3 (Replication)

The replication of $P$, denoted as $!\,P$, is a short hand for a call to a
process definition
$\texttt{bang}_{P}()\operatorname{:\\!--}P\parallel\mathbf{next}\,\texttt{bang}_{P}()$.
Hence, $!\,P$ means
$P\parallel\mathbf{next}\,P\parallel\mathbf{next}\,^{2}P...$.

###  2.2 Mobile behavior and utcc

As we have shown, interaction of tcc processes is asynchronous as
communication takes place through the shared store of partial information.
Similar to other formalisms, by defining local (or private) variables, tcc
processes specify boundaries in the interface they offer to interact with each
other. Once these interfaces are established, there are few mechanisms to
modify them. This is not the case e.g., in the $\pi$-calculus [Milner et al.
(1992)] where processes can change their communication patterns by exchanging
their private names. The following example illustrates the limitation of $ask$
processes to communicate values and local variables.

###### Example 1

Let $\operatorname{\textup{{out}}}(\cdot)$ be a constraint and let
$P=\mathbf{when}\ \operatorname{\textup{{out}}}(x)\ \mathbf{do}\ R$ be a
system that must react when receiving a stimulus (i.e., an input) of the form
$\operatorname{\textup{{out}}}(n)$ for $n>0$. We notice that $P$ in a store
$\operatorname{\textup{{out}}}(42)$ does not execute $R$ since
$\operatorname{\textup{{out}}}(42)\not\vdash\operatorname{\textup{{out}}}(x)$.

The key point in the previous example is that $x$ is a free-variable and
hence, it does not act as a formal parameter (or place holder) for every term
$t$ such that $\operatorname{\textup{{out}}}(t)$ is entailed by the store.

In [Olarte and Valencia (2008b)], tcc is extended for _mobile reactive_
systems leading to _universal timed_ ccp (utcc). To model mobile behavior,
utcc replaces the ask operation $\mathbf{when}\ c\ \mathbf{do}\ P$ with a
parametric ask construction, namely $(\mathbf{abs}\ \vec{x};c)\,P$. This
process can be viewed as a $\lambda$-_abstraction_ of the process $P$ on the
variables $\vec{x}$ under the constraint (or with the _guard_) $c$.
Intuitively, for all admissible substitution $[\vec{t}/\vec{x}]$ s.t. the
current store entails $c[\vec{t}/\vec{x}]$, the process $(\mathbf{abs}\
\vec{x};c)\,P$ performs $P[\vec{t}/\vec{x}]$. For example, $(\mathbf{abs}\
x;\operatorname{\textup{{out}}}(x))\,R$ in a store entailing both
$\operatorname{\textup{{out}}}(z)$ and $\operatorname{\textup{{out}}}(42)$
executes $R[42/x]$ and $R[z/x]$.

######  Definition 3 (utcc Processes and Programs)

The utcc processes and programs result from replacing in Definition 2 the
expression $\mathbf{when}\ c\ \mathbf{do}\ P$ with $(\mathbf{abs}\
\vec{x};c)\,P$ where the variables in $\vec{x}$ are pairwise distinct.

When $|\vec{x}|=0$ we write $\mathbf{when}\ c\ \mathbf{do}\ P$ instead of
$(\mathbf{abs}\ \epsilon;c)\,P$. Furthermore, the process $(\mathbf{abs}\
\vec{x};c)\,P$ binds $\vec{x}$ in $P$ and $c$. We thus extend accordingly the
sets ${\mathit{f}v}(\cdot)$ and ${\mathit{b}v}(\cdot)$ of free and bound
variables.

From a programming point of view, we can see the variables $\vec{x}$ in the
abstraction $(\mathbf{abs}\ \vec{x};c)\,P$ as the formal parameters of $P$. In
fact, the utcc calculus was introduced in [Olarte and Valencia (2008b)] with
replication ($!\,P$) and without process definitions since replication and
abstractions are enough to encode recursion. Here we add process definitions
to properly deal with tcc programs with recursion which are more expressive
than those without it (see [Nielsen et al. (2002b)]) and we omit replication
to avoid redundancy in the set of operators (see Notation 3). We thus could
have dispensed with the next-guarded restriction in Definition 2 for utcc
programs. Nevertheless, in order to give a unified presentation of the
forthcoming results, we assume that utcc programs adhere also to that
restriction.

We conclude with an example of mobile behavior where a process $P$ sends a
local variable to $Q$. Then, both processes can communicate through the shared
variable.

######  Example 2 (Scope extrusion)

Assume two components $P$ and $Q$ of a system such that $P$ creates a local
variable that must be shared with $Q$. This system can be modeled as

$\begin{array}[]{lll l
lll}P&=&(\mathbf{local}\,x)\,(\mathbf{tell}(\operatorname{\textup{{out}}}(x))\parallel
P^{\prime})&&Q&=&(\mathbf{abs}\
z;\operatorname{\textup{{out}}}(z))\,Q^{\prime}\end{array}$

We shall show later that the parallel composition of $P$ and $Q$ evolves to a
process of the form $P^{\prime}\parallel Q^{\prime}[x/z]$ where $P^{\prime}$
and $Q^{\prime}$ share the local variable $x$ created by $P$. Then, any
information produced by $P^{\prime}$ on $x$ can be seen by $Q^{\prime}$ and
vice versa.

###  2.3 Operational Semantics (SOS)

We take inspiration on the structural operational semantics (SOS) for linear
ccp in [Fages et al. (2001), Haemmerlé et al. (2007)] to define the behavior
of processes. We consider _transitions_ between _configurations_ of the form
$\left\langle{\vec{x};P;c}\right\rangle$ where $c$ is a constraint
representing the current store, $P$ a process and $\vec{x}$ is a set of
distinct variables representing the bound (local) variables of $c$ and $P$. We
shall use $\gamma,\gamma^{\prime},\ldots$ to range over configurations.
Processes are quotiented by $\equiv$ defined as follows.

######  Definition 4 (Structural Congruence)

Let $\equiv$ be the smallest congruence satisfying: (1) $P\equiv Q$ if they
differ only by a renaming of bound variables (alpha-conversion); (2)
$P\parallel\mathbf{skip}\equiv P$; (3) $P\parallel Q\equiv Q\parallel P$; and
(4) $P\parallel(Q\parallel R)\equiv(P\parallel Q)\parallel R$.

The congruence relation $\equiv$ is extended to configurations by decreeing
that
$\left\langle{\vec{x};P;c}\right\rangle\equiv\left\langle{\vec{y};Q;d}\right\rangle$
iff $(\mathbf{local}\,\vec{x})\,P\equiv(\mathbf{local}\,\vec{y})\,Q$ and
$\exists\vec{x}(c)\cong\exists\vec{y}(d)$.

$\begin{array}[]{ccc}\hbox{ \kern 0.0pt\raise
7.04001pt\hbox{$\mathrm{R}_{TELL}$}\kern 0.0pt\kern 5.0pt\vbox{ \moveright
59.98729pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$#$&& \rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr\cr}}\nointerlineskip\kern 2.0pt\moveright
0.0pt\vbox{\hrule width=119.97458pt}\nointerlineskip\kern 2.0pt\moveright
0.0pt\hbox{$\left\langle{\vec{x};\mathbf{tell}(c);d}\right\rangle\longrightarrow\left\langle{\vec{x};\mathbf{skip};d\sqcup
c}\right\rangle$}}}&&\hbox{ \kern 0.0pt\raise
7.92888pt\hbox{$\mathrm{R}_{PAR}$}\kern 0.0pt\kern 5.0pt\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt \@ReturnLeftOffsettrue$#$&&
\rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr\left\langle{\vec{x};P;c}\right\rangle\longrightarrow\left\langle{\vec{x}\cup\vec{y};P^{\prime};d}\right\rangle\mbox{
, }\vec{y}\cap{\mathit{f}v}(Q)=\emptyset\cr}}\nointerlineskip\kern
2.0pt\moveright 0.0pt\vbox{\hrule width=158.7325pt}\nointerlineskip\kern
2.0pt\moveright 16.22493pt\hbox{$\left\langle{\vec{x};P\parallel
Q;c}\right\rangle\longrightarrow\left\langle{\vec{x}\cup\vec{y};P^{\prime}\parallel
Q;d}\right\rangle$}}}\\\ \\\ \lx@intercol\hfil\hbox{ \kern 0.0pt\raise
7.04001pt\hbox{$\mathrm{R}_{LOC}$}\kern 0.0pt\kern 5.0pt\vbox{ \moveright
20.10533pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$#$&& \rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr\vec{y}\cap\vec{x}=\emptyset,\vec{y}\cap{\mathit{f}v}(d)=\emptyset\cr}}\nointerlineskip\kern
2.0pt\moveright 0.0pt\vbox{\hrule width=131.0694pt}\nointerlineskip\kern
2.0pt\moveright
0.0pt\hbox{$\left\langle{\vec{x};(\mathbf{local}\,\vec{y})\,P;d}\right\rangle\longrightarrow\left\langle{\vec{x}\cup\vec{y};P;d}\right\rangle$}}}\hfil\lx@intercol\\\
\\\ \lx@intercol\hfil\hbox{ \kern 0.0pt\raise
7.04001pt\hbox{$\mathrm{R}_{ABS}$}\kern 0.0pt\kern 5.0pt\vbox{ \moveright
51.86166pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$#$&& \rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr d\vdash
c[\vec{t}/\vec{y}],adm(\vec{y},\vec{t}),\ \mbox{and }E\not\Vdash
d_{\vec{y}\vec{t}}\cr}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule
width=268.69235pt}\nointerlineskip\kern 2.0pt\moveright
0.0pt\hbox{$\left\langle{\vec{x};(\mathbf{abs}\
\vec{y};c;E)\,P;d}\right\rangle\longrightarrow\left\langle{\vec{x};P[\vec{t}/\vec{y}]\parallel(\mathbf{abs}\
\vec{y};c;E\cup\\{d_{\vec{y}\vec{t}}\\})\,P;d}\right\rangle$}}}\hfil\lx@intercol\\\
\\\ \lx@intercol\hfil\hbox{ \kern 0.0pt\raise
7.04001pt\hbox{$\mathrm{R}_{STRVAR}$}\kern 0.0pt\kern 5.0pt\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt \@ReturnLeftOffsettrue$#$&&
\rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr{\mathit{n}f}(c)=\exists\vec{x}_{1}c_{1}\sqcup\cdots\sqcup\exists\vec{x}_{n}c_{n}\
\ \ \ \ \vec{y}\cap\vec{x}_{i}=\emptyset\ \ \mbox{forall }i\in
1..n\cr}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule
width=243.27905pt}\nointerlineskip\kern 2.0pt\moveright
50.84776pt\hbox{$\left\langle{\vec{y};P;c}\right\rangle\longrightarrow\left\langle{\vec{y}\cup\bigcup\vec{x}_{i};P;c_{1}\sqcup...\sqcup
c_{n}}\right\rangle$}}}\hfil\lx@intercol\\\ \\\ \lx@intercol\hfil\hbox{ \kern
0.0pt\raise 8.24pt\hbox{$\mathrm{R}_{STR}$}\kern 0.0pt\kern 5.0pt\vbox{
\moveright 0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$#$&& \rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr\left\langle{\vec{x};Q;c}\right\rangle\longrightarrow\left\langle{\vec{y};Q^{\prime};c^{\prime\prime}}\right\rangle\cr}}\nointerlineskip\kern
2.0pt\moveright 0.0pt\vbox{\hrule width=82.99583pt}\nointerlineskip\kern
2.0pt\moveright
0.09651pt\hbox{$\left\langle{\vec{x};P;c}\right\rangle\longrightarrow\left\langle{\vec{x}^{\prime};P^{\prime};c^{\prime}}\right\rangle$}}}\qquad\mbox{if
}P\equiv Q\mbox{ and
}\left\langle{\vec{x}^{\prime};P^{\prime};c^{\prime}}\right\rangle\equiv\left\langle{\vec{y};Q^{\prime};c^{\prime\prime}}\right\rangle\hfil\lx@intercol\\\
\\\ \hbox{ \kern 0.0pt\raise 7.04001pt\hbox{$\mathrm{R}_{CALL}$}\kern
0.0pt\kern 5.0pt\vbox{ \moveright
0.09367pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$#$&& \rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr p(\vec{x})\operatorname{:\\!--}P\in\mathcal{D}\
\ \ \ adm(\vec{x},\vec{t})\cr}}\nointerlineskip\kern 2.0pt\moveright
0.0pt\vbox{\hrule width=115.10762pt}\nointerlineskip\kern 2.0pt\moveright
0.0pt\hbox{$\left\langle{\vec{x};p(\vec{t});d}\right\rangle\longrightarrow\left\langle{\vec{x};P[\vec{t}/\vec{x}];d}\right\rangle$}}}&&\hbox{
\kern 0.0pt\raise 7.04001pt\hbox{$\mathrm{R}_{UNL}$}\kern 0.0pt\kern
5.0pt\vbox{ \moveright 63.26749pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$#$&& \rightinferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$#$\cr d\vdash c\cr}}\nointerlineskip\kern
2.0pt\moveright 0.0pt\vbox{\hrule width=147.73392pt}\nointerlineskip\kern
2.0pt\moveright 0.0pt\hbox{$\left\langle{\vec{x};\mathbf{unless}\ c\
\mathbf{next}\,P;d}\right\rangle\longrightarrow\left\langle{\vec{x};\mathbf{skip};d}\right\rangle$}}}\\\
\\\ \lx@intercol\mbox{ Observable Transition}\hfil\lx@intercol\\\
\lx@intercol\hfil\mathrm{R}_{OBS}\
\frac{\raisebox{2.84544pt}{$\left\langle{\emptyset;P;c}\right\rangle\longrightarrow^{*}\left\langle{\vec{x};Q;d}\right\rangle\not\longrightarrow$}}{\raisebox{-5.69046pt}{$P\stackrel{{\scriptstyle\,\,(c,\exists\vec{x}(d))\,\,}}{{\,\,===\Longrightarrow}}(\mathbf{local}\,\vec{x})\,F(Q)$}}\
\mbox{\ \ where \ \
}\par{F}(P)=\left\\{\begin{array}[]{ll}F(\mathbf{skip})=F((\mathbf{abs}\
\vec{x};c;D)\,Q)=\mathbf{skip}\\\ F(P_{1}\parallel P_{2})=F(P_{1})\parallel
F(P_{2})\\\ F(\mathbf{next}\,Q)=F(\mathbf{unless}\ c\
\mathbf{next}\,Q)=Q\end{array}\right.\hfil\lx@intercol\end{array}$

Figure 1:  SOS. In $\mathrm{R}_{STR}$, $\equiv$ is given in Definition 4. In
$\mathrm{R}_{ABS}$ and $\mathrm{R}_{CALL}$, $adm(\vec{x},\vec{t})$ is defined
in Notation 2. In $\mathrm{R}_{ABS}$, $E$ is assumed to be a set of diagonal
elements and $\not\Vdash$ is defined in Convention 1. In
$\mathrm{R}_{STRVAR}$, ${\mathit{n}f}(d)$ is defined in Notation 4.

Transitions are given by the relations $\longrightarrow$ and $\Longrightarrow$
in Figure 1. The _internal_ transition
$\left\langle{\vec{x};P;c}\right\rangle\longrightarrow\left\langle{\vec{x}^{\prime};P^{\prime};c^{\prime}}\right\rangle$
should be read as “$P$ with store $c$ reduces, in one internal step, to
$P^{\prime}$ with store $c^{\prime}$ ”. We shall use $\longrightarrow^{*}$ as
the reflexive and transitive closure of $\longrightarrow$. If
$\gamma\longrightarrow\gamma^{\prime}$ and
$\gamma^{\prime}\equiv\gamma^{\prime\prime}$ we write
$\gamma\longrightarrow\equiv\gamma^{\prime\prime}$. Similarly for
$\longrightarrow^{*}$.

The _observable transition_
$P\stackrel{{\scriptstyle\,\,(c,d)\,\,}}{{\,\,===\Longrightarrow}}R$ should be
read as “$P$ on input $c$, reduces in one _time-unit_ to $R$ and outputs $d$”.
The observable transitions are obtained from finite sequences of internal
ones.

The rules in Figure 1 are easily seen to realize the operational intuitions
given in Section 2.1. As clarified below, the seemingly missing rule for a
$\mathbf{next}$ process is given by $\mathrm{R}_{OBS}$. Before explaining such
rules, let us introduce the following notation needed for
$\mathrm{R}_{STRVAR}$.

######  Notation 4 (Normal Form)

We observe that the store $c$ in a configuration takes the form
$\exists\vec{x}_{1}(d_{1})\sqcup...\sqcup\exists\vec{x}_{n}(d_{n})$ where each
$\vec{x}_{i}$ may be an empty set of variables. The normal form of $c$,
notation ${\mathit{n}f}(c)$, is the constraint obtained by renaming the
variables in $c$ such that for all $i,j\in 1..n$, if $i\neq j$ then the
variables in $\vec{x}_{i}$ do not occur neither bound nor free in $d_{j}$. It
is easy to see that $c\cong{\mathit{n}f}(c)$.

\- $\mathrm{R}_{TELL}$ says that the process $\mathbf{tell}(c)$ adds $c$ to
the current store $d$ (via the lub operator of the constraint system) and then
evolves into $\mathbf{skip}$.
\- $\mathrm{R}_{PAR}$ says that if $P$ may evolve into $P^{\prime}$, this
reduction also takes place when running in parallel with $Q$.
\- The process $(\mathbf{local}\,\vec{y})\,Q$ adds $\vec{y}$ to the local
variables of the configuration and then evolves into $Q$. The side conditions
of the rule $\mathrm{R}_{LOC}$ guarantee that $Q$ runs with a different set of
variables from those in the store and those used by other processes.

\- We extend the transition relation to consider processes of the form
$(\mathbf{abs}\ \vec{y};c;E)\,Q$ where $E$ is a set of diagonal elements. If
$E$ is empty, we write $(\mathbf{abs}\ \vec{y};c)\,Q$ instead of
$(\mathbf{abs}\ \vec{y};c;\emptyset)\,Q$. If $d$ entails $c[\vec{t}/\vec{y}]$,
then $P[\vec{t}/\vec{y}]$ is executed (Rule $\mathrm{R}_{ABS}$). Moreover, the
abstraction persists in the current time interval to allow other potential
replacements of $\vec{y}$ in $P$. Notice that $E$ is augmented with
$d_{\vec{y}\vec{t}}$ and the side condition $E\not\Vdash d_{\vec{y}\vec{t}}$
prevents executing $P[\vec{t}/\vec{y}]$ again. The process
$P[\vec{t}/\vec{y}]$ is obtained by equating $\vec{y}$ and $\vec{t}$ and then,
hiding the information about $\vec{y}$, i.e.,
$(\mathbf{local}\,\vec{y})\,(!\,\mathbf{tell}(d_{\vec{y}\vec{t}})\parallel
P)$.

\- Rule $\mathrm{R}_{STRVAR}$ allows us to _open_ the scope of existentially
quantified constraints in the store (see Example 3 below). If $\gamma$ reduces
to $\gamma^{\prime}$ using this rule then $\gamma\equiv\gamma^{\prime}$.
\- Rule $\mathrm{R}_{STR}$ says that one can use the structural congruence on
processes to continue a derivation (e.g., to do alpha conversion). It is worth
noticing that we do not allow in this rule to transform the store via the
relation $\equiv$ on configurations and then, via $\cong$ on constraints. We
shall discuss the reasons behind this choice in Example 3.
-What we observe from $p(\vec{t})$ is $P[\vec{t}/\vec{x}]$ where the formal parameters are substituted by the actual parameter (Rule $\mathrm{R}_{CALL}$).
\- Since the process $P=\mathbf{unless}\ c\ \mathbf{next}\,Q$ executes $Q$ in
the next time-unit only if the final store at the current time-unit does not
entail $c$, in the rule $\mathrm{R}_{UNL}$ $P$ evolves into $\mathbf{skip}$ if
the current store $d$ entails $c$.

For the observable transition relation, rule $\mathrm{R}_{OBS}$ says that an
observable transition from $P$ labeled with $(c,\exists\vec{x}(d))$ is
obtained from a terminating sequence of internal transitions from
$\left\langle{\emptyset;P;c}\right\rangle$ to
$\left\langle{\vec{x};Q;d}\right\rangle$. The process to be executed in the
next time interval is $(\mathbf{local}\,\vec{x})\,F(Q)$ (the “future” of $Q$).
$F(Q)$ is obtained by removing from $Q$ the ${\mathbf{a}bs}$ processes that
could not be executed and by “unfolding” the sub-terms within $\mathbf{next}$
and $\mathbf{unless}$ expressions. Notice that the output of a process hides
the local variables ($\exists\vec{x}(d)$) and those variables are also hidden
in the next time-unit ($(\mathbf{local}\,\vec{x})\,F(Q)$).

Now we are ready to show that processes in Example 2 evolve into a
configuration where a (local) variable can be communicated and shared.

######  Example 3 (Scope Extrusion and Structural Rules)

Let $P$ and $Q$ be as in Example 2. In the following we show the evolution of
the process $P\parallel Q$ starting from the store $\exists
w(\operatorname{\textup{{out}}}(w))$:

$\begin{array}[]{llll}\mbox{\tiny 1}&\left\langle{\emptyset;P\parallel
Q;\exists
w(\operatorname{\textup{{out}}}(w))}\right\rangle&\longrightarrow^{*}&\left\langle{\\{x\\};\mathbf{tell}(\operatorname{\textup{{out}}}(x))\parallel
P^{\prime}\parallel Q;\exists
w(\operatorname{\textup{{out}}}(w))}\right\rangle\\\ \mbox{\tiny
2}&&\longrightarrow^{*}&\left\langle{\\{x\\};P^{\prime}\parallel Q;\exists
w(\operatorname{\textup{{out}}}(w))\sqcup\operatorname{\textup{{out}}}(x)}\right\rangle\\\
\mbox{\tiny 3}&&\longrightarrow^{*}&\left\langle{\\{x,w\\};P^{\prime}\parallel
Q;\operatorname{\textup{{out}}}(w)\sqcup\operatorname{\textup{{out}}}(x)}\right\rangle\\\
\mbox{\tiny 4}&&\longrightarrow^{*}&\left\langle{\\{x,w\\};P^{\prime}\parallel
Q_{1}\parallel
Q^{\prime}[w/z];\operatorname{\textup{{out}}}(w)\sqcup\operatorname{\textup{{out}}}(x)}\right\rangle\\\
\mbox{\tiny 5}&&\longrightarrow^{*}&\left\langle{\\{x,w\\};P^{\prime}\parallel
Q_{2}\parallel Q^{\prime}[w/z]\parallel
Q^{\prime}[x/z];\operatorname{\textup{{out}}}(w)\sqcup\operatorname{\textup{{out}}}(x)}\right\rangle\end{array}$

where $Q_{1}=(\mathbf{abs}\
z;\operatorname{\textup{{out}}}(z);\\{d_{wz}\\})\,Q^{\prime}$ and
$Q_{2}=(\mathbf{abs}\
z;\operatorname{\textup{{out}}}(z);\\{d_{wz},d_{xz}\\})\,Q^{\prime}$. Observe
that $P^{\prime}$ and $Q^{\prime}[x/z]$ share the local variable $x$ created
by $P$. The derivation from line 2 to line 3 uses the Rule
$\mathrm{R}_{STRVAR}$ to _open_ the scope of $w$ in the store $\exists
w(\operatorname{\textup{{out}}}(w))$. Let $c_{1}=\exists
w(\operatorname{\textup{{out}}}(w))\sqcup\operatorname{\textup{{out}}}(x)$
(store in line 2) and $c_{2}=\operatorname{\textup{{out}}}(x)$. We know that
$c_{1}\cong c_{2}$. As we said before, Rule $\mathrm{R}_{STR}$ allows us to
replace structural congruent processes ($\equiv$) but it does not modify the
store via the relation $\cong$ on constraints. The reason is that if we
replace $c_{1}$ in line 2 with $c_{2}$, then we will not observe the execution
of $Q^{\prime}[w/x]$.

###  2.4 Observables and Behavior

In this section we study the input-output behavior of programs and we show
that such relation is a function. More precisely, we show that the input-
output relation is a (partial) upper closure operator. Then, we characterize
the behavior of a process by the sequences of constraints such that the
process cannot add any information to them. We shall call this behavior the
strongest postcondition. This relation is fundamental to later develop the
denotational semantics for tcc and utcc programs.

Next lemma states some fundamental properties of the internal relation. The
proof follows from simple induction on the inference
$\gamma\longrightarrow\gamma^{\prime}$.

######  Lemma 1 (Properties of $\longrightarrow$)

Assume that
$\left\langle{\vec{x};P;c}\right\rangle\longrightarrow\left\langle{\vec{x}^{\prime};Q;d}\right\rangle$.
Then, $\vec{x}\subseteq\vec{x}^{\prime}$. Furthermore:
1\. (Internal Extensiveness):
$\exists\vec{x}^{\prime}(d)\vdash\exists\vec{x}(c)$, i.e., the store can only
be augmented.
2\. (Internal Potentiality): If $e\vdash c$ and $d\vdash e$ then
$\left\langle{\vec{x};P;e}\right\rangle\longrightarrow\equiv\left\langle{\vec{x}^{\prime};Q;d}\right\rangle$,
i.e., a stronger store triggers more internal transitions.
4\. (Internal Restartability):
$\left\langle{\vec{x};P;d}\right\rangle\longrightarrow\equiv\left\langle{\vec{x}^{\prime};Q;d}\right\rangle$.

####  2.4.1 Input-Output Behavior

Recall that tcc and utcc allows for the modeling of reactive systems where
processes react according to the stimuli (input) from the environment. We
define the behavior of a process $P$ as the relation of its outputs under the
influence of a sequence of inputs (constraints) from the environment. Before
formalizing this idea, it is worth noticing that unlike tcc, some utcc
processes may exhibit infinitely many internal reductions during a time-unit
due to the $\mathbf{abs}$ operator.

######  Example 4 (Infinite Behavior)

Consider a constant symbol “$a$”, a function symbol $f$, a unary predicate
(constraint) $c(\cdot)$ and let $Q=(\mathbf{abs}\
x;c(x))\,\mathbf{tell}(c(f(x)))$. Operationally, $Q$ in a store $c(a)$ engages
in an infinite sequence of internal transitions producing the constraints
$c(f(a))$, $c(f(f(a)))$, $c(f(f(f(a))))$ and so on.

The above behavior will arise, for instance, in applications to security as
those in Section 5.1. We shall see that the model of the attacker may generate
infinitely many messages (constraints) if we do not restrict the length of the
messages (i.e., the number of nested applications of $f$).

######  Definition 5 (Input-Output Behavior)

Let $s=c_{1}.c_{2}...c_{n}$,
$s^{\prime}=c_{1}^{\prime}.c_{2}^{\prime}...c_{n}^{\prime}$ (resp.
$w=c_{1}.c_{2}...$, $w^{\prime}=c_{1}^{\prime}.c_{2}^{\prime}...$) be finite
(resp. infinite) sequences of constraints. If
$P=P_{1}\stackrel{{\scriptstyle\,\,(c_{1},c_{1}^{\prime})\,\,}}{{\,\,===\Longrightarrow}}P_{2}\stackrel{{\scriptstyle\,\,(c_{2},c_{2}^{\prime})\,\,}}{{\,\,===\Longrightarrow}}...P_{n}\stackrel{{\scriptstyle\,\,(c_{n},c_{n}^{\prime})\,\,}}{{\,\,===\Longrightarrow}}P_{n+1}$
(resp.
$P=P_{1}\stackrel{{\scriptstyle\,\,(c_{1},c_{1}^{\prime})\,\,}}{{\,\,===\Longrightarrow}}P_{2}\stackrel{{\scriptstyle\,\,(c_{2},c_{2}^{\prime})\,\,}}{{\,\,===\Longrightarrow}}...$
) , we write
$P\stackrel{{\scriptstyle\,\,(s,s^{\prime})\,\,}}{{\,\,===\Longrightarrow}}$
(resp.
$P\stackrel{{\scriptstyle\,\,(w,w^{\prime})\,\,}}{{\,\,===\Longrightarrow_{\omega}}}$).
We define the _input-output_ behavior of $P$ as
$\mathit{i}o{(P)}=\mathit{i}o^{\mathit{f}in}{(P)}\cup\mathit{i}o^{\mathit{i}nf}{(P)}$
where

$\begin{array}[]{lll}\mathit{i}o^{\mathit{f}in}{(P)}&=&\\{(s,s^{\prime})\ |\
P\stackrel{{\scriptstyle\,\,(s,s^{\prime})\,\,}}{{\,\,===\Longrightarrow}}\\}\mbox{
for }s,s^{\prime}\in\mathcal{C}^{*}\\\
\mathit{i}o^{\mathit{i}nf}{(P)}&=&\\{(w,w^{\prime})\ |\
P\stackrel{{\scriptstyle\,\,(w,w^{\prime})\,\,}}{{\,\,===\Longrightarrow_{\omega}}}\\}\mbox{
for }w,w^{\prime}\in\mathcal{C}^{\omega}\end{array}$

We recall that the observable transition
($\stackrel{{\scriptstyle\,\,\,\,}}{{\,\,===\Longrightarrow}}$) is defined
through a finite number of internal transitions (rule $\mathrm{R}_{OBS}$ in
Figure 1). Hence, it may be the case that for some utcc processes (e.g., $Q$
in Example 4), $\mathit{i}o^{\mathit{i}nf}=\emptyset$. For this reason, we
distinguish finite and infinite sequences in the input-output behavior
relation. We notice that if $w\in\mathit{i}o^{\mathit{i}nf}(P)$ then any
finite prefix of $w$ belongs to $\mathit{i}o^{\mathit{f}in}(P)$. We shall call
_well-terminated_ the processes which do not exhibit infinite internal
behavior.

######  Definition 6 (Well-termination)

The process $P$ is said to be _well-terminated_ w.r.t. an infinite sequence
$w$ if there exists $w^{\prime}\in\mathcal{C}^{\omega}$ s.t.
$(w,w^{\prime})\in\mathit{i}o^{\mathit{i}nf}(P).$

Note that tcc processes are well-terminated since recursive calls must be
${\mathbf{n}ext}$ guarded. The fragment of well-terminated utcc processes has
been shown to be a meaningful one. For instance, in [Olarte and Valencia
(2008a)] the authors show that such fragment is enough to encode Turing-
powerful formalisms and [López et al. (2009)] shows the use of this fragment
in the declarative interpretation of languages for structured communications.

We conclude here by showing that the utcc calculus is deterministic. The
result follows from Lemma 1 (see A).

######  Theorem 1 (Determinism)

Let $s,w$ and $w^{\prime}$ be (possibly infinite) sequences of constraints. If
both $(s,w)$, $(s,w^{\prime})\in{\mathit{i}o}(P)$ then $w\cong w^{\prime}$.

####  2.4.2 Closure Properties and Strongest Postcondition

The $\mathbf{unless}$ operator is the only construct in the language that
exhibits non-monotonic input-output behavior in the following sense: Let
$P=\mathbf{unless}\ c\ \mathbf{next}\,Q$ and $s\leq s^{\prime}$. If
$(s,w),(s^{\prime},w^{\prime})\in{\mathit{i}o}(P)$, it may be the case that
$w\not\leq w^{\prime}$. For example, take $Q=\mathbf{tell}(d)$,
$s=\operatorname{\textup{{t}}}^{\omega}$ and
$s^{\prime}=c.\operatorname{\textup{{t}}}^{\omega}$. The reader can verify
that $w=\operatorname{\textup{{t}}}.d.\operatorname{\textup{{t}}}^{\omega}$,
$w^{\prime}=c.\operatorname{\textup{{t}}}^{\omega}$ and then, $w\not\leq
w^{\prime}$.

######  Definition 7 (Monotonic Processes)

We say that $P$ is a monotonic process if it does not have occurrences of
${\mathbf{u}nless}$ processes. Similarly, the program $\mathcal{D}.P$ is
monotonic if $P$ and all $P_{i}$ in a process definition
$p_{i}(\vec{x})\operatorname{:\\!--}P_{i}$ are monotonic.

Now we show that ${\mathit{i}o}(P)$ is a _partial upper closure operator_ ,
i.e., it is a function satisfying _extensiveness_ and _idempotence_.
Furthermore, if $P$ is _monotonic_ , ${\mathit{i}o}(P)$ is a _closure
operator_ satisfying additionally monotonicity. The proof of this result
follows from Lemma 1 (see details in A).

######  Lemma 2 (Closure Properties)

Let $P$ be a process. Then, ${\mathit{i}o}(P)$ is a function. Furthermore,
${\mathit{i}o}(P)$ is a partial upper closure operator, namely it satisfies:
Extensiveness: If $(s,s^{\prime})\in{\mathit{i}o}(P)$ then $s\leq s^{\prime}$.
Idempotence: If $(s,s^{\prime})\in{\mathit{i}o}(P)$ then
$(s^{\prime},s^{\prime})\in{\mathit{i}o}(P)$.

Moreover, if $P$ is monotonic, then:

Monotonicity: If $(s_{1},s_{1}^{\prime})\in{\mathit{i}o}(P)$,
$(s_{2},s_{2}^{\prime})\in{\mathit{i}o}(P)$ and $s_{1}\leq s_{2}$, then
$s_{1}^{\prime}\leq s_{2}^{\prime}$.

A pleasant property of closure operators is that they are uniquely determined
by their set of fixpoints, here called the _strongest postcondition_.

######  Definition 8 (Strongest Postcondition)

Given a utcc process $P$, the strongest postcondition of $P$, denoted by
${\mathit{s}p}(P)$, is defined as the set
$\\{s\in\mathcal{C}^{\omega}\cup\mathcal{C}^{*}\ |\
(s,s)\in{\mathit{i}o}(P)\\}$.

Intuitively, $s\in{\mathit{s}p}(P)$ iff $P$ under input $s$ cannot add any
information whatsoever, i.e. $s$ is a quiescent sequence for $P$. We can also
think of ${\mathit{s}p}(P)$ as the set of sequences that $P$ can output under
the influence of an arbitrary environment. Therefore, proving whether $P$
satisfies a given property $A$, in the presence of any environment, reduces to
proving whether ${\mathit{s}p}(P)$ is a subset of the set of sequences
(outputs) satisfying the property $A$. Recall that
$\mathit{i}o(P)=\mathit{i}o^{\mathit{f}in}(P)\cup\mathit{i}o^{\mathit{i}nf}(P)$.
Therefore, the sequences in ${\mathit{s}p}(P)$ can be finite or infinite.

We conclude here by showing that for the monotonic fragment, the input-output
behavior can be retrieved from the strongest postcondition. The proof of this
result follows straightforward from Lemma 2 and it can be found in A.

###### Theorem 2

Let $min$ be the minimum function w.r.t. the order induced by $\leq$ and $P$
be a monotonic process. Then, $(s,s^{\prime})\in{\mathit{i}o}(P)\mbox{\ \ iff\
\ }s^{\prime}=min({\mathit{s}p}(P)\cap\\{w\ |\ s\leq w\\})$.

##  3 A Denotational model for TCC and UTCC

As we explained before, the strongest postcondition relation fully captures
the behavior of a process considering any possible output under an arbitrary
environment. In this section we develop a denotational model for the strongest
postcondition. The semantics is compositional and it is the basis for the
abstract interpretation framework that we develop in Section 4.

Our semantics is built on the closure operator semantics for ccp and tcc in
[Saraswat et al. (1991), Saraswat et al. (1994)] and [de Boer et al. (1997),
Nielsen et al. (2002a)]. Unlike the denotational semantics for utcc in [Olarte
and Valencia (2008a)], our semantics is more appropriate for the data-flow
analysis due to its simpler domain based on sequences of constraints instead
of sequences of temporal formulas. In Section 6 we elaborate more on the
differences between both semantics.

Roughly speaking, the semantics is based on a continuous immediate consequence
operator $T_{\mathcal{D}}$, which computes in a bottom-up fashion the
_interpretation_ of each process definition $p(\vec{x})\operatorname{:\\!--}P$
in $\mathcal{D}$. Such an interpretation is given in terms of the set of the
quiescent sequences for $p(\vec{x})$.

Assume a utcc program $\mathcal{D}.P$. We shall denote the set of process
names with their formal parameters in $\mathcal{D}$ as ${\mathit{P}rocHeads}$.
We shall call _Interpretations_ the set of functions in the domain
${\mathit{P}rocHeads}\rightarrow{\mathcal{P}}(\mathcal{C}^{\omega})$. We shall
define the semantics as a function
$[\\![\cdot]\\!]_{I}:({\mathit{P}rocHeads}\rightarrow{\mathcal{P}}(\mathcal{C}^{\omega}))\rightarrow({\mathit{P}roc}\rightarrow{\mathcal{P}}(\mathcal{C}^{\omega}))$
which given an interpretation $I$, associates to each process a set of
sequences of constraints.

$\begin{array}[]{llcl}\mathrm{D}_{SKIP}&[\\![\mathbf{skip}]\\!]_{I}&=&\mathcal{C}^{\omega}\\\
\mathrm{D}_{TELL}&[\\![\mathbf{tell}(c)]\\!]_{I}&=&\uparrow\\!\\!c.\mathcal{C}^{\omega}\\\
\mathrm{D}_{ASK}&[\\![\mathbf{when}\ c\ \mathbf{do}\
P]\\!]_{I}&=&\overline{\uparrow\\!\\!c}.\mathcal{C}^{\omega}\ \cup\
(\uparrow\\!\\!c.\mathcal{C}^{\omega}\cap[\\![P]\\!]_{I})\\\
\mathrm{D}_{ABS}&[\\![(\mathbf{abs}\
\vec{x};c)\,P]\\!]_{I}&=&\operatorname{\forall\forall\
\\!}\vec{x}([\\![\mathbf{when}\ c\ \mathbf{do}\ P]\\!]_{I})\\\
\mathrm{D}_{PAR}&[\\![P\parallel
Q]\\!]_{I}&=&[\\![P]\\!]_{I}\cap[\\![Q]\\!]_{I}\\\
\mathrm{D}_{LOC}&[\\![(\mathbf{local}\,\vec{x})\,P]\\!]_{I}&=&\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!]_{I})\\\
{\mathrm{D}_{NEXT}}&[\\![\mathbf{next}\,P]\\!]_{I}&=&\mathcal{C}.[\\![P]\\!]_{I}\\\
{\mathrm{D}_{UNL}}&[\\![\mathbf{unless}\ c\
\mathbf{next}\,P]\\!]_{I}&=&\overline{\uparrow\\!\\!c}.[\\![P]\\!]_{I}\ \cup\
\uparrow\\!\\!c.\mathcal{C}^{\omega}\\\
\mathrm{D}_{CALL}&[\\![{p(\vec{t})}]\\!]_{I}&=&I(p(\vec{t}))\end{array}$

Figure 2: Semantic Equations for tcc and utcc constructs. Operands “.”,
$\uparrow\\!\\!$ , $\operatorname{\forall\forall\ \\!}$ and $\
\operatorname{\exists\exists\ \\!}$ are defined in Notation 5. $\overline{A}$
denotes the set complement of $A$ in $\mathcal{C}^{\omega}$.

Before defining the semantics, we introduce the following notation.

######  Notation 5 (Closures and Operators on Sequences)

Given a constraint $c$, we shall use $\uparrow\\!\\!c$ (the upward closure) to
denote the set $\\{d\in\mathcal{C}\ |\ d\vdash c\\}$, i.e., the set of
constraints entailing $c$. Similarly, we shall use $\uparrow\\!\\!s$ to denote
the set of sequences $\\{s^{\prime}\in\mathcal{C}^{\omega}\ |\ s\leq
s^{\prime}\\}$. Given $S\subseteq\mathcal{C}^{\omega}$ and
$\mathcal{C}^{\prime}\subseteq\mathcal{C}$, we shall extend the use of the
sequences-concatenation operator “.” by declaring that $c.S=\\{c.s\ |\ s\in
S\\}$, $\mathcal{C}^{\prime}.s=\\{c.s\ |\ c\in\mathcal{C}^{\prime}\\}$ and
$\mathcal{C}^{\prime}.S=\\{c.s\ |\ c\in\mathcal{C}^{\prime}\mbox{ and }s\in
S\\}$. Furthermore, given a set of sequences of constraints
$S\subseteq\mathcal{C}^{\omega}$, we define:

$\begin{array}[]{lll}\operatorname{\exists\exists\
\\!}\vec{x}(S)&=&\\{s\in\mathcal{C}^{\omega}\ |\ \mbox{ there exists
}s^{\prime}\in S\mbox{ s.t.
}\exists\vec{x}(s)\cong\exists\vec{x}(s^{\prime})\\}\\\
\operatorname{\forall\forall\ \\!}\vec{x}(S)&=&\\{\exists\vec{y}(s)\in S\ |\
\vec{y}\subseteq{\mathit{V}ar},s\in S\mbox{ and for all
}s^{\prime}\in\mathcal{C}^{\omega},\mbox{ if
}\exists\vec{x}(s)\cong\exists\vec{x}(s^{\prime})\mbox{,}\\\
&&\qquad\qquad\quad\ \ d_{\vec{x}\vec{t}}^{\omega}\leq s^{\prime}\mbox{ and
}adm(\vec{x},\vec{t})\mbox{ then }s^{\prime}\in S\\}\end{array}$

The operators above are used to define the semantic equations in Figure 2 and
explained in the following. Recall that $[\\![P]\\!]_{I}$ aims at capturing
the strongest postcondition (or quiescent sequences) of $P$, i.e. those
sequences $s$ such that $P$ under input $s$ cannot add any information
whatsoever. The process $\mathbf{skip}$ cannot add any information to any
sequence and hence, its denotation is $\mathcal{C}^{\omega}$ (Equation
$\mathrm{D}_{SKIP}$). The sequences to which $\mathbf{tell}(c)$ cannot add
information are those whose first element entails $c$, i.e., the upward
closure of $c$ (Equation $\mathrm{D}_{TELL}$). If neither $P$ nor $Q$ can add
any information to $s$, then $s$ is quiescent for $P\parallel Q$. (Equation
$\mathrm{D}_{PAR}$).

We say that $s$ is an ${\vec{x}}$-variant of $s^{\prime}$ if
$\exists\vec{x}(s)\cong\exists\vec{x}(s^{\prime})$, i.e., $s$ and $s^{\prime}$
differ only on the information about $\vec{x}$. Let
$S=\operatorname{\exists\exists\ \\!}\vec{x}(S^{\prime})$. We note that $s\in
S$ if there is an $\vec{x}$-variant $s^{\prime}$ of $s$ in $S^{\prime}$.
Therefore, a sequence $s$ is quiescent for $Q=(\mathbf{local}\,\vec{x})\,P$ if
there exists an $\vec{x}$-variant $s^{\prime}$ of $s$ s.t. $s^{\prime}$ is
quiescent for $P$. Hence, if $P$ cannot add any information to $s^{\prime}$
then $Q$ cannot add any information to $s$ (Equation $\mathrm{D}_{LOC}$).

The process $\mathbf{next}\,P$ has no influence on the first element of a
sequence. Hence if $s$ is quiescent for $P$ then $c.s$ is quiescent for
$\mathbf{next}\,P$ for any $c\in\mathcal{C}$ (Equation $\mathrm{D}_{NEXT}$).
Recall that the process $Q=\mathbf{unless}\ c\ \mathbf{next}\,P$ executes $P$
in the next time interval if and only if the guard $c$ cannot be deduced from
the store in the current time-unit. Then, a sequence $d.s$ is quiescent for
$Q$ if either $s$ is quiescent for $P$ or $d$ entails $c$ (Equation
$\mathrm{D}_{UNL}$). This equation can be equivalently written as
$\mathcal{C}.[\\![P]\\!]_{I}\ \cup\ \uparrow\\!\\!c.\mathcal{C}^{\omega}$.

Recall that the interpretation $I$ maps process names to sequences of
constraints. Then, the meaning of $p(\vec{t})$ is directly given by the
interpretation $I$ (Rule $\mathrm{D}_{CALL}$).

Let $Q=\mathbf{when}\ c\ \mathbf{do}\ P$. A sequence $d.s$ is quiescent for
$Q$ if $d$ does not entail $c$. If $d$ entails $c$, then $d.s$ must be
quiescent for $P$ (rule $\mathrm{D}_{ASK}$). In some cases, for the sake of
presentation, we may write this equations as:

$[\\![\mathbf{when}\ c\ \mathbf{do}\ P]\\!]_{I}=\\{d.s\ |\ \mbox{ if }d\vdash
c\mbox{ then }d.s\in[\\![P]\\!]_{I}\\}$

Before explaining the Rule $\mathrm{D}_{ABS}$, let us show some properties of
$\operatorname{\forall\forall\ \\!}\vec{x}(\cdot)$. First, we note that the
$\vec{x}$-variables satisfying the condition $d_{\vec{x}\vec{t}}^{\omega}\leq
s$ in the definition of $\operatorname{\forall\forall\ \\!}$ are equivalent
(see the proof in B).

######  Observation 1 (Equality and $\vec{x}$-variants)

Let $S\subseteq\mathcal{C}^{\omega}$, $\vec{z}\subseteq{\mathit{V}ar}$ and
$s,w\in\mathcal{C}^{\omega}$ be $\vec{x}$-variants such that
$d_{\vec{x}\vec{t}}^{\omega}\leq s$, $d_{\vec{x}\vec{t}}^{\omega}\leq w$ and
$adm(\vec{x},\vec{t})$. (1) $s\cong w$. (2)
$\exists\vec{z}(s)\in\operatorname{\forall\forall\ \\!}\vec{x}(S)$ iff
$s\in\operatorname{\forall\forall\ \\!}\vec{x}(S)$.

Now we establish the correspondence between the sets
$\operatorname{\forall\forall\ \\!}\vec{x}([\\![P]\\!]_{I})$ and
$[\\![P[\vec{t}/\vec{x}]]\\!]_{I}$ which is fundamental to understand the way
we defined the operator $\operatorname{\forall\forall\ \\!}$.

###### Proposition 1

$s\in\operatorname{\forall\forall\ \\!}\vec{x}([\\![P]\\!]_{I})$ if and only
if $s\in[\\![P[\vec{t}/\vec{x}]]\\!]_{I}$ for all admissible substitution
$[\vec{t}/\vec{x}]$.

######  Proof 3.3.

($\Rightarrow$)Let $s\in\operatorname{\forall\forall\
\\!}\vec{x}([\\![P]\\!]_{I})$ and $s^{\prime}$ be an $\vec{x}$-variant of $s$
s.t. $d_{\vec{x}\vec{t}}^{\omega}\leq s^{\prime}$ where
$adm(\vec{x},\vec{t})$. By definition of $\operatorname{\forall\forall\ \\!}$,
we know that $s^{\prime}\in[\\![P]\\!]_{I}$. Since
$d_{\vec{x}\vec{t}}^{\omega}\leq s^{\prime}$ then
$s^{\prime}\in[\\![P]\\!]_{I}\cap\uparrow\\!\\!(d_{\vec{x}\vec{t}}^{\omega})$.
Hence $s\in\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!]_{I}\cap\uparrow\\!\\!(d_{\vec{x}\vec{t}}^{\omega}))$
and we conclude $s\in[\\![P[\vec{t}/\vec{x}]]\\!]_{I}$.

($\Leftarrow$) Let $[\vec{t}/\vec{x}]$ be an admissible substitution. Suppose,
to obtain a contradiction, that $s\in[\\![P[\vec{t}/\vec{x}]]\\!]_{I}$, there
exists $s^{\prime}$ $\vec{x}$-variant of $s$ s.t.
$d_{\vec{x}\vec{t}}^{\omega}\leq s^{\prime}$ and
$s^{\prime}\notin[\\![P]\\!]_{I}$ (i.e., $s\notin\operatorname{\forall\forall\
\\!}\vec{x}([\\![P]\\!]_{I})$). Since $s\in[\\![P[\vec{t}/\vec{x}]]\\!]_{I}$
then $s\in\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!]_{I}\cap\uparrow\\!\\!d_{\vec{x}\vec{t}}^{\omega})$.
Therefore, there exists $s^{\prime\prime}$ $\vec{x}$-variant of $s$ s.t.
$s^{\prime\prime}\in[\\![P]\\!]_{I}$ and $d_{\vec{x}\vec{t}}^{\omega}\leq
s^{\prime\prime}$. By Observation 1, $s^{\prime}\cong s^{\prime\prime}$ and
thus, $s^{\prime}\in[\\![P]\\!]_{I}$, a contradiction.

A sequence $d.s$ is quiescent for the process $Q=(\mathbf{abs}\ x;c)\,P$ if
for all admissible substitution $[\vec{t}/\vec{x}]$, either $d\not\vdash
c[\vec{t}/\vec{x}]$ or $d.s$ is also quiescent for $P[\vec{t}/\vec{x}]$, i.e.,
$d.s\in\operatorname{\forall\forall\ \\!}\vec{x}([\\![(\mathbf{when}\ c\
\mathbf{do}\ P)]\\!]_{I})$ (rule $\mathrm{D}_{ABS}$). Notice that we can
simply write Equation $\mathrm{D}_{ABS}$ by unfolding the definition of
$\mathrm{D}_{ASK}$ as follows:

$[\\![(\mathbf{abs}\ \vec{x};c)\,P]\\!]_{I}=\operatorname{\forall\forall\
\\!}\vec{x}(\overline{\uparrow\\!\\!c}.\mathcal{C}^{\omega}\ \cup\
(\uparrow\\!\\!c.\mathcal{C}^{\omega}\cap[\\![P]\\!]_{I}))$

The reader may wonder why the operator $\operatorname{\forall\forall\ \\!}$
(resp. Rule $\mathrm{D}_{ABS}$) is not entirely dual w.r.t.
$\operatorname{\exists\exists\ \\!}$ (resp. Rule $\mathrm{D}_{LOC}$), i.e.,
why we only consider $\vec{x}$-variants entailing $d_{\vec{x}\vec{t}}$ where
$[\vec{t}/\vec{x}]$ is an admissible substitution. To explain this issue, let
$Q=(\mathbf{abs}\ x;c)\,P$ where $c=\operatorname{\textup{{out}}}{(x)}$ and
$P=\mathbf{tell}(\operatorname{\textup{{out}}}^{\prime}(x))$. We know that

$s=(\operatorname{\textup{{out}}}(a)\wedge\operatorname{\textup{{out}}}^{\prime}(a)).\operatorname{\textup{{t}}}^{\omega}\in{\mathit{s}p}(Q)$

for a given constant $a$. Suppose that we were to define:

$[\\![Q]\\!]_{I}={\ \\{s\ |\ \mbox{for all $x$-variant $s^{\prime}$ of $s$ if
}s^{\prime}(1)\vdash c\mbox{ then }s^{\prime}\in[\\![P]\\!]_{I}\\}}$

Let
$c^{\prime}=\operatorname{\textup{{out}}}(a)\wedge\operatorname{\textup{{out}}}^{\prime}(a)\wedge\operatorname{\textup{{out}}}(x)$
and $s^{\prime}=c^{\prime}.\operatorname{\textup{{t}}}^{\omega}$. Notice that
$s^{\prime}$ is an $x$-variant of $s$, $s^{\prime}(1)\vdash c$ but
$s^{\prime}\notin[\\![P]\\!]_{I}$ (since
$c^{\prime}\not\vdash\operatorname{\textup{{out}}}^{\prime}(x)$). Then
$s\notin[\\![Q]\\!]_{I}$ under this naive definition of $[\\![Q]\\!]_{I}$. We
thus consider only the $\vec{x}$-variants $s^{\prime}$ s.t. each element of
$s^{\prime}$ entails $d_{\vec{x}\vec{t}}$. Intuitively, this condition
requires that $s^{\prime}(1)\vdash c\sqcup d_{\vec{x}\vec{t}}$ in Equation
$\mathrm{D}_{ABS}$ and hence that $s^{\prime}(1)\vdash c[\vec{t}/\vec{x}]$.
Furthermore $s\in[\\![P[\vec{t}/\vec{x}]]\\!]_{I}$ realizes the operational
intuition that $P$ runs under the substitution $[\vec{t}/\vec{x}]$. The
operational rule $\mathrm{R}_{STRVAR}$ makes also echo in the design of our
semantics: the operator $\operatorname{\forall\forall\ \\!}$ considers
constraints of the form $\exists\vec{z}(s)$ where $\vec{z}$ is a (possibly
empty) set of variables, thus allowing us to open the existentially quantified
constraints as shown in the following example.

######  Example 3.4 (Scope extrusion).

Let $P=\mathbf{when}\ \operatorname{\textup{{out}}}(x)\ \mathbf{do}\
\mathbf{tell}(\operatorname{\textup{{out}}}^{\prime}(x))$, $Q=(\mathbf{abs}\
\vec{x};\operatorname{\textup{{out}}}(x))\,\mathbf{tell}(\operatorname{\textup{{out}}}^{\prime}(x))$.
We know that $[\\![Q]\\!]_{I}=\operatorname{\forall\forall\
\\!}x([\\![P]\\!]_{I})$. Assume that $d.s\in[\\![P]\\!]_{I}$. Then, $d$ must
be in the set:

$C=\\{\exists
x(\operatorname{\textup{{out}}}(x)),\operatorname{\textup{{out}}}(x)\sqcup\operatorname{\textup{{out}}}^{\prime}(x),\exists
x(\operatorname{\textup{{out}}}(x)\sqcup\operatorname{\textup{{out}}}^{\prime}(x)),\operatorname{\textup{{out}}}(y),\operatorname{\textup{{out}}}(y)\sqcup\operatorname{\textup{{out}}}^{\prime}(y)\cdots\\}$

where either, $d\not\vdash\operatorname{\textup{{out}}}(x)$ or
$d\vdash\operatorname{\textup{{out}}}^{\prime}(x)$. We note that: (1)
$(\exists x(\operatorname{\textup{{out}}}(x))).s\notin[\\![Q]\\!]_{I}$ since
$\operatorname{\textup{{out}}}(x)\not\in C$. Similarly, $\exists
y(\operatorname{\textup{{out}}}(y)).s\notin[\\![Q]\\!]_{I}$ since
$\operatorname{\textup{{out}}}(y)\in C$ but the $x$-variant
$\operatorname{\textup{{out}}}(x)\sqcup d_{xy}\not\in C$ (it does not entail
$\operatorname{\textup{{out}}}^{\prime}(x)$). (3)
$\operatorname{\textup{{out}}}(y).s\not\in[\\![P]\\!]_{I}$ for the same
reason. (4) Let
$e=(\operatorname{\textup{{out}}}(x)\sqcup\operatorname{\textup{{out}}}^{\prime}(x))$.
We note that $e.s\in[\\![Q]\\!]_{I}$ since $e\in C$ and there is not an
admissible substitution $[t/x]$ s.t. $\exists x(e)\cong\exists x(e[t/x])$. (5)
Let
$e=(\operatorname{\textup{{out}}}(y)\sqcup\operatorname{\textup{{out}}}^{\prime}(y))$.
Then, $e.s\in[\\![Q]\\!]_{I}$ since $e\in C$ and the $x$-variant $e\sqcup
d_{xy}\in C$. (6) Finally, if $e=\exists
x(\operatorname{\textup{{out}}}(x)\sqcup\operatorname{\textup{{out}}}^{\prime}(x)).s$,
then $e.s\in[\\![Q]\\!]_{I}$ as in (4) and (5).

###  3.1 Compositional Semantics

We choose as semantic domain $\mathbb{E}=(E,\sqsubseteq^{c})$ where $E=\\{X\
|\ X\in\mathcal{P}(\mathcal{C}^{\omega})\mbox{ and
}\operatorname{\textup{{f}}}^{\omega}\in X\\}$ and $X\sqsubseteq^{c}Y$ iff
$X\supseteq Y$. The bottom of $\mathbb{E}$ is then $\mathcal{C}^{\omega}$ (the
set of all the sequences) and the top element is the singleton
$\\{\operatorname{\textup{{f}}}^{\omega}\\}$ (recall that
$\operatorname{\textup{{f}}}$ is the greatest element in
($\mathcal{C},\leq$)). Given two interpretations $I_{1}$ and $I_{2}$, we write
$I_{1}\sqsubseteq^{c}I_{2}$ iff for all $p$,
$I_{1}(p)\sqsubseteq^{c}I_{2}(p)$.

######  Definition 3.5 (Concrete Semantics).

Let $[\\![\cdot]\\!]_{I}$ be defined as in Figure 2. The semantics of a
program $\mathcal{D}.P$ is the least fixpoint of the continuous operator:

$\begin{array}[]{lll}T_{\mathcal{D}}(I)(p(\vec{t}))=[\\![Q[\vec{t}/\vec{x}]]\\!]_{I}\mbox{
if }p(\vec{x})\operatorname{:\\!--}Q\in\mathcal{D}\end{array}$

We shall use $[\\![P]\\!]$ to represent
$[\\![P]\\!]_{\mathit{l}fp(T_{\mathcal{D}})}$.

In the following we prove some fundamental properties of the semantic operator
$T_{\mathcal{D}}$, namely, monotonicity and continuity. Before that, we shall
show that $\operatorname{\forall\forall\ \\!}$ is a closure operator and it is
continuous on the domain $\mathbb{E}$.

######  Lemma 3.6 (Properties of $\operatorname{\forall\forall\ \\!}$).

$\operatorname{\forall\forall\ \\!}$ is a closure operator, i.e., it satisfies
(1) Extensivity: $S\sqsubseteq^{c}\operatorname{\forall\forall\
\\!}\vec{x}(S)$; (2) Idempotency: $\operatorname{\forall\forall\
\\!}\vec{x}(\operatorname{\forall\forall\
\\!}\vec{x}(S))=\operatorname{\forall\forall\ \\!}\vec{x}(S)$; and (3)
Monotonicity: If $S\sqsubseteq^{c}S^{\prime}$ then
$\operatorname{\forall\forall\
\\!}\vec{x}(S)\sqsubseteq^{c}\operatorname{\forall\forall\
\\!}\vec{x}(S^{\prime})$. Furthermore, (4) $\operatorname{\forall\forall\
\\!}$ is continuous on $(E,\sqsubseteq^{c})$.

######  Proof 3.7.

The proofs of (1),(2) and (3) are straightforward from the definition of
$\operatorname{\forall\forall\ \\!}\vec{x}$. The proof of (4) proceeds as
follows. Assume a non-empty ascending chain
$S_{1}\sqsubseteq^{c}S_{2}\sqsubseteq^{c}S_{3}\sqsubseteq^{c}...$. Lubs in $E$
correspond to set intersection. We shall prove that
$\bigcap\operatorname{\forall\forall\
\\!}\vec{x}(S_{i})=\operatorname{\forall\forall\ \\!}\vec{x}(\bigcap S_{i})$.
The “$\subseteq$” part (i.e., $\sqsupseteq^{c}$) is trivial since
$\operatorname{\forall\forall\ \\!}$ is monotonic. As for the
$\bigcap\operatorname{\forall\forall\
\\!}\vec{x}(S_{i})\subseteq\operatorname{\forall\forall\ \\!}\vec{x}(\bigcap
S_{i})$ part, by extensiveness we know that $\operatorname{\forall\forall\
\\!}\vec{x}(S_{i})\subseteq S_{i}$ for all $S_{i}$ and then,
$\bigcap\operatorname{\forall\forall\ \\!}\vec{x}(S_{i})\subseteq\bigcap
S_{i}$. Let $s\in\bigcap\operatorname{\forall\forall\ \\!}\vec{x}(S_{i})$. By
definition we know that $s$ and all $\vec{x}$-variant $s^{\prime}$ of $s$
satisfying $d_{\vec{x}\vec{t}}^{\omega}\leq s^{\prime}$ for
$adm(\vec{x},\vec{t})$ belong to $\bigcap\operatorname{\forall\forall\
\\!}\vec{x}(S_{i})$ and then in $\bigcap S_{i}$. Hence,
$s\in\operatorname{\forall\forall\ \\!}\vec{x}(\bigcap S_{i})$ and we conclude
$\bigcap\operatorname{\forall\forall\
\\!}\vec{x}(S_{i})\subseteq\operatorname{\forall\forall\ \\!}\vec{x}(\bigcap
S_{i})$.

######  Proposition 3.8 (Monotonicity of $[\\![\cdot]\\!]$ and continuity of
$T_{\mathcal{D}}$).

Let $P$ be a process and $I_{1}\sqsubseteq^{c}I_{2}\sqsubseteq^{c}I_{3}...$ be
an ascending chain. Then,
$[\\![P]\\!]_{I_{i}}\sqsubseteq^{c}[\\![P]\\!]_{I_{i+1}}$ (Monotonicity).
Moreover,
$[\\![P]\\!]_{\bigsqcup_{I_{i}}}=\bigsqcup_{I_{i}}[\\![P]\\!]_{I_{i}}$
(Continuity).

######  Proof 3.9.

Monotonicity follows easily by induction on the structure of $P$ and it
implies the the “$\sqsupseteq^{c}$” part of continuity. As for the part
“$\sqsubseteq^{c}$” we proceed by induction on the structure of $P$. The
interesting cases are those of the local and the abstraction operator. For
$P=(\mathbf{local}\,\vec{x})\,Q$, by inductive hypothesis we know that
$[\\![Q]\\!]_{\bigsqcup_{I_{i}}}\sqsubseteq^{c}\bigsqcup_{I_{i}}[\\![Q]\\!]_{I_{i}}$.
Since $\exists$ (and therefore $\operatorname{\exists\exists\ \\!}$) is
continuous (see Property (5) in Definition 1), we conclude
$\operatorname{\exists\exists\
\\!}_{\vec{x}}([\\![Q]\\!]_{\bigsqcup_{I_{i}}})\sqsubseteq^{c}\bigsqcup_{I_{i}}\operatorname{\exists\exists\
\\!}_{\vec{x}}([\\![Q]\\!]_{I_{i}})$. The result for $P=(\mathbf{abs}\
\vec{x};c)\,Q$ follows similarly from the continuity of
$\operatorname{\forall\forall\ \\!}$ (Lemma 3.6).

$\begin{array}[]{lll}I_{1}\
:&p\to\uparrow\\!\\!\operatorname{\textup{{out}}}_{a}(x).\mathcal{C}^{\omega}\
\cap\
\mathcal{C}.\uparrow\\!\\!\operatorname{\textup{{out}}}_{a}(y).\mathcal{C}^{\omega}\mbox{
i.e.,
}p\to\uparrow\\!\\!\operatorname{\textup{{out}}}_{a}(x).\uparrow\\!\\!\operatorname{\textup{{out}}}_{a}(y).\mathcal{C}^{\omega}\\\
&q\to\operatorname{\forall\forall\ \\!}z(A.\mathcal{C}^{\omega})\cap\
\mathcal{C}.I_{\bot}(q)\mbox{ i.e., }q\to\operatorname{\forall\forall\
\\!}z(A).I_{\bot}(q)\\\
&r\to\mathcal{C}^{\omega}\cap\mathcal{C}^{\omega}=\mathcal{C}^{\omega}\\\
I_{2}\ :&p\to I_{1}(p)\\\ &q\to\operatorname{\forall\forall\
\\!}z(A.\mathcal{C}^{\omega})\cap\ \mathcal{C}.I_{1}(q)\mbox{ i.e.,
}q\to\operatorname{\forall\forall\ \\!}z(A).\operatorname{\forall\forall\
\\!}z(A.\mathcal{C}^{\omega})\cap\
\mathcal{C}.\mathcal{C}.\mathcal{C}^{\omega}\\\ &r\to I_{1}(p)\cap I_{1}(q)\\\
\dots\\\ I_{\omega}:&p\to I_{1}(p)\\\ &q\to\operatorname{\forall\forall\
\\!}z(A).\operatorname{\forall\forall\ \\!}z(A).\operatorname{\forall\forall\
\\!}z(A)...\\\ &r\to I_{\omega}(p)\cap I_{\omega}(q)\end{array}$

Figure 3: Semantics of the processes in Example 3.10.
$A_{1}=\uparrow\\!\\!(\operatorname{\textup{{out}}}_{a}(z)\sqcup\operatorname{\textup{{out}}}_{b}(z))$,
$A_{2}=\overline{\uparrow\\!\\!\operatorname{\textup{{out}}}_{a}(z)}$ and
$A=A_{1}\cup A_{2}$. We abuse of the notation and we write
$\operatorname{\forall\forall\ \\!}z(A).S$ instead of
$\operatorname{\forall\forall\
\\!}z(A.\mathcal{C}^{\omega})\cap\mathcal{C}.S$.

######  Example 3.10 (Computing the semantics).

Assume two constraints $\operatorname{\textup{{out}}}_{a}(\cdot)$ and
$\operatorname{\textup{{out}}}_{b}(\cdot)$, intuitively representing outputs
of names on two different channels $a$ and $b$. Let $\mathcal{D}$ be the
following procedure definitions

$\begin{array}[]{lll}\mathcal{D}&=&p()\operatorname{:\\!--}\
\mathbf{tell}(\operatorname{\textup{{out}}}_{a}(x))\parallel\mathbf{next}\,\mathbf{tell}(\operatorname{\textup{{out}}}_{a}(y))\\\
&&q()\operatorname{:\\!--}\ (\mathbf{abs}\
z;\operatorname{\textup{{out}}}_{a}(z))\,(\mathbf{tell}(\operatorname{\textup{{out}}}_{b}(z)))\parallel\mathbf{next}\,q()\\\
&&r()\operatorname{:\\!--}\ p()\parallel q()\end{array}$

The procedure $p()$ outputs on channel $a$ the variables $x$ and $y$ in the
first and second time-units respectively. The procedure $q()$ resends on
channel $b$ every message received on channel $a$. The computation of
$[\\![r()]\\!]$ can be found in Figure 3. Let $s\in[\\![r()]\\!]$. Then, it
must be the case that $s\in[\\![p()]\\!]$ and then,
$s(1)\vdash\operatorname{\textup{{out}}}_{a}(x)$ and
$s(2)\vdash\operatorname{\textup{{out}}}_{a}(y)$. Since $r\in[\\![q()]\\!]$,
for $i\geq 1$, if $s(i)\vdash\operatorname{\textup{{out}}}_{a}(t)$ then
$s(i)\vdash\operatorname{\textup{{out}}}_{b}(t)$ for any term $t$. Hence,
$s(1)\vdash\operatorname{\textup{{out}}}_{b}(x)$ and
$s(2)\vdash\operatorname{\textup{{out}}}_{b}(y)$.

###  3.2 Semantic Correspondence

In this section we prove the soundness and completeness of the semantics.

######  Lemma 3.11 (Soundness).

Let $[\\![\cdot]\\!]$ be as in Definition 3.5. If
$P\stackrel{{\scriptstyle\,\,(d,d^{\prime})\,\,}}{{\,\,===\Longrightarrow}}{R}$
and $d\cong d^{\prime}$, then $d.[\\![R]\\!]\subseteq[\\![P]\\!]$.

######  Proof 3.12.

Assume that
$\langle\vec{x};P;d\rangle\longrightarrow^{*}\langle\vec{x}^{\prime};P^{\prime};d^{\prime}\rangle\not\longrightarrow$,
$\exists\vec{x}(d)\cong\exists\vec{x}^{\prime}(d^{\prime})$. We shall prove
that $\exists\vec{x}(d).\operatorname{\exists\exists\
\\!}\vec{x}^{\prime}([\\![F(P^{\prime}))]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!])$. We proceed by induction on the lexicographical
order on the length of the internal derivation and the structure of $P$, where
the predominant component is the length of the derivation. We present the
interesting cases. The others can be found in B.

Case $P=Q\parallel S$. Assume a derivation for $Q=Q_{1}$ and $S=S_{1}$ of the
form

$\begin{array}[]{lll}\langle\vec{z};Q\parallel
S,d\rangle&\longrightarrow^{*}&\langle\vec{z}\cup\vec{x}_{1}\cup\vec{y}_{1};Q_{1}\parallel
S_{1},c_{1}\sqcup e_{1}\rangle\\\
&\longrightarrow^{*}&\langle\vec{z}\cup\vec{x}_{i}\cup\vec{y}_{j};Q_{i}\parallel
S_{j},c_{i}\sqcup e_{j}\rangle\\\
&\longrightarrow^{*}&\langle\vec{z}\cup\vec{x}_{m}\cup\vec{y}_{n};Q_{m}\parallel
S_{n};c_{m}\sqcup e_{n}\rangle\not\longrightarrow\end{array}$

such that for $i>0$, each $Q_{i+1}$ (resp. $S_{i+1}$) is an evolution of
$Q_{i}$ (resp. $S_{i}$); $\vec{x}_{i}$ (resp. $\vec{y}_{j}$) are the variables
added by $Q$ (resp. $S$); and $c_{i}$ (resp $e_{j}$) is the information added
by $Q$ (resp. $S$). We assume by alpha-conversion that
$\vec{x}_{m}\cap\vec{y}_{n}=\emptyset$. We know that
$\exists\vec{z}(d)\cong\exists\vec{z},\vec{x}_{m},\vec{y}_{n}(c_{m}\sqcup
e_{n})$ and from $\mathrm{R}_{PAR}$ we can derive:

$\begin{array}[]{lll}\langle\vec{z}\cup\vec{y}_{n};Q;d\sqcup
e_{n}\rangle&\longrightarrow^{*}\equiv&\langle\vec{z}\cup\vec{x}_{m}\cup\vec{y}_{n};Q_{m},c_{m}\sqcup
e_{n}\rangle\not\longrightarrow\mbox{\ \ \ and \ \ \ }\\\
\langle\vec{z}\cup\vec{x}_{m};S;d\sqcup
c_{m}\rangle&\longrightarrow^{*}\equiv&\langle\vec{z}\cup\vec{x}_{m}\cup\vec{y}_{n};S_{n},c_{m}\sqcup
e_{n}\rangle\not\longrightarrow\end{array}$

By (structural) inductive hypothesis, we know that
$\exists\vec{z},\vec{y}_{n}(d\sqcup e_{n}).\operatorname{\exists\exists\
\\!}\vec{z},\vec{x}_{m},\vec{y}_{n}[\\![F(Q_{m})]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{z},\vec{y}_{n}([\\![Q]\\!]$) and also
$\exists\vec{z},\vec{x}_{m}(d\sqcup c_{m}).\operatorname{\exists\exists\
\\!}\vec{z},\vec{y}_{n},\vec{x}_{m}[\\![F(S_{n})]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{z},\vec{x}_{m}([\\![S]\\!])$. We note that
$\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!]\cap[\\![Q]\\!])=\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!])\cap[\\![Q]\\!]$ if
$\vec{x}\cap{\mathit{f}v}(Q)=\emptyset$ (see Proposition D.58 in D). Hence,
from the fact that
$\vec{x}_{m}\cap{\mathit{f}v}(S_{n})=\vec{y}_{n}\cap{\mathit{f}v}(Q_{m})=\emptyset$,
we conclude:

$\exists\vec{z}(d).\operatorname{\exists\exists\
\\!}\vec{z},\vec{x}_{m},\vec{y}_{n}([\\![F(Q_{m})]\\!]\cap[\\![F(S_{n})]\\!])\subseteq\operatorname{\exists\exists\
\\!}\vec{z}([\\![Q]\\!]\cap[\\![S]\\!])$

Case $P=(\mathbf{abs}\ \vec{x};c)\,Q$. From the rule $\mathrm{R}_{ABS}$, we
can show that

$\begin{array}[]{ll}\langle\vec{y};P;d\rangle&\longrightarrow^{*}\langle\vec{y}_{1};P_{1}\parallel
Q_{1}^{1}[\vec{t_{1}}/\vec{x}];d_{1}\rangle\\\
&\longrightarrow^{*}\langle\vec{y}_{2};P_{2}\parallel
Q_{1}^{2}[\vec{t_{1}}/\vec{x}]\parallel
Q_{2}^{1}[\vec{t_{2}}/\vec{x}];d_{2}\rangle\\\
&\longrightarrow^{*}\langle\vec{y}_{3};P_{3}\parallel
Q_{1}^{3}[\vec{t_{1}}/\vec{x}]\parallel
Q_{2}^{2}[\vec{t_{2}}/\vec{x}]\parallel
Q_{3}^{1}[\vec{t_{3}}/\vec{x}];d_{3}\rangle\\\ &\longrightarrow^{*}\cdots\\\
&\longrightarrow^{*}\langle\vec{y}_{n};P_{n}\parallel
Q_{1}^{m_{1}}[\vec{t_{1}}/\vec{x}]\parallel
Q_{2}^{m_{2}}[\vec{t_{2}}/\vec{x}]\parallel
Q_{3}^{m_{3}}[\vec{t_{3}}/\vec{x}]\parallel\cdots\parallel
Q_{n}^{m_{n}}[\vec{t_{n}}/\vec{x}];d_{n}\rangle\end{array}$

where $P_{n}$ takes the form $(\mathbf{abs}\ \vec{x};c;E_{n})\,Q$,
$E_{n}=\\{d_{\vec{x}\vec{t_{1}}},...,d_{\vec{x}\vec{t_{n}}}\\}$ and
$\exists\vec{y}(d)\cong\exists\vec{y}_{n}(d_{n})$. Hence, there is a
derivation (shorter than that for $P$) for each $d_{\vec{x}\vec{t_{i}}}\in
E_{n}$:

$\langle\vec{y}_{i};Q_{i}^{1}[\vec{t_{i}}/\vec{x}];d_{i}\rangle\longrightarrow^{*}\equiv\langle\vec{y}_{i}^{\prime};Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}];d_{i}^{\prime}\rangle\not\longrightarrow$

with $Q[\vec{t_{i}}/\vec{x}]=Q^{1}_{i}[\vec{t_{i}}/\vec{x}]$ and
$\exists\vec{y}_{i}(d_{i})\cong\exists\vec{y}_{i}^{\prime}(d_{i}^{\prime})$.
Therefore, by inductive hypothesis,

$\exists\vec{y}_{i}(d_{i}).\operatorname{\exists\exists\
\\!}\vec{y}_{i}^{\prime}[\\![F(Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}])]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{y_{i}}[\\![Q[\vec{t_{i}}/\vec{x}]]\\!]$

for all $d_{\vec{x}\vec{t_{i}}}\in E_{n}$. We assume, by alpha conversion,
that the variables added for each $Q_{i}^{j}$ are distinct and then, their
intersection is empty. Furthermore, we note that
$\exists\vec{y}(d)\cong\exists\vec{y}_{1}(d_{1})$. Since
$F(P_{n})=\mathbf{skip}$, we then conclude:

$\exists\vec{y}(d).\operatorname{\exists\exists\
\\!}\vec{y}_{n}[\\![F(P_{n}\parallel\prod\limits_{d_{\vec{x}\vec{t_{i}}}\in
E_{n}}Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}])]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{y}[\\![\prod\limits_{d_{\vec{x}\vec{t_{i}}}\in
E_{n}}Q[\vec{t_{i}}/\vec{x}])]\\!]$

Let $d.s\in\operatorname{\exists\exists\
\\!}\vec{y}[\\![\prod\limits_{d_{\vec{x}\vec{t_{i}}}\in
E_{n}}Q[\vec{t_{i}}/\vec{x}])]\\!]$. For an admissible $d_{\vec{x}\vec{t}}$,
either $d\not\vdash c[\vec{t}/\vec{x}]$ or $d\vdash c[\vec{t}/\vec{x}]$. In
the first case, trivially $d.s\in[\\![(\mathbf{when}\ c\ \mathbf{do}\
Q)[\vec{t}/\vec{x}]]\\!]$. In the second case, $E_{n}\Vdash
d_{\vec{x}\vec{t}}$. Hence, $d.s\in[\\![Q[\vec{t}/\vec{x}]]\\!]$ and
$d.s\in[\\![(\mathbf{when}\ c\ \mathbf{do}\ Q)[\vec{t}/\vec{x}]]\\!]$. Here we
conclude that for all admissible $[\vec{t}/\vec{x}]$,
$d.s\in[\\![(\mathbf{when}\ c\ \mathbf{do}\ Q)[\vec{t}/\vec{x}]]\\!]$ and by
Proposition 1 we derive:

$\exists\vec{y}(d).\operatorname{\exists\exists\
\\!}\vec{y}[\\![F(\prod\limits_{d_{\vec{x}\vec{t_{i}}}\in
E_{n}}Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}])]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{y}\operatorname{\forall\forall\ \\!}\vec{x}[\\![(\mathbf{when}\ c\
\mathbf{do}\ Q)]\\!]$

Case $P=p(\vec{t})$. Assume that $p(\vec{x}):-Q\in\mathcal{D}$. We can verify
that

$\langle\vec{y};p(\vec{t});d\rangle\longrightarrow\langle\vec{y};Q[\vec{t}/\vec{x}];d\rangle\longrightarrow^{*}\langle\vec{y}^{\prime};Q^{\prime};d^{\prime}\rangle\not\longrightarrow$

where $\exists\vec{y}^{\prime}(d^{\prime})\cong\exists\vec{y}(d)$. By
induction $\exists\vec{y}(d).\operatorname{\exists\exists\
\\!}\vec{y}^{\prime}[\\![F(Q^{\prime})]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{y}[\\![Q[\vec{t}/\vec{x}]]\\!]$ and we conclude
$\exists\vec{y}(d).\operatorname{\exists\exists\
\\!}\vec{y}[\\![F(Q^{\prime})]\\!]\subseteq\operatorname{\exists\exists\
\\!}\vec{y}[\\![p(\vec{t})]\\!]$.

The previous lemma allows us to prove the soundness of the semantics.

######  Theorem 3.13 (Soundness).

If $s\in{\mathit{s}p}(P)$ then there exists $s^{\prime}$ s.t.
$s.s^{\prime}\in[\\![P]\\!]$.

######  Proof 3.14.

If $P$ is well-terminated under input $s$, let $s^{\prime}=\epsilon$. By
repeated applications of Lemma 3.11, $s\in[\\![P]\\!]$. If $P$ is not well-
terminated, then $s$ is finite and let
$s^{\prime}=\operatorname{\textup{{f}}}^{\omega}$ (recall that
$\operatorname{\textup{{f}}}^{\omega}$ is quiescent for any process). Via
Lemma 3.11 we can show $s.s^{\prime}\in[\\![P]\\!]$.

Moreover, the semantics approximates any infinite computation.

######  Corollary 3.15 (Infinite Computations).

Assume that $d.s\in\operatorname{\exists\exists\
\\!}\vec{x}_{1}([\\![P_{1}]\\!]\cap\uparrow\\!\\!(c_{1}.\mathcal{C}^{\omega}))$
and that
$\left\langle{\vec{x}_{1};P_{1};c_{1}}\right\rangle\longrightarrow^{*}\left\langle{\vec{x}_{i};P_{i};c_{i}}\right\rangle\longrightarrow^{*}\left\langle{\vec{x}_{n};P_{n};c_{n}}\right\rangle\longrightarrow^{*}\cdots.$
Then, $\bigsqcup\exists\vec{x}_{i}(c_{i})\leq d$.

######  Proof 3.16.

Recall that procedure calls must be next guarded. Then, any infinite behavior
in $P_{1}$ is due to a process of the form $(\mathbf{abs}\ \vec{x};c)\,Q$ that
executes $Q[\vec{t}_{i}/\vec{x}]$ and adds new information of the form
$e[\vec{t}_{i}/\vec{x}]$. By an analysis similar to that of Lemma 3.11, we can
show that $d$ entails $e[\vec{t}_{i}/\vec{x}]$.

######  Example 3.17 (Infinite behavior).

Let $P=(\mathbf{abs}\
z;\operatorname{\textup{{out}}}(z))\,(\mathbf{local}\,x)\,(\mathbf{tell}(\operatorname{\textup{{out}}}(x)))$
and let $c=\operatorname{\textup{{out}}}(w)$. Starting from the store $c$, the
process $P$ engages in infinitely many internal transitions of the form

$\begin{array}[]{c}\left\langle{\emptyset;P;c}\right\rangle\longrightarrow^{*}\left\langle{\\{x_{1},\cdots,x_{i}\\};P_{i};\operatorname{\textup{{out}}}(x_{1})\sqcup\cdots\sqcup\operatorname{\textup{{out}}}(x_{i})\sqcup\operatorname{\textup{{out}}}(w)}\right\rangle\longrightarrow^{*}\\\
\left\langle{\\{x_{1},\cdots,x_{i},\cdots,x_{n}\\};P_{n};\operatorname{\textup{{out}}}(x_{1})\sqcup\cdots\sqcup\operatorname{\textup{{out}}}(x_{n})\sqcup\operatorname{\textup{{out}}}(w)}\right\rangle\longrightarrow^{*}\cdots\end{array}$

At any step of the computation, the observable store is
$\operatorname{\textup{{out}}}(w)\sqcup\bigsqcup\limits_{i\in 1..n}\exists
x_{i}\operatorname{\textup{{out}}}(x_{i})$ which is equivalent to
$\operatorname{\textup{{out}}}(w)$. Note also that
$\operatorname{\textup{{out}}}(w).\mathcal{C}^{\omega}\in[\\![P]\\!]$.

For the converse of Theorem 3.13, we have similar technical problems as in the
case of tcc, namely: the combination of the $\mathbf{local}$ operator with the
$\mathbf{unless}$ constructor. Thus, similarly to tcc, completeness is
verified only for the fragment of utcc where there are no occurrences of
$\mathbf{unless}$ processes in the body of $\mathbf{local}$ processes. The
reader may refer [de Boer et al. (1995), Nielsen et al. (2002a)] for
counterexamples showing that $[\\![P]\\!]\not\subseteq{\mathit{s}p}(P)$ when
$P$ is not locally independent.

######  Definition 3.18 (Locally Independent Fragment).

Let $\mathcal{D}.P$ be a program where $\mathcal{D}$ contains process
definitions of the form $p_{i}(\vec{x})\operatorname{:\\!--}P_{i}$. We say
that $\mathcal{D}.P$ is locally independent if for each process of the form
$(\mathbf{local}\,\vec{x};c)\,Q$ in $P$ and $P_{i}$ it holds that (1) $Q$ does
not have occurrences of $\mathbf{unless}$ processes; and (2) if $Q$ calls to
$p_{j}(\vec{x})$, then $P_{j}$ satisfies also conditions (1) and (2).

######  Lemma 3.19 (Completeness).

Let $\mathcal{D}.P$ be a locally independent program s.t. $d.s\in[\\![P]\\!]$.
If
$P\stackrel{{\scriptstyle\,\,(d,d^{\prime})\,\,}}{{\,\,===\Longrightarrow}}R$
then $d^{\prime}\cong d$ and $s\in[\\![R]\\!]$.

######  Proof 3.20.

Assume that $P$ is locally independent, $d.s\in[\\![P]\\!]$ and there is a
derivation of the form
$\langle\vec{x};P;d\rangle\longrightarrow^{*}\langle\vec{x}^{\prime};P^{\prime};d^{\prime}\rangle\not\longrightarrow$.
We shall prove that
$\exists\vec{x}(d)\cong\exists\vec{x}^{\prime}(d^{\prime})$ and
$s\in\operatorname{\exists\exists\
\\!}\vec{x}^{\prime}[\\![F(P^{\prime})]\\!]$. We proceed by induction on the
lexicographical order on the length of the internal derivation
($\longrightarrow^{*}$) and the structure of $P$, where the predominant
component is the length of the derivation. The locally independent condition
is used for the case $P=(\mathbf{local}\,\vec{x};c)\,Q$. We only present the
interesting cases. The others can be found in B.

Case $P=Q\parallel S$. We know that $d.s\in[\\![Q]\\!]$ and
$d.s\in[\\![S]\\!]$ and by (structural) inductive hypothesis, there are
derivations
$\langle\vec{z};Q;d\rangle\longrightarrow^{*}\langle\vec{z}\cup\vec{x}^{\prime};Q^{\prime};d^{\prime}\sqcup
c\rangle\ \not\longrightarrow$ and
$\langle\vec{z};S;d\rangle\longrightarrow^{*}\langle\vec{z}\cup\vec{y}^{\prime};S^{\prime};d^{\prime\prime}\sqcup
e\rangle\ \not\longrightarrow$ s.t. $s\in\operatorname{\exists\exists\
\\!}\vec{z},\vec{x}^{\prime}[\\![F(Q^{\prime})]\\!]$,
$s\in\operatorname{\exists\exists\
\\!}\vec{z},\vec{y}^{\prime}[\\![F(S^{\prime})]\\!]$,
$\exists\vec{z}(d)\cong\exists\vec{z},\vec{x}^{\prime}(d^{\prime}\sqcup c)$
and
$\exists\vec{z}(d)\cong\exists\vec{z},\vec{y}^{\prime}(d^{\prime\prime}\sqcup
e)$. Therefore, assuming by alpha conversion that
$\vec{x}^{\prime}\cap\vec{y}^{\prime}=\emptyset$,
$\exists\vec{z}(d)\cong\exists\vec{z},\vec{x}^{\prime},\vec{y}^{\prime}(d^{\prime}\sqcup
d^{\prime\prime}\sqcup c\sqcup e)$ and by rule $\mathrm{R}_{PAR}$,

$\langle\vec{z};Q\parallel
S,d\rangle\longrightarrow^{*}\equiv\langle\vec{z}\cup\vec{x}^{\prime}\cup\vec{y}^{\prime};Q^{\prime}\parallel
S^{\prime};d^{\prime}\sqcup d^{\prime\prime}\sqcup c\sqcup
e\rangle\not\longrightarrow$

We note that $\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!]\cap[\\![Q]\\!])=\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!])\cap[\\![Q]\\!]$ if
$\vec{x}\cap{\mathit{f}v}(Q)=\emptyset$ (see Proposition D.58 in D). Since
$F(Q^{\prime}\parallel S^{\prime})=F(Q^{\prime})\parallel F(S^{\prime})$ and
$\vec{x}^{\prime}\cap{\mathit{f}v}(S^{\prime})=\vec{y}^{\prime}\cap{\mathit{f}v}(Q^{\prime})=\emptyset$,
we conclude $s\in\operatorname{\exists\exists\
\\!}\vec{z},\vec{x}^{\prime},\vec{y}^{\prime}([\\![F(Q^{\prime}\parallel
R^{\prime})]\\!])$.

Case $P=(\mathbf{abs}\ \vec{x};c)\,Q$. By using the rule $\mathrm{R}_{ABS}$ we
can show that:

$\begin{array}[]{ll}\langle\vec{x};P;d\rangle&\longrightarrow^{*}\langle\vec{y}_{1};P_{1}\parallel
Q_{1}^{1}[\vec{t_{1}}/\vec{x}];d_{1}^{1}\rangle\\\
&\longrightarrow^{*}\langle\vec{y}_{2};P_{2}\parallel
Q_{1}^{2}[\vec{t_{1}}/\vec{x}]\parallel
Q_{2}^{1}[\vec{t_{2}}/\vec{x}];d_{1}^{2}\sqcup d_{2}^{1}\rangle\\\
&\longrightarrow^{*}\langle\vec{y}_{3};P_{3}\parallel
Q_{1}^{3}[\vec{t_{1}}/\vec{x}]\parallel
Q_{2}^{2}[\vec{t_{2}}/\vec{x}]\parallel
Q_{3}^{1}[\vec{t_{3}}/\vec{x}];d_{1}^{3}\sqcup d_{2}^{2}\sqcup
d_{3}^{1}\rangle\\\ &\longrightarrow^{*}\cdots\\\
&\longrightarrow^{*}\langle\vec{y}_{n};P_{n}\parallel
Q_{1}^{m_{1}}[\vec{t_{1}}/\vec{x}]\parallel\cdots\parallel
Q_{n}^{m_{n}}[\vec{t_{n}}/\vec{x}];d_{1}^{m_{1}}\sqcup...\sqcup
d_{n}^{m_{n}}\rangle\end{array}$

where $P_{n}$ takes the form $(\mathbf{abs}\ \vec{x};c;E_{n})\,Q$ and
$E_{n}=\\{d_{\vec{x}\vec{t_{1}}},...,d_{\vec{x}\vec{t_{n}}}\\}$. In the
derivation above, $d_{i}^{j}$ represents the constraint added by
$Q_{i}^{j}[\vec{t_{i}}/\vec{x}]$. Note that
$Q[\vec{t_{i}}/\vec{x}]=Q_{i}^{1}[\vec{t_{i}}/\vec{x}]$. There is a derivation
(shorter than that for $P$) for each $d_{\vec{x}\vec{t_{i}}}\in E_{n}$ of the
form

$\langle\vec{y}_{i};Q_{i}^{1}[\vec{t_{i}}/\vec{x}];d_{i}\rangle\longrightarrow^{*}\equiv\langle\vec{y}_{i}^{\prime};Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}];d_{i}^{m_{i}}\rangle\not\longrightarrow$

Since $d.s\in[\\![P]\\!]$, by Proposition 1 we know that
$d.s\in[\\![Q_{i}^{1}[\vec{t_{i}}/\vec{x}]]\\!]$ and by induction,
$\exists\vec{y}_{i}(d_{i})\cong\exists\vec{y}_{i}^{\prime}(d_{i}^{m_{i}})$.
Furthermore, it must be the case that $s\in\operatorname{\exists\exists\
\\!}\vec{y}_{i}^{\prime}[\\![F(Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}])]\\!]$. Let
$e$ be the constraint $\exists\vec{y}_{n}(d_{1}^{m_{1}}\sqcup...\sqcup
d_{n}^{m_{n}})$. Given that
$\exists\vec{y}_{i}(d_{i})\cong\exists\vec{y}_{i}^{\prime}(d_{i}^{m_{i}})$, we
have $\exists\vec{x}(d)\cong e$. Furthermore, given that
$F(P_{n})=\mathbf{skip}$:

$(\mathbf{abs}\
\vec{x};c)\,Q\stackrel{{\scriptstyle\,\,(d,e)\,\,}}{{\,\,===\Longrightarrow}}(\mathbf{local}\,\vec{y}_{n})\,F\left(\prod\limits_{d_{\vec{x}\vec{t_{i}}}\in
E_{n}}Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}]\right)$

Since $s\in\operatorname{\exists\exists\
\\!}\vec{y}_{i}^{\prime}[\\![F(Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}])]\\!]$ for
all $d_{\vec{x}\vec{t}_{i}}\in E_{n}$, we conclude

$s\in\operatorname{\exists\exists\
\\!}\vec{y}_{n}[\\![F(\prod\limits_{d_{\vec{x}\vec{t_{i}}}\in
E_{n}}Q_{i}^{m_{i}}[\vec{t_{i}}/\vec{x}])]\\!]$

Case $P=(\mathbf{local}\,\vec{x})\,Q$. By alpha conversion assume
$\vec{x}\not\in{\mathit{f}v}(d.s)$. We know that there exists
$d^{\prime}.s^{\prime}$ ($\vec{x}$-variant of $d.s$) s.t.
$d^{\prime}.s^{\prime}\in[\\![Q]\\!]$, $\exists\vec{x}(d.s)\cong d.s$ and
$d.s\cong\exists\vec{x}(d^{\prime}.s^{\prime})$. By (structural) inductive
hypothesis, there is a derivation
$\langle\vec{y};Q;d^{\prime}\rangle\longrightarrow^{*}\langle\vec{y}^{\prime};Q^{\prime};d^{\prime\prime}\rangle\not\longrightarrow$
and $\exists\vec{y}(d^{\prime})\cong\exists\vec{y}^{\prime}(d^{\prime\prime})$
and $s^{\prime}\in\operatorname{\exists\exists\
\\!}\vec{y}^{\prime}[\\![F(Q^{\prime})]\\!]$. We assume by alpha conversion
that $\vec{x}\cap\vec{y}=\emptyset$. Consider now the following derivation:

$\langle\vec{y};(\mathbf{local}\,\vec{x})\,Q;d\rangle\longrightarrow\langle\vec{x}\cup\vec{y};Q;d\rangle\longrightarrow^{*}\langle\vec{y}^{\prime\prime};Q^{\prime\prime},c\rangle\not\longrightarrow$

where $\vec{x}\cup\vec{y}\subseteq\vec{y}^{\prime\prime}$. We know that
$d^{\prime}\vdash d$ and by monotonicity, we have
$\exists\vec{y}^{\prime}(d^{\prime\prime})\vdash\exists\vec{y}^{\prime\prime}(c)$
and then, $d^{\prime}\vdash\exists\vec{y}^{\prime\prime}(c)$. We then conclude
$\exists\vec{y}(d)\vdash\exists\vec{y}^{\prime\prime}(c)$.

Since $s^{\prime}\in\operatorname{\exists\exists\
\\!}\vec{y}^{\prime}[\\![F(Q^{\prime})]\\!]$ then
$s\in\operatorname{\exists\exists\ \\!}\vec{x}\operatorname{\exists\exists\
\\!}\vec{y}^{\prime}[\\![F(Q^{\prime})]\\!]$. Nevertheless, notice that in the
above derivation of $(\mathbf{local}\,\vec{x})\,Q$, the final process is
$Q^{\prime\prime}$ and not $Q^{\prime}$. Since $Q$ is monotonic, there are no
$\mathbf{unless}$ processes in it. Furthermore, since $d^{\prime}\vdash d$, it
must be the case that $Q^{\prime}$ may contain sub-terms (in parallel
composition) of the form $R^{\prime}[\vec{t}/\vec{x}]$ resulting from a
process of the form $(\mathbf{abs}\ \vec{y};e)\,R$ s.t.
$d^{\prime\prime}\vdash e[\vec{t}/\vec{x}]$ and $c\not\vdash
e[\vec{t}/\vec{x}]$. Therefore, by Rule $\mathrm{D}_{PAR}$, it must be also
the case that $s^{\prime}\in[\\![F(Q^{\prime\prime})]\\!]$ and then,
$s\in\operatorname{\exists\exists\
\\!}\vec{x},\vec{y}^{\prime}[\\![{F(Q^{\prime\prime})}]\\!]$. Finally, note
that $\vec{y}^{\prime\prime}$ is not necessarily equal to $\vec{y}^{\prime}$.
With a similar analysis we can show that in $Q^{\prime}$ there are possibly
more $\mathbf{local}$ processes running in parallel than in $Q^{\prime\prime}$
and then, $s\in\operatorname{\exists\exists\
\\!}\vec{y}^{\prime\prime}[\\![{F(Q^{\prime\prime})}]\\!]$.

By repeated applications of the previous Lemma, we show the completeness of
the denotation with respect to the strongest postcondition relation.

######  Theorem 3.21 (Completeness).

Let $\mathcal{D}.P$ be a locally independent program, $w=s_{1}.s_{1}^{\prime}$
and $w\in[\\![P]\\!]$. If
$P\stackrel{{\scriptstyle\,\,(s_{1},s_{1}^{\prime})\,\,}}{{\,\,===\Longrightarrow}}$
then $s_{1}\cong s_{1}^{\prime}$. Furthermore, if
$P\stackrel{{\scriptstyle\,\,(w,w^{\prime})\,\,}}{{\,\,===\Longrightarrow}}_{\omega}$
then $w\cong w^{\prime}$.

Notice that completeness of the semantics holds only for the locally
independent fragment, while soundness is achieved for the whole language. For
the abstract interpretation framework we develop in the next section, we
require the semantics to be a sound approximation of the operational semantics
and then, the restriction imposed for completeness does not affect the
applicability of the framework.

##  4 Abstract Interpretation Framework

In this section we develop an abstract interpretation framework [Cousot and
Cousot (1992)] for the analysis of utcc (and tcc) programs. The framework is
based on the above denotational semantics, thus allowing for a compositional
analysis. The abstraction proceeds as a composition of two different
abstractions: (1) we abstract the constraint system and then (2) we abstract
the infinite sequences of _abstract_ constraints. The abstraction in (1)
allows us to reuse the most popular abstract domains previously defined for
logic programming. Adapting those domains, it is possible to perform, e.g.,
groundness, freeness, type and suspension analyses of utcc programs. On the
other hand, the abstraction in (2) along with (1) allows for computing the
approximated output of the program in a finite number of steps.

###  4.1 Abstract Constraint Systems

Let us recall some notions from [Falaschi et al. (1997a)] and [Zaffanella et
al. (1997)].

######  Definition 4.22 (Descriptions).

A description $(\mathcal{C},\alpha,\mathcal{A})$ between two constraint
systems

$\begin{array}[]{lll}{\mathbf{C}}&=&\langle\mathcal{C},\leq\
,\sqcup,\operatorname{\textup{{t}}},\operatorname{\textup{{f}}},{\mathit{V}ar},\exists,D\rangle\\\
{\mathbf{A}}&=&\langle\mathcal{A},\leq^{\alpha},\sqcup^{\alpha},\operatorname{\textup{{t}}}^{\alpha},\operatorname{\textup{{f}}}^{\alpha},{\mathit{V}ar},\exists^{\alpha},D^{\alpha}\rangle\end{array}$

consists of an abstract domain $(\mathcal{A},\leq^{\alpha})$ and a surjective
and monotonic abstraction function $\alpha:\mathcal{C}\to\mathcal{A}$. We lift
$\alpha$ to sequences of constraints in the obvious way.

We shall use $c_{\alpha}$, $d_{\alpha}$ to range over constraints in
${\mathcal{A}}$ and
$s_{\alpha},s^{\prime}_{\alpha},w_{\alpha},w^{\prime}_{\alpha},$ to range over
sequences in $\mathcal{A}^{*}$ and $\mathcal{A}^{\omega}$ (the set of finite
and infinite sequences of constraints in $\mathcal{A}$). To simplify the
notation, we omit the subindex “$\alpha$” when no confusion arises. The
entailment $\vdash^{\alpha}$ is defined as in the concrete counterpart, i.e.
$c_{\alpha}\leq^{\alpha}d_{\alpha}$ iff $d_{\alpha}\vdash^{\alpha}c_{\alpha}$.
Similarly, $d_{\alpha}\cong_{\alpha}c_{\alpha}$ iff
$d_{\alpha}\vdash^{\alpha}c_{\alpha}$ and
$c_{\alpha}\vdash^{\alpha}d_{\alpha}$.

Following standard lines in [Giacobazzi et al. (1995), Falaschi et al.
(1997a), Zaffanella et al. (1997)] we impose the following restrictions over
$\alpha$ relating the cylindrification, diagonal and $lub$ operators of
${\mathbf{C}}$ and ${\mathbf{A}}$.

######  Definition 4.23 (Correctness).

Let $\alpha:\mathcal{C}\to\mathcal{A}$ be monotonic and surjective. We say
that ${\mathbf{A}}$ is _upper correct_ w.r.t. the constraint system
${\mathbf{C}}$ if for all $c\in\mathcal{C}$ and $x,y\in Var$:

(1)
$\alpha(\exists\vec{x}(c))\cong_{\alpha}\exists^{\alpha}\vec{x}(\alpha(c))$.

(2) $\alpha(d_{\vec{x}\vec{t}})\cong_{\alpha}d^{\alpha}_{\vec{x}\vec{t}}$.

Since $\alpha$ is monotonic, we also have $\alpha(c\sqcup
d)\vdash^{\alpha}\alpha(c)\sqcup^{\alpha}\alpha(d)$.

In the example below we illustrate an abstract domain for the groundness
analysis of tcc programs. Here we give just an intuitive description of it. We
shall elaborate more on this domain and its applications in Section 5.2.

######  Example 4.24 (Constraint System for Groundness).

Let the concrete constraint system ${\mathbf{C}}$ be the Herbrand constraint
system. As abstract constraint system A, let constraints be propositional
formulas representing groundness information as in $x\wedge(y\leftrightarrow
z)$ that means, $x$ is a ground variable and, $y$ is ground iff $z$ is ground.
In this setting, $\alpha(x=[a])=x$ (i.e., $x$ is a ground variable).
Furthermore, $\alpha(x=[a|y])=x\leftrightarrow y$ meaning $x$ is ground if and
only if $y$ is ground.

In the following definition we make precise the idea when an abstract
constraint approximates a concrete one.

######  Definition 4.25 (Approximations).

Let $(\mathcal{C},\alpha,\mathcal{A})$ be a description satisfying the
conditions in Definition 4.22. Given $d_{\alpha}=\alpha(d)$, we say that
$d_{\alpha}$ is the best approximation of $d$. Furthermore, for all
$c_{\alpha}\leq^{\alpha}d_{\alpha}$ we say that $c_{\alpha}$ approximates $d$
and we write $c_{\alpha}\propto d$. This definition is pointwise extended to
sequences of constraints in the obvious way (see Figure 4a).

(a)  (b)

Figure 4: (a). $c^{\prime}_{\alpha}$ approximates $c$ (i.e.,
$c^{\prime}_{\alpha}\propto c$) and $c_{\alpha}=\alpha(c)$ is the best
approximation of $c$ (Definition 4.25). Since $\alpha$ is monotonic and $c\leq
d$, $c_{\alpha}\leq^{\alpha}d_{\alpha}$. In (b), assume that for all $d$ s.t.
$d\not\vdash c$, $d$ is not approximated by $c_{\alpha}$. Then, all constraint
$c^{\prime}$ approximated by $c_{\alpha}$ (the upper cone of $c$) entails $c$.
In this case, $c_{\alpha}\vdash_{\mathcal{A}}c$ (Definition 4.26).

###  4.2 Abstract Semantics

Now we define an abstract semantics that approximates the observable behavior
of a program and is adequate for modular data-flow analysis. The semantic
equations are given in Figure 5 and they are parametric on the abstraction
function $\alpha$ of the description $(\mathcal{C},\alpha,\mathcal{A})$. We
shall dwell a little upon the description of the rules $\mathrm{A}_{ASK}$ and
$\mathrm{A}_{UNL}$. The other cases are self-explanatory.

$\begin{array}[]{llcl}\mathrm{A}_{SKIP}&[\\![\mathbf{skip}]\\!]^{\alpha}_{X}&=&\mathcal{A}^{\omega}\\\
\mathrm{A}_{TELL}&[\\![\mathbf{tell}(c)]\\!]^{\alpha}_{X}&=&\uparrow\\!\\!(\alpha(c)).\mathcal{A}^{\omega}\\\
\mathrm{A}_{ASK}&[\\![\mathbf{when}\ c\ \mathbf{do}\
P]\\!]^{\alpha}_{X}&=&\overline{\Uparrow\\!\\!c}.\mathcal{A}^{\omega}\cup(\Uparrow\\!\\!c.\mathcal{A}^{\omega}\cap[\\![P]\\!]^{\alpha}_{X})\\\
\mathrm{A}_{ABS}&[\\![(\mathbf{abs}\
\vec{x};c)\,P]\\!]^{\alpha}_{X}&=&\operatorname{\forall\forall\
\\!}\vec{x}([\\![\mathbf{when}\ c\ \mathbf{do}\ P]\\!]^{\alpha}_{X})\\\
\mathrm{A}_{PAR}&[\\![P\parallel
Q]\\!]^{\alpha}_{X}&=&[\\![P]\\!]^{\alpha}_{X}\cap[\\![Q]\\!]^{\alpha}_{X}\\\
\mathrm{A}_{LOC}&[\\![(\mathbf{local}\,\vec{x})\,P]\\!]^{\alpha}_{X}&=&\operatorname{\exists\exists\
\\!}\vec{x}([\\![P]\\!]^{\alpha}_{X})\\\
\mathrm{A}_{NEXT}&[\\![\mathbf{next}\,P]\\!]^{\alpha}_{X}&=&\mathcal{A}.[\\![P]\\!]^{\alpha}_{X}\\\
\mathrm{A}_{UNL}&[\\![\mathbf{unless}\ c\
\mathbf{next}\,P]\\!]^{\alpha}_{X}&=&\mathcal{A}^{\omega}\\\
\mathrm{A}_{CALL}&[\\![p(\vec{t})]\\!]^{\alpha}_{X}&=&X(p(\vec{t}))\end{array}$

Figure 5: Abstract denotational semantics for utcc. $\vdash_{\mathcal{A}}$ and
$\Uparrow\\!\\!$ are in Definition 4.26. $\overline{A}$ denotes the set
complement of $A$.

Given the right abstraction of the synchronization mechanism of blocking asks
in ccp is crucial to give a safe approximation of the behavior of programs. In
abstract interpretation, abstract elements are _weaker_ than the concrete
ones. Hence, if we approximate the behavior of $\mathbf{when}\ c\ \mathbf{do}\
P$ by replacing the guard $c$ with $\alpha(c)$, it could be the case that $P$
proceeds in the abstract semantics but it does not in the concrete one. More
precisely, let $d,c\in\mathcal{C}$. Notice that from
$\alpha(d)\vdash^{\alpha}\alpha(c)$ we cannot, in general, conclude $d\vdash
c$. Take for instance the constraint systems in Example 4.24. We know that
$\alpha(x=a)\cong^{\alpha}\alpha(x=b)$ but $x=a\not\vdash x=b$. Assume now we
were to define the abstract semantics of ask processes as:

$[\\![\mathbf{when}\ c\ \mathbf{do}\
Q]\\!]^{\alpha}_{X}=\overline{\uparrow(\alpha(c))}.\mathcal{A}^{\omega}\cup(\uparrow(\alpha(c)).\mathcal{A}^{\omega}\cap[\\![Q]\\!]^{\alpha}_{X})$
(1)

A correct analysis of the process $P=\mathbf{tell}(x=a)\parallel\mathbf{when}\
x=b\ \mathbf{do}\ \mathbf{tell}(y=b)$ should conclude that only $x$ is
definitely ground. Since $\alpha(x=a)\vdash^{\alpha}\alpha(x=b)$, if we use
Equation 1, the analysis ends with the result $(x\wedge
y).\mathcal{A}^{\omega}$, i.e., it wrongly concludes that $x$ and $y$ are
definitely ground.

We thus follow [Zaffanella et al. (1997), Falaschi et al. (1993), Falaschi et
al. (1997a)] for the abstract semantics of the ask operator. For this, we need
to define the entailment $\vdash_{\mathcal{A}}$ that relates constraints in
$\mathcal{A}$ and $\mathcal{C}$.

######  Definition 4.26 ($\vdash_{\mathcal{A}}$ relation).

Let $d_{\alpha}\in\mathcal{A}$ and $c\in\mathcal{C}$. We say that $d_{\alpha}$
entails $c$, notation $d_{\alpha}\vdash_{\mathcal{A}}c$, if for all
$c^{\prime}\in\mathcal{C}$ s.t. $d_{\alpha}\propto c^{\prime}$ it holds that
$c^{\prime}\vdash c$. We shall use $\Uparrow\\!\\!c$ to denote the set
$\\{d_{\alpha}\in\mathcal{A}\ |\ d_{\alpha}\vdash_{\mathcal{A}}c\\}$.

In words, the (abstract) constraint $d_{\alpha}$ entails the (concrete)
constraint $c$ if all constraints approximated by $d_{\alpha}$ entail $c$ (see
Figure 4b). Then, in Equation $\mathrm{A}_{ASK}$, we guarantee that if the
abstract computation proceeds (i.e., $d_{\alpha}\vdash_{\mathcal{A}}c$) then
every concrete computation it approximates proceeds too.

In Equations $\mathrm{D}_{ABS}$ and $\mathrm{D}_{LOC}$ we use the operators
$\operatorname{\forall\forall\ \\!}$ and $\operatorname{\exists\exists\ \\!}$
analogous to those in Notation 5. In this context, they are defined on
sequences of constraints in $\mathcal{A}^{\omega}$ and they use the elements
$\exists^{\alpha}$, $\sqcup^{\alpha}$ and $d^{\alpha}_{\vec{x}\vec{t}}$
instead of their concrete counterparts:

$\begin{array}[]{lll}\operatorname{\exists\exists\
\\!}\vec{x}(S_{\alpha})&=&\\{s_{\alpha}\in\mathcal{A}^{\omega}\ |\ \mbox{
there exists }s^{\prime}_{\alpha}\in S_{\alpha}\mbox{ s.t.
}\exists^{\alpha}\vec{x}(s_{\alpha})\cong_{\alpha}\exists^{\alpha}\vec{x}(s^{\prime}_{\alpha})\\}\\\
\operatorname{\forall\forall\
\\!}\vec{x}(S_{\alpha})&=&\\{\exists^{\alpha}\vec{y}(s_{\alpha})\in
S_{\alpha}\ |\ \vec{y}\subseteq{\mathit{V}ar},s_{\alpha}\in S_{\alpha}\mbox{
and for all }s^{\prime}_{\alpha}\in\mathcal{A}^{\omega},\\\ &&\quad\ \mbox{ if
}\exists^{\alpha}\vec{x}(s_{\alpha})\cong\exists^{\alpha}\vec{x}(s^{\prime}_{\alpha})\mbox{,}(d_{\vec{x}\vec{t}}^{\alpha})^{\omega}\leq
s_{\alpha}^{\prime}\mbox{ and }adm(\vec{x},\vec{t})\mbox{ then
}s^{\prime}_{\alpha}\in S_{\alpha}\\}\end{array}$

We omitted the superindex “$\alpha$” in these operators since it can be easily
inferred from the context.

The abstract semantics of the $\mathbf{unless}$ operator poses similar
difficulties as in the case of the ask operator. Moreover, even if we make use
of the entailment $\vdash_{\mathcal{A}}$ in Definition 4.26, we do not obtain
a safe approximation. Let us explain this. One could think of defining the
semantic equation for the unless process as follows:

$[\\![\mathbf{unless}\ c\
\mathbf{next}\,Q]\\!]^{\alpha}_{X}=\overline{\Uparrow\\!\\!c}.[\\![Q]\\!]^{\alpha}_{X}\cup\Uparrow\\!\\!c.\mathcal{A}^{\omega}$
(2)

The problem here is that $\alpha(d)\not\vdash_{\mathcal{A}}c$ does not imply,
in general, $d\not\vdash c$. Take for instance $\alpha$ in Example 4.24. We
know that $x\not\vdash_{\mathcal{A}}x=[a]$ and $x=[a]\vdash x=[a]$. Now let
$Q=\mathbf{unless}\ c\ \mathbf{next}\,\mathbf{tell}(e)$, $d$ be a constraint
s.t. $d\vdash c$ and $d_{\alpha}=\alpha(d)$. We know by rule
$\mathrm{D}_{UNL}$ that
$d.\operatorname{\textup{{t}}}^{\omega}\in[\\![Q]\\!]$. If
$\alpha(d)\not\vdash_{\mathcal{A}}c$, then by using the Equation (2), we
conclude that
$d_{\alpha}.(\operatorname{\textup{{t}}}^{\alpha})^{\omega}\notin[\\![Q]\\!]^{\alpha}$.
Hence, we have a sequence $s$ such that $s\in[\\![Q]\\!]$ and
$\alpha(s)\not\in[\\![Q]\\!]^{\alpha}$ and the abstract semantics cannot be
shown to be a sound approximation of the concrete semantics (see Theorem
4.31).

Notice that defining $d_{\alpha}\not\vdash_{\mathcal{A}}c$ as true iff
$c^{\prime}\not\vdash c$ for all $c^{\prime}$ approximated by $d_{\alpha}$
does not solve the problem. This is because under this definition,
$d_{\alpha}\not\vdash_{\mathcal{A}}c$ does not hold for any $d_{\alpha}$ and
$c$. To see this, notice that $\operatorname{\textup{{f}}}$ entails all the
concrete constraints and it is approximated by any abstract constraint.
Therefore, we cannot give a better (safe) approximation of the semantics of
$\mathbf{unless}\ c\ \mathbf{next}\,P$ than $\mathcal{A}^{\omega}$ (Rule
$\mathrm{A}_{UNL}$).

Now we can formally define the abstract semantics as we did in Section 3.
Given a description $(\mathcal{C},\alpha,\mathcal{A})$, we choose as abstract
domain is $\mathbb{A}=(A,\sqsubseteq^{\alpha})$ where $A=\\{X\ |\
X\in\mathcal{P}(\mathcal{A}^{\omega})\mbox{ and
}(\operatorname{\textup{{f}}}^{\alpha})^{\omega}\in X\\}$ and
$X\sqsubseteq^{\alpha}Y$ iff $X\supseteq Y$. The bottom and top of this domain
are similar to the concrete domain, i.e., $\mathcal{A}^{\omega}$ and
$\\{(\operatorname{\textup{{f}}}^{\alpha})^{\omega}\\}$ respectively.

######  Definition 4.27.

Let $[\\![\cdot]\\!]^{\alpha}_{X}$ be as in Figure 5. The abstract semantics
of a program $\mathcal{D}.P$ is defined as the least fixpoint of the
continuous semantic operator:

$T^{\alpha}_{\mathcal{D}}(X)(p(\vec{t}))={[\\![(Q[\vec{t}/\vec{x}])]\\!]^{\alpha}_{X}}\mbox{
if }p(\vec{x})\operatorname{:\\!--}Q\in\mathcal{D}$

We shall use $[\\![P]\\!]^{\alpha}$ to denote
$[\\![P]\\!]^{\alpha}_{\mathit{l}fp(T_{\mathcal{D}}^{\alpha})}$.

The following proposition shows the monotonicity of $[\\![\cdot]\\!]^{\alpha}$
and the continuity of $T_{\mathcal{D}}^{\alpha}$. The proof is analogous to
that of Proposition 3.8.

######  Proposition 4.28 (Monotonicity of $[\\![\cdot]\\!]^{\alpha}$ and
Continuity of $T_{\mathcal{D}}^{\alpha}$).

Let $P$ be a process and
$X_{1}\sqsubseteq^{\alpha}X_{2}\sqsubseteq^{\alpha}X_{3}...$ be an ascending
chain. Then,
$[\\![P]\\!]^{\alpha}_{X_{i}}\sqsubseteq^{c}[\\![P]\\!]^{\alpha}_{X_{i+1}}$
(Monotonicity). Moreover,
$[\\![P]\\!]^{\alpha}_{\bigsqcup_{X_{i}}}=\bigsqcup_{X_{i}}[\\![P]\\!]^{\alpha}_{X_{i}}$
(Continuity).

###  4.3 Soundness of the Approximation

This section proves the correctness of the abstract semantics in Definition
4.27. We first establish a Galois insertion between the concrete and the
abstract domains.

######  Proposition 4.29 (Galois Insertion).

Let $(\mathcal{C},\alpha^{\prime},\mathcal{A})$ be a description and
$\mathbb{E}$, $\mathbb{A}$ be the concrete and abstract domains. If
$\mathbf{A}$ is upper correct w.r.t. $\mathbf{C}$ then there exists an upper
Galois insertion $\mathbb{E}\galois{\alpha}{\gamma}\mathbb{A}$.

######  Proof 4.30.

Let $\mathbb{A}=(A,\sqsubseteq^{\alpha})$, $\mathbb{E}=(E,\sqsubseteq^{c})$
and $\alpha:E\to A$ and $\gamma:A\to E$ be defined as follows:

$\begin{array}[]{ll}\alpha(S)&=\\{\beta(s)\ |\ s\in S\\}\mbox{ for }S\in\\{X\
|\ X\in\mathcal{P}(\mathcal{C}^{\omega})\mbox{ and
}\operatorname{\textup{{f}}}^{\omega}\in X\\}\\\ \gamma(S_{\alpha})&=\\{s\ |\
\beta(s)\in S_{\alpha}\\}\mbox{ for }S_{\alpha}\in\\{X\ |\
X\in\mathcal{P}(\mathcal{A}^{\omega})\mbox{ and
}(\operatorname{\textup{{f}}}^{\alpha})^{\omega}\in X\\}\end{array}$

where $\beta$ is the pointwise extension of $\alpha^{\prime}$ over sequences.
Notice that $\beta$ is a monotonic and surjective function between
$\mathcal{C}^{\omega}$ and $\mathcal{A}^{\omega}$ and set intersection is the
lub in both $\mathbb{E}$ and $\mathbb{A}$. We conclude by the fact that any
additive and surjective function between complete lattices defines a Galois
insertion [Cousot and Cousot (1979)].

We lift, as standardly done in abstract interpretations [Cousot and Cousot
(1992)], the approximation induced by the above abstraction. Let
$I:ProcHeads\rightarrow E$, $X:ProcHeads\rightarrow A$, $\beta$ be as in
Proposition 4.29 and $p$ be a process definition. Then

$\begin{array}[]{lll}\alpha(I(p))=\\{\beta(s)\mid s\in
I(p)\\}&&\gamma(X(p))=\\{s\mid\beta(s)\in X(p)\\}\end{array}$

We conclude here by showing that concrete computations are safely approximated
by the abstract semantics.

######  Theorem 4.31 (Soundness of the approximation).

Let $(\mathcal{C},\alpha,\mathcal{A})$ be a description and ${\mathbf{A}}$ be
upper correct w.r.t. $\mathbf{C}$. Given a utcc program $\mathcal{D}.P$, if
$s\in[\\![P]\\!]$ then $\alpha(s)\in[\\![P]\\!]^{\alpha}$.

######  Proof 4.32.

Let $d_{\alpha}.s_{\alpha}=\alpha(d.s)$ and assume that $d.s\in[\\![P]\\!]$.
Then, $d.s\in[\\![P]\\!]_{I}$ where $I$ is the $lfp$ of $T_{\mathcal{D}}$. By
the continuity of $T_{\mathcal{D}}$, there exists $n$ s.t.
$I=T_{\mathcal{D}}^{n}(I_{\bot})$ (the $n$-th application of
$T_{\mathcal{D}}$). We proceed by induction on the lexicographical order on
the pair $n$ and the structure of $P$, where the predominant component is $n$.
We only present the interesting cases. The others can be found in C.

Case $P=(\mathbf{abs}\ \vec{x};c)\,Q$. Let $[\vec{t}/\vec{x}]$ be an
admissible substitution. We shall prove that $s\in[\\![(\mathbf{when}\ c\
\mathbf{do}\ Q)[\vec{t}/\vec{x}]]\\!]$ implies
$s_{\alpha}\in[\\![(\mathbf{when}\ c\ \mathbf{do}\
Q)[\vec{t}/\vec{x}]]\\!]^{\alpha}$. The result follows from Proposition 1 and
from the fact that $s_{\alpha}\in\operatorname{\forall\forall\
\\!}\vec{x}([\\![\mathbf{when}\ c\ \mathbf{do}\ Q]\\!]^{\alpha})$ iff
$s_{\alpha}\in[\\![(\mathbf{when}\ c\ \mathbf{do}\
Q)[\vec{t}/\vec{x}]]\\!]^{\alpha}$ for all $adm(\vec{x},\vec{t})$. The proof
of the previous statement is similar to that of Proposition 1 and it appears
in D.

Assume that $d\vdash c[\vec{t}/\vec{x}]$. Then,
$d.s\in[\\![Q[\vec{t}/\vec{x}]]\\!]$ and we distinguish two cases:

(1) $d_{\alpha}\vdash_{\mathcal{A}}c[\vec{t}/\vec{x}]$. Since
$d.s\in[\\![Q[\vec{t}/\vec{x}]]\\!]$ then $d.s\in\operatorname{\exists\exists\
\\!}\vec{x}([\\![Q]\\!]\cap\uparrow\\!\\!(d_{\vec{x}\vec{t}}^{\omega}))$.
Therefore, there exists $d^{\prime}.s^{\prime}$, an $\vec{x}$-variant of
$d.s$, s.t. $d^{\prime}.s^{\prime}\in[\\![Q]\\!]$ and
$d^{\prime}.s^{\prime}\in\uparrow\\!\\!(d_{\vec{x}\vec{t}}^{\omega})$. By
(structural) inductive hypothesis,
$\alpha(d^{\prime}.s^{\prime})\in[\\![Q]\\!]^{\alpha}$. Furthermore, by
monotonicity of $\alpha$ and Property (2) in Definition 4.23, we derive
$\alpha(d^{\prime}.s^{\prime})\in\uparrow(d^{\alpha}_{\vec{x}\vec{t}})^{\omega}$.
Hence
$\alpha(d^{\prime}.s^{\prime})\in([\\![Q]\\!]^{\alpha}\cap\uparrow\\!\\!((d^{\alpha}_{\vec{x}\vec{t}})^{\omega})$.
Since $\exists\vec{x}(d.s)=\exists\vec{x}(d^{\prime}.s^{\prime})$, by Property
(1) in Definition 4.23, we have
$\exists^{\alpha}\vec{x}(\alpha(d.s))=\exists^{\alpha}\vec{x}(\alpha(d^{\prime}.s^{\prime}))$
(i.e., $\alpha(d^{\prime}.s^{\prime})$ is an $\vec{x}$-variant of
$d_{\alpha}.s_{\alpha}$). Then,
$d_{\alpha}.s_{\alpha}\in\operatorname{\exists\exists\
\\!}\vec{x}([\\![Q]\\!]^{\alpha}\cap\uparrow\\!\\!((d^{\alpha}_{\vec{x}\vec{t}})^{\omega}))$
and we conclude
$d_{\alpha}.s_{\alpha}\in[\\![Q[\vec{t}/\vec{x}]]\\!]^{\alpha}$.

(2) $d_{\alpha}\not\vdash_{\mathcal{A}}c[\vec{t}/\vec{x}]$. Hence trivially
$d_{\alpha}.s_{\alpha}\in[\\![(\mathbf{when}\ c\ \mathbf{do}\
Q)[\vec{t}/\vec{x}]]\\!]^{\alpha}$.

We conclude by noticing that if $d\not\vdash c[\vec{t}/\vec{x}]$ then
$d_{\alpha}\not\vdash_{\mathcal{A}}c[\vec{t}/\vec{x}]$ and therefore
$d_{\alpha}.s_{\alpha}\in[\\![(\mathbf{when}\ c\ \mathbf{do}\
Q)[\vec{t}/\vec{x}]]\\!]^{\alpha}$.

Case $P\operatorname{:\\!--}p(\vec{t})$. Let
$p(\vec{x})\operatorname{:\\!--}Q$ in $\mathcal{D}$ be a process definition.
If $d.s\in[\\![p(\vec{t})]\\!]$ then $d.s\in I(p(\vec{t}))$ (recall that
$I=lfp(T_{\mathcal{D}})$). We know that $d.s\in[\\![Q[\vec{t}/\vec{x}]]\\!]$
and then, $d.s\in[\\![Q[\vec{t}/\vec{x}]]\\!]_{I^{\prime}}$ where
$I^{\prime}=T_{\mathcal{D}}^{m}(I_{\bot})$ with $m<n$. By induction, and
continuity of $T_{\mathcal{D}}^{\alpha}$, we know that
$d_{\alpha}.s_{\alpha}\in[\\![Q[\vec{t}/\vec{x}]]\\!]^{\alpha}$ and then
$d_{\alpha}.s_{\alpha}\in[\\![p(\vec{t})]\\!]^{\alpha}$.

###  4.4 Obtaining a finite analysis

As standard in Abstract Interpretation, it is possible to obtain an analysis
which terminates, by imposing several alternative conditions (see for instance
Chapter 9 in [Cousot and Cousot (1992)]). So, one possibility is to impose
that the abstract domain is noetherian (also called finite ascending chain
condition). Another possibility is to use widening operators, or to find an
abstract domain that guarantees termination after a finite number of steps.
So, our framework allows to use all this classical methodologies. In the
examples that we have developed we shall focus our attention on a special
class of abstract interpretations obtained by defining what we call a
_sequence abstraction_ mapping possibly infinite sequences of (abstract)
constraints into finite ones. Actually we can define these abstractions as
Galois connections.

######  Definition 4.33 ($k$-sequence Abstraction).

A $k$-sequence abstraction is given by the following pair of functions
$(\alpha_{k},\gamma_{k})$, with
$\alpha_{k}:(\mathcal{A}^{\omega},\leq^{\alpha})\rightarrow(\mathcal{A}_{k}^{*},\leq^{\alpha})$,
and
$\gamma_{k}:(\mathcal{A}_{k}^{*},\leq^{\alpha})\rightarrow(\mathcal{A}^{\omega},\leq^{\alpha})$.
As for the function $\alpha_{k}$, we set $\alpha_{k}(s)=s^{\prime}$ where
$s^{\prime}$ has length $k$ and $s^{\prime}(i)=s(i)$ for $i\leq k$. Similarly,
$\gamma_{k}(s^{\prime})=s$ where $s^{\prime}(i)=s(i)$ for $i\leq k$ and
$s^{\prime}(i)=\operatorname{\textup{{t}}}$ for $i>k$.

It is easy to see that, for any $k$, $(\alpha_{k},\gamma_{k})$ defines a
Galois connection between $(\mathcal{A}^{\omega},\leq^{\alpha})$ and
$(\mathcal{A}^{*}_{k},\leq^{\alpha})$. Thus it is possible to use compositions
of Galois connections for obtaining a new abstraction [Cousot and Cousot
(1992)].

If $\mathcal{A}$ in $(\mathcal{C},\alpha,\mathcal{A})$ leads to a Noetherian
abstract domain $\mathbb{A}$, then the abstraction obtained from the
composition of $\alpha$ and any $\alpha_{k}$ above guarantees that the
fixpoint of the abstract semantics can be reached in a finite number of
iterations. Actually the domain that we obtain in this way is given by
sequences cut at length $k$. The number $k$ determines the length of the cut
and hence the precision of the approximation. The bigger $k$ the better the
approximation.

##  5 Applications

This section is devoted to show some applications of the abstract semantics
developed here. We shall describe three specific abstract domains as instances
of our framework: (1) we abstract a constraint system representing
cryptographic primitives. Then we use the abstract semantics to exhibit a
secrecy flaw in a security protocol modeled in utcc. Next, (2) we tailor two
abstract domains from logic programming to perform a groundness and a type
analysis of a tcc program. We then apply this analysis in the verification of
a reactive system in tcc. Finally, (3) we propose an abstract constraint
system for the suspension analysis of tcc programs.

###  5.1 Verification of Security Protocols

The ability of utcc to express mobile behavior, as in Example 2, allows for
the modeling of security protocols. Here we describe an abstraction of a
cryptographic constraint system in order to bound the length of the messages
to be considered in a secrecy analysis. We start by recalling the constraint
system in [Olarte and Valencia (2008b)] whose terms represent the messages
generated by the protocol and cryptographic primitives are represented as
functions over such terms.

######  Definition 5.34 (Cryptographic Constraint System).

Let $\Sigma$ be a signature with constant symbols in
$\mathcal{P}\cup\mathcal{K}$, function symbols $\operatorname{\mathit{enc}}$,
$\operatorname{\mathit{pair}}$, $\operatorname{\mathit{priv}}$ and
$\operatorname{\mathit{pub}}$ and predicates
$\operatorname{\textup{{out}}}(\cdot)$ and
$\operatorname{\textup{{secret}}}(\cdot)$. Constraint in $\mathcal{C}$ are
formulas built from predicates in $\Sigma$, conjunction ($\sqcup$) and
$\exists$.

Intuitively, $\mathcal{P}$ and $\mathcal{K}$ represent respectively the
principal identifiers, e.g. $A,B,\ldots$ and keys $k,k^{\prime}$. We use
$\\{m\\}_{k}$ and $(m_{1},m_{2})$ respectively, for
$\operatorname{\mathit{enc}}(m,k)$ (encryption) and
$\operatorname{\mathit{pair}}(m_{1},m_{2})$ (composition). For the generation
of keys, $\operatorname{\mathit{priv}}(k)$ stands for the private key
associated to the value $k$ and $\operatorname{\mathit{pub}}(k)$ for its
public key.

As standardly done in the verification of security protocols, a Dolev-Yao
attacker [Dolev and Yao (1983)] is presupposed, able to eavesdrop,
disassemble, compose, encrypt and decrypt messages with available keys. The
ability to eavesdrop all the messages in transit in the network is implicit in
our model due to the shared store of constraints. The other abilities are
modeled by the following utcc processes:

$\begin{array}[]{lll}{Disam}()&\operatorname{:\\!--}&(\mathbf{abs}\
x,y;\operatorname{\textup{{out}}}(\ (x,y)\
))\,\mathbf{tell}(\operatorname{\textup{{out}}}{(x)}\sqcup\operatorname{\textup{{out}}}{(y)})\\\
{Comp}()&\operatorname{:\\!--}&(\mathbf{abs}\
x,y;\operatorname{\textup{{out}}}(x)\sqcup\operatorname{\textup{{out}}}(y))\,\mathbf{tell}(\operatorname{\textup{{out}}}{(\
(x,y)\ )})\\\ {Enc}()&\operatorname{:\\!--}&(\mathbf{abs}\
x,y;\operatorname{\textup{{out}}}(x)\sqcup\operatorname{\textup{{out}}}(y))\,\mathbf{tell}(\operatorname{\textup{{out}}}{(\\{x\\}_{\operatorname{\mathit{pub}}(y)})})\\\
{Dec}()&\operatorname{:\\!--}&(\mathbf{abs}\
x,y;\operatorname{\textup{{out}}}(\operatorname{\mathit{priv}}(y))\sqcup\operatorname{\textup{{out}}}(\\{x\\}_{\operatorname{\mathit{pub}}(y)}))\,\mathbf{tell}(\operatorname{\textup{{out}}}{(x)})\\\
{Pers}()&\operatorname{:\\!--}&(\mathbf{abs}\
x;\operatorname{\textup{{out}}}(x))\,\mathbf{next}\,\mathbf{tell}(\operatorname{\textup{{out}}}(x))\\\
{Spy}()&\operatorname{:\\!--}&{Disam}()\parallel{Comp}()\parallel{Enc}()\parallel{Dec}()\parallel{Pers}()\parallel\mathbf{next}\,{Spy}()\end{array}$

Since the final store is not automatically transferred to the next time-unit,
the process $Pers$ above models the ability to remember all messages posted so
far.

It is easy to see that the process ${Spy}()$ in a store
$\operatorname{\textup{{out}}}(m)$ may add messages of unbounded length. Take
for example the process ${Comp}()$ that will add the constraints
$\operatorname{\textup{{out}}}(m)$,
$\operatorname{\textup{{out}}}((m,(m,m)))$,
$\operatorname{\textup{{out}}}(((m,m),m))$ and so on.

To deal with the inherent state explosion problem in the model of the
attacker, symbolic (compact) representations of the behavior of the attacker
have been proposed, for instance in [Boreale (2001), Fiore and Abadi (2001),
Olarte and Valencia (2008b), Bodei et al. (2010)]. Here we follow the approach
of restricting the number of states to be considered in the verification of
the protocol, as for instance in [Escobar et al. (2011), Song et al. (2001),
Armando and Compagna (2008)]. Roughly, we shall cut the messages generated of
length greater than a given $\kappa$, thus allowing us to model a bounded
version of the attacker.

Before defining the abstraction, we notice that the constraint system we are
considering includes existentially quantified syntactic equations. For this
kind of equations it is necessary to refer to a solved form of them in order
to have a uniform way to compute an approximation of the constraint system. We
then consider constraints of the shape
$\exists\vec{y}(x_{1}=t_{1}(\vec{y})\sqcup...\sqcup x_{n}=t_{n}(\vec{y}))$
where $\vec{x}=x_{1},...x_{n}$ are pairwise distinct and
$\vec{x}\cap\vec{y}=\emptyset$. Here, $t(\vec{y})$ refers to a term where
${\mathit{f}v}(t(\vec{y}))\subseteq\vec{y}$. Given a constraint, its normal
form can be obtained by applying the algorithm proposed in [Maher (1988)]
where: quantifiers are moved to the outermost position and equations of the
form $f(t_{1},...,t_{n})=f(t_{1}^{\prime},...,t_{n}^{\prime})$ are replaced by
$t_{1}=t_{1}^{\prime}\sqcup...\sqcup t_{n}=t_{n}^{\prime}$; equations such as
$x=x$ are deleted; equation of the form $t=x$ are replaced by $x=t$; and given
$x=t$, if $x$ does not occur in $t$, $x$ is replaced by $t$ in $t^{\prime}$ in
all equation of the form $x^{\prime}=t^{\prime}$. For instance, the solved
form of $\exists z,y(x=f(y)\sqcup y=g(z))$ is the constraint $\exists
z(x=f(g(z)))$.

######  Definition 5.35 (Abstract secure constraint system).

Let $\mathcal{M}$ be the set of terms (messages) generated from the signature
$\Sigma$ in Definition 5.34. Let ${\mathit{l}g}:\mathcal{M}\to\mathbb{N}$ be
defined as ${\mathit{l}g}(m)=0$ if $m\in\mathcal{P}\cup\mathcal{K}\cup Var$;
${\mathit{l}g}(\\{m_{1}\\}_{m_{2}})={\mathit{l}g}(\ (m_{1},m_{2})\
)=1+{\mathit{l}g}(m_{1})+{\mathit{l}g}(m_{2})$. Let $cut_{\kappa}(m)=m$ if
${\mathit{l}g}(m)\leq\kappa$. Otherwise, $cut_{\kappa}(m)=m_{\top}$ where
$m_{\top}\notin\mathcal{M}$ represents all the messages whose length is
greater than $\kappa$. We define $\alpha(c)$ as $\alpha_{\kappa}(NF(c))$ where

$\begin{array}[]{llll l
llll}\alpha_{\kappa}(c(m))&=&c(cut_{\kappa}(m))&&\alpha_{\kappa}(d_{xt})&=&d_{xt^{\prime}}\mbox{
where }t^{\prime}=cut_{\kappa}(t)\\\ \alpha_{\kappa}(c\sqcup
c^{\prime})&=&\alpha_{\kappa}(c)\sqcup\alpha_{\kappa}(c^{\prime})&&\alpha_{\kappa}(\exists\vec{x}c)&=&\exists\vec{x}\alpha_{\kappa}(c)\\\
\end{array}$

and $NF(c)$ is a solved form of the constraint $c$. We omit the superscript
$\alpha$ in the abstract operators $\sqcup^{\alpha}$, $\exists^{\alpha}$ and
$d_{\vec{x}\vec{t}}^{\alpha}$ to simplify the notation.

We note that the previous abstraction reminds of the $depth\mbox{-}\kappa$
abstractions typically done in the analysis of logic programs (see e.g., [Sato
and Tamaki (1984)]).

We shall illustrate the use of the abstract constraint system above by