BRICS RS-01-20 Palamidessi & Valencia: A Temporal Concurrent Constraint Programming Calculus 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 \begin{matrix}c \\ ◯ \end{matrix} 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/

A Temporal Concurrent Constraint Programming Calculus

Catuscia Palamidessi  Frank D. Valencia

June 2001

Abstract

The tcc model is a formalism for reactive concurrent constraint programming. In this paper we propose a model of temporal concurrent constraint programming which adds to tcc the capability of modeling asynchronous and non-deterministic timed behavior. We call this tcc extension the ntcc calculus. The expressiveness of ntcc is illustrated by modeling cells and asynchronous bounded broadcasting, by specifying temporal requirements such as response and invariance, and by modeling timed systems such as RCX controllers. We present a denotational semantics for modeling the strongest-postcondition behavior of ntcc processes, and, based on this semantics, we develop a proof system for proving linear temporal properties of these processes.

1 Introduction

Research on concurrent constraint programming (ccp) for timed systems has attracted growing interest in the last years. Timed systems often involve specific domains (e.g., controllers, databases, reservation systems) and have time-constraints specifying their behavior (e.g., the lights must be switched on within the next three seconds). The ccp model enjoys a dual operational and declarative logical view allowing, on the one hand, programs to be expressed using a vocabulary and concepts appropriate to the specific domain, and on the other hand, to be read and understood as (logical) specifications. An obvious benefit of this view is to provide the developer with one domain specific ccp language suitable for both the specification and implementation of programs. Indeed, several timed extensions of ccp have been developed in order to provide settings for the programming and specification of timed systems with the declarative flavor 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 generalizes both concurrent logic programming ([34]) and constraint logic programming ([19]). A fundamental issue in ccp is the specification of concurrent systems by means of constraints. A constraint (e.g. x + y > 10) represents partial information about certain variables. During the computation, the current state of the system is specified by a set of constraints (store). Processes synchronize by asking and telling information. Whenever a process asks some information not yet entailed by the current store, it blocks, and remains blocked until some other process adds (tells) the requested information to the store.

In the ccp model processes are built by using the basic actions ask and tell, and the operators of parallel composition, hiding, recursion and guarded-choice. Unlike other models of concurrency, without guardedchoice the model is deterministic, namely the result of a finite computation is always the same, independently from the execution order (scheduling) of the parallel components ([33]).

1.2 Reactive Concurrent Constraint Programming: the tcc model

The tcc model ([31]) is a formalism for reactive ccp which combines deterministic ccp with ideas from the Synchronous Languages ([4], [15]). Whenever a tcc process receives a stimulus (partial information) c from the environment, it executes a deterministic ccp process P with c as initial store. In a bounded period of time, P reaches a resting point, and returns the information contained in the final store as a response to the environment. The residual ccp process at the resting point, P′, determines the ccp process P′′ to be executed in the next time interval. Each stimulus-response interaction between a process and its environment defines a time unit (or time interval). Since the computation in each time interval is deterministic, tcc is deterministic.

Many interesting temporal constructs can be expressed in tcc. In particular, the do P watching c construct of ESTEREL [4], which executes P continuously until the signal c is present. In general, tcc allows processes to be “clocked” by other processes, thus allowing meaningful pre-emption constructs.

1.3 A Model of Temporal Concurrent Constraint Programming

Being a model of reactive ccp based on the Synchronous Languages ([4], [15]) (i.e. programs must be determinate and respond immediately to input signals), the tcc model is not meant for the specification of nondeterministic 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 the delivery time” cannot be expressed within the model. It also rules out 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-determinism is useful.

In general, a benefit of allowing the specification of non-deterministic behavior is to free programmers from the necessity of coping with issues that are irrelevant to the problem specification. 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 a more straightforward presentation of programs.

This view is consistent with the declarative flavor of ccp: The programmer specifies by means of constraints the possible values that the program variables can take, without being required to provide a computational procedure to enforce the corresponding assignments. Constraints state what is to be satisfied but not how. Following this line of reasoning, we argue for a formalism for temporal programming where programs and specifications can be given in the same language. For example, we may think of the ccp program tell(x > 5) as a specification satisfied by the ccp programs (or refinements) tell(x = 7) and tell(x > 11).

Moreover, a very important benefit of allowing the specification of non-deterministic (and asynchronous) behavior arises when modeling the interaction among several components running in parallel, in which one component is part of the environment of the others. These systems often need non-determinism to be modeled faithfully.

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 nondeterministic behavior and an unbounded finite-delay operator for asynchronous behavior. Computation in ntcc progresses as in tcc, except for the non-determinism induced by the new constructs. The calculus allows for the specification of temporal properties, and for modeling (and expressing constraints upon) the environment, both of which are useful in proving properties of timed systems.

We will illustrate the expressiveness of ntcc by modeling several constructs such as cells, asynchronous bounded broadcasting, response and invariance, that in turn are useful for specifying timed systems. We also illustrate some applications involving RCX^{TM} controllers.

The declarative nature of ntcc comes to the surface when we consider the denotational characterization of the strongest postcondition observables, as defined 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 kind of guarded-choice allowed within the scope of local variables, which we shall call local-independent choice (i.e, either guards without free occurrences of local variables, internal or mutually exclusive choice), we also obtain completeness.

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) logic constructs ([7]). Following the lines of the proof system proposed in [7] for ccp, we develop a sound system for proving 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 for tcc as well, since every tcc process falls into the category of local-independent choice ntcc processes. The proof system for tcc in [31], whose underlying logic is intuitionistic rather than classical, is complete for hiding (and recursion) free tcc processes only.

We also report on current research on our notion of equality for ntcc: two processes are equivalent iff no context can distinguish them wrt to the input-output behavior. We show the existence of an universal (distinguishing) context and that such an equality is decidable for hiding-free and bounded non-deterministic processes.

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

(1) a model of temporal concurrent constraint programming that extends the specification power of the tcc model, (2) a denotational semantics capturing the strongest postcondition behavior of a ntcc process, (3) a proof system for proving whether a given ntcc process satisfies a property specified in linear temporal logic, and (4) an study of a natural behavioral equivalence for our calculus.

2 The Calculus

In this section we present the syntax and an operational semantics of the ntcc calculus. First we recall the notion of constraint system.

2.1 Constraint Systems

Concurrent constraint languages are parametrized by a constraint system. Basically, a constraint system defines the underlying universe of the particular language. It provides a signature from which syntactically denotable objects in language called constraints can be constructed, and an entailment relation specifying interdependencies between such constraints. For our purposes it will suffice to consider the notion of constraint system based on First-Order Predicate Logic, as it was done in [35]^{1}.

Definition 2.1 A constraint system is a pair (Σ, Δ) where Σ is a signature specifying functions and predicate symbols, and Δ is a consistent first order theory.

