BRICS RS-01-26 Frendrup & Jensen: A Complete Axiomatization of Simulation for Regular CCS Expressions BRICS

Basic Research in Computer Science

A Complete Axiomatization of Simulation for Regular CCS Expressions

Ulrik Frendrup Jesper Nyholm Jensen BRICS Report Series RS-01-26 ISSN 0909-0878 June 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Ulrik Frendrup & Jesper Nyholm Jensen.

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/26/

A Complete Axiomatization of Simulation for Regular CCS Expressions

Ulrik Frendrup & Jesper Nyholm Jensen

BRICS^{∗}

Aalborg University, Department of Computer Science Fredrik Bajers Vej 7E 9220 Aalborg Ø, Denmark

Email: frendrup@worldonline.dk, nyholm@gaztricjuice.dk

June, 2001

Abstract

This paper gives axiomatizations of strong and weak simulation over regular CCS expressions. The proof of completeness of the axiomatization of strong simulation is inspired by Milner’s proof of completeness of his axiomatization for strong equivalence over regular CCS expressions. Soundness and completeness of the axiomatization for weak simulation is easily deduced from the corresponding result for the axiomatization of strong simulation over regular CCS expressions.

1 Introduction

The main purpose of this paper is to give a sound and complete axiomatization of the notion of strong simulation over regular CCS expressions, i.e. agent descriptions in the regular fragment of Milner’s CCS[6] that may contain free variables. The axiomatization we give is an extension of the axiomatization of strong equivalence over regular CCS expressions presented by Milner in [4]. Soundness and completeness of our axiomatization of the notion of strong simulation is proved using techniques similar to those developed by Milner in [5] and [4]. The key axiom in the axiomatization we propose is the rule E ⊑ E + F that intuitively states that any expression E can be simulated by one that can exhibit at least the behavior of E. We also study the notion of weak simulation, i.e. a version of simulation that abstracts from internal steps in computations, over the regular fragment of CCS. We show that unlike observational equivalence[6], weak simulation is a precongruence for regular CCS. Finally, we present a sound and complete axiomatization of weak simulation over regular CCS expressions. The key axiom is one allowing for the elimination of τ-prefixes from expressions, i.e. E = τ.E. The proof of soundness and completeness of this axiomatization is easily deduced from soundness and completeness of the axiomatization of strong simulation over regular CCS expressions. Of related work can be mentioned [1], [2], [3], and [8].

∗Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation

The paper is organized as follows. The first two subsections of section 2 are devoted to preliminaries and background material on regular CCS and strong bisimulation. In the last subsection of section 2 the notion of strong simulation is defined and some properties of strong simulation are stated. In the first subsection of section 3, we present an axiomatization of strong simulation over regular CCS expressions. In the last subsection of section 3 soundness of this axiomatization is proven. Completeness is established in section 4. Section 5 contains the definition of weak simulation, some of its properties, and an axiomatization of weak simulation over regular CCS expressions.

For an introduction to regular CCS and bisimulation we refer to [6] and [4].

2 Preliminaries

In this section we present the strong simulation relation. First we give preliminaries on CCS and strong bisimulation as the notion of strong simulation is closely related to the notion of strong bisimulation.

2.1 Syntax and Semantics of Regular CCS

The syntactic categories for the subset of CCS we are working with are: the set of expressions, P, a countably infinite set of actions, Act, and a countably infinite set of variables, Var. We will denote elements of P by E, F, G, P, Q, and R, elements of Act by α, β, a, and b, and elements of Var by X, Y, and Z.

The set of expressions in P is given by the following grammar.

P ::= 0 | X | α.P | P + P | μX.P

A variable X in an expression E is bound if μX.F occurs in E for some F. We identify expressions that only differ in the names of their bound variables.

For a list of distinct variables X_{1}, …, X_{n} we use the shorthand notation X̃, and similarly for a list of expressions E_{1}, …, E_{n} we write Ẽ. We write E{F_{1}/X_{1}, …, F_{n}/X_{n}} or E{F̃/X̃} for the result of simultaneously substituting F_{i} for each free occurrence of X_{i} in E, renaming bound variables as necessary. The set of free variables of an expression E is denoted V ars(E).

The operational semantics for CCS is given by the labelled transition system (P, Act, ⟶), where ⟶ is the smallest relation closed under the rules in table 1.

[Act] \overline{α.P ⟶^{α} P}

[Sum]  \frac{P_{i} ⟶^{α} P′}{P_{1} + P_{2} ⟶^{α} P′}  i ∈ \{1, 2\}

[Rec] \frac{P \{μX.P/X\} ⟶^{α} P′}{μX.P ⟶^{α} P′}

Table 1: The operational semantics for CCS.

Now, we define a relation ▷ ⊆ P × Var. Intuitively, E ▷ X will hold if the initial transitions of E{P/X} depend on those of P, i.e. X occurs unguarded in E.

Definition 1 (Unguardedness) The relation ▷ ⊆ P × Var is the smallest relation that satisfies

(i) X ▷ X for every X ∈ Var.

(ii) if E ▷ X then E + F ▷ X and F + E ▷ X.

