BRICS Basic Research in Computer Science

B R ICS R S -01-20 P a lamid essi & V alen cia: A T emp o ral C on cu rr en t C on strain t P rogrammin g Calcu lu

BRICS

Basic Research in Computer Science

A Temporal Concurrent Constraint Programming Calculus

Catuscia Palamidessi Frank D. Valencia

BRICS Report Series RS-01-20

ISSN 0909-0878 June 2001

Copyright c 2001, Catuscia Palamidessi & Frank D. Valencia.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications.

Copies may be obtained by contacting:

BRICS

Department of Computer Science University of Aarhus

Ny Munkegade, building 540 DK–8000 Aarhus C

Denmark

Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk ftp://ftp.brics.dk

This document in subdirectory RS/01/20/

Programming Calculus

Catuscia Palamidessi Frank D. Valencia

June 2001

Abstract

Thetccmodelisaformalismforreactiveconcurrentconstraint

programming. Inthis paperwe proposea modeloftemporal con-

currentconstraintprogrammingwhichaddstotccthecapabilityof

modelingasynchronousandnon-deterministictimedbehavior. We

callthistccextensionthentcccalculus. Theexpressivenessofntcc

isillustratedbymodelingcellsand asynchronousboundedbroad-

casting,byspecifyingtemporalrequirementssuchasresponseand

invariance, and by modeling timed systems such as RCX con-

trollers. We present a denotational semantics for modeling the

strongest-postconditionbehaviorof ntcc processes,and,basedon

thissemantics, we develop aproof systemfor proving lineartem-

poralproperties ofthese processes.

1 Introduction

Researchonconcurrent constraintprogramming(ccp) fortimedsystems

has attracted growing interest in the last years. Timed systems often

involvespecicdomains(e.g.,controllers,databases,reservationsystems)

andhavetime-constraintsspecifying theirbehavior (e.g.,the lightsmust

be switched on within the next three seconds). The ccp model enjoys a

dual operationaland declarative logicalview allowing, onthe one hand,

programs to be expressed using a vocabulary and concepts appropriate

tothespecicdomain,andontheotherhand,tobereadandunderstood

as (logical) specications. An obvious benet of this view is to provide

the developer with one domain specic ccp language suitable for both

thespecication andimplementation ofprograms. Indeed,several timed

theprogrammingandspecicationoftimedsystemswiththedeclarative

avor of concurrent constraint programming([31], [30], [8], [12], [13]).

1.1 Concurrent Constraint Programming: the ccp

model

Concurrent constraint programming [32] has emerged as a simple but

powerful paradigm for concurrency tied to logics. Ccp subsumes and

generalizesbothconcurrentlogicprogramming([34])andconstraintlogic

programming([19]). A fundamental issue in ccp is the specication of

concurrent systems by means of constraints. A constraint (e.g.

x + y >

10

^{) represents partial} information about certain variables. During the computation,thecurrent state of thesystem is speciedby aset ofcon-

straints(store). Processessynchronizebyasking andtelling information.

Whenever a process asks some information not yet entailed by the cur-

rent store, it blocks, and remainsblocked until some other process adds

(tells)the requested informationto the store.

In the ccp model processes are built by using the basic actions ask

andtell,andthe operatorsofparallelcomposition,hiding,recursion and

guarded-choice. Unlike other models of concurrency, without guarded-

choice the modelisdeterministic,namely the result of anite computa-

tionisalwaysthesame,independentlyfromtheexecutionorder(schedul-

ing) of the parallelcomponents ([33]).

1.2 Reactive Concurrent Constraint Programming:

the tcc model

The tcc model([31]) is a formalismfor reactive ccp which combines de-

terministic ccp with ideas from the Synchronous Languages ([4], [15]).

Whenever a tcc process receives a stimulus (partial information)

c

^from

theenvironment,itexecutes adeterministic ccp process

P

^with

c

^asini-

tialstore. In a bounded period of time,

P

^{reaches a resting point, and}

returnsthe informationcontainedin the nal store asa response to the

environment. The residual ccp process at the resting point,

P ⁰

^{, deter-}

minesthe ccp process

P ⁰⁰

^{tobe executed inthe next timeinterval. Each}

stimulus-response interaction between a process and itsenvironmentde-

nes atime unit (or timeinterval). Since the computationin eachtime

intervalis deterministic,tcc is deterministic.

particular, the

do P watching c

^{construct of ESTEREL [4], which exe-}

cutes

P

continuously until the signal

c

^{is present. In general,tcc allows}

processes to be clocked by other processes, thus allowing meaningful

pre-emptionconstructs.

1.3 A ModelofTemporalConcurrent Constraint Pro-

gramming

Beingamodelof reactiveccp based onthe Synchronous Languages ([4],

[15]) (i.e. programs must be determinate and respond immediately to

input signals), the tcc model is not meant for the specication of non-

deterministic or asynchronous temporal behavior. Indeed, patterns of

temporal behavior such as the system must output

c

^{within the next}

t

time units or the message must be delivered but there is no bound in

thedeliverytime cannotbeexpressedwithinthemodel. Italsorulesout

the possibility of choosing one among several alternatives as an output

to the environment. The task of zigzagging (see Section 5), in which

a robot can unpredictably choose its next move, is an example where

non-determinismis useful.

Ingeneral,abenetofallowingthe specicationof non-deterministic

