2.3　Truly Concurrent Process Algebra-APTC

APTC eliminates the differences of structures of transition systems，event structures，etc.，and discusses their behavioral equivalences.It considers two kinds of causality relations：the chronological order modeled by sequential composition and the causal order between different parallel branches modeled by communication merge.It also considers two kinds of confliction relations：the structural confliction modeled by alternative composition and the conflicts in different parallel branches that should be eliminated.Based on conservative extension，APTC has four modules：BATC（Basic Algebra for True Concurrency），APTC（Algebra for Parallelism in True Concurrency），recursion and abstraction.

2.3.1　Basic Algebra for True Concurrency

BATC has sequential composition·and alternative composition+to capture the chronological ordered causality and the structural confliction.The constants are ranged over A ，the set ofatomic actions.The algebraic laws on·and+are sound and complete modulo truly concurrent bisimulation equivalences（including pomset bisimulation，step bisimulation，hp-bisimulation and hhp-bisimulation）.

Definition 2.15 （Prime event structure with silent event）.Let Λ be afixed set of labels，ranged 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 ∊ is the empty event.Let λ ：E Λ be a labelling function，and let λ （ τ ）= τ .And≤， ♯ 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 if 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 e‖e' ，if ¬（ e ≤ e' ）， ¬（ e' ≤ e ），and ¬（ e♯e' ）.

Definition 2.16 （Configuration）.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 of 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.17 （Pomset transitions and step）.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.18 （Pomset and step bisimulation）.Let E ₁ and E ₂ be PESs.A pomset bisimulation is a relation R⊆C （ E ₁ ） ×C （ E ₂ ），such that if（ C ₁ ， C ₂ ）∈ R ，and C ₁ C ₁ ' ，then ， with X ₁ ⊆ E ₁ ， X ₂ ⊆ E ₂ ， X ₁ ～X ₂ ，and（ ， ）∈ R ，and vice-versa.We say that E ₁ and E ₂ are pomset bisimilar，written E ₁ ～ _p E ₂ ，if there exists a pomset bisimulation R ，such that（∅，∅）∈ R .By replacing pomset transitions with steps，we can get the def inition of step bisimulation.When PESs E ₁ and E ₂ are step bisimilar，we w rite E ₁ ～ _s E ₂ .

Definition 2.19 （Posetal product）.Given two PESs E ₁ and E ₂ ，the posetal product of their conigurations，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'， ）point wise and（ ， f'， ）∈ R ，then（ C ₁ ， f，C ₂ ）∈ 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.Here， X ₁ ⊆ E ₁ ， X ₂ ⊆ E ₂ ， x ₁ ∈E ₁ ，and x ₂ ∈E ₂ .

Definition 2.20 （（Hereditary）history-preserving bisimulation）.A history-preserving（hp-）bisimulation is a posetal relation R⊆C （ E ₁ ） C （ E ₂ ）such that if（ C ₁ ， f，C ₂ ）∈ R ，and ，then ， with（ ， f ［ e ₁ e ₂ ］， ）∈ R ，and vice-versa. E ₁ and E ₂ are history-preserving（hp-）bisimilar and arewritten as E ₁ ～ _hp E ₂ if there exists a hp-bisimulation R such that（∅，∅，∅）∈ R .

A hereditary history-preserving（hhp-）bisimulation is a downward closed hpbisimulation. E ₁ and E ₂ are hereditary history-preserving（hhp-）bisimulation and are written as E ₁ ～ _hhp E ₂ .

In the following，let e ₁ ， e ₂ ， ， ∈E，and let variables x，y，z range over the set of terms for true concurrency，and variables p，q，s range over the set of closed terms.The set of axioms of BATC consists of the laws given in Table 2.1.

Definition 2.21 （Basic terms of BATC）.The set of basic terms of BATC，denoted B （BATC），is inductively defined as follows：

（1）E ⊂B （BATC）.

（2）If e ∈E， t ∈ B （BATC），then e·t∈ B （BATC）.

（3）If t，s∈ B （BATC），then t + s ∈ B （BATC）.

Theorem 2.3 （Elimination theorem of BATC）.Let p be a closed BATC term.Then there exists a basic BATC term q such that BATC ├ p = q .

We provide the operational transition rules of operators·and+as follows.The predicate √ represents successful termination after execution of the event e .