(iii) if E{μY.E/Y } ▷ X then μY.E ▷ X.

■

The variable X is guarded in E if E ⋫ X.

The following lemma describes the interaction between ▷ and the transition relation. The proof of the lemma can be found in [3].

Lemma 1 Let E, P ∈ P. Then

(i) if E{P/X} ⟶^{a} Q then

(a) E ▷ X and P ⟶^{a} Q, or

(b) E ⟶^{a} E′ and Q ≡ E′{P/X} for some E′ ∈ P.

(ii) if E ▷ X and P ⟶^{a} Q then E{P/X} ⟶^{a} Q.

(iii) if E ⟶^{a} E′ then E{Q/X} ⟶^{a} E′{Q/X} for every Q ∈ P.

■

We now proceed to define the notion of strong bisimulation and strong simulation and present some basic properties of these notions.

2.2 Definition and Properties of Strong Bisimulation

The notion of strong simulation, which we will introduce in the next subsection, is closely related to the notion of strong bisimulation defined by Park in [7]. For this reason, and for future reference, we now present the definition of strong bisimulation extended naturally to CCS.

Definition 2 (Strong Bisimulation) A relation R ⊆ P ×P is a strong bisimulation if (P, Q) ∈ R implies,

(i) if P ⟶^{α} P′, where α ∈ Act, then for some Q′ ∈ P, Q ⟶^{α} Q′ and (P′, Q′) ∈ R.

(ii) if Q ⟶^{α} Q′, where α ∈ Act, then for some P′ ∈ P, P ⟶^{α} P′ and (P′, Q′) ∈ R.

(iii) P ▷ X ⇔ Q ▷ X for all X ∈ Var.

■

From the definition of strong bisimulation the notion of strong equivalence is defined.

Definition 3 (Strong Equivalence) P and Q are strongly equivalent or strongly bisimilar, written P ∼ Q, if (P, Q) ∈ R for some strong bisimulation R. ■

Strong equivalence is reflexive, symmetric, and transitive[4]. Furthermore, it has been shown that strong equivalence is a congruence with respect to the operators of CCS[4].

2.3 Definition and Properties of Strong Simulation

We now proceed to define the notion of strong simulation over expressions.

Definition 4 (Strong Simulation) A relation R ⊆ P × P is a strong simulation if (E, F) ∈ R implies, (i) if E ⟶^{α} E′, where α ∈ Act, then there exists F′ ∈ P such that

F ⟶^{α} F′ and (E′, F′) ∈ R.

(ii) E ▷ X ⇒ F ▷ X for all X ∈ Var.

■

From the definition of strong simulation we define the notion of strong simulator.

Definition 5 (Strong Simulator) Q is a strong simulator for P, written P ⊑ Q, if (P, Q) ∈ R for some strong simulation R. ■

We now define a useful generalization of the notion of strong simulation, called strong simulation up to ⊑. In the definition of strong simulation up to ⊑ we use the notation P ⊑ S ⊑ Q, where S is a binary relation over expressions. This means that there exist P′ and Q′ such that P ⊑ P′ S Q′ ⊑ Q.

Definition 6 (Strong Simulation Up To ⊑) A relation S ⊆ P ×P is a strong simulation up to ⊑ if (P, Q) ∈ S implies,

(i) if P ⟶^{α} P′, where α ∈ Act, then there exists Q′ ∈ P such that

Q ⟶^{α} Q′ and P′ ⊑S⊑ Q′.

(ii) P ▷ X ⇒ Q ▷ X for all X ∈ Var.

■

The next theorem, which we will not prove, shows that to establish P ⊑ Q it is enough to prove that (P, Q) belongs to a strong simulation up to ⊑, and this is sometimes easier than finding a strong simulation which contains (P, Q).

Theorem 1 If S is a strong simulation up to ⊑ then ⊑ S ⊑ is a strong simulation and S ⊆ ⊑. ■

The following theorem shows that ⊑ is a precongruence. That is ⊑ is preserved by all the operators of CCS.

Theorem 2 Let P, Q ∈ P. Assume P ⊑ Q then

(i) α.P ⊑ α.Q.

(ii) P + R ⊑ Q + R.

(iii) μY.P ⊑ μX.Q.

Proof: This is easily proven using transition induction. ■

In section 3 we will present an axiomatization of ⊑ and in section 4 we prove completeness of this axiomatization.

3 Axiomatization and Soundness

In this section we will present an axiomatization, A, which is sound and complete for ⊑ over P. The axiom system A is an extension of Milner’s axiom system, A_{M}, for strong equivalence over regular CCS expressions presented in [4].

3.1 Axiomatization

Our axiom system A for strong simulation is defined by the following rules.

S1. E + F = F + E
S2. E + (F + G) = (E + F) + G
S3. E + E = E
S4. E + 0 = E
L.  E ⊑ E + F
R1. μX.E = E{μX.E/X}
RL1. If X is guarded in F and E ⊑ F {E/X} then E ⊑ μX.F
RL2. If F {E/X} ⊑ E then μX.F ⊑ E

We write E = F when E ⊑ F and F ⊑ E. As mentioned, A is an extension of Milner’s axiom system A_{M}. The axiom system A_{M} is defined as A without the rules L, RL1, and RL2 and with the rules R2 and R3 given by