behavioris tofreeprogrammers fromthe necessity of copingwith issues

that are irrelevant to the problem specication. Dijkstra's language of

guarded commands, for example, uses a nondeterministic construction

to help free the programmer from over-specifying a method of solution.

As pointed out in [38], a disciplined use of nondeterminism can lead to

amore straightforward presentation of programs.

This view is consistent with the declarative avor of ccp: The pro-

grammer species by means of constraints the possible values that the

programvariablescan take, withoutbeing required toprovidea compu-

tationalproceduretoenforcethecorrespondingassignments. Constraints

statewhat istobesatisedbutnothow. Followingthislineofreasoning,

weargueforaformalismfortemporalprogrammingwhereprogramsand

specications can be given in the same language. For example, we may

think of the ccp program

tell ( x > 5)

^{as a} specication satised by the ccp programs (or renements)

tell ( x = 7)

^and

tell ( x > 11)

^.

Moreover, a very important benet of allowing the specication of

non-deterministic(andasynchronous) behaviorariseswhenmodelingthe

interaction among several components running in parallel,in which one

neednon-determinism to bemodeledfaithfully.

In this paper we propose an extension of tcc, which we call the

ntcc calculus, for temporal concurrent constraint programming. The

ntcc calculus is obtained by adding guarded-choice for modeling non-

deterministicbehavior and an unbounded nite-delay operator for asyn-

chronous behavior. Computationin ntcc progresses asin tcc, except for

thenon-determinisminduced bythe newconstructs. Thecalculusallows

for the specication of temporal properties, and for modeling (and ex-

pressingconstraints upon) the environment, both of which are useful in

proving propertiesof timed systems.

We willillustratethe expressiveness of ntcc bymodelingseveral con-

structs such ascells, asynchronous bounded broadcasting, response and

invariance,that inturn are useful for specifyingtimed systems. Wealso

illustratesome applicationsinvolvingRCX TM

controllers.

Thedeclarativenatureofntcccomestothesurface whenweconsider

the denotational characterization of the strongest postcondition observ-

ables, as dened in [7] for ccp, and extended to a timed setting. We

show that the elegant model based on closure operators, developed in

[33] for deterministic ccp, can be extended to a sound model for ntcc

without losing its essential simplicity. Under certain conditions on the

kindofguarded-choiceallowed withinthe scopeof localvariables,which

weshall calllocal-independentchoice(i.e, either guardswithoutfreeoc-

currences of local variables, internal or mutually exclusive choice), we

alsoobtaincompleteness.

The logical nature of ntcc comes to the surface when we consider its

relation with linear temporal logic: We show that all the operators of

ntcc correspond to temporal logic constructs like the operators of ccp

correspond to(classical)logicconstructs ([7]). Followingthe lines of the

proofsystemproposedin[7]forccp,wedevelopasoundsystemforprov-

ing linear temporal properties of ntcc, and we show that the system is

also (relatively) complete wrt local-independent choice processes. Our

system is then complete fortcc aswell, since every tcc process fallsinto

the category of local-independent choice ntcc processes. The proof sys-

tem for tcc in [31], whose underlying logic is intuitionistic rather than

classical,is complete for hiding(and recursion) free tcc processes only.

We alsoreport oncurrentresearch onournotion ofequalityfor ntcc:

two processes are equivalent i no context can distinguish them wrt to

the input-output behavior. We show the existence of an universal (dis-

and bounded non-deterministic processes.

The main contributions of this paper can be summarized as follows:

(1)amodeloftemporalconcurrentconstraintprogrammingthatextends

the specication power of the tcc model, (2) a denotational semantics

capturing the strongest postcondition behavior of a ntcc process, (3) a

proofsystemforprovingwhetheragivenntcc process satisesaproperty

speciedinlineartemporallogic,and(4)anstudyofanaturalbehavioral

equivalencefor our calculus.

2 The Calculus

Inthissectionwepresentthesyntaxandanoperationalsemantics ofthe

ntcc calculus. First we recall the notion of constraint system.

2.1 Constraint Systems

Concurrent constraint languages are parametrized by a constraint sys-

tem. Basically, a constraint system denes the underlying universe of

theparticularlanguage. Itprovidesasignature fromwhichsyntactically

denotableobjects inlanguagecalledconstraints can beconstructed, and

an entailment relation specifying interdependencies between such con-

straints. For our purposes it will suce to consider the notion of con-

straint system based on First-Order Predicate Logic, as it was done in

[35]

1

.

Denition 2.1 A constraint system is a pair

(Σ , ∆)

^where

Σ

^{is a sig-}

nature specifying functions and predicate symbols, and

∆

^{is a consistent}

rst order theory.

Given aconstraint system

(Σ , ∆)

^,let

L

^{be the underlyingrst-order}

language

(Σ , V , S)

^{, where}

V = { x, y, z, . . . }

^{is the set of variables and}

S

isthesetcontainingthe symbols

¬ ˙ , ∧ ˙ , ⇒ ˙ , ∃ ˙ , true, ˙

^and

false ˙

^whichdenote

logicalnegation,conjunction, implication,existentialquantication, and

the always true and always false predicates, respectively. Constraints,

denotedby

c, d, . . .

^{are rst-orderformulaeover}

L

^{. Wesay that}

c

^entails

d

ⁱⁿ

∆

^{, written}

c ` _∆ d

^{(or just}

c ` d

^{whenno confusionarises), if}

