BRICS RS-01-48 Nielsen & Valencia: Temporal Concurrent Constraint Programming: Applications and Behavior BRICS

Basic Research in Computer Science

Temporal Concurrent Constraint Programming

Applications and Behavior

Mogens Nielsen Frank D. Valencia

BRICS Report Series RS-01-48 ISSN 0909-0878 December 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Mogens Nielsen & 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/48/

Temporal Concurrent Constraint Programming: Applications and Behavior

Mogens Nielsen  Frank D. Valencia

December, 2001

Abstract

The ntcc calculus is a model of non-deterministic temporal concurrent constraint programming. In this paper we study behavioral notions for this calculus. In the underlying computational model, concurrent constraint processes are executed in discrete time intervals. The behavioral notions studied reflect the reactive interactions between concurrent constraint processes and their environment, as well as internal interactions between individual processes. Relationships between the suggested notions are studied, and they are all proved to be decidable for a substantial fragment of the calculus. Furthermore, the expressive power of this fragment is illustrated by examples.

1 Introduction

Concurrent constraint programming [19] has been studied extensively as a paradigm for specifying and programming reactive systems. One of the main features of ccp is that it is based on a declarative as well as operational computational model.

The fundamental primitive of a constraint is a partial information on values of variables (e.g. x + y > 5). The state of a computation (also called a store) is simply a set of constraints, and during a computation, a process may modify the state by telling information. Also, a process may condition its activity by asking for certain information to be entailed by the present store - operationally blocking its activity until other processes provide the requested information (if ever). In this way concurrent processes may communicate via the common store of constraints. Processes in ccp are built using the basic primitives of telling and asking constraints, and the operators of parallel composition, hiding and recursion.

The temporal ccp computational model introduced in [20] is an extension aimed at specifying timed systems following the paradigms of Synchronous Languages ([2]). Time is conceptually divided into discrete intervals (or time units). In a particular time interval, a ccp process receives a stimulus (i.e. a constraint) from the environment, it executes with this stimulus as the initial store, and when it reaches its resting point, it responds to the environment with the resulting store. Also the resting point determines a residual process, which is then executed in the next time interval.

This temporal ccp model is inherently deterministic. In [17] a nondeterministic version of the calculus was introduced, adding e.g. (nondeterministic) guarded choice and unbounded-finite delay as new operators in the language of processes. The extension was argued to be consistent with the declarative flavor of ccp, i.e. to free the programmer from over-specifying a deterministic solution, when a non-deterministic simple solution is more appropriate (following the arguments behind Dijkstra’s language of guarded commands). Furthermore, it was argued that a very important benefit of allowing the specification of non-deterministic 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 introduce and study various notions of behavior for the ntcc calculus: the input-output and the language equivalence and their congruences, all motivated operationally and/or logically. The notions are related, and they are all proved to be decidable for a substantial fragment of the calculus. The decidability for the complete calculus is left open.

Furthermore, we illustrate the expressive power of our fragment of ntcc by modeling constructs such as cells and some applications involving the programming of RCX^{TM} controllers, and a version of a Predator/Prey (Pursuit) game.

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 parameterized 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 [24]^{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 is a countable set of variables and S is the set of logical symbols ∧, ∨, ⇒, ¬, ∃, true and false which denote logical conjunction, disjunction, implication, negation, existential quantification and the always true and false predicates, respectively. Constraints, denoted by c, d, … are first-order formulae over L. We say that c entails d in Δ, written c ⊢ d, if the formula c ⇒ d holds in all models of Δ. We shall require ⊢ to be decidable. We say that c is equivalent to d, written c ≈ d, iff c ⊢ d and d ⊢ c. We define the (relevant) free-variables of c as fv(c) = {x ∈ V | ∃_{x}c ≉ c} (e.g., fv(x = x ∧ y > 1) = {y}).

Henceforth, C is a set of constraints modulo ≈ in (Σ, Δ). The set C is closed wrt conjunction and existential quantification and it represents the constraints under consideration in the underlying constraint system.

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

2.2 Process 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.

The only move or action of process tell(c) is to add 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 non-deterministically choose one of the P_{j} (j ∈ I) whose corresponding constraint c_{j} is entailed by the store. The chosen alternative, if any, precludes the others. If no choice is possible then the summation is precluded. We use ∑_{i∈I} P_{i} as an abbreviation for the “blind-choice” process ∑_{i∈I} when (true) do P_{i}. We use skip as an abbreviation of the empty summation and “+” for binary summations.

Process P ∥ Q represents the parallel composition of P and Q. In one time unit (or interval) P and Q operate concurrently, “communicating” via the common store. We use ∏_{i∈I} P_{i}, where I is finite, to denote the parallel composition of all P_{i}. Process local x in P behaves like P, except that all the information on x produced by P can only be seen by P.

The process next P represents the activation of P in the next time interval. Hence, a move of next P is a unit-delay of P. 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 ([15]): ! P represents P ∥ next P ∥ next^{2}P ∥ …, i.e. unboundely many copies of P but one at a time. The replication operator is the only way of defining infinite behavior through the time intervals.

Our process language is essentially the language of the calculus ntcc from [17], but in order to unify and to simplify the presentation of our technical results, we have omitted the unbounded finite delay operator. As we shall clarify, it is not clear to what extent all our results generalize to the full language of ntcc.

2.3 An Operational Semantics.

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, true) in P.

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 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}), fv(local x in P) = fv(P) − {x}. The bound variables and the other cases are defined analogously.

Definition 2.2 (Structural Congruence) Let ≡ be the smallest congruence 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.

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, PAR and LOC are standard [22]. 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. 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 terminating 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.3 (Future Function) The partial function F : Proc ⇀ Proc 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 & if P = ∑_{i∈I} when c_{i} do P_{i} \end{matrix}

Remark: Function F does not need to be total since whenever we apply F to a process P (Rule OBS in Table 1), all replications operators in P occur within a next construction.

2.3.1 Interpreting Processes Runs.

Henceforward we use α, α′ to represent elements of C^{ω}. Let us consider the sequence of observable transitions

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

This sequence can be interpreted as a interaction between the system P and an environment. At the time unit i, the environment provides a stimulus c_{i} and P_{i} produces c′_{i} as response. We then regard (α, α′) as a reactive observation of P. If α = c_{1}.c_{2}.c_{3}…. and α′ = c′_{1}.c′_{2}.c′_{3} …, we represent the above interaction as P ⟹^{(α,α′)}^{ω}. Given P we shall refer to the set of all its reactive observations as the input-output behavior of P.

Alternatively, if α = true^{ω}, we can interpret the run as an interaction among the parallel components in P without the influence of an external environment (i.e., each component is part of the environment of the others). In this case α is called the empty input sequence and α′ is regarded as a timed observation of such an interaction in P. We shall refer to the set of all timed observations of a process P as the language of P.

In section 4 we study in detail input-output behavior and language of processes.

Notation 1 Throughout the paper we use the following notation on transitions:

1) P ⟶ Q  iff for some c, ⟨P, c⟩ ⟶ ⟨Q, c′⟩ .
2) P ⟹ Q iff P ⟶^{∗} P′ −̸→ and Q = F (P′).
3) P ⟹^{c} Q iff P ⟹^{(true,c)} Q.
4) P ⟹^{α}^{ω} iff P ⟹^{(true^{ω},α)}^{ω}.

2.4 A Logic of ntcc Processes

A relatively complete formal system for proving whether or not an ntcc process satisfies a linear-temporal property was introduced in [17]. In this section we summarize these results.

We extend the ccp notion of strongest postcondition of a process P ([6]), sp(P), to our setting. In ntcc, sp(P) denotes the set of all infinite sequences that P can possibly output. More precisely,

Definition 2.4 Given P its strongest postcondition is defined as

sp(P) = {α′ | for some α : P ⟹^{(α,α′)}^{ω}}.

2.4.1 Temporal Logic.

We define a linear temporal logic for expressing properties of ntcc processes. The formulae A, B, ... ∈ A are defined by the grammar

A := c | A ˙⇒ A | ˙¬ A | ˙∃_{x} A | ∘A | □A | ♢A,

where c denotes an arbitrary constraint. The intended meaning of the other symbols is the following: ˙⇒, ˙¬ and ˙∃ represent linear-temporal logic implication, negation and existential quantification. These symbols are not to be confused with the symbols ⇒, ¬ and ∃ in the underlying constraint system. The symbols ∘, □, and ♢ denote the temporal operators next, always and sometime. We use A ˙∨ B as an abbreviation of ˙¬ A ˙⇒ B and A ˙∧ B as an abbreviation of ˙¬( ˙¬ A ˙∨ ˙¬ B).

The semantics of the logic is given in Definition 2.5. The standard interpretation structures of linear temporal logic are infinite sequences of states [14]. In the case of ntcc, states are represented by constraints, thus we consider as interpretations the elements of C^{ω}.

Definition 2.5 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} implies ⟨α, i⟩ ⊧ A_{2}
⟨α, i⟩ ⊧ ∘A  iff ⟨α, i + 1⟩ ⊧ A
⟨α, i⟩ ⊧ □A  iff for all j ≥ i ⟨α, j⟩ ⊧ A
⟨α, i⟩ ⊧ ♢A  iff there is j ≥ i s.t. ⟨α, j⟩ ⊧ A
⟨α, i⟩ ⊧ ˙∃_{x} A  iff there is α′ ∈ C^{ω} s.t. ∃_{x}α = ∃_{x}α′ and ⟨α′, i⟩ ⊧ A,

where ∃_{x}α represents the sequence obtained by applying ∃_{x} to each constraint in α. Notation α(i) denotes the i-th element in α.

We define [[A]] to be the collection of all models of A, i.e,

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

