2.4　Truly Concurrent Process Algebra with Localities

2.4.1　Operational Semantics with Localities

Definition 2.35 （Prime event structure with silent event）.Let Λ be afixed set of labels，ranging over a，b，c，··· and τ .A（ Λ -labelled）prime event structure with silent event τ is a tuple E =〈E，≤， ♯，λ 〉，where E is a denumerable set of events，including the silent event τ .Let =E \｛τ｝，exactly excluding τ .It is obvious that = ∊ ，where ∊ represents the empty event.Let λ ：E Λ be a labelling function and let λ （ τ ）= τ .≤， ♯ are binary relations on E，called causality and conflict respectively，such that：

（1）≤is a partial order and 「e =｛ e' ∈E| e' ≤ e ｝is finite for all e ∈E.It is easy to see that e ≤ τ ^⋆ ≤ e' = e ≤ τ ≤ ···≤ τ ≤ e' ，then e ≤ e' .

（2） ♯ is irreflexive，symmetric and hereditary with respect to≤，that is，for all e，e'，e ^'' ∈E，if e♯e' ≤ e ^'' ，then e♯e ^'' .

Then，the concepts of consistency and concurrency can be drawn from the above definition：

（1） e，e' ∈E are consistent，denoted e ⌒ e' ，if¬（ e ♯ e' ）.A subset X ⊆E is called consistent，if e ⌒ e' for all e，e' ∈ X .

（2） e，e' ∈E are concurrent，denoted as e‖e' ，if ¬（ e ≤ e' ）， ¬（ e' ≤ e ），and ¬（ e♯e' ）.

Definition 2.36 （Con figuration）.Let E be a PES.A（finite）configuration in E is a（finite）consistent subset of events C⊆E ，closed with respect to causality（i.e. 「C = C ）.The set of finite configurations of E is denoted by C （ E ）.We let = C\｛τ ｝.

A consistent subset X⊆ E of events can be seen as apomset.Given X，Y⊆ E， ～ if and are isomorphic as pomsets.In the following of the paper，when we say C ₁ ～C ₂ ，we mean ～ .

Definition 2.37 （Pomset transitions and steps）.Let E be a PES， C ∈ C （ E ），and∅ /= X⊆ E.If C∩X =∅and C' =C∪X∈ C （ E ），then C C' is called a pomset transition from C to C' .When the events in X are pairwise concurrent，we say that C C' is a step.

Definition 2.38 （Posetal product）.Given two PESs E ₁ and E ₂ ，the posetal product of their conf igurations，denoted C （ E ₁ ） C （ E ₂ ），is defined as

｛（ C ₁ ， f，C ₂ ）| C ₁ ∈ C （ E ₁ ）， C ₂ ∈ C （ E ₂ ）， f ： C ₁ C ₂ isomorphism ｝.

A subset R ⊆ C （ E ₁ ） ×C （ E ₂ ）is called a posetal relation.We say that R is downward closed when for any（ C ₁ ， f，C ₂ ），（ ， f'， ）∈ C （ E ₁ ） C （ E ₂ ），if（ C ₁ ， f，C ₂ ） ⊆ （ ， f'， ）pointw isely and（ ， f'， ）∈ R ，then（ ， f， ）∈ R .

For f ： X ₁ X ₂ ，we define f ［ x ₁ x ₂ ］： X ₁ ∪｛ x ₁ ｝ X ₂ ∪｛ x ₂ ｝， z ∈ X ₁ ∪｛ x ₁ ｝as follows：① f ［ x ₁ x ₂ ］（ z ）= x ₂ ，if z = x ₁ ；② f ［ x ₁ x ₂ ］（ z ）= f （ z ），otherw ise，where X ₁ ⊆ E ₁ ， X ₂ ⊆ E ₂ ， x ₁ ∈E ₁ ， x ₂ ∈E ₂ .

Let Loc be the set of locations，and u，v ∈Loc ^⋆ .Let ≪be the sequential ordering on Loc ^⋆ ，we call v is an extension or a sublocation of u in u≪v ；and if u/≪v v/≪u ，then u and v are independent and denoted u◇v .