Theorem 2.4 （Congruence of BATC with respect to truly concurrent bisimulation equivalences）.Truly concurrent bisimulation equivalences～ _p ，～ _s ，～ _hp ，and～ _hhp are all congruences with respect to BATC.

Theorem 2.5 （Soundness of BATC modulo truly concurrent bisimulation equivalences）.The axiomatization of BATC is sound modulo truly concurrent bisimulation equivalences～ _p ，～ _s ，～ _hp ，and～ _hhp .That is，

（1）Let x and y be BATC terms，if BATC ├ x = y ，then x ～ _p y .

（2）Let x and y be BATC terms，if BATC ├ x = y ，then x ～ _s y .

（3）Let x and y be BATC terms，if BATC ├ x = y ，then x ～ _hp y .

（4）Let x and y be BATC terms，if BATC ├ x = y ，then x ～ _hhp y .

Theorem 2.6 （Completeness of BATC modulo truly concurrent bisimulation equivalences）.The axiomatization of BATC is complete modulo truly concurrent bisimulation equivalences～ _p ，～ _s ，～ _hp ，and～ _hhp .That is，

（1）Let p and q be closed BATC terms，if p ～ _p q ，then p = q .

（2）Let p and q be closed BATC terms，if p ～ _s q ，then p = q .

（3）Let p and q be closed BATC terms，if p ～ _hp q ，then p = q .

（4）Let p and q be closed BATC terms，if p ～ _hhp q ，then p = q .

Since hhp-bisimilarities is a downward closed hp-bisimilarities and can be downward closed to a singleatomic event，which implies bisimilarities.As proven by M oller［9］，there is no finite sound and complete axiomatization for parallelism‖modulo bisimulation equivalence，so there is no finite sound and comp lete axiomatization for parallelism‖modulo hhp-bisimulation equivalence either.Inspired by the approach of leftmerge used to model the fullmerge for bisimilarities，we introduce a left parallel composition to model the full parallelism‖for hhp-bisimilarities.

In the following subsection，we extend the theory by adding left parallel composition to the whole theory.Since the resulting theory is similar to the previous one，we will only highlight the significant differences，and the proofs of the conclusions are left to the reader.

2.3.2　APTC with Left Parallel Composition

We provide the transition rules of APTC as follows，which are applicable to all truly concurrent behavioral equivalences，including pomset bisimulation，step bisimulation，hp-bisimulation and hhp-bisimulation.Where≬is the whole concurrency operator，‖is the parallel operator， is the left parallel operator，|is the communication merge， Θ is the conflicts elimination operator，and ◁ is the auxiliary unless operator.

The transition rules of left parallel composition are presented as follows.With a little abuse，we extend the causal order relation≤on E to include the original partial order（denoted by ＜）and concurrency（denoted by=）.

The new axioms for parallelism are listed in Table 2.2.

Definition 2.22 （Basic terms of APTC with left parallel composition）.The set of basic terms of APTC，denoted B （APTC），is inductively defined as follows：

（1）E ⊂B （APTC）.

（2）If e ∈E and t ∈ B （APTC），then e·t∈ B （APTC）.

（3）If t，s∈ B （APTC），then t + s ∈ B （APTC）.

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

Theorem 2.7 （Generalization of the algebra for left parallelism with respect to BATC）.The algebra for left parallelism is a generalization of BATC.

Theorem 2.8 （Congruence theorem of APTC with left parallel composition）.Truly concurrent bisimulation equivalences～ _p ，～ _s ，～ _hp ，and～ _hhp are all congruences with respect to APTC with left parallel composition.

Theorem 2.9 （Elimination theorem of parallelism with left parallel composition）.Let p be a closed APTC with left parallel composition term.Then there is a basic APTC term q such that APTC ├ p = q .

Theorem 2.10 （Soundness of parallelism with left parallel composition modulo truly concurrent bisimulation equivalences）.Let x and y be APTC with left parallel composition terms.If APTC ├ x = y ，then

（1） x ～ _s y .

（2） x ～ _p y .

（3） x ～ _hp y .

（4） x ～ _hhp y .

Theorem 2.11 （Completeness of parallelism with left parallel composition modulo truly concurrent bisimulation equivalences）.Let x and y be APTC terms.

（1）If x ～ _s y ，then APTC ├ x = y .

（2）If x ～ _p y ，then APTC ├ x = y .