R2. μX.(E + X) = μX.E
R3. If X is guarded in F and E = F {E/X} then E = μX.F

In the following we will write A′ ⊢ E = F when E = F may be proved from the axioms of A′ (A′ ∈ {A_{M}, A}) together with the rules for reflexivity, symmetry, transitivity, and substitutivity of equality. Furthermore, we will write A ⊢ E ⊑ F when E ⊑ F may be proved from the set of axioms A together with the rules for reflexivity, transitivity, and substitutivity of equality and inequality.

3.2 Soundness of A

Since ∼ is contained in ⊑ and since A_{M} is sound with respect to ∼, to show soundness of A we only have to prove soundness of the rules RL1 and RL2 (soundness of L is easily seen).

The next theorem will be used to prove soundness of the axiom RL1 in A. The theorem states that if we have an equation, a solution for the equation up to ∼, and a postfix point for the equation up to ⊑ then the solution can simulate the postfix point.

Theorem 3 Let the variable X be guarded in the expression F, P ∼ F {P/X}, and Q ⊑ F {Q/X}. Then Q ⊑ P.

Proof: Let the relation S be defined as

S = {(E{Q/X}, E{P/X}) | E ∈ P}∪ ⊑

By letting E ≡ X it is seen that (Q, P) ∈ S. So by theorem 1 it will be enough to show that S is a strong simulation up to ⊑. To do this we must first prove that if E{Q/X} S E{P/X} and E{Q/X} ⟶^{α} Q′ then there exists P′ such that E{P/X} ⟶^{α} P′ and Q′ ⊑S⊑ P′. The proof will be by induction transition induction.

Basis:

Case E ≡ X.

In this case we have E{Q/X} ≡ Q ⟶^{α} Q′. Since Q ⊑ F {Q/X} there exists Q′′ such that F {Q/X} ⟶^{α} Q′′ and Q′ ⊑ Q′′. By

lemma 1, we know that Q′′ ≡ F′{Q/X} and F {P/X} ⟶^{α} F′{P/X}.

Since P ∼ F {P/X} there exists P′ such that E{P/X} ≡ P ⟶^{α} P′ and P′ ∼ F′{P/X}. Hence Q′ ⊑ F′{Q/X} S F′{P/X} ⊑ P′.

Case E ≡ α.E_{1}.

Then E{Q/X} ≡ α.E_{1}{Q/X} ⟶^{α} E_{1}{Q/X} and

E{P/X} ≡ α.E_{1}{P/X} ⟶^{α} E_{1}{P/X}.

Since (E_{1}{Q/X}, E_{1}{P/X}) ∈ S we also have E_{1}{Q/X} ⊑S ⊑ E_{1}{P/X} by the reflexivity of ⊑.

Case E ≡ μX.G. This case is trivial since (μX.G){Q/X} ≡ (μX.G){P/X} ≡ μX.G and ⊑ ⊆ S.

Step:

Case E ≡ E_{1} + E_{2}. Then we have E{Q/X} ≡ E_{1}{Q/X} + E_{2}{Q/X}. Assume without loss of generality that E_{1}{Q/X} ⟶^{α} Q′. Then by induction there must exist P′ such that E_{1}{P/X} ⟶^{α} P′ and Q′ ⊑S⊑ P′. Moreover, since E{P/X} ≡ E_{1}{P/X} + E_{2}{P/X}, it follows that E{P/X} ⟶^{α} P′.

Case E ≡ μY.G. In this case we have E{Q/X} ≡ μY.(G{Q/X}). Now,

μY.(G{Q/X}) ⟶^{α} Q′ if G{Q/X}{μY.(G{Q/X})/Y } ⟶^{α} Q′.

Since Y ∉ V ars(Q + P) we have G{Q/X}{μY.(G{Q/X})/Y } ≡ G{μY.G/Y }{Q/X}. By induction there must exist P′ such that G{P/X}{μY.(G{P/X})/Y } ≡

G{μY.G/Y }{P/X} ⟶^{α} P′ and Q′ ⊑ S ⊑ P′. This implies

E{P/X} ≡ μY.(G{P/X}) ⟶^{α} P′.

Furthermore, we must prove that E{Q/X}▷Y implies E{P/X}▷Y for every Y. If E ▷ Y and Y ≠ X we have E{P/X} ▷ Y.

If E ▷ X and Q ▷ Y we have F {Q/X} ▷ Y since Q ⊑ F {Q/X}. X is guarded in F which implies F ▷ Y. This means we also have F {P/X} ▷ Y. Since P ∼ F {P/X} it follows that P ▷ Y. Finally we conclude E{P/X} ▷ Y from E ▷ X and P ▷ Y. ■

We are now ready to prove the soundness of the rule RL1. This is easily done using the previous theorem.

Corollary 1 If X is guarded in F and E ⊑ F {E/X} then E ⊑ μX.F.

Proof: Assume X is guarded in F and E ⊑ F {E/X}. We know μX.F ∼ F {μX.F/X} from theorem 3 we can conclude that E ⊑ μX.F.

■