Definition 2.39 （Consistent location association）.A relation φ⊆ （Loc ^{⋆ ×} Loc ^⋆ ）is a Consistent Location Association（CLA），if（ u，v ）∈ φ ＆（ u'，v' ）∈ φ ，then u ◇ u' ⇔ v ◇ v' .

Definition 2.40 （Static location pomset，step bisimulation）.Let E ₁ and E ₂ be PESs.A static location pomset bisimulation is a relation R _φ ⊆C （ E ₁ ） ×C （ E ₂ ），such that if（ C ₁ ， C ₂ ）∈ R _φ and X ₁ ～X ₂ and（ ， ）∈ R _{φ∪｛ （ u，v ）｝} ，and vice-versa.We say that E ₁ and E ₂ are static ，then ，where X ₁ ⊆ E ₁ ， X ₂ ⊆ E ₂ ，location pomset bisimilar，written by E ₁ E ₂ ，if there existsa static location pomset bisimulation R _φ ，such that（∅，∅）∈ R _φ .By replacing pomset transitions with steps，we can get the def inition of static location step bisimulation.When PESs E ₁ and E ₂ are static location step bisimilar，we w rite E ₁ E ₂ .

Definition 2.41 （Static location（hereditary）history-preserving bisimulation）.A static location history-preserving（hp-）bisimulation is a posetal relation R _φ ⊆C （ E ₁ ） ×C （ E ₂ ），such that if（ C ₁ ， f，C ₂ ）∈ R _φ and ，then ，where（ ， f ［ e ₁ e ₂ ］， ）∈ R _{φ∪｛ （ u，v ）｝} ，and vice-versa. E ₁ and E ₂ are static location history-preserving（hp-）bisimilar，written by if there exists a static location hp-bisimulation R _φ such that（∅，∅，∅）∈ R _φ .

A static location hereditary history-preserving（hhp-）bisimu lation is a downward closed static location hp-bisimulation. E ₁ and E ₂ are static location hereditary history preserving（hhp-）bisimilar，written by .

Definition 2.42 （Weak static location pomset，step bisimulation）.Let E ₁ and E ₂ be PESs.A weak static location pomset bisimulation is a relation R _φ ⊆C （ E ₁ ） ×C （ E ₂ ），such that if（ C ₁ ， C ₂ ）∈ R _φ and ，then ，where X ₁ ⊆ ˆE ₁ ， X ₂ ⊆ ， X ₁ ～X ₂ ，（ ， ）∈ R _{φ∪｛ （ u，v ）｝} ，and vice-versa.We say that E ₁ and E ₂ are weak static location pomset bisimilar，written by ，if there exists a weak static location pomset bisimulation R _φ ，such that（∅，∅）∈ R _φ .By replacing weak pomset transitions with weak steps，we can get the def inition of weak static location step bisimulation.When PESs E ₁ and E ₂ are weak static location step bisimilar，we w rite .

Definition 2.43 （Weak static location（hereditary）history-preserving bisimulation）.A weak static location history-p reserving（hp-）bisimu lation is a weakly posetal relation R _φ ⊆C （ E ₁ ） C （ E ₂ ）such that if（ C ₁ ， f，C ₂ ）∈ R _φ ，and ，then ， with（ ， f ［ e ₁ e ₂ ］， ）∈ R _{φ∪｛ （ u，v ）｝} ，and vice-versa. E ₁ and E ₂ are weak static location history-preserving（hp-）bisimilar and are written by if there exists a weak static location hp-bisimulation R _φ such that（∅，∅，∅）∈ R _φ .

A weak static location hereditary history-preserving（hhp-）bisimulation is a downward closed weak static location hp-bisimulation. E ₁ and E ₂ are weak static location hereditary history-p reserving（hhp-）bisimilar and are written by .

Definition 2.44 （Branching static location pomset，step bisimulation）.Assume a special term ination predicate ，and let √ represent a state with √ .Let E ₁ and E ₂ be PESs.A branching static location pomset bisimulation is a relation R _φ ⊆C （ E ₁ ） ×C （ E ₂ ），such that：

（1）If（ C ₁ ， C ₂ ）∈ R _φ and ，then

