arXiv:1403.0461v2 [] 22 Apr 2014

Under consideration for publication in Theory and Practice of Logic Programming

1

Timed Soft Concurrent Constraint Programs:
An Interleaved and a Parallel Approach
Stefano Bistarelli
Dipartimento di Matematica e Informatica, Università di Perugia
Via Vanvitelli 1, 06123 Perugia Italy
E-mail: vista@dmi.unipg.it

Maurizio Gabbrielli
Dipartimento di Scienze dell’Informazione, Università di Bologna
Via Zamboni 33, 40126 Bologna, Italy
E-mail: gabbri@cs.unibo.it

Maria Chiara Meo
Dipartimento di Economia, Università “G. D’Annunzio”
Viale Pindaro 42, 65127 Pescara, Italy
E-mail: cmeo@unich.it

Francesco Santini
Centrum Wiskunde & Informatica (CWI)
Science Park 123, 1098XG Amsterdam, The Netherlands
E-mail: F.Santini@cwi.nl
submitted 20 May 2012; revised 15 February 2014; accepted 18 February 2014

Abstract
We propose a timed and soft extension of Concurrent Constraint Programming. The time
extension is based on the hypothesis of bounded asynchrony: the computation takes a
bounded period of time and is measured by a discrete global clock. Action prefixing is
then considered as the syntactic marker which distinguishes a time instant from the next
one. Supported by soft constraints instead of crisp ones, tell and ask agents are now
equipped with a preference (or consistency) threshold which is used to determine their
success or suspension. In the paper we provide a language to describe the agents behavior, together with its operational and denotational semantics, for which we also prove the
compositionality and correctness properties. After presenting a semantics using maximal
parallelism of actions, we also describe a version for their interleaving on a single processor (with maximal parallelism for time elapsing). Coordinating agents that need to take
decisions both on preference values and time events may benefit from this language. To
appear in Theory and Practice of Logic Programming (TPLP).
KEYWORDS: Soft Concurrent Constraint Programming, Timed Concurrent Constraint
Programming, Interleaving, Parallelism.

2

Bistarelli et al.
1 Introduction

Time is a particularly important aspect of cooperative environments. In many “reallife” computer applications, the activities have a temporal duration (that can be
even interrupted) and the coordination of such activities has to take into consideration this timeliness property. The interacting actors are mutually influenced by their
actions, meaning that A reacts accordingly to the timing and quantitative aspects
related to B ’s behavior, and vice versa. In fact, these interactions can be often related to quantities to be measured or minimized/maximized, in order to take actions
depending from these scores: consider, for example, some generic communicating
agents that need to take decisions on a (monetary) cost or a (fuzzy) preference
for a shared resource. They both need to coordinate through time-dependent and
preference-based decisions.
A practical example of such agents corresponds, for example, to software agents
that need to negotiate some service-level agreement on a resource, or a service,
with time-related side-conditions. For instance, a fitting example is given by auction
schemes, where the seller/bidder agents need to agree on a preference for a given
prize (e.g., a monetary cost). At the same time, the agents have to respect some
timeout and alarm events, respectively representing the absence and the presence
of bids for the prize (for instance). The language we present in this paper is well
suited for this kind of interactions, as Section 5 shows with examples.
The Timed Concurrent Constraint Programming (tccp), a timed extension of the
pure formalism of Concurrent Constraint Programming (ccp) (Saraswat 1989), has
been introduced in (de Boer et al. 2000). The language is based on the hypothesis
of bounded asynchrony (Saraswat et al. 1996): computation takes a bounded period
of time rather than being instantaneous as in the concurrent synchronous languages
ESTEREL (Berry and Gonthier 1992), LUSTRE (Halbwachs et al. 1991), SIGNAL (le Guernic et al. 1991)
and Statecharts (Harel 1987). Time itself is measured by a discrete global clock,
i.e., the internal clock of the tccp process. In (de Boer et al. 2000) the authors also
introduced timed reactive sequences, which describe the reaction of a tccp process
to the input of the external environment, at each moment in time. Formally, such a
reaction is a pair of constraints hc, d i, where c is the input and d is the constraint
produced by the process in response to c.
Soft constraints (Bistarelli 2004; Bistarelli et al. 1997) extend classical constraints
to represent multiple consistency levels, and thus provide a way to express preferences, fuzziness, and uncertainty. The ccp framework has been extended to work
with soft constraints (Bistarelli et al. 2006), and the resulting framework is named
Soft Concurrent Constraint Programming (sccp). With respect to ccp, in sccp the
tell and ask agents are equipped with a preference (or consistency) threshold, which
is used to determine their success, failure, or suspension, as well as to prune the
search; these preferences should preferably be satisfied but not necessarily (i.e. overconstrained problems). We adopt soft constraints instead of crisp ones, since classic
constraints show evident limitations when trying to represent real-life scenarios,
where the knowledge is not completely available nor crisp.
In this paper, we introduce a timed and soft extension of ccp that we call Timed

TSCCP: An Interleaved and a Parallel Approach

3

Soft Concurrent Constraint Programming (tsccp), inheriting from both tccp and
sccp at the same time. In tsccp, we directly introduce a timed interpretation of
the usual programming constructs of sccp, by identifying a time-unit with the time
needed for the execution of a basic sccp action (ask and tell), and by interpreting
action prefixing as the next-time operator. An explicit timing primitive is also introduced in order to allow for the specification of timeouts. In the first place, the
parallel operator of tsccp is first interpreted in terms of maximal parallelism, as in
(de Boer et al. 2000). Secondly, we also consider a different paradigm, where the
parallel operator is interpreted in terms of interleaving, however assuming maximal
parallelism for actions depending on time. In other words, time passes for all the
parallel processes involved in a computation. This approach, analogous to that one
adopted in (de Boer et al. 2004), is different from that one of (de Boer et al. 2000;
Bistarelli et al. 2008) (where maximal parallelism was assumed for any kind of action), and it is also different from the one considered in (Busi et al. 2000), where
time does not elapse for timeout constructs. This can be accomplished by allowing
all the time-only dependent actions (τ -transitions) to concurrently run with at most
one action manipulating the store (a ω-transition).
The paper extends the results in (Bistarelli et al. 2008) by providing new semantics that allows maximal parallelism for time elapsing and an interleaving model for
basic computation steps (see Section 7). This new language is called tsccp with interleaving, i.e., tsccp-i, to distinguish it from the version allowing maximal parallelism
of all actions. According to the maximal parallelism policy (applied, for example, in
the original works as (Saraswat 1989) and (Saraswat et al. 1994)), at each moment
every enabled agent of the system is activated, while in the interleaving paradigm
only one of the enabled agents is executed instead. This second paradigm is more
realistic if we consider limited resources, since it does not imply the existence of
an unbounded number of processors. However, in (de Boer et al. 2000) it is shown
that the notion of maximal parallelism of tsccp is more expressive than the notion
of interleaving parallelism of other concurrent constraint languages. The presence
of maximal parallelism can force the computation to discard some (non-enabled)
branches which could became enabled later on (because of the information produced by parallel agents), while this is not possible when considering an interleaving model. Therefore, tsccp is sensitive to delays in adding constraints to the store,
whereas this is not the case for ccp and tsccp-i.
The rest of the paper is organized as follows: in Section 2 we summarize the most
important background notions and frameworks from which tsccp derives, i.e. tccp
and sccp. In Section 3 we present the tsccp language, and in Section 4 describes
the operational semantics of tscc agents. Section 5 better explains the programming
idioms as timeout and interrupt, exemplifies the use of timed paradigms in the tscc
language and shows an application example on modeling an auction interaction
among several bidders and a single auctioneer. Section 6 describes the denotational
semantics for tsccp, and proves the denotational model correctness with the aid
of connected reactive sequences. Section 7 explains the semantics for interleaving
with maximal parallelism of time-elapsing actions (i.e. the tsccp-i language), while
Section 8 describes a timeline for the execution of three parallel agents in tsccp-i.

4

Bistarelli et al.

Section 9 describes the denotational semantics of tsccp-i and proves the correctness of the denotational model. Section 10 reports the related work and, at last,
Section 11 concludes by also indicating future research.
2 Background
2.1 Soft Constraints
A soft constraint (Bistarelli et al. 1997; Bistarelli 2004) may be seen as a constraint
where each instantiation of its variables has an associated value from a partially
ordered set which can be interpreted as a set of preference values. Combining constraints will then have to take into account such additional values, and thus the
formalism has also to provide suitable operations for combination (×) and comparison (+) of tuples of values and constraints. This is why this formalization is
based on the concept of c-semiring (Bistarelli et al. 1997; Bistarelli 2004), called
just semiring in the rest of the paper.
Semirings. A semiring is a tuple hA, +, ×, 0, 1i such that: i) A is a set and 0, 1 ∈ A;
ii) + is commutative, associative and 0 is its unit element; iii) × is associative,
distributes over +, 1 is its unit element and 0 is its absorbing element. A c-semiring
is a semiring hA, +, ×, 0, 1i such that: + is idempotent, 1 is its absorbing element
and × is commutative. Let us consider the relation ≤S over A such that a ≤S b
iff a + b = b. Then, it is possible to prove that (see (Bistarelli et al. 1997)): i) ≤S
is a partial order; ii) + and × are monotone on ≤S ; iii) 0 is its minimum and 1
its maximum; iv) hA, ≤S i is a complete lattice (a complete lattice is a partially
ordered set in which all subsets have both a supremum and an infimum) and, for
all a, b ∈ A, a + b = lub(a, b) (where lub is the least upper bound).
Moreover, if × is idempotent, then: + distributes over ×; hA, ≤S i is a complete
distributive lattice and × its glb (greatest lower bound). Informally, the relation ≤S
gives us a way to compare semiring values and constraints. In fact, when we have
a ≤S b, we will say that b is better than a. In the following, when the semiring will
be clear from the context, a ≤S b will be often indicated by a ≤ b.
Constraint System. Given a semiring S = hA, +, ×, 0, 1i and an ordered set of
variables V over a finite domain D , a soft constraint is a function which, given an
assignment η : V → D of the variables, returns a value of the semiring. Using this
notation C = η → A is the set of all possible constraints that can be built starting
from S , D and V .
Any function in C involves all the variables in V , but we impose that it depends on
the assignment of only a finite subset of them. So, for instance, a binary constraint
cx ,y over variables x and y, is a function cx ,y : (V → D ) → A, but it depends only
on the assignment of variables {x , y} ⊆ V (the support of the constraint, or scope).
Note that cη[v := d1 ] means cη ′ where η ′ is η modified with the assignment v := d1
(that is the operator [ ] has precedence over application). Note also that cη is the
application of a constraint function c : (V → D ) → A to a function η : V → D ;
what we obtain, is a semiring value cη.

TSCCP: An Interleaved and a Parallel Approach

5

The partial order ≤S over C can be easily extended among constraints by defining
c1 ⊑ c2 ⇔ c1 η ≤ c2 η, for each possible η.
Combining and projecting soft constraints. Given the set C, the combination function ⊗ : C ×C → C is defined as (c1 ⊗c2 )η = c1 η×c2 η (see also (Bistarelli et al. 1997;
Bistarelli 2004; Bistarelli et al. 2006)). Informally, performing the ⊗ between two
constraints means building a new constraint whose support involves all the variables of the original ones, and which associates with each tuple of domain values
for such variables a semiring element which is obtained by multiplying the elements
associated by the original constraints to the appropriate sub-tuples.
Given a constraint c ∈ C and a variable v ∈ V , the projection (Bistarelli et al. 1997;
Bistarelli 2004; Bistarelli et al. 2006) of c over V − {v }, written c ⇓(V −{v }) is the
P
constraint c ′ s.t. c ′ η = d∈D cη[v := d ]. Informally, projecting means eliminating
some variables from the support. This is done by associating with each tuple over
the remaining variables a semiring element which is the sum of the elements associated by the original constraint to all the extensions of this tuple over the eliminated
variables.
We define also a function ā (Bistarelli 2004; Bistarelli et al. 2006) as the function
that returns the semiring value a for all assignments η, that is, āη = a. We will
usually write ā simply as a. An example of constants that will be useful later are
0̄ and 1̄ that represent respectively the constraints associating 0 and 1 to all the
assignment of domain values.
Solutions. A SCSP (Bistarelli 2004) is defined as P = hV , D , C , S i, where C is the
set of constraints defined over variables in V (each with domain D ), and whose
preference is determined by semiring S . The best level of consistency notion is deN
fined as blevel(P ) = Sol(P ) ⇓∅ , where Sol (P ) =
C (Bistarelli 2004). A problem
P is α-consistent if blevel(P ) = α (Bistarelli 2004). P is instead simply “consistent” iff there exists α >S 0 such that P is α-consistent. P is inconsistent if it is
not consistent.
<a>
<b>

1
9

<a,a>
<a,b>
<b,a>
<b,b>

c1

5
1
2
2

X
c2

<a>
<b>

5
5
c3

Y

Fig. 1. A SCSP based on a weighted semiring.

Example 1
Figure 1 shows a weighted SCSP as a graph: the weighted semiring is used, i.e. hR+ ∪
{∞}, min, +̂, ∞, 0i (+̂ is the arithmetic plus operation). Variables and constraints
are represented respectively by nodes and arcs (unary for c1 -c3 , and binary for c2 );
D = {a, b}. The solution of the CSP in Figure 1 associates a semiring element to

6

Bistarelli et al.

