絞ヶ弇离ㄩ忑珜 >> >> Reniers. Discrete time process algebra with silent step

Reniers. Discrete time process algebra with silent step


Discrete Time Process Algebra with Silent Step
J.C.M. Baeten1 and J.A. Bergstra2 and M.A. Reniers1
Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, The Netherlands Programming Research Group, University of Amsterdam, Kruislaan 403, NL-1098 SJ Amsterdam, The Netherlands and Department of Philosophy, Utrecht University, Heidelberglaan 8, NL-3584 CS Utrecht, The Netherlands Abstract The axiom system ACP of [10] was extended to discrete time in [6]. Here, we proceed to de?ne the silent step in this theory in branching bisimulation semantics [7, 15] rather than weak bisimulation semantics [11, 20]. The version using relative timing is discussed extensively, versions using absolute and parametric timing are presented in brief. A term model and a graph model are presented and soundness and completeness results are given. The time free theories BPA汛 and BPA而 汛 are embedded in the discrete time theories. Examples of the use of the relative time theory are given by means of some calculations on communicating buffers.
Note: Partial support received from ESPRIT Basic Research Action 7166, CONCUR2. This paper supersedes [4].
1

2

1 Introduction
Process algebra was introduced by Milner in the form of CCS [19]. The original design of CCS and of subsequent versions of process algebra such as ACP [10] and TCSP [14] involves no explicit notion of time. Time is present in the interpretation of sequential composition: in p ﹞ q (ACP notation) the process p should be executed before q . Process algebras can be introduced that support standardized features to incorporate a quantitative view on time. Time may be represented by means of non-negative reals, and actions can be given time stamps. This line is followed in [1] for ACP, in [21] for CCS and in [23] for CSP. A second option is to divide time in slices indexed by natural numbers, to have an implicit or explicit time stamping mechanism that determines for each action the time slice in which it occurs and to have a time order within each slice only. This line has been followed in ATP [22], a process algebra that adds time slicing to a version of ACP based on action pre?xing rather than sequential composition. Further, [16] has extended ACP with time slices whereas [21] have added these features to CCS. Following [2, 6], we use the phrase discrete time process algebra if an enumeration of time slices is used. The objective of this paper is to extend the discrete time process algebra of ACP as given in [6] with the silent step 而 . Silent steps have been a cornerstone of CCS since its introduction. Milner used weak bisimulation to model processes with silent step. Van Glabbeek and Weijland [15] introduced branching bisimulation which also deals with silent step, but is slightly less abstract. This will allow a notion of abstraction. We mention that [18] has extended ACP老 , the real time ACP of [1], with silent steps. We present three views on discrete time process algebra with silent step: a version using relative timing (which we discuss extensively), a version using absolute timing, and a version using parametric timing, that integrates the relative and absolute timing versions. There are many practical uses conceivable for timed process algebras. In particular, we mention the TOOL B US (see [9]). This TOOL B US contains a program notation called T which is syntactically sugared discrete time process algebra. Programs in T are called T -scripts. The runtime system is also described in terms of discrete time process algebra. By using randomized symbolic execution the TOOL B US implementation enacts that the axioms of process algebra can be viewed as correctness preserving transformations of T -scripts. A comparable part of discrete time process algebra that is used to describe T -scripts has also been used for the description of 耳 SDL, ?at SDL, a subset of SDL that leaves out modularization and concentrates on timing aspects (see [12]). Discrete-time process algebra with relative timing has also been used for the formal speci?cation of the I 2 C -bus [13]. At this point we are happy to express our admiration for Milner*s contributions. In process theory, but not just there, he has guided the work in such directions, that the perspective of relevance and application is almost self evident. 1

2 Discrete Time Process Algebra with Relative Timing
2.1 Basic Process Algebra with Time Free Actions
The signature of BPA? drt has constants cts(a ) (for a ﹋ A), denoting a in the current time slice, and cts(汛) 步 denoting a deadlock at the end of the current time slice. Also, we have the immediate deadlock constant 汛 introduced in [6]. This constant denotes an immediate and catastrophic deadlock. Within a time slice, there is no explicit mention of the passage of time, we can see the passage to the next time slice as a clock tick. Thus, the cts(a ) can be called non-delayable actions: the action must occur before the next clock tick. The operators are alternative and sequential composition, and the relative discrete time unit delay 考rel (the notation 考 taken from [17]). The process 考rel (x ) will start x after one clock tick, i.e., in the next time slice. In addition, we add the auxiliary operator 糸rel. This operator, called the current slice time out operator, or current slice operator in short, disallows an initial time step, it gives the part of a process that starts with an action in the current time slice. It was introduced in [2] in a setting without immediate deadlock, there, the notation x dt 1 was used for 糸rel(x ). (The Greek letter 糸 sounds like §now§; this correspondence is even stronger in Dutch.) The axioms of BPA? drt are A1-A5,A6ID,A7ID,DCS1-DCS4,DCSID,DRT1-DRT5,DRTSID, as given in Table 1. The axiom DRT1 is the time factorization axiom of ATP ([22]): it says that the passage of time by itself cannot determine a choice. The addition of a silent step in strong bisimulation semantics now just amounts to the presence of a new constant cts(而 ) with the same axioms as the cts(a ) constants. We write A而 = A ﹍ {而 }, A汛 = A ﹍ {汛 }, etc. The axioms DRT3 and DRT5 are derivable from the other axioms 步 (see (see [24]). Note that x + cts(汛) = x for all closed terms x except those that are derivably equal to 汛 Proposition 2.1.7), which implies that in a theory without immediate deadlock the law x + cts(汛) = x will hold. The standard process algebra BPA汛 can be considered as an SRM speci?cation (Subalgebra of Reduced ? Model, in the terminology of [3]) of BPA? drt : consider the initial algebra of BPAdrt , reduce the signature by 步 omitting 汛, 考rel, 糸rel, then BPA汛 is a complete axiomatization of the reduced model, under the interpretation of a , 汛 (from BPA汛 ) by cts(a ), cts(汛). However, this is not the embedding of the time free theory into the discrete time theory that we prefer: it reduces the whole world to one time slice. Rather, we propose to view the time free actions as actions that can occur in any time slice. Following [6], we extend BPA? drt to BPAdrt by introducing constants ats(a ) (for a ﹋ A而 汛 ). The constant ats(a ) executes a in an arbitrary time slice, followed by immediate termination. We ? de?ne these constants in axiom ARTS (Any Relative Time Slice, see Table 1) using the operator 考rel , the ? time iteration operator: 考rel (x ) can start the execution of x in the current time slice, and can always delay to the next time slice. The de?ning axiom for this operator takes the form of a recursive equation (see axiom DRTI1, Discrete Relative Time Iteration, in Table 1). The presentation using the time iteration operator here differs slightly from the presentation in [6]. There, we used the unbounded start delay operator 肋 of [22] instead; the unbounded start delay operator can be simply expressed in terms of the time iteration ? operator as follows: x 肋 = 考rel (糸rel(x )). In order to prove identities for the time iteration operator, we need a restricted form of the Recursive Speci?cation Principle RSP (see, e.g. [7]). We call this principle RSP(DRT) (see Table 2). We give a semantics for the theory BPAdrt in terms of Plotkin-style operational rules. We have the following relations on the set of closed process expressions T (BPAdrt): ? ? ? ? action step ? T (BPAdrt ) ℅ A而 ℅ T (BPAdrt ), notation p ↙ p (denotes action execution); a ﹟ action termination ? T (BPAdrt) ℅ A而 , notation p ↙ (execution of a terminating action); 考 time step ? T (BPAdrt) ℅ T (BPAdrt ), notation p ↙ p (denotes passage to the next time slice); immediate deadlock ? T (BPAdrt ), notation ID( p) (immediate deadlock, holds only for process ex步). pressions equal to 汛
a

We enforce the time factorization axiom DRT1 by phrasing the rules so that each process expression has at most one 考 -step: in a transition system, each node has at most one outgoing 考 -edge. The operational semantics in Table 3 uses predicates and negative premises. Still, using terminology and results of [25], the rules satisfy the panth format, and determine a unique transition relation on closed process expressions. Due to the presence of the immediate deadlock constant we have a notion of bisimulation which is slightly 2

x+y= y+x (x + y ) + z = x + ( y + z ) x+x =x (x + y ) ﹞ z = x ﹞ z + y ﹞ z (x ﹞ y ) ﹞ z = x ﹞ ( y ﹞ z ) 糸rel(cts(a )) = cts(a ) 糸rel(x + y ) = 糸rel(x ) + 糸rel( y ) 糸rel(x ﹞ y ) = 糸rel(x ) ﹞ y 糸rel(考rel (x )) = cts(汛) 步 =汛 步 糸rel(汛)

A1 A2 A3 A4 A5 DCS1 DCS2 DCS3 DCS4 DCSID

步=x x +汛 步﹞x =汛 步 汛 考rel (x ) + 考rel ( y ) = 考rel (x + y ) 考rel (x ) ﹞ y = 考rel (x ﹞ y ) cts(汛) ﹞ x = cts(汛) cts(a ) + cts(汛) = cts(a ) 考rel (x ) + cts(汛) = 考rel (x ) 步 = cts(汛) 考rel (汛) ? ? 考rel (x ) = x + 考rel (考rel (x )) ? ats(a ) = 考rel (cts(a ))

A6ID A7ID DRT1 DRT2 DRT3 DRT4 DRT5 DRTSID DRTI1 ARTS

Table 1: Axioms of BPAdrt (a ﹋ A而 汛 ).

y = x + 考rel ( y )

?

? y = 考rel (x )

RSP(DRT)

Table 2: RSP(DRT).

步 ID(汛) cts(a ) ↙
a

ID(x ), ID( y ) ID(x + y ) ats(a ) ↙ x↙x
a a a

ID(x ) ID(x ﹞ y ) ats(a ) ↙ ats(a ) x﹞y↙y x↙
a 考

ID(x ) ID(糸rel(x )) ats(汛) ↙ ats(汛) x↙x
考 考 考






a

x﹞y↙x ﹞y
a

x﹞y↙x ﹞y

x +y ↙x ,y+x ↙x x+y↙x +y ?ID(x ) 考 考rel (x ) ↙ x
? 考rel (x ) ↙ x

x↙x

a

a

a ﹟ x↙ a ﹟ a ﹟ x + y ↙ ,y+x ↙ 考 考 x ↙x ,y ? 考

x ↙x ,y ↙ y






x+y↙x ,y+x ↙x 糸rel (x ) ↙ x




x↙x
a

a

糸rel (x ) ↙

x↙

a


a


考 x ? ? ? 考rel (x ) ↙ 考rel (x ) 考

x↙x
a

a

? 考rel (x ) ↙

x↙

a


a



x↙x 考 ? ? 考rel(x ) ↙ x + 考rel (x )

Table 3: Operational rules for BPAdrt (a ﹋ A而 ). 3