① X≡τ ^⋆ and（ ， C ₂ ）∈ R _φ ；

②There is a sequence of（zero or m ore） τ -transitions ，such that（ C ₁ ， ）∈ R _φ and with （ ， ）∈ R _φ∪ ｛ _{（ u，v ）｝} .

（2）If（ C ₁ ， C ₂ ）∈ R _φ and ，then

① X≡τ ^⋆ ，and（ C ₁ ， ）∈ R _φ ；

②There is a sequence of（zero or more） τ -transitions ，such that（ ， C ₂ ）∈ R _φ and with（ ， ）∈ R _{φ∪｛ （ u，v ）｝} .

（3）If（ C ₁ ， C ₂ ）∈ R _φ and C ₁ ，then there is a sequence of（zero or m ore） τ transitions such that（ C ₁ ， ）∈ R _φ and .

（4）If（ C ₁ ， C ₂ ）∈ R _φ and C ₂ ，then there is a sequence of（zero or more） τ transitions such that（ ， C ₂ ）∈ R _φ and .We say that E ₁ and E ₂ are branching static location pomset bisimilar，written by ，if there exists a branching static location pomset bisimulation R _φ ，such that（∅，∅）∈ R _φ .

By replacing pomset transitions with steps，we can get the def inition of branching static location step bisimulation.When PESs E ₁ and E ₂ are branching static location step bisimilar，wew rite .

Definition 2.45 （Rooted branching static locationpomset，step bisimulation）.Assume a special term ination predicate ，and let √ represent a state with √ .Let E ₁ and E ₂ be PESs.A rooted branching static location pomset bisimulation is a relation R _φ ⊆C （ E ₁ ） ×C （ E ₂ ），such that：

（1）If（ C ₁ ， C ₂ ）∈ R _φ and ，then with .

（2）If（ C ₁ ， C ₂ ）∈ R _φ and ，then with .

（3）If（ C ₁ ， C ₂ ）∈ R _φ and C ₁ ，then C ₂ .

（4）If（ C ₁ ， C ₂ ）∈ R _φ and C ₂ ，then C ₁ .

We say that E ₁ and E ₂ are rooted branching static location pomset bisimilar，written by ，if there exists a rooted branching static location pomset bisimulation R _φ ，such that（∅，∅）∈ R _φ .

By replacing pomset transitions with steps，we can get the def inition of rooted branching static location step bisimulation.When PESs E ₁ and E ₂ are rooted branching static location step bisimilar，wew rite .

Definition 2.46 （Branching static location（hereditary）history-preserving bisimulation）.Assume a special termination predicate ，and let √ represent a state with √ .A branching static location history-preserving（hp-）bisimulation is a posetal relation R _φ ⊆C （ E ₁ ） C （ E ₂ ）such that：

（1）If（ C ₁ ， f，C ₂ ）∈ R and ，then

① e ₁ ≡τ，and（ ， f ［ e ₁ τ ］， C ₂ ）∈ R _φ ；

②There is a sequence of（zero or m ore） τ -transitions ，such that（ C ₁ ， f， ）∈ R _φ and with（ ， f ［ e ₁ e ₂ ］， ）∈ R _{φ∪｛ （ u，v ）｝} .

（2）If（ C ₁ ， f，C ₂ ）∈ R _φ and ，then

① X≡τ，and（ C ₁ ， f ［ e ₂ τ ］， ）∈ R _φ ；

② There is a sequence of（zero or m ore） τ -transitions ，such that （ ， f，C ₂ ）∈ R _φ and with（ ， f ［ e ₂ e ₁ ］， ）∈ R _{φ∪｛ （ u，v ）｝} .

（3）If（ C ₁ ， f，C ₂ ）∈ R _φ and C ₁ ，then there is a sequence of（zero or more） τ -transitions such that（ C ₁ ， f， ）∈ R _φ and .

（4）If（ C ₁ ， f，C ₂ ）∈ R _φ and C ₂ ，then there is a sequence of（zero or more） τ -transitions such that（ ， f，C ₂ ）∈ R _φ and .