every domain value of variables X and Y by combining all the constraints together,
N
i.e. Sol (P ) =
C . For instance, for the tuple ha, ai (that is, X = Y = a), we have
to compute the sum of 1 (which is the value assigned to X = a in constraint c1 ),
5 (hX = a, Y = ai in c2 ) and 5 (Y = a in c3 ): the value for this tuple is 11. The
solution X = a, Y = b is a 7-consistent solution, where 7 corresponds to the blevel
of P , i.e., Sol(P ) ⇓∅ = 7.
2.2 Concurrent Constraint Programming over Soft Constraints
The basic idea underlying ccp (Saraswat 1989) is that computation progresses via
monotonic accumulation of information in a constraint global store. Information is
produced by the concurrent and asynchronous activity of several agents which can
add (tell) a constraint to the store. Dually, agents can also check (ask) whether a
constraint is entailed by the store, thus allowing synchronization among different
agents. The ccp languages are defined parametrically w.r.t. a given constraint system. The notion of constraint system has been formalized in (Saraswat and Rinard 1990)
following Scott’s treatment of information systems. Soft constraints over a semiring S = hA, +, ×, 0, 1i and an ordered set of variables V (over a domain D ) have
been showed to form a constraint system “à la Saraswat”, thus leading to the definition of Soft Concurrent Constraint Programmingg (sccp) (Bistarelli et al. 1997;
Bistarelli 2004; Bistarelli et al. 2006).
Consider the set C and the partial order ⊑. Then an entailment relation ⊢⊆
N
℘(C) × C is defined s.t. for each C ∈ ℘(C) and c ∈ C, we have C ⊢ c ⇔
C ⊑c
(see also (Bistarelli 2004; Bistarelli et al. 2006)). Note that in this setting the notion
of token (constraint) and of set of tokens (set of constraints) closed under entailment
is used indifferently. In fact, given a set of constraint functions C1 , its closure w.r.t.
N
entailment is a set C¯1 that contains all the constraints greater than
C1 . This set
N
is univocally representable by the constraint function
C1 . The definition of the
entailment operator ⊢ on top of C, and of the ⊑ relation, lead to the notion of soft
constraint system. It is also important to notice that in (Saraswat 1989) it is claimed
that a constraint system is a complete algebraic lattice. In the sccp framework,
algebraicity is not required (Bistarelli et al. 2006) instead, since the algebraic nature
of the structure C strictly depends on the properties of the semiring1 .
To treat the hiding operator of the language, a general notion of existential quantifier is introduced by using notions similar to those used in cylindric algebras. Consider a set of variables V with domain D and the corresponding soft constraint system C. For each x ∈ V , the hiding function (Bistarelli 2004; Bistarelli et al. 2006)
P
is the function (∃x c)η = di ∈D cη[x := di ]. To make the hiding operator computationally tractable, it is required that the number of domain elements in D , having
semiring values different from 0, is finite (Bistarelli et al. 2006). In this way, to compute the sum needed for (∃x c)η, we can consider just a finite number of elements
1

Notice that we do not aim at computing the closure of the entailment relation, but only to
use the entailment relation to establish if a constraint is entailed by the current store, and this
can be established even if the lattice is not algebraic (that is even if the times operator is not
idempotent).

TSCCP: An Interleaved and a Parallel Approach

7

(those different from 0), since 0 is the unit element of the sum. Note that by using
the hiding function we can represent the ⇓ operator defined in Section 2.1. In fact,
for any constraint c and any variable x ⊆ V , c ⇓V −x = ∃x c (Bistarelli et al. 2006).
To model parameter passing also diagonal elements have to be defined. Consider
a set of variables V and the corresponding soft constraint system. Then, for each
x , y ∈ V , a diagonal constraint is defined as dxy ∈ C s.t., dxy η[x := a, y := b] = 1 if
a = b, and dxy η[x := a, y := b] = 0 if a 6= b (Bistarelli 2004; Bistarelli et al. 2006).
Theorem 1 (cylindric constraint system (Bistarelli et al. 2006))
Consider a semiring S = hA, +, ×, 0, 1i, a domain of the variables D , an ordered set
of variables V , and the corresponding structure C. Then, SC = hC, ⊗, 0, 1, ∃x , dxy i,
is a cylindric constraint system.
2.3 Timed Concurrent Constraint Programming
A timed extension of ccp, called tccp has been introduced in (de Boer et al. 2000).
Similarly to other existing timed extensions of ccp defined in (Saraswat et al. 1996),
tccp is a language for reactive programming designed around the hypothesis of
bounded asynchrony (as introduced in (Saraswat et al. 1996): computation takes a
bounded period of time rather than being instantaneous).
When querying the store for some information that is not present (yet), a ccp
agent will simply suspend until the required information has arrived. In timed
applications however often one cannot wait indefinitely for an event. Consider for
example the case of a connection to a web service providing some on-line banking
facility. In case the connection cannot be established, after a reasonable amount of
time an appropriate time-out message has to be communicated to the user. A timed
language should then allow us to specify that, in case a given time bound is exceeded
(i.e. a time-out occurs), the wait is interrupted and an alternative action is taken.
Moreover, in some cases it is also necessary to have a preemption mechanism which
allows one to abort an active process A and to start a process B when a specific
(abnormal) event occurs.
In order to be able to specify these timing constraints tccp introduces a discrete
global clock and assumes that ask and tell actions take one time-unit. Computation evolves in steps of one time-unit, so called clock-cycles. Action prefixing is the
syntactic marker which distinguishes a time instant from the next one and it is
assumed that parallel processes are executed on different processors, which implies
that, at each moment, every enabled agent of the system is activated. This assumption gives rise to what is called maximal parallelism. The time in between two
successive moments of the global clock intuitively corresponds to the response time
of the underlying constraint system. Thus all parallel agents are synchronized by
the response time of the underlying constraint system. Since the store is monotonically increasing and one can have dynamic process creation, clearly the previous
assumptions imply that the constraint solver takes a constant time (no matter how
big the store is), and that there is an unbounded number of processors. However,
one can impose suitable restriction on programs, thus ensuring that the (significant

8

Bistarelli et al.

part of the) store and the number of processes do not exceed a fixed bound; these
restrictions would still allow significant forms of recursion with parameters.
Furthermore, a timing construct of the form now c then A else B is introduced
in tccp, whose semantics is the following: if the constraint c is entailed by the store
at the current time t , then the above agent behaves as A at time t , otherwise it
behaves as B at time t . This basic construct allows to derive such timing mechanisms as time-out and preemption (de Boer et al. 2000; Saraswat et al. 1996). The
instantaneous reaction can be obtained by evaluating nowc in parallel with A and
B , within the same time-unit. At the end of this time-unit, the store will be updated by using either the constraint produced by A, or that one produced by B ,
depending on the result of the evaluation of nowc. Clearly, since A and B could
contain nested now then else agents, a limit for the number of these nested agents
should be fixed. Note that, for recursive programs, such a limit is ensured by the
presence of the procedure-call, since we assume that the evaluation of such calls
takes one time-unit.
3 Timed Soft Concurrent Constraint Programming
In this section we present the tsccp language, which originates from both tccp and
sccp. To obtain this aim, we extend the syntax of the cc language with the timing
construct nowc thenA elseB (inherited from tccp), and also in order to directly
handle the cut level as in sccp. This means that the syntax and semantics of the
tell, ask and nowagents have to be enriched with a threshold that is used to check
when the agents may succeed, or suspend.
Definition 1 (tsccp Language)
Given a soft constraint system hS , D , V i, the corresponding structure C, any semiring value a, soft constraints φ, c ∈ C and any tuple of variables x , the syntax of
the tsccp language is given by the following grammar:
P ::=
F ::=
A ::=
E ::=

F .A
p(x ) :: A | F · F
success | tell(c) →φ A | tell(c) →a A | E | A k A | ∃xA | p(x ) |
Σni=1 Ei | nowφ c then A else A | nowa c then A else A
ask(c) →φ A | ask(c) →a A

where, as usual, P is the class of processes, F is the class of sequences of procedure
declarations (or clauses), A is the class of agents. In a tsccp process P = F .A, A
is the initial agent, to be executed in the context of the set of declarations F . The
agent success represents a successful termination, so it may not make any further
transition.
In the following, given an agent A, we denote by Fv (A) the set of the free variables
of A (namely, the variables which do not appear in the scope of the ∃ quantifier).
Besides the use of soft constraints (see Section 2.2) instead of crisp ones, there are
two fundamental differences between tsccp and ccp. The first main difference w.r.t.
the original cc syntax is the presence of a semiring element a and of a constraint

TSCCP: An Interleaved and a Parallel Approach

9

φ to be checked whenever an ask or tell operation is performed. More precisely,
the level a (respectively, φ) will be used as a cut level to prune computations that
are not good enough. The second main difference with respect to ccp (but, this
time, also with respect to sccp) is instead the presence of the nowc then A else
B construct introduced in Section 2.3. Even for this construct, the level a (or φ) is
used as a cut level to prune computations.
Action prefixing is denoted by →, non-determinism is introduced via the guarded
choice construct Σni=1 Ei , parallel composition is denoted by k, and a notion of
locality is introduced by the agent ∃xA, which behaves like A with x considered
local to A, thus hiding the information on x provided by the external environment.
In the next subsection we formally describe the operational semantics of tsccp. In
order to simplify the notation, in the following we will usually write a tsccp process
P = F .A simply as the corresponding agent A.
4 An Operational Semantics for tsccp Agents
The operational model of tscc agents can be formally described by a transition
system T = (Conf , −→) where we assume that each transition step takes exactly one time-unit. Configurations in Conf are pairs consisting of a process and
of a constraint in C, representing the common store shared by all the agents. The
transition relation −→⊆ Conf × Conf is the least relation satisfying the rules R1R17 in Figure 2, and it characterizes the (temporal) evolution of the system. So,
hA, σi −→ hB , δi means that, if at time t we have the process A and the store σ,
then at time t + 1 we have the process B and the store δ.
Let us now briefly discuss the rules in Figure 2. Here is a brief description of the
transition rules:
Valued-tell. The valued-tell rule checks for the a-consistency of the Soft Constraint Satisfaction Problem (Bistarelli 2004) (SCSP) defined by the store σ ⊗ c.
A SCSP P is a-consistent if blevel (P ) = a, where blevel (P ) = Sol (P ) ⇓∅ , i.e., the
best level of consistency of the problem P is a semiring value representing the
least upper bound among the values yielded by the solutions. Rule R1 can be
applied only if the store σ ⊗ c is b-consistent with b 6< a 2 . In this case the agent
evolves to the new agent A over the store σ ⊗ c. Note that different choices of
the cut level a could possibly lead to different computations. Finally, note that
the updated store σ ⊗ c will be visible only starting from the next time instant,
since each transition step involves exactly one time-unit.
Tell. The tell action is a finer check of the store. In this case (see rule R2), a
pointwise comparison between the store σ ⊗ c and the constraint φ is performed.
The idea is to perform an overall check of the store, and to continue the computation only if there is the possibility to compute a solution not worse than φ.
Note that this notion of tell could be also applied to the classical cc framework:
2

Notice that we use b 6< a instead of b ≥ a because we can possibly deal with partial orders.
The same holds also for 6⊏ instead of ⊒.

10

Bistarelli et al.
R1

(σ ⊗ c) ⇓∅ 6< a
htell(c) →a A, σi −→ hA, σ ⊗ ci

V-tell

R2

σ ⊗ c 6⊏ φ
htell(c) →φ A, σi −→ hA, σ ⊗ ci

Tell

R3

σ⊢c
σ ⇓∅ 6< a
hask(c) →a A, σi −→ hA, σi

V-ask

R4

σ ⊢ c σ 6⊏ φ
hask(c) →φ A, σi −→ hA, σi

Ask

R5

R6

R7

hA, σi −→ hA′ , σ ⊗ δi hB , σi −→ hB ′ , σ ⊗ δ ′ i
hA k B , σi −→ hA′ k B ′ , σ ⊗ δ ⊗ δ ′ i
hA, σi −→ hA′ , σ ′ i hB , σi 6−→
hA k B , σi −→ hA′ k B , σ ′ i
hB k A, σi −→ hB k A′ , σ ′ i
hEj , σi −→ hAj , σ ′ i
j ∈ [1, n]
hΣni=1 Ei , σi −→ hAj , σ ′ i

Parall1

Parall2

Nondet

R8

hA, σi −→ hA′ , σ ′ i
σ⊢c
σ ⇓∅ 6< a
hnowa c then A else B , σi −→ hA′ , σ ′ i

V-now1

R9

hA, σi 6−→
σ⊢c
σ ⇓∅ 6< a
hnowa c then A else B , σi −→ hA, σi

V-now2

R10

hB , σi −→ hB ′ , σ ′ i
σ 6⊢ c σ ⇓∅ 6< a
hnowa c then A else B , σi −→ hB ′ , σ ′ i

V-now3

R11

hB , σi 6−→
σ 6⊢ c
σ ⇓∅ 6< a
hnowa c then A else B , σi −→ hB , σi

V-now4

R12

hA, σi −→ hA′ , σ ′ i σ ⊢ c σ 6⊏ φ
hnowφ c then A else B , σi −→ hA′ , σ ′ i

Now1

R13

hA, σi 6−→
σ ⊢ c σ 6⊏ φ
hnowφ c then A else B , σi −→ hA, σi

Now2

R14

hB , σi −→ hB ′ , σ ′ i σ 6⊢ c σ 6⊏ φ
hnowφ c then A else B , σi −→ hB ′ , σ ′ i

Now3

R15

hB , σi 6−→
σ 6⊢ c σ 6⊏ φ
hnowφ c then A else B , σi −→ hB , σi

Now4

R16

hA[x /y], σi −→ hB , σ ′ i
h∃xA, σi −→ hB , σ ′ i

Hide

R17

hp(x ), σi −→ hA, σi

P-call

p(x) :: A ∈ F

Fig. 2. The transition system for tsccp.

TSCCP: An Interleaved and a Parallel Approach

11

