Show description

In this construction, x is a local variable, so (x : B → P (x)) = (y : B → P (y)) The set B defines the initial menu of the process, since it gives the set of actions between which a choice is to be made at the start. Examples X8 A process which at all times can engage in any event of its alphabet A αRUNA = A RUNA = (x : A → RUNA ) In the special case that the menu contains only one event e, (x : {e} → P (x)) = (e → P (e)) since e is the only possible initial event. 1 Introduction 11 Choice between three or more alternatives can be similarly expressed.

1), (P / s) denotes the whole subtree whose root lies at the end of the path labelled by the symbols of s. 1 is denoted by VMC / in2p, small, out1p The following laws describe the meaning of the operator /. , ∀ s : traces(P ) • ∃ t • (P / (s t ) = P ) STOP is trivially cyclic; but if any other process is cyclic, then it also has the desirable property of never stopping. 4 X2) (coin → VMS ), (choc → VMCT ), (around → CT7 ) For example, in the initial state of choc → VMCT only a chocolate is obtainable, but subsequently whenever choc is obtainable a choice of toffee is also possible; consequently none of these subsequent states is equal to the initial state.

From this it follows that is a trace of every process up to the moment in which it engages in its very first event. Furthermore, if (s t ) is a trace of a process up to some moment, then s must have been a trace of that process up to some earlier moment. Finally, every event that occurs must be in the alphabet of the process. These three facts are formalised in the laws L6 ∈ traces(P ) L7 s t ∈ traces(P ) ⇒ s ∈ traces(P ) L8 traces(P ) ⊆ (αP )∗ There is a close relationship between the traces of a process and the picture of its behaviour drawn as a tree.