different from the usual strong bisimulation. This notion is called strong tail bisimulation in this paper. In the terminology of [25] this notion of strong tail bisimulation would be called a bisimulation anyway. De?nition 2.1.1 (Strong tail bisimulation) Two closed terms p and q are called strongly tail bisimilar, notation p? q , if there exists a symmetric binary relation R on closed terms, called strong tail bisimulation, relating p and q such that for all r, s with R (r, s ) we have: 1. if r ↙ r (u ﹋ A而 考 ), then there exists a node s such that s ↙ s and R (r , s ); a ﹟ a ﹟ 2. if r ↙ (a ﹋ A而 ), then s ↙ ; 3. if ID(r ), then ID(s ). We state that strong tail bisimulation is a congruence with respect to the operators from the algebra BPAdrt. Following [24] we can prove that BPAdrt is a sound and complete axiomatization of the model of closed process expressions modulo strong tail bisimulation equivalence. Now, we want to de?ne a notion of bisimulation that takes into account the special status of the immediate deadlock and the silent step. We start from the de?nition of branching bisimulation in the time free case, and adapt this to our timed setting. An immediate deadlock term can only be related to another imme﹟ diate deadlock term. As a consequence, we can have no term that is related to . This is different from the usual de?nition of branching bisimulation of [7, 15]. In order to emphasize this fact, we call the relations to be de?ned branching tail bisimulations. The following de?nition is easier to read if we use a couple of abbreviations: ?rst, we write p ↙ p if either p ↙ p or u √ 而 and p = p . Further, we write p ? q if it is possible to reach q from p by executing a number of 而 -steps (0 or more). De?nition 2.1.2 (Branching tail bisimulation) Two closed terms p and q are called branching tail bisimilar, notation p? btq , if there exists a symmetric binary relation R on closed terms, called branching tail bisimulation, relating p and q such that for all r, s with R (r, s ) we have: 1. if r ↙ r (u ﹋ A而 考 ), then there exist s ? , s such that s ? s ? ↙ s and R (r, s ? ) and R (r , s ); a ﹟ a ﹟ 2. if r ↙ (a ﹋ A而 ), then there exists s ? such that s ? s ? ↙ and R (r, s ? ); 3. if ID(r ), then ID(s ). Actually, we gave the de?nition of semi-branching bisimulation here, as optimized in [8]. The present de?nition is shorter and easier to work with than the original de?nition in [15], and induces the same equivalence relation (see [8]). De?nition 2.1.3 (Rooted branching tail bisimulation) If R is a branching tail bisimulation, then we say that the related pair ( p, q ) satis?es the root condition if: 1. if p ↙ p (u ﹋ A而 考 ), then there exists q such that q ↙ q and R ( p , q ); a ﹟ a ﹟ 2. if p ↙ (a ﹋ A而 ), then q ↙ . A term r is called 考 -reachable from a term p iff there exists a k ﹋ IN such that p √ p0 ↙ p1 ↙ ﹞ ﹞ ﹞ ↙ pk √ r . Two terms p and q are called rooted branching tail bisimilar, notation p? rbtq , if there is a branching tail bisimulation relation R relating p and q such that whenever R (r, s ) and r is 考 -reachable from p, then the pair (r, s ) satis?es the root condition. Thus the root condition amounts to the condition that the bisimulation is strong as long as no action is executed. We can prove that rooted branching tail bisimulation is a congruence relation with respect to the operators from the algebra BPAdrt, thus obtaining the algebra T (BPAdrt)/? rbt of closed process expressions modulo rooted branching tail bisimulation. We can establish that the algebras T (BPAdrt)/? , T (BPAdrt)/? bt , and T (BPAdrt)/? rbt satisfy all laws of BPAdrt+RSP(DRT). Theorem 2.1.4 (Soundness) The laws of BPAdrt +RSP(DRT) are valid in T (BPA drt )/? , T (BPA drt )/? bt , and T (BPA drt )/? rbt . 4
考 考 考 u u u (u ) (u ) u u u

Note that if we take the reduced model obtained by omitting the immediate deadlock constant, then we can ﹟ de?ne a notion of branching bisimulation without the tail condition, where a term can be related to . Using the embedding of discrete time process algebra into real time process algebra given in [2, 6] we ?nd that our notion of silent step in time is in line with the notion of timed branching bisimulation of [18]. Proposition 2.1.5 The following identities are derivable from BPA drt +RSP(DRT):
? ? ? 考rel (x + y ) = 考rel (x ) + 考rel ( y) ? ? 考rel (x ﹞ y ) = 考rel (x ) ﹞ y ? ? 考rel (考rel (x )) = 考rel (考rel (x )) ? ? ? 考rel (考rel (x )) = 考rel (x ) ? 步 考rel (汛) = ats(汛) ? 糸rel (考rel (x )) = 糸rel (x ) + cts(汛)

DRTI2 DRTI3 DRTI4 DRTI5 DRTIID DCSTI

Table 4: Derivable equations. As it turns out these identities are used in the proof of the completeness theorem. By using those, the principle RSP(DRT) does not have to be used directly, but only in the proof of these identities. As a matter of fact we prove completeness for the algebra BPAdrt 而 + DRTI2-DRTI5, DRTIID, DCSTI. The most important place where those identities are used is the Elimination Theorem. This theorem expresses that every closed term can be rewritten into a basic term, i.e., a closed term with a more restricted syntax. We de?ne basic terms over BPAdrt in such a way that they closely resemble the process graphs (see Section 3), in the sense that in every sum-context there is at most one summand ready to perform a time step, and that time iteration does not occur in any sum-context. To achieve this we de?ne auxiliary sets of basic terms 糸(BPAdrt ), (BPAdrt ), and (BPAdrt). De?nition 2.1.6 (Basic terms) The set B (BPAdrt) of basic terms over BPAdrt is de?ned inductively by: 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 步 ﹋ 糸(BPAdrt); 汛 a ﹋ A而 汛 ? cts(a ) ﹋ 糸(BPAdrt ); a ﹋ A而 _ p ﹋ B (BPAdrt) ? cts(a ) ﹞ p ﹋ 糸(BPAdrt ); 步_q √ 汛 步 ? p + q ﹋ 糸(BPAdrt); p, q ﹋ 糸(BPAdrt) _ p √ 汛 步 ? 考rel ( p) ﹋ (BPAdrt); p ﹋ B (BPAdrt) _ p √ 汛 步 ? 考 ? ( p) ﹋ (BPAdrt ); p ﹋ 糸(BPAdrt ) _ p √ 汛 rel 糸(BPAdrt ) ? B (BPAdrt); (BPAdrt) ? B (BPAdrt); (BPAdrt) ? B (BPAdrt ); 步 _ q ﹋ (BPAdrt) ? p + q , q + p ﹋ B (BPAdrt). p ﹋ 糸(BPAdrt ) _ p √ 汛

With this de?nition of basic terms the normal form of cts(b) + ats(a ) is given by the term (cts(b) + cts(a )) + ? 考rel (考rel (cts(a ))). Proposition 2.1.7 For closed BPA drt -terms x such that BPAdrt 步 we have BPA drt x =汛 x + cts(汛) = x.

Theorem 2.1.8 (Elimination) For every closed BPAdrt -term p there exists a basic term q such that A1,A2,A4,A5,A6ID,A7ID,DRT1-DRT3,DRTSID,DCS1-DCS4,DCSID, ARTS,DRTI1-DRTI5,DRTIID,DCSTI p = q.

Note that usually we are less careful with respect to the axioms used for the Elimination Theorem, we just write BPAdrt p = q . However, with the upcoming proof of completeness in mind (see Section 4), we explicitly list the axioms used in the Elimination Theorem. 5

Theorem 2.1.9 (Completeness) BPA drt is a complete axiomatization of strong tail bisimulation on closed BPAdrt terms. Now, the process algebra BPA汛 can be considered as an SRM speci?cation of BPAdrt: reduce the signature 步, 考rel , 糸rel, cts(a ) (for a ﹋ A而 汛 ), and 考 ? , then BPA汛 is a complete of the initial algebra of BPAdrt by omitting 汛 rel axiomatization of the reduced model, with the interpretation of a by ats(a ).

2.2

Axiomatization for Silent Step

Now we want to formulate algebraic laws for the silent step, that hold in the algebra T (BPAdrt)/? rbt . We cannot just transpose the well-known laws, because of the special status of 考 -steps. An example: cts(a ) ﹞ (cts(而 ) ﹞ (考rel (cts(b )) + 考rel (cts(c ))) + 考rel (cts(b))) is not rooted branching tail bisimulation equivalent to cts(a ) ﹞ (考rel (cts(b)) + 考rel (cts(c ))), as in the ?rst term, the choice for b can be made by the execution of the 考 -step, and in the second term, the choice must be made after the 考 -step (however the second term is equal to cts(a ) ﹞ 考rel(cts(b) + cts(c))). In order to ensure that we do not split terms that both have an initial 考 -step, we use the current slice operator 糸rel. In Table 5, DRTB1 and DRTB2 are variants of the branching law B2: x ﹞ (而 ﹞ ( y + z ) + y ) = x ﹞ ( y + z ). In DRTB1, we have the case where the &loose* term ( y in B2) does not have an initial time step, in DRTB2 the other term (z in B2) does not have an initial time step. 步. A simple instance is the We add cts(汛) to ensure that the expression following cts(而 ) does not equal 汛 identity x ﹞ cts(而 ) ﹞ cts(而 ) = x ﹞ cts(而 ). However, we do not have the law x ﹞ cts(而 ) = x (the counterpart of 步 must be distinguished from cts(a ) ﹞ 汛 步 (this can be appreciated in the branching law B1), as cts(a ) ﹞ cts(而 ) ﹞ 汛 a setting with parallel composition: the ?rst term allows execution of actions in the current time slice from a parallel component after the execution of a , the second term does not). In [4] the conditional axiom cts(a ) ﹞ x = cts(a ) ﹞ y ? cts(a ) ﹞ (考rel (x ) + 糸rel (z )) = cts(a ) ﹞ (考rel ( y ) + 糸rel (z )) was introduced to omit a 而 -step following one or more time steps. In this paper we replace this conditional axiom by DRTB3 (see Table 5). A simple instance is cts(a ) ﹞ 考rel(cts(而 ) ﹞ cts(b)) = cts(a ) ﹞ 考rel (cts(b)). ? We have one additional axiom for the constant ats(而 ). In axiom DRTB4 it appears as 考rel (cts(而 )). Axiom DRTB4 can also be given as
? ? ? x ﹞ (ats(而 ) ﹞ 考rel (糸rel ( y ) + 糸rel(z ) + cts(汛)) + 考rel (糸rel ( y ))) = x ﹞ 考rel (糸rel ( y ) + 糸rel (z ) + cts(汛)) ? by replacing 考rel (cts(而 )) by ats(而 ) and using DRTI2, DRTI3, or as

x ﹞ (ats(而 ) ﹞ y + z + cts(汛)
? by also replacing 考rel (糸rel ( y )) by y 肋 , etc.



+ y 肋 ) = x ﹞ y + z + cts(汛)



x ﹞ (cts(而 ) ﹞ (糸rel( y ) + z + cts(汛)) + 糸rel( y )) = x ﹞ (糸rel ( y ) + z + cts(汛)) x ﹞ (cts(而 ) ﹞ (糸rel( y ) + z + cts(汛)) + z ) = x ﹞ (糸rel ( y ) + z + cts(汛)) x ﹞ (考rel (cts(而 ) ﹞ ( y + cts(汛))) + 糸rel(z )) = x ﹞ (考rel ( y + cts(汛)) + 糸rel(z )) ? ? x ﹞ 考rel (cts(而 ) ﹞ 考rel (糸rel ( y ) + 糸rel (z ) + cts(汛)) + 糸rel ( y )) ? = x ﹞ 考rel (糸rel ( y ) + 糸rel(z ) + cts(汛))

DRTB1 DRTB2 DRTB3 DRTB4

Table 5: BPAdrt而 = BPAdrt+ DRTB1-4. We ?nd that rooted branching tail bisimulation is a congruence with respect to the operators from the algebra BPAdrt而 , and that the laws of BPAdrt而 +RSP(DRT) are valid in T (BPAdrt而 )/? rbt. Basic terms for BPAdrt而 are de?ned in the same way as basic terms for BPAdrt. Theorem 2.2.1 (Soundness) The laws of BPAdrt 而 +RSP(DRT) are valid in T (BPA drt 而 )/? rbt .

6

m Before we introduce a number of useful axioms for the silent step, we ?rst de?ne an auxiliary operator 考rel . m The term 考rel (x ) represents the operator 考rel applied to x m times, i.e., for m ≡ 0: 0 考rel (x ) = x m +1 m 考rel (x ) = 考rel (考rel (x ))