E ₁ and E ₂ are branching static location history-preserving（hp-）bisimilar and are written by ，if there exists a branching static location hp-bisimulation R _φ such that（∅，∅，∅）∈ R _φ .

A branching static location hereditary history-p reserving（hhp-）bisimulation is a downward closed branching static location hhp-bisimulation. E ₁ and E ₂ are branching static location hereditary history-preserving（hhp-）bisimilar，arewritten by E ₁ ≈ E 2.

Definition 2.47 （Rooted branching static location（hereditary）history-preserving bisimulation）.Assume a special term ination predicate ，and let √ represent a state with √ .A rooted branching static location history-preserving（hp-）bisimulation is a posetal relation R _φ ⊆C （ E ₁ ） C （ E ₂ ）such that：

（1）If（ C ₁ ， f，C ₂ ）∈ R _φ and ，then with .

（2）If（ C ₁ ， f，C ₂ ）∈ R _φ and ，then with .

（3）If（ C ₁ ， f，C ₂ ）∈ R _φ and C ₁ ，then C ₂ .

（4）If（ C ₁ ， f，C ₂ ）∈ R _φ and C ₂ ，then C ₁ .

E ₁ and E ₂ are rooted branching static location history-p reserving（hp-）bisimilar and are written by ，if there exists a rooted branching static location hp-bisimulation R _φ such that（∅，∅，∅）∈ R _φ .

A rooted branching static location hereditary history-preserving（hhp-）bisimulation is a downward closed rooted branching static location hp-bisimulation. E ₁ and E ₂ are rooted branching static location hereditary history-preserving（hhp-）bisimilar，and are written by .

2.4.2　BATC with Localities

Let Loc be the set of locations，and loc∈Loc， u，v ∈Loc ^⋆ ， ∊ represents an empty location.A distribution allocatesa location u ∈Loc ^⋆ to an action e denoted as u e ，or to a process x denoted as u x .

In the following，let e ₁ ， e ₂ ， ， ∈E，and let variables x，y，z range over the set of terms for true concurrency，and p，q，s range over the set of closed terms.The set of axioms of BATC with static localities（BATC ^sl ）consists of the laws are given in Table 2.9.

Definition 2.48 （Basic terms of BATC with static localities）.The set of basic terms of BATC with static localities， B （BATC ^sl ），is inductively defined as follows：

（1）E ⊂B （BATC ^sl ）.

（2）If u ∈Loc ^⋆ and t ∈ B （BATC ^sl ），then u t ∈ B （BATC ^sl ）.

（3）If e ∈E and t ∈ B （BATC ^sl ），then e·t∈ B （BATC ^sl ）.

（4）If t，s∈ B （BATC ^sl ），then t + s ∈ B （BATC ^sl ）.

Theorem 2.37 （Elimination theorem of BATC with static localities）.Let p be a closed BATC with static localities term.Then there is a basic BATC with static localities term q such that BATC ^sl ├ p = q .

In this subsection，we will define a term-deduction system that provides the operational semantics of BATC with static localities.We present the operational transition rules for the operators·and+as follows.The predicate √ represents successful term ination after execution of the event e at location u .

Theorem 2.38 （Congruence of BATC with static localities with respect to static location pomset bisimulation equivalence）.Static location pomset bisimulation equivalence is a congruence with respect to BATC with static localities.

Theorem 2.39 （Soundness of BATC with static localities modulo static location pomset bisimulation equivalence）.Let x and y be BATC with static localities terms.If BATC ^sl ├ x = y ，then x y .

Theorem 2.40 （Completeness of BATC with static localities modulo static location pomset bisimulation equivalence）.Let p and q be closed BATC with static localities terms.If p q ，then p = q .

Theorem 2.41 （Congruence of BATC with static localities with respect to static location step bisimulation equivalence）.Static location step bisimulation equivalence is a congruence with respect to BATC with static localities.

Theorem 2.42 （Soundness of BATC with static localities modulo static location step bisimulation equivalence）.Let x and y be BATC with static localities terms.If BATC ^sl ├ x = y ，then x y .

Theorem 2.43 （Completeness of BATC with static localities modulo static location step bisimulation equivalence）.Let p and q be closed BATC with static localities terms.If p q ，then p = q .

