BRICS Basic Research in Computer Science

BRICSRS-94-43Aceto&Jeffrey:ACompleteAxiomatizationofTimedBisimulation

BRICS

Basic Research in Computer Science

A Complete Axiomatization of

Timed Bisimulation for a Class of Timed Regular Behaviours

(Revised Version)

Luca Aceto Alan Jeffrey

BRICS Report Series RS-94-43

ISSN 0909-0878 December 1994

Copyright c 1994, 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 publications in the BRICS Report Series. 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@daimi.aau.dk

A complete axiomatization of timed bisimulation for a class of timed regular behaviours

(Revised version)

Luca Aceto

BRICS y

Department of Mathematics and Computer Science Aalborg University

Fredrik Bajersvej 7E 9220 Aalborg , Denmark

Alan Jerey

^z

School of Cognitive and Computing Sciences University of Sussex, Brighton BN1 9QH, UK

Abstract

One of the most satisfactory results in process theory is Milner's axiom- atization of strong bisimulation for regular CCS. This result holds for open terms with nite-state recursion. Wang has shown that timed bisimulation can also be axiomatized, but only for closed terms without recursion. In this paper, we provide an axiomatization for timed bisimulation of open terms with nite-state recursion.

Key words and phrases.

Complete axiomatizations, ^!-complete- ness, equational logic, timed bisimulation equivalence, regular processes, timed CCS.

1 Introduction

Much research in concurrency theory has recently been devoted to the devel- opment of extensions of standard process algebras like CCS 16], CSP 11] and ACP 3] with constructs allowing for the modelling of timing aspects in the behaviour of processes. By now, most process algebras have a timed counter- part (see, e.g., 1, 6, 18, 21]), and the development of results and techniques for these languages is becoming comparable with that for the standard process description languages. For example, complete axiomatizations of behavioural

On leave from School of Cognitive and Computing Sciences, University of Sussex, Brighton BN1 9QH, UK. Email: luca@iesd.auc.dk.

yBasic Research in Computer Science, Centre of the Danish National Research Foundation.

zSupported by SERC project GR/H 16537. Additional funding was received from EC BRA 7166 . Email: alanje@cogs.susx.ac.uk.

congruences for subsets of timed process algebras have been presented in, e.g., 10, 14, 18, 22]|showing that behavioural congruences which deal with timing considerations are as mathematically tractable as the standard untimed ones.

Two of the most beautiful results in the theory of process algebras are the complete axiomatizations of strong bisimulation equivalence and observational congruence for regular CCS processes provided by Milner in his classic papers 15] and 17], respectively. These results have put the notions of behaviour used in the theory of CCS on an equal footing with the one common in formal language theory, and have contributed to the realization that the notion of processis at least as elegant and mathematically tractable as that of language.

The main purpose of this paper is to show that the techniques developed by Milner in 15, 17] can be adapted to provide a complete axiomatization of the notion of timed bisimulation equivalence, due to Wang Yi 21], over a class of regular timed CCS processes 12, 22]. More precisely, we shall oer a complete axiomatization of timed bisimulation over the language of action guarded reg- ular expressions studied in 12]. This complete axiomatization is obtained by combining an improved version of the laws which were shown in 22] to char- acterize timed bisimulation over nite trees with standard laws for recursively dened processes, viz, laws to unwind recursive denitions of expressions, and a version of unique xed-point induction.

The paper is organized as follows. Section 2 is devoted to preliminaries, and background material on timed CCS and timed bisimulation. The axiomatiza- tion of timed bisimulation is presented and discussed in Section 3, where its soundness is also proved. The proof of completeness of the axiomatization is given in detail in Section 4, and relies on an adaptation of the techniques used by Milner in 15, 17].

As this is not an introductory paper on timed CCS, we have taken the liberty to refer the reader to the original papers by Wang Yi for motivations and examples. We hope, however, that the paper will still be suciently readable for the uninitiated reader.

2 Timed regular behaviours and timed bisimulation

The language for expressions that we shall consider in this paper is a generaliza- tion of the regular subcalculus of Wang Yi's timed CCS 21, 23]. This language has been investigated by Holmer, Larsen and Wang Yi in 12], and we shall mostly follow the notation and denitions given in that reference.

As usual, we shall assume a countably innite set of action names, ranged over by

a

and

b

, and a distinguished action

⁶². Let Act = ^f

^g, be the set of actions, ranged over by

and

.