（3）If x ～ _hp y ，then APTC ├ x = y .

（4）If x ～ _hhp y ，then APTC ├ x = y .

The axioms of encapsulation operator are shown in Table 2.3.

Theorem 2.12 （Conservativity of APTC with respect to the algebra for parallelism with left parallel composition）.APTC is a conservative extension of the algebra for parallelism with left parallel composition.

Theorem 2.13 （Congruence theorem of encapsulation operator ∂ _H ）.Truly concurrent bisimulation equivalences～ _p ，～ _s ，～ _hp ，and～ _hhp are all congruences with respect to encapsulation operator ∂ _H .

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

Theorem 2.15 （Soundness of APTC modulo truly concurrent bisimulation equivalences）.Let x and y be APTC terms including encapsulation operator ∂ _H .If APTC ├ x = y ，then

（1） x ～ _s y .

（2） x ～ _p y .

（3） x ～ _hp y .

（4） x ～ _hhp y .

Theorem 2.16 （Completeness of APTC modulo truly concurrent bisimulation equivalences）.Let p and q be closed APTC terms including encapsulation operator ∂ _H ，then

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

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

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

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

2.3.3　Recursion

Definition 2.23 （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 possible occurrences of the recursive variables X ₁ ，···， X _n .

Definition 2.24 （Solution）.Processes p ₁ ，···， p _n are a solution for a recursive specification｛ X _i = t _i （ X ₁ ，···， X _n ）| i ∈｛1，···， n ｝｝（with respect to truly concurrent bisimulation equivalences～ _s （～ _p ，～ _hp ，～ _hhp ））if p _i ～ _s （～ _p ，～ _hp ，～ _hhp ） t _i （ p ₁ ，···， p _n ）for i ∈｛1，···， n ｝.

Definition 2.25 （Guarded recursive specification）.A recursive specification

is guarded if the right-hand sides of its recursive equations can be adapted to the form by applications of the axioms in APTC，and replacing recursive variables by 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.26 （Linear recursive specification）.A recursive specification is linear if its recursive equations are of 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 δ .

The transition rules of recursive solution are following.

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

Theorem 2.17 （Conservativity of APTC with guarded recursion）.APTC with guarded recursion is a conservative extension of APTC.

Theorem 2.18 （Congruence theorem of APTC with guarded recursion）.Truly concurrent bisimulation equivalences～ _p ，～ _s ，～ _hp ，and～ _hhp are all congruences with respect to APTC with guarded recursion.

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

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

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

（1） x ～ _s y .

（2） x ～ _p y .

（3） x ～ _hp y .

（4） x ～ _hhp y .

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

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

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

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

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

2.3.4　Abstraction

Definition 2.27 （Weak pomset transitions and weak steps）.Let E be a PES， C ∈ C （ E ），and∅ /= X⊆ .If C∩X =∅and = ∪ X ∈ C （ E ），then C C' is called a weak pomset transition from C to C' .Here，we define ，and ，for every e ∈ X .When the events in X are pairwise concurrent，we say that C ^X =⇒C'is a weak step.

Definition 2.28 （Branching pomset and step bisimulation）.Assume a special termination predicate ，and let √ represent a state with √ .Let E ₁ and E ₂ be PESs.A branching 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 more） τ -transitions ，such that（ C ₁ ， ）∈ R and with（ ， ）∈ R .

（2）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 .

（3）If（ C ₁ ， C ₂ ）∈ R and C ₁ ，then there is a sequence of（zero or more） τ 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 pomset bisimilar，written E ₁ ≈ _bp E ₂ ，if there exists a branching pomset bisimulation R ，such that（∅，∅）∈ R .

By replacing pomset transitions with steps，we can get the definition of branching step bisimulation.When PESs E ₁ and E ₂ are branching step bisimilar，wew rite E ₁ ≈ _bs E 2.

Definition 2.29 （Rooted branching pomset and step bisimulation）.Assume a special termination predicate ，and let √ represent a state with √ .Let E ₁ and E ₂ be PESs.A rooted branching 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 pomset bisimilar，written E ₁ ≈ _rbp E ₂ ，if there exists a rooted branching pomset bisimulation R ，such that（∅，∅）∈ R .

By replacing pomset transitions with steps，we can get the definition of rooted branching step bisimulation.When PESs E ₁ and E ₂ are rooted branching step bisimilar，we write E ₁ ≈ _rbs E ₂ .