Theorem 2.44 （Congruence of BATC with static localities with respect to static location hp-bisimulation equivalence）.Static location hp-bisimulation equivalence is a congruence with respect to BATC with static localities.

Theorem 2.45 （Soundness of BATC with static localities modulo static location hp-bisimulation equivalence）.Let x and y be BATC with static localities terms.If BATC ├ x = y ，then x y .

Theorem 2.46 （Completeness of BATC with static localities modulo static location hp-bisimulation equivalence）.Let p and q be closed BATC with static localities terms.If p q ，then p = q .

Theorem 2.47 （Congruence of BATC with static localities with respect to static location hhp-bisimulation equivalence）.Static location hhp-bisimulation equivalence is a congruence with respect to BATC with static localities.

Theorem 2.48 （Soundness of BATC with static localities modulo static location hhp-bisimulation equivalence）.Let x and y be BATC with static localities terms.If BATC ├ x = y ，then x y .

Theorem 2.49 （Completeness of BATC with static localities modulo static location hhp-bisimulation equivalence）.Let p and q be closed BATC with static localities terms.If p q ，then p = q .

2.4.3　APTC with Localities

We provide the transition rules for APTC with static localities as follows.Where≬represents the whole concurrency operator，‖represents the parallel operator， represents the left parallel operator，|represents the communication merge， Θ represents the conflicts elimination operator，and ◁ represents the auxiliary unless operator.

In the following，wewill show that the elimination theorem does not hold for truly concurrent processes combined with the operators·，+，and .Firstly，we will define the basic terms for APTC with static localities.

Definition 2.49 （Basic terms of APTC with static localities）.The set of basic terms of APTC with static localities， B （APTC ^sl ），is inductively defined as follows：

（1）E ⊂B （APTC ^sl ）.

（2）If u ∈Loc ^⋆ and t ∈ B （APTC ^sl ），then u t ∈ B （APTC ^sl ）.

（3）If e ∈E and t ∈ B （APTC ^sl ），then e·t∈ B （APTC ^sl ）.

（4）If t，s∈ B （APTC ^sl ），then t + s ∈ B （APTC ^sl ）.

（5）If t，s∈ B （APTC ^sl ），then t ‖- s ∈ B （APTC ^sl ）.

Theorem 2.50 （Congruence theorem of APTC with static localities）.Static location truly concurrent bisimulation equivalences ，and are all congruences with respect to APTC with static localities.

So，we design the axioms of parallelism in Table 2.10.These axioms include algebraic laws for the parallel operator‖，the communication operator|，the con f lict elimination operator Θ ，the unless operator ◁ ，and the whole parallel operator≬.The communication between two communicating events in different parallel branches may cause dead lock（a state of inactivity），which is caused by m ismatch of two communicating events or the im perfectness of the communication channel.We introduce a new constant δ to denote the dead lock，and let theatomic event e ∈E∪｛ δ ｝.

Based on the def inition of basic terms for APTC with static localities（see Definition 2.49）and axioms of parallelism（see Table 2.10），we can prove the elimination theorem of parallelism.

Theorem 2.51 （Elimination theorem of parallelism）.Let p be a closed APTC with static localities term.Then there is a basic APTC with static localities term q such that APTC ^sl ├ p = q .

Theorem 2.52 （Generalization of APTC with static localities with respect to BATC with static localities）.APTC with static localities is a generalization of BATC with static localities.

Theorem 2.53 （Soundness of APTC with static localities modulo static location pomset bisimulation equivalence）.Let x and y be APTC with static localities terms.If APTC ^sl ├ x = y ，then x y .

Theorem 2.54 （Completeness of APTC with static localities modulo static location pomset bisimulation equivalence）.Let p and q be closed APTC with static localities terms.If p q ，then p = q .

Theorem 2.55 （Soundness of APTC with static localities modulo static location step bisimulation equivalence）.Let x and y be APTC with static localities terms.If APTC ^sl ├ x = y ，then x y .

Theorem 2.56 （Completeness of APTC with static localities modulo static location step bisimulation equivalence）.Let p and q be closed APTC with static localities terms.If p q ，then p = q .