the tell operation would succeed when the set of tuples satisfying constraint φ
is not a superset of the set of tuples allowed by σ ∩ c.3 As for the valued tell,
the updated store σ ⊗ c will be visible only since the next time instant. In the
following, let us use tell(c) → A and tell(c) as a shorthand for tell(c) →0̄ A
and tell(c) →0̄ success, respectively.
Valued-ask. The semantics of the valued-ask is extended in a way similar to what
we have done for the valued-tell action. This means that, to apply the rule R3,
we need to check if the store σ entails the constraint c, and also if σ is “consistent
enough” w.r.t. the threshold a set by the programmer.
Ask. In rule R4, we check if the store σ entails the constraint c, but, similarly to
rule R2, we also compare a finer (pointwise) threshold φ to the store σ. As for
the tell action, let us use ask(c) → A as a shorthand for ask(c) →0̄ A.
Parallelism. Rules R5 and R6 model the parallel composition operator in terms
of maximal parallelism: the agent A k B executes in one time-unit all the initial
enabled actions of A and B . Considering rule R5 (where maximal parallelism is
accomplished in practice), notice that the ordering of the operands in σ ⊗ δ ⊗ δ ′ is
not relevant, since ⊗ is commutative and associative. Moreover, for the same two
properties, if σ ⊗δ = σ ⊗γ and σ ⊗δ ′ = σ ⊗γ ′ , we have that σ ⊗δ ⊗δ ′ = σ ⊗γ ⊗γ ′.
Therefore the resulting store σ ⊗ δ ⊗ δ ′ is independent from the choice of the
constraint δ such that hA, σi −→ hA′ , σ ′ i and σ ′ = σ ⊗ δ (analogously for δ ′ ).
Nondeterminism. According to rule R7, the guarded choice operator gives rise
to global non-determinism: the external environment can affect the choice, since
ask(cj ) is enabled at time t (and Aj is started at time t + 1) if and only if the
store σ entails cj (and if it is compatible with the threshold too), and σ can be
modified by other agents.
Valued-now and Now. Rules R8-R11 show that the agent nowa c then A else
B behaves as A or B depending on the fact that c is or is not entailed by the store,
provided that the current store σ is compatible with the threshold. Differently
from the case of the ask, here the evaluation of the guard is instantaneous: if
current store σ is compatible with the threshold a, hA, σi (hB , σi) can make a
transition at time t and c is (is not) entailed by the store σ, then the agent
nowa c then A else B can make the same transition at time t . Moreover,
observe that in any case the control is passed either to A (if c is entailed by
the current store σ and σ is compatible with the threshold) or to B (in case σ
does not entail c and σ is compatible with the threshold). Analogously for the
not-valued version, i.e., nowφ c then A else B (see rules R12-R15). Finally, we
use now c then A else B as a shorthand for the agent now0̄ c then A else B
Hiding variables. The agent ∃xA behaves like A, with x considered local to A, as
show by rule R16. This is obtained by substituting the variable x for a variable
y, which we assume to be new and not used by any other process. Standard
renaming techniques can be used to ensure this; in rule R16, A[x /y] denotes the
process obtained from A by replacing the variable x for the variable y.

3

Notice that the ⊗ operator in the crisp case reduces to set intersection.

12

Bistarelli et al.

Procedure-calls. Rule R17 treats the case of a procedure-call when the actual
parameter equals the formal parameter. We do not need more rules since, for the
sake of simplicity, here and in the following we assume that the set F of procedure
declarations is closed w.r.t. parameter names: that is, for every procedure-call
p(y) appearing in a process F.A, we assume that, if the original declaration for p
in F is p(x ) :: A, then F contains also the declaration p(y) :: ∃x (tell(dxy ) k A).4
Moreover, we assume that if p(x ) :: A ∈ F , then Fv (A) ⊆ x .
Using the transition system described by (the rules in) Figure 2, we can now define
our notion of observables, which considers the results of successful terminating
computations that the agent A can perform for each tsccp process P = F .A.
Here and in the following, given a transition relation −→, we denote by −→∗ its
reflexive and transitive closure.
Definition 2 (Observables)
Let P = F .A be a tsccp process. We define
mp
Oio
(P ) = {γ ⇓Fv (A) | hA, 1i −→∗ hSuccess, γi}

where Success is any agent which contains only occurrences of the agent success
and of the operator k.
5 Programming Idioms and Examples
We can consider the primitives in Definition 1 to derive the soft version of the
programming idioms in (de Boer et al. 2000), which are typical of reactive programming.
t

t

Delay. The delay constructs tell(c) −→φ A or ask(c) −→φ A are used to delay the
execution of agent A after the execution of tell(c) or ask(c); t is the number
of the time-units of delay. Therefore, in addiction to a constraint φ, in tsccp
the transition arrow can have also a number of delay slots. This idiom can
0
be defined by induction: the base case is −→φ A ≡→φ A, and the inductive
n+1

n

step is −→φ A ≡→φ tell(1̄) −→0̄ A. The valued version can be defined in an
analogous way.
Timeout. The timed guarded choice agent Σni=1 ask(ci ) →i Ai timeout(m) B waits at
most m time-units (m ≥ 0) for the satisfaction of one of the guards; notice
that all the ask actions have a soft transition arrow, i.e. →i is either of the
form →φi or →ai , as in Figure 2. Before this time-out, the process behaves
just like the guarded choice: as soon as there exist enabled guards, one of them
(and the corresponding branch) is nondeterministically selected. After waiting
for m time-units, if no guard is enabled, the timed choice agent behaves as
B . Timeout constructs can be assembled through the composition of several
4

Here the (original) formal parameter is identified as a local alias of the actual parameter.
Alternatively, we could have introduced a new rule treating explicitly this case, as it was in the
original ccp papers.

TSCCP: An Interleaved and a Parallel Approach

13

nowφ c then A else B primitives (or their valued version), as explained in
(de Boer et al. 2000) for the (crisp) tccp language.
The timeout can be defined inductively as follows: let us denote by A the agent
Σni=1 ask(ci ) →i Ai . In the base case, that is m = 0, we define Σni=1 ask(ci ) →i
Ai timeout(0) B as the agent:
now1 c1 then A
else ( now2 c2 then A
else (. . . ( nown cn then A else ask(1̄) → B ) . . .))
where for i = 1, . . . , n, either nowi = nowφi if →i is of the form →φi or
nowi = nowai if →i is of the form →ai . Because of the operational semantics
explained in rules R8-R11 (see Figure 2), if a guard ci is true, then the agent
Σni=1 ask(ci ) →i Ai is evaluated in the same time slot. Otherwise, if no guard
ci is true, the agent B is evaluated in the next time slot. Then, by inductively
reasoning on the number of time-units m, we can define Σni=1 ask(ci ) →i
Ai timeout(m) B as
Σni=1 ask(ci ) →i Ai timeout(0) (Σni=1 ask(ci ) →i Ai timeout(m − 1) B ).
Watchdog. Watchdogs are used to interrupt the activity of a process on a signal from a
specific event. The idiom do A watchingφ c behaves as A, as long as c is not
entailed by the store and the current store is compatible with the threshold;
when c is entailed and the current store is compatible with the threshold, the
process A is immediately aborted.
The reaction is instantaneous, in the sense that A is aborted at the same
time instant of the detection of the entailment of c. However, according to
the computational model, if c is detected at time t , then c has to be produced
at time t ′ with t ′ < t . Thus, we have a form of weak preemption.
As well as timeouts, also watchdog agents can be defined in terms of the other
basic constructs of the language (see Figure 3).
In the following we assume that there exists an (injective) renaming function
ρ which, given a procedure name p, returns a new name ρ(p) that is not used
elsewhere in the program. Moreover, let us use nowφ c else B as a shorthand
for nowφ c then success else B , where we assume that, for any procedure
p declared as p(x ) :: A, a declaration ρ(p)(x ) :: do ρ(A) watchingφ c is
added, where ρ(A) denotes the agent obtained from A by replacing in it each
occurrence of any procedure q by ρ(q). The assumption in the case of the
∃xA agent is needed for correctness. In practical cases, it can be satisfied by
suitably renaming the variables associated to signals. In the following →′ is
either of the form →ψ or →a . Analogously for now′ .
The translation in Figure 3 can be easily extended to the case of the agent
do A watchingφ c else B , which behaves as the previous watchdog and also
activates the process B when A is aborted (i.e., when c is entailed and the
current state is compatible with the threshold). In the following we will then
use also this form of watchdog.

14

Bistarelli et al.
do success watchingφ c

=⇒

success

do tell(d ) →′ A watchingφ c

=⇒

nowφ c else tell(d ) →′ do A watchingφ c

do Σni=1 ask(ci ) →i Ai watchingφ c

=⇒

nowφ c else Σni=1 ask(ci ) →i do Ai watchingφ c

do (now′ d then A else B ) watchingφ c

=⇒

now′ d

do A k B watchingφ c

=⇒

do A watchingφ c k do B watchingφ c

do ∃xA watchingφ c

=⇒

∃x do A watchingφ c, assuming ∃x c = c

do p(x ) watchingφ c

=⇒

nowφ c else ρ(p)(x ) watchingφ c

then do A watchingφ c
else do B watchingφ c

Fig. 3. Examples of watchdog constructs.
c1 : ({x } → N ) → R+ s.t. c1 (x ) = x + 3

c2 : ({x } → N ) → R+ s.t. c2 (x ) = x + 5

c3 : ({x } → N ) → R+ s.t. c3 (x ) = 2x + 8

Fig. 4. Three (weighted) soft constraints; c3 = c1 ⊗ c2 , c2 ⊢ c1 , c3 ⊢ c1 and c3 ⊢ c2 .
The assumption on the instantaneous evaluation of nowφ c is essential in
order to obtain a preemption mechanism which can be expressed in terms of
the nowφ then else primitive. In fact, if the evaluation of nowφ c took one
time-unit, then this unit delay would change the compositional behavior of
the agent controlled by the watchdog. Consider, for example, the agent A =
tell(a) → tell(b), which takes two time-units to complete its computation.
The agent At = now c else tell(a) → now c else tell(b) (resulting from
the translation of do A watching0̄ c) compositionally behaves as A, unless
a c signal is detected and the current state is compatible with the threshold,
in which case the evaluation of A is interrupted. On the other hand, if the
evaluation of now c took one time-unit, then At would take four time-units
and would not behave anymore as A when c is not present. In fact, in this
case, the agent A k B would produce d while At k B would not, where B is
the agent ask(1̄) → now a then tell(d ) else success.
The valued version of watchdogs can be defined in an analogous way.
With this small set of idioms, we have now enough expressiveness to describe
complex interactions. For the following examples on the new programming idioms,
we consider the Weighted semiring h + ∪ {+∞}, min, +, +∞, 0i (Bistarelli 2004;
Bistarelli et al. 1997) and the (weighted) soft constraints in Figure 4. We first provide simple program examples in order to explain as more details as possible on
how a computation of tsccp agents proceeds. In Section 5.1 we show a more complex example describing the classical actions during a negotiation process; the aim
of that example is instead to show the expressivity of the tsccp language, without
analyzing its execution in detail.

R

Example 2 (Delay)

TSCCP: An Interleaved and a Parallel Approach

15

As a first very simple example, suppose to have two agents A1 , A2 of the form:
2
1
A1 :: tell(1̄) −→ +∞ tell(c2 ) → +∞ success and A2 :: tell(1̄) −→ +∞ ask(c1 ) →9
success; their concurrent evaluation in the 1̄ ≡ 0̄ empty store is:
2

1

h(tell(0̄) −→ +∞ tell(c2 )→+∞ success) k (tell(0̄) −→ +∞ ask(c1 ) →9 success), 0̄i.
The timeline for this parallel execution is described in Figure 5. For the evaluation
of tell and ask we respectively consider the rules R1 and R3 in Figure 2, since
both transitions are a-valued. However, both these two actions are delayed: three
time-units for the tell(c2 ) of A1 (including the first tell(0̄)), and two time-units
for the ask(c1 ) of A2 (including the first tell(0̄)). As explained before, this can be
obtained by adding 1̄ to the store with a tell action respectively three, and two
times. Therefore, the parallel agent A1 k A2 corresponds to:
(tell(0̄) → +∞ tell(0̄) →

+∞

tell(0̄) → +∞ tell(c2 ) → +∞ success) k

(tell(0̄) → +∞ tell(0̄) → +∞ ask(c1 ) →9 success).
This agent is interpreted by using R5-R6 in Figure 2 in terms of maximal parallelism, i.e., all the actions are executed in parallel. The first two tell of A1 and A2
can be simultaneously executed by using rule R1: the precondition (0̄⊗0̄) ⇓∅ = 0 6< 9
of the rule is then satisfied. The store does not change since 0̄ ⊗ 0̄ = 0̄. At this point,
the ask action of A2 is not enabled because 0̄ 6⊢ c1 , that is the precondition σ ⊢ c1
of R3 is not satisfied. Therefore, the processor can only be allocated to A1 and,
since (0̄ ⊗ 0̄) ⇓∅ = 0 6< +∞ is true (i.e. the precondition of R1 is satisfied), at t = 3
the computation is in the state:
htell(c2 ) → +∞ success k ask(c1 ) →9 success, 0̄i.
Now the tell can be executed because (0̄ ⊗ c2 ) ⇓∅ = 5 6< +∞: therefore, the store
becomes equal to 0̄ ⊗ c2 = c2 :
hsuccess k ask(c1 ) →9 success, c2 i.
At t = 5 (see Figure 5) we can successfully terminate the program: in the store
σ = c2 the ask is finally enabled at t = 4, according to the two preconditions of
rule R3, i.e., c2 ⊢ c1 and c2 ⇓∅ = 5 6< 9: therefore we have A1 k A2 :: hsuccess k
success, c2 i.

Fig. 5. The timeline of the execution of the A1 k A2 parallel agent in Example 2.

16

Bistarelli et al.

Example 3 (Timeout )
In this second example we evaluate a timeout construct. Suppose we have two
agents A1 and A2 of the form:
A1 :: ((ask(c1 ) → +∞ success) + (ask(c2 ) → +∞ success)) timeout(1)
ask(c1 ) → +∞ success
and
2