c ⇒ ˙ d

1

See [33] for a more general notion of constraints based on Scott's information

systems.

is true in all models of

∆

^{. We write}

c ≈ d

ⁱ

c ` d

^and

d ` c

^{. We will}

consider constraints modulo

≈

^{and use}

C

^{for the set of} representants of equivalence classes of constraints. For operational reasons we shall

require

`

^{to be decidable.}

2.2 Syntax

Processes

P

^,

Q

^{, ...}

∈ Proc

^{are builtfrom}constraints

c ∈ C

^andvariables

x ∈ V

^{inthe underlying constraintsystem by the followingsyntax.}

P, Q, . . .

^::=

tell ( c ) | P

i ∈ I

when c _i do P _i | P k Q | local x in P

| next P | unless c next P | ! P | ? P

Informally,theintendedbehavioristhefollowing: Theprocess

tell ( c )

addstheconstraint

c

^{tothecurrentstore,thusmaking}

c

^{availabletoother}

processes in the current time interval. The guarded choice

P

i ∈ I when c _i do P _i

^{, where}

I

^{is aniteset ofindexes, representsapro-}

cess that, in the current time interval, must select non-deterministically

one of the

P _j

⁽

j ∈ I

^{) whose} corresponding constraint

c _j

^{is entailed by}

the store. Once an alternative is selected the others are precluded, and

if none of them can be selected then all of them will be precluded in

the next time interval. We omit

∈ I

^{, if}

I

^is unimportant or obvious and we omit

P

i ∈ I

^when

I

^{is a singleton set. In case}

I = ∅

^{, we write}

skip

^{. Weusethe symbol}

+

^{toindicatebinary}summations. Finally,we use

P

i ∈ I P _i

^{as an}abbreviation for

P

i ∈ I when ( ˙ true ) do P _i

^{(i.e., blind}

choice).

Theprocess

P k Q

^{representsthe parallelactivationof}

P

^and

Q

^{. We}

use

Q

i ∈ I P _i

^{, where}

I

^{is nite, to denote the parallel} composition of all

P _j

^{, for}

j ∈ I

^.

Theprocess

local x in P

^behaveslike

P

^{,exceptthatalltheinforma-}

tionon

x

^producedby

P

^{can onlybe seen by}

P

^{,and the} informationon

x

^{producedbyotherprocessescannotbeseenby}

P

^{. Weuse}

local x ¯ in P

as a shorthand for

local x ₁ in ( local x ₂ in ( . . . ( local x n in P ) . . . ))

^,

where

x ¯

^{represents the sequence}

x ₁ x ₂ . . . x _n

^.

The process

next P

^{represents the activation of}

P

^{in the next time}

interval. The process

unless c next P

^{is similar, but}

P

^{will be acti-}

vated only if

c

^{cannot be inferred from the current store. The unless}

processes add (weak) time-outsto the calculus, i.e., they wait one time

unitforapieceofinformation

c

^{tobepresentand ifitisnot,they trigger}

activity in the next time interval. We use

next ⁿ ( P )

^{as an} abbreviation for

next ( next ( . . . ( next P ) . . . ))

^{, where}

next

^isrepeated

n

^times.

The operator

!

^{is a delayed version of the} replication operator for the

π −

^{calculus ([26]):}

! P

^represents

P k next P k next ² P k . . .

^{, i.e.}

unboundely many copies of

P

^{but one at a time, so there is no risk of}

innite activity within a time interval. The replication operator is the

only way of dening innite behavior through the time intervals. The

operator

?

^is reminiscent of the nite delay operator for synchronous CCS ([25]) and it allows us to express asynchronous behavior through

the time intervals. The process

? P

^{represents a nite but unbounded}

delay for the activation of

P

^{. For example,}

? tell ( c )

^{can be viewed as a}

message

c

^{that is eventually delivered but there is no upper bound on}

the delivery time.

Note that the bounded versions of

! P

^and

? P

^{can be derived from}

thepreviousconstructs. Weuse

! I P

^and

? _I P

^{, where}

I

^{isnite,asanab-}

breviationfor

Q

i ∈ I next ⁱ P

^and

P

i ∈ I next ⁱ P

^,respectively. Forinstance,

? _[ m,n ] P

^meansthat

P

^{iseventuallyactivebetween thenext}

m

^and

m + n

timeunits, while

! [ m,n ] P

^meansthat

P

^{isalways activebetween the next}

m

^and

m + n

^{time units.}

2.3 Some examples

Wenowshowsomeexamplesillustratingspecicationoftemporalbehav-

ior in ntcc such as response requirements. Assume that the underlying

constraint system includes the predicate symbols in

{O,TurnOn,OutofOrder,OverHeated}. Considerthepowersavingpro-

cess

! ( unless ( Off ( lights )) next ? tell ( Off ( lights ))) .

Call it

! P

^{. This process triggers a copy of}

P

^{each time unit. Thus,}

the lights are eventually turned o, unless the environment (or another

process)tells

P

^{thatthelightsarealreadyturnedo. Process}

P

^isalways

active. Wemay want,however, tospecify that the lightmust be turned

o not only eventually but within the next

60

^{time units. A process}

specifyingthis and thus rening the previous one would be

! ( unless ( Off ( lights )) next ? _{[0 , 60]} tell ( Off ( lights ))) .

Finally,we may alsowant towrite an implementation of these speci-

cations. Forinstance, the process

! ( unless ( Off ( lights )) next tell ( Off ( lights )))

two.

Anotherexampleisthespecicationof (bounded)invariancerequire-

ments. Consider the followingtwoprocesses:

! ( when OutofOrder ( M ) do ! tell ( ˙ ¬ T urnOn ( M )))

! ( when OverHeated ( M ) do ! [0 ,t ] tell ( ˙ ¬ T urnOn ( M )))

The rst process repeatedly checks the state of a machine

M

^and,

whenever it detects that

M

^{is out of order, it tells the other processes}

that

M

^{should not be used anymore. The second process, whenever it}

detectsthat

M

^isoverheated, tellsother processesthat

M

^shouldnotbe

turnedonduring the next

t

^{time units.}

2.4 An operational semantics for ntcc

We dene now an operational semantics for ntcc which formalizes the

intended meaningexplained above.

2.4.1 The store and the congurations

Operationally,the current informationis represented asaconstraint

c ∈ C

^{, so-called store. Our} operational semantics is given by considering transitions between congurations

γ

^{of the form}

h P, c i

^{. We dene}

Γ

^as

the set of all congurations. Following standard lines, we extend the

syntax with aconstruct

local ( x, d ) in P

^{, which represents the evolution}

of a process of the form

local x in Q

^{, where}

d

^{is the local} information (or store) produced during this evolution. Initially

d

^{is empty, so we}

regard

local x in P

^as

local ( x, true ˙ ) in P

^.

2.4.2 A structural congruence

We need to introduce a notion of free variables that is invariant wrt

the equivalence on constraints. We can do so by dening the relevant

free variables of

c

^as

fv ( c ) = { x ∈ V | ∃ x c 6≈ c }

^{. For instance, we have}

f v ( x = x ∧ ˙ y > 1) = { y }

^{. For the bound variables, dene}

bv ( c ) = { x ∈ V | x

^{occurs in}

c } − fv ( c )

^{. Regardingprocesses, dene}

fv ( tell ( c )) = fv ( c )

^,

fv ( P

i when c _i do P _i ) = S

i fv ( c _i ) ∪ fv ( P _i )

^{, and similarly for the}

bound variables. Further, dene

fv ( local x in P ) = fv ( P ) − { x }

^and

bv ( local x in P ) = bv ( P ) ∪ { x }

^{. The other cases are dened} inductively inthe obvious way.

Denition 2.2 (Structural congruence) Let

≡

^{be the smallest con-}

gruence relation over processes satisfying the following laws:

1.

(

^Proc

/ _≡ , k , skip )

^{is a symmetric monoid.}

2.

P ≡ Q

^{if they only dier by a renaming of bound variables.}

3.

next skip ≡ skip next ( P k Q ) ≡ next P k next Q

4.

local x in skip ≡ skip local x y in P ≡ local y x in P

5.

local x in next P ≡ next ( local x in P )

6.

local x in ( P k Q ) ≡ P k local x in Q

^if

x 6∈ fv ( P )

We extend

≡

^tocongurations by dening

h P, c i ≡ h Q, c i

^if

P ≡ Q

^.

One interesting property of our calculusis that itadmits a notionof

standard form:

Denition 2.3 A process

P

^{of the form}

local x ¯ in Y

i ∈[0 ,n ]

next ⁱ



 Y

j _i

P j _i k Y

k _i

unless c k _i next Q k _i k Y

l _i

! Q l _i k Y

m _i

? Q m _i





is said to be in standard form if each

P _{j i}

^{is a non-empty summation or}

a tell process, and each

Q _{k i} , Q _{l i}

^and

Q _{m i}

^{isitself a standard form.}

Proposition2.4 Every process

P

^{in the original syntax (i.e. with no}

occurrencesofconstructsoftheform

local ( x, c ) in P

^)isstructurallycon- gruent to a process

Q

^{in standard form, and such}

Q

^{is unique modulo}

congruence.

2.4.3 Reduction Relations

The reduction relations

−→ ⊆ Γ × Γ

^and

= ⇒ ⊆ Proc × C × C × Proc

are the least relations satisfying the rules appearing in Table 1. The

internal transition

h P, c i −→ h Q, d i

^{should be read as}

P

^{with store}

c

reduces,inoneinternalstep,to

Q

^withstore

d

^{. Theobservabletransition}

P ==== ^{( c,d )} ⇒ Q

^{shouldbe read as}

P

^{on input}

c

^{reduces, inone time unit,}

to

Q

^{with store}

d

^{. As in tcc, the store does not transfer} automatically fromone interval toanother.

CHOICE, and PAR are standard. The intuition behind LOC is the

following: From the internal point of view of

P

^{, the global informa-}

tion about the variable

x

^{cannot be observed. Thus, in order to reduce}

h local ( x, c ) in P, d i

^{, we should rst hide the} informationabout

x

^that

d

^{may have. We do this by} existentially quantifying

x

ⁱⁿ

d

^{. From the}

external point of view, the internal information produced in

c ⁰

^about

x

cannot be observed, thus we quantify

x

ⁱⁿ

c ⁰

^{in the global store. Addi-}

tionally,

c ⁰

^{becomes the new private store of the process for its future}

evolutions.

Rule UNLESSsays thatif

c

^{isentailedbythe current store,then the}

executionofthe process

P

^{(inthe next time interval)isprecluded. Rule}

REPL species that the process

! P

^{produces a copy}

P

^{at the current}

time unit, and then persists in the next time unit. Since this is the

onlyway ofspecifyinginnitebehavior,itfollows thatthere canbe only

nitely many internal transitions in one time unit. STAR says that

? P

triggers

P

^{in some time interval(eitherin the current one orin afuture}

one). Rule STRUCT simply says that structurally congruent processes

have the same reductions.

Rule OBSsays thatanobservable transitionfrom

P

^labeledby

( c, d )

is obtained by performing a nite sequence of internal transitions from

h P, c i

^to

h Q, d i

^{, for some}

Q

^{. The process to be executed in the next}

time interval,

F ( Q )

^{(future of}

Q

^{), is obtained by removing from}

Q

what was meant to be executed only in the current time interval and

anylocalinformationwhichhasbeenstoredin

Q

^{,andbyunfolding the}

sub-terms within

next R

expressions. More precisely:

Denition 2.5

F : P roc → P roc

^{is dened as follows:}

F ( P ) =

 

 

 



Q

^if

P = next Q

^or

P = unless c next Q F ( P ₁ ) k F ( P ₂ )

^if

P = P ₁ k P ₂

local x in F ( Q )

^if

P = local ( x, c ) in Q

skip

^otherwise

Note that both

F (! P )

^and

F ( ? P )

^{are dened to be}

skip

^because

neither

! P

^nor

? P

^{occursat the top levelin anal} conguration.

We conclude this section illustrating how processes evolve through

the time intervals. An (innite)sequence of observable transitions

P ₁ ^{( c 1 ,c}

0 1 )

==== ⇒ P ₂ ^{( c 2 ,c}

0 2 )

==== ⇒ P ₃ ^{( c 3 ,c}

0 3 )

==== ⇒ . . .

P ₁

^{and an} environment. At the time unit

i

^{, the} environment provides a

stimulus

c _i

^{andthe system}

P _i

^produces

c ⁰ _i

^{asresponse. If}

α = c ₁ .c ₂ .c ₃ . . . .

and

α ⁰ = c ⁰ ₁ .c ⁰ ₂ .c ⁰ ₃ . . .

^{, we represent the above}interaction by the notation

P ₁ ==== ^{( α,α 0 )} ⇒ ^∞

A run can alternativelybe interpreted asan interaction among the par-

allelcomponentsinthe initialsystem(eachcomponentbeingpartof the

environment of the others): if

α = ˙ true. true. ˙ true . . . ˙

^{, i.e., the input se-}

quenceis empty, then

α ⁰

^{can beregarded as atimed} observation of such aninteraction.

3 Strongest postconditions: denotation and

logic for ntcc

Inthis section weintroduce anotion ofobservablessuitable toberepre-

sented logically,and we investigateits denotationalcounterpart.

In the following we use

α, α ⁰

^{to represent elements of}

C ^∞

^and

β

^to

represent an element of

C ^∗

^{. Given}

c ∈ C

^,

c.α

^{represents the concate-}

nation of

c

^and

α

^{. F}urthermore,

β.α

^{represents the} concatenation of

β

and

α

^{. We use}

∃ ˙ x α

^{to represent the sequence obtained by applying}

∃ ˙ x

toeachconstraint in

α

^{. Notation}

α ( i )

^{denotes the}

i

^{-thelement in}

α

^.

Denition 3.1 (Observables) 1. Theinput-output(orstimulus-response)

relation of a process

P

^{is dened as}

io ( P ) = {( α, α ⁰ ) | P ==== ^{( α,α 0 )} ⇒ ^∞ }

2. Thequiescent sequences of a process

P

^{are dened as}

sp ( P ) = { α | P ==== ^{( α,α )} ⇒ ^∞ }

Following[7]weshallreferto

sp ( P )

^{asthestrongest} postconditionof

P

^(wrt

C ^∞

^{)as it satisesthe following:}

Proposition3.2

α ∈ sp ( P )

^{i there exists}

α ⁰

^{such that}

P ==== ^{( α 0 ,α )} ⇒ ^∞

^.

We give now adenotational characterization of the strongest postcondi-

tion observables of ntcc, followingideas developed in [7]and [31] for the

ccp and tcc case, respectively. The presence of non-determinism, how-

ever, presents a technical problem todeal with: The observables for the

hidingoperatorcannot bespeciedcompositionally(see [7]). Therefore,

we will have to identify a practical fragment for which the semantics is

complete wrt our observables.

The denotational semantics is dened as a function

[[·]]

^{which as-}

sociates to each process a set of innite constraint sequences, namely

[[·]] : Proc → P( C ^∞ )

^{. The denition of this functionis given inTable 2.}

Intuitively,

[[ P ]]

^{is meant tocapture the quiescent sequences of apro-}

cess

P

^{. For instance, the sequences to which}

tell ( c )

^{cannot add infor-}

mation are those whose rst element is stronger than

c

^{(D1). Process}

next P

^{has not inuence in the rst element of a sequence, thus}

d.α

^is

quiescent for it if

α

^{is quiescent for}

P

^{(D5). A sequence is quiescent for}

! P

^{if every sux of it is quiescent for}

P

^{(D7). A sequence is quiescent}

for

? P

^{if there is a sux of it which isquiescent for}

P

^{(D8). The other}

rules can be explainedanalogously.

Remark 3.3 The

!

^{and the}

?

^{operators are dual. In fact,we could have}

dened

[[! P ]] = ν _X ([[ P ]] ∩ { d.α | d ∈ C , α ∈ X }) [[ ? P ]] = µ _X ([[ P ]] ∪ { d.α | d ∈ C , α ∈ X })

where

ν

^and

µ

^represent respectively the greatest and the least x-point operators in the completelattice

(P ( C ^∞ ) , ⊆)

^.

Next theoremstates the relationbetween thedenotationalsemantics

of antcc process and itsstrongest postconditions.

Theorem 3.4 (Soundness) For every ntcc process

P

^,

sp ( P ) ⊆ [[ P ]] .

For the reasons mentioned at the beginning of this section, the con-

verse of this theorem does not hold in general. As in ccp, in ntcc the

converse holds for restricted choice processes, namely those ntcc pro-

cessesinwhich,for everyconstruct ofthe form

P

i ∈ I when c _i do P _i

^,the

c _i

^{'s are pairwise either mutually exclusive or} equivalent. Formally, this means that for all

i, j ∈ I

^{, if there exists}

d 6= false ˙

^{such that}

d ` c _i