We shall say that P satisfies A iff every infinite sequence that P can possibly output satisfies the property expressed by A, i.e. sp(P) ⊆ [[A]]. A relatively complete proof system for assertions P ⊢ A, whose intended meaning is that P satisfies A, can be found in [17]. We shall write P ⊢ A if there is a derivation of P ⊢ A in this system.

3 Applications

Let us assume that the underlying constraint system is FD[max] which has {succ, prd, +, ×, =, <, >, 0, 1, …} as signature and the set of sentences valid in arithmetic modulo max as theory. Henceforth, we designate Dom as the set {0, 1, ...., max − 1} and use v and w to range over its elements.

It will be convenient to specify our applications using defining equations of the form q(x_{1}, …, x_{m}) =^{def} P_{q}. In ntcc we encode definitions of this sort provided that 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 the response time of the system bounded: we do not want P_{q} to make unboundely many recursive calls within a time interval. The intended behavior of a call of q with arguments t_{1}, …, t_{m}, written ⌜q(t_{1}, …, t_{m})⌝, when t_{i} = v_{i} in the current store, is that of P_{q}[v_{1}/x_{1}, …, v_{m}/x_{m}] ^{2}. The encoding of a process definition requires the use of replication and, if the definition is recursive or it has at least one parameter, also hiding (see [18] for the exact details of the encoding).

3.1 Cell Example

Cells provide a basis for the specification and analysis of mutable and persistent data structures as shown for the π calculus. We assume that the signature is extended with an unary predicate symbol change. A mutable cell x: (v) can be viewed as a structure x which has a current value v and can, in the future, be assigned a new value.

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

Definition x: (z) represents a cell x whose value is z and it will be the same in the next time interval unless it is to be changed next (i.e., change(x)). Definition g_{exch}(x, y) represents an exchange operation between the contents of x and y. If v is x’s current value then g(v) and v will be the next values of x and y respectively. In the case of functions that always return the same value (i.e. constants), we 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 assignment of v to a cell x, written x := v, can then be encoded as local y in ⌜v_{exch}(x, y)⌝ where the local variable y is used as dummy variable (cell).

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 3.1 ⌜x:(v)⌝ ⊢ (A ˙∧ ˙¬ change(x)) ˙⇒∘A.

2[v_{1}/x_{1}, …, v_{m}/x_{m}] is the operation of (syntactical) replacement of every occurrence of the x_{i} by v_{i}

3.2 The Zigzagging Example

An RCX is a programmable, controller-based LEGO^{\begin{matrix}r \\ ◯ \end{matrix}} brick used to create autonomous robotic devices ([13]). Zigzagging [7] 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. We use cells a_{1} and a_{2} to “look back” one and two time units, respectively. We use three distinct constants f,r,l ∈ Dom − {0} and extend the signature with the predicate symbols forward,right,left.

GoF  =^{def} ⌜f_{exch}(a_{1} , a_{2} )⌝ ∥ tell(forward)
GoR  =^{def} ⌜r_{exch}(a_{1} , a_{2} )⌝ ∥ tell(right)
GoL  =^{def} ⌜l_{exch}(a_{1} , a_{2} )⌝ ∥ tell(left)
Zigzag  =^{def} ! ( \begin{matrix}& when & (a_{1} ≠ f) & do ⌜GoF ⌝ \\ + & when & (a_{2} ≠ r) & do ⌜GoR⌝ \\ + & when & (a_{2} ≠ l) & do ⌜GoL⌝ ) \end{matrix}

GoZigzag =^{def} ⌜a_{1}:(0)⌝ ∥ ⌜a_{2}:(0)⌝ ∥ ⌜Zigzag⌝.

Initially cells a_{1} and a_{2} contain neither f, r nor l. After a choice is made according to (1), (2) and (3), it is recorded in a_{1} and the previous one moved to a_{2} . The property below states that the robot indeed goes right and left infinitely often.

Proposition 3.2 ⌜GoZigzag⌝ ⊢ □(♢right ˙∧ ♢left).

3.3 Multi-Agent Systems: The Pursuit Game Example

The Predator/Prey (or Pursuit) game [1] has been studied using a wide variety of approaches [11] and it has many different instantiations that can be used to illustrate different multi-agent scenarios [25]. As the Zigzagging example, instances of the Predator/Prey game have been modeled using autonomous robots [16]. Here we model a simple instance of this game.

The predators and prey move around in a discrete, grid-like toroidal world with square spaces; they can move off one end of the board and come back on the other end. Predators and prey move simultaneously. They can move vertically and horizontally in any direction. In order to simulate fast but not very precise predators and a slower but more maneuverable prey we assume that predators move two squares in straight line while the prey moves just one.

The goal of the predators is to “capture” the prey. A capture position occurs when the prey moves into a position which is within the threesquares line of a predator current move; i.e. if for some of the predators, the prey current position is either the predator current position, the predator previous position, or the square between these two positions. This simulates the prey deadly moving through the line of attack of a predator.

For simplicity, we assume that initially the predators are in the same row immediately next to each other, while the prey is in front of a predator (i.e, in the same column, above this predator) one square from it. The prey’s maneuver to try to escape is to move in an unpredictable zigzagging around the world. The strategy of the predators is to cooperate to catch the prey. Whenever one of the predators is in front of the prey it declares itself as the leader of the attack and the other becomes its support. Therefore depending on the moves of the prey the role of leader can be alternated between the predators. The leader moves towards the prey, i.e. if it sees the prey above it then it moves up, if it sees the prey below it then it moves down, and so on. The support predator moves in the direction the leader moves, thus making sure it is always next to leader.

In order to model this example we extend the signature with the predicates symbols right_{i}, left_{i}, up_{i}, down_{i} for i ∈ {0, 1}. For simplicity we assume there are only two predators Pred_{0} and Pred_{1}. We use the cells x_{i}, y_{i} and cells x, y for representing the current positions of predator i and the prey, respectively, in a max × max matrix (with max = 2^{k} for some k > 1) representing the world. We also use the primed version of these cells to keep track of corresponding previous positions and cell l to remember which predator is the current leader. We can now formulate the capture condition. Predator i captures the prey with a horizontal move iff

\begin{aligned}x′_{i} = x = x_{i} ∧ ( & (y_{i} = y′_{i} − 2 ∧ (y = y′_{i} ∨ y = y′_{i} − 1 ∨ y = y′_{i} − 2))∨ \\ & (y_{i} = y′_{i} + 2 ∧ (y = y′_{i} ∨ y = y′_{i} + 1 ∨ y = y′_{i} + 2)) ) \end{aligned}

and with a vertical move iff

\begin{aligned}y′_{i} = y = y_{i} ∧ ( & (x_{i} = x′_{i} − 2 ∧ (x = x′_{i} ∨ x = x′_{i} − 1 ∨ x = x′_{i} − 2))∨ \\ & (x_{i} = x′_{i} + 2 ∧ (x = x′_{i} ∨ x = x′_{i} + 1 ∨ x = x′_{i} + 2)) ). \end{aligned}

We define capture_{i} as the conjunction of the two previous constraints.

The process below models the behavior of the prey. The preys moves as in the Zigzagging example. Furthermore, the values of cells x, y and x′, y′ are updated according to the zigzag move (e.g., if it goes right the value of x is increased and x′ takes x’s previous value).

Prey =^{def} ⌜GoZigzag⌝ ∥ !( when forward do ⌜succ_{exch}(y, y′)⌝
+ when right do ⌜succ_{exch}(x, x′)⌝
+ when left  do ⌜prd_{exch}(x, x′)⌝).

The process Pred_{i} with i ∈ {0, 1} models the behavior of predator i. The operator ⊕ denotes binary summation.

Pred_{i} =^{def} ! ( when x_{i} = x  do ( ⌜l := i⌝ ∥ ⌜Pursuit_{i}⌝)
+ when l = i ∧ x_{i⊕1} ≠ x do ⌜Pursuit_{i}⌝
+ when l = i ⊕ 1 ∧ x_{i} ≠ x do ⌜Support_{i}⌝ ).

Thus whenever Pred_{i} is in front of the prey (i.e. x_{i} = x ) it declares itself as the leader by assigning i to the cell l. Then it runs process Pursuit_{i} defined below and keep doing it until the other predator Pred_{i⊕1} declares itself the leader. If the other process is the leader then Pred_{i} runs process Support_{i} defined below.

Process Pursuit_{i}, whenever the prey is above of corresponding predator (y_{i} < y ∧ x_{i} = x), tells the other predator that the move is to go up and increases by two the contents of y_{i} while keeping in cell y′_{i} the previous value. The other cases which correspond to going left, right and down can be described similarly.

Pursuit_{i} =^{def} when (y_{i} < y ∧ x_{i} = x) do
(⌜succ_{exch}^{2}(y_{i}, y′_{i})⌝ ∥ tell(up_{i}))
+ when (y_{i} > y ∧ x_{i} = x) do
(⌜prd_{exch}^{2}(y_{i}, y′_{i})⌝ ∥ tell(down_{i}))
+ when (x_{i} < x ∧ y_{i} = y) do
(⌜succ_{exch}^{2}(x_{i}, x′_{i})⌝ ∥ tell(right_{i}))
+ when (x_{i} > x ∧ y_{i} = y) do
(⌜prd_{exch}^{2}(x_{i}, x′_{i})⌝ ∥ tell(left_{i})).

The process Support_{i} is defined according to the move decision of the leader. Hence, if the leader moves up (e.g. up_{i⊕1}) then the support predator moves up as well. The other cases are similar.