Definition 2.30 （Branching（hereditary）history-p reserving bisimulation）.Assume a special term ination predicate ，and let √ represent a state with √ .A branching history-preserving（hp-）bisimulation isaposetalrelation 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 .

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

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

②There is a sequence of（zero or more） τ -transitions ，such that（ ， f，C ₂ ）∈ R and with（ ， f ［ e ₂ e ₁ ］， ）∈ R .

（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 history-preserving（hp-）bisimilar and are written as E ₁ ≈ _bhp E ₂ ，if there exists a branching hp-bisimulation R such that（∅，∅，∅）∈ R .

A branching hereditary history-p reserving（hhp-）bisimulation is a downward closed branching hhp-bisimulation. E ₁ and E ₂ are branching hereditary historypreserving（hhp-）bisimilar and are written E ₁ ≈ _bhhp E ₂ .

Definition 2.31 （Rooted branching（hereditary）history-preserving bisimulation）.Assume a special term ination predicate ，and let √ represent a state with √ .A rooted branching 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 history-preserving（hp-）bisimilar and are written as E ₁ ≈ _rbhp E ₂ ，if there exists a rooted branching hp-bisimulation R such that（∅，∅，∅）∈ R .

A rooted branching hereditary history-preserving（hhp-）bisimulation is a downward closed rooted branching hhp-bisimulation. E ₁ and E ₂ are rooted branching hereditary history-preserving（hhp-）bisimilar and are written as E ₁ ≈ _rbhhp E ₂ .

Definition 2.32 （Guarded linear recursive specification）.A recursive specification is linear if its recursive equations are of 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〈 X|E〉 〈 X'|E〉 〈 X ^'' | E 〉 ···.

The transition rules for τ are shown as follows，and the axioms of τ are shown in Table 2.5.

Theorem 2.22 （Conservativity of APTC with silent step and guarded linear recursion）.APTC with silent step and guarded linear recursion is a conservative extension of APTC with linear recursion.

Theorem 2.23 （Congruence theorem of APTC with silent step and guarded linear recursion）.Rooted branching truly concurrent bisimu lation equivalences≈ _rbp ，≈ _rbs ，≈ _rbhp ，and≈ _rbhhp are all congruences with respect to APTC with silent step and guarded linear recursion.

Theorem 2.24 （Elimination theorem of APTC with silent step and guarded linear recursion）.Each process term in APTC with silent step and guarded linear recursion isequal to a process term〈 X ₁ | E 〉 with E being a guarded linear recursivespecification.

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

（1） x ≈ _rbs y .

（2） x ≈ _rbp y .

（3） x ≈ _rbhp y .

（4） x ≈ _rbhhp y .

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

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

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

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

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

The axioms of abstraction operator are shown in Table 2.6.

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

Theorem 2.28 （Congruence theorem of APTC _τ with guarded linear recursion）.Rooted branching truly concurrent bisimulation equivalences≈ _rbp ，≈ _rbs ，≈ _rbhp ，and≈ _rbhhp are all congruences with respect to APTC _τ with guarded linear recursion.

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

（1） x ≈ _rbs y .

（2） x ≈ _rbp y .

（3） x ≈ _rbhp y .

（4） x ≈ _rbhhp y .

Definition 2.33 （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∪｛τ｝.

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

Cluster fair abstraction rule is shown in Table 2.7.

Theorem 2.30 （Soundness of CFAR）.CFAR is sound modulo rooted branching tru ly concurrent bisimulation equivalences≈ _rbs ，≈ _rbp ，≈ _rbhp ，and≈ _rbhhp .

Theorem 2.31 （Completeness of APTC _τ with guarded linear recursion and CFAR）.Let p and q be closed APTC _τ with guarded linear recursion and CFAR terms，then

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

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

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

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

2.3.5　Placeholder

We introduce a constant called the shadow constantⓈto act as a placeholder that we ever used to deal entanglement in quantum process algebra.The transition rule for the shadow constantⓈis shown as follows.The rule states thatⓈcan terminate successfully without executing any action.

We will ad just the def inition of guarded linear recursive specification to the following one.