Soundness of RL2 is stated in the following theorem.

Theorem 4 Let F {E/X} ⊑ E. Then μX.E ⊑ E.

Proof: Let the relation S be defined as

S = {(G{μX.F/X}, G{E/X}) | G ∈ P}∪ ⊑

We will show that S is a simulation up to ⊑. Assume G{μX.F/X} ⟶^{α} P. We have to show that G{E/X} ⟶^{α} Q such that P ⊑ S ⊑ Q. We will prove this by transition induction.

Basis:

Case G ≡ α.G_{1}.

Then G{μX.F/X} ≡ α.G_{1}{μX.F/X} ⟶^{α} G_{1}{μX.F/X} and

G{E/X} ≡ α.G_{1}{E/X} ⟶^{α} G_{1}{E/X}.

Since (G_{1}{μX.F/X}, G_{1}{E/X}) ∈ S we also have G_{1}{μX.F/X} ⊑S⊑ G_{1}{E/X} by the reflexivity of ⊑.

Case G ≡ μX.G_{1}.

This case is trivial since (μX.G_{1}){μX.F/X} ≡ (μX.G_{1}){E/X} ≡ μX.G_{1} and ⊑ ⊆ S.

Step:

Case G ≡ X.

In this case G{μX.F/X} ≡ μX.F ⟶^{α} P, and by a shorter inference we get F {μX.F/X} ⟶^{α} P. By induction there exists Q′

such that F {E/X} ⟶^{α} Q′ and P ⊑ S ⊑ Q′. Since F {E/X} ⊑ E

there exists Q such that G{E/X} ≡ E ⟶^{α} Q and Q′ ⊑ Q.

Case G ≡ G_{1} + G_{2}.

Then we have G{μX.F/X} ≡ G_{1}{μX.F/X}+G_{2}{μx.F/X}. Assume without loss of generality that G_{1}{μX.F/X} ⟶^{α} P′. Then by induction there must exist Q′ such that G_{1}{E/X} ⟶^{α} Q′ and P′ ⊑S⊑ Q′. Moreover, since G{E/X} ≡ G_{1}{E/X} + G_{2}{E/X}, it follows that G{E/X} ⟶^{α} Q′.

Case G ≡ μY.G_{1}.

In this case we have G{μX.F/X} ≡ μY.(G_{1}{μX.F/X}). Now,

μY.(G_{1}{μX.F/X}) ⟶^{α} P′ if

G_{1}{μX.F/X}{μY.(G_{1}{μX.F/X})/Y } ⟶^{α} P′.

Since Y ∉ V ars(μX.F + E) we have

G_{1}{μX.F/X}{μY.(G_{1}{μX.F/X})/Y } ≡ G_{1}{μY.G_{1}/Y }{μX.F/X}. By induction there must exist Q′ such that

G_{1}{E/X}{μY.(G_{1}{E/X})/Y } ≡ G_{1}{μY.G_{1}/Y }{E/X} ⟶^{α} Q′

and P′ ⊑S⊑ Q′. This implies G{E/X} ≡ μY.(G_{1}{E/X}) ⟶^{α} Q′.

Furthermore, we must prove that G{μX.F/X} ▷ Y implies G{E/X} ▷ Y for every Y. If G ▷ Y and Y ≠ X we have G{E/X} ▷ Y. If G ▷ X and μX.F ▷ Y we have F ▷ Y. Since F {E/X} ⊑ E we have that E ▷ Y. We also have that G{E/X} ▷ Y.

Finally we note that (μX.F, E) ∈ S. ■

We state soundness of A with respect to ⊑ in the following corollary.

Corollary 2 (Soundness of A) For all expressions E, F ∈ P, A ⊢ E ⊑ F ⇒ E ⊑ F. ■

The next section is devoted to proving completeness of A with respect to ⊑.

4 Completeness

In this section we will show completeness of the set of axioms A for strong simulation over regular CCS expressions. The structure of the proof of completeness will be similar to that of the proof of completeness of the axiomatization for strong equivalence over regular CCS expressions given by Milner in [4]. The idea in the proof of completeness of A is as follows. When we have two expressions where one can be simulated by the other with respect to ⊑, i.e. E ⊑ E′, we will use the fact that E provably satisfies a list of equations X̃ = F̃ and E′ provably satisfies a list of equations Ỹ = F̃′. From these two lists of equations we construct a new list of equations which E provably satisfies and which E′ is provably a prefix point for. Finally we use the fact that when we have a list of equations and two expressions where the first expression E provably satisfies this list of equations and the second expression E′ is provably a prefix point for the list of equations then it is provable that E can be simulated by E′.

Definition 7 A list of equations L over variables X̃ = (X_{1}, …, X_{n}) is a list

X_{1} = F_{1}
X_{2} = F_{2}
⋮ ⋮
X_{n} = F_{n}

where F̃ = (F_{1}, …, F_{n}) are expressions. The variable X_{1} will be referred to as the leading variable.

An expression E A-provably satisfies L if there exist expressions E_{1}, …, E_{n} (E ≡ E_{1}) such that

A ⊢ E_{i} = F_{i}{E_{1}/X_{1}, …, E_{n}/X_{n}} (i ≤ n)