A2 :: tell(0̄) −→ +∞ tell(c3 ) → +∞ success
The description of agent A1 is a shortcut for the following agent, as previously
explained in the definition of the timeout:
now+∞ c1 then B else (now+∞ c2 then B else
(ask(1̄) → now+∞ c1 then B else
(now+∞ c2 then B else (ask(1̄) → ask(c1 ) → +∞ success)))).
where B :: (ask(c1 ) → +∞ success + ask(c2 ) → +∞ success). Their concurrent
evaluation in the 1̄ ≡ 0̄ empty store is:
h(B timeout(1) ask(c1 ) → +∞ success k
2

tell(0̄) −→ +∞ tell(c3 ) → +∞ success), 0̄i.
The timeline for this parallel execution is given in Figure 6. At t = 0 the store is
empty (i.e., σ = 0̄), thus both constraints c1 and c2 asked by the nondeterministic
choice agent A1 are not entailed. In A2 , the tell of c3 , which would entail both c1
and c2 , is delayed by three time-units: in the first three time-units, tell(0̄) →+∞
is executed according to the delay construct, as shown in Example 2. At t = 2 the
timeout is triggered in A1 , since, according to R1, R6 and R9 (see Figure 2), the
time elapsing in the timeout construct can be executed together with the delay-tell
actions of A2 . After the timeout triggering, agent A1 is however blocked, since c1 is
not entailed by the current empty store, and the precondition of the ask (rule R3)
is not satisfied. A2 can execute the last delay-tell, and then perform the tell(c3 )
operation at t = 3; the store becomes σ = 0̄ ⊗ c3 = c3 . This finally unblocks A1
at t = 4, since, according to the precondition of rule R3, σ ⊑ c1 (i.e., c3 ⊑ c1 ).
Finally, at t = 5 we have hsuccess k success, c3 i.

Fig. 6. The timeline of the execution of the A1 k A2 agent in Example 3.

TSCCP: An Interleaved and a Parallel Approach
t=0

t=1

17

t=2
Watch-else

tell (c1)

A1

A2

tell (c3)

tell (c2)

Fig. 7. The timeline of the execution of the A1 k A2 parallel agent in Example 4.
Example 4 (Watchdog)
In this example let
A1 :: do (tell(c1 ) → +∞ ask(c3 ) → +∞ success) watching+∞ (c2 ) else
( tell(c3 ) → +∞ success )
and
A2 :: tell(c2 ) →+∞ success.
We evaluate the following watchguard construct with two agents A1 and A2 in
parallel:
h(do (tell(c1 ) → +∞ ask(c3 ) → +∞ success) watching +∞ (c2 ) else
( tell(c3 ) → +∞ success ) k tell(c2 ) →+∞ success), 0̄i.
According to Figure 3, agent A1 is translated in the following way, where the
agent B is a shorthand for the “else” branch of the watchdog, that is tell(c3 ) →+∞
success:
now+∞ c2 then B else (tell(c1 ) →+∞ now+∞ c2 then B else
(ask(c3 ) →+∞ now+∞ c2 then B else success)).
The execution timeline for this parallel agent is shown in Figure 7. In the first
time-unit we have that σ = 0̄ 6⊑ c2 , i.e., the store does not imply the guard of the
now+∞ , and therefore the interruption of the watchguard in A1 is not triggered
yet. Thus, in the first time-unit, both tell(c1 ) →+∞ of agent A1 and tell(c2 ) →+∞
of agent A2 are executed. At time t = 1, the interruption of the watchguard is
immediately activated (i.e. now+∞ c2 ), since the store is now equal to c1 ⊗ c2 = c3
and c3 ⊢ c2 (rule R8 in Figure 2). Therefore, tell(c3 ) →+∞ of agent B in A1 is
executed, while A2 already corresponds to the success agent).
5.1 An Auction Example
In Figure 8 we model the negotiation and the management of a generic service
offered with a sort of auction: auctions, as other forms of negotiation, naturally need
both timed and quantitative means to describe the interactions among agents. We
reckon that an auction provides one of the most suitable example where to show the
expressivity of the tsccp language, since both time and preference (for a service or

18

Bistarelli et al.

an object) are considered. In the following of the description we consider a buyout
auction (Gallien and Gupta 2007), where the auctioneer improves the service and
the related consumed resources (or, alternatively, its money price), bid after bid.
When one (ore more) of the bidders agrees with the offer, it bids for it and the
auction is immediately declared as over.
The auctioneer (i.e. AUCTIONEER in Figure 8) begins by offering a service
described with the soft constraint cA1 . We suppose that the cost associated to
the soft constraint is expressed in terms of computational capabilities needed to
support the execution of the service: e.g., ci ⊑ cj means that the service described
by ci needs more computational resources than cj . By choosing the proper semiring,
this load can be expressed as a percentage of the CPU use, or in terms of money,
for example; we left this preference generic in the example, since we focus on the
interaction among the agents.
We suppose that a constraint can be defined over three domains of QoS features: availability, reliability and execution time. For instance, cA1 is defined as
availability > 95% ∧ reliability > 99% ∧ execution time < 3sec. Clearly, providing
a higher availability or reliability, and a lower execution time implies raising the
computational resources to support this improvement, thus worsening the preference of the store.
AUCTIONEER ::
INIT A −→
t

sell
tell(cA1 ) −→
(Σni=1 ask(bidderi = i ) →aA tell(winner = i ) → CHECK ) timeout(wA )

t

sell
(tell(cA2 ) −→
(Σni=1 ask(bidderi = i ) →aA tell(winner = i ) → CHECK ) timeout(wA )

t

sell
(tell(cA3 ) −→
(Σni=1 ask(bidderi = i ) →aA tell(winner = i ) → CHECK ) timeout(wA )
success))

CHECK ::
do ( (ask(service = end ) −→ success) timeout(wC ) tell(service = interrupt) )
watchingφCheck (ccheck ) else (tell(service = interrupt) −→ STOPC )
BIDDERi ::
INIT Bi −→
tbuy

do ( TASKi ) watchingφBidder (cBi ) else ask(1̄) −→i tell(bidderi = i ) −→
( (ask(winner = i ) −→ USERi ) + (ask(winner 6= i ) −→ success) )
USERi ::
do ( USE SERVICEi −→ tell(service = end ) −→ success )
watchingφU ser (service = interrupt) else (ST OPi )
AUCTION &MONITOR :: AUCTIONEER k BIDER1 k BIDDER2 k . . . k BIDDERn

Fig. 8. An “auction and management” example for a generic service
After the offer, the auctioneer gives time to the bidders (each of them described
with a possibly different agent BIDDERi in Figure 8) to make their offer, since the
choice of the winner is delayed by tsell time-units (as in many real-world auction
schemes). A level aA is used to effectively check that the global consistency of the
store is enough good, i.e., the computational power would not be already consumed
under the given threshold. After the winner is nondeterministically chosen among
all the bidders asking for the service, the auctioneer becomes a supervisor of the

TSCCP: An Interleaved and a Parallel Approach

19

used resource by executing the agent CHECK . Otherwise, if no offer is received
within wA time-units, a timeout interrupts the wait and the auctioneer improves
the offered service by adding a new constraint: for example, in tell(cA2 ), cA2 could
be equivalent to execution time < 1sec, thus reducing the latency of the service
(from 3 to 1 second) and consequently raising, at the same time, its computational
cost (i.e., σ = cA1 ⊗ cA2 ⊑ cA1 means that we worsen the consistency level of the
store). The same offer/wait process is repeated three times in Figure 8.
Each of the bidders in Figure 8 executes its own task (i.e., TASKi , left generic
since not in the scope of the example), but as soon as the offered resource meets
its demand (i.e. cBi is satisfied by the store: σ ⊑ cBi ), the bidder is interrupted
and then asks to use the service. The time needed to react and make an offer is
modeled with tbuyi : fast bidders will have more chances to win the auction, if their
request arrives before the choice of the auctioneer. If one of the bidders wins, then
it becomes a user of the resource, by executing USERi .
The agent USERi uses the service (through the agentUSE SERVICEi , left generic
in Figure 8), but it stops (using agent STOPi , left generic in Figure 8) as soon as
the service is interrupted, i.e., as the store satisfies service = interrupt. On the
other side, agent CHECK waits for the use termination, but it interrupts the user
if the computation takes too long (more than wC time-units), or if the user absorbs
the computational capabilities beyond a given threshold, i.e. as soon as the ccheck
becomes implied by the store (i.e. σ ⊑ ccheck ): in fact, USE SERVICEi could be
allowed to ask for more power by “telling” some more constraints to the store. To
interrupt the service use, agent CHECK performs a tell(service = interrupt). All
the agents INIT , left generic in Figure 8, can be used to initialize the computation.
In order to avoid a heavy notation in Figure 8, we do not show the preference associated to constraints and the consistency check label on the transition arrows, when
they are not significative for the example description. Also the φCheck , φBidder and
φUser thresholds of the watchguard constructs are not detailed.
Finally, in the following we model a more refined behaviour of the auctioneer,
which accepts the bidding with the highest value, where CHECK , BIDDERi and
USERi are defined as in Figure 8.
AUCTIONEER ′ ::
INIT A −→
t

sell
tell(cA1 ) −→
(Σni=1 ask(bidderi = i ) →aA CHOOSE ) timeout(wA )

t

sell
(tell(cA2 ) −→
(Σni=1 ask(bidderi = i ) →aA CHOOSE ) timeout(wA )

t

sell
(tell(cA3 ) −→
(Σni=1 ask(bidderi = i ) →aA CHOOSE ) timeout(wA ) success))

CHOOSE ::
now (biddern = n) then tell(winner = n) → CHECK
else ( now (biddern−1 = n − 1) then tell(winner = n − 1) → CHECK
else (. . . ( now (bidder2 = 2) then tell(winner = 2) → CHECK
else tell(winner = 1) → CHECK ) . . .)).
newAUCTION &MONITOR :: AUCTIONEER ′ k BIDER1 k BIDDER2 k . . . k BIDDERn

Fig. 9. A new “auction and management” example for a generic service
Many other real-life automated tasks can be modeled with the tsccp language.

20

Bistarelli et al.

For example, a quality-driven composition of web services: the agents that represent different web services can add to the store their functionalities (represented
by soft constraints) with tell actions; the final store models their composition. The
consistency level of the store represents (for example) the total monetary cost of
the obtained service, or a value representing the consistency of the integrated functionalities. The reason is that, when we compose the services offered by different
providers, we cannot be sure of how much they are compatible. A client wishing
to use the composed service can perform an ask with a threshold such that it prevents the client from paying a high price, or having an unreliable service. Softness is
also useful to model incomplete service specifications that may evolve incrementally
and, in general, for non-functional aspects.

6 The Denotational Model
In this section we define a denotational characterization of the operational semantics obtained by following the construction in (de Boer et al. 2000), and by using timed reactive sequences to represent tsccp computations. These sequences are
similar to those used in the semantics of dataflow languages (Jonsson 1985), imperative languages (Brookes 1993) and (timed) ccp (de Boer and Palamidessi 1991;
de Boer et al. 2000).
The denotational model associates with a process a set of timed reactive sequences
of the form hσ1 , γ1 i · · · hσn , γn ihσ, σi where a pair of constraints hσi , γi i represents a
reaction of the given process at time i: intuitively, the process transforms the global
store from σi to γi or, in other words, σi is the assumption on the external environment while γi is the contribution of the process itself (which always entails the
assumption). The last pair denotes a “stuttering step” in which the agent Success
has been reached. Since the basic actions of tsccp are monotonic and we can also
model a new input of the external environment by a corresponding tell operation,
it is natural to assume that reactive sequences are monotonic. Thus, in the following we assume that each timed reactive sequence hσ1 , γ1 i · · · hσn−1 , γn−1 ihσn , σn i
satisfies the conditions γi ⊢ σi and σj ⊢ γj −1 , for any i ∈ [1, n − 1] and j ∈ [2, n].
The set of all reactive sequences is denoted by S, its typical elements by s, s1 . . .,
while sets of reactive sequences are denoted by S , S1 . . ., and ε indicates the empty
reactive sequence. Furthermore, the symbol · denotes the operator that concatenates
sequences. In the following, Process denotes the set of tsccp processes.
Operationally, the reactive sequences of an agent are generated as follows.
Definition 3 (Processes Semantics)
We define the semantics R ∈ P rocess → P(S) by
R(F .A) =

{hσ, σ ′ i · w ∈ S | hA, σi −→ hB, σ ′ i and w ∈ R(F .B)}
∪
{hσ, σi · w ∈ S | hA, σi 6−→ and
either A 6= Success and w ∈ R(F .A)
or A = Success and w ∈ R(F .A) ∪ {ε}}.

TSCCP: An Interleaved and a Parallel Approach

21

Formally R is defined as the least fixed-point of the operator Φ ∈ (P rocess →
P(S)) → P rocess → P(S) defined by
Φ(I )(F .A) = {hσ, δi · w ∈ S | hA, σi −→ hB, δi and w ∈ I (F .B)}
∪
{hσ, σi · w ∈ S | hA, σi 6−→ and
either A 6= Success and w ∈ I (F .A)
or A = Success and w ∈ I (F .A) ∪ {ε}}.
The ordering on P rocess → P(S) is that of (point-wise extended) set-inclusion, and
since it is straightforward to check that Φ is continuous, standard results ensure
that the least fixpoint exists (and it is equal to ⊔n≥0 Φn (⊥)).
Note that R(F .A) is the union of the set of all successful reactive sequences that
start with a reaction of A, and the set of all successful reactive sequences that start
with a stuttering step of A. In fact, when an agent is blocked, i.e., it cannot react to
the input of the environment, a stuttering step is generated. After such a stuttering
step, the computation can either continue with the further evaluation of A (possibly
generating more stuttering steps), or it can terminate if A is the Success agent.
Note also that, since the Success agent used in the transition system cannot make
any move, an arbitrary (finite) sequence of stuttering steps is always appended to
each reactive sequence.
6.1 Correctness
mp
The observables Oio
(P ) describing the input/output pairs of successful computations can be obtained from R(P ) by considering suitable sequences, namely those
sequences which do not perform assumptions on the store. In fact, note that some
reactive sequences do not correspond to real computations: Clearly, when considering a real computation no further contribution from the environment is possible.
This means that, at each step, the assumption on the current store must be equal
to the store produced by the previous step. In other words, for any two consecutive
′
steps hσi , σi′ ihσi+1 , σi+1
i we must have σi′ = σi+1 . Thus, we are led to the following.