Following 13], we dene a monoid (

X

+

0) to be:

left-cancellative i (

x

+

y

=

x

+

z

)⁾(

y

=

z

), and

anti-symmetrici (

x

+

y

= 0)⁾(

x

=

y

= 0).

Examples of left-cancellative anti-symmetric monoids include:

The singleton set (

1

⁺

^0).

The natural numbers (

N

+

0).

The non-negative rationals (

Q

⁺

⁺

^0).

The non-negative reals (

R

⁺

+

0).

The countable ordinals (

!

¹

+

0).

We can dene a partial order on

X

as:

x

y

i ⁹

z : x

+

z

=

y

It is simple to verify thatis a partial order if (

X

+

0) is a left-cancellative anti-symmetric monoid. A time domain is a left-cancellative anti-symmetric monoid (Tim

+

0), ranged over by

t

,

u

and

v

, such that is a total order.

Dene:

t

^{^}

u

= the minimum of

t

and

u t

^_

u

= the maximum of

t

and

u

and when

t

u

:

t

^;

u

= the unique

v

such that

u

+

v

=

t

Let Tim⁺= Tim^nf0^g be the set of positive delays, ranged over by

c

,

d

and

e

. Let Lab = Act^f

"

(

c

)^j

c

²Tim^+g be the set of labels, ranged over by . Let Var be a countably innite set of process variables, ranged over by

x

,

y

and

z

.

The set of regular process expressions over Act, Tim and Var is given by the following grammar:

E

::=

0

^j

x

^j

:E

^j

"

(

t

)

:E

^j

E

+

E

^j

x

(

x

=

E

)

The interested reader is referred to 21, 23] for intuition on the operators used in the above denition.

We shall assume the standard notions of free and bound variables in expres- sions, with

x

(

x

= ) as the binding construct. The set of free variables in an expression

E

is denoted by fv

E

. Throughout this paper we shall restrict our- selves to considering regular process expressions in which recursions are action guarded, a notion that is dened below.

Denition

^{A variable}

^x

^is action guarded in

E

i

x

²

AG

⁽

^E

^{), dened:}

AG

⁽

0

^{) = Var}

AG

⁽

^x

^{) = Varnf}

^x

^g

AG

(

:E

) = Var

AG

(

"

(

t

)

:E

) =

AG

(

E

)

AG

⁽

^E

⁺

^F

^{) =}

AG

⁽

^E

^)\

AG

⁽

^F

⁾

AG

⁽

x

⁽

^x

⁼

^E

^{)) =}

AG

⁽

^E

^)f

^x

^g

A regular process expression

E

is well-formed i for every subexpression of

E

of the form

x

⁽

^x

⁼

^F

^),

^x

is action guarded in

F

.

0

^;";(!c)

0 :P

^;!

P a:P

^;";(!c)

a:P

"

(

c

+

t

)

:P

^;";(!c)

"

(

t

)

:P P

^;";(!c)

P

⁰

"

(

t

)

:P

^;";(t;+!c)

P

⁰

P

^;!

P

⁰

"

(0)

:P

^;!

P

⁰

P

^;!

P

⁰

P

+

Q

^;!

P

⁰

Q

^;!

Q

⁰

P

+

Q

^;!

Q

⁰

P

^;";(!c)

P

⁰

Q

^;";(!c)

Q

⁰

P

+

Q

^;";(!c)

P

⁰+

Q

⁰

E

^f

x

⁽

^x

⁼

^E

⁾

^=x

^g;!

^P

x

(

x

=

E

)^;!

P

Figure 1: The operational semantics for

TC

⁰

For example, the expression (

x

⁽

^x

⁼

^:x

⁾⁾⁺

^y

is well-formed, while the expres- sion

x

(

x

=

"

(

c

)

:x

) is not. The above denition departs slightly from the one given in 12, Denition 2.1]. In particular, the expression (

x

(

x

=

:x

)) +

y

would not be well-formed according to the denition of 12] because the free variable

y

does not occur within a subexpression of the form

:F

.

The set of all well-formed regular process expressions is

TC

, ranged over by

E

,

F

and

G

. The set of all closed, well-formed regular process expressions is

TC

⁰, ranged over by

P

,

Q

and

R

. Elements of this set will often be referred to as processes.

Following Milner 17], we shall identify expressions which dier only by the renaming of bound variables. We shall also write

E

^f

F

¹

:::F

n

=x

¹

:::x

n^g for the result of simultaneously substituting