An expression G is A-provably a prefix point for L if there exist expressions G_{1}, …, G_{n} (G ≡ G_{1}) such that

A ⊢ F_{i}{G_{1}/X_{1}, …, G_{n}/X_{n}} ⊑ G_{i} (i ≤ n)
■

Before we show the final part of the idea for the proof of completeness of A, which we call the ‘Least Solution of Equations’ theorem, we will present some classic results from [4]. These results will be used in the proof of ‘Least Solution of Equations’ theorem and in the proof of completeness theorem for A.

The first result we present is a lemma about syntactic substitution in expressions.

Lemma 2 (Syntactic Substitution in Expressions)

(i) If no variable from X̃ is free in E then

A_{M} ⊢ E{F̃/X̃} = E

(ii) If X̃ and Ỹ are disjoint sets of variables then

A_{M} ⊢ E{F̃/X̃}{G̃/Ỹ } = E{F̃{G̃/Ỹ }/X̃, G̃/Ỹ }
■

The last result from [4] we present shows that every expression is provably equal to an expression in a special form. The result means that to prove completeness of A we only have to look at expressions in this special form.

Theorem 5 (Equational Characterization) For any expression E, with free variables in Ỹ, there exist expressions E_{1}, …, E_{p} (p > 0) with free variables in Ỹ such that

A_{M} ⊢ E_{i} = ∑_{j=1}^{m(i)} a_{ij}.E_{f(i,j)} + ∑_{j=1}^{n(i)} Y_{g(i,j)} (i ≤ p)

and A_{M} ⊢ E = E_{1}. ■

The following theorem states that the rules R2 and R3 from A_{M} can be derived from A.

Theorem 6 (A_{M} ⊂ A)

(i) If X is guarded in F and A ⊢ E = F {E/X} then A ⊢ E = μX.F

(ii) A ⊢ μX.(E + X) = μX.E

Proof: Case (i) follows directly from the rules RL1 and RL2. For case (ii) we show that A ⊢ μX.E ⊑ μX.(E + X) and A ⊢ μX.(E + X) ⊑ μX.E. The former case is proven by a simple application of the rule L. The latter case is proven as follows. By the rules S3 and R1 we get A ⊢ μX.E = μX.E + μX.E = E{μX.E/X} + μX.E = (E + X){μX.E/X}. By the rule RL2 we have A ⊢ μX.(E + X) ⊑ μX.E. ■

Since A_{M} is a subset of A the results from lemma 2 and theorem 5 also hold if A_{M} is substituted with A.

We are now ready to prove the ‘Least Solution of Equations’ theorem. The theorem will play an important role in the proof of completeness of A.

Theorem 7 (Least Solutions of Equations) Let X̃ = (X_{1}, …, X_{m}) and Ỹ = (Y_{1}, …, Y_{n}) be distinct variables and F̃ = (F_{1}, …, F_{m}) expressions with free variables in X̃ and Ỹ in which each X_{i} is guarded. If Ẽ = (E_{1}, …, E_{m}) and Ẽ′ = (E′_{1}, …, E′_{m}) are expressions with free variables in Ỹ such that

A ⊢E_{i} = F_{i}{Ẽ/X̃},  i ≤ m and
A ⊢F_{i}{Ẽ′/X̃} ⊑ E′_{i},  i ≤ m

then

A ⊢E_{i} ⊑ E′_{i},  i ≤ m

Proof: The proof will be by induction on m.

Basis: m = 1. We have

A ⊢E_{1} = F_{1}{E_{1}/X_{1}} and  (1)
A ⊢F_{1}{E′_{1}/X_{1}} ⊑ E′_{1}  (2)

By R3 and (1) we get

A ⊢μX_{1}.F_{1} = E_{1}

and by (2) and RL2 we deduce

A ⊢μX_{1}.F_{1} ⊑ E′_{1}

This gives us

A ⊢ E_{1} ⊑ E′_{1}

Step: Assume the theorem holds for m. Let F̃ = {F_{1}, …, F_{m}} and F_{m+1} be expressions with free variables in (X̃, X_{m+1}, Ỹ) in which each X_{i} is guarded (i ≤ m + 1), such that

A ⊢E_{i} = F_{i}{Ẽ/X̃, E_{m+1}/X_{m+1}},  i ≤ m + 1 and  (3)
A ⊢F_{i}{Ẽ′/X̃, E′_{m+1}/X_{m+1}} ⊑ E′_{i},  i ≤ m + 1  (4)

As shown in the proof of theorem 5.7 in [4] we have

A_{M} ⊢ E_{i} = G_{i}{Ẽ/X̃}, i ≤ m + 1

where the G_{i}’s are defined as

G_{i} ≡ F_{i}{G_{m+1}/X_{m+1}},  i ≤ m and  (5)
G_{m+1} ≡ μX_{m+1}.F_{m+1}  (6)

Using lemma 2 with equation m + 1 in (4) we get

A ⊢ F_{m+1}{Ẽ′/X̃}{E′_{m+1}/X_{m+1}} ⊑ E′_{m+1}

Since X_{m+1} is guarded in F_{m+1}{Ẽ′/X̃} we have from RL2 that