Support_{i} =^{def} when up_{i⊕1}  do
(⌜succ_{exch}^{2}(y_{i}, y′_{i})⌝ ∥ tell(up_{i}))
+ when down_{i⊕1}  do
(⌜prd_{exch}^{2}(y_{i}, y′_{i})⌝ ∥ tell(down_{i}))
+ when right_{i⊕1}  do
(⌜succ_{exch}^{2}(x_{i}, x′_{i})⌝ ∥ tell(right_{i}))
+ when left_{i⊕1}  do
(⌜prd_{exch}^{2}(x_{i}, x′_{i})⌝ ∥ tell(left_{i})).

We assume that initially Pred_{0} is the leader and that it is in the first row in the middle column . The other predator is next to it in the same row. The prey is just above Pred_{0} . The process Init below specifies these conditions. Let p = max/2.

\begin{aligned}Init & =^{def} & ∏_{i∈0,1}(⌜x_{i} : (p + i)⌝ ∥ ⌜y_{i} : (0)⌝ ∥ ⌜x′_{i} : (p + i)⌝ ∥ ⌜y′_{i} : (0))⌝ \\ & & ∥ ⌜x : (p)⌝ ∥ ⌜y : (1)⌝ ∥ ⌜x′ : (p)⌝ ∥ ⌜y′_{i} : (1)⌝ ∥ ⌜l : 0⌝. \end{aligned}

The proposition states that the predators eventually capture the prey under our initial conditions.

Proposition 3.3 Init ∥ Pred_{0} ∥ Pred_{1} ∥ Prey ⊢ ♢(capture_{0} ˙∨ capture_{1}).

It is worth noticing that in the case of one single predator, say Pred_{0} , the prey may sometimes escape under the same initial conditions, i.e. Init ∥ Pred_{0} ∥ Prey ⊬ ♢capture_{0}. A similar situation occurs if the predators were not allowed to alternate the leader role.

4 Behavioral Equivalence

In this section we introduce notions of equality for our calculus. We wish to distinguish between the observable behavior of two processes if the distinction can somehow be detected by a process interacting with them. A natural observation we can make of a process is its input-output behavior, i.e. its infinite sequences of input-output constraints.

Furthermore, in Section 2.3 we mentioned that we can model the behavior of processes in which each component is part of the environment of the others. Thus the only “external” input is the empty one, i.e., true^{ω}. Therefore, another interesting observation to make is the set of outputs on the empty sequence, which we shall call the language of a process.

We now introduce the observables and the corresponding equivalences we are interested in.

Definition 4.1 Given P, the input-output behavior of P and the language of P are defined as

io(P) = {(α, α′) | P ⟹^{(α,α′)}^{ω}} and L(P) = {α | P ⟹^{(true^{ω},α)}^{ω}},

respectively. For all P and Q, we define P ∼_{io} Q iff io(P) = io(Q) and P ∼_{L} Q iff L(P) = L(Q).

Unfortunately, the equivalences ∼_{io} and ∼_{L} are not preserved by process constructions, i.e. they are not congruences.

Example. Assume that a, b, c are non-equivalent constraints such that c ⊢ b ⊢ a. Let

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

+

when true do (tell(a) ∥ when (b) do tell(c))

and let R = when a do tell(b). We leave it to the reader to verify that we can distinguish P from Q if we make R to interact with them, i.e. although P ∼_{io} Q (and thus P ∼_{L} Q) we have R ∥ P ≁_{L} R ∥ Q (and thus R ∥ P ≁_{io} R ∥ Q).

Therefore, we ought to consider the largest congruences included in ∼_{io} and ∼_{L}, respectively. More precisely,

Definition 4.2 For all P and Q, P ≈_{io} Q iff for every process context C[.], C[P] ∼_{io} C[Q], and P ≈_{L} Q iff for every process context C[.], C[P] ∼_{L} C[Q].

As usual a process context C[.] is a process term with a single hole such that placing a process in the hole yields a well-formed process. The relations ≈_{io} and ≈_{L} are then our first proper notion of equality for the calculus.

It is important to point out that the mismatch between ≈_{io} and ∼_{io} arises from allowing nondeterminism. In fact, the following result follows from ([18], Theorem 3).

Definition 4.3 A process P is said to be deterministic iff for every construct of the form ∑_{i∈I} when c_{i} do P_{i} in P, the c_{i}’s are mutually exclusive.

Proposition 4.4 For all deterministic processes P and Q, P ≈_{io} Q iff P ∼_{io} Q.

The reason for using the name “deterministic process” is because given an input, the output of a process of this kind is always the same independently of the execution order of its parallel component [22].

Let us now see the relation between the different equivalences for arbitrary processes. The relation ≡ denotes structural congruence (Definition 2.2). For technical purposes we consider the finite prefixes of the language of a process. Let L^{i}(P) = {α^{i}| α ∈ L(P)} where α^{i} is the i − th prefix of α and define P ∼_{L}^{i} Q iff L^{i}(P) = L^{i}(Q). Obviously, relation ∼_{L} is weaker than ∼_{io}, however, the corresponding congruences coincide.

Theorem 4.5 ≡ ⊂ ≈_{io} = ≈_{L} ⊂ ∼_{io} ⊂ ∼_{L} = ⋂_{n∈ω} ∼_{L}^{n} .

Proof: The proper inclusions are left for the reader to verify. The final equality follows from the fact that our calculus is finitely branching. Here we prove ≈_{io} = ≈_{L}. The case ≈_{io} ⊆ ≈_{L} is trivial. We want to prove that P ≈_{L} Q implies P ≈_{io} Q. Suppose that P ≈_{L} Q but P ≉_{io} Q. Then there must exist a context C[.] s.t C[P] ≁_{io} C[Q]. Consider the case io(C[P]) ⊅ io(C[Q]). Take an α = c_{1}.c_{2} … such that (α, α′) ∈ io(C[Q]) but (α, α′) ∉ io(C[P]). There must then be a prefix of α′ which differs from all other prefixes of sequences α′′ s.t. (α, α′′) ∈ io(C[P]). Suppose that this is the n−th prefix. One can verify that for the context

C′[.] = C[.] ∥ ∏_{i≤n} next^{i} tell(c_{i}),

L(C′[P]) ≠ L(C′[Q]). This contradicts our assumption P ≈_{L} Q. The case io(C[Q]) ⊅ io([P]) is symmetric. Therefore P ≉_{L} Q as required.

We next investigate the type of contexts C[.] in ntcc needed to verify P ≈_{io} Q and focus on relation ≈_{L} as it is equivalent to ≈_{io}. The proposition below allows us to approximate the behavior of !P.

Proposition 4.6 For all P, Q, n ≥ 0: Q ∥!P ∼_{L}^{n} Q ∥ ∏_{i≤n} next^{i}P.

The next proposition states that it is sufficient to consider parallel contexts.

Lemma 4.7 P ≈_{L} Q iff for all R, R ∥ P ∼_{L} R ∥ Q.

Proof: Suppose that for all R, P ∥ R ∼_{L} Q ∥ R. We can prove that for all contexts C[.], C[P] ∥ R ∼_{L} C[Q] ∥ R for an arbitrary R. Here we outline the proof of the next and replication context cases. The other cases are trivial. For the next case we have next P ∥ R ⟹^{(c,c′)} P ∥ R′ iff

R ⟹^{(c,c′)} R′. Similarly, next Q ∥ R ⟹^{(c,c′)} Q ∥ R′ iff R ⟹^{(c,c′)} R′.

Thus, the result follows immediately from the initial assumption. As for the replication case, from the Prop. 4.6 for all n, R ∥!P ∼_{L}^{n} R ∥ ∏_{i≤n} next^{i}P and R ∥!Q ∼_{L}^{n} R ∥ ∏_{i≤n} next^{i}Q. With the help of Theorem 4.5 ( ∼_{L} = ⋂_{n∈ω} ∼_{L}^{n} ) we get that R ∥!P ∼_{L} R ∥!Q if for all n ≥ 0, R ∥!P ∼_{L}^{n} R ∥!Q. The result now follows from the next and parallel cases.

Moreover, if C (i.e., the underlying set of constraints) is finite we have the notion of a universal context, i.e., a context that can distinguish any two processes iff they are not language (or input-output) congruent. Intuitively, the idea is to provide a single process that can simulate all possible interactions that a process can have with others.

Consider R ∥ P with P and R as in Example 4. By telling information, process P provides information which influences the evolution of R, i.e., the constraint a. Similarly, R influences the evolution of P by providing the constraint b. Thus asking a and then telling b is one possible interaction a process can have with P while telling a and then asking b is a possible interaction a process can have with R. In general, interactions can be represented as strictly increasing and alternating sequences of ask and tell operations (see [22]).

In the following we write c′ ≺ c iff c ⊢ c′ and c ⊬ c′. The assertion S ⊆_{fin} S′ holds iff S is a finite subset of S′. Given S ⊆_{fin} C, ic(S) denotes the set of strictly increasing sequences in S^{∗}, i.e., ic(S) = {c_{1} … c_{n} ∈ S^{∗} | c_{1} ≺ c_{2} ≺ … ≺ c_{n}}. Furthermore, we extend the underlying constraint system signature Σ to a signature Σ′ with unary predicates tr_{β} for each β ∈ C^{∗}. These predicates are “private” in the sense that they are only allowed to occur in the process contexts U^{S}[.] defined below.

Definition 4.8 The distinguishing context wrt S ⊆_{fin} C, written U^{S}[.], is defined as

! ( ∑_{β∈ic(S)} tell(tr_{β}) ∥ T_{β}) ∥ [.]

where for each β ∈ S^{∗}, T_{c.β} = tell(c) ∥ W_{β} and W_{c.β} = when c do T_{β} with T_{ϵ} = W_{ϵ} = skip.

Theorem 4.9 Suppose that C is finite. Then P ≈_{L} Q iff U^{C}[P] ∼_{L} U^{C}[Q].