F

i for each free occurrence of

x

i in

E

, renaming bound variables as necessary.

The operational semantics for

TC

⁰is given by the labelled transition system (

TC

⁰

Lab

^!) in Figure 1. The interested reader is referred to 21, 23] for comments on the rules. Note that, following Wang Yi 21, 23],

"

(0) has been excluded from the semantics of processes.

To conclude this introductory section, we shall now dene the notion of timed bisimulation equivalence21].

Denition

^{A relation Rover}

TC

^{0 is a}timed bisimulation i

P

^R

Q

implies, for all :

whenever

P

^;!

P

⁰ then, for some

Q

⁰,

Q

^;!

Q

⁰ and

P

^0R

Q

⁰.

whenever

Q

^;!

Q

⁰ then, for some

P

⁰,

P

^;!

P

⁰ and

P

^0R

Q

⁰.

The relation of timed bisimulation equivalence, denoted by , is the largest timed bisimulation.

The interested reader is referred to the aforementioned papers by Wang Yi, and to 12] for intuition and examples of processes that are equivalent or inequivalent

with respect to . The denition of can be extended to expressions in the standard way as follows:

Denition

^Let

^E

^and

^F

be expressions with free variables in

x

~=

x

¹

:::x

m. Then

E

F

i for all vectors ~

P

=

P

¹

:::P

m,

E

^f

P=

^~

x

~^g

F

^f

P=

^~

x

~^g.

Proposition 1 (21, Theorem 5.1])

Timed bisimulation equivalence forms a congruence over

TC

^.

In the remainder of this paper, we shall present a complete axiomatization of

over

TC

^.

3 Axiomatization and soundness

In 21] various equational laws were proved to hold for Wang Yi's timed CCS modulo timed bisimulation equivalence, and in 22] a set of such axioms was shown to be complete over the language of recursion-free

TC

⁰ processes with delays from the time domain of the positive reals. We shall now present an axiomatization which will be proven complete forover the whole of

TC

, i.e., complete for regular process expressions with action guarded recursion. The detailed proof of completeness occupies Section 4 of this paper.

Wang's axiomatization for recursion-free

TC

⁰ processes is given by the ax- iom system^F in Figures 2 and 3. Our axiomatization for regular

TC

^process

expressions is given by the axiom system^E in Figures 2 and 4.

The axioms (S1){(S4) are the standard laws for a complete axiomatization of strong bisimulation equivalence over nite trees 9]. Together with axioms (R1) and (R2), these form a complete axiomatization of strong bisimulation equivalence for guarded regular CCS terms 15]. (In fact, the axiomatization in 15] can be obtained as a special case of that in Figure 2 by taking the time domain to be the singleton set (

1

⁺

^0).)

The axioms (TD), (TA) and (T0) correspond to the operational properties of time determinacy, time additivity and zero delay. These axioms are present in Wang's 21, 22] axiomatization. As we shall see in Section 4, the axiom system^Ggiven in Figure 2 is powerful enough to prove Milner's 15] Equational Characterization Theorem for timed regular expressions. However, ^G is not powerful enough to give a complete axiomatization for recursion-free timed expressions.

Wang 21, 22] added the axioms (MP), (AP) and (NP) to ^G to provide a complete axiomatization for recursion-free

TC

⁰ processes. These axioms cor- respond to the operational properties of maximal progress and persistency, and are discussed in detail by Wang. However, the resulting axiom system ^F, given in Figure 3, is not powerful enough to give a complete axiomatization for recursion-free

TC

process expressions.

Our axiomatization replaces (AP) and (NP) with one new persistency axiom (P). In Section 4 we show that^E is complete for timed bisimulation equivalence over

TC

process expressions. In Section 5 we show that ^E is strictly stronger than ^F, and thus that Wang's axiomatization is not complete for open

TC

process expressions.

(S1)

E

+

F

=

F

+

E

(S2)

E

+ (

F

+

G

) = (

E

+

F

) +

G

(S3)

E

+

E

=

E

(S4)

E

+

0

=

E

(TD)

"

(

t

)

:

(

E

+

F

) =

"

(

t

)

:E

+

"

(

t

)

:F

(TA)

"

(

t

+

u

)

:E

=

"

(

t

)

:"

(

u

)

:E

(T0)

"

(0)

:E

=

E

(R1)

x

(

x

=

E

) =

E

^f

x

(

x

=

E

)

=x

^g