A ⊢ μX_{m+1}.(F_{m+1}{Ẽ′/X̃}) ⊑ E′_{m+1}

Since μX_{m+1}.(F_{m+1}{Ẽ′/X̃}) ≡ (μX_{m+1}.F_{m+1}){Ẽ′/X̃}, by (6) we have

A ⊢ G_{m+1}{Ẽ′/X̃} ⊑ E′_{m+1}  (7)

By (4) and (7) we obtain

A ⊢ F_{i}{Ẽ′/X̃, G_{m+1}{Ẽ′/X̃}/X_{m+1}} ⊑ E′_{i}, i ≤ m

From lemma 2 we get

A ⊢ F_{i}{G_{m+1}/X_{m+1}}{Ẽ′/X̃} ⊑ E′_{i}, i ≤ m

By (5) we deduce

A ⊢ G_{i}{Ẽ′/X̃} ⊑ E′_{i}, i ≤ m

Since

A ⊢ G_{i}{Ẽ/X̃} = E_{i}, i ≤ m

and V ars(G_{1}) ∪ ⋯ ∪ V ars(G_{m}) ⊆ (X̃, Ỹ) and each X_{j} (j ≤ m) is guarded in each G_{i} (i ≤ m) we have by induction

A ⊢ E_{i} ⊑ E′_{i},  i ≤ m  (8)

Using A ⊢ E_{m+1} = G_{m+1}{Ẽ/X̃} and (8) we get

A ⊢ E_{m+1} = G_{m+1}{Ẽ/X̃} ⊑ G_{m+1}{Ẽ′/X̃}

By (7) we deduce

A ⊢ E_{m+1} ⊑ E′_{m+1}

completing the proof.

■

Finally we are ready to put the things together in the proof of completeness of A.

Theorem 8 For all expressions E, E′ ∈ P, E ⊑ E′ ⇒ A ⊢ E ⊑ E′

Proof: Let Ỹ = V ars(E) ∪ V ars(E′). By theorem 5 there exist Ẽ = (E_{1}, …, E_{p}) and Ẽ′ = (E′_{1}, …, E′_{p′}) such that

A_{M} ⊢ E_{i} = ∑_{j=1}^{m(i)} a_{ij}.E_{f(i,j)} + ∑_{j=1}^{n(i)} Y_{g(i,j)},  (i ≤ p)  (9)

A_{M} ⊢ E′_{i} = ∑_{j=1}^{m′(i)} a′_{ij}.E′_{f′(i,j)} + ∑_{j=1}^{n′(i)} Y_{g′(i,j)},  (i ≤ p′)  (10)

where A_{M} ⊢ E = E_{1} and A_{M} ⊢ E′ = E′_{1}.

Now let I = {(i, i′) | E_{i} ⊑ E′_{i′}}. We observe that since E ⊑ E′, A ⊢ E = E_{1} and A ⊢ E′ = E′_{1} we must have E_{1} ⊑ E′_{1} and therefore (1, 1) ∈ I. For each (i, i′) ∈ I the following must hold 1. For each summand a_{ij}.E_{f(i,j)} of the right-hand side of equation i in

(9) there must exist a summand a′_{i′j′}.E′_{f′(i′,j′)} in the right-hand side of equation i′ in (10) such that a_{ij} = a′_{i′j′} and E_{f(i,j)} ⊑ E′_{f′(i′,j′)}.

2. Each summand Y_{g(i,j)} of the right-hand side of equation i in (9) must also be a summand in the right-hand side of equation i′ in (10). That is A ⊢ ∑_{j=1}^{n(i)} Y_{g(i,j)} ⊑ ∑_{j=1}^{n′(i′)} Y_{g′(i′,j)}.

Point 1 above implies that the relation J_{ii′} defined by

J_{ii′} = {(j, j′) | a_{ij} = a′_{i′j′} ∧ (f(i, j), f′(i′, j′)) ∈ I}

is total between {1, …, m(i)} and {1, …, m′(i′)} if (i, i′) ∈ I. We will use these relations to construct a list of equations which E_{1} provably satisfies and E′_{1} is provably a prefix point for. The list of equations is defined by

X_{ii′} = ∑_{(j,j′)∈J_{ii′}} a_{ij}.X_{f(i,j)f′(i′,j′)} + ∑_{j=1}^{n(i)} Y_{g(i,j)},  ((i, i′) ∈ I)  (11)

where the X_{ii′}’s are free variables not in Ỹ. We take X_{11} to be the leading variable in the equation list.

To see that the list of equations (11) is provably satisfied by E_{1} we first instantiate each X_{ii′} to E_{i}. The equations then become

E_{i} = ∑_{(j,j′)∈J_{ii′}} a_{ij}.E_{f(i,j)} + ∑_{j=1}^{n(i)} Y_{g(i,j)},  ((i, i′) ∈ I)  (12)

This is provable using S1, S2 and S3 since the totality of J_{ii′} implies that the right-hand side of (12) only differs from the right-hand side of (9) by repeated, reordered and regrouped summands.

To show that E′_{1} is provably a prefix point for the equation list (11) we will show that