Given a constraint system (Σ, Δ), let L be the underlying first-order language (Σ, V, S), where V = {x, y, z, … } is the set of variables and S is the set containing the symbols ˙¬, ˙∧, ˙⇒, ˙∃, ṫrue, and ḟalse which denote logical negation, conjunction, implication, existential quantification, and the always true and always false predicates, respectively. Constraints, denoted by c, d, … are first-order formulae over L. We say that c entails d in Δ, written c ⊢_{Δ} d (or just c ⊢ d when no confusion arises), if c ˙⇒ d is true in all models of Δ. We write c ≈ d iff 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.

1See [33] for a more general notion of constraints based on Scott’s information systems.

2.2 Syntax

Processes P, Q, … ∈ Proc are built from constraints c ∈ C and variables x ∈ V in the underlying constraint system by the following syntax.

P, Q, …::= tell(c) | ∑_{i∈I} when c_{i} do P_{i} | P ∥ Q | local x in P
| next P | unless c next P | ! P | ⋆ P

Informally, the intended behavior is the following: The process tell(c) adds the constraint c to the current store, thus making c available to other processes in the current time interval. The guarded choice ∑_{i∈I} when c_{i} do P_{i}, where I is a finite set of indexes, represents a process 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 “∑_{i∈I}” when I is a singleton set. In case I = ∅, we write skip. We use the symbol “+” to indicate binary summations. Finally, we use ∑_{i∈I} P_{i} as an abbreviation for ∑_{i∈I} when (ṫrue) do P_{i} (i.e., blind choice).

The process P ∥ Q represents the parallel activation of P and Q. We use ∏_{i∈I} P_{i}, where I is finite, to denote the parallel composition of all P_{j}, for j ∈ I.

The process local x in P behaves like P, except that all the information on x produced by P can only be seen by P, and the information on x produced by other processes cannot be seen by P. We use local x̄ in P as a shorthand for local x_{1} in (local x_{2} in (… (local x_{n} in P) …)), where x̄ represents the sequence x_{1}x_{2} … 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 activated only if c cannot be inferred from the current store. The “unless” processes add (weak) time-outs to the calculus, i.e., they wait one time unit for a piece of information c to be present and if it is not, they trigger activity in the next time interval. We use next^{n}(P) as an abbreviation for next(next(… (next P) …)), where next is repeated n times.

The operator “!” is a delayed version of the replication operator for the π−calculus ([26]): ! P represents P ∥ next P ∥ next^{2}P ∥ …, i.e. unboundely many copies of P but one at a time, so there is no risk of infinite activity within a time interval. The replication operator is the only way of defining infinite behavior through the time intervals. The operator “⋆” is reminiscent of the finite delay operator for synchronous CCS ([25]) and it allows us to express asynchronous behavior through the time intervals. The process ⋆ P represents a finite 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 the previous constructs. We use !_{I}P and ⋆_{I}P, where I is finite, as an abbreviation for ∏_{i∈I} next^{i}P and ∑_{i∈I} next^{i}P, respectively. For instance, ⋆_{[m,n]}P means that P is eventually active between the next m and m + n time units, while !_{[m,n]}P means that P is always active between the next m and m + n time units.

2.3 Some examples

We now show some examples illustrating specification of temporal behavior in ntcc such as response requirements. Assume that the underlying constraint system includes the predicate symbols in {Off,TurnOn,OutofOrder,OverHeated}. Consider the “power saving” process

! (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 off, unless the environment (or another process) tells P that the lights are already turned off. Process P is always active. We may want, however, to specify that the light must be turned off not only eventually but within the next 60 time units. A process specifying this and thus “refining” the previous one would be

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

Finally, we may also want to write an “implementation” of these specifications. For instance, the process

! (unless (Off (lights)) next tell (Off (lights))) is one of the possible deterministic processes implementing the above two.

Another example is the specification of (bounded) invariance requirements. Consider the following two processes:

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

The first 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 detects that M is overheated, tells other processes that M should not be turned on during the next t time units.

2.4 An operational semantics for ntcc

We define now an operational semantics for ntcc which formalizes the intended meaning explained above.

2.4.1 The store and the configurations

Operationally, the current information is represented as a constraint c ∈ C, so-called store. Our operational semantics is given by considering transitions between configurations γ of the form ⟨P, c⟩. We define Γ as the set of all configurations. Following standard lines, we extend the syntax with a construct 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, ṫrue) 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 defining the “relevant” free variables of c as fv(c) = {x ∈ V | ∃_{x}c ≉ c}. For instance, we have fv(x = x ˙∧y > 1) = {y}. For the bound variables, define bv(c) = {x ∈ V | x occurs in c} − fv(c). Regarding processes, define fv(tell(c)) = fv(c), fv(∑_{i} when c_{i} do P_{i}) = ⋃_{i} fv(c_{i}) ∪ fv(P_{i}), and similarly for the bound variables. Further, define fv(local x in P) = fv(P) − {x} and bv(local x in P) = bv(P) ∪ {x}. The other cases are defined inductively in the obvious way.

Definition 2.2 (Structural congruence) Let ≡ be the smallest congruence relation over processes satisfying the following laws:

1. (Proc/_{≡}, ∥, skip) is a symmetric monoid.

2. P ≡ Q if they only differ by a renaming of bound variables.

3. next skip ≡ skip next(P ∥ Q) ≡ next P ∥ 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 ∥ Q) ≡ P ∥ local x in Q if x ∉ fv(P)

We extend ≡ to configurations by defining ⟨P, c⟩ ≡ ⟨Q, c⟩ if P ≡ Q. One interesting property of our calculus is that it admits a notion of

standard form:

Definition 2.3 A process P of the form

local x̄ in ∏_{i∈[0,n]} next^{i} (∏_{j_{i}} P_{j_{i}} ∥ ∏_{k_{i}} unless c_{k_{i}} next Q_{k_{i}} ∥ ∏_{l_{i}}! Q_{l_{i}} ∥ ∏_{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}} is itself a standard form.

Proposition 2.4 Every process P in the original syntax (i.e. with no occurrences of constructs of the form local (x, c) in P) is structurally congruent 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 ⟨P, c⟩ ⟶ ⟨Q, d⟩ should be read as “P with store c reduces, in one internal step, to Q with store d”. The observable transition P ⟹^{(c,d)} Q should be read as “P on input c reduces, in one time unit, to Q with store d”. As in tcc, the store does not transfer automatically from one interval to another.

We now give a description of the operational rules. Rules TELL, CHOICE, and PAR are standard. The intuition behind LOC is the following: From the internal point of view of P, the global information about the variable x cannot be observed. Thus, in order to reduce ⟨local (x, c) in P, d⟩, we should first hide the information about x that d may have. We do this by existentially quantifying x in d. From the external point of view, the internal information produced in c′ about x cannot be observed, thus we quantify x in c′ in the global store. Additionally, c′ becomes the new private store of the process for its future evolutions.

Rule UNLESS says that if c is entailed by the current store, then the execution of the process P (in the next time interval) is precluded. Rule REPL specifies 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 only way of specifying infinite behavior, it follows that there can be only finitely many internal transitions in one time unit. STAR says that ⋆ P triggers P in some time interval (either in the current one or in a future one). Rule STRUCT simply says that structurally congruent processes have the same reductions.