Proof: The “only if” direction is trivial. Here we outline the proof of the “if” direction. From Lemma 4.7 it is sufficient to prove that U^{C}[P] ∼_{L} U^{C}[Q] implies R ∥ P ∼_{L} R ∥ Q for all R. Suppose that R is such that R ∥ P ≁_{L} R ∥ Q. We want to prove that U^{C}[P] ≁_{L} U^{C}[Q].

Consider the case L(R ∥ P) ⊄ L(R ∥ Q). Take an α = d_{0}.d_{1} … such that α ∈ L(R ∥ P) and α ∉ L(R ∥ Q). Furthermore, suppose that

R_{0} ∥ P_{0} ⟹^{d_{0}} R_{1} ∥ P_{1} ⟹^{d_{1}} … with P = P_{0} and R = R_{0}.

We can represent the internal reduction of each R_{i} ∥ P_{i} which gives us d_{i} and R_{i+1} ∥ P_{i+1}, as a sequence of internal transitions (or interactions) ⟨R_{i}^{0} ∥ P_{0}^{0}, c_{i}^{0}⟩ ⟶^{∗} ⟨R_{i}^{n} ∥ P_{i}^{n}, c_{i}^{n}⟩ −̸→, with R_{i} = R_{i}^{0}, P_{i} = P_{i}^{0}, c_{i}^{0} = true, P_{i+1} = F (P_{i}^{n}), R_{i+1} = F (R_{i}^{n}) and d_{i} = c_{i}^{n}, satisfying

⟨P_{i}^{0}, a_{i}^{0}⟩ ⟶^{∗} ⟨P_{i}^{1}, a_{i}^{1}⟩
⟨P_{i}^{1}, a_{i}^{1} ∧ b_{i}^{1}⟩ ⟶^{∗} ⟨P_{i}^{2}, a_{i}^{2}⟩
⋮

⟨P_{i}^{j}, a_{i}^{j} ∧ b_{i}^{j}⟩ ⟶^{∗} ⟨P_{i}^{j+1}, a_{i}^{j+1}⟩

⟨R_{i}^{0}, b_{i}^{0}⟩ ⟶^{∗} ⟨R_{i}^{1}, b_{i}^{1}⟩
⟨R_{i}^{1}, a_{i}^{1} ∧ b_{i}^{1}⟩ ⟶^{∗} ⟨R_{i}^{2}, b_{i}^{2}⟩
⋮
⟨R_{i}^{j}, a_{i}^{j} ∧ b_{i}^{j}⟩ ⟶^{∗} ⟨R_{i}^{j+1}, b_{i}^{j+1}⟩

where for each j ≤ n, c_{i}^{j} = a_{i}^{j} ∧ b_{i}^{j}. Let σ_{i} = b_{i}^{1}.c_{i}^{1} ….b_{i}^{n}.c_{i}^{n}. It is easy to see that ⟨T_{σ_{i}} ∥ P_{i}^{0}, c_{i}^{0}⟩ ⟶^{∗} ⟨T_{ϵ} ∥ P_{i}^{n}, c_{i}^{n}⟩ −̸→ (see Definition 4.8). Note that sequence σ_{i} is increasing, thus by removing all constraint repetitions we get a strictly increasing sequence. Let β_{i} be such a sequence. One can verify that T_{β_{i}} can “mimic” R_{i}^{0} interacting with P_{i}^{0}. More precisely, ⟨T_{β_{i}} ∥ P_{i}^{0}, c_{i}^{0}⟩ ⟶^{∗} ⟨T_{ϵ} ∥ P_{i}^{n}, c_{i}^{n}⟩ −̸→. This implies:

⟨!( ∑_{β∈ic(C)} tell(tr_{β}) ∥ T_{β}) ∥ P_{i}^{0}, true⟩ ⟶^{∗} ⟨T_{ϵ} ∥ P_{i}^{n}, d_{i} ∧ tr_{β_{i}}⟩ −̸→ (1)

By observing that last(β_{i}) = d_{i} (where last(β_{i}) denotes the last element of β_{i}), one can show that R_{i} can mimic T_{β_{i}} interacting with any P′ provided that the result is d_{i}. More precisely,:

For all P′, if ⟨T_{β_{i}} ∥ P′, true⟩ ⟶^{∗} ⟨T_{ϵ} ∥ P′′, d_{i}⟩ −̸→
where P′ ⟶^{∗} P′′,
then ⟨R_{i}^{0} ∥ P′, true⟩ ⟶^{∗} ⟨R_{i}^{n} ∥ P′′, d_{i}⟩ −̸→  (2)

¿From (1), α′ = (d_{0} ∧ tr_{β_{0}}).(d_{1} ∧ tr_{β_{1}}) … ∈ L(!(∑_{β∈ic(C)} tell(tr_{β}) ∥ T_{β}) ∥ P) where β_{i} corresponds to the internal T_{β_{i}} selected to “mimic” R_{i}. We want to show α′ is not in L(!(∑_{β∈ic(C)} tell(tr_{β}) ∥ T_{β}) ∥ Q). Suppose it is. Then at time i, T_{β_{i}} must be selected in the execution of !(∑_{β∈ic(C)} tell(tr_{β}) ∥ T_{β}) ∥ Q that outputs α′. By using Property (2) (and observing our restriction on the use of tr_{β_{i}} predicates), one can inductively construct a sequence R_{0} ∥ Q_{0} ⟹^{d_{0}} R_{1} ∥ Q_{1} ⟹^{d_{1}} … with Q = Q_{0}, R = R_{0}. We conclude that α ∈ L(R ∥ Q) thus contradicting the assumption about α.

The case of L(R ∥ Q) ⊄ L(R ∥ P) is symmetric.

Therefore context U^{C}[.] is the universal distinguishing context, provided that C is finite, as it can distinguish any two processes P and Q which are not language congruent.

It is interesting that even if C is not finite, we can construct specialized distinguishing contexts for arbitrary processes as stated in the following result. The idea is to choose a suitable finite set of constraints.

Definition 4.10 Let Λ ⊂_{fin} Proc. Define C(Λ) ⊆_{fin} C as the set whose elements are true, false and all constraints resulting from the closure under conjunction and existential quantification of the constraints occurring in Λ’s processes.

Theorem 4.11 For all P, Q ∈ Λ ⊂_{fin} Proc, P ≈_{L} Q iff U^{C(Λ)}[P] ∼_{L} U^{C(Λ)}[Q].

Proof: The proof is the same as that of Theorem 4.9 except for the role of β_{i} which is now played by a sequence \overline{β_{i}}, defined below, that depends only on constraints in Λ’s processes. More precisely, let consq(c, S) = \{d ∈ S | c ⊢ d\}. Define \overline{e} as the conjunction of all constraints in consq(e, C(Λ)) and let \overline{s} be the sequence that results from replacing each constraint e in a sequence s with \overline{e}. By definition every constraint in C(Λ) which can be inferred from e, can also be inferred from \overline{e} ∈ C(Λ). We proceed exactly as in the proof of Theorem 4.9 until properties (1) and (2), which we re-state as:

⟨!( ∑_{β∈ic(C(Λ))} tell(tr_{β}) ∥ T_{β}) ∥ P_{i}^{0}, true⟩ ⟶^{∗} ⟨T_{ϵ} ∥ P_{i}^{n}, \overline{d_{i}} ∧ tr\overline{β_{i}}⟩ −̸→

(3)

and

For all P′ ∈ Λ, if ⟨T\overline{β_{i}} ∥ P′, true⟩ ⟶^{∗} ⟨T_{ϵ} ∥ P′′, \overline{d_{i}}⟩ −̸→
where P′ ⟶^{∗} P′′,
then ⟨R_{i}^{0} ∥ P′, true⟩ ⟶^{∗} ⟨R_{i}^{n} ∥ P′′, d_{i}⟩ −̸→ (4)

We then proceed as in the proof of Theorem 4.9; getting a contradiction out of (3) and (4).

Therefore U^{C(Λ)} is an universal context for Λ’s processes. The ability of constructing distinguishing contexts for arbitrary processes is important as it can be used for proving decidability results for ≈_{io} (note that P ≈_{L} Q iff U^{C({P,Q})}[P] ∼_{L} U^{C({P,Q})}[Q]). It turns out that ∼_{L} is decidable for a significant fragment of the calculus. The languages of these processes can be recognized by automata over infinite sequences, more precisely Büchi Automata ([3]). We will elaborate on this in the next section.

4.1 Decidability and Characterization of Processes Languages

In this section we will characterize processes languages in terms of ωregular languages (i.e., the languages accepted by Büchi automata). Recall that Büchi automata are ordinary nondeterministic finite-state automata equipped with an acceptance condition that is appropriate for ω-sequences: an ω-sequence is accepted if the automaton can read it from left to right while visiting a sequence of states in which some final state occurs infinitely often. This condition is called Büchi acceptance ([3]).

We aim at proving decidability of the relation ∼_{L} for a fragment of ntcc which we call restricted-nondeterministic.

Definition 4.12 A process P is said to be restricted-nondeterministic iff for all local x in Q in P, for every construct of the form ∑_{i∈I} when c_{i} do Q_{i} in Q, the c_{i}’s are mutually exclusive. We use Proc^{r} to denote the set of all restricted-nondeterministic processes.

This fragment allows non-deterministic process (summations) out of the scope of local variables. In fact, all application examples in this paper (Section 3) belong to this fragment. Notice that each local x in P ∈ Proc^{r} is deterministic in the sense of Definition 4.3.

We shall show that the languages of restricted-nondeterministic processes are ω-regular. We will also show that given a P ∈ Proc^{r} we can construct a Büchi automaton recognizing the language of P. Then using the fact that language equivalence for Büchi automata is decidable [23], we conclude that ∼_{L} is decidable for restricted-nondeterministic processes and thus so are ≈_{L} and ≈_{io} (see Theorem 4.11).

