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 C1 ～C2，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 E1 and E2 be PESs.A pomset bisimulation is a relation R⊆C（E1）×C（E2），such that if（C1， C2）∈ R，and C1 C1 '，then ， with X1 ⊆E1， X2 ⊆E2， X1 ～X2，and（， ）∈ R，and vice-versa.We say that E1 and E2 are pomset bisimilar，written E1～ p E2，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 E1 and E2 are step bisimilar，we w rite E1～ s E2.

Definition 2.19（Posetal product）.Given two PESs E1 and E2，the posetal product of their conigurations，denoted C（E1） C（E2），is defined as

｛（C1， f，C2）| C1∈ C（E1）， C2∈ C（E2）， f： C1 C2 isomorphism｝

A subset R⊆C（E1） C（E2）is called a posetal relation.We say that R is downward closed when for any（C1， f，C2），（， f'， ）∈ C（E1） C（E2），if（C1， f，C2）⊆（， f'， ）point wise and（， f'， ）∈ R，then（C1， f，C2）∈ R.

For f： X1 X2，we define f［x1 x2］： X1∪｛ x1｝ X2∪｛ x2｝， z∈ X1∪｛ x1｝as follows：① f［x1 x2］（z）=x2，if z=x1；② f［x1 x2］（z）=f（z），otherw ise.Here， X1 ⊆E1， X2 ⊆E2， x1∈E1，and x2∈E2.

Definition 2.20（（Hereditary）history-preserving bisimulation）.A history-preserving（hp-）bisimulation is a posetal relation R⊆C（E1） C（E2）such that if（C1， f，C2）∈ R，and ，then ， with（， f［e1 e2］， ）∈ R，and vice-versa. E1 and E2 are history-preserving（hp-）bisimilar and arewritten as E1～hp E2 if there exists a hp-bisimulation R such that（∅，∅，∅）∈ R.

A hereditary history-preserving（hhp-）bisimulation is a downward closed hpbisimulation. E1 and E2 are hereditary history-preserving（hhp-）bisimulation and are written as E1～hhp E2.

In the following，let e1， e2， ， ∈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.