Definition 4 (Connected Sequences)
Let s = hσ1 , σ1′ ihσ2 , σ2′ i · · · hσn , σn i be a reactive sequence. We say that s is con′
nected if σ1 = 1 and σi = σi−1
for each i, 2 ≤ i ≤ n.
According to the previous definition, a sequence is connected if all the information
assumed on the store is produced by the process itself. To be defined as connected,
a sequence must also have 1 as the initial constraint. A connected sequence s =
h1, σ1 ihσ1 , σ2 i · · · hσn , σn i represents a tsccp computation of a process F .A, where
1 is the input constraint and σn ⇓Fv (A) is the result. From the above discussion we
can derive the following property:
Proposition 1 (Correctness)
For any process P = F .A we have
mp
Oio
(P ) = {σn ⇓Fv (A) | there exists a connected sequence s ∈ R(P ) such that
s = h1, σ1 ihσ1 , σ2 i · · · hσn , σn i}.

22

Bistarelli et al.

Proof
From the close correspondence between the rules of the transition system and the
definition of the denotational semantics, we have that s ∈ R(P ) if and only if
s = hσ1 , σ1′ ihσ2 , σ2′ i · · · hσn , σn i, A1 = A, An = Success and for i ∈ [1, n − 1],
• either hAi , σi i −→ hAi+1 , σi′ i
• or hAi , σi i 6−→, Ai+1 = Ai and σi′ = σi .
Then there exists a connected sequence s ∈ R(P ) if and only if s = hσ1 , σ2 ihσ2 , σ3 i
· · · hσn , σn i, A1 = A, σ1 = 1, An = Success and for i ∈ [1, n − 1], hAi , σi i −→
mp
hAi+1 , σi+1 i. Therefore, the proof follows by definition of Oio
(P ).

6.2 Compositionality of the Denotational Semantics for tsccp
Processes
In order to prove the compositionality of the denotational semantics, we now introduce a semantics [[F .A]](e), which is compositional by definition and where, for
technical reasons, we explicitly represent the environment e that associates a denotation to each procedure identifier. More precisely, assuming that Pvar denotes
the set of procedure identifiers, Env = P var → P(S), with typical element e, is
the set of environments. Given e ∈ Env , p ∈ P var and f ∈ P(S), we denote by
e ′ = e{f /p} the new environment such that e ′ (p) = f and e ′ (p ′ ) = e(p ′ ) for each
procedure identifier p ′ 6= p.
Given a process F .A, the denotational semantics [[F .A]] : Env → P(S) is defined
by the equations in Figure 10, where µ denotes the least fixpoint with respect
to the subset inclusion of elements of P(S). The semantic operators appearing in
Figure 10 are formally defined as follows; intuitively they reflect the operational
behavior of their syntactic counterparts in terms of reactive sequences.5 We first
need the following definition.
Definition 5
Let σ, φ and c be constraints in C and let a ∈ A. We say that
• σ ≻a c, if (σ ⊢ c and σ ⇓∅ 6< a)

while

σ ≻φ c, if (σ ⊢ c and σ 6⊏ φ).

Definition 6 (Semantic operators)
Let S , Si be sets of reactive sequences, c, ci be constraints and let ≻i be either
˜ , P̃, k̃, now
˜ as
of the form ≻ai or ≻φi . Then we define the operators tell
˜ and ∃x
follows:
The (valued) tell operator

5

˜ a (c, S ) =
tell

{s ∈ S | s = hσ, σ ⊗ ci · s ′ , σ ⊗ c ⇓∅ 6< a and s ′ ∈ S }.

˜ φ (c, S ) =
tell

{s ∈ S | s = hσ, σ ⊗ ci · s ′ , σ ⊗ c 6⊏ φ and s ′ ∈ S }.

In Figure 10 the syntactic operator →i is either of the form →ai or →φi .

TSCCP: An Interleaved and a Parallel Approach

23

The guarded choice
X̃n
ci ≻i Si = {s · s ′ ∈ S | s = hσ1 , σ1 i · · · hσm , σm i, σj 6≻i ci
i=1
for each j ∈ [1, m-1], i ∈ [1, n],
σm ≻h ch and s ′ ∈ Sh for an h ∈ [1, n] }.
The parallel composition Let k̃ ∈ S × S → S be the (commutative and associative) partial operator defined as follows:
hσ1 , σ1 ⊗ γ1 i · · · hσn , σn ⊗ γn ihσ, σi k̃ hσ1 , σ1 ⊗ δ1 i · · · hσn , σn ⊗ δn ihσ, σi
hσ1 , σ1 ⊗ γ1 ⊗ δ1 i · · · hσn , σn ⊗ γn ⊗ δn ihσ, σi.

=

We define S1 k̃S2 as the point-wise extension of the above operator to sets.
The (valued) now operator
now
˜ a (c, S1 , S2 ) = {s ∈ S | s = hσ, σ ′ i · s ′ , σ ⇓∅ 6< a and
either σ ⊢ c and s ∈ S1
or σ 6⊢ c and s ∈ S2 }.
now
˜ φ (c, S1 , S2 ) = {s ∈ S | s = hσ, σ ′ i · s ′ , σ 6⊏ φ and
either σ ⊢ c and s ∈ S1
or σ 6⊢ c and s ∈ S2 }.
The hiding operator The semantic hiding operator can be defined as follows:
˜
∃xS = {s ∈ S | there exists s ′ ∈ S such that s = s ′ [x /y] with y new }
where s ′ [x /y] denotes the sequence obtained from s ′ by replacing the variable x for
the variable y, which we assume to be new.6
Obviously, the semantic (valued) tell operator reflects the operational behavior
of the syntactic (valued) tell. Concerning the semantic choice operator, a sequence
P̃n
in i=1 ci ≻i Si consists of an initial period of waiting for a store which satisfies
one of the guards. During this waiting period, only the environment is active by
producing the constraints σj , while the process itself generates the stuttering steps
hσj , σj i. When the store is strong enough to satisfy a guard, that is to entail a ch
and to satisfy the condition on the cut level, the resulting sequence is obtained
by adding s ′ ∈ Sh to the initial waiting period. In the semantic parallel operator
defined on sequences, we require that the two arguments of the operator agree at
each point of time with respect to the contribution of the environment (the σi ’s),
and that they have the same length (in all other cases the parallel composition is
assumed being undefined).
If F .A is a closed process, that is if all the procedure names occurring in A are
defined in F , then [[F .A]](e) does not depend on e, and it will be indicated as
[[F .A]]. Environments in general allow us to define the semantics also of processes
that are not closed. The following result shows the correspondence between the
two semantics we have introduced and, therefore, it proves the compositionality of
R(F .A). From the above discussion we can derive the following property:
6

To be more precise, we assume that each time that we consider a new application of the operator
˜
∃ we use a new, different y. As in the case of the operational semantics, this can be ensured by
a suitable renaming mechanism.

24

Bistarelli et al.

Proposition 2 (Compositionality)
If F .A is closed then R(F .A) = [[F .A]] holds.
Proof
We prove by induction on the complexity of the agent A that
[[F .A]] = {s | s = hσ1 , σ1′ ihσ2 , σ2′ i · · · hσn , σn i,
A1 = A, An = Success and for i ∈ [1, n − 1],
either hAi , σi i −→ hAi+1 , σi′ i
or hAi , σi i 6−→, Ai+1 = Ai , σi′ = σi }.
Then the proof follows by definition of R(P ).
When the P is not of the form F .B k C the thesis follows immediately from the
close correspondence between the rules of the transition system and the definition
of the denotational semantics.
Assume now that P is of the form F .B k C . By definition of the denotational
semantics, s ∈ [[F .A]] if and only if s = hσ1 , σ1′ ihσ2 , σ2′ i · · · hσn , σn i and there exist
s ′ ∈ [[F .B ]] and s ′′ ∈ [[F .C ]],
s ′ = hσ1 , σ1 ⊗ γ1 ihσ2 , σ2 ⊗ γ2 i · · · hσn , σn i
s ′′ = hσ1 , σ1 ⊗ δ1 ihσ2 , σ2 ⊗ δ2 i · · · hσn , σn i
such that for each i ∈ [1, n −1], σi′ = σi ⊗γi ⊗δi . By inductive hypothesis s ′ ∈ [[F .B ]]
and s ′′ ∈ [[F .C ]] if and only if for i ∈ [1, n − 1],
either hBi , σi i −→ hBi+1 , σi ⊗ γi i,
or hBi , σi i 6−→, Bi+1 = Bi , σi ⊗ γi = σi and
either hCi , σi i −→ hCi+1 , σi ⊗ δi i,
or hCi , σi i 6−→, Ci+1 = Ci , σi ⊗ δi = σi .

(1)

B1 = B , Bn = Success, C1 = C and Cn = Success. Therefore, by Rule R8 and
previous observations, we have that (1) holds if and only if B1 k C1 = B k C ,
Bn k Cn = Success and for i ∈ [1, n − 1],
either hBi k Ci , σi i −→ hBi+1 k Ci+1 , σi′ i
or hBi k Ci , σi i 6−→, Ai+1 k Bi+1 = Ai k Bi , σi′ = σi
and then the thesis.

7 An Interleaving Approach for non-Time-elapsing Actions
In this section, we show a different version of the tsccp language: while in tsccp the
parallel operator is modeled in terms of maximal parallelism, the same operator
can be treated also in terms of interleaving. According to maximal parallelism, at
each moment every enabled agent of the system is activated, while in the second
paradigm an agent could not be assigned to a “free” processor. Clearly, since we
have dynamic process creation, a maximal parallelism approach has the disadvantage that, in general, it implies the existence of an unbound number of processes.
On the other hand a naive interleaving semantic could be problematic from the

TSCCP: An Interleaved and a Parallel Approach
E1

[[F .success]](e) = {hσ1 , σ1 ihσ2 , σ2 i · · · hσn , σn i ∈ S | n ≥ 1}

E2

˜ a (c, [[F .A]](e))
[[F .tell(c) →a A]](e) = tell

E3

˜ φ (c, [[F .A]](e))
[[F .tell(c) →φ A]](e) = tell

E4

[[F .

E5

[[F .nowa c then A else B]](e) = now
˜ a (c, [[F .A]](e), [[F .B]](e))

E6

[[F .nowφ c then A else B]](e) = now
˜ φ (c, [[F .A]](e), [[F .B]](e))

E7

[[F .A k B]](e) = [[F .A]](e) k̃ [[G.B]](e)

E8

˜ [[F .A]](e)
[[F .∃xA]](e) = ∃x

E9

[[F .p(x)]](e) = µΨ where Ψ(f ) = [[F \ {p}.ask (1̄) → A]](e{f /p}), p(x ) :: A ∈ F

Pn

i= ask(ci )

→i Ai ]](e) =

P̃n

i=1 ci

25

≻i [[F .Ai ]](e)

Fig. 10. The semantics [[F .A]](e).

time viewpoint, as in principle the time does not pass for enabled agent which are
not scheduled. For the semantics in this section we follow a solution analogous to
that one adopted in (de Boer et al. 2004): we assume that the parallel operator
is interpreted in terms of interleaving, as usual, however we must assume maximal parallelism for actions depending on time. In other words, time passes for all
the parallel processes involved in a computation. To summarize, in this section we
adopt maximal parallelism for time elapsing (i.e. for timeout constructs) and an
interleaving model for basic computation steps (i.e. (valued) ask and (valued) tell
actions).
To distinguish this new approach, we named the resulting language as tsccpi, i.e., tsccp with interleaving. Time-outs are modeled in tsccp-i by the construct
askpt (c)?φ A:B which replaces the nowφ c then A else B construct of tsccp and
directly has time t as one of its parameters, differently from the nowφ agent.
The askpt agent can be interpreted as follows: one is allowed to wait t time-units
for the entailment of the constraint c by the store and the subsequent evaluation
of the process A; if this time limit is exceeded, then the process B is evaluated.
Analogously for the construct askpt (c)?a A:B .

Definition 7 (tsccp-i)
Given a soft constraint system hS , D , V i, the corresponding structure C, any semir-

26

Bistarelli et al.

ing value a, soft constraints φ, c ∈ C and any tuple of variables x , the syntax of the
tsccp-i language is given by the following grammar:
P ::=
F ::=
A ::=
E ::=

F .A
p(x ) :: A | F · F
success | tell(c) →φ A | tell(c) →a A | E | A k A | ∃xA | p(x ) |
Σni=1 Ei | askpt (c)?φ A:A | askpt (c)?a A:A
ask(c) →φ A | ask(c) →a A

where, as in Definition 1, P is the class of processes, F is the class of sequences of
procedure declarations (or clauses), A is the class of agents. As before, in a tsccp-i
process P = F .A, A is the initial agent, to be executed in the context of the set of
declarations F .
Analogously to tsccp processes, in order to simplify the notation, in the following
we will usually write a tsccp-i process P = F .A simply as the corresponding agent
A.
The operational model of tsccp-i processes can be formally described by a labeled
transition system T = (Conf , Label , 7−→), where we assume that each transition
step exactly takes one time-unit. Configurations (in) Conf are pairs consisting of
a process and a constraint in C representing the common store. L = {τ, ω} is the
set of labels. We use labels to distinguish “real” computational steps performed by
processes which have the control (label ω) from the transitions which model only
the passing of time (label τ ). So ω-actions are those performed by processes that
modify the store (tell), perform a check on the store (ask, askpt ), correspond to
exceeding a time-out (askp0 ), or perform a choice (Σni=1 Ei ). On the other hand,
τ -actions are those performed by time-out processes (askpt ) in case they have not
the control. In Figure 11 we show the semantics of all the tsccp-i actions, but in the
following we describe only the actions whose semantics is different from that one
presented in Figure 2 (i.e., for tsccp), that is we describe in detail the parallelism
and the askpt agent. The semantics of the other actions of tsccp-i is the same as
for tsccp, except for the fact that their transition is labeled with ω.
Parallelism Rules Q5 and Q6 in Figure 11 model the parallel composition operator in terms of interleaving, since only one basic ω-action is allowed for each
transition (i.e. for each unit of time). This means that the access to the shared
store is granted to one process a time. However, time passes for all the processes
appearing in the k context at the external level, as shown by rule Q5, since
τ -actions are allowed together with a ω-action. On the other hand, a parallel
component is allowed to proceed in isolation if (and only if) the other parallel
component cannot perform a τ -action (rule Q6). To summarize, we adopt maximal parallelism for time elapsing (i.e. τ -actions) and an interleaving model for
basic computation steps (i.e. ω-actions).
We have adopted this approach because it seems more adequate to the nature
of time-out operators not to interrupt the elapsing of time, once the evaluation
of a time-out has started. Clearly one could start the elapsing of time when the
time out process is scheduled, rather than when it appears in the top-level current