To illustrate the problem in trying to use finite-state machines for representing processes let us consider the following example.

Example. Let Q = !!P with P = ∑_{j∈J} tell(c_{j}). We have the following transition sequence (on input true^{ω}):

Q ⟹^{d_{1}} Q ∥!P ⟹^{d_{2}} Q ∥!P ∥!P ⟹^{d_{3}} … ⟹^{d_{n}} Q ∥ ∏_{n}!P ⟹^{d_{n+1}} …

This example illustrates that in a transition system where states are the elements of Proc it is possible to have infinite paths where all states are different up to structural congruence (i.e., there can be an infinite set of derivatives). Moreover, notice that in this particular example, the process at time i can output everything the process at time i − 1 can, but not necessarily the other way round. This situation arises from the nondeterminism specified by P.

Nevertheless, we will show that after some time units the states can be identified up to ≈_{L}. More precisely, the property we would like to have is that there exists t such that for all k ≥ t, ∏_{k}!P ≈_{L} ∏_{k+1}!P. In the above example for any k ≥ |J| we have ∏_{k}!P ≈_{L} ∏_{k+1}!P thus validating the property. Unfortunately, the property does not hold for processes out of Proc^{r}. Let us define an arbitrary-delay operation δP which delays P arbitrarily:

δP =^{def} P + δP.

The encoding in our calculus of the recursive definition of δP requires hiding over non-mutually exclusive summations (see [18]) thus it is out of Proc^{r}. Assume that P = tell(c). Then two copies of δP can output c at two (arbitrary) points of time while a single copy cannot. In general one can prove that for any k > 1, L(∏_{k} δP) ⊂ L(∏_{k+1} δP), thus invalidating the property.

The following property is needed in the proof of Lemma 4.15 which implies the property described above. It relates the language of processes with the language of processes arising at intermediate steps of the internal computations.

Proposition 4.13 α ∈ L(P) iff there are Q and c such that ⟨P, true⟩ ⟶^{∗}

⟨Q, c⟩ and Q ∥ tell(c) ⟹^{α}^{ω}.

We now introduce the notion of multiplicity of a process.

Definition 4.14 Let m : Proc^{r} → Nat. The multiplicity of P, m(P) is defined as

m(skip) = 0

m(tell(c)) = 1

m(∑_{i∈I} when c_{i} do P_{i}) = ∑_{i∈I} m(P_{i})

m(P ∥ Q) = max{m(P), m(Q)}

m(local x in P) = m(nextP) = m(unless c next P) = m(!P) = m(P).

The value m(P) is aimed to be the number of copies of P, after which, further copies are redundant. This is stated in the following lemma which is the key for decidability of ∼_{L}.

Lemma 4.15 Let P ∈ Proc^{r}. For all k > m(P), ∏_{k−1} P ≈_{L} ∏_{k} P.

Proof: The proof proceeds by induction on the structure of P ∈ Proc^{r}. Here we show some cases. Suppose k > m(P).

• Case P = P_{1} ∥ P_{2}. From Theorem 4.5 we get ∏_{k}(P_{1} ∥ P_{2}) ≈_{L} ∏_{k} P_{1} ∥ ∏_{k} P_{2}. Note that k > m(P) ≥ m(P_{1}) and k > m(P) ≥ m(P_{2}). Therefore, from the hypothesis ∏_{k} P_{1} ∥ ∏_{k} P_{2} ≈_{L} ∏_{k−1} P_{1} ∥ ∏_{k−1} P_{2} ≈_{L} ∏_{k−1}(P_{1} ∥ P_{2}) as required.

• Case P = next Q. We have ∏_{k} next Q ≈_{L} next ∏_{k} Q from Theorem 4.5. From m(P) = m(Q), the hypothesis and Theorem 4.5, we get next ∏_{k} Q ≈_{L} next ∏_{k−1} Q ≈_{L} ∏_{k−1} next Q.

• Case P = !Q. We verify that ∏_{k}! Q ≈_{L}! ∏_{k} Q. From m(P) = m(Q) and hypothesis we verify that ! ∏_{k} Q ≈_{L}! ∏_{k−1} Q ≈_{L} ∏_{k−1}! Q.

• Case P = ∑_{u∈I} when c_{u} do P_{u}. ¿From Lemma 4.7 we know that it is enough to consider parallel contexts. Let E an arbitrary process and suppose that α = c.α′ ∈ L(E ∥ ∏_{k} P) (1). We want to show that α ∈ L(E ∥ ∏_{k−1} P). From (1) we know that there exists sequence of internal transitions t = ⟨E ∥ ∏_{k} P, true⟩ ⟶^{∗} γ_{1} ⟶^{∗}, ...., ⟶^{∗} γ_{n} ⟶^{∗} ⟨R, c⟩ −̸→ with α′ ∈ L(F (R)) which contains only the initial and final configuration, and those configurations γ_{1}, ...., γ_{n} in which a reduction from a P takes place, if any. By monotonicity of the store if t contains a configuration with store c s.t. ⟨P, c⟩ ⟶ then since a reduction of each P must eventually take place n = k ( I ) otherwise n = 0 (II ).

(I). Suppose n = k. Define E_{0} = E, P_{0} = skip. For 0 < j ≤ n, each γ_{j} can be defined as ⟨E_{j} ∥ P_{j} ∥ ∏_{n−j} P, c_{j}⟩, where

⟨E_{j−1} ∥ P_{j−1}, c_{j−1}⟩ ⟶^{∗} ⟨E_{j}, c′_{j}⟩ for some c′_{j} s.t. ⟨P, c′_{j}⟩ ⟶ ⟨P_{j}, c_{j}⟩ (a reduction from one of the k P′s). Notice k > m(P) = Σ_{Q:P ⟶Q}m(Q), so from the pigeon-hole principle there must be a process P′, P ⟶ P′ with r > m(P′) configurations γ_{j_{1}}, … γ_{j_{r}} such that each corresponding P_{j_{1}}, …, P_{j_{r}} is P′. Let γ_{i} be the first among these configurations and let P_{i} be the process in such a configuration, i.e., E_{i} ∥ P′ ∥ ∏_{k−i} P. ¿From Proposition 4.13, we have α ∈ L(P_{i} ∥ tell(c_{i})). As r copies of P′ are eventually triggered, one can verify that α ∈ L(E_{i} ∥ ∏_{r} P′ ∥ ∏_{k−(i+r−1)} P ∥ tell(c_{i})). Since P′ is a subprocess of P, from the hypothesis α ∈ L(Q_{i} ∥ tell(c_{i})) with Q_{i} = E_{i} ∥ ∏_{r−1} P′ ∥ ∏_{k−(i+r−1)} P. One can then construct the sequence

⟨E ∥ ∏_{(k−1)} P, true⟩ ⟶^{∗} ⟨E_{i} ∥ P′ ∥ ∏_{(k−1)−i} P, c_{i}⟩
⟶ ⟨E_{i} ∥ ∏_{2} P′ ∥ ∏_{(k−1)−(i+1)} P, c_{i}⟩
⋮
⟶ ⟨E_{i} ∥ ∏_{r−1} P′ ∥ ∏_{(k−1)−(i+r−2)} P, c_{i}⟩
= ⟨Q_{i}, c_{i}⟩ .

From Proposition 4.13, α ∈ L(E ∥ ∏_{(k−1)} P) as required.

(II). Suppose n = 0. Then R = E′ ∥ ∏_{k} P for some E′ s.t. ⟨E, true⟩ ⟶^{∗} ⟨E′, c⟩ −̸→. Trivially ⟨E ∥ ∏_{k−1} P, true⟩ ⟶ ⟨R′, c⟩ −̸→ with R′ = E′ ∥ ∏_{k−1} P. From the definition of F (.), F (P) ≡ skip, thus F (R) = F (E′) ∥ ∏_{k} F (P) ≡ F (E′) ≡ F (R′) = F (E′) ∥ ∏_{k−1} F (P). Hence F (R) ≈_{L} F (R′) by Theorem 4.5, thus α′ ∈ F (R′). We then conclude α ∈ L(E ∥ ∏_{k−1} P).

• Case P = local x in Q. In this case P is a deterministic process. It is easy to verify that if P is a deterministic process then P ≈_{L} ∏_{k} P for any k, thus validating the property.

The lemma below states that every language transition sequence over Proc^{r} ultimately contains two language congruent processes.

Lemma 4.16 Let P_{0} ⟹^{c_{1}} P_{1} ⟹^{c_{2}} … be an arbitrary language transition sequence where P_{0} ∈ Proc^{r}. Then there are two processes P_{m}, P_{n} with m < n such that P_{n} ≈_{L} P_{m}.

Proof: Let P_{0} ⟹^{c_{1}} P_{1} ⟹^{c_{2}} … be an arbitrary language transition sequence where P_{0} ∈ Proc^{r}. It is sufficient to construct a sequence

P′_{0} ⟹^{c_{1}}≈_{L} P′_{1} ⟹^{c_{2}}≈_{L} … with P_{i} ≈_{L} P′_{i} for every i ≥ 0 and two

processes P′_{m}, P′_{n} with m < n satisfying P′_{n} ≡ P′_{m} (Definition 2.2). We sketch such a construction next.

Every process P can be rewritten via ≡ as ∏_{i∈I}!R_{i} ∥ E where E is a replication-free processes. Hence P_{0} ⟹^{c_{0}} P_{1} ⟹^{c_{1}} … can be rewritten as:

∏_{i∈I_{0}}!R_{i} ∥ E_{0} ⟹^{c_{0}} ∏_{i∈I_{1}}!R_{i} ∥ E_{1} ⟹^{c_{1}} …  (5)