(R2) If

F

=

E

^f

F=x

^g, then

F

=

x

⁽

^x

⁼

^E

^{), if}

^x

is action guarded in

E

Figure 2: The axiom system^G

(MP)

:E

+

"

(

c

)

:F

=

:E

(AP)

a:E

+

"

(

t

)

:a:E

=

a:E

(NP)

"

(

t

)

: 0

=

0

Figure 3: The axiom system^F is ^G plus (MP), (AP) and (NP)

(MP)

:E

+

"

(

c

)

:F

=

:E

(P)

E

+

"

(

t

)

:E

=

E

Figure 4: The axiom system^E is ^G plus (MP) and (P)

We shall write ^{E `}

E

=

F

when

E

=

F

may be proved from ^E together with the structural rules for = to be a congruence, and similarly for^{F `}

E

=

F

and^{G `}

E

=

F

.

To conclude this section, we shall show that^E is indeed sound with respect to timed bisimulation equivalence over

TC

.

Proposition 2 (Soundness)

^{For all}

TC

expressions

EF

, ^{E `}

E

=

F

im- plies

E

F

.

Proof

. All the laws in ^E have been shown sound by Wang Yi in 22]. The only exception is the persistency axiom ^(P), the soundness of which is established by the timed bisimulation:

(^f(

Q

+

PQ

)^j9

c : P

^;";(!c)

Q

^gf(

PP

)^j

P

²

TC

^0g)

where denotes composition of relations. The proof that this relation is a bisimulation depends on the properties of time determinacy, time additivity and persistency of the operational semantics for

TC

⁰, and the soundness of

(T0). (The interested reader is referred to 21] and 20] for details on these

properties). ²

4 Completeness

In this section, we shall present the proof of completeness of the set of laws^E over

TC

. The structure of the proof of this result will follow closely the most beautiful arguments used by Milner in 15, 17] to prove the completeness of the axiomatizations for strong bisimulation and observational congruence over regular CCS processes.

The structure of the completeness proof will be as follows: rst of all, we shall show that every

TC

expression

E

provably satises a certain kind of equa- tion set. This is what Milner calls the Equational Characterization Theorem.

Next, we shall show that if

E

F

and

E

provably satises an equation set, while

F

provably satises another equation set, then both

E

and

F

provably satisfy a common equation set. Finally, we show that whenever two

TC

ex- pressions provably satisfy the same equation set, then ^E proves that they are equal.

Denition

^An equation set ~

x

= ~

E

is a nite non-empty sequence of declara- tions

x

¹ =

E

¹

:::x

n =

E

n, where the

x

is are pairwise distinct variables, and the

E

is are

TC

expressions.

A vector ~

F

=

F

¹

:::F

n satises ~

x

= ~

E

i ⁸

i : F

i

E

i^f

F=

~

x

~^g.

For an equational theory ^T, a vector ~

F

=

F

¹

:::F

n ^T-provably satises

x

~= ~

E

i ⁸

i :

^{T `}

F

i=

E

i^f

F=

~

x

~^g.

An expression

E

(^T-provably) satises

x

~ = ~

F

i we can nd a vector ~

E

which (^T-provably) satises ~

x

= ~

F

and

E

E

¹ (^{T `}

E

=

E

¹).

We refer to

x

¹ as the leading variable of the equation set

x

~= ~

F

. For example, the equation set:

x

¹=

"

(1)

:a:x

²+

"

(3)

:y x

² =

"

(2)

:b:x

¹ (1) is satised by

x

⁽

^z

⁼

^"

⁽¹⁾

^:a:"

⁽²⁾

^:b:z

⁺

^"

⁽³⁾

^:y

^).

Denition

An equation set

x

~= ~

E

is standard i each

E

i is of the form:

X

j²Jⁱ

"

(

t

j)

:

j

:x

j+ ^X

k²Kⁱ

"

(

u

k)

:w

k

where the vectors

x

~ and

w

~ are disjoint. By convention, we indentify each

E

i

with

0

when the index sets

J

i and

K

i are both empty. We call

x

~ the formal variables of

x

~= ~

E

, and

w

~ the free variables of ~

x

= ~

E

.

For example, the above equation set (1) is standard, but the following is not:

x

¹=

"

(1)

:x

²+

"

(3)

:y x

² =

a:"

(2)

:b:x

¹

Proposition 3

^If

^x

^{~ = ~}

^E

is standard and

w