Definition 2.34 （Guarded linear recursivespecification）.A linear recursivespecification E is guarded if there does not exist an infinite sequence of τ -transitions〈 X|E〉 〈 X'|E〉 〈 X ^'' | E 〉 ···，and there does not exist an infinite sequence ofⓈ-transitions〈 X|E〉 〈 X'|E〉 〈 X ^'' | E 〉 ···.

Theorem 2.32 （Conservativity of APTC with respect to the shadow constant）.APTC _τ with guarded linear recursion and the shadow constant is a conservative extension of APTC _τ .

We design the axioms for the shadow constantⓈin Table 2.8.And for ，we introduce a superscrip t e to denote thatⓈbelongs to e ，and a subscript i to denote that it is the i -th shadow of e .Moreover，we extend the set E to the set E∪｛ τ ｝∪｛ δ ｝∪｛ ｝.

The m ismatch between an action and its shadows in parallelism can lead to a deadlock，that is， e ‖ = δ with e/= e' .We must make all shadows are distinct，to ensure f in hp-bisimulation is an isom orphism.

Theorem 2.33 （Soundness of the shadow constant）.Let x and y be APTC _τ with guarded linear recursion and the shadow constant terms.If APTC _τ with guarded linear recursion and the shadow constant ├ x = y ，then

（1） x ≈ _rbs y .

（2） x ≈ _rbp y .

（3） x ≈ _rbhp y .

Theorem 2.34 （Completeness of the shadow constant）.Let p and q be closed APTC _τ with guarded linear recursion，and CFAR，and the shadow constant terms，then

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

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

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

With the shadow constant，we have

∂ _H （（ a·r _b ）≬ w _b ）= ∂ _H （（ a·r _b ）≬（ ·w _b ））= a·c _b

where H =｛ r _b ， w _b ｝and γ （ r _b ， w _b ） c _b .

And we observe the following example：

What do we observe？Yes，the parallelism contains both interleaving and true concurrency.Thismay be why true concurrency is called true concurrency.

2.3.6　App lications

APTC provides a formal framework based on tru ly concurrent behavioral sem antics，which can be used to verify the correctness of system behaviors.In this subsection，we tend to choose Alternating Bit Protocol（ABP） ^［10］ .

The ABP isused to ensure the successful transm ission of data through a corrupted channel.This success isbased on the assum ption that data can be resent an unlim ited number of times，as illustrated in Figure 2.1.Then we alter the ABP into the true concurrency situation.

（1）Data elem ents d ₁ ， d ₂ ， d ₃ ，···， d _n from a finite setΔcommunicate between a Sender and a Receiver.

（2）If the Sender reads a datum from channel A ₁ ，then this datum is sent to the Receiver in parallel through channel A ₂ .

（3）The Sender processes the data inΔ，generates new data，and sends them to the Receiver through channel B .

（4）The Receiver receives thedata through channel B ，and sends them into channel C 2.

（5）If channel B is corrupted，them essage communicated through channel B can be turned into an errormessage⊥.

（6）Every time the Receiver receives a message through channel B ，it sends an acknow ledgem ent to the Sender through channel D ，which is also corrupted.

（7）Finally，the Sender and the Receiver send out their outputs in parallel through channels C ₁ and C ₂ .

In the truly concurrent ABP，the Sender sends its data to the Receiver，and the Receiver can also send its data to the Sender.However，for simplicity and without loss of generality，we will assume that only the Sender sends itsdata，and the Receiver just receives the data from the Sender.The Sender attaches a bit 0 to data elements d _{2 k- 1} and a bit 1 to data elem ents d _{2 k} ，when they are sent into channel B .When the Receiver reading a datum，it sends back the attached bit via channel D .If the Receiverreceives a corrupted message， then it sends back the previous acknowledgement to the Sender.

Then the state transition of the Sender can be described by APTC as follows：

U _db = r _D （ b ） ·S _{1 -b} +（ r _D （1 -b ）+ r _D （⊥）） ·T _db

where s _B denotes sending data through channel B ， r _D denotes receiving data through channel D ，similarly， r _{A 1} denotes receiving data through channel A ₁ ， s _{C 1} denotes sending data through channel C ₁ ，and b ∈｛0，1｝.

And the state transition of the Receiver can be described by APTC as follows：

Q _b =（ s _D （ b ）+ s _D （⊥）） ·R _{1 -b}

where r _{A 2} denotes receiving data through channel A ₂ ， r _B denotes receiving data through channel B ， s _{C 2} denotes sending data through channel C ₂ ， s _D denotes sending data through channel D ，and b ∈｛0，1｝.