∑_{(j,j′)∈J_{ii′}} a_{ij}.E′_{f′(i′,j′)} + ∑_{j=1}^{n(i)} Y_{g(i,j)} ⊑ E′_{i′},  ((i, i′) ∈ I)  (13)

is provable. The left-hand side of (13) is obtained by replacing each X_{ii′} with E′_{i′} in the right-hand side of (11). Equation (13) is provable using S1, S2, S3, and L since each summand of the right-hand side of (13) is also a summand of the right-hand side of equation i′ in (10).

From theorem 7 it follows that A ⊢ E_{i} ⊑ E′_{i′} for each (i, i′) ∈ I. Since (1, 1) ∈ I, A ⊢ E_{1} = E, and A ⊢ E′_{1} = E′, we conclude A ⊢ E ⊑ E′. ■

5 Weak Simulation

At this point we proceed by looking at a weaker notion of simulation which allows for the abstraction from silent transitions (τ-transitions). This weaker notion of simulation is called weak simulation.

5.1 Definition and Properties of Weak Simulation

Let Act_{τ} = Act ∪ {τ}. If α ≠ τ then E ⟹^{α̂} E′ is a shorthand notation for E ⟶^{τ}*⟶^{α}⟶^{τ}*E′ otherwise it is a shorthand notation for E ⟶^{τ}*E′. We

also write E ⟹^{a} E′ if E ⟶^{τ}*⟶^{a}⟶^{τ}*E′ and E ⟹^{ε} E′ if E ⟶^{τ}*E′.

Definition 8 (Weak Simulation) A relation R ⊆ P ×P is a weak simulation if (P, Q) ∈ R implies,

(i) if P ⟶^{α} P′, where α ∈ Act_{τ}, then for some Q′ ∈ P, Q ⟹^{α̂} Q′ and (P′, Q′) ∈ R and

(ii) if P ▷ X then there exists Q′ such that Q ⟹^{ε} Q′ and Q′ ▷ X.

■

From the definition of weak simulation we define weak simulator.

Definition 9 (Weak Simulator) Q is a weak simulator for P, written P ⪅ Q, if (P, Q) ∈ R for some weak simulation R. ■

Note that ⪅ is reflexive and transitive.

For an expression E we let E^{−τ} denote the expression obtained by removing the τ-prefixes from E.

Definition 10 The function (·)^{−τ} : P ↦ P is defined by