The generalizations of the axioms for silent step are useful in the completeness proof in Section 4. Proposition 2.2.2 (Other axioms for abstraction) For closed BPA drt 而 -terms p, x , y , z, and m ≡ 0, we have 1. BPAdrt 而 2. BPAdrt 而 3. BPAdrt 而 4. BPAdrt 而 5. BPAdrt 而
m m x ﹞ 考rel (cts(而 ) ﹞ (糸rel ( y ) + z + cts(汛)) + 糸rel( y )) = x ﹞ 考rel (糸rel ( y ) + z + cts(汛)); m m x ﹞ 考rel (cts(而 ) ﹞ (糸rel ( y ) + z + cts(汛)) + z ) = x ﹞ 考rel (糸rel ( y ) + z + cts(汛)); m x ﹞ 考rel (考rel (cts(而 ) ﹞ (糸rel ( y ) + z + cts(汛)) + 糸rel ( y )) + 糸rel ( p)) m = x ﹞ 考rel (考rel (糸rel ( y ) + z + cts(汛)) + 糸rel ( p)); m x ﹞ 考rel (考rel (cts(而 ) ﹞ (糸rel ( y ) + z + cts(汛)) + z ) + 糸rel( p)) m = x ﹞ 考rel (考rel (糸rel ( y ) + z + cts(汛)) + 糸rel ( p)); m ? ? (考rel (考rel (cts(而 ) ﹞ 考rel (糸rel ( y ) + 糸rel (z ) + cts(汛)) + 糸rel( y ))) + 糸rel ( p)) x ﹞ 考rel m ? = x ﹞ 考rel (考rel (考rel (糸rel ( y ) + 糸rel (z ) + cts(汛))) + 糸rel ( p)).

Let us consider the embedding of the time free theory BPA而 汛 in BPAdrt 而 . If we reduce the initial algebra of 步, ats(a ) (for a ﹋ A而 汛 ), 考rel , 糸rel, 考 ? , and interpret a by cts(a ), BPAdrt而 by reducing the signature by omitting 汛 rel we do not obtain BPA而 汛 of [7, 15]. The ?rst branching law x ﹞ 而 = x will not hold, but instead x ﹞ 而 ﹞ y = x ﹞ y . We can nevertheless obtain BPA而 汛 as an SRM speci?cation as follows. First we add constants ctstau(a ) (for 步, cts(a ), ats(a ), 考rel , 糸rel, 考 ? and a ﹋ A而 汛 ) de?ned by ctstau(a ) = cts(a ) ﹞ cts(而 ). Then, by omitting 汛 rel 而 interpreting a as ctstau(a ), BPA汛 becomes an SRM speci?cation of BPAdrt而 . The following proposition shows that analogues of DRTB1 and DRTB2 and in addition the ?rst 而 -law are valid for the new constants. Proposition 2.2.3 The following laws are derivable from BPA drt 而 : 1. BPAdrt 而 2. BPAdrt 而 3. BPAdrt 而 ctstau(a ) ﹞ ctstau(而 ) = ctstau(a ); x ﹞ (ctstau(而 ) ﹞ (糸rel ( y ) + z + cts(汛)) + 糸rel ( y )) = x ﹞ (糸rel ( y ) + z + cts(汛)); x ﹞ (ctstau(而 ) ﹞ (糸rel ( y ) + z + cts(汛)) + z ) = x ﹞ (糸rel ( y ) + z + cts(汛)).

As a consequence, we can prove x ﹞ ctstau(而 ) = x for all closed terms. Thus, we have embedded the time free theory into the relative discrete time theory. Again, this is not the embedding of the time free theory into the discrete time theory that we prefer: the whole world is reduced to one time slice. We cannot obtain the time free theory BPA而 汛 as an SRM speci?cation by interpreting a by ats(a ), since ats(a ) ﹞ ats(而 ) is not branching tail bisimilar to ats(a ): the ?rst term can still perform time steps after executing the action. Note that the second branching law is valid, as time iteration is the identity on all time free processes. In order to achieve an SRM speci?cation, nonetheless, we will de?ne a different interpretation of time free atoms in our timed setting. We de?ne constants atstau(a ) as follows (a ﹋ A而 汛 ): atstau(a ) = ats(a ) ﹞ ats(而 ). If we reduce the initial algebra of BPAdrt 而 , with the additional constants 步, cts(a ), ats(a ) (for a ﹋ A而 汛 ), 考rel , 糸rel, 考 ? , and we interpret a by atstau(a ), we atstau(a ), by omitting 汛 rel 而 do obtain BPA汛 as an SRM speci?cation. The following proposition shows that the analogue of DRTB4 and in addition the ?rst 而 -law are valid for the new constants. Proposition 2.2.4 The following laws are derivable from BPA drt 而 for a ﹋ A而 : 1. atstau(a ) ﹞ atstau(而 ) = atstau(a ); ? ? ? 2. x ﹞ (atstau(而 ) ﹞ 考rel (糸rel ( y + z )) + 考rel (糸rel ( y ))) = x ﹞ 考rel (糸rel ( y + z )).

7

3 A graph model for BPAdrt 而
In Section 4, we will prove that the present axiomatization of silent step is complete for the model of closed terms modulo rooted branching tail bisimulation. We do this by showing completeness for a model that is isomorphic to T (BPAdrt)/? rbt , namely a model consisting of process graphs. In this section we proceed to de?ne this graph model for BPAdrt而 . An equivalence relation, called rooted branching tail bisimulation, is de?ned on the set of process graphs. Operators resembling the operators of the algebra both in name and in intention are de?ned on process graphs. Finally, we introduce an equivalent characterization of rooted branching tail bisimilarity in Section 3.4. This characterization of rooted branching tail bisimulation will be used in the completeness proof in Section 4.

3.1

Process graphs

We de?ne a set of process graphs as in [7] with labels from A而 考 satisfying the extra condition that every node has at most one outgoing 考 -labeled edge. End-nodes can be labeled with a label ∣ (for successful termination) or a label ID (for immediate deadlock). A 考 -labeled edge may not lead to a successful termination node or an ID-labeled termination node. De?nition 3.1.1 A process graph is a quintuple N , E , r, ∣, ID , where N is a non-empty set of nodes, E ? N ℅ A而 考 ℅ N is a set of labeled edges, r ﹋ N is the root node, ∣? N and ID ? N are disjoint sets of successful termination nodes and immediate deadlock nodes respectively. The following criteria must hold for every process graph: ? every node can have at most one outgoing 考 -edge (time factorization): for all n ﹋ N , if there exist 考 考 nodes s and t such that n ↙ s and n ↙ t , then s = t ; ? a successful termination or an immediate deadlock node cannot have an outgoing edge: for all n ﹋∣ u ﹍ID: {n ↙ s | u ﹋ A而 考 _ s ﹋ N } = ?; ? a successful termination or an immediate deadlock node cannot have an incoming 考 -edge: for all 考 n ﹋∣ ﹍ID, there does not exist a node s ﹋ N such that s ↙ n ﹋ E . Actually, for our purposes we will only need graphs that are interpretations of closed terms. Such graphs 考 always have ?nite node sets, and the only cycles that occur are of the form s ↙ s . The class of all such process graphs is denoted by G. We obtain the set of process graphs G+ by requiring in addition that the root node cannot have a successful termination label, i.e., r ﹋∣. For a process graph g = N , E , r, ∣, ID and a node s ﹋ N , the subgraph of g with s as its root node , notation (g )s , is de?ned as follows: (g )s = N , E , s , ∣, ID , where it is understood that only the nodes and edges that are reachable from s are relevant. u u For a set S and E ? N ℅ A而 考 ℅ N , we de?ne S ? E = {(s , n 1 ) ↙ (s , n 2 ) | s ﹋ S _ n 1 ↙ n 2 ﹋ E }. For a node s ﹋ N and E ? N ℅ A而 考 ℅ N , we de?ne E [s ↙ t ] to be the set E with all occurrences of s replaced by node t . This notation is extended to replace nodes from a set S simultaneously as follows: E [s ﹋ S ↙ t ]. Note that s can occur in t .

3.2

Tail Bisimulations

De?nition 3.2.1 Two graphs g = Ng , E g , rg , ∣ g , IDg and h = Nh , E h , rh , ∣h , IDh are called strongly tail bisimilar, notation g ? h , if there exists a symmetric binary relation R , called strong tail bisimulation, on the nodes of g and h such that for all nodes r, s with R (r, s ) we have: 1. 2. 3. 4. the roots of g and h are related, i.e., R (rg , rh ); u u if r ↙ r ﹋ E g ﹍ E h (u ﹋ A而 考 ), then there exists a node s such that s ↙ s ﹋ E g ﹍ E h and R (r , s ); if r ﹋∣ g ﹍ ∣h , then s ﹋∣ g ﹍ ∣h ; if r ﹋ IDg ﹍ IDh , then s ﹋ IDg ﹍ IDh .

De?nition 3.2.2 Two graphs g and h are called branching tail bisimilar, notation g ?bt h , if there exists a symmetric binary relation R , called branching tail bisimulation, on the nodes of g and h such that for all nodes r, s with R (r, s ) we have: 8

1. the roots of g and h are related; (u ) u 2. if r ↙ r ﹋ E g ﹍ E h (u ﹋ A而 考 ), then there exist nodes s ? , s such that s ? s ? ↙ s ﹋ E g ﹍ E h and R (r, s ? ) and R (r , s ); 3. if r ﹋∣ g ﹍ ∣h , then s ﹋∣ g ﹍ ∣h ; 4. if r ﹋ IDg ﹍ IDh , then s ﹋ IDg ﹍ IDh . De?nition 3.2.3 If R is a branching tail bisimulation, then we say that the related pair (r, s ) satis?es the root u u condition iff whenever r ↙ r ﹋ E g ﹍ E h (u ﹋ A而 考 ), then there exists a node s such that s ↙ s ﹋ E g ﹍ E h and R (r , s ). Two graphs g and h are called rooted branching tail bisimilar, notation g ?rbt h , if there is a branching tail bisimulation relation R between the nodes of g and h such that if R (r, s ) and r is 考 -reachable from the root of g or s is 考 -reachable from the root of h , then the pair (r, s ) satis?es the root condition.

3.3

Isomorphy of the term model and the graph model

In this section we will de?ne mappings graph and term which associate a process graph to a closed term and a closed term to a graph respectively. These mappings are such that they are each other*s inverse modulo strong tail bisimulation. This results in a theorem that states that the term deduction model and the graph model are isomorphic. As a consequence the soundness result can be transfered from the term model to the graph model and the completeness result to come can be transformed from the graph model to the term model. In the following de?nitions we de?ne operators on the graph model which are both in appearance and in intention similar to the operators of the algebra. In these de?nitions we assume that the sets of nodes of the graphs to be composed are disjoint. This assumption is fair since we are only interested in process graphs modulo graph isomorphism (see Section 3.4 for a de?nition of graph isomorphism). De?nition 3.3.1 The following constants are de?ned on the graph model, for a ﹋ A而 : 步 汛 cts(汛) cts(a ) ats(汛) ats(a ) = = = = = {r }, ?, r, ?, {r } ; {r }, ?, r, ?, ? ; a {r, s }, {r ↙ s }, r, {s }, ? ; 考 {r }, {r ↙ r }, r, ?, ? ; 考 a {r, s }, {r ↙ r, r ↙ s }, r, {s }, ? .