TSCCP: An Interleaved and a Parallel Approach
Q1

(σ ⊗ c) ⇓∅ 6< a
ω
htell(c) →a A, σi 7−→ hA, σ ⊗ ci

V-tell

Q2

σ ⊗ c 6⊏ φ
ω
htell(c) →φ A, σi 7−→ hA, σ ⊗ ci

Tell

Q3

σ⊢c
σ ⇓∅ 6< a
ω
hask(c) →a A, σi 7−→ hA, σi

V-ask

Q4

σ ⊢ c σ 6⊏ φ
ω
hask(c) →φ A, σi 7−→ hA, σi

Ask

ξ

Q5

τ

hA, σi 7−→ hA′ , σ ′ i

hB , σi 7−→ hB ′ , σi

ξ ∈ {τ, ω}

ξ

hA k B , σi 7−→ hA′ k B ′ , σ ′ i

Parall1

ξ

hB k A, σi 7−→ hB ′ k A′ , σ ′ i
ξ

Q6

τ

hA, σi 7−→ hA′ , σ ′ i

hB , σi 67−→
ξ

ξ ∈ {τ, ω}

Parall2

′

hA k B , σi 7−→ hA k B , σ ′ i
ξ

hB k A, σi 7−→ hB k A′ , σ ′ i
ω

Q7

hEj , σi 7−→ hAj , σ ′ i
j ∈ [1, n]
ω
hΣni=1 Ei , σi 7−→ hAj , σ ′ i

Q8

hp(x ), σi 7−→ hA, σi

ω

p(x) :: A ∈ F

ξ

Q9

Nondet

hA[x /y], σi 7−→ hB , σ ′ i

P-call

ξ ∈ {τ, ω}

Hide

ξ

h∃xA, σi 7−→ hB , σ ′ i

Q10

σ ⊢ c σ ⇓∅ 6< a t > 0
ω
haskpt (c)?a A:B , σi 7−→ hA, σi

V-askp1

Q11

σ ⇓∅ < a t > 0
ω
haskpt (c)?a A:B , σi 7−→ hB , σi

V-askp2

Q12

σ 6⊢ c σ ⇓∅ 6< a t > 0
ω
haskpt (c)?a A:B , σi 7−→ haskpt −1 (c)?a A:B , σi

V-askp3

Q13

haskpt (c)?a A:B , σi 7−→ haskpt −1 (c)?a A:B , σi

Q14

haskp0 (c)?a A:B , σi 7−→ hB , σi

V-askp5

Q15

σ ⊢ c σ 6⊏ φ t > 0
ω
haskpt (c)?φ A:B , σi 7−→ hA, σi

Askp1

Q16

σ⊏φ t >0
ω
haskpt (c)?φ A:B , σi 7−→ hB , σi

Askp2

Q17

σ 6⊢ c σ 6⊏ φ t > 0
ω
haskpt (c)?φ A:B , σi 7−→ haskpt −1 (c)?φ A:B , σi

Askp3

Q18

haskpt (c)?φ A:B , σi 7−→ haskpt −1 (c)?φ A:B , σi

Q19

haskp0 (c)?φ A:B , σi 7−→ hB , σi

τ

t >0

ω

τ

ω

Fig. 11. The transition system for tsccp-i.

t >0

V-askp4

Askp4
Askp5

27

28

Bistarelli et al.

parallel context. This modification could easily be obtained by adding a syntactic
construct to differentiate active timeouts from inactive ones, and by accordingly
changing the transition system. One could also easily modify the semantics (both
operational and denotational) to consider a more liberal assumption which allows
multiple ask actions in parallel.
Valued-Askpt The rules Q10-Q14 in Figure 11 show that the time-out process
askpt (c)?a A:B behaves as A if c is entailed by the store and the store is “consistent enough” with respect to the threshold a in the next t time-units: if t > 0
and the condition on the store and the cut level are satisfied, then the agent A
is evaluated (rule Q10). If t > 0 and the condition on the cut level is not satisfied, then the agent B is evaluated (rule Q11). Finally if t > 0, the condition
on the cut level is satisfied, but the condition on the store is not satisfied, then
the control is repeated at the next time instant and the value of the counter t is
decreased (axiom Q12); note that in this case we use the label ω, since a check
on the store has been performed. As shown by axiom Q13, the counter can be
decreased also by performing a τ -action: intuitively, this rule is used to model the
situation in which, even though the evaluation of the time-out started already, another (parallel) process has the control. In this case, analogously to the approach
in (de Boer et al. 2004) and differently from the approach in (Busi et al. 2000),
time continues to elapse (via τ -actions) also for the time-out process (see also the
rules Q5 and Q6 of the parallel operator). Axiom Q14 shows that, if the timeout is exceeded, i.e., the counter t has reached the value of 0, then the process
askpt (c)?a A:B behaves as B .
Askpt The rules Q15-Q19 in Figure 11 are similar to rules Q10-Q14 described
before, with the exception that here a finer (pointwise) threshold φ is compared
to the store σ, analogously to what happens with the tell and ask agents.
In the following we provide the definition for the observables of the language,
which are clearly based only on ω-actions.
Definition 8 (Observables for tsccp-i)
Let P = F .A be a tsccp-i process. We define
ω ∗

i
Oio
(P ) = {γ ⇓Fv (A) | hA, 1̄i 7−→ hSuccess, γi},

where Success is any agent that contains only occurrences of the agent success
and of the operator k.
8 An Execution Timeline for a tsccp-i Parallel Agent
In this section we show a timeline for the execution of three tsccp-i agents in parallel.
We consider the three soft constraints shown in Figure 4 and the Weighted semiring
h + ∪ {+∞}, min, +, +∞, 0i (Bistarelli 2004; Bistarelli et al. 1997). Our parallel
agent is defined by:

R

A1 :: askp5 (c3 )?+∞ (tell(c1 ) →+∞ success):(success)
A2 :: tell(c1 ) →+∞ success
A3 :: tell(c2 ) →+∞ success.

TSCCP: An Interleaved and a Parallel Approach

29

Their concurrent evaluation in the 0̄ empty store is shown in Figure 12. At t = 0
and t = 1 the agent A1 can make a τ -transition (rule Q13 in Figure 11), waiting
for the elapsing of 1 time-unit. This can be done in parallel with a single other ωaction: therefore, the tell(c1 ) of agent A2 , and the tell(c2 ) of agent A3 cannot run
in parallel at the same time, since they are both ω-actions. In the execution shown
in Figure 12, A2 is executed before A3 (also the opposite is possible, depending
on the scheduling), leading to the store σ = c1 ⊗ c2 = c3 . At t = 2, the guard of
askp5 in agent A1 is enabled since σ ⊢ c3 and, therefore, rule Q10 in Figure 11 is
executed. Finally, at t = 3 the tell(c1 ) action of agent A1 is executed as the last
action, and at t = 4 we have hsuccess k success k success, c1 ⊗ c2 ⊗ c1 i.

Fig. 12. A timeline for the execution of A1 k A2 k A3 .

9 Denotational Semantics for tsccp-i
In this section we define a denotational characterization of the operational semantics for tsccp-i. Differently from the denotational semantics for the maximal parallelism version presented in Section. 6.2, here for computational states we consider
triples rather than pairs, as ω-actions have to be distinguished from τ -actions. This
difference leads to a different technical development.
Our denotational model for tsccp-i associates with a process a set of timed reactive sequences of the form hσ1 , γ1 , ξ1 i · · · hσn , γn , ξn ihσ, σ, ωi. Any triple hσi , γi , ξi i
represents a reaction (a computation step) of the given process at time i: intuitively,
the process transforms the global store from σi to γi by performing a transition step
labeled by ξi or, in other words, σi is the assumption on the external environment,
ξi is the label of the performed step while γi is the contribution of the process
itself (which entails always the assumption). The last pair denotes a “stuttering
step”, in which the agent Success has been reached. In the following we will assume that each timed reactive sequence hσ1 , γ1 , ξ1 i · · · hσn−1 , γn−1 , ξn−1 ihσn , σn , ωi
satisfies the following condition: γi ⊢ σi and σj ⊢ γj −1 , for any i ∈ [1, n − 1] and
j ∈ [2, n].
The basic idea underlying the denotational model then is that, differently from
the operational semantics, inactive processes can always make a τ -step, where an
inactive process is either suspended (due to the absence of the required constraint
in the store) or it is a non-scheduled component of a parallel construct. These

30

Bistarelli et al.

additional τ -steps, which represent time-elapsing and are needed to obtain a compositional model in a simple way, are then added to denotations as triples of the
form hσ, σ, τ i. For example, the denotation of the process tell(c) →a success contains all the reactive sequences that have, as first element, a triple hσ, σ ⊗ c, ωi for
any possible initial store σ with (σ ⊗ c) ⇓∅ 6< a, as these represent the action of
adding the constraint c to the current store. However, such a denotation contains
also sequences where the triple hσ, σ ⊗ c, ωi (still with (σ ⊗ c) ⇓∅ 6< a) is preceded
by a finite sequence of triples of the form hσ1 , σ1 , τ ihσ2 , σ2 , τ i . . . hσn , σn , τ i. Such a
sequence represents time-elapsing while the process is inactive because some other
parallel process is scheduled.
The set of all reactive sequences for tsccp-i process is denoted by Si , its typical
elements by s, s1 . . ., while sets of reactive sequences are denoted by S , S1 . . . and
ε indicates the empty reactive sequence. The operator · denotes the operator that
concatenates these sequences.

9.1 Compositionality of the Denotational Semantics for tsccp-i
Processes
As in Section 6.2 for the tsccp version, we now introduce a denotational semantics
D(F .A)(e) which is compositional by definition and where, for technical reasons, we
represent explicitly the environment e which associates a denotation to each procedure identifier. More precisely, assuming that Pvar denotes the set of procedure
identifier, Env i = P var → P(Si ), with typical element e, is the set of environments. Analogously to Section 6.2, given e ∈ Env i , p ∈ P var and f ∈ P(Si ), we
denote by e ′ = e{f /p} the new environment such that e ′ (p) = f and e ′ (p ′ ) = e(p ′ )
for each procedure identifier p ′ 6= p.
Before defining formally the denotational semantics, we need to define the op¯ , P̄, k̄, askp
¯ and ∃x
¯ , analogous to those given in Section 6.2 for the
erators tell
maximal parallelism language.
Definition 9 (Semantic operators for tsccp-i)
Let S , Si be sets of reactive sequences, c, ci be constraints. Moreover let ≻i be either
of the form ≻ai or ≻φi , defined as in Definition 5. Then we define the operators
¯ , P̄, k̄, askp
¯ and ∃x
¯ as follows:
tell
¯ a : C × ℘(Si ) → ℘(Si ) (tell
¯ φ : C × ℘(Si ) → ℘(Si ))
The (valued) tell operator tell
is the least function (w.r.t. the ordering induced by ⊆) which satisfies the following
equation
¯ a (c, S ) =
tell

