Process Algebra Approach to Reasoning About Concurrent Actions

May 2004, Vol. 19, No.3, pp.364- 373J. Comput. Sci. & Technol.Process Algebra Approach to Reasoning About ConcurrentActionsYuan Feng and Ming Sheng YingState Key Laboratory of Inteligent Technology and Systemns, Department of Compuler Science and TechnologyTainghua University, Beijing 100084, P.R. ChinaE-mail: fengy99g@mails.tsinghua. edu.cnReceived February 27, 2001; revised July 8, 2002.Abstract A reasonable Lransition rule is proposed for synchronized actions and some equatioual properties ofbisimilarity and weak bisirnilarity in the process algebra for reasoning about concurrent actious are presented.Keywords process, global storc, constraint set, bisimulation1 Introductiongence and that of concurrency theory in theoreti-cal computer science. The reasoning problem con-Reasoning about actions is a very active research sidered by Chen and De Giacomol3) is the modelfield in artificial intelligence. The major thesis ischecking which is different from the typical onespecifying and reasoning about dynamic systersmentioned above. They introduced a modal logicwhich may evolve in perforning actions. Various Mμ which is suitable to describe of properties offormal methods for this purpose have been pro- states in a dynamic system. The model checking isposed, e.g., see [i, 2]. The typical methodology of then to verify whether a formula in Mu is true inspeifying dynamic systems is to introduce a set of a state of a given system. The main result in [3)] isfacts whose values change as the system evolves and a linear reduction of model checking in Mu to thethe cffects of actions on these facts. This allows usone in standard pu-calculus.to describe state transitions resulting from execut-As usual, a structured operational sermnantics ofing certain actions, see [1] for details. The typical' the process algebra in [3] was introduced as a tran-reasoning problem in the field is logical implica sition system. The major diference between thistion. More explicitly, we introduce a certain logic transition system and the transitional semantics ofwhich is suitable to the describe dynamic systemsprevious process algebras is that in the former aand then with this logic we deduce some properties state is a configuration consisting of a process andof states of the system under consideration from a a global store, whereas in the latter a state is merelyset of hypotheses about the system.a process. Coping with global stores in most transi-Chen and De Giacomols! presented a new ap-tions is quite easy, but the global store in the tran-proach to reasoning about actions by employ-sitions caused by performing synchronized (concur-ing some modelling tools from process algebrasA.rent) actions deserves a careful treatment. In [3],They constructed an algebra of proceses in which the rule for synchronized actions is given as folowseach process is accompanied by a global store char-acterizing certain facts about the current states.Sym: (n.,0)当(0%,1) (02,0) (吆咀This provides us with a formal method of speci-(pl1lp2,0) of(I'p2,o°)fying concurrent actions and allows u8 to organizeactions within suitable control structures such as where σ' may be chosen a8 any global store ob-sequential and parallel compositions and nondeter-tained by executing the synchronized action 01 UQ2ministic choice. The method of specifying systems of a1 and a2 in σ, and it is completely indepen-adopted in this approach may be seen as a combi- dent of the global stores σ1 and 02. This is obvi-nation of process algebra and the typical method of ously unreasonable. One of the aims of this paperspecifying systems in the area of reasoning about is to overcome this objection by introducing theactions, and this establishes a bridge between thenotion of composition of global stores and present-area of reasoning about actions in artificial intelli- ing a more reasonable rule for synchronized actions.*CorrespondenceThis work was supported by the National Natural Science Foundation of China (Grant No.60273003) and the KeyGrant Project of Chinese Ministry of Education.中国煤化工MYHCNMHGYuan Feng et al: Reasoning About Concurrent Actions365A bisimulation equivalence between processes was cussed in the previous process algebras, which willintroduced in [3], but algebraic properties of this be briefly presented in Subsection 2.3. A globalequivalence were ignored because the main purpose store is intended to describe certain properties ofwas to give a reduction from model checking in Mp the current state, and it may change as the systemto model checking in standard pu-calculus. As an evolves. To describe the change of a global store,addendum, various algebraic properties of bisimu- the notion of update of global store is introduced inlation in the process algebra in [3] are exploited in Subsection 2.1. The evolution of a system happensthis paper.in performing an action. We assume a set of atomicThe issue of equivalent descriptions is very im- actions. A synchronized (concurrent) action exe-portant for the representation of and reasoning on cuted by a system composed of several (concurrent)dynamic systems. In the context of process alge- subsysterms is usully treated as a certain combina-bras, the equivalence of the two descriptions of the tion of some atomic actions. In [3], a synchronizedsame system has been well investigated and vari- action is defined as a set of atomic action, but inous tools have been implemented for verifying the this paper we need a slightly generalized conceptequivalences. A question that naturally arises is of synchronized action. In Subsection 2.2, a syn-when the two descriptions of a dynamic system can chronized action is defined as a multiset of atomicbe considered equivalent. We adopt here the most actions, and its effect on a global store is discussed.popular notion of equivalence that has been pro-posed in the process algebra: bisimulation equiva- 2.1 Updates of Global Storeslence. Roughly speaking, two systems are bisimilarif during every run whenever one system can per-Let Prop be a finite set of primitive propositions.form a certain action, the other system can performThen we write Lit for the set of literals- primitivepropositions and their negations-over Prop, ie.,the same matching such a move.As we all know, a system may perform a lot ofLit= Prop∪-Prop= {A, A:A∈Prop}. (1)actions, many of which we do not care. In fact,sometimes we can hardly determnine all actions a By a global store we mean an interpretation oversystem can perform, soit is reasonable to focus Prop, ie., a mapping from Prop into the set {t,f}our attention on the“constraint set" that contains of truth values.all actions we concentrate on. If two processes canDefinition 2.1 ([3], Definition 2.1). Letσ beperform the samne actions in the constraint set, we a global store, and let L∈Lit be noncontradictry,say that they are weak bisimilar, i.e., if we concen- i.e, for each A∈Prop,AtL or-A≠L. Thentrate on the actions in the constraint set, then theythe update σoL ofσ under L is defined tobe aare undistinguishable.global store and for any A∈Prop,We organize this paper as follows. In Section' tt， if A∈L;2, we introduce the notion of composition of global(σoL)(A)={ f,if→A∈L;(2)stores and use it to present a reasonable rule forsynchronized actions. In this section, we also recallσ(A)，otherwise.some concepts and notations needed in a sequenceObviously, σ0 L is the global store most similarof sections from [3]. In Section 3, we study thor-to σ that satisfies all literals in L. The followingoughly various equational properties of bisimilaritylemma indicates that the update of a global storein the process algebra for reasoning about concur-under the union of several sets of literals is exactlyrent actions. A weak bisimulation is introduced inthe iterated update of the global store under theseSection 4.sets of literals.Lemma 2.1. If L1∪L2 is not contrudictory,2 Algebra of Processes with Global Stores then (σoL1)oLz≈σo(Li∪L2).and Its Transitional SemanticsProof. It is direct from Definition 2.1.0For the case that L1 U L2 is contradictory,In this section a slightly modified process al- σo(L1 ∪L2) is not defined, but (σ0 L1)0L2 isgebra based on the one in [3} for reasoning about always defined provided both L1 and L2 are not .concurrent actions is constructed. As in [3], a state contradictory.of a dynamic system is represented as a configura-Definition 2.2. If σ and σ' are two globaltion, which consists of a process and a global store. stores and there is a non-contradictory set L of lit-Processes in our setting are similar to those dis- erals such that σ' = σ。L, then σ' is called an中国煤化工MYHCNMHG366J. Comput. Sci. & Technol, May 2004, Vol.19, No.3update of σ, and L is called an update set of o' σ1 and σ2 is well-defined. The followving lemmafrom o.demonstrates that Definition 2.3 is reasonable, i.e,It is worth noting that there may be more than the composition of global stores does not dependone update set of o' fromFor example, let upon the choice of update scts of its components.σ(A)= o'(A)=tt for every A∈Prop, then anyLemma 2.4. Letσ1 andσ2 be two updates ofL∈Prop is an update set of o' from σ. The small-σ, L and l be two updale sets ofσ1 from σ, andest update set of a global store from another oneis L2 and L4 be two update sets ofσz fromσ. If botheasy to find and it is given by the fllwing lemma. L1 U L2 and L U E are not contradictory, thenLemma 2.2.Lo,。,={A:σ(A)≠o'(A)= t}σ°(Ln∪L2) =σ0(LI∪L2).(5).U{-A:o(A)≠o'(A)=f} (3)In particular, ifσ1 and σ2 are composable, thenis the smallest update set ofσ' from σ.Proof. First we show that σ' =σo Lo,o'. Forany A∈Prop, ifσ(A) =σ'(A), then A,-A≠Lo,g1σ1 *02=σo (Lo,o1 U Lo,o).(6)and (σ0 Lo,o")(A) = o(A) = o'(A); if o(A)≠o'(A) = tt, then A∈Lo,o' and (o。Lo,r)(A)Proof. For any A∈Prop, if (σo(LqULz))(A) =tt=o"(A);andifσ(A)≠o'(A)=f,thentt,thenA∈L1,orA∈L2,orA,-A史L∪L2.→A∈Lo,o' and (σoLo,r)(A)= f=σ'(A).and σ(A) = tt. We are going to show thatNow we suppose thatσ' =σoL. We are going (σ0 (L U L2))(A) = tt in the following cases:to show that L 2 Lo,o'. Indeed, if A∈Lo,o, andCase 1. A∈L1. Then (σo L4)(A) = (σoA史L, theno(4)≠o'(A)= tt，o(A)= f, and Ln)(4)=tt,A∈ L1,or A,-A4 L4 and o(A)= t.fromAF L,it holds that -A∈L,(σoL)(A)=f, IfA∈ H，then A∈HqUL2 and (σo(Li∪L))(A)=or -A史L，(σ°L)(A) = o(A) = f.. Thus tt. IfA,-AF h and o(4) = tt, then we have to .σ(A) = tt≠f= (σ。L)(A), a contradiction.consider the following two subcases:In addition, -A∈Lo,g' and -A史L leads to aSubcase 1.1. -A生L2. Then-A生Li∪L2.contradiction too. This completes the proof.口Fromσ(4) = tt, we obtain (σo(Li∪L2))(A)=tt.We now introduce the key concept of composi-Subcase 1.2. -A∈I2. Then (σo L2)(A) =tion of global stores, which helps us to give a rea-(σo[2)(4)= f. Noting that o(A) = tt, we havesonable transition rule of synchronized actions.Definition 2.3. Let σ1 = σoLr and σ2 =-A∈L2. Thus, A, 7A∈Li∪L2 is contradictory.σoL2. IfL1∪Lz is not contradictory, thenσ1 andThis is impossible.σ2 are said to be composable, and the compositionCase2. A∈L2. Similar to Case 1.ofσ1 andσz is defined asCase 3. A,-A 生Lq∪L2 and σ(A)= tt. If-A史Li∪L2, then (σo(Li∪L2))(A)= tt. Oth-σ1*σ2=σ°(Lr∪L2).erwise, -A∈LiU L2, and we have:It is possible that two updates σ1 and σ2 of σ areSubcase 3.1. -A∈Li. Then (σo L1)(A) =composable and there are update sets L1 andLz2of (σo L4)(A)= f. Since-A 史L, it must be that01 and 02, respectively, from σ such that L∪L2 σ(A) = f, a contradiction.is contradictory. For instance, let Prop = {A},Subcase 3.2. -A∈L2. Similar to Subcase 3.1.σ(A)= f, σ1(A)= tt and σ2(A) =f. If we setLikewise, we are able to prove that (σ o(L1∪L1={A}andL2 =0, theno1 =σoL1,02 =σoL2Lz))(A) = f implies (σo(L∪Ll))(A)=jf. Thisand 01 and 02 are composable. However, if we put"completes the proof.Li={A}andL2={-A},thenσ1=σ。Li,02 =σoI2 and L1 U L2 is contradictory. On theIt is obvious that the composition of the globalstores is commutative. The following lemma fur-other hand, we have:Lemma 2.3. Ifσ1 andσ2 are two updates ofther shows its associativity. This lemma is veryσ，and they are composable, then Lo,o1 U Lo,an isuseful in the study of algebraic properties of theparallel composition of processes.not contradictory.Proof. Immediate from Lemma 2.2 and Defini-Lemma 2.5. Ifσl, σ2 andσ3 are updates oftion 2.3.] σ, andσ1*(σ2 *03) is defined, then (σ1 *σ2) *σ3Since update sets are generally not unique, one is also defined andσ1*(σ2 *02)= (σ1*02)*σ3.may wonder whether the notion of composition ofProof. Immediate from Definition 2.3.0中国煤化工MYHCNMHGYuan Feng et al: Reasoning About Concurrent Actions3672.2 Synchronized Actions and Theirthe feedback of the executions of the others, andEffectsfor each i∈I, i may be used to indicate the placeLet Act be a finite set of atomic actions. Beforewhere a(i) happens. The set of all synchronizedintroducing the concept of effect function, we needactions is denoted as SAct. In [3), a synchronizedto give several notations. We write W;fT for the setaction is defined as a subset of Act. The reasonof well-formed (propositional) formulae over Prop,why here we define a synchronized action to be ai.e., the free {-, ^}-algebra generated by Prop. Formultiset over Act is mainly technical. lf we keepany set X, P(X) stands for the power set of X, i.e,the original definition of the synchronized action inthe set of subsets of X, and Pfrn(X) for the set of[3], then Lemma 2.6 below is not valid in general(see the explanation after Lemma 2.6). Note thatfinite subsets of X.Definition 2.4 ([3], p.67). An effect functionLemma 2.6 is a key result which guarantees thereasonableness of the rule of the synchronizationis a mappingin Subsection 2.3. On the other hand, Definitioneffect: Act→Prm(Wf x P(Li)). (72.5 is also intuitively reasonable. For example, ifaction a is consuming one resource named R, thenFor anya∈Act, efect(a) is of the formtwo different agents performing the same action aefec(a) = {(y), .E..... En)}(8should consume two R's, but one agent consumesonly one R. Thus, the synchronized action {a, a}wheren≥0, ....E Wf and E....En∈.cannot be identified with the action {a}. However,Lit.- For each (4i;E:)∈efect(a), 中is called itsif we treat a synchronized action as an ordinarypremise and E; its effect.subset of Act, then it must be that {a,a}= {a}.To present the notion of the synchronized ac-We are now ready to consider the change oftion, we need the multiset concept. Let X be a set.global stores in executing synchronized actions. AA finite multiset over X is a mapping a:I→Xglobal store σ is an interpretation over Prop, sowhere I is a finite set, called the index set of a. Ifit may be extended to be a unique truth valuex∈a(I), then x is clledl an element ofa and we function, i.e, a homomorphism frorm Wf to {t,f}write x∈a; andif Y S X anda(I)S Y, then we(equipped with operations -,八 in the usual way).writea∈Y. IfI≠0, then ax is said to be non-For simplicity, the truth value function generatedempty. Obviously, ifa:I→X is a finite multisetbyσ is still denoted asσ. Thus for eachψ∈Wf,over x and it is a one-to-one mapping, then a may 0(吵) ∈{tt, f} expresses the truth value of ψ underbe identifed with the ordinary subset {a(i):i∈I}the interpretation σ.of X. Leta:I→X and β:J→X be two finiteDeinition 2.8. Leta:I →Act be a synchro-multisets over X. If there is a one-onto-one map-nized action andσ a global store. Then the set ofpingh:I→Jsuchthata=βoh,thenwesaypossible global stores obtained by executing a in σthat a and β are equal and writea=β. In whatisσ/a= {σoUi∈rE; :Ui∈E; is not contradictory,follows, we always identify two equal multisets. Ifand for everyi∈I, there is帕∈Wff such thata:I→X andβ:J→X are two finite multisets(中;, E)∈effect(a(i)) and 0(4i)= tt}.over X andI∩J = 0, then the union ofa and βis the finite multiset a∪β:I∪J→x such thatThe above definition is a straight generalizationfor every k∈I∪J,of Definition 2.3 in [3], but for the case that thereare no effects of ax(i) (i∈I) whose premises are{ a(k)， h∈1;(a∪$)(k)=l B(k)， k∈J.(9satisfied by σ, we adopt a different design. In thiscase, according to Definition 2.3 in [3]， we haveInthecaseofI∩J≠0,wecanchangeIandJtoσ/a= {σ}. However, using the above definition weI'= {1}xI and J'= {2} x J, respectively, andobtain σ/a = 0. The reason for our decision is thatthen it holds that I'∩J'=0. So in the sequel weif no premnises in effect(a(i)) (i∈I) are satisfiedalways suppose that the index sets of a and β arethen a cannot be performed and no global storescan be obtained by executing a because premises indisjoint, when talking about aUβ.Definition 2.5. A synchronized action is aeffect(a(i))(i∈I) are preconditions of performingnon-empty finite multiset over Act.Intuitively, a synchronized actiona : I→ActThe following lemma shows that if global storesmeans that atomic actions {a(i) :i∈I} occur si-σ1 and σ2 may be obtained by executing actionsmultaneously as a unity, each implicitly relying on x1 and a2 respectively in global store σ, then their中国煤化工MYHCNMHG368J. Comput. Sci. & Technol, May 2004, Vol.19, No.3composition may be obtained by executing the syn-whereφ∈Wf and r is a set of expressions of thechronization of a1 and 02 in the same global store. formφ →ρ withρ∈Wf and ρ∈Wf。. Ifa pro-This enables us to introduce a reasonable transition cess expression contains no process variables, thenrule of synchronized actions.it is called a process. We use p, 9.... to range overLemma 2.6. Ifσ1∈σ/a1, σz∈σ/a2, and σ1 processes. For each process constant P we assumeand σ2 are composable, thenσ1 *σ2∈o/(x1∪a2). a defining equation P = P with p a process. It isProof. Suppose that a1 : I1 + Act and obvious that the syntax of processes given above isa2: I2→Act and I1∩lz= 0. Since 01∈σ/a1 almost the same as that in [3]. The only differenceand σ2∈σ/az, there are (V)i, Ers)∈efet(a()) is that in [3] only atomic actions are allowed to(i∈1) and (2i, E2i)∈efee(l()) (i∈I2) such appear in prefxes (P→a).p. In this paper, how.that (4x)= tt(i∈1), (021) =tt(i∈I2)，ever, we consider prefixes of the form (P→a),pUi∈n Eri and Uielz Ezi are not contradictory, σ1 =in which Q may be a synchronized action. Accord-σo∪i∈h Er; and σ2 =σo∪i∈rE2; Thenit is easy ing to [3), synchronized actions are exclusively per-to see that σ1*σ2 = σo(Ui∈Eni∪UεrEz2)∈formed by parallel compositions of processes, ando/(a1 Ua2) when Uier1EiUUierE2i is not con- prefixes are seen as a single process evolving alonetradictory.and so they can only execute atomic actions. OnFrom the proof of Lemma 2.6, it is easy to seethe other hand, a dynamic system may have a cer-that σo(Uieh EiUUiEI2 E2s) may fail to belong to tain itrinsic strucure, being conpoed of severalσ/(a∪a2) whenI∩l2≠0. This means that if subsystems with each acting concurrenty with thear1 and 02 are seen as ordinary subsets of Act thenothers. Note that the intrinsic structure of a dy-Lemma 2.6 is not true provided a1∩a2≠0.namic system is usually visible from outside. ThenThe fllowing is a generalization of Definitin it is reasonable to suppose that a synchronized acIndeed, it is an iterated version of Definitiontion may occur in a single system. This is why2.6. This definition will be used in Propositionin our syntax of processes a synchronized action is3.1.3).admitted into a prefix.Definition 2.7. Let σ be a global storeand△s SAct.. Then we define σ/ *△= 2.4 Transitional Semantics{... o/a)a)../an:n≥0 and 1...nEO}.The operational semantics of a process algebrais usually given as a transition system. In previ-ous process algebra such as CCsl4, the states of a2.3 Processestransition system are processes. But according toWe assume a setV of process variables and[3], we deal with a transition system whose statesa set C of process constants. They are rangedare configurations. A configuration is an orderedover by X,Y... and P,... respectively. Fopair (p,σ) in which p is a process and σ a globaleach atomic action a∈Act we assume a primitivestore. We write Con for the set of all configura-proposition. For simplicity, this primitive propo-tions. The structural operational semantics of oursition is also denoted as a. Then we have the setalgebra of processes with global stores is the tran-Wfa of propositional formulae over Act, i.e, Wf。sition systerm (Con, SAct,{9 :a∈SAct}), whereis the free {-, A}-algebra generated by Act. EachSAct is the set of all synchronized actions, and thesynchronized action a: I→Act induces an inter-transition relations斗(a∈SAct) are generated bypretation over Act which is still written as a. Thisthe following transition rules.Transition rules:interpretation is defined as follows:ftt， if a∈a;(10Act :((4→a),P,σ) <(p,")a(a)={ ff, otherwse.ifσ(p)=tt andσ'∈σ/a.For anyρ∈Wfa, we write a(p) for the truth valueof ρ under the interpretation induced by a. ThenSum; :(p1,0)9(p,o1)the syntax of process expressions, ranged over by(P1 + P2,σ)号(p',0{)e,e1, e.... is given as fllows:Sum2 :(2,0)9(P2,吃)e := XIPInil(p→a).ele + ellerler(pr + p2;0) (p2,02)中国煤化工MYHCNMHGYuan Feng et al: Reasoning About Concurrent ActionsInt1 :(p1,0)9(P,01)Definition 3.1. A binary relation R∈Con x(lp2,0) 4(rllp2,01)Con is called a bisimulation if (p,σ)R(q,8) implies,for alla∈SAct,(p2,0)4(2,02)Int2(llp2,0) (1p%,02)(i) whenever (p,σ)→(p',σ') then, for some(g',8')∈Con andβ∈SAct, a= B, (q,8) +(q',8")(0n,0)°2(01,01) (2,0)“3(0202)and (p',o')R(q',8), andSyn:(i) whenever (q,8)9(q',8') then, for some(p',o)∈ConandβSAct, a = B,if ol and 2 are composable.(p,o) 4(p',o) and (p',o')R(q',8').Definition 3.2. 1) Letp and q be two pro-(p,o)$(p',o')cesses, andσ and δ be two global stores. If there(p\y,o) (p"\x,o')eaxists a bisimulation R such that (p, σ)R(q, 8), thenwe say that (p,σ) and (q,8) are bisimilar. In thisifσ(4)= tt implies a(p)=tt for anyφ→ρ∈γ.case, we write (p,σ)~ (9,0).2) Let P and q be two processes. If(p,σ)~ (q,σ)Def:(p,0) 9(r",o")for all global storeso, then we say thatp andq are(P,o) 9(",o")bisimilar and writep~q.The only diference between Definition 7.2 in [3]ifP≈p.nd the above two definitions is that in [3] an as-The fllowin proposition means that the global signment of primitive propositions in Prop to sets ofstore of the successor of configuration (p,σ) after states is added into a transition system, and then aperforming action a must be in σ/a.condition of identity of such assignments is requiredProposition 2.1. If(p,σ) $(p',o), thenσ'∈in the definition of bisimulation.The main purpose of this section is to estab-σ/a.Proof. It may be easily carried out by induc-lish some fundamental equational properties of ourtion on the inference depth of (p,σ) &(p',o), i.e.,process algebra.transition induction (see [4], Subsection 2.9) andProposition3.1. 1) Ifo(q)= f, then for anyby using Lemma 2.6.global store 8, ((4→a)p,a)~ (nil,5).Before concluding this section, we introduce two2) If o($) = 0(4), then ((ψ→a)p,σ) ~concepts needed in the next section.(必→a)-P,σ).Definition 2.8. 1) If there are .....3) (p\7;σ) ~ (p\Yo,p,σ), where ~Yo,p = {o→an∈SAct, proceses ...... and glood ρ∈γ:3o'∈o/*l(p)8t. 0(4)= t}, andl(p) isstores .....n_1,o' such that (p,σ)4(P],a sort ofp.Proof. 1) and 2) are obvious. We now prove 3σ1)3..+(pn-1,0n-1)°$(p',o'), then (p',0') isLet R= {(p"\r,o'), ("\o,p,o")):σ' ∈σ/*e(p)called a derivative of (Pp,0). .2) If for some global store o, (p',o') is a deriva-and p' is a derivative of p}. Then it suffices toshow that R is a bisimulation. Since 7o,p E Y,tive of (p,o), then p' is called a derivative of p.Definition 2.9. Letp be a process, a∈SActeach action of (p'\r,o') is obviously matched bythe same actionof (p^\Yo,p,o'). Conversely, ifand L S SAct.1) If for some process p' and global storesσ and(p'\ro,p,o")("\Yo,p,o"), then (p',o)(p",o")σ' it holds that (p,o)气(p',o'), thena is called anand foranyo→ρ∈7o,p,o'(4)= tt implies a(p) =tt. To prove that (印p^\r,σ') 9(p"\r,o"), we onlyaction ofp.2) If L contains all actions of p and its deriva-need to demonstrate that for anyφ→ρ∈γ- 7o,p;o'(4)= tt implies a(p)= tt. Note that γ- Yoptives, then L is called a sort of p.{ψ→ρ∈r: foranyδ∈0/*l(), 8(p)= f}.Then for any φ→ρ∈γ→γop; σ(4)= f. It is3 Bisimilarityeasy to see that p" is a derivative of p. In addition,from Proposition 2.1 it holds that o”∈σ'/a. SinceSince the operational semantics of our process o' ∈σ/*l(p) anda∈l(p), we haveσ"∈σ/*e(p).algebra is defined as a transition system, we can Thus, (p"\7y,o")R(p"\Yop,o"), and R is a bisimu-define the bisimulation in it in the usual way. For lation.convenience, we display the following definitions.To present Proposition 3.2(11), we need some中国煤化工MYHCNMHG370J, Comput. Sci. & Technl, May 2004, Vol.19, No.3auxiliary results.p. In particular, if for any a∈((p) and for anyDefinition 3.3. Let μ be a clause over Act,φ→ρ∈γ, a(p)= tt, then p\γ~ p;i.e, a disjunction of some literals over Act, and lel10) p\r\η~ p\(γ∪η). .M C Act. If μ satisfies the following condition,11) (llq)\r ~ (p\r)I(q\r) if for eachφ→ρ∈thenμ is said to be M -separate;7, p is range(E(p) U l())-separate, where (p) and(S) ifμ contains a literal in M or a negativee(q) are sorts of p and q respectively.literal then it contains -a for some a史M.Proof. As examples, we prove 7), 9) and 11)Lemma 3.1. Let μ be a clause over Act and here.M,N∈Act. Ifμ is M∪N-separate, then for 7) Let R = ((I(r),0), (l)lr,)) p,qanya∈M andβ∈N,a(2)=B(4)=ttifind r are processes and σ is a global store}. It(a∪β)(u)= tt.sufices to show that R is a bisimulation.nProof. If a(μ)= B()= tt, then we have thefact, if (l(l|r),) +(u,8), then (o,σ) 4(p',σ1),following two cases:(llr,o)4(o,A), a = an∪β，u= pl|u, σ1Case 1. μ contains some a∈a or someb∈B.and λ are composable and δ = σ1 *入.Then μ contains somec∈a∪β and (aU$)(u)=tt. thermore, (q,σ)器(q',σ2), (r,o)9(r',03), β =Case2. μ contains -a for somea史a and -b forQ2∪a3，U = q'|r'， 02 and σ3 are compos-someb史B. With the condition (S) in Definitionable and λ = σ2 * σ3. Consequently, 01 and3.3 we know that 1 contains nc for somec史MUN.02 are composable, (llq,σ)41 “(pllq',o1 * 2).Since a∈M and β∈N, it holds that cf a∪βMoreover，σi * 02 and σ3 are composable andand (a∪β)(μ)= tt.((p{q)|r, o)21Ua2)Uc(ly')Ir', (σ1 *02) * 03).In the above two cases, it always holds thatThus, a = a1∪(azUa3) = (a1Ua2)Ua3, and with(a∪β)(4)= tt.Conversely, if (a∪3)(4) = tt, then we haveLemma 2.5 we have 01*(02*03)= (σ1 *02) *03and (u,0) = ('l"'r"), σ1 * (0σ2 * 3))(l'l}')lr',a(1)= β(μ)= tt for the following three cases:(σ1 *σ2) * o3).Case 1. μ contains -c for somec史aUβ. Then9) It. sufces to show that R = ((p\r,o);cFa,c史βand a(1)= B(1)=tt.(p^\yp,o')):p' is a derivative of P and o' is a globalCase 2. μ contains somea∈c. Then a(μ)= tt.store} is a bisimulation. This is similar to Propo-From the condition (S) in Definition 3.3 it followssition 3.1(3).that μ contains -c for some c # M U N. Thus,11) First we have: .c史β and 3(2)= tt.Claim1.Forany中→ρ∈γ,a1∈l(p)andCase 3. μ contains some b∈B. Similar to Case ;a2∈l(q); a1(p)=a2(p)=tt iff (an∪a2)(p)= tt.In fact, suppose that ρ = AE14i is a canon-Defnition 3.4. Let p be a propositional for~ical conjunctive form. Then a2∈l(q), ar(p) =mula over Act and M∈Act. If ρ has a canon-a2(p)=ttiffforalli≤n,a1(u)=a2(u)ical conjunctive form p =二1H where all 山tt. If μ contains contradictory literals, a1(14) =(i = 1...,n are clauses over Act such that fora2(14i)(a1 U a2)(μ) = tt. Otherwise, 4; iseachi = 1..,n, ui contains contradictory liter-range(l(p) U l(q))-separate. Using Lemma 3.2 weals or μi is M-separate, then p is said to be M-know that a1(mu)= a2(μi)= tt if (a1 U a2)(μ;)=separate.tt. Therefore, ax(p)= a2()= tt if for alli≤n,The following proposition presents some opera-(a1∪a2)()=tt if (a1∪a2)(p)=tt.tion propertics of prefix, summation, parallel com-Secondly with the rules Syn and Res we obtainposition and restriction.the following two claims:Proposition 3.2. 1) (fF→a)p~ nil;Claim 2. ('l"'"\y,o) 9(r,8) i2)p+q~q+ p;(i) (p',a)气(p",8),r = (p"l')\r and for all3)p+(q+r)~(p+q)+r;ψ→ρ∈r, (4)= tt implies a(p)= tt, or4)p+p~p;(i) (q',o)9(q",5),r = 'llq")\r and for all5) p+rnil~ p;φ→ρ∈γ, σ(p) = tt implies a(p)= tt, or6) p|q ~ q|p;(ii) (p',o)°(p",σ1), (',o)%(q",02), for all7) pl(llr) ~ (lq)lr.;φ→ρ∈γ,σ(p)=ttimplies a(p)=tt,a=8) p|nil ~ p;an∪a2;r= (?"!q")\r, σ1 and σ2 are composable9) p\r ~ p\rp, where7p= {p→ρ∈1andδ=σ1 *02.3a∈l(p)s.t. a(p) = f}, and l(p) is a sort ofClaim 3. ()ll(q\),o)9(r,8)迅中国煤化工MYHCNMHGYuan Feng et al: Reasoning About Concurrent Actions371(i) (',o) 4(p*",5), r = (p"\r)|(q^\r) and forProof. Similar to Proposition 4.14(2) in [4] andallφ→ρ∈7Y,σ(p) = tt implies a(p)= tt, orthe above Proposition 3.4(i).(i) (',o)9(q",8), r = (p)\)(q"\r) and forallyφ→ρ∈γ,σ(p)= tt implies a()=tt, or(ii) (p',σ)°(p",σ1), (q',o)"字(q",σ2), for all4 Weak Bisimulationφ→ρ∈γ, o(p)= tt implies a1()= a2(p)= tt,a = a1∪02, r = (p"\>)|(q"\r), 01 and σ2 areSince in our algebra, actions have no comple-composable andδ=σ1 *σ2.mentary ones, we cannot present the weak bisim-By combining the above three claims it is easyulation by the normal way. On the other hand, ato show that R = {(l'lq')\y, o),(p^\)l(q^\r)，system may perform a lot of actions, many of whicho)) : p' and q' arc derivatives of p and q respec-we do not care. In fact sounetimes we can hardlytively, and σ is a global store} is a bisimulation.determine all actions a system can perform, so itThis completes the proof.The fllowing proposition shows that bisimilar- action set that contains all actions that we care.ity is a congruence relation, ie, it is substitutiveSuppose we care only the actions in the setunder prefix, summation, parallel composition andτ∈SAct, we can define T-weak bisimulation rerestriction.lation as follows.Proposition 3.3. I{p1~ P2, then .Defnition 4.1. Letτ C SAct. We say R∈1) (ψ→a)P1~(ψ→ax).P2,.Con x Con is a T-weak bisimulation if (P, o)R(q,0)2)P1 +q~p2+ q，implies, for alla∈SAct,3) pl|q ~ p|g, and .(i) whenever (p,o)9(p',o') then, for sorme4) p\γ~ p2\r.Proof, Similar to Proposition 4.10 in [4].口(q',")_ ∈Con and β∈SAct, a∩τ = β∩τ,We now prove that bisimilarity is compatible(q,8)与(q',8') and (p',o')R(q', 5), andwith recursive definition.(i) whenever (q,8)4(q',8') then, for someProposition 3.4. (1) IfP=p, then P~ p;(p',σ') ∈Con and β∈SAct, a∩τ = β∩τ,(2) Lete1 and e2 only contain variable X, and(p,0) 4(r',o^) and (p',σ )R(',8).let P=e1{P1/X} and Pr=ex{P2/X}. Ife1 ~ e2,Definition 4.2. Letr E SAct,thenP~ P:.1) Let (p,σ) and (q,8) be two configurations.Proof. (i) is obvious. Note that a bisim-We say (P,σ) and (q,6) are T-weak bisimilar, de-ulation introduced in Definition 3.1 is exactlynoted by (p,o) ≈r (q,5), if there exists a T-weaka usual bisimulation in the transition systembisimulation R such that (p, o)R(g,8).(Con, SAct,{4: a∈SAct}), we may freely use2) Let p and q be two processes. We say pthe proof technique of bisimulation up to ~ (seeand q are T-weak bisimilar, denoted by p≈r q, if[4], Definition 4.4, Lemma 4.5 and Proposition 4.6).(p,σ)≈r (q,o) for any global store σ.To prove (i), we only need to demonstrate thatBecause≈, is weaker than ~, Proposition 3.1R = {(e{P/X},o), (e{P2/X},o): e only con-and Proposition 3.2 hold for ≈r，To prove simi-tains variable X and σ is a global store} is a bisimn-lar results like Proposition 3.3, we need a notion ofulation up to ~. This may be carried out by tran-independent processes as follows:sition induction on (e{P/X},o) 9(41,8).0Definition 4.3. A process p is independentTo conclude this section, we prove uniqueness ofif any action ofp is not constrained by the globalsolutions of bisimilarity equations. X is said to bestore, and perforrning it will lead P to another inde-guarded in e if each occurrence of X in e is withinpendent process leaving the global store unchanged,some prefix (4→a).e'. By induction on the lengthie, f(p,σ)+(p',o), then .ofe it is easy to prove the following:Lemma 3.2. If X is guarded in e，and(i)σ' =σ and p' is also independent.(e{p/X},o)9(p' ,8), then there erists process ex-(i) (p,8) 4(p' ,8) for any global store 8.pression e' such thatIntuitively, a process is independent if actionsi)p' =e'{p/X}, andof itself and its alternatives are not restricted byi) for all processq, (e{q/X},o) $(e'{q/X},8).the global stores accompanying with them and fur-Proposition 3.5. Lete contain variable X at thternore, performing these actions will leave themost, andlet X be guarded ine. Ifp~ e{p/X}global stores unchanged. So an independent pro-andq~e{q/X}, thenp~ q.cess is just like a process in CCS. The concept of中国煤化工MYHCNMHG372J. Cormpul. Sci. & Technol, May 2004, Vol.19, No.3independence helps us to avoid affecting the abili-(i) whenever (q,8)号(q',8') then, for someties of processes when parallelizing other processes(p',o') ∈Con and β∈SAct, a∩τ = β∩T,with thern.(p,o) +(w',o') and(p',o')≈, R≈r (',8);The following proposition shows that T- weakand becausc of the following graph:bisimulation is a congruence relation under the con-straint that the parallel composition is performed[(p,o)≈r (P1,σ1) (P1,σ1)R (91,01)]with an independent process.Proposition 4.1. LetT S SAct, ifP1≈r P2a↓a1↓R↓then(p',o')≈r (p{,) (P',σi)≈r R≈r (q{,81)|1)(φ→a)pn≈+ (p→ax).P2z; .|a∩τ =c1∩τ∞1∩τ = β∩τ2)P1 +q≈r P2+q;3)p|lq≈r Pa1|q, ifq is independent;(qn,61)≈τ (q,8) .4) PI\γ≈r p2\r.Proof. As an example, we prove 3).(q;,&)≈t (',8')In fact, we can prove a more stronger result. Ifβi∩T= β∩τ(p1,0)≈r (R2,8) then (P1 |q,o)≈+ (P21|q,8). Ifq is independent, letWe can prove that R C≈r provided that R isS ={(P1 |q,o),(P2 Iq,5)) :(p1,0}≈r (2,8)a T-weak bisimulation up to≈r. That is, to proveand q is independent}(11)(p,o)≈r (q, 8) we only have to find a T-weak bisim-ulation up to≈r which contains ((p,o), (q,8)).Suppose (P1 | q,σ)4(r,σ). There are threeWith the help of weak bisimulations up to≈r,cases:we can prove similarly that ≈r is preserved by re-Case 1. (pn,σ) $(p',o'),r=pIJ q- Be-cursion definition and the uniqueness of solutionscause(Pn,σ)≈r_ (2,5), we have (2,8) 4(p2,8"),of weak bisimilarity equations, that is, Proposition(p',σ)≈r (02,8') and a∩τ = β∩τ, hence also3.4 and Proposition 3.5 both hold for weak bisim-(D2. | q,8)号(% |I q,8") and (p{ |I q,o'),(% |Iulations.q,'))∈S.Case 2. (q,σ)9(q',σ) andr = p1 II q', then .5 Conclusion(q,8)9(q',8) and (P2 I|I q,0)号(p2 | q',8) and((n||4',0),(P21|q',8))∈S.This paper proposes a transition rule reasonableCase 3. (pI,o)*+(p',o'), (q,0)字(q',o), r =for synchronization in the process algebra for tea-pl|q' anda= ai∪a2. Because (Pr,σ)≈+ (2,8)soning about the concurrent actions, which was de-we have (p2,8)4(p%,8), (p',o') ≈r (%2,8') andveloped in [3] by Chen and Giacomo by introducingthe composition of global stores, and presents vari-a∩τ= 3r∩T, hence also (P2 |q,8) -(% |q',8")ous equational properties of bisimilarity in this pro-where β = R∪a2 and β∩τ= (β1∪a2)∩τ=(A∩cess algebra. In [3], a modal logic Mu suitable forr)U(a2∩T)= (a1∩T)U(a2∩τ)= (Q1∪a2)∩r=reasoning about concurrent actions is introduced.a∩r. And we have ((pl iq',o),(p'llq',^))∈S.One of the main results in [3] is a linear reduction ofBy a symmetric argument, we can complete model checking in Mμ to standard modal pu-calculusthe proof that S is a T- weakly bisimulation, i.e.,where only atomic actions are concerned. In thisp1 lq,σ)≈, (P2 II q,5).paper a synchronized action is defined as a multi-Just as in [4]，in order to reduce the complexityset of atomic actions. This is different from whatof proving the bisimulation of two confgurations, was done in [3]. So this reduction does not applywe can define weak bisimulation up to≈r as fol-directly but may be easily generalized to the set-lows.ting of this paper. (By the way, we point out thatDefinition4.4. Letτ∈SAct, RC ConxCon the proof of Theorern 6.5 in [3)] may be consider-is a binary relation betueen configurutions. We say ably simplied. Indeed, we do not need to use aR is aT-weak bisimulation u to≈τ if (p,o)R(q,8)transfinite induction in the case ofφ= μX.业andimplies, for alla∈SAct,the proof may be carried out by simply using the() whenever (p,o)9(p',0") then, for. some definition of (1u.)沿(see [3], p.82, line 30).)(q',8')∈Con and β∈SAct, a∩τ = β∩τ,One interesting problem for further study is to(q,8)气(q',8") and (p',o°)≈, R≈, (',8), andconsider confuence [5 and 4, Chapter 11] in the中国煤化工MYHCNMHGYuan Feng et al: Reasoning About Concurrent Actions373Yuan Feng received theprocess algebra for reasoning about concurrent ac-B.S. degree from Departrmenttions. The results obtained in this direction mayof Mathematics, Tsinghua Uni-be used to study confluent evolution of dynamicversity in 1999. Ile is cursystems.rently a Ph.lD. candidate of De-In [5], the notion of bisimulation limit was in-partmenl of Computer Sciencetroduced in the framework of CCS. This notion isand Technology, Tsinghua Uni-intended to describe the evolution trend of dyuarmnicversity, majoring in theoreticalsystems. We believe that it is also useful in thecomputer science. His currentresearch is focusing on quantumstudy of reasoning about actions in artificial intel-information and quantum computation.ligence.Ming-Sheng Ying was born in 1964. He gradu-ated from Department of Mat hematics, Fuzhou Teach-Referencesers College, Jiangxi, China, in 1981. He is currently[1] Reiter R. The frame problem in the situation calculus: Aa Cheung Kong Professor at the State Key Laborartory of Intelligent Technology and Systerms, Depart-simple solution (sometimes) and a completeness resultrment of Computer Science and Technology, Tsinghuafor goal regression. Artificial Intelligence and MatheUniversity, and Chairman of the Association of Fuzzymatical Theory of Computation: Papers in Honor ofMathemnatics and Fuzzy Systems of China. His re-John McCarthy, Lifschilz V (Ed.), Academic Press, NewYork, 1991, PP.359 -380.search interests include semantics of programming lan-[2] Gelfong M, Lifschitz V. Representing action and changeguages, mathematical logic and its applications, quan-by logic programs. J. Logic Programming, 1993, 17:tum comuputation, and fuzzy logic. He has published301-322.mnore than 60 papers in various journals including Jour-[3] Chen X J, De Giacomo G. Reasoning about nondeter-nal of Symbolic Logic, Acta Informatica, Artificial In-ministic and concurrent actions: A process algebra ap-telligence, Theoretical Computer Science, Mathemati-proach. Artificial Intelligence, 1999, 107: 63- 98. .] Milner R. Communication and Concurrency. Prenticecal Proceedings of Cambridge Philosophy Society, andHall, New York, 1989.IEEE Transactions on Fuzzy Systems. He also pub-Ying M S. Topology in Process Caleulus: Approximatelished a research monograph“Topology in Process Cal-Corrctness and InfinEvolution.n.n Sprnper-Verlaculus: Approximate Correctness and Infinite EvolutionNewW York, 2001.of Concurrent Programs" , Springer-Verlag, New York,2001.中国煤化工MYHCNMHG