and

d ` c _j

^{, then}

c _i = c _j

^. Blind-choice processes are a typical case of

impliesstructuralconuence in the sense of [10], namely the outcome of

a process does not depend upon the scheduling strategy on its parallel

components.

Nevertheless, forntccwecanshowthattheconverseholdsforalarger

set of processes which we calllocal-independent choice processes. These

areprocessesinwhich,foreveryconstruct

P

i ∈ I when c _i do P _i

^occurring

within a process

local x in Q,

^{either (a)}

x 6∈ S

i ∈ I fv ( c _i )

^{, or (b) the}

c _i

^'s

are pairwisemutuallyexclusive orequivalent. This fragment ispractical

sinceeveryrestricted-choiceprocess isalsolocal-independentchoiceand,

unlikethe restricted-choicefragment,itscondition doesnotimplystruc-

tural congruence. In fact, all the process examples in this paper belong

to the local-independent choice fragment but not all of them belong to

the restricted choice one (Zigzagging inSection 5).

Theorem 3.5 (Completeness) If

P

^isa local-independentchoicentcc process, then

sp ( P ) = [[ P ]] .

Fordeterministicprocessessuchastcc processes,namelythosewhich

contain neither the choice (except when the index set is a singleton)

nor the

?

^{operator, we have an even stronger result: the semantics al-}

lows to retrieve the input-output relation (which for deterministic pro-

cesses isa function). Letus use

≤

^{to denotethe (partial)order relation}

{( α, α ⁰ ) | ∀ i ≥ 1 α ⁰ ( i ) ` α ( i )}