0^{−τ} = 0
X^{−τ} = X
(α.E)^{−τ} = \{ \begin{matrix}α.E^{−τ} & if α ≠ τ \\ E^{−τ} & otherwise \end{matrix}
(E_{1} + E_{2})^{−τ} = E_{1}^{−τ} + E_{2}^{−τ}
(μX.E)^{−τ} = μX.E^{−τ}
■

In the following we will prove that E and E^{−τ} can simulate each other. To do this we need the following definition and lemma.

Definition 11 =_{AC} is the least congruence over regular CCS expressions satisfying the equations S1, S2, S4, and R1. ■

Lemma 3

(i) If E ⟶^{a} F then E^{−τ} ⟶^{a} F^{−τ}.

(ii) If E ⟶^{τ} F then E^{−τ} =_{AC} F^{−τ} + G for some τ-free expression G.

(iii) If E^{−τ} ⟶^{a} E′ then E ⟹^{a} F for some F such that F^{−τ} ≡ E′.

■

Theorem 9 Let E ∈ P. Then E ⪅ E^{−τ} and E^{−τ} ⪅ E.

Proof: We will show that the relation R defined as

R =^{def} {(E, F) | E ∈ P ∧ ∃G ∈ P.F =_{AC} E^{−τ} + G^{−τ} } ∪ {(E^{−τ} , E) | E ∈ P }

is a weak simulation. We consider each of the kinds of pairs in this relation in turn, and show that the defining clauses of weak simulation are met.

Case ERF, where F =_{AC} E^{−τ} + G^{−τ}.

Assume E ⟶^{α} E′ and α ≠ τ.

By lemma 3 E^{−τ} ⟶^{α} E^{′−τ} and clearly (E′, E^{′−τ} + 0) ∈ R.

Assume E ⟶^{τ} E′.

By lemma 3 E^{−τ} =_{AC} E^{′−τ} + G′ for some G′. Since G′ contain

no τs it follows that (E′, E^{′−τ} + (G′ + G^{−τ})) ∈ R.

Case E^{−τ} RE.

Assume E^{−τ} ⟶^{a} E′. By lemma 3 E ⟹^{a} F for some F such that

F^{−τ} ≡ E′ and clearly (E′, F) ∈ R.

Finally, we note that E ▷ X implies F =_{AC} E^{−τ} + G^{−τ} ▷ X, and E^{−τ} ▷ X implies E ⟹^{ε} E′ ▷ X for some E′.

Since ERE^{−τ} and E^{−τ} RE both hold and R is a weak simulation, we may conclude that E ⪅ E^{−τ} and E^{−τ} ⪅ E. ■

Unlike Milner’s observation equivalence, the weak simulation ⪅ is preserved by all the operators of CCS. The following corollary states that ⪅ is a precongruence. The proof uses the above theorem to lift the precongruence result from ⊑ to ⪅.

Corollary 3 If P ⪅ Q then

(i) α.P ⪅ α.Q

(ii) P + R ⪅ Q + R , for all R ∈ P (iii) μX.P ⪅ μX.Q

Proof: We will only prove that (ii) holds, since the other cases are shown in a similarly way. By theorem 9 and the transitivity of ⪅ we get P^{−τ} ⪅ Q^{−τ}. This implies P^{−τ} ⊑ Q^{−τ}. As ⊑ is a precongruence we have P^{−τ} + R^{−τ} ⊑ Q^{−τ} + R^{−τ}. Since ⊑ ⊆ ⪅ we deduce P^{−τ} + R^{−τ} ⪅ Q^{−τ} + R^{−τ}. Now, by theorem 9 and the transitivity of ⪅ we get P + R ⪅ Q + R. ■

5.2 Axiomatization

An axiomatization, A_{W}, of weak simulation for regular CCS expressions is presented below.

S1. E + F = F + E
S2. E + (F + G) = (E + F) + G
S3. E + E = E
S4. E + 0 = E
T.  E = τ.E
L.  E ⪅ E + F
R1. μX.E = E{μX.E/X}
RL1. If X is guarded in F and E ⪅ F {E/X} then E ⪅ μX.F
RL2. If F {E/X} ⪅ E then μX.F ⪅ E

Soundness and completeness of A_{W} is easily proven using the rule T, theorem 9, and soundness and completeness of A for ⊑ over regular CCS expressions.

Theorem 10 (Soundness and Completeness of A_{W}) For all expressions E, F ∈ P, A_{W} ⊢ E ⪅ F ⇔ E ⪅ F. ■

6 Conclusion

In this paper we have presented a sound and complete axiomatization of strong simulation over regular CCS expressions. The proof of completeness of the proposed axiomatization uses an adaptation of Milner’s classic arguments in [4]. We have also presented a sound and complete axiomatization of weak simulation over regular CCS expressions. The proof of soundness and completeness of this was easily deduced from soundness and completeness of the axiomatization of strong simulation over regular CCS expressions and the fact that τ-prefixes can be removed from and inserted into an expression without changing its observable behavior.

References

[1] Bergstra, J. & Fokkink, W. & Ponse, A. Process Algebra with Recursive Operations. Chapter from Handbook of Process Algebra, pp. 333-389, 2001.

[2] Fokkink, W. An Axiomatization for Regular Processes in Timed Branching Bisimulation. Fundamenta Informaticae, 32(3/4):329-340, December 1997.

[3] Glabbeek, Robert Jan van. A Complete Axiomatization for Branching Bisimulation Congruence of Finite-state Behaviours. Mathematical Foundations of Computer Science, pp. 473-484, August/September 1993.

[4] Milner, Robin. A Complete Inference System for a Class of Regular Behaviors. Journal of Computer and System Sciences, 28:439-466, 1984.

[5] Milner, Robin. A Complete Axiomatization for Observational Congruence of Finite-state Behaviors. Information and Computation, 81(2):227-247, May 1989.

[6] Milner, Robin. Communication and Concurrency. Prentice Hall International, Englewood Cliffs, 1989. ISBN: 0-13-115007-3.

[7] Park, David. Concurrency and Automata on Infinite Sequences. Lecture Notes in Computer Science, 104:167-183, 1981.

[8] Rabinovich, Alexander. A Complete Axiomatisation for Trace Congruence of Finite State Behaviors. Mathematical Foundations of Programming Semantics (New Orleans, LA, 1993), pp. 530-543, 1994.

Recent BRICS Report Series Publications

RS-01-26 Ulrik Frendrup and Jesper Nyholm Jensen. A Complete Axiomatization of Simulation for Regular CCS Expressions. June 2001. 18 pp.

RS-01-25 Bernd Grobauer. Cost Recurrences for DML Programs. June 2001. 51 pp. Extended version of a paper to appear in Leroy, editor, Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming, 2001.

RS-01-24 ZoltánÉsik and Zoltán L. Németh. Automata on Series-Parallel Biposets. June 2001. 15 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.

RS-01-23 Olivier Danvy and Lasse R. Nielsen. Defunctionalization at Work. June 2001. 45 pp. Extended version of an article to appear in Søndergaard, editor, 3rd International Conference on Principles and Practice of Declarative Programming, PPDP ’01 Proceedings, 2001.

RS-01-22 Zoltán Ésik. The Equational Theory of Fixed Points with Applications to Generalized Language Theory. June 2001. 21 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.

RS-01-21 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational Theories of Tropical Semirings. June 2001. 52 pp. Extended abstracts of parts of this paper have appeared in Honsell and Miculan, editors, Foundations of Software Science and Computation Structures, FoSSaCS ’01 Proceedings, LNCS 2030, 2000, pages 42–56 and in Gaubert and Loiseau, editors, Workshop on Max-plus Algebras and their Applications to Discrete-event Systems, Theoretical Computer Science, and Optimization, MAX-PLUS ’01 Proceedings, IFAC (International Federation of Automatic Control) IFAC Publications, 2001.

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