{s ∈ Si | s = hσ, σ ⊗ c, ωi · s ′ , σ ⊗ c ⇓∅ 6< a and s ′ ∈ S } ∪
¯ a (c, S ) }.
{s ∈ Si | s = hσ, σ, τ i · s ′ and s ′ ∈ tell

¯ φ (c, S ) = {s ∈ Si | s = hσ, σ ⊗ c, ωi · s ′ , σ ⊗ c 6⊏ φ and s ′ ∈ S } ∪
tell
¯ φ (c, S ) }.
{s ∈ Si | s = hσ, σ, τ i · s ′ and s ′ ∈ tell
The guarded choice The semantic choice operator

TSCCP: An Interleaved and a Parallel Approach

31

P̄n

: (C × ℘(Si )) × · · · × (C × ℘(Si )) → ℘(Si ) is the least function which satisfies
the following equation:
i=1

X̄n

i=1

ci ≻i Si = {s ∈ Si | s = hσ, σ, ωi · s ′ ,
σ ≻h ch and s ′ ∈ Sh for an h ∈ [1, n] }
∪
P̄n
{s ∈ Si | s = hσ, σ, τ i · s ′ and s ′ ∈ i=1 ci ≻i Si }.

Parallel Composition. Let k̄ ∈ Si ×Si → Si be the (commutative and associative)
partial operator defined by induction on the length of the sequences as follows:
hσ, σ, ωik̄hσ, σ, ωi = hσ, σ, ωi
hσ, σ ′ , x i · s k̄hσ, σ, τ i · s ′ = hσ, σ, τ i · s ′ k̄hσ, σ ′ , x i · s = hσ, σ ′ , x i · (s k̄s ′ ),
where x ∈ {ω, τ }.
We define the operator S1 k̄S2 on sets as the image of Si × Si under the above
operator.
¯ ) :
¯
The (valued) askp operator askp(t
)a : C × ℘(Si ) × ℘(Si ) → ℘(Si ) (askp(t
φ
C × ℘(Si ) × ℘(Si ) → ℘(Si )), with t > 0, is defined as:
¯
askp(t
)a (c, S1 , S2 ) =

{s ∈ Si | s = hσ, σ, ωi · s ′ and
either σ ≻a c and s ∈ S1
or σ ⇓∅ < a and s ∈ S2 } ∪
¯
{s ∈ Si | s = hσ, σ, x i · s ′ , s ′ ∈ askp(t
− 1)a (c, S1 , S2 )
and either x = τ
or x = ω, σ 6⊢ c and σ ⇓∅ 6< a }.

¯
askp(t
)φ (c, S1 , S2 ) =

{s ∈ Si | s = hσ, σ ′ , ωi · s ′ and
either σ ≻φ c and s ∈ S1
or σ ⊏ φ and s ∈ S2 } ∪
¯
{s ∈ Si | s = hσ, σ, x i · s ′ , s ′ ∈ askp(t
− 1)φ (c, S1 , S2 )
and either x = τ
or x = ω, σ 6⊢ c and σ 6⊏ φ }.

a
¯
¯
The (valued) askp operator askp(0)
: C × ℘(Si ) × ℘(Si ) → ℘(Si ) (askp(0)
φ :
C×℘(Si )×℘(Si ) → ℘(Si )) is the least function which satisfies the following equation
a
¯
askp(0)
(c, S1 , S2 ) =

{s ∈ Si | either s = hσ, σ, ωi · s ′ and s ′ ∈ S2
or s = hσ, σ, τ i · s ′
a
¯
and s ′ ∈ askp(0)
(c, S1 , S2 ) }.

¯
askp(0)
φ (c, S1 , S2 ) =

{s ∈ Si | either s = hσ, σ, ωi · s ′ and s ′ ∈ S2
or s = hσ, σ, τ i · s ′
¯
and s ′ ∈ askp(0)
φ (c, S1 , S2 ) }.

The hiding operator The semantic hiding operator can be defined as follows:
¯
∃xS = {s ∈ Si | there exists s ′ ∈ S such that s = s ′ [x /y] with y new }

32

Bistarelli et al.

where s ′ [x /y] denotes the sequence obtained from s ′ by replacing the variable x for
the variable y that we assume to be new.7
It is immediate to see that the previous semantic operators are well defined,
that is, the least function which satisfies the equations actually exists and can be
¯ , P̄, k̄, askp
¯ and ∃x
¯ operators
obtained by a standard fix-point construction. The tell
have the expected definition, including the mentioned addition of τ -steps.
In the semantic parallel operator (acting on sequences) we require that at each
point of time at most one ω-action is present and the two arguments of the operator
agree with respect to the contribution of the environment (the first component of
the triple). We also require that the two arguments have the same length (in all
other cases the parallel composition is assumed being undefined): this is necessary
to reflect the passage of time since the i − th element of any sequence corresponds
to the given processes action on the i − th time step. Even though we merge pointwise sequences of the same length, this models an interleaving approach for ωactions, because of the previously mentioned addition of τ -steps to denotations.
P̄n
Concerning the semantic choice operator, a sequence in i=1 ci ≻i Si consists of
an initial period of waiting for a store which satisfies one of the guards. During this
waiting period, only the environment is active by producing the constraint σ, while
the process itself generates the stuttering steps hσ, σ, τ i. When the store is strong
enough to satisfy a guard, that is to entail a ch and to satisfy the condition on the
cut level, then the resulting sequence is obtained by adding s ′ ∈ Sh to the initial
waiting period.
We can define the denotational semantics D as follows. Here, Processi denotes
the set of tsccp-i processes.
Definition 10 (Processes Semantics)
We define the semantics D ∈ P rocessi → P(Si ) is the least function with respect to
the ordering induced by the set-inclusion, which satisfies the equations in Figure 13
Also D is well defined and can be obtained by a fix-point construction. To see
this, let us define an interpretation as a mapping I : Processi → ℘(Si ). Then let
us denote by I the cpo of all the interpretations (with the ordering induced by ⊆).
To the equations in Figure 13, we can then associate a monotonic (and continuous)
mapping F : I → I defined by the equations of Figure 13, provided that we replace
the symbol D for F (I ), we delete the environment e and that we replace equation
F9 for the following one: F (I )(F .p(x)) = I (F .ask (1̄) → A).
Then, one can easily prove that a function satisfies the equations in Figure 13 iff
it is a fix-point of the function F . Because this function is continuous (on a cpo),
well known results ensure us that its least fix-point exists and it equals F ω , where
the powers are defined as follows: F 0 = I0 (this is the least interpretation which
maps any process to the empty set); F n = F (F n−1 ) and F ω = lub{F n |n ≥ 0}
(where lub is the least upper bound on the cpo I).
7

As before, we assume that each time that we consider a new applications of the operator ¯
∃ we
use a new, different y.

TSCCP: An Interleaved and a Parallel Approach
F1

D(F .success)(e) = {hσ1 , σ1 , τ ihσ2 , σ2 , τ i · · · hσn , σn , ωi ∈ Si | n ≥ 1}

F2

¯ (c, D(F .A)(e))
D(F .tell(c) →a A)(e) = tell

F3

¯ φ (c, D(F .A)(e))
D(F .tell(c) →φ A)(e) = tell

F4

D(F .

F5

a
¯
D(F .askpt (c)?a A:B)(e) = askp(t)
(c, D(F .A)(e), D(F .B)(e))

F6

¯
D(F .askpt (c)?φ A:B)(e) = askp(t)
φ (c, D(F .A)(e), D(F .B)(e))

F7

D(F .A k B)(e) = D(F .A)(e) k̄ D(F .B)(e)

F8

¯ D(F .A)(e)
D(F .∃xA)(e) = ∃x

F9

D(F .p(x))(e) = µΨi where Ψi (f ) = D(F \ {p}.ask (1̄) → A)(e{f /p}),
p(x ) :: A ∈ F

33

a

Pn

i= ask(ci )

→i Ai )(e) =

P̃n

i=1 ci

≻i D(F .Ai )(e)

Fig. 13. The semantics D (F .A)(e) for tsccp-i.
9.2 Correctness of the Denotational Semantics for tsccp-i Processes
As for the correctness of the denotational semantics presented in Section 6.1,
at each step, the assumption on the current store must be equal to the store
produced by the previous step. In other words, for any two consecutive steps
′
hσi , σi′ , xi ihσi+1 , σi+1
, xi+1 i we must have σi′ = σi+1 . Furthermore, triples containing τ -actions do not correspond to observable computational steps, as these involve
ω-actions only.
Definition 11 (Connected Sequences in tsccp-i)
Let s = hσ1 , σ1′ , x1 ihσ2 , σ2′ , x2 i · · · hσn , σn , ωi be a reactive sequence. We say that
′
s is connected if σ1 = 1̄, σi = σi−1
and xj = ω for each i, j , 2 ≤ i ≤ n and
1 ≤ j ≤ n − 1.
According to the previous definition, a sequence is connected if all the information
assumed on the tuple space is produced by the process itself and only ω-actions
are involved. To be defined as connected, a sequence must also have 1̄ as the initial
constraint. A connected sequence represents a tsccp-i computation, as it will be
proved in the remaining of this section.
In order to prove the correctness of the denotational semantics, we use a modified
transition system T ′ , where inactive (either suspended or not scheduled) processes
can perform τ -actions. When considering our notions of observables, we can prove
that such a modified transition system is equivalent to the previous one and agrees
with the denotational model.
The new transition system T ′ is obtained from the one in Figure 11 by deleting
rule Q6 and by adding the rules Q0’, Q1’, Q2’, Q3’, Q4’, Q7’, Q8’, Q14’ and
Q19’, contained in Figure 14. We denote by ⇒ the relation defined by T ′ .
The observables induced by the transition system T ′ are formally defined as
follows.

34

Bistarelli et al.
τ

Q0’

hsuccess, σi ⇒ hsuccess, σi

Q1’

htell(c) →a A, σi ⇒ htell(c) →a A, σi

Q2’

htell(c) →φ A, σi ⇒ htell(c) →φ A, σi

Q3’

hask(c) →a A, σi ⇒ hask(c) →a A, σi

Q4’

hask(c) →φ A, σi ⇒ hask(c) →φ A, σi

Q7’

hΣni=1 Ei , σi ⇒ hΣni=1 Ei , σi

τ

V-Telll

τ

Tell

τ

V-ask

τ

Ask

τ

τ

success

Q8’

hp(x ), σi ⇒ hA, σi

p(x) :: A ∈ F

Q14’

haskp0 (c)?a A:B , σi ⇒ haskp0 (c)?a A:B , σi

Q19’

haskp0 (c)?φ A:B , σi ⇒ haskp0 (c)?φ A:B , σi

τ

τ

Nondet
P-call
V-askp5
Askp5

Fig. 14. The τ -rules for tsccp-i.
Definition 12
Let P = F .A be a tsccp-i process. We define
ω

′

i
Oio
(P ) = {γ ⇓Fv (A) | hA, 1̄i ⇒ ∗ hSuccess, γi},

where Success is any agent which contains only occurrences of the agent success
and of the operator k.
Lemma 3 shows that the modified transition system agrees with the original one
when considering our notion of observables.
We first need some definitions and technical lemmata. In the following, given two
agents A and B , we say that A ≃ B if and only if B is obtained from A by replacing
an agent of the form ∃xA1 in A with A1 [x /y], where y is new in A. ≈ denotes the
reflexive and transitive closure of ≃. The following lemmata hold.
Lemma 1
Let F .A and F .B be tsccp-i processes such that A ≈ B . Then for each store σ and
for x ∈ {ω, τ }
x

x

hF .A, σi 7−→ hF .C , σ ′ i if and only if hF .B , σi 7−→ hF .C , σ ′ i.
Proof
The proof is immediate, by using rule Q9 and by a straightforward inductive argument.
From the above Lemma we derive the following corollary:
Corollary 1
Let F .A and F .B be tsccp-i processes such that A ≈ B . Then for each store σ,
ω
ω
hF .A, σi 7−→ ∗ hSuccess, γi if and only if hF .B , σi 7−→ ∗ hSuccess, γi.

TSCCP: An Interleaved and a Parallel Approach

35

Lemma 2
Let P = F .A be a tsccp-i process. Then for each store σ,
τ

1. hF .A, σi ⇒ hF .B , σ ′ i if and only if σ = σ ′ and
τ

• either hF .A, σi 7−→ hF .C , σi and C ≈ B
τ

• or hF .A, σi 67−→ and B ≈ A.
ω

ω

2. hF .A, σi ⇒ hF .B , σ ′ i if and only if hF .A, σi 7−→ hF .C , σ ′ i and C ≈ B .
Proof
1. The proof is by induction on the complexity of the agent A.
• A is of the form success, tell(c) →a A, tell(c) →φ A, ask(c) →a A,
ask(c) →φ A, Σni=1 Ei , p(x ), askp0 (c)?a A:B and askp0 (c)?φ A:B .
τ

The proof is immediate by observing that by the rules in Figure 11, hA, σi 67−→
τ
and by the rules in Figure 14, hA, σi ⇒ hB , σ ′ i if and only if hA, σi = hB , σ ′ i.
• A is of the form askpt (c)?a A1 :A2 (askpt (c)?φ A1 :A2 ), with t > 0.
The proof is immediate since both the transition systems use the rule Q13
(Q18) of Figure 11.
• If A is of the form A1 k A2 .
In this case, by definition of the transition system T ′ and by using rule Q5
of Figure 11, for each store σ,
τ

hA1 k A2 , σi ⇒ hB1 k B2 , σ ′ i if and only if
τ
τ
hA1 , σi ⇒ hB1 , σ ′ i and hA2 , σi ⇒ hB2 , σi
(the symmetric case is analogous and hence it is omitted).
By inductive hypothesis this holds if and only if σ ′ = σ and for i = 1, 2
τ

— either hAi , σi 7−→ hCi , σi and Ci ≈ Bi
τ

— or hAi , σi 67−→ and Bi ≈ Ai .
τ

If there exists i ∈ [1, 2] such that hAi , σi 7−→ hCi , σi then the thesis follows
by using either rule Q5 or rule Q6.
τ

Otherwise hA1 k A2 , σi 67−→. Then the thesis follows since by the previous
results B1 k B2 ≈ A1 k A2 .
• A is of the form ∃xA1 . By rule Q9 of Figure 11 for each store σ,
τ

τ

h∃xA1 , σi ⇒ hB , σ ′ i if and only if hA1 [x /y], σi ⇒ hB , σ ′ i
By inductive hypothesis this holds if and only if σ ′ = σ
τ

— either hA1 [x /y], σi 7−→ hC , σi and C ≈ B
τ

— or hA1 [x /y], σi 67−→ and B ≈ A1 [x /y].
Therefore, by using rule Q9 of Figure 11 and since ∃xA1 ≈ A1 [x /y], we have
that
τ

— either h∃xA1 , σi 7−→ hC , σi and C ≈ B
τ

— or h∃xA1 , σi 67−→ and B ≈ ∃xA1 and then the thesis.
2. The proof is analogous to the previous one and hence it is omitted.

36

Bistarelli et al.

Lemma 3
i′
i
Let P = F .A be a tsccp-i process. Then Oio
(P ) = Oio
(P )·
Proof
ω
We prove that there exists a computation hA, σi ⇒ ∗ hSuccess, γi if and only if
∗
ω
there exists a computation hA, σi 7−→ hSuccess, γi. Then the thesis follows by
i
i′
definition of Oio (P ) and Oio (P )· The proof is by induction on the length of the
ω
computation hA, σi ⇒ ∗ hSuccess, γi.
n = 1) In this case A = Success and then the thesis.
n > 1) In this case
ω

hA, σi ⇒ ∗ hSuccess, γi
(by definition)
ω
ω
hA, σi ⇒ hA1 , σ1 i and hA1 , σ1 i ⇒ ∗ hSuccess, γi
(by inductive hypothesis)
ω
ω
hA, σi ⇒ hA1 , σ1 i and hA1 , σ1 i 7−→ ∗ hSuccess, γi
(by Point 2 of Lemma 2)
ω
ω
hA, σi 7−→ hA2 , σ1 i, A2 ≈ A1 and hA1 , σ1 i 7−→ ∗ hSuccess, γi
(by Corollary 1)
ω
ω
hA, σi 7−→ hA2 , σ1 i and hA2 , σ1 i 7−→ ∗ hSuccess, γi
(by definition)
ω
hA, σi 7−→ ∗ hSuccess, γi·