The send action and receive action of the same data through the same channel can communicate with each other，other wise，a dead lock δ will be caused.We define the following communication functions：

γ （ s _B （ d'，b ）， r _B （ d'，b ））≜ c _B （ d'，b ）

γ （ s _B （⊥）， r _B （⊥））≜ c _B （⊥）

γ （ s _D （ b ）， r _D （ b ））≜ c _D （ b ）

γ （ s _D （⊥）， r _D （⊥））≜ c _D （⊥）

Let R0 and S0 be in parallel，then the system R0S0 can be represented by the following process term：

τ _I （ ∂ _H （ Θ （ R0 ≬ S0 ）））= τ _I （ ∂ _H （ R0 ≬ S0 ））

where H =｛ s _B （ d'，b ）， r _B （ d'，b ）， s _D （ b ）， r _D （ b ）| d' ∈Δ， b ∈｛0，1 ｝｝∪｛s _B （⊥）， r _B （⊥）， s _D （⊥）， r _D （⊥）｝

I =｛ c _B （ d'，b ）， c _D （ b ）| d' ∈Δ， b ∈｛0，1 ｝｝∪｛c _B （⊥）， c _D （⊥）｝.

Then we get the following conclusion.

Theorem 2.35 （Correctness of the ABP）.The ABP τ _I （ ∂ _H （ R0 ≬ S0 ））can exhibit the desired external behaviors.

Proof： By using the algebraic laws of APTC，we can derive the following expansions：

Similarly，we can get the following equations.

∂ _H （ T _d 0 ≬ ）= c _B （ d'， 0）·（ （ d' ）‖ （ d' ）） ·∂ _H （ U _d 0 ≬ Q0 ）+ c _B （⊥） ·∂ _H （ U _d 0 ≬ Q ₁ ）

∂ _H （ U _d 0 ≬ Q ₁ ）=（ c _D （1）+ c _D （⊥）） ·∂ _H （ T _d 0 ≬ R'0 ）

∂ _H （ Q0 ≬ U _d 0 ）= c _D （0） ·∂ _H （ R ₁ ≬ S ₁ ）+ c _D （⊥） ·∂ _H （ ≬ T _d 0 ）

∂ _H （ ≬ T _d 0 ）= ^（ c _B （ d'， 0）+ c _B （⊥）） ·∂ _H （ Q0 ≬ U _d 0 ）

∂ _H （ T _{d 1} ≬ ）= c _B （ d'， 1）·（ （ d' ）‖ （ d' ）） ·∂ _H （ U _{d 1} ≬ Q ₁ ）+ c _B （⊥） ·∂ _H （ U _{d 1} ≬ ）

∂ _H （ U _{d 1} ≬ ）=（ c _D （0）+ c _D （⊥）） ·∂ _H （ T _{d 1} ≬ ）

∂ _H （ Q ₁ ≬ U _{d 1} ）= c _D （1） ·∂ _H （ R0 ≬ S0 ）+ c _D （⊥） ·∂ _H （ ≬ T _{d 1} ）

∂ _H （ ≬ T _{d 1} ）=（ c _B （ d'， 1）+ c _B （⊥）） ·∂ _H （ Q ₁ ≬ U _{d 1} ）

Let ∂ _H （ R0 ≬ S0 ）=〈 X ₁ | E 〉，where E is the following guarded linear recursive specification：

X _{2 d} = c _B （ d'， 0） ·X _{4 d} + c _B （⊥） ·X _{3 d} ， Y _{2 d} = c _B （ d'， 1） ·Y _{4 d} + c _B （⊥） ·Y _{3 d} ，

X _{3 d} =（ c _D （1）+ c _D （⊥）） ·X _{2 d} ， Y _{3 d} =（ c _D （0）+ c _D （⊥）） ·Y _{2 d} ，

X _{4 d} =（ s _{C 1} （ d' ） ‖s _{C 2} （ d' ）） ·X _{5 d} ， Y _{4 d} =（ s _{C 1} （ d' ） ‖s _{C 2} （ d' ）） ·Y _{5 d} ，

X _{5 d} = c _D （0） ·Y ₁ + c _D （⊥） ·X _{6 d} ， Y _{5 d} = c _D （1） ·X ₁ + c _D （⊥） ·Y _{6 d} ，

