2.1　Operational Semantics

The semantics of ACP is based on bisimulation/rooted branching bisimulation equivalences，and the modularity of ACP relies on the concept of conservative extension.For the conveniences，we introduce some concepts and conclusions related to them.

Definition 2.1 （Signature）.A signature Σ consists of a finite set of function symbols（or operators） f，g，··· ，where each function symbol f has an arity ar（ f ），representing its number of arguments.A function symbol a，b，c，··· of arity zero is called a constant，a function symbol of arity one is called unary，and a function symbol of arity two is called binary.

We assume a non-empty set S of states，a finite and non-empty set of transition labels A and a finite set of predicate symbols.

Definition 2.2 （Labeled transition system）.A transition is a triple（s，a，s'）with a ∈ A ，or a pair（ s ， P ）where P is a predicate，and s，s' ∈ S .A Labeled Transition System（LTS）is possibly in finite set of transitions.An LTS is finitely branching if each of its states has only finitely many outgoing transitions.

Definition 2.3 （Transition system specification）.A transition rule ρ is an expression of the form ，where H is a set of expressions t t' and tP ， with t，t' ∈T（ Σ ）.These exp ressions are called the（positive）premises of ρ ，The expression π is either t t' or tP ， with t，t' ∈T（ Σ ），called the conclusion of ρ .The left-hand side of π is called the source of ρ .A transition rule is closed if it does not contain any variables.A Transition System Specification（TSS）is a（possible infinite）set of transition rules.

Definition 2.4 （Process（graph））.A process（graph） p is an LTS in which one state s is elected to be the root.If the LTS contains a transition s s' ，then p p' ，where p' has the root state s' .Moreover，if the LTS contains a transition sP ，then pP .There are two conditions for a process p0 ：①A process p0 is finite if there are only finitely many sequences ；②A process p0 is regular if there are only finitely many processes p _k such that .

Definition 2.5 （Bisimulation）.A bisimulation relation R is a binary relation on processes such that：① if pRq and p p' ，then q q' with p'Rq' ；② if pRq and q q' ，then p p' with p'Rq' ；③if pRq and pP ，then qP ；④if pRq and qP ，then pP .Two processes p and q are bisimilar，denoted by p ～HM q ，if there is a bisimulation relation R such that pRq .Note that p，p'，q，q' are processes， a is anatomic action，and P is a predicate.

Definition 2.6 （Branching bisimulation）.A branching bisimulation relation R is a binary relation on the collection of processes such that：① if pRq and p p' ，then either a≡τand p'Rq ，or there is a sequence of（zero or more） τ -transitions q ··· q0 such that pRq0 and q0 q' with p'Rq' ；② if pRq and q q' ，then either a≡τand pRq' ，or there is a sequence of（zero or more） τ -transitions p ··· p0 such that p0Rq and p0 p' with p'Rq' ；③if pRq and pP ，then there is a sequence of（zero or more） τ -transitions q ··· q0 such that pRq0 and q0P ；④if pRq and qP ，then there is a sequence of（zero or more） τ -transitions p ··· p0 such that p0Rq and p0P .Two processes p and q are branching bisimilar，denoted by p ≈ _bHM q ，if there is a branching bisimulation relation R such that pRq .

Definition 2.7 （Rooted branching bisimu lation）.A rooted branching bisimulation relation R is a binary relation on processes such that：① if pRq and p p' ，then q q' with p' ≈ _bHM q' ；② if pRq and q q' ，then p p' with p' ≈ _bHM q' ；③if pRq and pP ，then qP ；④if pRq and qP ，then pP .Two processes p and q are rooted branching bisimilar，denoted by p ≈ _{r bHM} q ，if there is a rooted branching bisimulation relation R such that pRq .

Definition 2.8 （Congruence）.Let Σ be a signature.An equivalence relation R on terms T （ Σ ）is a congruence if for each f ∈ Σ ，if s _i Rt _i for i ∈｛1，···，ar（ f ）｝ ，then f （ s ₁ ，···， sar _{（f ）} ） Rf （ t ₁ ，···， tar _{（f ）} ）.

Definition 2.9 （Conservative extension）.Let T0 and T ₁ be TSSs（Transition System Specifications）over signatures Σ0 and Σ ₁ ，respectively.The TSS T0 ⊕ T ₁ is a conservative extension of T0 if the LTSs（Labeled Transition Systems）generated by T0 and T0 ⊕ T ₁ contain exactly the same transitions t t' and tP with t ∈ T （ Σ0 ）.

Definition 2.10 （Source-dependency）.The source-dependent variables in a transition rule of ρ are defined inductively as follows：①all variables in the source of ρ are sourcedependent；② if t t' is a premise of ρ and all variables in t are source-dependent，then all variables in t' are source-dependent.A transition rule is source-dependent if all its variables are.A TSS is source-dependent if all its rules are.

Definition 2.11 （Freshness）.Let T0 and T ₁ be TSSs over signatures Σ0 and Σ ₁ ，respectively.A term in T（ T0 ⊕ T ₁ ）is said to be fresh if it contains a function symbol from Σ ₁ \Σ 0 .Similarly，a transition labelor predicate symbol in T ₁ is fresh if it does not occur in T0 .

Theorem 2.1 （Conservative extension）.Let T0 and T ₁ be TSSsover signatures Σ0 and Σ ₁ ，respectively，where T0 and T0 ⊕ T ₁ are positive after reduction.Under the following conditions， T0 ⊕ T ₁ is a conservative extension of T0 ：① T0 is source-dependent；② For each ρ ∈ T ₁ ，either the source of ρ is fresh，or ρ has a premise of the form t t' or tP ，where t ∈T（ Σ0 ），all variables in t occur in the source of ρ and t' ，and a or P is fresh. 4HQtPdNZedPsfa7JRbllZ7FGABoV32Z2P0HV+W5lE49enZmYlYdlwVNPGwA0WPQF