^and

min ( S )

^{todenotetheminimalelement}

of

S ⊆ C ^∞

^{inthe complete lattice}

( C ^∞ , ≤) .

Theorem 3.6 If

P

^{is a} deterministic process, then

( α, α ⁰ ) ∈ io ( P )

ⁱ

α ⁰ = min ([[ P ]]∩ ↑ α )

^{, where}

↑ α = { α ⁰⁰ | α ≤ α ⁰⁰ }

^.

4 A logic for ntcc

Inthis sectionwedenealinear temporallogicfor expressing properties

of ntcc processes.

4.1 Syntax

The temporal logic formulae

A, B, ... ∈ A

^{are dened by the following}

grammar.

A

^::=

c | A ∨ A | A ∧ A | A ⇒ A | ¬ A | ∃ x A | ◦ ^{A | A | ♦ A}

In the above grammar,

c

^{denotes an arbitrary} constraint. The in- tendedmeaningoftheothersymbolsisthe following:

∨

^,

∧

^,

⇒

^,

¬

^and

∃ x

represent temporallogic disjunction, conjunction, implication, negation

andexistentialquantication. Thesesymbolsarenottobeconfusedwith

thelogicsymbols

∧ ˙

^,

⇒ ˙

^,

¬ ˙

^and

∃ ˙ x