where each E_{u} is a non-replicated processes. It is easy to verify that I_{0} ⊆ I_{1} ⊆ … since new replicated processes can move up to the top level. Assume that k is such that satisfies ∏_{i∈I_{k}}!R_{i} ≈_{L} ∏_{i∈I_{j}}!R_{i} for any j > k. Such a k is guaranteed to exist from Lemma 4.15. Thus the sequence in (5) is point-wise ≈_{L}-equivalent to the sequence

∏_{i∈I_{0}}!R_{i} ∥ E_{0} ⟹^{c_{1}} … ∏_{i∈I_{k}}!R_{i} ∥ E_{k} ⟹^{c_{k}}≈_{L} ∏_{i∈I_{k}}!R_{i} ∥ E_{k+1} ⟹^{c_{k+1}}≈_{L} …

(6)

Now notice that both the E_{j}’s (j > k) and ∏_{i∈I_{k}} R_{i} can have replicated processes !R which can move up to the top level. However, ∏_{i∈I_{k}}!R_{i} ∥ !R ≈_{L} ∏_{i∈I_{k}}!R_{i} from our assumption about k. Therefore we can replace such replications with skip. Given Q let us use Q̂ to denote the processes resulting from replacing each replicated process in Q with skip. We can then verify that the sequence

∏_{i∈I_{0}}!R_{i} ∥ E_{0} ⟹^{c_{1}} … ∏_{i∈I_{k}}!R̂_{i} ∥ Ê_{k} ⟹^{c_{k}}≈_{L} ∏_{i∈I_{k}}!R̂_{i} ∥ Ê_{k+1} ⟹^{c_{k+1}}≈_{L} …

(7)

is point-wise ≈_{L}-equivalent to the one in (6). We claim the following:

Claim 4.17 For some n > k there exists a m, with k ≤ m < n such that Ê_{m} ≡ Ê_{n}

Thus, for m and n in the above claim, it follows ∏_{i∈I_{k}}!R̂_{i} ∥ Ê_{m} ≡ ∏_{i∈I_{k}}!R̂_{i} ∥ Ê_{n} thus proving the Lemma. Below we prove this claim.

Define the next-depth of a process Q, written nd(Q), as the maximum number of nesting of next operations in Q. Let D(Q, i) = {Q′ | Q ⟹^{i} Q′}, i.e. the set of all processes which Q can possibly evolve to in i times units. Trivially, if Q is replication-free then for all u > nd(Q), D(Q, u) = {skip} (2).

Let R = ∏_{i∈I_{k}} R̂_{i}, Rr = ∏_{i∈I_{k}}!R̂_{i} and E = Ê_{k}. Without loss of generality assume that nd(R) > nd(E) (by adding next-guarded skips we can always augment the next-depth of a process). Let h = nd(R). At time k the processes E and R are the ones to be executed in parallel with Rr. At time k + 1, a process in D(E, 1), a process in D(R, 1), and R which is a process in D(R, 0) are the ones to be executed with Rr. In general, at time k + n there are n + 2 processes E′ ∈ D(E, n), Q_{n} ∈ D(R, n), Q_{n−1} ∈ D(R, n − 1), …, Q_{0} ∈ D(R, 0) to be executed with Rr. If n ≥ h, however, we know from (2) that at each following time unit it is enough to consider the process in the (finite) sets D(R, 0), …, D(R, h) since D(R, u) = {skip} for u > h. The are w = |D(R, 0)|×…×|D(R, h)| many choices of the h process in these sets. Thus after h + w time units at least one choice must be repeated.

By using the Lemma 4.16 we can prove that the set of derivatives of P, which we define as S(P) = {Q | P ⟹^{c_{1}} … ⟹^{c_{n}} Q}, modulo ∼_{L} is finite.

Lemma 4.18 For every P ∈ Proc^{r}, S(P)/ ∼_{L} is finite.

Proof: Here we outline the proof. Consider the finitely-branching transition system graph of P with labeled transitions ⟹^{c} modulo ∼_{L}. One can verify that if the transition graph were infinite then it would have to have an infinite path P ∼_{L} Q_{0} ⟹^{c_{0}}∼_{L} Q_{1} ⟹^{c_{1}}∼_{L} Q_{2} …, where all the Q_{i}’s are different (modulo ∼_{L}). But this would imply that there is a sequence P = P_{0} ⟹^{c_{0}} P_{1} ⟹^{c_{1}} P_{2} … (with P_{i} ∼_{L} Q_{i} for all i ≥ 0) where all the P_{i}’s are different modulo ≈_{L} which is impossible according to Lemma 4.16 (Recall that from Theorem 4.5, ≈_{L}⊂∼_{L} ).

Given a restricted-nondeterministic process P, Lemma 4.18 above allows us to define a Büchi automaton A_{P/∼_{L}} which accepts L(P). The set of states is S(P)/ ∼_{L} in Lemma 4.18. All states are accepting. The start state is P. There is transition from Q to Q′ labeled by c iff Q ⟹^{c} Q′. It is easy to verify such an automaton accepts L(P).

Theorem 4.19 For every P ∈ Proc^{r}, L(P) is an ω-regular language.

The definition of A_{P/∼_{L}} above does not give us an effective way of constructing the automaton. In Algorithm 1 we describe a method which given P ∈ Proc^{r} constructs a Büchi automaton A_{P} accepting L(P).

First we need the following definitions: given Q and R let r(R, Q) be the number of occurrences of R in Q at the top level. Let Q ↓_{R} the process that results from replacing with skip each non-top-level occurrence of !R in Q if r(!R, Q) > m(!R) (See Definition 4.14). Let Q ↑_{R} be the process that results from replacing with skip, r(!R, Q) − m(!R) top-level occurrence of !R in Q in some fixed order. Suppose that we enumerate all the replicated process in Q in some fixed order R_{1}, …, R_{n}. Let us define Q ↓ as the process Q ↓_{R_{1}} … ↓_{R_{n}} and Q ↑ as Q ↑_{R_{1}} … ↑_{R_{n}}. Recall that ≡ denotes the structural congruence (Definition 2.2).

Remark 4.20 For each permutation π on {1, …, m}, Q ↑_{R_{1}} … ↑_{R_{m}}≡ Q ↑_{R_{π(1)}} … ↑_{R_{π(m)}} and Q ↓_{R_{1}} … ↓_{R_{m}}≡ Q ↓_{R_{π(1)}} … ↓_{R_{π(m)}}

The proposition below follows from Lemma 4.15.

Proposition 4.21 For all Q, Q ↓ ≈_{L} Q ↑ ≈_{L} Q.

Algorithm 1 Constructing the automaton A_{P}

1. Start by creating the initial state and label it with (P ↓↑).

2. Choose a state p′ labeled by P′ from the current transition graph and a reduction P′ ⟹^{c} Q. The choice should satisfy that there is not already an edge labeled with c from p′ to a state q with a label structurally congruent to (Q ↓↑). If such a choice is not possible we stop.

3. If there is already a state q labeled with a process (structurally equivalent to) (Q ↓↑) then create an edge from p′ to it with label c. Otherwise create a new state q with label (Q ↓↑) and an edge from p′ to it with label c.

4. Go to (2).

This algorithm assumes decidability of ≡ which basically follows from the decidability of the π-calculus structural congruence without the replication axiom [15]. The termination of Algorithm 1 is based on the proof of Lemma 4.16. Basically, each path in the transition graph constructed by this method is constructed as in the proof of the lemma; if the method did not terminate then the construction would violate the claim in the proof. The partial correctness is easy to verify.

Theorem 4.22 For all P ∈ Proc^{r}, one can effectively construct a Büchi automaton A_{P} accepting the set L(P).

Therefore ∼_{L} is decidable for restricted-nondeterministic processes (Definition 4.1). Moreover, ≈_{L} = ≈_{io} is also decidable for these processes as we need to consider only one context to check whether two processes are language congruent (Theorem 4.11).

Corollary 4.23 Relations ∼_{L}, ≈_{L} and ≈_{io} are decidable for restricted nondeterministic processes.

5 Automata for the Strongest-Postcondition and Input-Output Behavior

In the previous sections we introduced the notion of the language of a process and described how to construct automata for the language of restricted-nondeterministic processes. In this section we use such notions and constructions and relate them to the strongest postcondition and input-output behavior of processes.

Henceforth we assume that the underlying set of constraints C is the set of all constraints in F D[max] (Section 3). The following results, however, can be extended to C’s defined over finite-domain constraint systems or, of course, to finite C’s. Notice that C is infinite since we have infinitely many variables

Given P, we want to find a finite set which contains the “relevant” inputs for a processes P. We shall prove in Lemma 5.1 that if x does not occur in the free-variables of P, fv(P), then the reductions of P on c[x] can be identified with those of P on ∃_{x}c[x]. We can then say that if a constraint has all its free variables in fv(P) is “relevant” for P, otherwise is “irrelevant”.

The next lemma states that indeed we can abstract away from the variables not occurring free in the program.

Lemma 5.1 For all x ∉ fv(P), P ⟹^{(c[x],d[x])} Q if and only if P ⟹^{(∃_{x}c,∃_{x}d)}

Q

Proof: We first prove the following property: For all P, Q and x ∉ fv(P), ⟨P, c[x]⟩ ⟶ ⟨Q, d[x]⟩ iff ⟨P, ∃_{x}c⟩ ⟶ ⟨Q, ∃_{x}d⟩ (1).

Both directions proceeed by induction on (depth of the) inference. Here we only show the “only if” direction as the other case is simlar. Suppose that x ∉ fv(P). Consider the final step of the inference of ⟨P, c[x]⟩ ⟶ ⟨Q, d[x]⟩. These are the key cases.