is not a formal variable, then we can nd a standard

x

~= ~

F

such that ⁸

i :

^{G `}

F

i =

E

i^f

E

¹

=w

^g.

Proof

. Dene ~

F

as:

F

i ^X

j²Jⁱ

"

(

t

j)

:

j

:x

j+^X

k²Kⁱ w^k6=w

"

(

u

k)

:w

k

+^X

k²Kⁱ w^k=w j⁰²J¹

"

(

u

k+

t

j⁰)

:

j⁰

:x

j⁰+^X

k²Kⁱ w^k=w k⁰²K¹

"

(

u

k +

u

k⁰)

:w

k⁰

It is simple to show that this is standard, and that⁸

i :

^G`

F

i =

E

i^f

E

¹

=w

^g. ²

Proposition 4

^If

^x

is action guarded in

E

and ^{G `}

E

=

F

then

x

is action guarded in

F

.

Proof

. Show that

AG

( ) is a model for the equational theory^G. ²

Proposition 5

We shall use the following standard results about substitution:

1.

G

^f

F=

^~

x

~^gf

E=w

^g

G

^f

E=w

^gf

F

^~f

E=w

^g

= x

~^g, if

w

does not occur in

x

~, and

x

~ are not free in

E

.

2.

F

^f

G=w

^gf

E=

^~

x

~^g

F

^f

G

^f

E=

^~

x

~^g

=w

^gf

E=

^~

x

~^g, if

x

~ are not free in ~

E

.

Proof

. Routine structural induction. ²

Theorem 6 (Equational Characterization)

For any

E

we can nd a stan- dard equation set

x

~ = ~

G

which

E

^G-provably satises. Moreover

E

and the equation set

x

~= ~

G

have the same free variables.

Proof

. An induction on

E

. The only dicult case is when

E

x

(

w

=

F

).

In this case, by induction we nd a ~

x

= ~

H

which

F

^G-provably satises, and wlog we can assume that

w

is not a formal variable of ~

x

= ~

H

, and that ~

x

are not free in

E

. Thus we have a ~

F

such that:

G`

F

¹ =

F

(2)

8

i :

^G`

F

i =

H

i^f

F=

~

x

~^g (3) Dene:

E

i

F

i^f

E=w

^g (4)

Let ~

G

be the standard equation set given by Proposition 3 such that:

G`

G

i=

H

i^f

H

¹

=w

^g (5) Since

w

is action guarded in

F

, by Proposition 4 it must be action guarded in

H

^1f

F=

^~

x

~^g, so, as

w

⁶²

x

~, must be action guarded in

H

¹, so cannot be free in

H

¹. Then:

G`

E

=

F

^f

E=w

^g (R1)

=

F

^1f

E=w

^g (2)

=

E

¹ (4)

and:

G `

E

¹

=

F

^1f

E=w

^g (4)

=

H

^1f

F=

^~

x

~^gf

E=w

^g (3)

=

H

^1f

E=w

^gf

F

^~f

E=w

^g

= x

~^g (Propn 5.1)

=

H

^1f

E=w

^gf

E=

^~

x

~^g (4)

=

H

^1f

E=

^~

x

~^g (

w

⁶²fv

H

¹)

and so:

G`

E

i

=

F

i^f

E=w

^g (4)

=

H

i^f

F=

~

x

~^gf

E=w

^g (3)

=

H

i^f

E=w

^gf

F

^~f

E=w

^g

= x

~^g (Propn 5.1)

=

H

i^f

E=w

^gf

E=

^~

x

~^g (4)

=

H

i^f

H

^1f

E=

^~

x

~^g

=w

^gf

E=

^~

x

~^g (above)

=

H

i^f

H

¹

=w

^gf

E=

^~

x

~^g (Propn 5.2)

=

G

i^f

E=

~

x

~^g (5)

Thus we have found a standard ~

x

= ~

G

which

E

^G-provably satises. ² Theorem 6 shows that every expression

E

in

TC

^G-provably satises a standard equation set ~

x

= ~

G

. The second stepping stone towards the promised complete- ness theorem is a result showing that if

E

F

, where

F

^G-provably satises a standard equation set ~

y

= ~

H

, then there exists a third standard equation set

E-provably satised by both

E

and

F

. Note that this part of the completeness proof requires the axioms (MP) and (P).

Theorem 7

^Let

^E

^and

^E

⁰ be expressions in

TC

^{such that}

^E

^E

^{0. Assume}

that

E

^E-provably satises a standard equation set

x

~ = ~

F

, and

E

^{0 E}-provably satises a standard equation set

x

~⁰= ~

F

⁰. Then there exists a standard equation set^E-provably satised by both

E

and

E

⁰.

Proof (Following Milner)

. Assume that:

F

i ^X

j²Jⁱ

"

(

t

j)

:a

j

:x

j+ ^X

k²Kⁱ

"

(

u

k)

::x

k+ ^X

l²Lⁱ

"

(

v

l)

:w

l (6)

F

_i^{00 X}

j⁰²Ji⁰ 0

"

(

t

⁰_j⁰)

:a

j⁰

:x

⁰_j⁰+ ^X

k⁰²Ki⁰ 0

"

(

u

⁰_k⁰)

::x

⁰_k⁰ + ^X

l⁰²L⁰i 0

"

(

v

⁰_l⁰)

:w

_l⁰⁰ (7) As

E

^E-provably satises ~

x

= ~

F

and

E

^{0 E}-provably satises ~

x

⁰ = ~

F

⁰, we can nd ~

E

and ~

E

⁰such that:

E

=

E

(8)

8

i :

^{E `}

E

i =

F

i^f

E=

~

x

~^g (9)

E `

E

⁰ =

E

¹⁰ (10)

8

i :

^{E `}