^{ofthe constraintsystem. Thesymbols}

◦

^,

^{, and}

^♦

^{denotethe temporaloperators next,always and sometime.}

4.2 Semantics

The standard interpretation structures of linear temporallogic are in-

nite sequences of states [23]. In the case of ntcc, it is natural to replace

states by constraints, and consider therefore as interpretations the ele-

ments of

C ^∞

^{. Wesay that}

α ∈ C ^∞

^{is amodel of}

A

^{, notation}

α | = A

^{, if}

h α, 1i | = A

^{, where:}

h α, i i | = c

ⁱ

α ( i ) ` c h α, i i | = ¬ A

ⁱ

h α, i i 6| = A

h α, i i | = A ₁ ∨ A ₂

ⁱ

h α, i i | = A ₁

^or

h α, i i | = A ₂ h α, i i | = A ₁ ∧ A ₂

ⁱ

h α, i i | = A ₁

^and

h α, i i | = A ₂ h α, i i | = A ₁ ⇒ A ₂

ⁱ

h α, i i | = A ₁

^implies

h α, i i | = A ₂ h α, i i | = ◦ ^A

ⁱ

^{h α, i + 1i | = A}

h α, i i | = A

^{i for all}

j ≥ i h α, j i | = A

h α, i i | = ♦ A

^{i there exists}

j ≥ i

^s.t.

h α, j i | = A

h α, i i | = ∃ x A

^{i there exists}

α ⁰ ∈ C ^∞

^s.t.

∃ ˙ x α = ∃ ˙ x α ⁰

^and

h α ⁰ , i i | = A.

We dene

[[ A ]]

^{tobethe collectionof allmodels of}

A

^{. Formally:}

[[ A ]] = { α | α | = A }

4.3 Proving properties of ntcc processes

Weare interested inassertionsof theform

P ` A