De?nition 3.3.2 Let g = N , E , r, ∣, ID . Assume that r ? ﹋ N . Then 考rel (g ) is de?ned as follows: 1. if r ﹋ ID, then 考rel(g ) = {r }, ?, r, ?, ? ; 考 2. otherwise, 考rel (g ) = N ﹍ {r ? }, E ﹍ {r ? ↙ r }, r ? , ∣, ID . De?nition 3.3.3 Let g = N , E , r, ∣, ID . Then 糸rel(g ) is de?ned as follows: 糸rel(g ) = N , E \{r ↙ s | s ﹋ N }, r, ∣, ID . De?nition 3.3.4 Let g = Ng , E g , rg , ∣ g , IDg and h = Nh , E h , rh , ∣h , IDh . Then g ﹞ h is de?ned as follows: g﹞h = , , , , . ( Ng \ ∣ g ) ﹍ (∣ g ℅ Nh ) E g [ f ﹋∣ g ↙ ( f , rh )]﹍ ∣ g ? E h rg ∣ g ℅ ∣h IDg ﹍ (∣ g ℅IDh )


Before we can de?ne + on the graph model, we ?rst have to de?ne a root unwinding map. 9

De?nition 3.3.5 The mapping 老 is for all g = N , E , r, ∣, ID , de?ned as follows (u ﹋ A而 考 ): 老(g ) = N ﹍ {r ? }, E ﹍ {r ? ↙ s | r ↙ s ﹋ E }, r ? , ∣, ID ﹍ {r ? | r ﹋ ID} . De?nition 3.3.6 Let g = Ng , E g , rg , ∣ g , IDg and h = Nh , E h , rh , ∣h , IDh . Then g + h is de?ned as follows: 1. if rg ﹋ IDg , then g + h = h ; 2. if rh ﹋ IDh , then g + h = g ; 3. if rg ﹋ IDg and rh ﹋ IDh , then (a) if rg ↙ rg ﹋ E g and rh ↙ rh ﹋ E h , then g+h = , , , , ; ( Ng \{rg }) ﹍ ( Nh \{rh }) ﹍ {rg +h } E g [rg ↙ rg +h ] ﹍ E h [rh ↙ rg +h ] r g +h ∣ g ﹍ ∣h IDg ﹍ IDh
考 考 u u

(b) if rg ↙ sg ﹋ E g and rh ↙ sh ﹋ E h for some sg ﹋ Ng and sh ﹋ Nh such that sg √ rg or sh √ rh , then suppose that 老(g ) = Ng , E g , rg , ∣ g , IDg and 老(h ) = Nh , E h , rh , ∣h , IDh . Suppose that rg ↙ sg and rh ↙ sh . Suppose that (g )sg + (h )sh = N , E , r, ∣, ID . Then, g+h = , , , , ;
考 考





Ng ﹍ Nh ﹍ N ﹍ {rg +h } 考 考 考 E g \{rg ↙ sg } ﹍ E h \{rh ↙ sh } ﹍ E ﹍ {rg +h ↙ r } r g +h ∣ g ﹍ ∣h ﹍ ∣ IDg ﹍ IDh ﹍ ID

(c) otherwise, suppose that 老(g ) = Ng , E g , rg , ∣ g , IDg and 老(h ) = Nh , E h , rh , ∣h , IDh . Then, g +h = , , , , . ( Ng \{rg }) ﹍ ( Nh \{rh }) ﹍ {rg +h } E g [rg ↙ rg +h ] ﹍ E h [rh ↙ rg +h ] r g +h ∣ g ﹍ ∣h IDg ﹍ IDh

? De?nition 3.3.7 Let g = N , E , r, ∣, ID . Then 考rel is de?ned inductively as follows: ? 1. if r ↙ r , then 考rel (g ) = g ; 考 考 2. if r ↙ s for some s = r , then de?ne 糸 = N , E \{r ↙ s }, r, ∣, ID and 肉 = (g )s . Suppose ? 考rel (糸 + 肉) = N , E , r , ∣ , ID . Then, ? 考rel (g ) = N ﹍ N , E \{r ↙ s } ﹍ E ﹍ {r ↙ r }, r, ∣ ﹍ ∣ , ID ﹍ ID ; ? ? 3. otherwise, if r ﹋ ID, then 考rel (g ) = {r }, {r ↙ r }, r, ?, ? , else 考rel (g ) = N , E ﹍{r ↙ r }, r, ∣, ID . 考 考 考 考 考

This is a well-founded inductive de?nition since the length of the path from r consisting of 考 -steps only (not 考 -loops) decreases. The mapping graph which associates to a closed BPAdrt 而 term a process graph is de?ned inductively as can be expected by using the previously given operators on process graphs. Applying the mapping graph to an arbitrary closed BPAdrt而 term always gives a graph without cycles other than 考 -loops. Such graphs will be called root unwound process graphs on several occasions. 10

De?nition 3.3.8 The mapping term : G+ ↙ T (BPAdrt而 ) is for all process graphs g = N , E , r, ∣, ID de?ned inductively by: ? 考 考 ? ? r ﹋ E; ? ? 考rel (term( N , E \{r ↙ r }, r, ∣, ID )) if r ↙ ? 考 ? 步 ? 汛 if r ↙ r ﹋ E _ r ﹋ ID; 考 ? term(g ) = cts(汛) if r ↙ r ﹋ E _ r ﹋ ID _ E = ; ? ? u ? ? termg (r ↙ s ) otherwise, ? ? u
r↙s﹋E

where termg : E ↙ T (BPAdrt 而) is, for a ﹋ A而 , de?ned by termg (r ↙ s ) termg (r ↙ s )
考 a

=

cts(a ) if s ﹋∣; cts(a ) ﹞ term((g )s ) otherwise; = 考rel (term((g )s )).

Theorem 3.3.9 (Isomorphy) T (BPA drt 而 )/? and G/? are isomorphic.

3.4

Alternative characterization of the bisimulations

We proceed to ?nd formulations for our bisimulation relations in terms of colourings, analogous to [15]. Let C be a given set, the set of colours. A coloured graph is a process graph with colours C ﹋ C as labels attached at the nodes. A concrete coloured trace of a coloured graph g is a ?nite sequence (C0 , a1 , C1 , ﹞ ﹞ ﹞ , Ck?1 , ak , Ck ) for a1 a2 ak which there exists a path r0 ↙ r1 ↙ ﹞ ﹞ ﹞ ↙ rk from the root node r0 of g such that ri has colour Ci . A concrete consistent colouring of a set of process graphs is a colouring of their nodes with the property that two nodes (also from the same graph) have the same colour only if they have the same concrete trace set and the same label. Two process graphs g and h are concrete coloured trace equivalent, notation g √cc h , if, for some concrete consistent colouring on {g , h }, they have the same concrete coloured trace set, or equivalently, the root nodes have the same colour. As in [15], we have the following theorem. Theorem 3.4.1 For process graphs g , h ﹋ G, we have g ?h iff g √cc h. An abstract coloured trace of a coloured graph is a sequence of the form (C0 , a1 , C1 , a2 , ﹞ ﹞ ﹞ , ak , Ck ) which is obtained from a concrete coloured trace of this graph by replacing all subsequences of the form (C, 而, C, 而, ﹞ ﹞ ﹞ , 而, C ) by C . An abstract consistent colouring of a set of graphs is a colouring of their nodes with the property that two nodes have the same colour only if they have the same abstract coloured trace set and the same label. For two coloured graphs g and h we write g √c h , if, for some abstract consistent colouring on {g , h }, they have the same abstract coloured trace set. In the sequel, we leave out the adjectives &abstract*. Theorem 3.4.2 For process graphs g , h ﹋ G, we have g ?bt h iff g √c h. A rooted coloured trace of a coloured graph is a sequence of the form (C0 , a1 , C1 , a2 , ﹞ ﹞ ﹞ , ak , Ck ) which is obtained from a concrete coloured trace of this graph by replacing all non-考 -reachable subsequences (C, 而, C, 而, ﹞ ﹞ ﹞ , 而, C ) by C . A rooted consistent colouring of a set of graphs is a colouring of their nodes with the property that two nodes have the same colour only if they have the same rooted coloured trace set and the same label. For two root unwound coloured graphs g and h we write g √rc h , if, for some rooted consistent colouring on {g , h }, they have the same rooted coloured trace set. Theorem 3.4.3 For process graphs g , h ﹋ G, we have g ?rbt h iff g √rc h. It is possible to colour the nodes of a root unwound process graph g in such a way that two nodes have the same colour iff they can be related by a rooted branching tail autobisimulation on g . This colouring is rooted and consistent. The largest rooted branching tail autobisimulation relation of a graph is called its canonical colouring. 11

De?nition 3.4.4 Let g be a root unwound process graph and consider its canonical colouring with colour set C. Let N (g ), the normal form of g , be the graph which can be found by contracting all nodes with the same colour and removing 而 -loops. More precisely: 1. N (g ) has colours C ﹋ C as its nodes; a a 2. N (g ) has an edge C ↙ C (a ﹋ A考 ) iff g has an edge r ↙ r such that r has colour C and r has colour C ; 而 而 3. N (g ) has an edge C ↙ C iff C = C and g has an edge r ↙ r and r has colour C and r has colour C; 4. C has a label ∣ iff g has a node r with label ∣ and r has colour C ; 5. C has a label ID iff g has a node r with label ID and r has colour C . For all root unwound process graphs g ﹋ G, we have g ? rbt N (g ). De?nition 3.4.5 (Graph Isomorphism) A graph isomorphism is a bijective relation R between the nodes of two process graphs g = Ng , E g , rg , ∣ g , IDg and h = Nh , E h , rh , ∣h , IDh such that: 1. the roots of g and h are related by R , i.e., R (rg , rh ); a a 2. if R (r, s ) and R (r , s ) then r ↙ r ﹋ E g iff s ↙ s ﹋ E h ; 3. if R (r, s ) then r ﹋∣ g iff s ﹋∣h and r ﹋ IDg iff s ﹋ IDh . Two graphs are isomorphic, notation g h , iff there exists an isomorphism between them. Note that is a congruence relation on process graphs. Note also that only the nodes which are reachable from the root nodes of g and h are taken into account. As a consequence we have that a process graph g is graph isomorphic with the graph consisting of the edges and nodes of g that are reachable from the root node of g. As in [15] we have the following Normal Form Theorem. Theorem 3.4.6 (Normal form theorem) Let g and h be root unwound process graphs that are in normal form. Then g ? rbt h if and only if g h.

4 Completeness of the Axiomatization
4.1 Introduction
In this section we will prove, following the approach of [15], that BPAdrt而 is a complete axiomatization of rooted branching tail bisimulation on process graphs from G+ . The basic idea in the completeness proof is to establish a graph rewriting system on process graphs, which is con?uent and strongly normalizing (up to graph isomorphism), and for which every rewrite step preserves rooted branching tail bisimilarity. Con?uence and strong normalization together are needed to ensure that for every process graph there is a unique normal form up to graph isomorphism. We want the rewrite steps of the graph rewriting system to preserve rooted branching tail bisimilarity since for every such rewrite step we can prove (rather easily) that the corresponding terms are derivably equal (see Theorem 4.4.3). Furthermore, we will show that the normal forms with respect to the graph rewriting system are normal forms in the sense of Section 3.4. As a consequence we have that the normal forms with respect to the graph rewriting system of two rooted branching tail bisimilar process graphs are isomorphic. All that remains is to show that for every term p, the mapping term ? graph is an identity modulo derivability. This is the sole subject of Section 4.3.

4.2

The Graph Rewriting System

The graph rewriting system will be such that it is capable of performing two transformations on process graphs. Firstly, it can contract two nodes which are essentially the same. Such nodes are called double nodes. Secondly, it can contract a 而 -edge that is redundant. Such 而 -edges are called manifestly inert.

12

De?nition 4.2.1 (Double Nodes) A pair (r, s ), with r = s , of nodes in a process graph g = N , E , r, ∣, ID is called a pair of double nodes if ? ? ? ? for all nodes t = r, s and labels u ﹋ A而 考 : r ↙ t ﹋ E iff s ↙ t ﹋ E ; 考 考 r ↙ r ﹋ E iff s ↙ s ﹋ E ; r ﹋∣ iff s ﹋∣; r ﹋ ID iff s ﹋ ID.
u u