E

_i⁰ =

F

_i^0f

E

^~0

= x

~^0g (11) Let ~

w

denote the set of free variables occurring in either

E

or

E

⁰. Choose a vector ~

a

of distinct actions, one action

a

w for each

w

²

w

~, that do not occur in

E

and

E

⁰. (This is always possible as the set of action names is countably innite.) Take the vector ~

P

of processes given by

P

w

a

w

: 0

^{. As}

^E

^E

^{0, it}

follows, in particular, that

E

^f

P=

^~

w

~^g

E

^0f

P=

^~

w

~^g. Thus, by (8) and (10), we have that

E

^1f

P=

^~

w

~^g

E

^10f

P=

^~

w

~^g.

Let ^R be the relation ^f(

ii

⁰)^j

E

i^f

P=

~

w

~^g

E

_i^00f

P=

^~

w

~^gg, let ~

z

be the vector of fresh variables ^f

z

ii^{0 j}

i

^R

i

^0g (with

z

¹¹ as leading variable), and dene the vectors ~

G

, ~

H

and ~

H

⁰ as:

G

ii^{0 X} j²Jⁱj⁰²Jⁱ⁰⁰ j^Rj⁰a^j=a^0j0

"

(

t

j ^_

t

⁰_j⁰)

:a

j

:z

jj⁰+^X

k²Kⁱk²Kⁱ⁰⁰ k^Rk⁰

"

(

u

k ^_

u

⁰_k⁰)

::z

kk⁰+^X

l²Lⁱl⁰²L⁰ⁱ⁰ w^l=w^0l0

"

(

v

l^_

v

_l⁰⁰)

:w

l(12)

H

ii⁰

E

i (13)

H

_ii⁰⁰

E

_i⁰⁰ (14)

Note that the equation set ~

z

= ~

G

is standard by construction. We now show that the vector ~

H

^E-provably satises ~

z

= ~

G

. To this end, we prove, rst of all, that, for each

i

^R

i

⁰, every summand of

G

ii^0f

H=

~

z

~^g can be absorbed into

H

ii⁰. We consider three cases, depending on the form taken by the summand of

G

ii^0f

H=

~

z

~^g.

For any

i

^R

i

⁰,

j

²

J

i and

j

⁰²

J

_i⁰⁰ such that

j

^R

j

⁰ and

a

j =

a

⁰_j⁰:

