![离散与混杂控制的代数理论(英文版)](https://wfqqreader-1252317822.image.myqcloud.com/cover/160/48836160/b_48836160.jpg)
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.
![](https://epubservercos.yuewen.com/6FFB00/28537873604991806/epubprivate/OEBPS/Images/txt002_81.jpg?sign=1739285629-xNGgVN7JvRZ3z9HBn1nhqvVfK8v49Gh0-0-c0638425814bb5fc53db7ceddb17a8d8)
![](https://epubservercos.yuewen.com/6FFB00/28537873604991806/epubprivate/OEBPS/Images/txt002_82.jpg?sign=1739285629-t2lqUaLpctmMYtintR1D8YDR3UylgUr7-0-75f045ebf8ca2a5a81f6637ad261eb17)
The transition rules of left parallel compositionare 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=).
![](https://epubservercos.yuewen.com/6FFB00/28537873604991806/epubprivate/OEBPS/Images/txt002_84.jpg?sign=1739285629-csjJmgzau5HNlCNzbZ1ITSq3HH5wbMLY-0-7b849129fda2985df5967d5826907de9)
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.
Table 2.2 Axioms of parallelism with left parallel composition
![](https://epubservercos.yuewen.com/6FFB00/28537873604991806/epubprivate/OEBPS/Images/txt002_86.jpg?sign=1739285629-y6qV2V3hlDWufIU1we9o8jSr9i43PwxI-0-f9e754bbb09bd28f908ddec356b4a17c)
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.
Table 2.3 The axioms of encapsulation operator with left parallel composition
![](https://epubservercos.yuewen.com/6FFB00/28537873604991806/epubprivate/OEBPS/Images/txt002_87.jpg?sign=1739285629-XOOJtRikvGhpTYQzQlmz5cFlB2WQlrYr-0-91eb85b5d3b3b6c1cc358792c03cb178)
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.