iff
iff
iff
iff
iff

We can now easily prove that, given our definition of D, the modified transition
system T ′ agrees with the denotational model.
Theorem 2
For any tsccp-i process P = F .A we have
′

i
Oio
(P ) = {σn ⇓Fv (A) | there exists a connected sequence s ∈ D(P ) such that
s = hσ1 , σ2 , ωihσ2 , σ3 , ωi · · · hσn , σn , ωi}.

Proof
We prove by induction on the complexity of the agent A that
D(P ) = {s |

s = hσ1 , σ1′ , x1 ihσ2 , σ2′ , x2 i · · · hσn , σn , ωi, A1 = A,
x
for i ∈ [1, n − 1], hAi , σi i ⇒i hAi+1 , σi′ i and An = Success}.
′

i
Then the proof follows by definition of Oio
(P ).
When the tsccp-i P is not of the form F .B k C the thesis follows immediately
from the close correspondence between the rules of the transition system and the
definition of the denotational semantics.
Assume now that P is of the form F .B k C . By definition of the denotational

TSCCP: An Interleaved and a Parallel Approach

37

semantics, s ∈ D(P ) if and only if s = hσ1 , σ1′ , x1 ihσ2 , σ2′ , x2 i · · · hσn , σn , ωi and
there exist s ′ ∈ D(F .B ) and s ′′ ∈ D(F .C ),
s ′ = hσ1 , κ′1 , x1′ ihσ2 , κ′2 , x2′ i · · · hσn , σn , ωi
and
′′
′′
′′
′′
′′
s = hσ1 , κ1 , x1 ihσ2 , κ2 , x2 i · · · hσn , σn , ωi,
such that for each i ∈ [1, n − 1],
xi = τ if and only if
xi = ω if and only if

xi′ = xi′′ = τ and in this case σi′ = κ′i = κ′′i = σi ,
either xi′ = ω, xi′′ = τ, κ′i = σi′ and κ′′i = σi
or xi′ = τ, xi′′ = ω, κ′′i = σi′ and κ′i = σi ·

(2)

By inductive hypothesis s ′ ∈ D(F .B ) and s ′′ ∈ D(F .C ) if and only if
x′

hBi , σi i ⇒i hBi+1 , κ′i i for i ∈ [1, n − 1], B1 = B and Bn = Success,
x ′′

i
hCi , σi i ⇒
hCi+1 , κ′′i i for i ∈ [1, n − 1], C1 = C and Cn = Success.

(3)

Therefore, by Rule R8 and by (2), we have that (3) holds if and only if
x

hBi k Ci , σi i ⇒i hBi+1 k Ci+1 , σi+1 i for i ∈ [1, n − 1],
B1 k C1 = B k C and Bn k Cn = Success
and then the thesis.
Thus we obtain the following correctness result whose proof is immediate from
the previous theorems.
Corollary 2 (Correctness of tsccp-i)
For any tsccp-i process P = F .A we have
i
Oio
(P ) = {σn ⇓Fv (A) | there exists a connected sequence s ∈ D(P ) such that
s = hσ1 , σ2 , ωihσ2 , σ3 , ωi · · · hσn , σn , ωi}.
10 Related Work
By comparing this work with other timed languages using crisp constraints (instead
of soft ones as in this paper) as (Saraswat et al. 1996; Saraswat et al. 1994), there
are three main differences we can find out.
First, the computational model of both the languages tcc (Saraswat et al. 1994)
and default tcc (Saraswat et al. 1996) is inspired by that one of synchronous languages: each time interval is identified with the time needed for a ccp process to
terminate a computation. Clearly, in order to ensure that the next time instant is
reached, the (default) ccp program has to be always terminating; thus, it is assumed
that it does not contain recursion. On the other hand, we directly introduce a timed
interpretation of the usual programming constructs of ccp by considering the primitive ccp constructs ask and tell as the elementary actions whose evaluation takes
one time-unit. Therefore, in our model, each time interval is identified with the time
needed for the underlying constraint system to accumulate the tells and to answer
the queries (asks) issued at each computation step by the processes of the system.
For the definition of our tsccp agents we do not need any restriction on recursion to

38

Bistarelli et al.

ensure that the next time instant is reached, since at each moment there are only a
finite number of parallel agents, and the next moment in time occurs as soon as the
underlying constraint system has responded to the initial actions of all the current
agents of the system.
A second difference relies in the transfer of information across time boundaries. In
(Saraswat et al. 1994) and (Saraswat et al. 1996), the programmer has to explicitly
transfer the (positive) information from a time instant to the next one, by using
special primitives that allow one to control the temporal evolution of the system.
In fact, at the end of a time interval all the constraints accumulated and all the
processes suspended are discarded, unless they are arguments to a specific primitive.
On the contrary, no explicit transfer is needed in tsccp, since the computational
model is based on the monotonic evolution of the store which is usual in ccp.
A third relevant difference is in (Saraswat et al. 1994) and (Saraswat et al. 1996)
the authors present deterministic languages while our language allows for nondeterminism. These three differences also hold between (Saraswat et al. 1994) or
(Saraswat et al. 1996), and the original crisp version of the language, i.e., tccp (de Boer et al. 2000).
In (Olarte et al. 2007), the authors generalize the model in (Saraswat et al. 1994)
in order to extend it with temporary parametric ask operations. Intuitively, these
operations behave as persistent parametric asks during a time-interval, but may
disappear afterwards. The presented extension goes in the direction of better modeling mobile systems with the use of private channels between the agents. However,
also the agents in (Olarte et al. 2007) show a deterministic behavior, instead of our
not-deterministic choice.
Other timed extension of concurrent constraint programming have been proposed
in (Nielsen and Valencia 2002; Palamidessi and Valencia 2001), however these languages, differently from tsccp, do not take into account quantitative aspects; therefore, this achievement represents a very important expressivity improvement with
respect to related works. These have been considered by Di Pierro and Wiklicky,
who have extensively studied probabilistic ccp (see for example (Di Pierro and Wiklicky 1998)).
This language provides a construct for probabilistic choice which allows one to express randomness in a program, without assuming any additional structure on the
underlying constraint system. This approach is therefore deeply different from ours.
More recently, stochastic ccp has been introduced in (Bortolussi 2006) to model biological systems. This language is obtained by adding a stochastic duration to the
ask and tell primitives, thus it differs from our solutions.
In literature we can find other proposals that are related to tuple-based kernellanguages instead of a constraint store, as KLAIM (de Nicola et al. 1998) (A Kernel Language for Agents Interaction and Mobility) or SCEL (De Nicola et al. 2011)
(Software Component Ensemble Language) for instance. These languages are designed to study different properties of systems, as mobility and autonomicity of
modeled agents. Their basic specification do not encompass time-based primitives,
while mobility features are not present in any of the constraint-based languages
reported in this section. The purpose of our language is to model systems where a
level of preference and time-sensitive primitives (as a timeout) is required: a good

TSCCP: An Interleaved and a Parallel Approach

39

example is represented by agents participating to an auction, as the example given
in Section 5.1.
In general, since semiring-based soft constraints allow one to express several quantitative features, our proposal provides a framework which can be instantiated to
obtain a variety of specific extensions of ccp.
11 Conclusion and Future Work
We have presented the tsccp and tsccp-i in order to join together the expressive capabilities of soft constraints and timing mechanisms in a new programming framework. The agents modeled with these languages are able to deal with time and
preference-dependent decisions that are often found during complex interactions.
An application scenario can be represented by different entities that need to negotiate generic resources or services, as, for instance, during an auction process.
Mechanisms as timeout and interrupt may model the wait for pending conditions
or the triggering of some new events. All the tsccp and tsccp-i rules have been
formally described by a transition system and, then, also with a denotational characterization of the operational semantics obtained with the use of timed reactive
sequences. The resulting semantics has been proved to be compositional and correct.
About future work, a first improvement of the presented languages can be the
inclusion of a fail agent in the syntax given in Definition 1 and Definition 7, and
a semantics for the transition rules that lead to a failed computation, in case the
guard on the transition rule cannot be enforced due to the preference of the store. In
fact, the transition systems we have defined consider only successful computations.
If this could be a reasonable choice in a don’t know interpretation of the language
it will lead to an insufficient analysis of the behavior in a pessimistic interpretation
of the indeterminism.
At last, we would like to consider other time management strategies (as the
one proposed in (Valencia 2003)), and to study how timing and non-monotonic
constructs (Bistarelli and Santini 2011) can be integrated together.
References
Berry, G. and Gonthier, G. 1992. The ESTEREL synchronous programming language:
design, semantics, implementation. Sci. Comput. Program. 19, 2, 87–152.
Bistarelli, S. 2004. Semirings for Soft Constraint Solving and Programming (LNCS).
Springer Verlag, London, UK.
Bistarelli, S., Gabbrielli, M., Meo, M. C., and Santini, F. 2008. Timed soft concurrent constraint programs. In Coordination Models and Languages, 10th International
Conference, COORDINATION. Lecture Notes in Computer Science, vol. 5052. Springer,
London, UK, 50–66.
Bistarelli, S., Montanari, U., and Rossi, F. 1997. Semiring-based constraint satisfaction and optimization. J. ACM 44, 2, 201–236.
Bistarelli, S., Montanari, U., and Rossi, F. 2006. Soft concurrent constraint programming. ACM Trans. Comput. Logic 7, 3, 563–589.
Bistarelli, S. and Santini, F. 2011. A nonmonotonic soft concurrent constraint language to model the negotiation process. Fundam. Inform. 111, 3, 257–279.

40

Bistarelli et al.

Bortolussi, L. 2006. Stochastic concurrent constraint programming. Electr. Notes Theor.
Comput. Sci. 164, 3, 65–80.
Brookes, S. D. 1993. Full abstraction for a shared variable parallel language. In LICS.
IEEE Computer Society, Los Alamitos, CA, USA, 98–109.
Busi, N., Gorrieri, R., and Zavattaro, G. 2000. Process calculi for coordination: From
Linda to JavaSpaces. In AMAST. Springer-Verlag, London, UK, 198–212.
de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2000. A timed concurrent constraint
language. Inf. Comput. 161, 1, 45–83.
de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2004. A timed Linda language and
its denotational semantics. Fundam. Inf. 63, 4, 309–330.
de Boer, F. S. and Palamidessi, C. 1991. A fully abstract model for concurrent constraint programming. In TAPSOFT ’91: Proceedings of CAAP ’91. Vol. 1. SpringerVerlag New York, Inc., New York, USA, 296–319.
De Nicola, R., Ferrari, G. L., Loreti, M., and Pugliese, R. 2011. A language-based
approach to autonomic computing. In FMCO, B. Beckert, F. Damiani, F. S. de Boer,
and M. M. Bonsangue, Eds. Lecture Notes in Computer Science, vol. 7542. Springer,
25–48.
de Nicola, R., Ferrari, G. L., and Pugliese, R. 1998. KLAIM: A Kernel Language
for Agents Interaction and Mobility. IEEE Transactions on Software Engineering 24, 5,
315–330.
Di Pierro, A. and Wiklicky, H. 1998. Probabilistic concurrent constraint programming:
Towards a fully abstract model. In MFCS ’98: Proceedings of Mathematical Foundations
of Computer Science. Springer-Verlag, London, UK, 446–455.
Gallien, J. and Gupta, S. 2007. Temporary and permanent buyout prices in online
auctions. Management Science 53, 5, 814–833.
Halbwachs, N., Caspi, P., Raymond, P., and Pilaud, D. 1991. The synchronous
data-flow programming language LUSTRE. Proceedings of the IEEE 79, 9, 1305–1320.
Harel, D. 1987. Statecharts: A visual formalism for complex systems. Sci. Comput.
Program. 8, 3, 231–274.
Jonsson, B. 1985. A model and proof system for asynchronous networks. In PODC ’85:
Proceedings ACM symposium on Principles of distributed computing. ACM Press, New
York, USA, 49–58.
le Guernic, P., le Borgne, M., Gautier, T., and le Maire, C. 1991. Programming
real-time applications with signal. Proceedings of the IEEE 79, 9, 1321–1336.
Nielsen, M. and Valencia, F. D. 2002. Temporal concurrent constraint programming:
Applications and behavior. In Formal and Natural Computing - Essays Dedicated to
Grzegorz Rozenberg. Springer-Verlag, London, UK, 298–324.
Olarte, C., Palamidessi, C., and Valencia, F. 2007. Universal timed concurrent
constraint programming. In Logic Programming, 23rd International Conference, ICLP.
LNCS, vol. 4670. Springer, London, UK, 464–465.
Palamidessi, C. and Valencia, F. D. 2001. A temporal concurrent constraint programming calculus. In CP ’01: Proceedings of Principles and Practice of Constraint
Programming. Springer-Verlag, London, UK, 302–316.
Saraswat, V. 1989. Concurrent constraint programming languages. PhD thesis.
Saraswat, V., Jagadeesan, R., and Gupta, V. 1996. Timed default concurrent constraint programming. J. Symb. Comput. 22, 5-6, 475–520.
Saraswat, V. and Rinard, M. 1990. Concurrent constraint programming. In POPL
’90: Proceedings of Principles of programming languages. ACM Press, New York, USA,
232–245.

TSCCP: An Interleaved and a Parallel Approach

41

Saraswat, V. A., Jagadeesan, R., and Gupta, V. 1994. Foundations of timed concurrent constraint programming. In Proceedings, Ninth Annual IEEE Symposium on
Logic in Computer Science, LICS. IEEE Computer Society, Los Alamitos, CA, USA,
71–80.
Valencia, F. D. 2003. Timed concurrent constraint programming: Decidability results
and their application to LTL. In ICLP. LNCS, vol. 2916. Springer, London, UK, 422–
437.