The following proposition formalizes the statement that double nodes are essentially the same: their subgraphs are isomorphic. Proposition 4.2.2 Let g be a process graph. If (r, s ) is a pair of double nodes in g, then (g )r (g )s .

A 而 -edge between two nodes r and s is called manifestly inert if r and s agree with respect to the labels and 考 -loops and if any other outgoing edge of r is also an outgoing edge of s . De?nition 4.2.3 (Manifestly inert 而 -edges) An edge r ↙ s in a process graph g is manifestly inert if r is not 考 -reachable from the root node of g , r and s have the same label (if any), and for all nodes t and labels a a 考 考 a ﹋ A而 考 such that (a , t ) = (而, s ) and (a , t ) = (考, r ): r ↙ t implies s ↙ t , and r ↙ r iff s ↙ s . Basically, for an edge to be manifestly inert means that it can be removed with one of the axioms for silent step. The next theorem states that in order to obtain a normal form for a process graph we only have to repeatedly unify a pair of double nodes or contract a manifestly inert 而 -edge. Theorem 4.2.4 A process graph g ﹋ G without double nodes and without manifestly inert 而 -edges is in normal form. Proof. Let g be a ?nite process graph which is not in normal form. Then it has at least one pair of different nodes with the same colour with respect to the canonical colouring. The depth of a node s in g is de?ned to be the number of edges in its longest path not counting 考 -loops. Then, we de?ne the combined depth of two nodes as the sum of their depths. We mention the following property of the depth of a node: u if r ↙ s (r = s ), then d (s ) < d (r ). We will use it in the remainder of the proof. Choose a pair (r, s ) of different, but equally coloured nodes in g with minimal combined depth. Now we have the following trivial claim: if r and s are nodes in g which have the same colour and moreover d (r ) + d (s ) < d (r ) + d (s ), then r = s (*). If this would not be the case then clearly (r, s ) is not a minimal pair. Assume, without loss of generality, d (s ) ≒ d (r ). Now, we prove the following two properties: 1. if r ↙ t and (u , t ) = (而, s ), then s ↙ t , and u 而 u 2. if s ↙ t , then r ↙ s or r ↙ t . Ad 1. Suppose that r ↙ t and that (u , t ) = (而, s ). Since r and s have the same colour we ?nd that either (1) u = 而 and t has the same colour as r and s , or (2) s has the coloured trace (C (r ), u , C (t )). For the ?rst case we ?nd t = s from (*) and d (t ) < d (r ). This is in contradiction with the assumption (u , t ) = (而, s ). 而 For the second case we reason as follows. Suppose that s ↙ p with C ( p) = C (s ). Then from d ( p) < d (s ) we have p = r . Then we also have the following contradiction: d ( p) < d (s ) ≒ d (r ). So clearly, u = 而 . u Suppose that s ↙ p for some node p such that C ( p) = C (t ). Since d ( p) < d (s ) and d (t ) < d (r ), we have d ( p) + d (t ) < d (s ) + d (r ). We also have C ( p) = C (t ) and C (s ) = C (r ). But then we have by (*) u that t = p. So clearly s ↙ t is an edge in g . u Ad 2. Suppose that s ↙ t . Then we have d (t ) < d (s ). But then also d (t ) + d (r ) < d (s ) + d (r ). If s and t have the same colour, then by (*) we have r = t . This is in contradiction with d (t ) < d (s ) ≒ d (r ). So clearly s and t do not have the same colour. Then (C (s ), u , C (t )) is a coloured trace of r , since s and 而 r have the same colour. Now two cases can be distinguished. First, suppose that r ↙ p for some node p such that C ( p) = C (r ). Then d ( p) < d (r ) and also d ( p) + d (s ) < d (r ) + d (s ). Hence, from (*) we have 而 u p = s . So we have r ↙ s . Second, suppose that r ↙ p (u = 而 ) for some node p with C ( p) = C (t ). 13
u u u 而

Since d ( p) < d (r ) and d (t ) < d (s ), we have d ( p) + d (t ) < d (r ) + d (s ). From (*) we obtain p = t . So u 而 u r ↙ t . Concluding, either r ↙ s or r ↙ t . 而 From the two properties we just proved it follows that if r ↙ s is an edge in g , then it is manifestly 而 inert, and if r ↙ s is not an edge in g , then (r, s ) is a pair of double nodes. The previous theorem can serve as a source of inspiration for de?ning the graph rewriting system. De?nition 4.2.5 The rewriting relation ↙ is de?ned by the following one-step reductions: 1. sharing a pair of double nodes (r, s ) : replace all edges t ↙ r by t ↙ s (if not already there, otherwise u just remove t ↙ r ) and remove r with all its outgoing edges from the graph. 而 a a 2. contracting a manifestly inert 而 -edge r ↙ s : replace all edges t ↙ r by t ↙ s (if not already there, a otherwise just remove t ↙ r ) and remove r with all its outgoing edges from the graph. Theorem 4.2.6 The graph rewrite relation ↙ has the following properties: 1. 2. 3. 4. if g ﹋ G+ and g ↙ h, then h ﹋ G+ ; ↙ preserves rooted branching tail bisimilarity, i.e., if g ↙ h, then g ? rbt h; the graph rewrite system is strongly normalizing; the graph rewrite system is con?uent (up to graph isomorphism).
u u

Proof. We will omit the proof for the ?rst property. For the second property, we will show that rooted branching tail bisimilarity is preserved under the application of each of the two rewrite rules. (1) Sharing a pair of double nodes. Suppose that (r, s ) is a pair of double nodes in g . Then ↙ identi?es the nodes r and s , i.e., it removes the node r . Then the relation R = I d (h ) ﹍ {(r, s ), (s , r )} is clearly a rooted branching 而 tail bisimulation between g and h . (2) Contracting a manifestly inert 而 -edge. Suppose that r ↙ s is a manifestly inert 而 -edge. The relation R = I d (h ) ﹍ {(r, s ), (s , r )} is a rooted branching tail bisimulation between g and h . For the third property we reason as follows. Strong normalization of the graph rewrite system follows immediately from the following observations: (1) every ?nite process graph has only ?nitely many nodes, and (2) in every application of a rewrite rule the number of nodes decreases with one. For the proof of the fourth property, suppose that g has two normal forms g1 and g2 . Then both g1 and g2 are without double nodes and without manifestly inert 而 -edges by Theorem 4.2.4. From the second item of this theorem and g ↙? g1 , g ↙? g2 , we have g ? rbt g1 and g ? rbt g2 and since rooted branching tail bisimilarity is an equivalence relation also g1 ? rbt g2 . From the Normal Form Theorem (Theorem 3.4.6) we obtain g1 g2 .

4.3

Correspondence between G+ and BPAdrt 而

As already announced we need to show that the mapping term ? graph is an identity modulo derivability. For basic terms this turns out to be easy. The extension of this result to closed terms in general is based on the observation that for every axiom used in the Elimination Theorem the graphs corresponding to the left-hand side and the right-hand side are isomorphic, and hence the corresponding terms are derivably equal. 步. Proposition 4.3.1 Let g = N , E , r, ∣, ID and s ﹋ N . Then s ﹋ ID iff term((g )s ) = 汛 Proposition 4.3.2 If g , h ﹋ G+ and g h, then A1, A2 term(g ) = term(h ).

Proposition 4.3.3 For closed BPA drt 而 terms p and q, we have 1. if p ﹋ B (BPA drt 而 ), then A1,A2,DRT4,DRT5 term(graph( p)) = p; 2. if A1,A2,A4,A5,A6ID,A7ID,DRT1-DRT3,DRTSID, p = q, then graph( p) DCS1-DCS4,DCSID,ARTS,DRTI1-DRTI5,DRTIID,DCSTI graph(q ).

14

Theorem 4.3.4 For closed BPAdrt 而 -terms p we have A1,A2,A4,A5,A6ID,A7ID,DRT1-DRT3,DRTSID,DCS1-DCS4,DCSID, ARTS,DRTI1-DRTI5,DRTIID,DCSTI Proof. term(graph( p)) = p.

By the Elimination Theorem we have the existence of a basic term q such that A1,A2,A4,A5,A6ID,A7ID,DRT1-DRT3,DRTSID, DCS1-DCS4,DCSID,ARTS,DRTI1-DRTI5,DRTIID,DCSTI p = q.

Then we obtain from Proposition 4.3.3.2 that graph( p) graph(q ). Then, by Proposition 4.3.2, we have A1, A2 term(graph( p)) = term(graph(q )). By Proposition 4.3.3.1 we also have A1,A2,DRT4,DRT5 term(graph(q )) = q . So, A1,A2,A4,A5,A6ID,A7ID,DRT1-DRT3,DRTSID, term(graph( p)) = term(graph(q )) = q = p. DCS1-DCS4,DCSID,ARTS,DRTI1-DRTI5,DRTIID,DCSTI

4.4

Every rewrite step corresponds to a proof step

Proposition 4.4.1 Let (r, s ) be a pair of double nodes in a process graph g. Then we have A1, A2 term((g )r ) = term((g )s ). Proof. This proposition follows immediately from Proposition 4.2.2 and Proposition 4.3.2.

Proposition 4.4.2 Let r ↙ s be a manifestly inert 而 -edge in a process graph g. Let x be a closed BPA ? drt 而 term. Then 1. BPA? drt 而 2. BPAdrt 而
m m x ﹞ 考rel (term((g )r )) = x ﹞ 考rel (term((g )s )); m m x ﹞ 考rel (考rel (term((g )r )) + 糸rel ( y )) = x ﹞ 考rel (考rel (term((g )s )) + 糸rel ( y )).



Proof. We will only give the proof for the second property. The proof for the ?rst property is similar 而 (though easier). Since r ↙ s , we have ?ID(r ), and hence ?ID(s ). Then we have by Proposition 4.3.1 that 步 and therefore by Proposition 2.1.7, we have term((g )s ) = term((g )s ) + cts(汛). Two cases term((g )s ) = 汛 can be distinguished: (1) r does not have a 考 -loop, or (2) r does have a 考 -loop. We only show the derivation ? ? for the second case. Then term((g )r ) = 考rel (cts(而 ) ﹞ term((g )s ) + q ) and term((g )s ) = 考rel ( p + q ) for some basic terms p and q such that neither p nor q has a 考 -summand. Then BPAdrt而 = = = = = =
m x ﹞ 考rel (考rel (term((g )r )) + 糸rel( y )) m ? x ﹞ 考rel (考rel (考rel (cts(而 ) ﹞ term((g )s ) + q )) + 糸rel( y )) m ? ? x ﹞ 考rel (考rel (考rel (cts(而 ) ﹞ 考rel ( p + q ) + q )) + 糸rel( y )) m ? ? x ﹞ 考rel (考rel (考rel (cts(而 ) ﹞ 考rel ( p + q + cts(汛)) + q )) + 糸rel( y )) m ? x ﹞ 考rel (考rel (考rel ( p + q + cts(汛))) + 糸rel( y )) m ? x ﹞ 考rel (考rel (考rel ( p + q )) + 糸rel( y )) m x ﹞ 考rel (考rel (term((g )s )) + 糸rel ( y )).

Theorem 4.4.3 If g ↙ h, then BPA drt 而

term(g ) = term(h ).