• Suppose that it is inferred by using rule TELL where P = tell(e), Q = skip and d = c ∧ e. Since x ∉ fv(e), ∃_{x}c ∧ e = ∃_{x}(c ∧ e). Then, by using TELL ⟨P, ∃_{x}c⟩ ⟶ ⟨Q, ∃_{x}d⟩.

• Suppose that it is inferred by using rule ASK where P = ∑_{i∈I} when (c_{i}) doP_{i}, Q = P_{j} for j ∈ J s.t. c ⊢ c_{j}, and d = c. Since x ∉ fv(c_{j}), one can verify that c ⊢ c_{j} iff ∃_{x}c ⊢ c_{j}. Thus, by using ASK ⟨P, ∃_{x}c⟩ ⟶ ⟨Q, ∃_{x}d⟩.

• Suppose that it is inferred by using rule PAR P = P_{1} ∥ P_{2} and Q = P′_{1} ∥ P_{2} with ⟨P_{1}, c⟩ ⟶ ⟨P′_{1}, d⟩ inferred by a shorter inference. We have x ∉ fv(P_{1}) thus by appeal to induction we get ⟨P_{1}, ∃_{x}c⟩ ⟶ ⟨P′_{1}, ∃_{x}d⟩. Then, by using PAR we obtain ⟨P, ∃_{x}c⟩ ⟶ ⟨Q, ∃_{x}d⟩ as required.

• Suppose that it is inferred by using rule LOC where for some variable ν P = local (ν, e) in P′, Q = local (ν, e′) in Q′, d = c ∧ ∃_{ν}e′ with ⟨P′, e ∧ ∃_{ν}c⟩ ⟶ ⟨Q, e′⟩ inferred by a shorter inference. First, suppose that ν is x. In this case by using the shorther inference in the premise of LOC and simple logic manipulations we have:

⟨P′, e ∧ ∃_{x}∃_{x}c⟩ = ⟨P′, e ∧ ∃_{x}c⟩ ⟶ ⟨Q′, e′⟩
⟨local (x, e) in P′, ∃_{x}c ⟩ ⟶ ⟨local (x, e′) in Q′, ∃_{x}c ∧ ∃_{x}e′⟩ = ⟨local (x, e′) in Q′, ∃_{x}(c ∧ ∃_{x}e′)⟩

as wanted. Now suppose that v is not x. In this case x ∉ fv(P′) and x ∉ fv(e). So we can α-convert P by replacing ν with x without risk of capture. By using STRUCT after LOC we get the desired result.

It follows from (1) above and a simple induction on n that for x ∉ fv(P), ⟨P, c[x]⟩ ⟶^{n} ⟨Q, d[x]⟩ iff ⟨P, ∃_{x}c⟩ ⟶^{n} ⟨Q, ∃_{x}d⟩ which proves the Lemma. □

In what follows δ_{V} c where V is set of variables, denotes the constraint resulting from the existential quantification of each free variable in c not in V (e.g. δ_{{x,y}}(x + w = z) = ∃_{w}∃_{z}(x + w = z)). We extend this notation to other structures; δ_{V} t, δ_{V} (α) and δ_{V} (S) denotes the elementwise application of δ_{P} to a tuple t, sequence α and set S, respectively. For simplicity, we will write δ_{P_{1},...,P_{n}} instead of δ_{fv(P_{1})∪...∪fv(P_{n})}. Thus, each constraint δ_{P_{1},...,P_{n}}c is of the form ∃_{x_{1}...x_{m}}c where none of the x_{i}’s a free-variable of some P_{j}. The following corollary follows inmediately from Lemma 5.1.

Corollary 5.2 P ⟹^{(c,d)} Q if and only if P ⟹^{δ_{P} (c,d)} Q

Notice that δ_{P} (C) = {c ∈ C | fv(c) ⊆ fv(P) }, i.e., the set of what we called “relevant” constraints for P. Moreover, there are only finitely constraints in δ_{P} (C) since the set of free-variables of a P is finite and C is defined over the finite-domain constraint system F D[max].

Proposition 5.3 The set δ_{P} (C) is finite.

Therefore from Corollary 5.2 it follows that the finite set δ_{P} (C)^{ω} is the contains all the relevant inputs for P.

Let us define I_{S} = ! (∑_{c∈S} tell(c)). Notice that in R = P ∥ I_{S}, process I_{S} can provide P with all inputs in S^{ω}. More precisely, the set of outputs of P on inputs in S^{ω} is the same as the set of outputs of R on the empty input true^{ω}, i.e. the language of R. Hence in P ∥ I_{δ_{P}} process I_{δ_{P}} can provide all sequences of relevant input constraints for P. Now, recall that the strongest postcondition of P, sp(P) (Definition 2.4) is the set all sequences that P can possibly output on some input, i.e, the set of outputs of P on inputs in C. This leads to the next result wich can be proven with the help of Corollary 5.2.

Lemma 5.4 For any P, L(P ∥ I_{δ_{P}}) = δ_{P} (sp(P)) ⊆ sp(P).

In Section 2.4 we define the assertion P ⊧ B, where B is temporal formula, to hold iff the strongest-postcondition of P, sp(P) ⊆ [[B]], where ⊆ [[B]] is the set of models of B). We confine ourselves to assertions P ⊧ B in which B refers only to variables of the program P, i.e., fv(B) ⊆ fv(P). The following theorem relates P ⊧ B to the language of P ∥ I_{δ_{P}}.

Theorem 5.5 For all P and temporal formula B with fv(B) ⊆ fv(P)