Theorem 2.57 （Soundness of APTC with static localities modulo static location hp-bisimulation equivalence）.Let x and y be APTC with static localities terms.If APTC ^sl ├ x = y ，then x y .

Theorem 2.58 （Completeness of APTC with static localities modulo static location hp-bisimulation equivalence）.Let p and q be closed APTC with static localities terms.If p q ，then p = q .

Theorem 2.59 （Soundness of APTC with static localities modulo static location hhp-bisimulation equivalence）.Let x and y be APTC with static localities terms.If APTC ^sl ├ x = y ，then x y .

Theorem 2.60 （Completeness of APTC with static localities modulo static location hhp-bisimulation equivalence）.Let p and q be closed APTC with static localities terms.If p q ，then p = q .

The transition rules for encapsulation operator ∂ _H are shown as follows：

Based on the transition rules for the encapsulation operator ∂ _H ，we design the axioms as Table 2.11 shows.

Theorem 2.61 （Congruence theorem of encapsulation operator ∂ _H ）.Static location truly concurrent bisimulation equivalences ，and areall congruences with respect to the encapsulation operator ∂ _H .

Theorem 2.62 （Elimination theorem of APTC with static localities）.Let p be a closed APTC with static localities term including the encapsulation operator ∂ _H .Then there is a basic APTC with static localities term q such that APTC ├ p = q .

Theorem 2.63 （Soundness of APTC with static localities modulo static location pomset bisimulation equivalence）.Let x and y be APTC with static localities terms including the encapsulation operator ∂ _H .If APTC ^sl ├ x = y ，then x y .

Theorem 2.64 （Completeness of APTC with static localities modulo static location pomset bisimulation equivalence）.Let p and q be closed APTC with static localities terms including the encapsulation operator ∂ _H .If p q ，then p = q .

Theorem 2.65 （Soundness of APTC with static localities modulo static location step bisimulation equivalence）.Let x and y be APTC with static localities terms including the encapsulation operator ∂ _H .If APTC ^sl ├ x = y ，then x y .

Theorem 2.66 （Completeness of APTC with static localities modulo static location step bisimulation equivalence）.Let p and q be closed APTC with static localities terms including the encapsulation operator ∂ _H .If p q ，then p = q .

Theorem 2.67 （Soundness of APTC with static localities modulo static location hp-bisimulation equivalence）.Let x and y be APTC with static localities terms including the encapsulation operator ∂ _H .If APTC ^sl ├ x = y ，then x y .

Theorem 2.68 （Completeness of APTC with static localities modulo static location hp-bisimulation equivalence）.Let p and q be closed APTC with static localities terms including the encapsulation operator ∂ _H .If p q ，then p = q .

Theorem 2.69 （Soundness of APTC with static localities modulo static location hhp-bisimulation equivalence）.Let x and y be APTC with static localities terms including the encapsulation operator ∂ _H .If APTC ^sl ├ x = y ，then x y .

Theorem 2.70 （Completeness of APTC with static localities modulo static location hhp-bisimulation equivalence）.Let p and q be closed APTC with static localities terms including the encapsulation operator ∂ _H .If p q ，then p = q .

2.4.4　Recursion with Localities

In this section，we introduce recursion to capture infinite processes based on APTC with static localities.Since in APTC with static localities has four basic operators， ，·，+，and ，then the recursion must be adapted this situation to include .

In the following，we use E，F，G to represent recursive specifications，and X，Y，Z to denote recursive variables.

Definition 2.50 （Recursive specification）.A recursive specification is a finite set of recursive equations：

where the left-hand sides X _i are called recursive variables，and the right-hand sides t _i （ X ₁ ，···， X _n ）are process terms in APTC with static localities with possible occurrences of the recursive variables X ₁ ，···， X _n .

Definition 2.51 （Solution）.Processes p ₁ ，···， p _n area solution for a recursive specification｛ X _i = t _i （ X ₁ ，···， X _n ）| i ∈｛1，···， n ｝｝［with respect to static location truly concurrent bisimulation equivalences ］if t _i （ p ₁ ，···， p _n ）for i ∈｛1，···， n ｝.