Proof. Suppose that g ↙ h . This must be due to either the sharing of a pair of double nodes, or the contraction of a manifestly inert 而 -edge. Each of these two rewritings in turn is built up from more elementary rewritings. These are the removal of an unreachable node, the replacement of an edge by another one, or the removal of an edge. With respect to the removal of unreachable parts of process graphs we have that the original graph and the resulting graph are isomorphic since unreachable nodes are not taken into account. 而 For the sharing of a pair of double nodes (r, s ) or the contraction of a manifestly inert 而 -edge r ↙ s the u following cases can be distinguished: (1) r has no incoming edges, (2) r does have an incoming edge t ↙ r u u and s does not have an incoming edge t ↙ s , or (3) r has an incoming edge t ↙ r and s has an incoming u edge t ↙ s . For double nodes we give the derivations for the second case and for manifestly inert 而 -edges we give the derivations for the third case: 15

? Let (r, s ) be a pair of double nodes in g such that r has an incoming edge t ↙ r and such that s u does not have an incoming edge t ↙ s . In the case that u ﹋ A而 , we have that for some basic term p: if t does not have a 考 -loop, then term((g )t ) = cts(u ) ﹞ term((g )r ) + p and term((h )t ) = cts(u ) ﹞ ? term((h )s ) + p, or, if t does have a 考 -loop, then term((g )t ) = 考rel (cts(u ) ﹞ term((g )r ) + p) and ? term((h )t ) = 考rel (cts(u ) ﹞ term((h )s ) + p). Furthermore we have by construction that (g )s (h )s , and therefore by Proposition 4.3.2, A1, A2 term((g )s ) = term((h )s ). Since (r, s ) is a pair of double nodes we have from Proposition 4.4.1 that A1, A2 term((g )r ) = term((g )s ). Combining these gives us, in the case that t does not have a 考 -loop: BPAdrt而 = = = = and in the other case: BPAdrt而 = = = = term((g )t ) cts(u ) ﹞ term((g )r ) + p cts(u ) ﹞ term((g )s ) + p cts(u ) ﹞ term((h )s ) + p term((h )t ),

u

term((g )t ) ? 考rel (cts(u ) ﹞ term((g )r ) + p) ? 考rel (cts(u ) ﹞ term((g )s ) + p) ? 考rel (cts(u ) ﹞ term((h )s ) + p) term((h )t ).

If, on the other hand u = 考 , then we have that for some basic term p: term((g )t ) = 考rel (term((g )r )) + p and term((h )t ) = 考rel (term((h )s )) + p. Please note that t cannot have a 考 -loop since every node may have at most one outgoing 考 -edge. We have, by construction, (g )s (h )s , and therefore by Proposition 4.3.2 also A1, A2 term((g )s ) = term((h )s ). Finally, since (r, s ) is a pair of double nodes we have by Proposition 4.4.1 that A1, A2 term((g )r ) = term((g )s ). Combining these gives us: BPAdrt而 term((g )t ) = 考rel (term((g )r )) + p = 考rel (term((g )s )) + p = 考rel (term((h )s )) + p = term((h )t ). ? Let r ↙ s be a manifestly inert 而 -edge in g such that r has an incoming edge t ↙ r and such that s u also has an incoming edge t ↙ s . Then, since t cannot have two outgoing 考 -edges, we have u ﹋ A而 . Two cases are distinguished: t does not have a 考 -loop and t does have a 考 -loop. First, suppose that t does not have a 考 -loop. Then, we have that for some basic term p: term((g )t ) = cts(u ) ﹞ term((g )r ) + cts(u ) ﹞ term((g )s ) + p and term((h )t ) = cts(u ) ﹞ term((h )s ) + p. Furthermore, we have by construction that (g )s (h )s , and therefore by Proposition 4.3.2 that A1, A2 term((g )s ) = term((h )s ). Since 而 r ↙ s is a manifestly inert 而 -edge, we have by Proposition 4.4.2 that BPAdrt而 cts(u ) ﹞ term((g )r ) = cts(u ) ﹞ term((g )s ). Combining these gives us: BPAdrt 而 = = = = = term((g )t ) cts(u ) ﹞ term((g )r ) + cts(u ) ﹞ term((g )s ) + p cts(u ) ﹞ term((g )s ) + cts(u ) ﹞ term((g )s ) + p cts(u ) ﹞ term((g )s ) + p cts(u ) ﹞ term((h )s ) + p term((h )t ).
而 u

Second, suppose that t does have a 考 -loop. Then, we have that for some basic term p: term((g )t ) = ? ? (cts(u ) ﹞ term((h )s ) + p). Fur(cts(u ) ﹞ term((g )r ) + cts(u ) ﹞ term((g )s ) + p) and term((h )t ) = 考rel 考rel thermore, we have by construction that (g )s (h )s , and therefore by Proposition 4.3.2 that A1, A2 而 term((g )s ) = term((h )s ). Since r ↙ s is a manifestly inert 而 -edge, we have by Proposition 4.4.2 that

16

BPAdrt而

cts(u ) ﹞ term((g )r ) = cts(u ) ﹞ term((g )s ). Combining these gives us: BPAdrt 而 = = = = = term((g )t ) ? 考rel (cts(u ) ﹞ term((g )r ) + cts(u ) ﹞ term((g )s ) + p) ? 考rel (cts(u ) ﹞ term((g )s ) + cts(u ) ﹞ term((g )s ) + p) ? 考rel (cts(u ) ﹞ term((g )s ) + p) ? 考rel (cts(u ) ﹞ term((h )s ) + p) term((h )t ).

Theorem 4.4.4 (Completeness) BPA drt 而 is a complete axiomatization of rooted branching tail bisimilarity on process graphs. Proof. Let p and q be arbitrary closed BPAdrt而 terms. Suppose that graph( p)? rbtgraph(q ). Then we must prove that BPAdrt而 p = q . Let g and h be the unique normal forms with respect to ↙ of graph( p) and graph(q ) respectively. Then, by Theorem 4.2.6, we ?nd g ?rbt graph( p)? rbt graph(q )? rbt h . By Theorem 4.2.4 it follows that g and h must be in normal form in the sense of Section 3.4. Then, by Theorem 3.4.6, we have g h . Thus, by Proposition 4.3.2, we have BPAdrt而 term(g ) = term(h ). Also, by Theorem 4.3.4, we have BPAdrt 而 p = term(graph( p)) and BPAdrt而 term(graph(q )) = q . By Theorem 4.4.3, we have BPAdrt 而 term(graph( p)) = term(g ) and BPAdrt而 term(h ) = term(graph(q )). Combining these gives us BPAdrt 而 p = term(graph( p)) = term(g ) = term(h ) = term(graph(q )) = q .

5 Additional Operators
In this section we will consider some extensions of BPAdrt而 . First a simple notion of time free projection will be introduced. This operator is useful when relating a speci?cation without timing information to a speci?cation with timing information. Also, an operator for parallel composition with communication is de?ned.

5.1

Time Abstraction

We have embedded the time free theory into the discrete time theory. We call a process time free if it can be generated from the constants ats(a ), ats(汛), ats(而 ) and the operators +, ﹞. In this section, we de?ne an operator that throws away all timing information, so that the image of a discrete time closed term will always be a time free term. This operator is called time abstraction or time free projection, and is denoted by 羽tf (see [13]). We present axioms in Table 6, operational rules in Table 7. All axioms in Table 6 are sound with respect to strong and rooted branching tail bisimulation on the term model. From these axioms one can easily derive 羽tf (ats(a )) = ats(a ). 步 = ats(汛) 羽tf (汛) 羽tf (cts(a )) = ats(a ) 羽tf (考rel (x )) = 羽tf (x ) 羽tf (x + y ) = 羽tf (x ) + 羽tf ( y ) 羽tf (x ﹞ y ) = 羽tf (x ) ﹞ 羽tf ( y ) ? 羽tf (考rel (x )) = 羽tf (x )

Table 6: Axioms for time abstraction (a ﹋ A而 汛 ).

5.2

Merge with Communication

The extension of the theory BPAdrt 而 with parallel composition, with or without communication, can be done along the lines of [4]. We present the extension with parallel composition with communication. In fact the axioms presented in this paper are almost identical to those presented in [4]. The only differences are that 17

羽tf (x ) ↙ 羽tf (x ) x ↙ x , 羽tf (x ) ↙ x 羽tf (x ) ↙ x
a 考 a

x↙x
a

a

羽tf (x ) ↙

x↙

a


a




羽tf (x ) ↙ 羽tf (x )
a



x ↙ x , 羽tf (x ) ↙ a ﹟ 羽tf (x ) ↙



Table 7: Operational rules for time abstraction (a ﹋ A而 ). some minor mistakes are corrected (see [24]). The additional syntax has binary operators (merge), (left merge), and | (communication merge) and unary operators ? H (encapsulation, for H ? A), and 而 I (abstraction, for I ? A). We present axioms for ACPdrt而 in Table 8 and Table 9. The operational rules are exactly those given in [4] and are therefore omitted. We assume given a partial, commutative and associative communication function 污 : A ℅ A ↙ A. x y=x y+ y x +x |y 步=汛 步 x 汛 步 步 x =汛 汛 (x + y ) z = x z + y z cts(a ) (x + cts(汛)) = cts(a ) ﹞ (x + cts(汛)) cts(a ) ﹞ x ( y + cts(汛)) = cts(a ) ﹞ (x ( y + cts(汛))) 考rel (x ) (考rel ( y ) + 糸rel (z )) = 考rel(x y) 步=汛 步 x |汛 步|x =汛 步 汛 cts(a ) | cts(b ) = cts(污 (a , b)) if de?ned cts(a ) | cts(b ) = cts(汛) otherwise cts(a ) | cts(b ) ﹞ x = (cts(a ) | cts(b)) ﹞ x cts(a ) ﹞ x | cts(b) = (cts(a ) | cts(b)) ﹞ x cts(a ) ﹞ x | cts(b) ﹞ y = (cts(a ) | cts(b)) ﹞ (x (x + y ) | z = x | z + y | z x | ( y + z) = x | y + x | z 考rel (x ) | (糸rel (z ) + cts(汛)) = cts(汛) (糸rel ( y ) + cts(汛)) | 考rel(z ) = cts(汛) 考rel (x ) | 考rel (z ) = 考rel (x | y )

y)

Table 8: Axioms for parallel composition in ACPdrt而 (a ﹋ A而 ).

步 =汛 步 ? H (汛) ? H (cts(a )) = cts(a ) ? H (cts(a )) = cts(汛) ? H (x + y ) = ? H (x ) + ? H ( y ) ? H (x ﹞ y ) = ? H (x ) ﹞ ? H ( y ) ? H (考rel (x )) = 考rel (? H (x ))

if a ﹋ H if a ﹋ H

步 =汛 步 而 I (汛) 而 I (cts(a )) = cts(a ) 而 I (cts(a )) = cts(而 ) 而 I (x + y ) = 而 I (x ) + 而 I ( y ) 而 I (x ﹞ y ) = 而 I (x ) ﹞ 而 I ( y ) 而 I (考rel (x )) = 考rel (而 I (x ))

if a ﹋ I if a ﹋ I

Table 9: Axioms for renaming operators in ACPdrt 而 (a ﹋ A而 ). Proposition 5.2.1 We mention the following identities which are useful in the calculations to come: 1. 2. 3. 4. 5. 考rel (x ) 考rel ( y ) = 考rel (x y ); ats(a ) ﹞ x y 肋 = ats(a ) ﹞ (x y 肋 ); cts(a ) ﹞ x 考rel ( y ) = cts(a ) ﹞ (x 考rel ( y )); cts(a ) ﹞ x 考rel ( y ) = cts(a ) ﹞ (x 考rel ( y )); ats(a ) ﹞ x cts(b) ﹞ y = cts(a ) ﹞ (x cts(b) ﹞ y ); 18

6. 7. 8. 9. 10.