^{,whoseintuitivemean-}

ing is that the strongest postcondition of

P

^{satises the property ex-}

pressed by

A

^.

An inference system for such assertions is presented in Table 3. We

willsay that

P ` A

^{holds if the assertion}

P ` A

^{has a proof in this}

system.

The following theorem states the soundness and the relative com-

pleteness of the proof system.

Theorem 4.1 For every ntcc process

P

^{and every formula}

A

^,

P ` A

holdsi

[[ P ]] ⊆ [[ A ]]

^holds.

because of the side condition in Rule P9 (consequence rule): the proof

system iscomplete modulo the capability of provingthe formulae of the

form

A ⇒ B

^{whichwe need touse ina proof. Proving}

A ⇒ B

^isknown

to be decidable for the quantier-free fragment of linear time temporal

formulae([23])as wellasforsomeother interesting rst-orderfragments

(see [17]).

FromTheorems 4.1, 3.4and 3.5 weimmediatelyderivethe following:

Corollary 4.2 1. For every ntcc process

P

^{and every formula}

A

^{, if}

P ` A

^holdsthen

sp ( P ) ⊆ [[ A ]]

^holds.

2. Foreverylocal-independentchoicentccprocess

P

^{andeveryformula}

A

^,

P ` A

^{holds i}

sp ( P ) ⊆ [[ A ]]

^holds.

We shall see that the kind of recursion considered in [31] can be

encoded in ntcc. Hence, tcc processes can be considered as a particular

case of local-independent choice ntcc processes, and therefore the proof

system iscomplete fortcc.

The following notion will be useful in the Section 5, for discussing

properties of our examples.

Denition 4.3 A formula

A

^{isthe strongest temporalformula derivable}

for

P

^if

P ` A

^{and for all}

A ⁰

^{such that}

P ` A ⁰

^{, we have}

A ⇒ A ⁰

^.

Note that the strongest temporal formula of a process

P

^{is unique}

modulo logical equivalence. We give now a constructive denition of

such formula.

Denition 4.4 The function

stf : Proc → A

^{is dened as follows:}

stf ( tell ( c )) = c stf ( P

i∈I when ( c _i ) do P _i ) = W

i ∈ I c _i ∧ stf ( P _i )

∨ V

i ∈ I ¬ c _i stf ( P k Q ) = stf ( P ) ∧ stf ( Q )

stf ( local x P ) = ∃ x stf ( P ) stf ( next P ) = ◦ ^{stf ( P )}

stf ( unless c next P ) = c ∨ ◦ ^{stf ( P )}

stf (! P ) = stf ( P )

stf ( ? P ) = ♦ stf ( P )

We can easily prove that

[[ stf ( P )]] = [[ P ]]

^{and that}

P ` stf ( P )

^{. From}

thesewe have:

Proposition4.5 For every process

P

^,

stf ( P )

^{is the strongest temporal}

formula derivable for

P

^.

Notethattoprovethat

P ` A

^{issucienttoprovethat}

stf ( P ) ⇒ A

^.

However, toprovesuchimplicationmaynotbealwaysfeasibleorpossible.

Theproof system providesthe additionalexibility ofproving

P ` A

^by

using the consequence rule (P9) on subprocesses of

P

^{and on formulae}

dierent from

A

^.

5 Applications

In this sectionwe illustrate somentcc examples. We rst need todene

anunderlyingconstraint system.

Denition 5.1 Let max be a positive integer number. Dene

FD [ max ]

as the constraint system whose signature

Σ

^{includes symbols in}

{0 , succ, + , × , =}

^{andtherst-order theory}

∆

^{isthesetofsentencesvalid}

in arithmetic modulo max.

Theintendedmeaningof

FD [ max ]

^{isthenaturalnumbers}interpreted asinarithmeticmodulo

max

^. Henceforth,weassumethat the signature isextended with two new unary predicate symbols calland change. We

will designate Dom as the set

{0 , 1 , ...., max − 1}

^{and use}

v

^and

w

^to

rangeover itselements.

5.1 Recursion

Often it is convenient to specify behavior by using recursive denitions.

In our language we do not have them, but we can show that we can

encode a (restricted) form of recursion. Namely, we consider recursive

denitions of the form

q ( x )

^def

= P _q ,

^where

q

^{is the process name and}

P _q

containsatmostoneoccurrenceof

q

^{whichmustbewithinthescopeof a}

next

^{andout of the scopeof any}

!

^{. Thereason forsuch a}restriction isthatwe wanttokeep bounded the response timeof thesystem: we do

not want

P _q

^{to make innitely or unboundely many recursive calls of}

q

withinthe same time interval.

We alsowant toconsider the call-by-value. This maylookunnatural

since in constraint programming the natural parameter passing mecha-

nism is through logical variables, like in logic programming. Indeed,

variable. However, for the kind of applications we have in mind (some

of which are illustrated in the rest of this section), call-by-value is the