Definition 2.52 （Guarded recursive specification）.A recursive specification：is guarded if the right-hand sides of its recursive equations can be adapted to the following form，by applying the axioms in APTC with static localities and replacing recursive variables with the right-hand sides of their recursive equations：

where a ₁₁ ，···， ， a _{k 1} ，···， ， b ₁₁ ，···， ， ，···， ∈E，and the sum above is allowed to be empty，in which case it represents the dead lock δ .

Definition 2.53 （Linear recursive specification）.A recursive specification is linear if its recursive equations are of the form

where a ₁₁ ，···， a _{1 i 1} ， a _{k 1} ，···， a _kik ， b ₁₁ ，···， b _{1 j 1} ， b _{1 j 1} ，···， b _ljl ∈E，and the sum above is allowed to be empty，in which case it represents the dead lock δ .

For a guarded recursive specifications E with the form：

The behavior of the solution〈 X _i | E 〉for the recursive variable X _i in E ，where i ∈｛1，···， n ｝，isexactly the behavior of their right-hand sides t _i （ X ₁ ，···， X _n ），which is captured by the two transition rules as follows：

Theorem 2.71 （Conservativity of APTC with static localities and guarded recursion）.APTC with static localities and guarded recursion is a conservative extension of APTC with static localities.

Theorem 2.72 （Congruence theorem of APTC with static localities and guarded recursion）.Static location truly concurrent bisimulation equivalences ，and are all congruences with respect to APTC with static localities and guarded recursion.

The RDP（Recursive Definition Princip le）and the RSP（Recursive Specification Principle）are shown in Table 2.12.

Theorem 2.73 （Elimination theorem of APTC with static localities and linear recursion）.Each process term in APTC with static localities and linear recursion is equal to a process term〈 X ₁ | E 〉 with E being a linear recursive specification.

Theorem 2.74 （Soundness of APTC with static localities and guarded recursion）.Let x and y be APTC with static localities and guarded recursion terms.If APTC with guarded recursive ├ x = y ，then

（1） .

（2） .

（3） .

（4） .

Theorem 2.75 （Completeness of APTC with static localities and linear recursion）.Let p and q be closed APTC with static localities and linear recursion terms，then

（1）If p q ，then p = q .

（2）If p q ，then p = q .

（3）If p q ，then p = q .

（4）If p q ，then p = q .

2.4.5　Abstraction with Localities

To abstract away from the internal implementations of a program，and verify that the program exhibits the desired external behaviors，we introduce the silent step τ （dlistinguished as τ ^e ）and the abstraction operator τ _I ，where I⊆ E denotes the internal events.The silent step τ represents internal events，when we consider the external behaviors of a process， τ events can be removed，that is， τ events must keep silent.The transition rule for τ is shown as follows.In the following，we let theatomic event e range over E∪｛δ｝∪｛τ｝，and let the communication function γ ：E∪｛ τ｝× E∪｛ τ ｝ E∪｛ δ ｝，where each communication involved τ resulting into δ .

The silent step τ is introduced as anatomic event in E .Considering the recursive specification X =τX， τs ， ττs ，and τ···s are all its solutions，that is，the solutions make the existence of τ -loops cause un fairness.To prevent τ -loops，we extend the def inition of linear recursive specification（Definition 3.6）to the guarded one.

Definition 2.54 （Guarded linear recursive specification）.A recursive specification is linear，if its recursive equations are with the form：

where a ₁₁ ，···， ， a _{k 1} ，···， ， b ₁₁ ，···， ， ，···， ∈E∪｛ τ ｝，and the sum above is allowed to be empty，in which case it represents the dead lock δ .

A linear recursive specification E is guarded，if there does not exist an infinite sequence of τ -transitions ···.

Theorem 2.76 （Conservativity of APTC with static localities，silent step，and guarded linear recursion）.APTC with static localities，silent step，and guarded linear recursion is a conservative extension of APTC with static localities and linear recursion.

Theorem 2.77 （Congruence theorem of APTC with static localities，silent step，and guarded linear recursion）.Rooted branching static location tru ly concurrent bisimulation equivalences ， ，and are all congruences with respect to APTC with static localities，silent step，and guarded linear recursion.