ats(a ) | ats(b) = ats(c ) if 污 (a , b) = c, and ats(a ) | ats(b) = ats(汛) otherwise; ats(a ) ﹞ x | ats(b) ﹞ y = (ats(a ) | ats(b)) ﹞ (x y ); ats(a ) ﹞ x | cts(b ) ﹞ y = (cts(a ) | cts(b)) ﹞ (x y ); ? H (ats(a )) = ats(a ) if a ﹋ H , and ? H (ats(a )) = ats(汛) if a ﹋ H ; 而 I (ats(a )) = ats(a ) if a ﹋ I , and 而 I (ats(a )) = ats(而 ) if a ﹋ I .

Proposition 5.2.2 The following identity, useful in veri?cations, can be proved for all closed terms x,y: cts(a ) ﹞ (cts(而 ) ﹞ (x + cts(汛)) ( y + cts(汛))) = cts(a ) ﹞ ((x + cts(汛)) ( y + cts(汛))).

5.3

Some Simple Calculations: Communicating Buffers

In this section, we give some simple calculations in order to illustrate the use of our discrete time theory. In the setting with unbounded start delay instead of time iteration these calculations can be found in [5]. We keep formulas compact by writing a instead of cts(a ) and a instead of ats(a ) (this is in line with notation used in [2, 13]). The communication format follows the so-called standard communication function. Suppose we have given two ?nite sets, the set of messages or data D , and the set of ports P . For each d ﹋ D and i ﹋ P , we have atomic actions ri (d ), si (d ), ci (d ) (denoting receive, send and communicate d along i ) and the only de?ned communications are 污 (ri (d ), si (d )) = 污 (si (d ), ri (d )) = ci (d ). In time free process algebra, there is the following standard speci?cation of a one-item buffer with input port i and output port j : Bi j = ri (d ) ﹞ s j (d ) ﹞ B i j

d ﹋D

A straightforward calculation (see e.g. [7], page 106) shows that the composition of two such buffers in sequence gives a two-item buffer. In the following, we consider three timed versions of this buffer. In each case, only one input per time slice is possible. We can de?ne a channel that allows one input in every time slice, and outputs with no delay, with input port i and output port j by the following recursive equation: Ci j =
? We see C i j = 考rel 糸rel C i j

d ﹋D

ri (d ) ﹞ s j (d ) ﹞ 考rel C i j

= Ci j



. With H = {r2 (d ), s2 (d ) | d ﹋ D } we can derive:

? H C 12 = ? H C 12 =
d ﹋D

C 23 C 23 + ? H C 23 C 12 + ? H C 12 | C 23 C 23


? H r1 (d ) ﹞ s2 (d ) ﹞ 考rel C 12

+ + =

d ﹋D

? H r2 (d ) ﹞ s3 (d ) ﹞ 考rel C 23

C 12



d ,e ﹋ D

? H r1 (d ) ﹞ s2 (d ) ﹞ 考rel C 12 | r2 (e) ﹞ s3 (e) ﹞ 考rel C 23 C 23 +
d ﹋D

d ﹋D

r1 (d ) ﹞ ? H s2 (d ) ﹞ 考rel C 12 汛 ﹞ ? H s2 (d ) ﹞ 考rel C 12

汛 ﹞ ? H s3 (d ) ﹞ 考rel C 23

C 12

+ =

d ,e ﹋ D

s3 (e) ﹞ 考rel C 23 C 23 + ? H C 23 19 s2 (d ) ﹞ 考rel C 12

d ﹋D

r1 (d ) ﹞ ? H s2 (d ) ﹞ 考rel C 12

+ ? H s2 (d ) ﹞ 考rel C 12 | C 23 =
d ﹋D

+汛 s2 (d ) ﹞ 考rel C 12

r1 (d ) ﹞ 汛 +

e﹋ D

? H r2 (e) ﹞ s3 (e) ﹞ 考rel C 23

+ = = =

e﹋ D

? H s2 (d ) ﹞ 考rel C 12 | r2 (e) ﹞ s3 (e) ﹞ 考rel C 23 s3 (d ) ﹞ 考rel C 23 考rel C 23 C 23 .

d ﹋D d ﹋D d ﹋D

r1 (d ) ﹞ 汛 + 汛 + c2 (d ) ﹞ ? H 考rel C 12 r1 (d ) ﹞ c2 (d ) ﹞ s3 (d ) ﹞ ? H 考rel C 12 r1 (d ) ﹞ c2 (d ) ﹞ s3 (d ) ﹞ 考rel ? H C 12

Next, we put I = {c2 (d ) | d ﹋ D } and obtain the following recursive equation: 而 I ? ? H C 12 C 23 = r1 (d ) ﹞ s3 (d ) ﹞ 考rel 而 I ? ? H C 12 C 23 .

d ﹋D

We see that the composition behaves again as a no-delay channel, with input port 1 and output port 3. It is interesting to see what happens if we change the previous speci?cation slightly. Consider Di j = ri (d ) ﹞ 考rel s j (d ) ﹞ D i j .

d ﹋D

This speci?cation describes a buffer with capacity one and delay between input and output of one time unit. The composition ? H D 12 D 23 (with H as above) satis?es the following recursive speci?cation: X Xd = = r1 (d ) ﹞ 考rel c2 (d ) ﹞ X d , r1 (e) ﹞ 考rel s3 (d ) ﹞ c2 (e) ﹞ X e
e﹋ D

d ﹋D e﹋ D

+ 考rel s3 (d ) ﹞ X +

r1 (e) ﹞ s3 (d ) ﹞ 考rel c2 (e) ﹞ X e

(for d ﹋ D ).

Hiding the internal communications, we obtain 而I (X ) =
d ﹋D e﹋ D

r1 (d ) ﹞ 考rel (而 I ( X d )) , r1 (e) ﹞ 考rel s3 (d ) ﹞ 而 I ( X e )
e﹋ D

而I (X d ) =

+ 考rel s3 (d ) ﹞ 而 I ( X ) +

r1 (e) ﹞ s3 (d ) ﹞ 考rel (而 I ( X e )) .

The composition denotes a buffer with capacity two and delay of two time units. Now, we apply the time abstraction operator, and obtain the following speci?cation: 羽tf ? 而 I ( X ) =
d ﹋D

r1 (d ) ﹞ 羽tf ? 而 I ( X d ) ,
e﹋ D

羽tf ? 而 I ( X d ) = s3 (d ) ﹞ 羽tf ? 而 I ( X ) +

r1 (e) ﹞ s3 (d ) ﹞ 羽tf ? 而 I ( X e ) .

This is exactly the result of the time free calculation on page 106 of [7] (after abstraction). We ?nd that the following remarkable equation holds for the buffers D i j , but not for the other variants of buffers we discuss: ? H 羽tf D 12 羽tf D 23 = 羽tf ? ? H D 12 20 D 23 .

Finally, we drop the restriction in the previous speci?cation that output must occur before the next input. We obtain the following speci?cation: Eij = Eij .

d ﹋D

ri (d ) ﹞ 考rel s j (d )

Now, the composition satis?es the following recursive speci?cation: Y0
1 Yd 2 Yd 3 Yde

=

2 = c2 (d ) ﹞ Yd +

d ﹋D

1 r1 (d ) ﹞ 考rel Yd , e﹋ D

3 r1 (e) ﹞ c2 (d ) ﹞ 考rel Yde

(for d ﹋ D ), +
e﹋ D 3 r1 (e) ﹞ 考rel Yde

= 考rel s3 (d ) ﹞ Y 0 +

e﹋ D

r1 (e) ﹞ s3 (d ) ﹞ 考rel Ye1
f ﹋D

(for d ﹋ D ),

2 = s3 (d ) ﹞ Ye1 + c2 (e) ﹞ s3 (d ) ﹞ Yd +

r1 ( f ) ﹞ s3 (d ) ﹞ 考rel Ye3f (for d , e ﹋ D ).

+

f ﹋D

r1 ( f ) ﹞ c2 (e)

s3 (d ) ﹞ 考rel Ye3f

After abstraction, we obtain the following speci?cation for Z 0 = 而 I Y 0 : Z0
1 Zd 2 Z de

=

= 考rel s3 (d ) ﹞ Z 0 +
1 = s3 (d ) ﹞ Z e + f ﹋D

d ﹋D

1 r1 (d ) ﹞ 考rel Z d , 1 r1 (e) ﹞ s3 (d ) ﹞ 考rel Z e

2 r1 ( f ) ﹞ s3 (d ) ﹞ 考rel Z e f

e﹋ D

+

(for d , e ﹋ D ).

e﹋ D

2 r1 (e) ﹞ 考rel Z de

(for d ﹋ D ),

Again, the delay between input and output is two time units, but now, it is possible that three data elements are present in the system at the same time.

6 Absolute and Parametric Timing
6.1 Discrete Time Process Algebra with Absolute Timing
We present a version of the theory in the previous section using absolute timing, where all timing is related to a global clock. We start with constants fts(a ), denoting a in the ?rst time slice (a ﹋ A汛而 ), followed by immediate termination. Besides, we have operators +, ﹞ as before. In addition, we have the absolute discrete time unit delay 考abs , that increments all timing in its scope. Thus, 考abs (fts(a )) denotes a in the second time slice. In the axioms we use the absolute value operator | |. This operator turns out to be the identity for all processes using absolute timing only: it initializes a process in the ?rst time slice. Note that in the term 考abs (fts(a )) ﹞ fts(汛), after execution of the a in slice 2, an immediate deadlock will occur. This term is different from 考abs (fts(a ) ﹞ fts(汛)), where after the execution of a in slice 2, further activity in this slice can take place (of a parallel process). We conclude that in the absolute time theory, the immediate deadlock constant 步 is necessary. The axiomatization of BPAdat adds the axioms of Table 10 to the axioms A1-5, A6ID, A7ID 汛 (see Table 1). The extension with delayable actions is similar to the relative time case. Here, we see a large advantage of the time iteration operator over the unbounded start delay operator. Again, we can ?nd BPA而 汛 as an SRM speci?cation by using the interpretation of a as atstau(a ). The extension with parallel composition can be found along the same lines as for the relative time case (see [6]). ? The principle RSP(DAT) can be used to prove identities for 考abs : y = x + 考abs ( y ) ?
? y = 考abs (x )

RSP(DAT).

21

考abs (x ) + 考abs ( y ) = 考abs (x + y ) 步 = 考abs (x ﹞ 汛) 步 考abs (x ) ﹞ 汛 考abs (x ) ﹞ (糸abs ( y ) + z ) = 考abs (x ) ﹞ z 考abs (x ) ﹞ 考abs ( y ) = 考abs (x ﹞ | y |) fts(汛) ﹞ x = fts(汛) 步 = fts(汛) 考abs (汛) fts(a ) + fts(汛) = fts(a ) 考abs (x ) + fts(汛) = 考abs (x ) ? ? 考abs (x ) = x + 考abs (考abs (x )) ? ats(a ) = 考abs (fts(a ))

步 =汛 步 糸abs(汛) 糸abs(fts(a )) = fts(a ) 糸abs(x + y ) = 糸abs (x ) + 糸abs( y ) 糸abs(x ﹞ y ) = 糸abs (x ) ﹞ y 糸abs(考abs (x )) = fts(汛) 步 =汛 步 汛 |fts(a )| = fts(a ) | x + y | = |x | + | y | |x ﹞ y | = |x | ﹞ y |考abs (x )| = 考abs (| x |)

Table 10: Axioms of BPAdat (a ﹋ A而 ). The operational rules are more complicated in this case, as we have to keep track of which time slice we are in, we have to keep track of the global clock. The pair x , n denotes x in the (n + 1)st time slice. The operational rules for the absolute value operator are trivial. For the operational rules for the constants fts(a ) 步 and the operators +, ﹞, 考abs we refer to [6]. Operational rules for 糸abs , 考 ? , ats(a ) (a ﹋ A而 ) (a ﹋ A而 ) and 汛 abs are presented in Table 11.
a

糸abs (x ), 0 ↙ x , 0 ID( 糸abs (x ), n + 1 )
a ? 考abs (x ), n a