mechanism we need. Note also that we mean call-by-value in the sense

of value persisting through the time intervals, and this would not be

possible to achieve directly with the call-by-logical-variable, because

the values of variablesare notmaintained fromone intervalto the next.

More precisely: The intended behavior of a call

q ( t )

^{, where}

t

^{is a term}

xedtoavalue

v

^(i.e.

t = v

^{inthecurrentstore),isthatof}

P _q [ v/x ]

^,where

[ v/x ]

^{isthe operationof}(syntactical)replacementofeveryoccurrenceof

x

^by

v

^.

We now showhow to encode such a kind of recursion by using repli-

cation. Given

q ( x )

^def

= P _q

^{, we willuse}

q, qarg

^{todenote anytwovariables}

not in

f v ( P _q )

^{. Let}

p x := t q

^{be dened as the process}

P

v when t = v do ! tell ( x = v )

^{, i.e., the persistent assignment of}

t

^{'s xed value to}

x.

Then the ntcc process corresponding to denition of

q ( x )

^{, denoted as}

p q ( x )

^def

= P _q q

^{, is :}

! ( when call ( q ) do local x in (p x := qarg q k p P _q q)) ,

where

p P _q q

^{denotes the process that results from replacing in}

P _q

^each

q ( t )

^with

tell ( call ( q )) k tell ( qarg = t )

^{(thus telling that there is a call}

of

q

^{with argument}

t

^). Intuitively, whenever the process

q

^{iscalled with}

argument

qarg

^{, the local}

x

^{isassigned the argument'svalue so itcan be}

used by

q

^{'s body}

p P _q q

^.

We then consider the calls

q ( t )

^{in other processes. Each such a call}

isreplaced by

local q qarg in (p q ( x )

^def

= P _q q k tell ( call ( q )) k tell ( qarg = t ))

^{, which we shall denote by}

p q ( t )q

^{. The local} declarations are needed toavoidinterference with other recursive calls.

The above encoding generalizes easily to stratied recursion and to

the case of arbitrary number of parameters including the parameterless

recursion of tcc considered in [31]. We now show some temporal prop-

erties satised by the encoding. Next theorem describes the strongest

temporalformulae satised by

p q ( t )q .

Proposition5.2 Given

p q ( x )

^def

= P q q

^{, let}

B

^{the strongest temporal for-}

mula derivable for

p P _q q

^{. Then the temporal formula}

∃ q,qarg ( call ( q )∧ qarg = t ∧( call ( q ) ⇒ ∃ x ( B ∧ ^

w

( qarg = w ⇒ x = w )))

isthe strongest temporal formula derivable for

p q ( t )q

terms of lineartemporallogic. It givesus a proof principlefor recursive

denitions,i.e., in orderto prove that

p q ( t )q ` A

^{itis sucient toprove}

thatastrongesttemporalformulaof

p q ( t )q

^implies

A

^{. Thenextcorollary}

states a property that one would expect of recursive calls, i.e., if

B

^is

satised by

q ⁰ s

^{body then}

B [ v/x ]

^{should be satised by}

q ( t )

^provided

that

t = v

^.

Corollary 5.3 Given

p q ( x )

^def

= P _q q

^{, suppose that}

q, qarg

^{do not occur}

free in

B

^and

p P _q q ` B

^{. Then for all}

v ∈ Dom

^,

p q ( t )q ` t = v ⇒ B [ v/x ] .

5.2 Cells

Cells provide a basis for the specication and analysis of mutable and

persistentdata structuresasshown forthe

π

^{calculus[26]. Acell canbe}

thought of as a structure that contains a value, and if tested, it yields

thisvalue. Amutable cell isacellthatcanbeassignedanewvalue 2

. We

modelmutable cells of the form

x : ( v )

^{, which we interpret as a variable}

x

^{currently xed tosome}

v

^.

x : ( z )

^def

= tell ( x = z ) k unless change ( x ) next x : ( z ) f _exch ( x, y )

^def

= P

v when ( x = v ) do ( tell ( change ( x )) k tell ( change ( y )) next ( p x : ( f ( v ))q k p y : ( v )q ) )

Denition

x : ( z )

^{represents a cell}

x

^{whose current content is}

z

^{. The}

current content of

x

^{will be the same in the next time interval unless it}

istobechangednext(i.e

change ( x )

^{). Denition}

f _exch ( x, y )

^{represents an}

exchange operation between the contents of

x

^and

y

^{. If}

v

^is

x

^{'s current}

value then

f ( v )

^and

v

^{will be the next}

x

^and

y ⁰ s

^values, respectively. In the case of functions that always returnthe same value (i.e. constants),

we will take the liberty of using that value as its symbol. For example,

p x :(3)q k p y :(5)q k p7 exch ( x, y )q

^{gives usthe cells}

x :(7)

^and

y :(3)

^{in the}

next time interval.

The following temporal property states the invariant behavior of a

cell, i.e., if itsatises

A

^{now, it willsatisfy}

A

^{next unlessit is changed.}

Proposition5.4 For all

v ∈ Dom

^,

p x :( v )q ` ( A ∧¬ change ( x )) ⇒ ◦ ^A

2

A richer notionof cell canbe found in ccp basedmodels, either as aprimitive

construct(theOzcalculus[36])orasaderivedconstruct(

π ⁺

^{calculus[9],andPiCO}

[1]).