E`

H

ii⁰

=

E

i (13)

=

F

i^f

E=

~

x

~^g (9)

=

F

i^f

E=

~

x

~^g+

"

(

t

j)

:a

j

:E

j (S1{S3,6)

=

F

i^f

E=

~

x

~^g+

"

(

t

j)

:

(

a

j

:E

j+

"

((

t

j^_

t

⁰_j⁰)^;

t

j)

:a

j

:E

j) (P)

=

F

i^f

E=

~

x

~^g+

"

(

t

j)

:a

j

:E

j+

"

(

t

j)

:"

((

t

j^_

t

⁰_j⁰)^;

t

j)

:a

j

:E

j (TD)

=

F

i^f

E=

~

x

~^g+

"

(

t

j)

:a

j

:E

j+

"

(

t

j+ ((

t

j^_

t

⁰_j⁰)^;

t

j))

:a

j

:E

j (TA)

=

F

i^f

E=

~

x

~^g+

"

(

t

j)

:a

j

:E

j+

"

(

t

j^_

t

⁰_j⁰)

:a

j

:E

j (

t

+ (

u

^;

t

) =

u

)

=

F

i^f

E=

~

x

~^g+

"

(

t

j^_

t

⁰_j⁰)

:a

j

:E

j (S1{S3,6)

=

E

i+

"

(

t

j^_

t

⁰_j⁰)

:a

j

:E

j (9)

=

H

ii⁰+

"

(

t

j ^_

t

⁰_j⁰)

:a

j

:H

jj⁰ (13)

=

H

ii⁰+

"

(

t

j ^_

t

⁰_j⁰)

:a

j

:z

jj^0f

H=

~

z

~^g (substitution) Similarly, for any

i

^R

i

⁰,

k

²

K

i and

k

⁰²

K

_i⁰⁰ such that

k

^R

k

⁰:

E `

H

ii⁰ =

H

ii⁰ +

"

(

u

k ^_

u

⁰_k⁰)

::z

kk^0f

H=

~

z

~^g and for any

i

^R

i

⁰,

l

²

L

i and

l

⁰²

L

⁰_i⁰ such that

w

l=

w

⁰_l⁰:

E`

H

ii⁰ =

H

ii⁰+

"

(

v

l^_

v

_l⁰⁰)

:w

l^f

H=

~

z

~^g

We remark here that the proof of the above equality makes an essential use of axiom (P), and could not have been carried out using Wang's persistency axioms (AP) and (NP).

Thus each summand of

G

ii^0f

H=

~

z

~^g can be absorbed into

H

ii⁰, and by (S1){

(S4):

E`

H

ii⁰ =

H

ii⁰+

G

ii^0f

H=

~

z

~^g (15) We now show that the converse also holds, namely that

H

ii⁰ can be absorbed into

G

ii^0f

H=

~

z

~^g. To this end, by (9) and (13), it is sucient to prove that each summand of

F

i^f

E=

~

x

~^g can be absorbed into

G

ii^0f

H=

~

z

~^g. Again, we distinguish three cases depending on the form the summand takes.

For any

i

^R

i

⁰ and

j

²

J

i, either:

t

j

u

k, for every

k

²

K

i, or:

there exists

k

²

K

i such that

t

j

> u

k. We proceed to show that in either case:

E `

G

ii^0f

H=

~

z

~^g=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:x

j^f

E=

~

x

~^g

Case ⁸

k

²

K

i

: t

j

u

k. In this case, by the operational semantics for

TC

⁰, it follows that:

F

i^f

E=

~

x

~^gf

P=

^~

w

~^{g;";(t!j);a!j}

E

j^f

P=

~

w

~^g

As

E

i^f

P=

~

w

~^g

E

_i^00f

P=

^~

w

~^gand ^G is sound for, we have that

F

i^f

E=

~

x

~^gf

P=

^~

w

~^g

F

_i^00f

E=

^~

x

~^0gf

P=

^~

w

~^g

So, as the actions in ~

a

were chosen to be fresh:

F

_i^00f

E

^~0

= x

~^0gf

P=

^~

w

~^{g;"(;t!j);a!j}

E

_j^00f

P=

^~

w

~^g

for some

j

⁰ with

t

j

t

⁰_j⁰,

a

j =

a

⁰_j⁰ and

E

j^f

P=

~

w

~^g

E

_j^00f

P=

^~

w

~^g. By the denition of the relation^R, it follows that

j

^R

j

⁰. Thus:

E`

G

ii^0f

H=

~

z

~^g

=

G

ii^0f

H=

~

z

~^g+

"

(

t

j^_

t

⁰_j⁰)

:a

j

:H