x, 0 ↙ x , 0
a

﹟ ,0 a ﹟ 糸abs(x ), 0 ↙ , 0 x, 0 ↙
a

ID( x , 0 ) ID( 糸abs (x ), 0 ) ats(汛), n ↙ ats(汛), n + 1
? ? 考abs (x ), n ↙ 考abs (x ), n + 1 考 考

ats(a ), n ↙

a

﹟ ,n

ats(a ), n ↙ ats(a ), n + 1 x, n ↙
a



x, n ↙ x , n


a

+k ↙ x ,n + k

? 考abs (x ), n

+k ↙

,n ﹟

,n + k

Table 11: Operational rules for BPAdat (a ﹋ A而 ). We also have to adapt the de?nition of bisimulation. A strong bisimulationrelation is a symmetric binary relation R on P ℅ IN such that (u ﹋ A而 考 , a ﹋ A而 ): 1. if R ( s , n , s , n ), then n = n and if ID( s , n ), then ID( s , n ); u u 2. if R ( s , n , t , n ) and s , n ↙ s , n , then there is a term t such that t , n ↙ t , n and R ( s , n , t , n ); a ﹟ a ﹟ 3. if R ( s , n , t , n ) and s , n ↙ , n , then t , n ↙ , n . We say process expressions x and y are strongly (tail) bisimilar, denoted x ? y , if there exists a strong bisimulation relation with R ( x , 0 , y , 0 ). A branching tail bisimulation relation is a binary relation R on P ℅ IN such that (u ﹋ A而 考 , a ﹋ A而 ): 1. if R ( s , n , s , n ), then n = n and if ID( s , n ), then ID( s , n ); (u ) u 2. if R ( s , n , t , n ) and s , n ↙ s , n , then there are terms t ?, t such that t , n ? t ? , n ↙ ? t , n and R ( s , n , t , n ), R ( s , n , t , n ); ﹟ a ﹟ a 3. if R ( s , n , t , n ) and s , n ↙ , n , then there is a term t such that t , n ? t , n ↙ ,n and R ( s , n , t , n ).

22

We say process expressions x and y are branching tail bisimilar, denoted x ? bt y , if there exists a branching tail bisimulation relation with R ( x , 0 , y , 0 ). Process expressions x and y are rooted branching tail bisimilar, denoted x ? rbt y , if there exists a branching tail bisimulation relation with R ( x , 0 , y , 0 ), that is strong for all pairs that can be reached from x , 0 , y , 0 by just performing time steps. Axioms for the silent step are comparable to the ones for relative time. The model of closed process expressions modulo rooted branching tail bisimilarity satis?es the axioms in Table 12. x ﹞ (fts(而 ) ﹞ (糸abs ( y ) + z + fts(汛)) + 糸abs ( y )) = x ﹞ (糸abs ( y ) + z + fts(汛)) x ﹞ (fts(而 ) ﹞ (糸abs ( y ) + z + fts(汛)) + z ) = x ﹞ (糸abs ( y ) + z + fts(汛)) x ﹞ (考abs (fts(而 ) ﹞ ( y + fts(汛))) + 糸abs (z )) = x ﹞ (考abs ( y + fts(汛)) + 糸abs(z )) ? ? ? x ﹞ 考abs (fts(而 ) ﹞ 考abs (糸abs ( y ) + 糸abs(z ) + fts(汛)) + 糸abs( y )) = x ﹞ 考abs (糸abs ( y ) + 糸abs (z ) + fts(汛))

Table 12: Axioms for BPAdt 而 .

6.2

Parametric Time

In this section we integrate the absolute time and the relative time approach. All axioms presented in the previous sections are still valid for all parametric time processes. We obtain a ?nite axiomatization, that allows an elimination theorem. As a consequence, we can expand expressions like cts(a ) fts(b ), cts(a ) (fts(b) + ats(汛)). We follow [6], where we introduced the operators , the (relative) time spectrum combinator, and ?, the spectrum tail operator. The absolute value operator can also be called the spectrum head operator. P Q is a process that, when initialized in the ?rst time slice, behaves as | P |; when initialized in slice n + 1 its behaviour is determined by Q as follows: initialize in slice n thereafter apply 考abs . The process ?( X ) computes a process such that X = | X | ?( X ). For a parametric discrete time process we have the time spectrum sequence | X |, |?( X )|, ?2 ( X ) , ﹞ ﹞ ﹞ . For each in?nite sequence ( Pn )n﹋IN one may imagine a process P with |?n ( P ) | = Pn though not all such P can be ?nitely expressed. The theory BPAdpt unites the theories BPAdrt and BPAdat together with the additional axioms in Table 13. We extend with delayable actions, to BPAdpt, as indicated in [6]. We can de?ne: |cts(a )| = fts(a ) |考rel (x )| = 考abs (|?(x ) |) |糸rel(x )| = 糸abs(|x |) 考abs (x ) = 考abs (| x |) 糸abs(x ) = 糸abs(| x |) |x y | = |x | ?(x y ) = y x = |x | ?(x ) 步 =汛 步 ?(汛) ?(cts(a )) = cts(a ) ?(x + y ) = ?(x ) + ?( y ) ?(x ﹞ y ) = ?(x ) ﹞ ?( y ) ?(考rel (x )) = 考rel (?(x )) ?(糸rel (x )) = 糸rel (?(x )) 步 ?(fts(a )) = 汛 ?(考abs (x )) = |x | 步 ?(糸abs (x )) = 汛 考abs (x ) ﹞ y = 考abs (x ﹞ ?( y ))

Table 13: Additional axioms of BPAdpt (a ﹋ A而 ). ? x is an absolute time process iff BPAdpt x = |x |; ? x is an relative time process iff BPAdpt x = ?(x ). X = |X | |?( X ) |

Each BPAdpt process expression can be written in the form . . . ?n ( X ) 23 ?n+1 ( X ).

One can reduce each |?n ( X )| to a BPAdat -term and if n is suf?ciently large, we can write ?n+1 ( X ) without any 考abs or fts(a ), so it will be in the relative time signature. We call (| X |, |?( X ) |, ?2 ( X ) , . . . ) the time spectrum expansion sequence (TSS) of X . Note that we obtain the following spectrum expansion for the 糸rel operator: 糸rel (x ) = 糸abs (x ) 糸rel(?(x )).

For further details, we refer to [6]. Now the axioms introduced for silent steps in relative and absolute time are valid in parametric time as well.

7 Concluding Remarks
We presented axioms for discrete time process algebra with silent step in branching bisimulation semantics. A small difference with previously published work is that we use time iteration instead of unbounded start delay and that the conditional axiom for silent step is replaced by an unconditional one. For the ?rst version, relative discrete time process algebra, we have given soundness and completeness results with respect to the term model and the graph model (exploiting the isomorphy of those two structures). From this completeness result we can conclude that the principle RSP(DRT) that is used for deriving equalities concerning time iteration can be replaced by axioms. We have given several embeddings of the time free theories BPA汛 and BPA而 汛 in the discrete time theories BPAdrt and BPAdrt而 respectively. The extension of the relative discrete time theories with additional operators such as time abstraction, merge with communication, encapsulation and abstraction follows along the same lines as in the time free theory. Some calculations regarding communicating buffers illustrate the use of the relative discrete time theory. Finally, an outline is given for de?ning absolute and parametric time versions of discrete time process algebra. An interesting topic for future research is obtaining soundness and completeness results for the absolute and parametric time process algebras as presented in this paper. The authors expect that, at least for the absolute time version, a similar approach should give these results. With respect to parametric time process algebra a lot of work has to be done. We have reasons to believe that the theory is sound, but a major open question is whether the theory is complete. Also issues relating to the applicability of the theory have to be investigated.

References
[1] J. C. M. Baeten and J. A. Bergstra. Real time process algebra. Formal Aspects of Computing, 3(2):142每 188, 1991. [2] J. C. M. Baeten and J. A. Bergstra. Discrete time process algebra (extended abstract). In W.R. Cleaveland, editor, CONCUR*92, Third International Conference on Concurrency Theory, volume 630 of Lecture Notes in Computer Science, pages 401每420, Stony Brook, 1992. Springer-Verlag. [3] J. C. M. Baeten and J. A. Bergstra. On sequential composition, action pre?xes and process pre?x. Formal Aspects of Computing, 6(3):250每268, 1994. [4] J. C. M. Baeten and J. A. Bergstra. Discrete time process algebra with abstraction. In H. Reichel, editor, FCT*95, International Conference on Fundamentals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 1每15, Dresden, 1995. Springer-Verlag. [5] J. C. M. Baeten and J. A. Bergstra. Some simple calculations in relative discrete time process algebra. In E. H. L. Aarts, H. M. M. ten Eikelder, C. Hemerik, and M. Rem, editors, Simplex Sigillum Veri, pages 67每74. Eindhoven University of Technology, 1995. Liber Amicorum dedicated to prof.dr. F. E. J. Kruseman Aretz. 24

[6] J. C. M. Baeten and J. A. Bergstra. Discrete time process algebra. Formal Aspects of Computing, 8(2):188每208, 1996. [7] J. C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990. [8] T. Basten. Branching bisimilarity is an equivalence indeed! 58(1):141每147, 1996. Information Processing Letters,

[9] J. A. Bergstra and P. Klint. The discrete time Toolbus. In M. Wirsing and M. Nivat, editors, Algebraic Methodology and Software Technology (AMAST*96), volume 1101 of Lecture Notes in Computer Science, pages 286每305, Munich, 1996. Springer-Verlag. [10] J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Control, 60(1/3):109每137, 1984. [11] J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37(1):77每121, 1985. [12] J. A. Bergstra and C. A. Middelburg. A process algebra semantics of 耳 SDL. Technical Report LGPS 129, Utrecht University, Department of Philisophy, 1995. [13] S. H. J. Bos and M. A. Reniers. The I2 C-bus in discrete-time process algebra. Science of Computer Programming, 1996. To appear. [14] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560每599, 1984. [15] R. J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555每600, 1996. [16] J. F. Groote. Speci?cation and veri?cation of real time systems in ACP. In L. Logrippo, R. L. Probert, and H. Ural, editors, Protocol Speci?cation, Testing and Veri?cation, volume 10 of Proc. IFIP WG 6.1 Tenth International Symposium, pages 261每274, Ottawa, 1990. North-Holland. [17] M. Hennessy and T. Regan. A temporal process algebra. Technical Report 2/90, University of Sussex, 1990. [18] A. S. Klusener. Models and Axioms for a Fragment of Real Time Process Algebra. PhD thesis, Eindhoven University of Technology, 1993. [19] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980. [20] R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall International, 1989. [21] F. Moller and C. Tofts. A temporal calculus of communicating systems. In J. C. M. Baeten and J. W. Klop, editors, CONCUR*90 每 Theories of Concurrency: Uni?cation and Extension, volume 458 of Lecture Notes in Computer Science, pages 401每415, Amsterdam, 1990. Springer-Verlag. [22] X. Nicollin and J. Sifakis. The algebra of timed processes, ATP: Theory and application. Information and Computation, 114(1):131每178, 1994. [23] G. M. Reed and A. W. Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 58:249每261, 1988. [24] M. A. Reniers and J. J. Vereijken. Completeness in discrete-time process algebra. Technical Report CSR 96/15, Eindhoven University of Technology, Department of Computing Science, 1996. [25] C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. Nordic Journal of Computing, 2(2):274每302, 1995.

25


婝翑妀蟈諉
載嗣眈壽恅紫:
載嗣眈壽梓ワ:
厙桴華芞

恅紫訧蹋僕砅厙 nexoncn.com copyright ©right 2010-2020﹝
恅紫訧蹋僕砅厙囀暌棚奜讕蝤畏觬陎硊裔蹅肢翕芛﹝email:zhit325@126.com