Rule OBS says that an observable transition from P labeled by (c, d) is obtained by performing a finite sequence of internal transitions from ⟨P, c⟩ to ⟨Q, d⟩, 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 any local information which has been stored in Q, and by “unfolding” the sub-terms within next R expressions. More precisely:

Definition 2.5 F : P roc → P roc is defined as follows:

F (P) = \{ \begin{matrix}Q & if P = next Q or P = unless c next Q \\ F (P_{1}) ∥ F (P_{2}) & if P = P_{1} ∥ P_{2} \\ local x in F (Q) & if P = local (x, c) in Q \\ skip & otherwise \end{matrix}

Note that both F (! P) and F (⋆ P) are defined to be skip because neither ! P nor ⋆ P occurs at the top level in a final configuration.

We conclude this section illustrating how processes evolve through the time intervals. An (infinite) sequence of observable transitions

P_{1} ⟹^{(c_{1},c′_{1})} P_{2} ⟹^{(c_{2},c′_{2})} P_{3} ⟹^{(c_{3},c′_{3})} …

can be interpreted as a stimulus-response interaction between the process P_{1} and an environment. At the time unit i, the environment provides a stimulus c_{i} and the system P_{i} produces c′_{i} as response. If α = c_{1}.c_{2}.c_{3}…. and α′ = c′_{1}.c′_{2}.c′_{3} …, we represent the above interaction by the notation

P_{1} ⟹^{(α,α′)}^{∞}

A run can alternatively be interpreted as an interaction among the parallel components in the initial system (each component being part of the environment of the others): if α = ṫrue.ṫrue.ṫrue …, i.e., the input sequence is empty, then α′ can be regarded as a timed observation of such an interaction.

3 Strongest postconditions: denotation and logic for ntcc

In this section we introduce a notion of observables suitable to be represented logically, and we investigate its denotational counterpart.

In the following we use α, α′ to represent elements of C^{∞} and β to represent an element of C^{∗}. Given c ∈ C , c.α represents the concatenation of c and α. Furthermore, β.α represents the concatenation of β and α. We use ˙∃_{x}α to represent the sequence obtained by applying ˙∃_{x} to each constraint in α. Notation α(i) denotes the i-th element in α.

Definition 3.1 (Observables) 1. The input-output (or stimulus-response) relation of a process P is defined as

io(P) = {(α, α′) | P ⟹^{(α,α′)}^{∞}}

2. The quiescent sequences of a process P are defined as

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

Following [7] we shall refer to sp(P) as the strongest postcondition of P (wrt C^{∞}) as it satisfies the following:

Proposition 3.2 α ∈ sp(P) iff there exists α′ such that P ⟹^{(α′,α)}^{∞}.

3.1 Denotational semantics

We give now a denotational characterization of the strongest postcondition observables of ntcc, following ideas developed in [7] and [31] for the ccp and tcc case, respectively. The presence of non-determinism, however, presents a technical problem to deal with: The observables for the hiding operator cannot be specified compositionally (see [7]). Therefore, we will have to identify a practical fragment for which the semantics is complete wrt our observables.

The denotational semantics is defined as a function [[·]] which associates to each process a set of infinite constraint sequences, namely [[·]] : Proc → P(C^{∞}). The definition of this function is given in Table 2.

Intuitively, [[P]] is meant to capture the quiescent sequences of a process P. For instance, the sequences to which tell(c) cannot add information are those whose first element is stronger than c (D1). Process next P has not influence in the first element of a sequence, thus d.α is quiescent for it if α is quiescent for P (D5). A sequence is quiescent for ! P if every suffix of it is quiescent for P (D7). A sequence is quiescent for ⋆ P if there is a suffix of it which is quiescent for P (D8). The other rules can be explained analogously.

Remark 3.3 The ! and the ⋆ operators are dual. In fact, we could have defined

\begin{aligned}[[! P]] & = & ν_{X} & ([[P]] ∩ \{d.α | d ∈ C , α ∈ X \}) \\ [[⋆ P]] & = & μ_{X} & ([[P]] ∪ \{d.α | d ∈ C , α ∈ X \}) \end{aligned}

where ν and μ represent respectively the greatest and the least fix-point operators in the complete lattice (P(C^{∞}), ⊆).

Next theorem states the relation between the denotational semantics of a ntcc process and its strongest postconditions.

Theorem 3.4 (Soundness) For every ntcc process P, sp(P) ⊆ [[P]].

For the reasons mentioned at the beginning of this section, the converse of this theorem does not hold in general. As in ccp, in ntcc the converse holds for restricted choice processes, namely those ntcc processes in which, for every construct of the form ∑_{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 ≠ ḟalse such that d ⊢ c_{i} and d ⊢ c_{j}, then c_{i} = c_{j}. Blind-choice processes are a typical case of restricted-choice. The condition required for restricted-choice processes implies structural confluence in the sense of [10], namely the outcome of a process does not depend upon the scheduling strategy on its parallel components.

Nevertheless, for ntcc we can show that the converse holds for a larger set of processes which we call local-independent choice processes. These are processes in which, for every construct ∑_{i∈I} when c_{i} do P_{i} occurring within a process local x in Q, either (a) x ∉ ⋃_{i∈I} fv(c_{i}), or (b) the c_{i}’s are pairwise mutually exclusive or equivalent. This fragment is practical since every restricted-choice process is also local-independent choice and, unlike the restricted-choice fragment, its condition does not imply structural 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 in Section 5).

Theorem 3.5 (Completeness) If P is a local-independent choice ntcc process, then sp(P) = [[P]].

For deterministic processes such as tcc processes, namely those which contain neither the choice (except when the index set is a singleton) nor the ⋆ operator, we have an even stronger result: the semantics allows to retrieve the input-output relation (which for deterministic processes is a function). Let us use ≤ to denote the (partial) order relation {(α, α′) | ∀i ≥ 1 α′(i) ⊢ α(i)} and min(S) to denote the minimal element of S ⊆ C^{∞} in the complete lattice (C^{∞}, ≤).

Theorem 3.6 If P is a deterministic process, then (α, α′) ∈ io(P) iff α′ = min([[P]]∩ ↑ α), where ↑ α = {α′′|α ≤ α′′}.

4 A logic for ntcc

In this section we define a linear temporal logic for expressing properties of ntcc processes.

4.1 Syntax

The temporal logic formulae A, B, ... ∈ A are defined 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 intended meaning of the other symbols is the following: ∨, ∧, ⇒, ¬ and ∃_{x} represent temporal logic disjunction, conjunction, implication, negation and existential quantification. These symbols are not to be confused with the logic symbols ˙∧, ˙⇒, ˙¬ and ˙∃_{x} of the constraint system. The symbols ∘, □, and ♢ denote the temporal operators next, always and sometime.

4.2 Semantics

The standard interpretation structures of linear temporal logic are infinite sequences of states [23]. In the case of ntcc, it is natural to replace states by constraints, and consider therefore as interpretations the elements of C^{∞}. We say that α ∈ C^{∞} is a model of A, notation α ⊧ A, if ⟨α, 1⟩ ⊧ A, where:

⟨α, i⟩ ⊧ c  iff α(i) ⊢ c
⟨α, i⟩ ⊧ ¬A  iff ⟨α, i⟩ |̸= A
⟨α, i⟩ ⊧ A_{1} ∨ A_{2} iff ⟨α, i⟩ ⊧ A_{1} or ⟨α, i⟩ ⊧ A_{2}
⟨α, i⟩ ⊧ A_{1} ∧ A_{2} iff ⟨α, i⟩ ⊧ A_{1} and ⟨α, i⟩ ⊧ A_{2}
⟨α, i⟩ ⊧ A_{1} ⇒ A_{2} iff ⟨α, i⟩ ⊧ A_{1} implies ⟨α, i⟩ ⊧ A_{2}
⟨α, i⟩ ⊧ ∘A  iff ⟨α, i + 1⟩ ⊧ A
⟨α, i⟩ ⊧ □A  iff for all j ≥ i ⟨α, j⟩ ⊧ A
⟨α, i⟩ ⊧ ♢A  iff there exists j ≥ i s.t. ⟨α, j⟩ ⊧ A
⟨α, i⟩ ⊧ ∃_{x}A  iff there exists α′ ∈ C^{∞} s.t. ˙∃_{x}α = ˙∃_{x}α′ and ⟨α′, i⟩ ⊧ A.

We define [[A]] to be the collection of all models of A. Formally:

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

4.3 Proving properties of ntcc processes

We are interested in assertions of the form P ⊢ A, whose intuitive meaning is that the strongest postcondition of P satisfies the property expressed by A.

An inference system for such assertions is presented in Table 3. We will say that P ⊢ A holds if the assertion P ⊢ A has a proof in this system.

The following theorem states the soundness and the relative completeness of the proof system.

Theorem 4.1 For every ntcc process P and every formula A, P ⊢ A holds iff [[P]] ⊆ [[A]] holds.

Note: the reason why this theorem is called “relative completeness” is because of the side condition in Rule P9 (consequence rule): the proof system is complete modulo the capability of proving the formulae of the form A ⇒ B which we need to use in a proof. Proving A ⇒ B is known to be decidable for the quantifier-free fragment of linear time temporal formulae ([23]) as well as for some other interesting first-order fragments (see [17]).

From Theorems 4.1, 3.4 and 3.5 we immediately derive the following:

Corollary 4.2 1. For every ntcc process P and every formula A, if P ⊢ A holds then sp(P) ⊆ [[A]] holds.

2. For every local-independent choice ntcc process P and every formula A, P ⊢ A holds iff 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 is complete for tcc.

The following notion will be useful in the Section 5, for discussing properties of our examples.

Definition 4.3 A formula A is the strongest temporal formula 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 definition of such formula.

Definition 4.4 The function stf : Proc → A is defined as follows:

stf (tell(c))  = c
stf (∑_{i∈I} when (c_{i}) do P_{i}) = (⋁_{i∈I} c_{i} ∧ stf (P_{i})) ∨ ⋀_{i∈I} ¬c_{i}
stf (P ∥ 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 these we have:

Proposition 4.5 For every process P, stf (P) is the strongest temporal formula derivable for P.

Note that to prove that P ⊢ A is sufficient to prove that stf (P) ⇒ A. However, to prove such implication may not be always feasible or possible. The proof system provides the additional flexibility of proving P ⊢ A by using the consequence rule (P9) on subprocesses of P and on formulae different from A.

5 Applications

In this section we illustrate some ntcc examples. We first need to define an underlying constraint system.

Definition 5.1 Let max be a positive integer number. Define FD[max] as the constraint system whose signature Σ includes symbols in {0, succ, +, ×, =} and the first-order theory Δ is the set of sentences valid in arithmetic modulo max.

The intended meaning of FD[max] is the natural numbers interpreted as in arithmetic modulo max. Henceforth, we assume that the signature is extended with two new unary predicate symbols call and change. We will designate Dom as the set {0, 1, ...., max − 1} and use v and w to range over its elements.

5.1 Recursion

Often it is convenient to specify behavior by using recursive definitions. 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 definitions of the form q(x) =^{def} P_{q}, where q is the process name and P_{q} contains at most one occurrence of q which must be within the scope of a “next” and out of the scope of any “!”. The reason for such a restriction is that we want to keep bounded the response time of the system: we do not want P_{q} to make infinitely or unboundely many recursive calls of q within the same time interval.

We also want to consider the call-by-value. This may look unnatural since in constraint programming the natural parameter passing mechanism is through “logical variables”, like in logic programming. Indeed, it is more difficult to encode in ntcc call-by-value than “call-by-logical-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 variables are not maintained from one interval to the next. More precisely: The intended behavior of a call q(t), where t is a term fixed to a value v (i.e. t = v in the current store), is that of P_{q}[v/x], where [v/x] is the operation of (syntactical) replacement of every occurrence of x by v.

We now show how to encode such a kind of recursion by using replication. Given q(x) =^{def} P_{q}, we will use q, qarg to denote any two variables not in fv(P_{q}). Let ⌜x := t⌝ be defined as the process ∑_{v} when t = v do ! tell(x = v), i.e., the persistent assignment of t’s fixed value to x. Then the ntcc process corresponding to definition of q(x), denoted as

⌜q(x) =^{def} P_{q}⌝, is :

! (when call(q) do local x in (⌜x := qarg⌝ ∥ ⌜P_{q}⌝)) ,

where ⌜P_{q}⌝ denotes the process that results from replacing in P_{q} each q(t) with tell(call(q)) ∥ tell(qarg = t) (thus telling that there is a call of q with argument t). Intuitively, whenever the process q is called with argument qarg, the local x is assigned the argument’s value so it can be used by q’s body ⌜P_{q}⌝.

We then consider the calls q(t) in other processes. Each such a call is replaced by local q qarg in (⌜q(x) =^{def} P_{q}⌝ ∥ tell(call(q)) ∥ tell(qarg = t)), which we shall denote by ⌜q(t)⌝. The local declarations are needed to avoid interference with other recursive calls.

The above encoding generalizes easily to stratified recursion and to the case of arbitrary number of parameters including the parameterless recursion of tcc considered in [31]. We now show some temporal properties satisfied by the encoding. Next theorem describes the strongest temporal formulae satisfied by ⌜q(t)⌝.

Proposition 5.2 Given ⌜q(x) =^{def} P_{q}⌝, let B the strongest temporal formula derivable for ⌜P_{q}⌝. Then the temporal formula

∃_{q,qarg}(call(q)∧qarg = t∧□(call(q) ⇒ ∃_{x}(B∧⋀_{w}(qarg = w ⇒ □x = w)))

is the strongest temporal formula derivable for ⌜q(t)⌝

This theorem expresses the essence of our encoding of recursion in terms of linear temporal logic. It gives us a proof principle for recursive definitions, i.e., in order to prove that ⌜q(t)⌝ ⊢ A it is sufficient to prove that a strongest temporal formula of ⌜q(t)⌝ implies A. The next corollary states a property that one would expect of recursive calls, i.e., if B is satisfied by q′s body then B[v/x] should be satisfied by q(t) provided that t = v.

Corollary 5.3 Given ⌜q(x) =^{def} P_{q}⌝, suppose that q, qarg do not occur free in B and ⌜P_{q}⌝ ⊢ B. Then for all v ∈ Dom, ⌜q(t)⌝ ⊢ t = v ⇒ B[v/x].

5.2 Cells

Cells provide a basis for the specification and analysis of mutable and persistent data structures as shown for the π calculus [26]. A cell can be thought of as a structure that contains a value, and if tested, it yields this value. A mutable cell is a cell that can be assigned a new value^{2}. We model mutable cells of the form x: (v), which we interpret as a variable x currently fixed to some v.

x: (z)  =^{def} tell(x = z) ∥ unless change(x) next x: (z)
f_{exch}(x, y) =^{def} ∑_{v} when (x = v) do ( \begin{matrix}tell(change(x)) ∥ tell(change(y)) \\ next( ⌜x: (f(v))⌝ ∥ ⌜y: (v)⌝) ) \end{matrix}

Definition 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 is to be changed next (i.e change(x)). Definition 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 return the same value (i.e. constants), we will take the liberty of using that value as its symbol. For example, ⌜x:(3)⌝ ∥ ⌜y:(5)⌝ ∥ ⌜7_{exch}(x, y)⌝ gives us the 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 it satisfies A now, it will satisfy A next unless it is changed.

Proposition 5.4 For all v ∈ Dom, ⌜x:(v)⌝ ⊢ (A∧¬change(x)) ⇒ ∘A

2A richer notion of cell can be found in ccp based models, either as a primitive construct (the Oz calculus [36]) or as a derived construct (π^{+} calculus [9], and PiCO [1]).

5.3 Zigzagging

An RCX is a programmable, microcontroller-based LEGO^{\begin{matrix}r \\ ◯ \end{matrix}} brick used to create autonomous robotic devices (see [22], [18]). Zigzagging [11] is a task in which an (RCX-based) robot can go either forward, left, or right but (1) it cannot go forward if its preceding action was to go forward,

(2) it cannot turn right if its second-to-last action was to go right, and (3) it cannot turn left if its second-to-last action was to go left.

In order to model this problem, without over-specifying it, we use guarded choice and cells. We use cells act_{1} and act_{2} to be able to “look back” one and two time units, respectively. We use three distinct f , r, l ∈ Dom − {0} (standing for forward, right and left respectively) and three distinct forward, right, left ∈ C.

GoForward =^{def}  ⌜f_{exch}(act_{1} , act_{2} )⌝ ∥ tell(forward)
GoRight  =^{def}  ⌜r_{exch}(act_{1} , act_{2} )⌝ ∥ tell(right)
GoLeft  =^{def}  ⌜l_{exch}(act_{1} , act_{2} )⌝ ∥ tell(left)
Zigzag  =^{def} ( when (act_{1} ≠ f ) do ⌜GoForward⌝
+ when (act_{2} ≠ r) do ⌜GoRight⌝
+ when (act_{2} ≠ l) do ⌜GoLeft⌝ )
∥ next Zigzag
StartZigzag =^{def}  ⌜act_{1}:(0)⌝ ∥ ⌜act_{2}:(0)⌝ ∥ ⌜Zigzag⌝

Initially cells act_{1} and act_{2} contain neither f , r nor l. Just before a choice is made act_{1} and act_{2} contain the previous and the second-to-last taken actions (if any). After a choice is made according to (1), (2) and (3), the choice is recorded in act_{1} and the previous choice moved to act_{2} . The definitions of the various processes are self-explanatory.

The next temporal property states that the robot chooses to go right and left infinitely often.

Proposition 5.5 ⌜StartZigzag⌝ ⊢ □(♢right ∧ ♢left)

Other RCX examples modeled by ntcc includes a crane [37] and a wall-avoiding robot [37].

5.4 Value-passing Communication

Value passing plays an important role in process calculus. Suppose that x ↑ (v) denotes the action of writing a value (or message) v in channel x which is then kept in the channel for one time unit. We assume that in the same time unit, two different values cannot be written in the same channel. The notation x ↓_{P [y]} represents the action of reading, without consuming, the value (if any) in channel x which is then used in P. The variable y, which may occur free in P, is the placeholder for the read value. Several read actions can get the same value if they read the same channel in the same time interval. These basic actions can be defined as x ↑ (y) =^{def} tell(x = y) and x ↓_{P [y]}=^{def} ∑_{v} when (x = v) do local y in (! tell(y = v) ∥ P).

Having defined the two basic actions, we can specify different behaviors, e.g., process ! ( ⋆_{[0,1]}(x ↓_{P [y]})) checks “very often” for messages in channel x. Here we illustrate a form of asynchronous broadcasting communication.

SendAsyn_{x}(y) =^{def} ⋆(⌜x ↑ (y)⌝)
Waiting_{Q,x}  =^{def} local stop in ( \begin{matrix}⌜x ↓_{(Q∥tell(stop=1))[y]}⌝ \\ ∥ unless stop = 1 next Waiting_{Q,x}). \end{matrix}

Process SendAsyn_{x}(v) asynchronously sends value v in channel x. Process Waiting_{Q,x} waits for a value in channel x. Note that, if a process is waiting at the time SendAsyn_{x}(v) is executed, then it is guaranteed to get the value, while other processes may not get it. This property is expressed by the following result.

Proposition 5.6 Suppose that Q ⊢ B and stop ∉ fv(Q). Then for all v ∈ Dom,

⌜SendAsyn_{x}(v)⌝ ∥ ⌜Waiting_{Q,x}⌝ ⊢ ♢B[v/y]

6 Behavioral Equivalence

We wish to distinguish between the observable behavior of processes P and Q if the distinction can somehow be detected by a process interacting with them. A natural observation is the input-output behavior of P (Definition 3.1). Let ∼_{io} be defined by P ∼_{io} Q iff io(P) = io(Q). Let us consider

P = when ṫrue do tell(a) + when (b) do tell(c)
Q = when ṫrue do tell(a) + when (b) do tell(c)

+

when ṫrue do (tell(a) ∥ when (b) do tell(c))

Assuming that a, b, c are non equivalent constraints such that c ⊢ b ⊢ a, we can verify that P ∼_{io} Q, but P ∥ R ≁_{io} Q ∥ R where R = when a do tell(b). This tells us that ∼_{io} is not a congruence and that we can distinguish P from Q if we make R to interact with them. Therefore, let ≈_{io} be the corresponding congruence equating processes iff they are (input-output) indistinguishable, i.e., P ≈_{io} Q iff for every process context C[.], C[P] ∼_{io} C[Q]. The relation ≈_{io} is our first proper notion of equality for the calculus.

Moreover, let us consider the language of a process P, l(P) = {α | (true.true …, α) ∈ io(P)}, i.e., the set of outputs on the “empty” input sequence. As in the input-output case, we define ∼_{l} and ≈_{l} as the corresponding language equivalence and language congruence. Obviously, relation ∼_{l} is weaker than ∼_{io}, however, the corresponding congruences coincide, i.e:

Proposition 6.1 ∼_{io} ⊆ ∼_{l} and ≈_{io} = ≈_{l}

We next investigate the type of contexts needed to verify P ≈_{io} Q and focus on relation ≈_{l} as it is equivalent to ≈_{io}. We first observe that it is enough to consider parallel contexts, i.e.,

Proposition 6.2 P ≈_{l} Q iff for all R, R ∥ P ∼_{l} R ∥ Q.

Furthermore, we show that in ntcc we have the notion of universal context, i.e., a context that can distinguish two processes iff they are not language (or input-output) congruent. Recall C is the set of representatives of equivalent classes of constraints in the constraint system (Σ, Δ). In what follows β ranges over elements of C^{∗}. Let us assume that the signature Σ is extended to a signature Σ′ with unary predicates t_{β} and w_{β} for each β. These predicates are allowed to occur only in the process contexts U^{S}[.] defined below. We assume that C is still defined wrt the original signature so it does not involve any t_{β} or w_{β} predicates.

Definition 6.3 Let S ⊆_{fin} C. Define ≺_{S} = {(c, c′) ∈ S × S | c′ ⊢ c and c ⊬ c′} and ic(S) = {c_{1} … c_{n} ∈ S^{∗} | c_{1} ≺_{S} c_{2} ≺_{S} … ≺_{S} c_{n}}. For each β let W_{c.β} = when c do T_{β} and T_{c.β} = tell(c) ∥ W_{β} where T_{ϵ} = W_{ϵ} = skip . The distinguishing context wrt S, U^{S}[.] is defined as

!(( ∑_{β∈ic(S)} tell(w_{β}) ∥ W_{β}) + ( ∑_{β∈ic(S)} tell(t_{β}) ∥ T_{β})) ∥ [.]

Proposition 6.4 Suppose that C is finite. Then P ≈_{l} Q iff U^{C}[P] ∼_{l} U^{C}[Q].

Thus context U^{C}[.] is the universal context, provided that C is finite. Roughly speaking, in U^{C}[P], the distinguishing process in parallel with P, say D, can provide all infinite interactions P can have with other processes. Its selected interaction will be identified with an output (c_{1} ˙∧d_{1}).(c_{2} ˙∧d_{2})…. (with c_{i} ∈ {w_{β_{i}}, t_{β_{i}}}) of U^{C}[P]. When interacting with Q, D will be forced to select the same interaction in U^{C}[Q] to match the output of U^{C}[P].

Nevertheless, if C is not finite, we can construct specialized distinguishing contexts for arbitrary processes.

Definition 6.5 Let Λ ⊂_{fin} Proc. Define const(Λ) as the set whose elements are ṫrue, ḟalse and all constraints (module logical equivalence) from the closure under conjunction and existential quantification of the constraints occurring in Λ’s processes.

Proposition 6.6 Let Λ ⊂_{fin} Proc. For all P, Q ∈ Λ, P ≈_{l} Q iff U^{const(Λ)}[P] ∼_{l} U^{const(Λ)}[Q].

Therefore U^{const(Λ)} is an universal context for Λ’s processes. Apart from its theoretical value, the ability of constructing distinguishing contexts for arbitrary processes is important as it can be used for proving decidability results for ≈_{io}. Note that in order to verify P ≈_{l} Q it is sufficient to verify U^{const({P,Q})}[P] ∼_{l} U^{const({P,Q})}[Q]. It turns out that ∼_{l} is decidable for hiding and unbounded-delay free processes. The languages of these processes can be recognized by automata over infinite objects, more precisely Büchi Automata ([6]).

Proposition 6.7 ∼_{l} is decidable for hiding and unbounded-delay free processes.

Corollary 6.8 ≈_{l} and ≈_{io} are decidable for hiding and unbounded-delay free processes.

7 Related Work and Concluding Remarks

7.1 Related Work

The issue of developing a formalism for timed systems with both a logic and an operational flavor has been considered in several works, particularly in the area of temporal logic programming languages (tpl) ([5], [27], [3], [24]). These proposals provide the machinery for the direct execution of temporal formulas. Another example is the modal process logic (mpl) of [21], where process constructs are included as connectives and formulae are given operational interpretations. In contrast to tpl, our approach is not based on logic programming but on ccp. Consequently, some of the main advantages of ccp over logic programming can also be claimed for ntcc over tpl, in particular it provides us with a more algebraic view of process combinators. Ntcc and mpl are of a different nature: the former provides linear-time temporal specifications, whereas the latter provides branching-time ones. Being based on tcc, ntcc also provides a programming language while mpl is only a specification language.

The ntcc model was inspired in part by the recent work on real-time modeling of RCX micro-controllers programs ([18]). This work presents a method to synthesize control RCX programs by merging them with control automata. Constraints on the behavior of the control program are given in a temporal logic and then translated into control automata by using the Mona tool ([20]).

The works which are most closely related to our paper are those on tcc (timed ccp, [31]). Our proposal is a strict extension of tcc, in the sense that tcc can be encoded in (the restricted-choice subset of) ntcc, while the vice-versa is not possible because tcc does not have constructs to express non-determinism or unbounded finite-delay. In [31] the authors proposed also a proof system for tcc, based on an intuitionistic logic enriched with a next operator. The system however is partially complete; namely, it is complete only for hiding-free (and recursion-free) processes. In contrast our system is based on the standard classical temporal logic of ([23]) and is complete for local-indepent choice ntcc processes, hence also for tcc processes.

Other extensions of tcc have been proposed in [13, 14, 30]. None of these, however, consider non-determinism or unbounded finite-delay. In [13] default-tcc processes can evolve continuously as well as discretely. The language in [14] adds to default-tcc random assignments with some given distribution. Finally, the language proposed in [30] adds to tcc the possibility of expressing strong pre-emption: the “unless” can trigger activity in the current time interval. In contrast, ntcc can only express weak pre-emption. As argued in ([8]), in the specification of (large) timed systems weak pre-emption often suffices (and non-determinism is crucial). Nevertheless, strong pre-emption is important for modeling reactive systems. In principle, strong pre-emption could be incorporated in ntcc too: Semantically one would have to consider assumptions about the future evolutions of the system. As for the logic, one would have to consider a temporal extension of Default Logic [29])

The tccp calculus ([8]) is the only other proposal for a non-deterministic timed extension of ccp that we know of. As such, tccp provides a declarative language for the specification of (large) timed systems. In fact, interesting examples of specifying such systems are given in ([8]). An elegant denotational account for tccp is presented in [8], although no proof system or direct relation with temporal specifications is given. One major difference with our approach is that the information about the store is carried through the time units, so the semantic setting is rather different. Also, there is no operator for specifying (unbounded) finite-delay. Like ntcc, the deterministic fragment of tccp can be used to program reactive systems. A store that grows monotonically, however, may be inadequate for the kind of application we have in mind, like RCX micro-controllers.

7.2 Concluding remarks and future work

We introduced ntcc, a model of temporal concurrent constraint programming, and showed examples of its applicability to timed systems (e.g., RCX programs). We illustrated how ntcc can express various temporal requirements (e.g., bounded invariance and eventuality) and other constructs (e.g., cells and value passing processes). We provided a denotational semantics that approximates the notion of strongest postcondition of processes (in the sense of [7]) and identified an important fragment for which such a denotation is complete. We defined a linear temporal (classic) logic following the standard definition of [23], and related it with the denotational semantics. This allowed us to define what it means for a process to satisfy a linear temporal specification. Finally, we defined a (relatively) complete proof system for proving that a process satisfies a linear temporal specification, and we applied it to prove temporal properties of our examples.

Our current research in ntcc includes the study of the decidability of ≈_{io} for arbitrary ntcc processes. In the search of a fully-abstract fixpoint model with respect to this input-output behavior, we found that although ntcc allows countable non-determinism and infinite computations to happen (see [2] and [28] for impossibility results under these conditions), a relatively simple model seems to exist as a result of the particular nature of ntcc.

The plan for future research includes the extension of ntcc to a probabilistic model following ideas in [16]. This is justified by the existence of RCX program examples involving stochastic behavior which cannot be faithfully modeled with non-deterministic behavior. In a more practical setting we plan to define a programming language for RCX controllers based on ntcc.

Acknowledgments

We are indebted to Mogens Nielsen for having suggested and discussed this work. We thank Andrzej Filinski, Kim Larsen, Dale Miller, Maurizio Gabbrielli, Vineet Gupta, Radha Jagadeesan and Prakash Panangaden for helpful comments on various aspects of this work.

References

[1] G. Alvarez, J.F. Diaz, L.O. Quesada, C. Rueda, G. Tamura, F. Valencia, and G. Assayag. Integrating constraints and concurrent objects in musical applications: A calculus and its visual language. Constraints, jan 2001.

[2] Krzysztof R. Apt and Gordon D. Plotkin. Countable nondeterminism and random assignment. JACM, 33:724–767, 1986.

[3] H Barringer, M Fisher, D Gabbay, G Gough, and R Owens. Metatem: An introduction. Formal Aspects of Computing, 7(5):533– 549, 1995.

[4] G. Berry and G. Gonthier. The Esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19(2):87–152, November 1992.

[5] Christoph Brzoska. Temporal logic programming and its relation to constraint logic programming. In Kazunori Saraswat, Vijay; Ueda, editor, Proceedings of the 1991 International Symposium on Logic Programming (ISLP’91), pages 661–677, San Diego, CA, October 1991. MIT Press.

[6] J. R. Buchi. On a decision method in restricted second order arithmetic. In Proc. Int. Cong. on Logic, Methodology, and Philosophy of Science, pages 1–11. Stanford University Press, 1962.

[7] F. S. de Boer, M. Gabbrielli, E. Marchiori, and C. Palamidessi. Proving concurrent constraint programs correct. ACM Transactions on Programming Languages and Systems, 19(5):685–725, 1997.

[8] Frank de Boer, Maurizio Gabbrielli, and Maria Chiara Meo. A timed concurrent constraint language. Information and Computation, 1999. To appear.

[9] Juan Francisco Diaz, Camilo Rueda, and Frank Valencia. A calculus for concurrent processes with constraints. CLEI Electronic Journal, 1(2), December 1998.

[10] M. Falaschi, M. Gabbrielli, K. Marriott, and C. Palamidessi. Confluence in concurrent constraint programming. Theoretical Computer Science, 183(2):281–315, 1997.

[11] Jakob Fredslund. The assumption architecture, November 1999. BRICS, Progress Report.

[12] V. Gupta, R. Jagadeesan, and V. A. Saraswat. Computing with continuous change. Science of Computer Programming, 30(1–2):3– 49, January 1998.

[13] Vineet Gupta, Radha Jagadeesan, and Vijay Saraswat. Models for concurrent constraint programming. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR ’96: Concurrency Theory, 7th International Conference, volume 1119 of Lecture Notes in Computer Science, pages 66–83, Pisa, Italy, 26–29 August 1996. Springer-Verlag.

[14] Vineet Gupta, Radha Jagadeesan, and Vijay Saraswat. Probabilistic concurrent constraint programming. In Antoni Mazurkiewicz and Józef Winkowski, editors, CONCUR ’97: Concurrency Theory, 8th International Conference, volume 1243 of Lecture Notes in Computer Science, pages 243–257, Warsaw, Poland, 1–4 July 1997. Springer-Verlag.

[15] N. Halbwachs. Synchronous programming of reactive systems. Lecture Notes in Computer Science, 1427:1–16, 1998.

[16] O. Herescu and C. Palamidessi. Probabilistic asynchronous picalculus. FoSSaCS, pages 146–160, 2000.

[17] I. Hodkinson, F. Wolter, and M. Zakharyaschev. Decidable fragments of first-order temporal logics, 2000.

[18] Thomas S. Hune and Anders B. Sandholm. A case study on using automata in control synthesis. LNCS-1783, pages 349–362, 2000.

[19] J. Jaffar and J.-L. Lassez. Constraint logic programming. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, pages 111–119. ACM, ACM Press, 1987.

[20] Nils Klarlund and Anders Moller. MONA Version 1.3 User Manual. BRICS, jun 1998.

[21] Kim G. Larsen and Bent Thomsen. A modal process logic. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 203–210, Edinburgh, Scotland, 5–8 July 1988. IEEE Computer Society.

[22] H. H. Lund and L. Pagliarini. Robot soccer with LEGO mindstorms. Lecture Notes in Computer Science, 1604, 1999.

[23] Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, 1991.

[24] S. Merz. Efficiently executable temporal logic programs. Lecture Notes in Computer Science, 897, 1995.

[25] R. Milner. A finite delay operator in synchronous ccs. Technical Report CSR-116-82, University of Edinburgh, 1992.

[26] R. Milner. Communicating and Mobile Systems: the π-calculus. Cambridge University Press, 1999.

[27] B. Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, Cambridge, 1986.

[28] Sven-Olof Nyström. There is no fully abstract fixpoint semantics for non-deterministic languages with infinite computations. IPL, 60(6):289–293, 1996.

[29] R. Reiter. A logic for default reasoning. Artificial Intelligence, 13(1– 2):81–132, April 1980.

[30] V. Saraswat, R. Jagadeesan, and V. Gupta. Timed default concurrent constraint programming. Journal of Symbolic Computation, 22(5–6):475–520, November–December 1996.

[31] Vijay Saraswat, Radha Jagadeesan, and Vineet Gupta. Foundations of timed concurrent constraint programming. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 71– 80, Paris, France, 4–7 July 1994. IEEE Computer Society Press.

[32] Vijay A. Saraswat. Concurrent Constraint Programming. ACM Doctoral Dissertation Awards: Logic Programming. The MIT Press, Cambridge, MA, 1993.

[33] Vijay A. Saraswat, Martin Rinard, and Prakash Panangaden. The semantic foundations of concurrent constraint programming. In ACM, editor, POPL ’91. Proceedings of the eighteenth annual ACM symposium on Principles of programming languages, January 21– 23, 1991, Orlando, FL, pages 333–352, New York, NY, USA, 1991. ACM Press.

[34] E. Shapiro. The Family of Concurrent Logic Programming Languages. Computing Surveys, 21(3):413–510, 1990.

[35] Gert Smolka. A Foundation for Concurrent Constraint Programming. In Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, Munich, Germany, September 1994. Invited Talk.

[36] Gert Smolka. The Oz programming model. In Jan van Leeuwen, editor, Computer Science Today, Lecture Notes in Computer Science, vol. 1000, pages 324–343. Springer-Verlag, Berlin, 1995.

[37] Frank D. Valencia. Reactive constraint programming, June 2000. BRICS Progress Report - availabe via http://www.brics.dk/∼fvalenci/publications.html.

[38] G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993.

TELL  ⟨tell(c), d⟩ ⟶ ⟨skip, d ˙∧c⟩
CHOICE ⟨∑_{i∈I} when c_{i} do P_{i}, d⟩ ⟶ ⟨P_{j}, d⟩ if d ⊢ c_{j}, for j ∈ I

PAR  {⟨P, c⟩ ⟶ ⟨P′, d⟩ \atop ⟨P ∥ Q, c⟩ ⟶ ⟨P′ ∥ Q, d⟩}

LOC

⟨P, c ˙∧ ˙∃_{x}d⟩ ⟶ ⟨Q, c′⟩
⟨local (x, c) in P, d⟩ ⟶ ⟨local (x, c′) in Q, d ˙∧ ˙∃_{x}c′⟩
UNLESS ⟨unless c next P, d⟩ ⟶ ⟨skip, d⟩ if d ⊢ c
REPL  ⟨! P, c⟩ ⟶ ⟨P ∥ next ! P, c⟩
STAR  ⟨⋆ P, c⟩ ⟶ ⟨next^{n}P, c⟩ for some n ≥ 0.
STRUCT {γ_{1} ≡ γ′_{1} γ′_{1} ⟶ γ′_{2} γ′_{2} ≡ γ_{2} \atop γ_{1} ⟶ γ_{2}}

OBS  {⟨P, c⟩ ⟶^{∗} ⟨Q, d⟩ −̸→ \atop P ⟹^{(c,d)} F (Q)}

Table 1: An operational semantics for ntcc. The function F, used in OBS, is given in Definition 2.5

D1 [[tell(c)]] = {d.α | d ⊢ c, α ∈ C^{∞}}
D2 [[∑_{i∈I} when c_{i} do P_{i}]] = \begin{matrix}⋃_{i∈I}\{d.α | d ⊢ c_{i}, d.α ∈ [[P_{i}]]\} \\ ∪ \\ ⋂_{i∈I}\{d.α | d ⊬ c_{i}, d.α ∈ C^{∞}\} \end{matrix}
D3 [[P ∥ Q]] = [[P]] ∩ [[Q]]
D4 [[local x in P]] = {α | there exists α′ ∈ [[P]] s.t. ˙∃_{x}α = ˙∃_{x}α′}
D5 [[next P]] = {d.α | d ∈ C , α ∈ [[P]]}
D6 [[unless c next P]] = \begin{matrix}\{d.α | d ⊢ c, α ∈ C^{∞}\} \\ ∪ \\ \{d.α | d ⊬ c, α ∈ [[P]]\} \end{matrix}
D7 [[! P]] = {α | ∀β ∈ C^{∗}, α′ ∈ C^{∞} s.t. α = β.α′, we have α′ ∈ [[P]]}
D8 [[⋆ P]] = {β.α | β ∈ C^{∗}, α ∈ [[P]]}

Table 2: Denotational semantics of ntcc

P1 tell(c) ⊢ c
P2 \frac{∀i ∈ I P_{i} ⊢ A_{i}}{∑_{i∈I} when c_{i} do P_{i} ⊢ ⋁_{i∈I}(c_{i} ∧ A_{i}) ∨ ⋀_{i∈I} ¬c_{i}}

P3 \frac{P ⊢ A Q ⊢ B}{P ∥ Q ⊢ A ∧ B}

P4 \frac{P ⊢ A}{local x in P ⊢ ∃_{x}A}

P5 \frac{P ⊢ A}{next P ⊢ ∘A}

P6 \frac{P ⊢ A}{unless c next P ⊢ c ∨ ∘A}

P7 \frac{P ⊢ A}{! P ⊢ □A}

P8 \frac{P ⊢ A}{⋆ P ⊢ ♢A}

P9 \frac{P ⊢ A}{P ⊢ B} if A ⇒ B

Table 3: A proof system for proving linear temporal properties of ntcc processes

Recent BRICS Report Series Publications

RS-01-20 Catuscia Palamidessi and Frank D. Valencia. A Temporal Concurrent Constraint Programming Calculus. June 2001. 31 pp.

RS-01-19 Jiří Srba. On the Power of Labels in Transition Systems. June

2001.

RS-01-18 Katalin M. Hangos, Zsolt Tuza, and Anders Yeo. Some Complexity Problems on Single Input Double Output Controllers. 2001. 27 pp.

RS-01-17 Claus Brabrand, Anders Møller, Steffan Olesen, and Michael I. Schwartzbach. Language-Based Caching of Dynamically Generated HTML. May 2001. 18 pp.

RS-01-16 Olivier Danvy, Morten Rhiger, and Kristoffer H. Rose. Normalization by Evaluation with Typed Abstract Syntax. May 2001. 9 pp. To appear in Journal of Functional Programming.

RS-01-15 Luigi Santocanale. A Calculus of Circular Proofs and its Categorical Semantics. May 2001. 30 pp.

RS-01-14 Ulrich Kohlenbach and Paulo B. Oliva. Effective Bounds on Strong Unicity in L_{1}-Approximation. May 2001. 38 pp.

RS-01-13 Federico Crazzolara and Glynn Winskel. Events in Security Protocols. April 2001. 30 pp.

RS-01-12 Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The Abstraction and Instantiation of String-Matching Programs. April 2001.

RS-01-11 Alexandre David and M. Oliver Möller. From HUppaal to Uppaal: A Translation from Hierarchical Timed Automata to Flat Timed Automata. March 2001. 40 pp.

RS-01-10 Daniel Fridlender and Mia Indrika. Do we Need Dependent Types? March 2001. 6 pp. Appears in Journal of Functional Programming, 10(4):409–415, 2000. Superseeds BRICS Report RS-98-38.

RS-01-9 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. Static Validation of Dynamically Generated HTML. February 2001. 18 pp.

RS-01-8 Ulrik Frendrup and Jesper Nyholm Jensen. Checking for Open Bisimilarity in the π-Calculus. February 2001. 61 pp.