The sequence of direct test which can be performed will be build up from the direct test relation⇒G holding through an A∈Gbetween configurations, with each BL-expression being a possible start configuration. Configurations are expressions from CL, which is almost like BL with ∆ extended with † (a symbol distinct from those of ∆). Intuitively
† represents the extinct action. Formally CL is defined to be the least set C satisfying:
† ∈C BL⊆C
E0;E1 ∈C if E0 ∈C and E1 ∈BL E0kE1 ∈C if E0, E1 ∈C
The construction of CL reflects the idea that control cannot pass ; before all previous actions are extinct.
Example: ak(†;b)∈CL but † ⊕a6∈CL and a; (†;b)6∈CL.
We shall often prove properties by induction on the structure of an E ∈ CL. Strictly speaking we then first prove the property for expressions from BLand then look at†and sequential/ parallel composition afterwards. This implies that e.g., E =E0 ;E1 shall be treated two times with the only difference that for the first time we can assume E0 not to contain †. We will therefore treat these cases together except at rare occasions where the distinction is crucial. The same applies for E =E0 kE1.
So⇒G is actually a subset ofCL×G×CL. IfhE, A, E0i ∈ ⇒Gwe write this asE ⇒A GE0. One can think of this asE can evolve to E0 when the direct test A is performed.
We shall follow DeNicola [Nic87] and Hennessy [Hen88a] when defining ⇒G. Hennessy does this in an extended labelled transition system by means of a relation >−→, which reflects the step of an internal computation, and by a relation −→G for an external computation step corresponding to a direct test. The slight deviation from Hennessy in defining the relation,>−→, for internal steps are manily due to differences in the languages considered.
Definition 7.2.1 >−→ ⊆CL×CL and −→G⊆CL×G×CLare defined as the least relations satisfying the following axioms and inference rules.
a−→a G † E0 −→A G E00 E0;E1 −→A G E00 ;E1 E0 −→A G E00
E0kE1 −→A G E00 kE1 E1kE0 −→A G E1kE00
E0 −→A0 G E00, E1 −→A1 G E10, A0×A1 ∈G E0kE1 A−→0×A1G E00 kE10
†;E >−→E E0 >−→E00 E0;E1 >−→E00 ;E1 E0⊕E1 >−→E0
E0⊕E1 >−→E1
† kE >−→E Ek †>−→E
E0 >−→ E00 E0kE1 >−→ E00 kE1 E1kE0 >−→ E1kE00
In this way an internal step either resolves an internal nondeterministic choice or removes an extinct action. The idea of using >−→ for other purposes than resolving internal nondeterministic choices is not inconsistent with Hennessy—he also uses >−→ to unfold recursive definitions.
Notice that the definition of −→A G is well-defined because of the premise A0×A1 ∈G in the rule for a composed action and because we assume ∆⊆G (fora −→a G†).
Example: Let G be a set of direct test containing a2. Then
a;bka;d−→a2 G †;bk †;d >−→ †;bkd−→d G †;bk †>−→bk †−→b G † k †>−→ † The test relation, ⇒A G, is now defined as >−→∗−→A G>−→∗ and for a sequence of direct tests s∈G∗ and E, E0 ∈CL we define:
E ⇒s G E0, s=A1A2. . .An iff
∃E1,. . ., En ∈CL∃A1,. . ., An ∈G, n ≥0.
E =A⇒1 GE1 =A⇒2 G . . .=A⇒n G En=E0 where the case n = 0 means E >−→∗ E0.
With this notion of sequences of direct test it follows that any maximal sequence, s, of direct is of the form E ⇒s G †, so we can define our basic operational preorder:
Definition 7.2.2 <∼G ⊆BL×BL
E0 <∼G E1 iff
E0 ⇒s G † impliesE1 ⇒s G† for all s∈G∗ 2 Notice that as expected the equivalence of <∼G, <∼>∼G, identifies a; (b⊕c) and a;b⊕a;c.
Throughout this section we will fix G and so will leave it out as a subscript of −→G and
⇒G except when dealing with certain G’s. This will also be the case in the remaining sections whenever the direct test setG in question is clear from the context.
Given a concrete sequence of internal and external steps, written ⇒s , we define its length as the total number of steps in the sequence. If E under this sequence evolves to E0 we also write this as E ⇒s E0. This allows us to make induction on the length of a concrete sequence.
As a first result notice that by an easy induction on the length of ⇒s (where ⇒s is a concrete sequence for E0 ⇒s E00) one can prove:
Proposition 7.2.3 Suppose E ∈BL, E0, E1 ∈CL and E0 ⇒s E00. Then
• E0;E ⇒s E00 ;E
• E0kE1 ⇒s E00 kE1
• E1kE0 ⇒s E1kE00
Since we only have a combinator for internal nondeterministic choice a natural ques-tion to raise is whether a processes reacts successful to a test iff one of the syntactic
“controlled behaviours” of it does. Such a behaviour can be regarded as a deterministic process (∈DBL) or configuration (∈DCL)—deterministic in the sense that no internal nondeterminism is explicit present in the form of a ⊕-combinator, but of course their might be indirectly as in aka. A behaviour would in Petri net terms correspond to a possible process/ concurrent behaviour of a Petri net system—more accurately it would correspond to to an occurrence net of a place/ transition net [BF88]. Formally:
Definition 7.2.4 Behaviours
The set of configurationbehaviours, DCL, is defined to be the ⊕-free expressions of CL.
Similar DBL=DCL∩BL is the set of process behaviours.
The behaviours of a configuration expression is given by the map Beh :CL−→ P(DCL) defined as follows:
Beh(†) ={†}
Beh(a) ={a}
Beh(E0;E1) = Beh(E0) ; Beh(E1) Beh(E0⊕E1) = Beh(E0)∪Beh(E1) Beh(E0kE1) = Beh(E0)kBeh(E1)
where Beh(E0) ; Beh(E1) denotes {E00 ;E10 |E00 ∈Beh(E0), E10 ∈Beh(E1)}. Similar for k. 2 Notice that E ∈BL implies Beh(E)⊆DBL.
Because BL ⊆ CLwe from the proposition below deduce a positive answer to the ques-tion whether a processes reacts successful to a test iff one of the syntactic “controlled behaviours” of it does.
Proposition 7.2.5 For a configuration E ∈CLand s∈G∗ we have E ⇒ †s iff ∃F ∈Beh(E). F ⇒ †s
Because in general † ∈Beh(E) iff E =† this proposition is immediate from:
Proposition 7.2.6 Given s∈G∗ and configurations E and F0. Then:
∃E0 ⇒s E0, F0 ∈Beh(E0) m ∃F ∈Beh(E). F ⇒s F0
Proof Both implication are proven by induction on the length of ⇒s using the following
three propositions. 2
Proposition 7.2.7 Given configurations E and F0 we have:
∃E0. E >−→E0, F0 ∈Beh(E0)
⇓ ∃F ∈Beh(E). F >−→∗ F0
Proof By induction on the structure ofE.
E =† or E =a: In both cases E cannot do any internal step so the implication holds vacuously.
E =E0;E1: According to the definition of >−→there are two subcases:
E0 = †: Then E0 = E1 and F0 ∈ Beh(E1). Now Beh(E) = †; Beh(E1) so F :=
†;F0 ∈Beh(E) and of courseD >−→F0.
E0 >−→ E10: I.e., E0 = E00 ; E1, so F ∈ Beh(E0) means F0 = F10 ;F1 for some F00 ∈ Beh(E00), F1 ∈ Beh(E1). By induction ∃F0 ∈ Beh(E0). F0 >−→∗ F00. By proposition 7.2.3 this implies F :=F0;F1 >−→∗ F00 ;F1 = F0. Since Fi ∈ Beh(Ei) for i= 0,1 we also have F ∈Beh(E).
E =E0⊕E1: By definition of >−→ then either E0 = E0 or E0 = E1. W.l.o.g. assume E0 = E0. Then F ∈ Beh(E0) means F0 ∈ Beh(E0) ⊆ Beh(E0) ∪ Beh(E1) = Beh(E0⊕E1) so we can just chooseF =F0 since F0 >−→0 F0.
E =E0kE1: Again according to the definition of>−→there are four possibilities. If the internal step E0 kE1 >−→ E0 derives from one of the axioms for k the proof goes similar/ symmetric as in the first subcase of E =E0;E1 and if it derives from one of the inference rules for k it goes as in the second subcase.
2
Proposition 7.2.8 If E and F0 are configurations then:
∃F ∈Beh(E). F >−→F0
⇓ ∃E0. E >−→∗ E0, F0 ∈Beh(E0)
Proof By induction on the structure ofE.
E =† or E =a: Then Beh(E) = {E} and F = E. Since E of this form can do no internal step the implication holds trivially.
E =E0;E1: F ∈Beh(E0;E1) meansF =F0;F1 where Fi ∈Beh(Ei) for i= 0,1.
E0 =†: Since F0 ∈ Beh(†) implies F0 =† we see that F >−→F0 implies F0 =F1. LetE0 =E1. We have E =†;E1 >−→E0 with F0 ∈Beh(E0) as desired.
E0 6= †: Now F0 ∈ Beh(E0), E0 6= † implies F0 6= †. Inspecting the definition of
>−→we see thatF >−→F0 must be due toF0 >−→F00,F0 =F00;F1. By hypothesis of induction there exists E00 such that E0 >−→∗ E00 and F00 ∈ Beh(E00). Then also E >−→∗ E00 ;E1 and F0 ∈Beh(E00) ; Beh(E1). Choosing E0 =E00 ;E1 we are done.
E =E0⊕E1: F ∈ Beh(E) means F ∈ Beh(E0) or F ∈ Beh(E1). Suppose w.l.o.g.
F ∈Beh(E0). Then by induction∃E0. E0 >−→∗ E0, F0 ∈ Beh(E0). By definition of
>−→ then also E0⊕E1 >−→E0 >−→∗ E0 and thereby E >−→∗ E0. E =E1kE1: Has similar/ symmetric subcases to those ofE =E0;E1.
2
By an easy induction on the structure ofE one can prove:
Proposition 7.2.9 For configurations E and F0 we have:
∃E0. E −→A E0, F0 ∈Beh(E0) m
∃F ∈Beh(E). F −→A F0