jj⁰ (S1{S3,12)

=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:H

jj⁰ (

t

j

t

⁰_j⁰)

=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:E

j (13)

=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:x

j^f

E=

~

x

~^g (substitution)

Case ⁹

k

²

K

i

: t

j

> u

k. Choose

k

such that

u

k is minimal in the set

f

u

h ^j

h

²

K

i^g. Then, by the operational semantics for

TC

⁰:

F

i^f

E=

~

x

~^gf

P=

^~

w

~^g;";(u;k!);!

E

k^f

P=

~

w

~^g Therefore, as in the previous case, we have:

F

_i

E

^~

= x

~

P=

^~

w

~ ^{"(u )}

E

_k

P=

^~

w

~

for some

k

^{0 2}

K

_i⁰⁰ with

u

k

u

⁰_k⁰ and

k

^R

k

⁰. In fact, by symmetry and the fact that

u

k is minimal in the set ^f

u

h ^j

h

²

K

i^g, it is easy to see that

u

k =

u

⁰_k⁰. Thus:

E`

G

ii^0f

H=

~

z

~^g

=

G

ii^0f

H=

~

z

~^g+

"

(

u

k^_

u

⁰_k⁰)

::H

kk⁰ (S1{S3,12)

=

G

ii^0f

H=

~

z

~^g+

"

(

u

k)

::H

kk⁰ (

u

k =

u

⁰_k⁰)

=

G

ii^0f

H=

~

z

~^g+

"

(

u

k)

:

(

:H

kk⁰+

"

(

t

j ^;

u

k)

:a

j

:H

jj⁰) (MP,

t

j

> u

k)

=

G

ii^0f

H=

~

z

~^g+

"

(

u

k)

::H

kk⁰+

"

(

u

k)

:"

(

t

j ^;

u

k)

:a

j

:H

jj⁰ (TD)

=

G

ii^0f

H=

~

z

~^g+

"

(

u

k)

::H

kk⁰+

"

(

u

k+ (

t

j^;

u

k))

:a

j

:H

jj⁰ (TA)

=

G

ii^0f

H=

~

z

~^g+

"

(

u

k)

::H

kk⁰+

"

(

t

j)

:a

j

:H

jj⁰ (

t

+ (

u

^;

t

) =

u

)

=

G

ii^0f

H=

~

z

~^g+

"

(

u

k^_

u

⁰_k⁰)

::H

kk⁰+

"

(

t

j)

:a

j

:H

jj⁰ (

u

k =

u

⁰_k⁰)

=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:H

jj⁰ (S1{S3,12)

=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:E

j (13)

=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:x

j^f

E=

~

x

~^g (substitution) Note that the above reasoning uses the equation (MP).

Thus:

E `

G

ii^0f

H=

~

z

~^g=

G

ii^0f

H=

~

z

~^g+

"

(

t

j)

:a

j

:x

j^f

E=

~

x

~^g

Similarly, for any

i

^R

i

⁰and

k

²

K

i, it is not too dicult to prove that:

E`

G

ii^0f

H=

~

z

~^g=

G

ii^0f

H=

~

z

~^g+

"

(

u

k)

::x

k^f

E=

~

x

~^g We are now left to show that for any

i

^R

i

⁰ and

l

²

L

i:

E`

G

ii^0f

H=

~

z

~^g=

G

ii^0f

H=

~

z

~^g+

"

(

v

l)

:w

l^f

E=

~

x

~^g (16) As before, we prove this statement by considering the following two sub-cases:

v

l

u

k, for every

k

²

K

i, or:

there exists

k

²

K

i such that

v

l

> u

k.

The proof of (16) when there exists

k

²

K

i such that

v

l

> u

k follows the lines spelled out in detail above. We shall thus concentrate on presenting a detailed proof of (16) in the case

v

l

u

k, for every

k

²

K

i.

Assume that

l

²

L

i and that

v

l

u

k, for every

k

²

K

i. We claim that there exists

l

^{0 2}

L

⁰_i⁰ such that

v

_l⁰⁰

v

l and

w

l =

w

_l⁰⁰. To see that this is indeed the case, note that, by (9), (11) and the soundness of^E:

F

i^f

E=

~

x

~^gf

P=

^~

w

~^g

F

_i^00f

E

^~0

= x

~^0gf

P=

^~

w

~^g (17) As

l

²

L

iand

v

l

u

k, for every

k

²

K

i, it follows that

F

i^f

E=

~

x

~^gf

P=

^~

w

~^{g;";(v!l);a;w!l}. By (17) and the fact that

a

w^l does not occur in

F

_i^00f

E

^~0

= x

~^0g, we then have that

F

_i^00f

E

^~0

= x

~^0gf

P=

^~

w

~^{g ;";(v!l);a;w!l} hence, for some

l

^{0 2}

L

⁰_i⁰, we have

v

_l⁰⁰

v

l and

w

_l⁰⁰ =

w

l as claimed.