P ⊧ B iff L(P ∥ O_{I_{P}} ⊆ [[B]]

Proof: The “only if” direction follows from Lemma 5.4 Suppose that L(P ∥ I_{δ_{P}}) ⊆ [[B]]. From Lemma 5.4 δ_{P} α ⊧ B for all α ∈ sp(P). Whence, for all α ∈ sp(P), α ⊧ B since each assertion δ_{P} α ⊧ B holds independently of the variables outside of fv(P). □

We now proceed to relate input-output equivalence ∼_{io} (Definition 4.1) with language equivalence of certain kind of Büchi automata derived from the previous constructions. Let P ∈ Proc^{r} and S ⊆_{fin} C. We show next how to construct a Büchi automaton A_{P}^{S} over the alphabet (S ×C)^{ω} for the input-ouput behavior of P on inputs in S^{ω}. The automaton is constructed from the automaton A_{P ∥I_{S}} which recognizes the language of P ∥ I_{S}. Notice that states of A_{P ∥I_{S}} are labelled by processes of the form Q ∥ I_{S} for some Q. The construction is described in Algorithm 2.

Remark 5.6 Consider an arbitrary infinite path from the starting state in the transition graph of A_{P}^{S} whose arcs are labelled succesively (c_{1}, c′_{1}).(c_{2}, c′_{2}) . . .. The sequence (c_{1}, c′_{1}).(c_{2}, c′_{2}) … is accepted by A_{P}^{S} since c′_{1}.c′_{2}…. is accepted by A_{P ∥I_{S}} and the two paths go through the same states. It should also be clear that (c_{1}.c_{2}…. , c′_{1}.c′_{2} …) ∈ io(P).

Algorithm 2 Constructing the automaton A_{P}^{S}

1. Start by making the start state, the accepting states, and the set of states of A_{P ∥I_{S}} to be the corresponding ones for A_{P}^{S}.

2. Take a transition in A_{P ∥I_{S}} labelled by d from a state q labeled with Q ∥ I_{S} to a state r labelled R ∥ I_{S}.

3. Then create a new transition from q labelled with Q to r labelled with R. Make (c, d) the label of the transition, where c ∈ S, if

Q ⟹^{(c,d)} R′ with R′ ≈_{L} R.

4. Add the transition to the current transition graph of A_{P}^{S}.

5. Repeat (2-4) until no new transition can be added.

¿From the construction of A_{P}^{S} and Corollary 5.2 we can prove the following result relating the input-output behaviour of a process P and the language of A_{P}^{δ_{P} (C)}.

Proposition 5.7 For every restricted-nondeterministic process P

(c_{1}.c_{2}…. , c′_{1}.c′_{2} …) ∈ io(P) iff δ_{P} ((c_{1}, c′_{1}).(c_{2}.c′_{2}) …) ∈ L(A_{P}^{δ_{P} (C)}).

We can also reduce the question of input-output equivalence between processes to language equivalence in Büchi automata as stated in the theorem below.

Theorem 5.8 For all P, Q ∈ Proc^{r}, P ∼_{io} Q iff L(A_{P}^{δ_{P,Q}C}) = L(A_{Q}^{δ_{P,Q}C})

Proof: The “only if” direction is trivial. Suppose that L(A_{P}^{δ_{P,Q}C}) = L(A_{Q}^{δ_{P,Q}C}) (1). Consider the case io(P) ⊆ io(Q). Take an arbitrary (α, α′) ∈ io(P) with α = c_{1}.c_{2}…. and α′ = c′_{1}.c′_{2}. . . .. From the construction of A_{P}^{δ_{P,Q}C} (and with the help of Corollary 5.2) we can verify that δ_{P,Q}((c_{1}.c′_{1}).(c_{2}.c′_{2})….) ∈ L(A_{P}^{δ_{P,Q}C}). Hence from our assumption δ_{P,Q}((c_{1}.c′_{1}).(c_{2}.c′_{2})….) ∈ L(A_{Q}^{δ_{P,Q}C}). This implies (Remark 5.6) that δ_{P,Q}(α, α′) ∈ Q. Notice that the constraints δ_{P,Q}c_{i} and δ_{P,Q}c′_{i} are of the form ∃_{x_{1}...x_{n}}c_{i} and ∃_{x_{1}...x_{n}}c′_{i}, resp., where none of the x_{i}’s is in fv(Q). By using Corollary 5.2 one verifies that (α, α′) ∈ Q. The case io(Q) ⊆ io(P) is symmetric. □

We can also use the automaton A_{P}^{C[P]} as a simple input-output execution model for P. We conclude this section by defining such a model of execution.

Input-Output Execution of A_{P}^{C[P]}: The execution starts at time unit 0 in the initial state of the automaton. At time i the automaton is in some state p. Given an input c_{i} from the environment the automaton nondeterministically selects a transition labeled by (δ_{fv(P)}c_{i}, δ_{fv(P)}d_{i}) from p to some q. The constraint d′_{i} = c_{i}∧δ_{fv(P)}d_{i} is the output to the environment at time i. The automaton then moves to state q and repeat this process (at time i + 1). We then say that on input α = c_{1}.c_{2} … the automaton can produce an output α′ = d′_{1}.d′_{2}. . . .. Let us denote by io(A_{P}^{io}) the set of all (α, α′) such that on input α, A_{P}^{io} can produce α′.

The correspondence between the execution of processes and the execution of its automaton is stated by the following theorem.

Theorem 5.9 For all P ∈ Proc^{r}, io(P) = io(A_{P}^{io}).

Proof: Here we prove io(P) ⊆ io(A_{P}^{io}) as the other direction is trivial. Suppose that (α, α′) ∈ io(P), with α = c_{1}.c_{2} … and α = c′_{1}.c_{2}. . . .. By monotonicity of the store each c′_{i} = c_{i} ∧ d_{i} with d_{i} s.t. fv(d_{i}) ⊆ fv(P). From proposition 5.7 we know that δ_{P} ((c_{1}, c′_{1}), (c_{2}, c′_{2}), …) ∈ L(A_{P}^{io}). On each each c_{i} the automaton can output c_{i} ∧ δ_{P} c′_{i}. Notice that each δ_{P} c′_{i} must then have the form (∃_{x_{1},...,x_{m}}c_{i}) ∧ d_{i}. So, c_{i} ∧ δ_{P} c′_{i} = c_{i} ∧ d_{i} = c′_{i}. Consequentely, on α, the automaton A_{P}^{io} can output α′. □.

6 Related Work and Concluding Remarks

6.0.1 Related Work.

The work most closely related to our paper is that of tcc ([20]). Our proposal is a strict extension of tcc, in the sense that tcc can be encoded in (the deterministic fragment of) ntcc, while the vice-versa is not possible because tcc does not have constructs to express non-determinism. The input-output behavior of tcc has been studied in [20]. In tcc the input-output equivalence and congruence coincide as only deterministic processes are allowed. Therefore, there is no need for the study of universal or distinguishing contexts as in the ntcc case. In [20] it was shown that tcc processes can be compiled into (deterministic) finite-state automata. Moreover such a compilation is compositional. This result relies on determinacy of tcc processes. As shown in this paper, in ntcc the non-deterministic constructs are the ones which present technical difficulties to deal with when trying to represent them as finite-state machines. Other interesting extensions of tcc have been proposed in [9, 10, 21]. None of these, however, consider non-determinism.

The tccp calculus ([5]) 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. 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. The notion of time is also different; in tccp each time unit is identified with the time needed to ask and tell information to the store. As for the constructs, unlike ntcc, tccp provides for arbitrary recursion. 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.

A proof system for reasoning about the correctness of tccp processes was recently introduced in [4]. The underlying temporal logic in [4] can be used for describing input-output behavior while the one in [17] for ntcc can only be used for the strongest-postcondition. As such the temporal logic of ntcc processes is less expressive than that one underlying the proof system of tccp, but it is also semantically simpler and defined as the standard linear-temporal logic of [14]. This may come in handy when using the Consequence Rule present in the proof systems of both [4] and [17].

6.0.2 Concluding Remarks.

In this paper we introduced and studied different notions of equality for ntcc. We showed that the languages of restricted-nondeterministic processes can be characterized in terms of ω-languages. Furthermore, we described how to construct Büchi automata accepting the language of restricted-nondeterministic processes. This allowed us to prove decidability of language-equivalence for these processes. By proving the existence of distinguishing contexts, and that the input-output and language congruences coincide, we also proved decidability for these relations. We have also used the automata constructions for characterizing the strongest postcondition and input-output behavior of processes. This gives us some decidability results for these notions and also a simple execution model for restricted-nondeterministic processes.

On the practical side we show applications examples illustrating the expressiveness of (the restricted-nondeterministic fragment of) ntcc.

Our current research includes the study of the decidability of ≈_{L} for arbitrary ntcc processes as it remains an open question. The plan for future research includes the extension of ntcc to a probabilistic model following ideas in [12] and [8]. 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 owe much to Catuscia Palamidessi, with whom we have worked on ntcc, for her insight into ccp issues. We would also like to thank Maurizio Gabbrielli, Paulo Oliva, Pawel Sobocinski, Jesus Almansa for helpful comments on different aspects of ntcc.

References

[1] M. Benda, V. Jagannathan, and R. Dodhiawala. On optimal cooperation of knowledge sources - an empirical investigation. Technical Report BCS-G2010-28, Boeing Advanced Technology Center, 1986.

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

[3] 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.

[4] F. de Boer, M. Gabbrielli, and M. Chiara. A temporal logic for reasoning about timed concurrent constraint programs. In TIME 01. IEEE Press, 2001.

[5] F. de Boer, M. Gabbrielli, and M. C. Meo. A timed concurrent constraint language. Information and Computation, 1999. To appear.

[6] 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.

[7] J. Fredslund. The assumption architecture. Progress Report, Department of Computer Science, University of Aarhus, November 1999.

[8] V. Gupta, R. Jagadeesan, and P. Panangaden. Stochastic processes as concurrent constraint programs. In Symposium on Principles of Programming Languages, pages 189–202, 1999.

[9] V. Gupta, R. Jagadeesan, and V. 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, 26–29 August 1996.

[10] V. Gupta, R. Jagadeesan, and V. Saraswat. Probabilistic concurrent constraint programming. In CONCUR ’97: Concurrency Theory, 8th International Conference, volume 1243 of LNCS, pages 243–257, 1–4 July 1997.

[11] T. Haynes and S. Sen. The evolution of multiagent coordination strategies. Adaptive Behavior, 1997.

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

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

[14] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, 1991.

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

[16] S. Nolfi and D. Floreano. Coevolving predator and prey robots: Do “arms races” arise in artificial evolution? Artificial Life, 4(4):311– 335, 1998.

[17] C. Palamidessi and F. Valencia. A temporal concurrent constraint programming calculus. In Proc. of the Seventh International Conference on Principles and Practice of Constraint Programming, 26 November 2001.

[18] C. Palamidessi and F. Valencia. A temporal constraint programming calculus. Technical Report RS-01-20, BRICS, University of Aarhus, June 2001. availabe via http://www.brics.dk/∼fvalenci/publications.html.

[19] V. Saraswat. Concurrent Constraint Programming. The MIT Press, Cambridge, MA, 1993.

[20] V. Saraswat, R. Jagadeesan, and V. Gupta. Foundations of timed concurrent constraint programming. In Proc. of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 71–80, 4–7 July 1994.

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

[22] V. Saraswat, M. Rinard, and P. Panangaden. The semantic foundations of concurrent constraint programming. In POPL ’91. Proceedings of the eighteenth annual ACM symposium on Principles of programming languages, pages 333–352, 21–23 January 1991.

[23] A. Sistla, M. Vardi, and P. Wolper. The complementation problem for buchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.

[24] G. 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.

[25] P. Stone and M. Veloso. Multiagent systems: A survey from a machine learning perspective. Autonomous Robots, 8:345–383, 2000.

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⟩
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 upper part defines the internal transitions while the lower part defines the observable transitions. The function F, used in OBS, is given in Definition 2.3

Recent BRICS Report Series Publications

RS-01-48 Mogens Nielsen and Frank D. Valencia. Temporal Concurrent Constraint Programming: Applications and Behavior. December 2001. 36 pp.

RS-01-47 Jesper Buus Nielsen. Non-Committing Encryption is Too Easy in the Random Oracle Model. December 2001. 20 pp.

RS-01-46 Lars Kristiansen. The Implicit Computational Complexity of Imperative Programming Languages. November 2001. 46 pp.

RS-01-45 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.

RS-01-44 M. Oliver Möller, Harald Rueß, and Maria Sorea. Predicate Abstraction for Dense Real-Time Systems. November 2001. 27 pp.

RS-01-43 Ivan B. Damgård and Jesper Buus Nielsen. From Known-Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.

RS-01-42 Zoltán Ésik and Werner Kuich. Rationally Additive Semirings. November 2001. 11 pp.

RS-01-41 Ivan B. Damgård and Jesper Buus Nielsen. Perfect Hiding and Perfect Binding Universally Composable Commitment Schemes with Constant Expansion Factor. October 2001. 43 pp.

RS-01-40 Daniel Damian and Olivier Danvy. CPS Transformation of Flow Information, Part II: Administrative Reductions. October 2001. 9 pp.

RS-01-39 Olivier Danvy and Mayer Goldberg. There and Back Again. October 2001. 14 pp.

RS-01-38 Zoltán Ésik. Free De Morgan Bisemigroups and Bisemilattices. October 2001. 13 pp.

RS-01-37 Ronald Cramer and Victor Shoup. Universal Hash Proofs and a Paradigm for Adaptive Chosen Ciphertext Secure Public-Key Encryption. October 2001. 34 pp.

RS-01-36 Gerth Stølting Brodal, Rolf Fagerberg, and Riko Jacob. Cache Oblivious Search Trees via Binary Trees of Small Height. October 2001. 20 pp.