X _{6 d} =（ c _B （ d， 0）+ c _B （⊥）） ·X _{5 d} ， Y _{6 d} =（ c _B （ d， 1）+ c _B （⊥）） ·Y _{5 d} | d，d' ∈Δ｝

Then we app ly the abstraction operator τ _I to〈 X ₁ | E 〉.

Similarly，we can get ·τ _I （〈 X ₁ | E 〉）.We get τ _I （ ∂ _H （ R0 ≬ S0 ）） ·τ _I （ ∂ _H （ R0 ≬ S0 ））.So，the ABP τ _I （ ∂ _H （ R0 ≬ S0 ））can exhibit the desired external behaviors.

With the help of the shadow constant，we can now verify the traditional ABP［10］.

The ABP is used to ensure successful transmission of data through a corrupted channel.This success is based on the assumption that data can be resent an unlimited number of times，as illustrated in Figure 2.2，we alter the ABP into the true concurrency situation.

（1）Data elements d ₁ ， d ₂ ， d ₃ ，···， d _n from a finite set Δ are communicated between a Sender and a Receiver.

（2）The Sender reads a datum from channel A .

（3）The Sender processes the data inΔ，formes new data，and sends them to the Receiver through channel B .

（4）The Receiver sends the datum to channel C .

（5）If channel B is corrupted，them essage communicated through channel B can be turned into an error message⊥.

（6）Every time the Receiver receives a message through channel B ，it sends an acknowledgement to the Sender through channel D ，which is also corrupted.

The Sender attaches a bit 0 to data elem ents d _{2 k- 1} and a bit 1 to data elem ents d _{2 k} ，when they are sent into channel B .When the Receiver reads a datum，it sends back the attached bit through channel D .If the Receiver receives a corrupted message，then it sends back the previous acknowledgement to the Sender.

Then the state transition of the Sender can be described by APTC as follows.

U _db = r _D （ b ） ·S _{1 -b} +（ r _D （1 -b ）+ r _D （⊥）） ·T _db

where s _B denotes sending data through channel B ， r _D denotes receiving data through channel D ，similarly， r _A denoted receiving data through channel A ， denotes the shadow of s _C （ d' ）.

The state transition of the Receiver can be described by APTC as follows：

Q _b =（ s _D （ b ）+ s _D （⊥）） ·R _{1 -b}

where Ⓢ ^{r A （ d ）} denotes the shadow of r _A （ d ）， r _B denotes receiving data through channel B ， s _C denotes sending data through channel C ， s _D denotes sending data through channel D ，and b ∈｛0，1｝.

The sending action and receiving action of the same data through the same channel can communicate with each other，other wise，a dead lock δ will be caused.We define the following communication functions：

γ （ s _D （⊥）， r _D （⊥））≜ c _D （⊥）

Let R0 and S0 be in parallel，then the system R0S0 can be represented by the following process term：

τ _I （ ∂ _H （ Θ （ R0 ≬ S0 ）））= τ _I （ ∂ _H （ R0 ≬ S0 ））

where H =｛ s _B （ d'，b ）， r _B （ d'，b ）， s _D （ b ）， r _D （ b ）| d' ∈Δ， b ∈｛0，1 ｝｝∪｛s _B （⊥）， r _B （⊥）， s _D （⊥）， r _D （⊥）｝

I =｛ c _B （ d'，b ）， c _D （ b ）| d' ∈Δ， b ∈｛0，1｝｝ ∪ ｛ c _B （⊥）， c _D （⊥）｝.

Then we get the following conclusion.

Theorem 2.36 （Correctness of the ABP）.The ABP τ _I （ ∂ _H （ R0 ≬ S0 ））can exhibit the desired external behaviors.

Proof： Similarly，we can get τ _I （〈 X ₁ | E 〉）= r _A （ d ） ·s _C （ d' ） ·τ _I （〈 Y ₁ | E 〉），and τ _I （〈 Y ₁ | E 〉）= r _A （ d ） ·s _C （ d' ） ·τ _I （〈 X ₁ | E 〉）.

So，the ABP τ _I （ ∂ _H （ R0 ≬ S0 ））can exhibit the desired external behaviors. DRcAG63NYmIpsnpjchilxRA+OySxkjWBZvSqbm5ZMtvHkMqzRovR+DhGCQ2CWwqq