We design the axioms for the silent step τ as shown in Table 2.13.

Theorem 2.78 （Elimination theorem of APTC with static localities，silent step，and guarded linear recursion）.Each process term in APTC with static localities，silent step，and guarded linear recursion is equal to a process term〈 X ₁ | E 〉 with E being a guarded linear recursive specification.

Theorem 2.79 （Soundness of APTC with static localities，silent step，and guarded linear recursion）.Let x and y be APTC with static localities，silent step，and guarded linear recursive terms.If APTC with static localities，silent step，and guarded linear recursion ├ x = y ，then

（1） x y .

（2） x y .

（3） x y .

（4） x y .

Theorem 2.80 （Completeness of APTC with static localities，silent step，and guarded linear recursion）.Let p and q be closed APTC with static localities，silent step，and guarded linear recursion terms，then

（1）If p q ，then p = q .

（2）If p q ，then p = q .

（3）If p q ，then p = q .

（4）If p q ，then p = q .

The unary abstraction operator τ _I （ I⊆ E）renames allatomic events in I into τ .APTC with static localities，silent step，and the abstraction operator is denoted as APTC _τ with static localities.The transition ru les of operator τ _I are as follows：

Theorem 2.81 （Conservativity of APTC _τ with static localities and guarded linear recursion）.APTC _τ with static localities and guarded linear recursion is a conservative extension of APTC with static localities，silent step，and guarded linear recursion.

Theorem 2.82 （Congruence theorem of APTC _τ with static localities and guarded linear recursion）.Rooted branching static location truly concurrent bisimulation equivalences ， ， ，and areall congruences with respect to APTC _τ with static localities and guarded linear recursion.

We design the axioms for the abstraction operator τ _I in Table 2.14.

Theorem 2.83 （Soundness of APTC _τ with static localities and guarded linear recursion）.Let x and y be APTC _τ with static localities and guarded linear recursion terms.If APTC _τ with static localities and guarded linear recursion ├ x = y ，then

（1） x y .

（2） x y .

（3） x y .

（4） x y .

Although τ -loops are prohibited in guarded linear recursive specifications（see Definition 2.54）in a specif iable way，they can be constructed using the abstraction operator.For example，there exist τ -loops in the process term τ _｛a｝ （〈 X|X=aX〉）.To avoid τ -loops caused by τ _I and ensure fairness，the concept of cluster and CFAR（Cluster Fair Abstraction Rule） ^［11］ are still valid in true concurrency，we introduce them below.

Definition 2.55 （Cluster）.Let E be a guarded linear recursive specification，and I⊆ E.Two recursive variable X and Y in E are in the same cluster for I iffthere exist sequences of transitions ，and ，where b ₁₁ ，···， b _mi ， c ₁₁ ，···， c _nj ∈ I∪ ｛ τ ｝.

u ₁ a ₁ ···‖- u _k a _k or（ u ₁ a ₁ ···‖- u _k a _k ） X is an exit for the cluster C iff：① u ₁ a ₁ ···‖- u _k a _k or（ u ₁ a ₁ ···‖- u _k a _k ） X is a summand on the righth and side of the recursive equation for a recursive variable in C ；②in the case of（ u ₁ a ₁ ···‖- u _k a _k ） X ，either a _l I∪｛τ｝（ l ∈｛1，2，···， k ｝）or X C .

Cluster fair abstraction rule is shown in Table 2.15

Theorem 2.84 （Soundness of CFAR）.CFAR is sound modulo rooted branching truly concurrent bisimulation equivalences ，and .

Theorem 2.85 （Com pleteness of APTC _τ with static localities and guarded linear recursion and CFAR）.Let p and q be closed APTC _τ with static localities and guarded linear recursion and CFAR terms，then

（1）If p q ，then p = q .

（2）If p q ，then p = q .

（3）If p q ，then p = q .

（4）If p q ，then p = q . 8JtS2fDz+KGMeHx9deCE+CdEePYLMjEVPJvMV+odB0ogT6zHEtU5ZpmsfTgXSe2l