Linking Operational Semantics and Algebraic Semantics for a Probabilistic
Timed Shared-Variable Language
Huibiao Zhua , Fan Yanga , Jifeng Hea , Jonathan P. Bowenb , Jeff W. Sandersc , Shengchao Qinda Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, Chinab Centre for Applied Formal Methods, London South Bank University, London SE1 0AA, UK

c International Institute for Software Technology, United Nations University, Macau SAR, Chinad School of Computing, Teesside University, Middlesbrough, TS1 3BA, UK

Abstract
Complex sfotware systems typically involve features like time, concurrency and probability, and probabilistic computations are playing an increasing role. However it is currently challenging to formalize languages incorporating all
those features. Recently the language PTSC has been proposed to integrate probability and time with shared-variableconcurrency [56, 59], where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper investigates the link between the operational and algebraic semantics of PTSC,
highlighting both its theoretical and practical aspects.
The link is obtained by deriving the operational semantics from the algebraic, an approach which may be understood as establishing soundness of the operational semantics with respect to the algebraic semantics. Algebraic laws
are provided which suffice to convert any PTSC program into a form consisting of a guarded choice or an internal
choice between programs which are initially deterministic. That form corresponds to a simple execution of the program, so it is used as a basis for an operational semantics. In that way, the operational semantics is derived from thealgebraic, with transition rules resulting from the derivation strategy. In fact the derived transition rules and the derivation strategy are shown to be equivalent, which may be understood as establishing completeness of the operationalsemantics with respect to the algebraic semantics.
That theoretical approach to the link is complemented by a practical one, which animates the link using Prolog. The link between the two semantics proceeds via head normal form. Firstly, generation of head normal form is
explored, in particular animating the expansion laws for probabilistic interleaving. Then the derivation of the operational semantics is animated using a strategy which exploits head normal form. The operational semantics is also
animated. Those animations, which again supports to claim soundness and completeness of the operational semantics
with respect to the algebraic, are interesting because they provide a practical demonstration of the theoretical results.
Keywords: PTSC, Opeartional Semantics, Algebraic Semantics, Semantic Linking, Head Normal Form, Animation

1. Introduction
Probabilistic computations play an increasingly important role in solving various problems [45]. As a consequenceof that, a number of probabilistic languages have been proposed [11, 12, 14, 21, 35, 36, 37, 42, 43, 44]. In addition
to probability, complex software systems can often involve important features like real-time [41] and shared-memory
based concurrency. The shared-variable mechanism is typically used for communications among components runningin parallel, e.g. the case for Java and the case for the Verilog hardware description language. However, it proves tobe rather challenging to formalise a system comprising those features [20, 51, 52, 55]. A formal model integrating
probability, real-time and shared-variable concurrency would be highly expected by system designers as it can offer
better support for the specification and modelling of complex software systems.
In our previous work [56, 59], we have proposed an integrated language PTSC equiped with probability, time andshared-variable concurrency features, to facilitate the specification of complex software systems. In the language,
the probability feature is reflected by the probabilistic nondeterministic choice, probabilistic guarded choice andthe probabilistic scheduling of actions from different concurrent components in a program. In that work, we have
Preprint submitted to The Journal of Logic & Algebraic Programming

February 28, 2011

formalized an operational semantics for this language, on top of which an abstract bisimulation relation has been
defined and several algebraic laws have been derived for program equivalence.
The PTSC language has recently been used to specify a circuit in the register-transfer level [39, 40]. The circuittakes two integers as the input and sums up them as the output, where the register containing one of the inputs may be
faulty. The algebraic laws proposed for the PTSC language have also been employed to verify that an implementationof the circuit with probabilistic behavior conforms to the probabilistic specification.
As described in Hoare and He’s Unifying Theories of Programming (abbreviated as UTP) [27], three different
mathematical models are often used to represent a theory of programming, namely, the operational, the denotational,
and the algebraic ones [46, 50, 28]. Each of these representations has its distinctive advantages for theories of programming. For instance, the operational semantics provides a set of transition rules that model how a program performs
step by step. The correctness of the transitions of an operational semantics is essential for applying the operationalsemantics in further study. The algebraic semantics is well suited in symbolic calculation of parameters and stricturesof an optimal design. The algebraic approach has been successfully applied in provably-correct compilation. A comprehensive theory of programming should offer all these semantic models and should ensure that all the models are
pairwise consistent [27].
For our proposed language PTSC, we have previously defined the operational semantics from which a set ofalgebraic laws are derived. To ensure the consistency between the operational and algebraic semantics, a link should
be constructed between the two models, so that one model can be derived from the other. In this paper, we tackle
this problem by constructing a link from the algebraic semantics to the operational semantics. We first derive an
operational semantics from the algebraic semantics. If the derived operational semantics is the same as our previous
achieved one [56, 59], we can conclude that our operational semantics is consistent with the algebraic semantics.
This can be considered as the soundness exploration of operational semantics from the algebraic viewpoint. The
investigation can be understood as the inverse work of [56, 59] and a significant contribution in unifying theories of
PTSC [27].
In order to support the derivation of operational semantics from algebraic semantics, a derivation strategy is required to be defined. Therefore, we introduce the concept of head normal form, where very program can be expressed
as either a guarded choice or the summation of a set of processes which are deterministic initially. Our definition forthe derivation strategy is based on head normal form. We study the algebraic laws for PTSC, which supports the definition of head normal form. Based on the derivation strategy, we can achieve a transition system (i.e., an operationalsemantics). There remains a question concerning the equivalence of the derivation strategy and the derived transition
system. The advantage of this equivalence is that we can use either the derivation strategy or the derived transition
system when working on the application of operational semantics. Further, this result also indicates the completenessof our operational semantics from the viewpoint of algebraic semantics.
For the derived operational semantics, if we can have an executed version, the correctness of the operationalsemantics can be checked from various test results. Moreover, if we can have the animation of the derivation strategy,
we can also model the execution of a program. From various test examples, if the execution results of the above two
animation approaches are the same, we can claim that the derivation strategy is the same as the derived operationalsemantics. This supports to claim that our derived operational semantics is sound and complete with respect to headnormal form (i.e., algebraic semantics in general) from the practical viewpoint. Therefore, in this paper we also
consider the animation of the linking between operational semantics and algebraic semantics for PTSC. The logic
programming language Prolog [8] is used for the development. In order to support the animation, we also consider
the mechanical generation of the head normal form for each program in Prolog, where twenty-five parallel expansion
laws are animated.
The remainder of this paper is organized as follows. Section 2 introduces our language PTSC. Section 3 lists a
set of algebraic laws, where every program can be represented as either a guarded choice, or the summation of a setof processes which are initially deterministic. We also give the concept of head normal form which is the key point
for studying the link between the operational semantics and algebraic semantics. We explore how to generate thealgebraic laws via Prolog in section 4, especially the parallel expansion laws. Meanwhile, section 4 also calculates
the head normal form of a program via Prolog. Section 5 investigates the derivation of the operational semantics
from the algebraic semantics. We give the derivation strategy and show that a transition system (i.e., the operationalsemantics) can be derived by strict proof. Section 5 also studies the equivalence of the derivation strategy and thederived transition system. Section 6 is about the animation of operational semantics from two viewpoints. Firstly,2

for our derived operational semantics in section 5.3 from the transition system viewpoint, we explore the animationof the achieved operational semantics. All transition rules are expressed in the form of Prolog style. Secondly, we
also explore the generation of operational semantics from the viewpoint of derivation strategy via head normal form
mechanically. Section 7 discusses the related work about probability, time, shared-variable concurrency and semantic
linking. Section 8 concludes the paper.
2. The PTSC Language
Shared-variable concurrency has long been used as an alternative to message passing in describing systems composed of concurrently interacting components. Originally termed ‘multiprogramming’ in the 1960s and 70s [15, 16]
its subtleties have continued to provoke research [5, 6, 10, 47]. It finds recent application in the analysis of threads,
for instance in the Java memory model [34], and for reasoning about Verilog [20].
The purpose of this paper is to continue the study of the language PTSC which integrates probability and timewith shared-variable concurrency. PTSC has been designed to express the scheduling of threads, incorporating concurrency and nondeterminism as well as probability and time. It is thus well suited to discrete event simulation where
those features are present, as is the case in a growing number of distributed protocols which employ random-number
generators to facilitate choice between alternatives [38].
Our language PTSC integrates of probability, time and shared-variable concurrency. It has the following syntactical elements:
P ::= Skip | x := e | if b then P else P | while b do P | @b P | #n P | P ; P | P u P | P u p P | P k p P
Note that:(1) Assignment, x := e, is atomic, so that no action can interleave between reading the variables involved in theexpression e and writing the result of e to x. The vacuous assignment x := x is abbreviated Skip. Similar toa conventional language, if b then P else Q stands for the conditional, whereas while b do P stands for theiteration. P ; Q stands for sequential composition.
(2) The event guarded program, @b P, is enabled when the guard b holds in which case P may be scheduled;otherwise it is disabled (i.e. not able to be scheduled) and waits. Here b a Boolean condition. Since we model
closed systems, time advances only when the guard b is false. Between evaluation of b and commencing
execution of P, other commands may be scheduled. In this paper we take the understanding that @b is atomic.
When @b appears in a guarded choice (to be introduced slightly later), it is also atomic. For #n P, after n timeunits elapse, process P can be scheduled. Time advances in unit steps.
(3) u stands for the nondeterministic choice, where u p stands for the probabilistic nondeterministic choice. P u p Q
indicates that the probability for P u p Q to behave as P is p, where the probability for P u p Q to behave as Q is1−p.
(4) The mechanism for parallel composition P k p Q is a shared-variable interleaving model with probability feature(i.e., probabilistic interleaving model). If process P can perform an atomic action, P k p Q has conditional
probability p to do that atomic action. On the other hand, if process Q can perform an atomic action, P k p Q
has conditional probability 1−p to perform that action.
Probabilistic interleaving models the situation in which priority is given to an enabled action. For example if one
thread performs assignments a1 ; a2 and another performs assignment a3 then the result of a scheduler which chooses
a3 before the other assignments three quarters of the time, between them a little less than a quarter of the time, andafter them the rest of the time, can be expressed as a probabilistic interleaving(a1 ; a2) k 14 a3 = (a3 ; a1 ; a2) k 43 [ a1 ; ((a2 ; a3) k 14 (a3 ; a2))]
Indeed, by repeated expansion, the left-hand side gives the interleaving a3 ; a1 ; a2 with probability 3/4, the interleaving a1 ; a3 ; a2 with probability 3/16 and the remaining interleaving a1 ; a2 ; a3 with probability 1/16.
In order to facilitate algebraic reasoning, we enrich our language with a guarded choice [17] in our language.
As our parallel composition has probability feature, the guarded choice also shares this feature. Guarded choice isclassified into five types.
The first type is composed of a set of assignment-guarded components.
3

(gtype-1) []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )}Note that I and Ji stand for finite index sets. The notation b&(x := e) P stands for the assignment guarded component.
Assignment x := e will be executed only when Boolean condition b is satisfied. After that, the subsequent behaviour
can be expressed as process P. For the construct choice, its form can be expressed as choicem∈M (bm &(xm := em ) Pm ).
Its Boolean conditions should be pairwise disjoint or exhaustive, i.e., it should satisfy the condition below.
W( m∈M bm = true) and (∀m1 , m2 • (m1 , m2 ) ⇒ ((bm1 ∧ bm2 ) = f alse))
The meaning of the choice construct is that at any moment there is one and only one Boolean condition to be satisfied,
which indicates that the corresponding assignment can be scheduled.
For the notation [p]choicem∈M (bm &(xm := em ) Pm ), it means that the probability for the choice construct to be performed is p; i.e., if the Boolean condition in one assignment guarded component is satisfied, the probability forselecting the corresponding assignment is p. The first type of guarded choice is composed of a set of choice constructwith probability. For (gtype − 1) above, all pi (i ∈ I) should satisfy the condition +i∈I pi = 1
The second type is composed of a set of event guarded components. It waits any of the guards to be fired. If one
guard is satisfied, the subsequent behaviour for the whole process will be followed by its subsequent behaviour of thesatisfied component.
(gtype-2) []i∈I {@bi Pi }The third type is composed of one time delay component. Initially, it cannot do anything except letting time advance one unit.
(gtype-3) []{#1 R}
The fourth type is the guarded choice composition of the first and second type of guarded choice 1 .
(gtype-4) []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )}[][]k∈K {@ck Qk }If there exists one ck (k ∈ K) being satisfied currently, then the event @ ck is fired and the subsequent behaviour is Qk .
If there is no satisfied ck , any of the assignment guarded components can be scheduled provided that the corresponding
Boolean condition is true.
The fifth type is the compound of the second and third type of guarded choice.
(gtype-5) []i∈I {@bi Pi }[]{#1 R}
Currently, if there exists i (i ∈ I) such that bi is satisfied, then the subsequent behaviour of the whole guarded choice is
as Pi . On the other hand, if there is no i (i ∈ I) such that bi is satisfied currently, then the whole guarded choice cannot
do anything initially except letting time advance one unit. The subsequent behaviour is the same as the behaviour ofR.
A choice construct contains a set of assignment guarded components. An assignment guarded component can bescheduled at the current time point provided that the corresponding Boolean condition is satisfied. And the executionof assignment is instantaneous. On the other hand, a delay component might be scheduled to make time advance one
unit. These facts indicate that, if a choice construct and a time delay component appear in the same set of a guarded
choice, the time delay component will not have a chance to be scheduled. Therefore, we assume that there is no typeof guarded choice composing of the first and third type of guarded choice, which indicates that guarded choice canonly have the above five types of guarded choice.
Example 2.1 Let P = []{ [0.7]choice( true&(x := 5) P1 ) ,[0.3]choice( (x > 2)&(x := x) P2 , (x ≤ 2)&(x := x) P3 )1 The notation []{P , · · · , P }[][]{Q , · · · , Q } stands for []{P , · · · , P , Q , · · · , Q }
1
n
1
m
1
n
1
m

4

}
For program P, it is of the form of the first type guarded choice, which has two choice constructs. The probabilityof selecting the first choice construct is 0.7, whereas the probability of selecting the second choice construct is 0.3.
For the first choice construct, it has only on component, which means that assignmnet x := 5 will be scheduled andsubsequent behaviour is P1 . For the second choice construct, it has two components. The execution of the first one
is under condition x > 2 and the execution of the second one is under condition x ≤ 2. The second choice construct
behaves the same as if (x > 2) then P1 else P2 . Therefore, this process selects x := 5 with probability 0.7, followedby process P1 . It can also select the conditional statement with probability 0.3.
¤
3. Algebraic Semantics and Head Normal Form
This section studies the algebraic semantics for PTSC, where every program can be expressed as a guarded choiceor the summation of a set of processes which are initially deterministic. We also introduce the concept of headnormal form in this section, which is the key point for exploring the link between operational semantics and algebraic
semantics.
3.1. Algebraic Semantics for Guarded Choice
Now we explore the algebraic laws for guarded choice. The order of the guarded components in a guarded choice
can be re-arranged.
(gchoice-1) []{C1 , · · · · · · , Cn } = []{Ci1 , · · · · · · , Cin }, where, i1 , · · · , in is a permutation of 1, · · · , n.
The assignment guarded component can be eliminated if its Boolean condition is always false.
(gchoice-2) []{[p]choice{false&(x := e) P, G1 }, G2 } = []{[p]choice{G1 }, G2 }Two assignment guarded components can be combined into a single one if the assignment guards and their subsequent
processes are the same. This can be represented by combining two Boolean conditions together as disjunction.
(gchoice-3) []{[p]choice{b1 &(x := e) P, b2 &(x := e) P, G1 }, G2 } = []{[p]choice{(b1 ∨ b2 )&(x := e) P, G1 }, G2 }Two event guarded components can be combined into a single one if their subsequent processes are the same. This
combination can be represented by an or-compound guard.
(gchoice-4) []{@b P, @c P, G} = []{@(b ∨ c) P, G}
The self-assignment can be represented by any program variables.
(gchoice-5) []{[p]choice{b&(x := x) P, G1 }, G2 } = []{[p]choice{(b&(y := y) P, G1 }, G2 }Two same choice components can be combined into a single one. The associated probability for the combined component is the addition of the probabilities of the two separate ones.
(gchoice-6) []{[p]choice{G1 }, [q]choice{G1 }, G2 } = []{[p + q]choice{G1 }, G2 }3.2. Algebraic Semantics for Sequential Constructs
In this section we list the laws for sequential constructs. The laws below indicate that a sequential program can be
represented as a guarded choice. We have the following considerations.
Assignment can be expressed as a guarded choice composed of only one guarded component with probability 1.
(assign-1) x := e = []{ [1]choice{true&(x := e) ε} }Skip = []{ [1]choice{true&(x := x) ε} }Here, ε stands for the empty process.
An event guard can be expressed as a guarded choice composed of one event guard component. Similar consideration
also applies to time delay guard.
(guard-1) @b = []{@b ε}(delay-1)#1 = []{#1 ε}#n = []{#1 #(n − 1)}, where n > 1
5

Conditionals can also be expressed as a guarded choice composed of only one choice component with probability 1.
The choice component has two assignment guarded sub-components. Iteration has a similar structure.
(cond-1) if b then P else Q = []{ [1]choice{b&(x := x) P, ¬b&(x := x) Q} }(itera-1) while b do P = []{ [1]choice{b&(x := x) (P ; while b do P), ¬b&(x := x) ε} }If program P is expressed as a guarded choice, its sequential composition with Q is also a guarded choice, where eachcomponent is the combination of the corresponding component in P with Q via the function seq defined below.
(seq-2) Assume P = []{C1 , . . . , Cn }, then P ; Q = []{seq(C1 , Q), . . . , seq(Cn , Q)}.
where,

[p]choice j∈J {b j &(x j := e j ) seq1(P j , Q)}
if C = [p]choice j∈J {b j &(x j := e j ) P j }




0
@b seq1(P , Q)
if C = @b P0
seq(C, Q) =d f  #1 seq1(P0 , Q)
if C = #1 P0(
P; Q
if P , εseq1(P, Q) =d fQ
if P = εThe definition of seq(C, Q) is based on the type of guarded component C. The subsequent behaviour after the corresponding guard can be expressed via function seq1. Here seq1(X, Q) stands for Q if X is the empty process. Otherwise,
it stands for X; Q.
3.3. Algebraic Laws for Parallel Construct
Probabilistic parallel composition is not purely symmetric and associative. Its symmetry and associativity rely on
the change of the associated probabilities as well.
(par-1) P k p Q = Q k1−p P(par-2) P k p (Q kq R) = (P k x Q) ky R,

where, x = p/(p + q − p × q) and y = p + q − p × q.

For (par-2), the formulae for x and y indicate that the probability for an assignment in the left hand side to bescheduled is the same as the probability of the corresponding assignment in the right hand side. For example, for an
assignment in process Q of the left hand side process, its probability is (1− p)×q. For the corresponding assignment inprocess Q of the right hand side process, its probability is (1− x)×y = (1− p/(p+q− p×q))×(p+q− p×q) = (1− p)×q.
Now we give the definition for the function par, which can be used in reducing the number of parallel expansion
laws relating to empty process. It can also be used to reduce the number of transition rules for parallel composition.
P k p1 Q
if P , ε and Q , ε







if P , ε and Q = ε Ppar(P, Q, p1 ) =d f Q
if P = ε and Q , ε





ε
if P = ε and Q = ε
In what follows we give a collection of parallel expansion laws. As mentioned earlier, there exist five typesof guarded choice. To take into account a parallel composition of two arbitrary guarded choices, we end up withtwenty-five different expansion laws. Due to the above symmetric law (associated with probability), these twenty fiveexpansion laws can be reduced into fifteen different laws. Here we highlight some expansion laws with the rest listed
in the appendix.
For a parallel process, if the first component is an assignment-guarded choice and the second component is also
an assignment-guarded choice, the scheduling rule is that any assignment could be scheduled with the associatedprobability provided that its Boolean condition is satisfied. Law (par-3-1) below depicts this case.
(par-3-1) Let P = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )} and Q = []k∈K {[qk ] choicel∈Lk (bkl &(xkl := ekl ) Qkl )}Then
P kr Q = []i∈I {[r × pi ] choice j∈Ji (bi j &(xi j := ei j ) par(Pi j , Q, r)}[][]k∈K {[(1 − r) × qk ] choicel∈Lk (bkl &(xkl := ekl ) par(P, Qkl , r)}6

If the first component is an assignment-guarded choice and the second component is an event-guarded choice,the behaviour of the parallel composition can be described as the guarded choice of a set of assignment-guarded
components and a set of event-guarded components. This case is presented in law (par-3-2).
(par-3-2) Let P = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )} and Q = []k∈K {@ck Qk }Then
P kr Q = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) par(Pi j , Q, r)}[][]k∈K {@ck par(P, Qk , r)}If both of the two components are event-guarded choices, there are several scenarios. If one guard from thefirst component is triggered but no guards from the second component are triggered, the subsequent behaviour is theparallel composition of the remaining part of the first component with the second component. If two guards fromboth components are triggered simultaneously, the subsequent behaviour is the parallel composition of the remaining
processes of both sides. This is illustrated in law (par-3-6).
(par-3-6) Let P = []i∈I {@bi Pi } and Q = [] j∈J {@c j Q j }Then
P kr Q = []i∈I {@(bi ∧ ¬c) par(Pi , Q, r)}[][] j∈J {@(c j ∧ ¬b) par(P, Q j , r)}[][]i∈I∧ j∈J {@(bi ∧ c j ) par(Pi , Q j , r)}where, b = ∨i∈I bi and c = ∨ j∈J c j
3.4. Algebraic Laws for Probabilistic Nondeterministic Choice and Nondeterministic Choice
Probabilistic nondeterministic choice can be expressed as a guarded choice comprising two assignment guarded
components. The probability for the selection of one guarded component is p, whereas the probability for the selection of another component is 1 − p.
(pnonde-1) P u p Q = []{ [p]choice{true&(x := x) P}, [1 − p]choice{true&(x := x) Q}}
L
Now we introduce a new construct, called summation, which is denoted as{P1 , · · · , Pn }, where each Pi is initially deterministic. For summation, the selection among all components Pi is nondeterministic. For a process whose
outmost structure is not parallel structure, it is called initially deterministic if its outmost structure is not nondeterministic choice. On the other hand, if the outmost structure of a process is parallel composition, it is called initiallydeterministic if both of its two parallel components (i.e., left hand side and right hand side of parallel composition)
are initially deterministic.
L
For example, let P =expressed as {x := 1; x := 2} andLx := 1 u x := 2 and Q = y := 1 u y := 2. Then P can be L
Q can be expressed as{y := 1, y := 2}. Further, P kr Q can be expressed as{x := 1 kr y := 1, x := 1 kr y :=2, x := 2 kr y := 1, x :=
2
k
y
:=
2}
and
every
elementinthissummation
setisinitially
deterministic. Further, weLhave the law below for
.
L
L
L
( -1)
{P1 , · · · , Pn } ={Pi1 , · · · , Pin }, where, i1 , · · · , in is the permutation of 1, · · · , n.
For u, it also shares the symmetric law and associative law. Now we consider the transformation of nondeterministic choice to the form of summation.
L
L
L(nonde-1) If P ={P1 , · · · , Pn } and Q ={Q1 , · · · , Qm },then P u Q ={P1 , · · · , Pn , Q1 , · · · , Qm }The law below indicates how we can transform sequential composition into the form of summation.
LL(seq-3) If P ={P1 , · · · , Pn } ,then P ; Q ={(P1 ; Q), · · · , (Pn ; Q)}

3.5. Head Normal Form
Now we assign every program P a normal form called head normal form HF (P) [18]. Our later discussion about
relating algebraic semantics with operational semantics is based on head normal form.
7(1) HF (x := e) =d f []{ [1]choice{true&@(x := e) ε} }HF (Skip) =d f []{ [1]{true&@(x := x) ε} }(2) HF (@b) =d f []{@b ε}(3) HF (#1) =d f []{#1 ε}
HF (#n) =d f []{#1 #(n − 1)}, where n > 1(4) HF (if b then P else Q ) =d f []{ [1]choice{b&@(x := x) P, ¬b&@(x := x) Q} }(5) HF (while b do P) =d f []{ [1]choice{b&@(x := x) (P ; while b do P), &@(x := x) ε} }(6) If P is a guarded choice, then HF (P) =d f P(7) If HF (P) = []{C1 , . . . , Cn }, then HF (P ; Q) = []{seq(C1 , Q), . . . , seq(Cn , Q)}LL
If HF (P) =i∈I Pi and |I| > 1, then HF (P ; Q) =d fi∈I (Pi ; Q)
(8) HF (P u p Q) =d f []{ [p]choice{true&(x := x) P}, [1 − p]choice{true&(x := x) Q}}
L
L{P1 , · · · , Pn } and HF (Q) ={Q1 , · · · , Qn },(9) If HF (P) =Lthen HF (P u Q) =d f
{P1 , · · · , Pn , Q1 , · · · , Qn }The head normal form of parallel composition can be expressed as the summation of a set of processes which are
initially deterministic. We can take one component from one parallel branch and another component from anotherparallel branch. Then the guarded choice can be defined by applying the corresponding parallel expansion laws basedon the selected two components.
LL(10) If HF (P) =HF (Q) =i∈I Pi andj∈J Q j ,Lthen HF (P kr Q) =d fi∈I, j∈J (Pi kr Q j )For HF (Pi kr Q j ), it can be defined as the result of applying the parallel expansion laws for HF(Pi ) kr HF(Q j ),as illustrated in section 3.3.
Example 3.1 Let U =d f if x > 1 then P1 else P2 , V =d f y := x+1 ; Q, W =d f z := x+1 ; R, S =d f (UuV) k0.7 W
Now we consider the head normal form of HF (S ). From the definition of head normal form, we know:L
HF ((U u V) k0.7 W) = U k0.7 W
V k0.7 W
Moreover, we have:
HF (U k0.7 W)= []{ [0.7]choice{x > 1&(x := x) (P1 k0.7 W), x ≤ 1&(x := x) (P2 k0.7 W)},[0.3]choice{true&(z := x + 1) (U k0.7 R)}}HF (V k0.7 W)= []{ [0.7]choice{true&(y := x + 1) (Q k0.7 W)},[0.3]choice{true&(z := x + 1) (V k0.7 R)}}¤

From the definition of head normal form, we know that it is in the form of one step forward expansion. This can
support the derivation of operational semantics from head normal form because operational semantics also makes one
step forward for each transition.
4. Animation of Algebraic Semantics and Head Normal Form
As mentioned earlier, head normal form can be applied in linking the algebraic semantics and operational semantics. Our approach is to derive the operational semantics from algebraic semantics, which will be explored in section
8

5. In order to explore the mechanical derivation of operational semantics from algebraic semantics (i.e., automatic
derivation of operational semantics from algebraic semantics), we consider the animation of algebraic semantics andhead normal form (i.e., the simulation of algebraic semantics and automatic generation of head normal form) in thissection. The animation can be processed in Prolog.
Programs written in Prolog is composed of clauses describing relations. Rule and fact are the two types of clauses.
A rule is in the form of “H : −B1 , B2 , ..., Bn .”, with H as its head and B1 , B2 , ..., Bn as its body. This can be read as “His true if B1 and B2 and...and Bn are true”. Facts are clauses with empty body in the form of “H.”. The execution of a
Prolog program is triggered when the user proposes a query in the form “? − G1 , G2 , ..., Gn ” where Gi is a goal clause.
For variables in Prolog, if a variable begins with an underscore ( ), it can be instantiated as any value. A single
underscore, which means “any term”, is usually used to denote an anonymous variable. List in Porlog is used forholding a group of terms and is defined inductively. A list is denoted as [A|B] where A is the first element of the list
and B is the tail which is also a list. The [ ] used to terminate a list is suppressed. A list can also be in the form
[A1 , A2 , ..., An ] where all Ai are its elements separated by commas.
4.1. Generating Algebraic Laws
Now we explore the generating of algebraic laws for our probabilistic language by using animation style. Here
we mainly focus on the parallel expansion laws, which enable us to expand a probabilistic parallel composition to aguarded choice construct.
In order to animate these rules, we define the structure of the five types of probabilistic guarded choice first. We
denote the assignment guarded choices as assignGuardChoice, event guarded choices as eventGuardChoice, timedelays as timeDelay. assign event is used to represent the guarded choice composition of the assignment guarded
choice and the event guarded choice. The guarded choice composition of the event guarded choice and time delays isdenoted as event time.
For the choice construct [P]choice j∈J (b j &(V j := E j ) S j ), it can be expressed as a set of components in the formP f or b j then (V j = E j )$S j when animating. Therefore, for a guarded choice, when implementing in Prolog, the components can be of three forms, P f or EB then (V = E)$S (assignment under condition EB with probability P withsubsequent behaviour S ), @EB$S (event guard component) and #1$S (time delay component).
assignGuardChoice([[P f or EB then (V = E) $ S ]|S 0 ]) :− bool(EB), variable(V), expr(E), probability(P), assignGuardChoice(S 0 ).
eventGuardChoice([[@EB $ S ]|S 0 ]) :− bool(EB), eventGuardChoice(S 0 ).
timeDelay([[#1 $ S ]]).
assign event(S ) :− assignGuardChoice(S 1 ), eventGuardChoice(S 2 ), append(S 1 , S 2 , S ).
event time(S ) :− eventGuardChoice(S 1 ), timeDelay(S 2 ), append(S 1 , S 2 , S ).

Here, bool(EB) is defined as a set of rules in Prolog to check if EB is an legal expression in PTSC with a Boolean
value [4]. Similarly, variable(V) is use to ensure that V is in a proper form of variable and expr(E) guarantees that E
is a legal expression.
The assignGuardChoice form can be defined recursively. It indicates that the first guarded component is an assignment guarded component and the remaining components still satisfy assignGuardChoice form. The probability P
is defined as a variable whose value is a number in the range of [0,1] and its validity is checked by rule probability(P).
The eventGuardChoice indicates the event guarded choice and is defined similarly. For timeDelay, it only contains
the time delay component. For assign event, it combines the assignGuardChoice form and eventGuardChoice form
by using the append function. append(S 1 , S 2 , ...S n , S ) concatenates list S 1 , S 2 and S n into list S .
As mentioned earlier, there exist five types of guarded choice and twenty-five parallel expansion laws. Now weare ready to generate the parallel expansion laws by giving the definition for npar(S 1kR S 2 , T ). Here, T stands for the
expansion form for parallel process S 1kR S 2 by the corresponding parallel expansion laws. Firstly we simulate parallel
expansion law (par-3-1) (see page 6), which stands for the case that both of the two parallel branches are of the formof assignment guarded choice. This indicates that both of the two parallel branches are of type assignGuardChoice.
In this case, rule assign2 L and assign2 R will be called.
npar(S 1 kR S 2 , T ) :− assignGuardChoice(S 1 ), assignGuardChoice(S 2 ), assign2 L(S 1 kR S 2 , T 1 ),9assign2 R(S 1 kR S 2 , T 2 ), append(T 1 , T 2 , T ).

For S 1 kR S 2 , when S 1 and S 2 are assignment guarded choices, any assignment in S 1 and S 2 can be scheduled.
assign2 L(S 1 kR S 2 , T 1 ) generates the guarded components stored in T 1 when the assignment in S 1 is scheduled.
Meanwhile, assign2 R(S 1 kR S 2 , T 2 ) generates the guarded components stored in T 2 when the assignment in S 2 isscheduled. Their definitions can be defined recursively.
assign2 L([[P1 f or EB1 then (V1 = E1 ) $ S 1 ]] kR S 2 , [[(P1 ∗ R) f or EB1 then (V1 = E1 ) $ (S 1 kR S 2 )]]).
assign2 L([[P1 f or EB1 then (V1 = E1 ) $ S 1 ]|S 10 ]kR S 2 , T ):− assign2 L([[P1 f or EB1 then (V1 = E1 ) $ S 1 ]] kR S 2 , T 1 ), assign2 L(S 10 kR S 2 , T 2 ), append(T 1 , T 2 , T ).
assign2 R(S 1 kR [[P2 f or EB2 then (V2 = E2 ) $ S 2 ]], [[(P2 ∗ (1 − R)) f or EB2 then (V2 = E2 ) $ (S 1 kR S 2 )]]).
assign2 R(S 1 kR [[P2 f or EB2 then (V2 = E2 ) $ S 2 ]|S 20 ], T ):− assign2 R(S 1 kR [[P2 f or EB2 then (V2 = E2 ) $ S 2 ]], T 1 ), assign2 R(S 1 kR S 20 , T 2 ), append(T 1 , T 2 , T ).

Now we consider the generating and animation for the parallel expansion law that both of the two parallel branches
are of the form of event guarded choice. The law is illustrated in law (par-3-6) (see page 7).
For S 1 kR S 2 , if both S 1 and S 2 are of the form of event guarded choice, the following npar(S 1 kR S 2 , T ) generates
the event guarded components stored in T .
npar(S 1 kR S 2 , T ) :− eventGuardChoice(S 1 ), eventGuardChoice(S 2 ), event2 L(S 1 kR S 2 , T 1 ), event2 R(S 1 kR S 2 , T 2 ),event2 Both(S 1 kR S 2 , T 3 ), append(T 1 , T 2 , T 3 , T ).

From algebraic law (par-3-6) (see page 7), we know that there are three firing cases. The append function combines T 1 , T 2 and T 3 into one single list T sequentially. event2 L(S 1 kR S 2 , T 1 ) stands for the case that one event in S 1
is fired and all events in S 2 are not fired at this moment. Then the resulted event guarded components are recorded in
T1.
event2 L([[ P1 f or EB1 then ( V1 = E1 ) $ S 1 ]|S 10 ] kR S 2 , T ) :− event2 L(S 10 kR S 2 , T ).
event2 L([[#1 $ S 1 ]] kR S 2 , [ ]).
event2 L([[@EB1 $ S 1 ]] kR S 2 , [[@(EB1 ∧ B) $ (S 1 kR S 2 )]]) :− compound(S 2 , B).
event2 L([[@EB1 $ S 1 ]|S 10 ] kR S 2 , T ) :− event2 L([[@EB1 $ S 1 ]] kR S 2 , T 1 ), event2 L(S 10 kR S 2 , T 2 ), append(T 1 , T 2 , T ).

In the above definitions, compound(S 2 , B) combines all the events in S 2 in the disjunction form and stores theresult in B.
Similarly, event2 R(S 1 kR S 2 , T 2 ) stands for the case that one event in S 2 is fired and all events in S 1 are notfired at this moment. Then the resulted event guarded components are recorded in T 2 . Its definition is similar toevent2 L(S 1 kR S 2 , T 1 ).
Thirdly, event2 Both(S 1 kR S 2 , T 3 ) stands for the case that one event from S 1 and another event from S 2 are fired
simultaneously. Then the resulted event guarded components are recorded in T 3 .
event2 Both([[@ EB1 $ S 1 ]| S 10 ] kR [[#1 $ S ]], [ ]).
event2 Both([[@EB1 $ S 1 ]|S 10 ] kR [[ P2 f or EB2 then ( V2 = E2 ) $ S 2 ]|S 20 ], T ) :− event2 Both([[@EB1 $ S 1 ]|S 10 ] kR S 20 , T ).
event2 Both([[#1 $ S ]] kR [[@ EB1 $ S 1 ]| S 10 ], [ ]).
event2 Both([[ P1 f or EB1 then ( V1 = E1 ) $ S 1 ]|S 10 ] kR S 2 , T ) :− event2 Both(S 10 kR S 2 , T ).
event2 Both([[@EB1 $ S 1 ]] kR [[@EB2 $ S 2 ]], [[@(EB1 ∧ EB2 ) $ (S 1 kR S 2 )]]).
event2 Both([[@EB1 $ S 1 ]] kR [[@EB2 $ S 2 ]|S 20 ], T ):− event2 Both([[@EB1 $ S 1 ]] kR [[@EB2 $ S 2 ]], T 1 ), event2 Both([[@EB1 $ S 1 ]] kR S 20 , T 2 ), append(T 1 , T 2 , T ).
event2 Both([[@EB1 $ S 1 ]|S 10 ] kR [[@EB2 $ S 2 ]|S 20 ], T ):− event2 Both([[@EB1 $ S 1 ]] kR [[@EB2 $ S 2 ]|S 20 ], T 1 ), event2 Both(S 10 kR [[@EB2 $ S 2 ]|S 20 ], T 2 ), append(T 1 , T 2 , T ).

10

The following parallel expansion law captures the case where both of the two components are time-delay guarded
constructs. The whole process performs a time delay and then behaves as the parallel composition of the remaining
parts from both sides:(par-3-10) Let P = []{#1 R} and Q = []{#1 T }Then
P kr Q = []{#1 par(R, T, r)}

For the animation, the npar function below defines the calculating of the guarded choice for this case.
npar([[#1 $ S 1 ]] kR [[#1 $ S 2 ]], [[#1 $ (S 1 kR S 2 )]]).

We now move to the parallel composition where the first parallel branch comprises both assignment guarded components and event guarded components. The following law (par-3-14) captures the scenario where the second parallel
branch consists of event guarded components and the time-delay.
(par-3-14) Let P = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )}[][]k∈K {@bk Rk }and Q = []l∈L {@cl Ql }[]{#1 T }Then P kr Q = []i∈I {[pi ] choice j∈J (bi j &(xi j := ei j ) par(Pi j , Q, r))}[][]k∈K {@(bk ∧ ¬c) par(Rk , Q, r)}[][]l∈L {@(cl ∧ b) par(P, Ql , r)}[][]k∈K∧l∈L {@(bk ∧ cl ) par(Rk , Ql , r)}where, b = ∨k∈K bk andc = ∨l∈L cl

For S 1 kR S 2 , if S 1 is in the form of combing the assignment guarded choice and the event guarded choice and S 2
is in the form of combing the event guarded choice and the time delay choice, then time delay will not be scheduled
initially. It can only have event guarded components and assignment guarded components. We use npar(S 1 kR S 2 , T )to generate these components stored in T .
npar(S 1 kR S 2 , T ) :− assign event(S 1 ), event time(S 2 ), trans1 2(S 1 kR S 2 , T 1 ), event2 L(S 1 kR S 2 , T 2 ), event2 R(S 1 kR S 2 , T 3 ),event2 Both(S 1 kR S 2 , T 4 ), append(T 1 , T 2 , T 3 , T 4 , T ).

Here, assign event(S 1 ) and event time(S 2 ) stand for the guarded choice type of S 1 and S 2 respectively. For algebraic law (par-3-14), there are three firing cases. Therefore, event2 L, event2 R and event2 Both have also been applied.
As S 1 contains assignment guarded components, assign1 L(S 1 kR S 2 , T ) stands for the case that assignment can bescheduled first, which keeps the scheduling probability unchanged.
assign1 L([[P1 f or EB1 then (V1 = E1 ) $ S 1 ]] kR S 2 , [[P1 f or EB1 then (V1 = E1 ) $ (S 1 kR S 2 )]]).
assign1 L([[P1 f or EB1 then (V1 = E1 ) $ S 1 ]|S 10 ] kR S 2 , T ):− assign1 L([[P1 f or EB1 then (V1 = E1 ) $ S 1 ] kR S 2 , T 1 ), assign1 L(S 10 kR S 2 , T 2 ), append(T 1 , T 2 , T ).

In this section we considered the mechanical generation of algebraic laws using animation approach. Amongtwenty-five parallel expansion laws, here we only listed four of them (i.e., (par-3-1), (par-3-6), (par-3-10), (par-314)) for introducing the animation approach. The consideration for the animation of other parallel expansion laws issimilar.
4.2. Generating Head Normal Forms
For the aim of linking the algebraic semantics with operational semantics, we have introduced the concept of headnormal form for every program. In this section we explore how to generate the head normal form via animation.
For program P, we use the function below to generate the head normal form of P.
h f (P, T )11where, T stands for the head normal form of program P. Here T can be expressed as the summation of a set of guarded
choices 2 . We use a list to represent the summation.
Assignment can be expressed as a guarded choice composed of only one guarded component with probability 1.
(1) h f (V = E, [ [ 1 f or true then V = E $ epsilon ] ]). 3
The whole clause means that the head normal form of V = E is [[1 f or true then V = E $ epsilon]], which is a list
containing only one element.
Event guard can be expressed as a guarded choice composed of one event guard component. Similar consideration
also applies to time delay guard.
(2) h f (@EB, [ [ @EB $ epsilon ] ]).
h f (#1, [ [ #1 $ epsilon ] ]).
h f (#N, [ [ #1 $ #(N − 1) ] ]) :− N > 1.

Conditional can also be expressed as a guarded choice composed of two assignment guarded subcomponents withprobability 1. Iteration has similar structure.
(3) h f (i f (EB) $ S 1 else S 2 , [ [ 1 f or EB then [ ] $ S 1 ], [ 1 f or ∼ EB then [ ] $ S 2 ] ]).
h f (while (EB) $ S , [ [ 1 f or EB then [ ] $ ( S ; while EB $ S ) ], [ 1 f or ∼ EB then [ ] $ epsilon ] ]).

Here [ ] stands for the empty assignment which does nothing for state update.
The head normal form of guarded choice has the same form as the guard choice itself.
(4) h f (S , S ) :− pgc(S ).
pgc(S ) :− assignGuardChoice(S ).
pgc(S ) :− eventGuardChoice(S ).
pgc(S ) :− timeDelay(S ).
pgc(S ) :− assign event(S ).
pgc(S ) :− event time(S ).

A process may have nondeterministic behaviours. We can express a process as the summation of a set of guarded
choices. Each guarded choice can be regarded as an initially deterministic process for the whole program.
(5) h f (S 1 u S 2 , T ) :− summation (S 1 u S 2 , T ).
The summation rules are designed to differentiate nondeterministic process from the others. A nondeterministic
process will be represented by a list whose elements are the initially deterministic.
summation (L1 u L2 , T ) :− summation (L1 , T 1 ), summation (L2 , T 2 ), append (T 1 , T 2 , T ).
summation (S , [S ]).

Now we start to consider the calculation of the head normal form for sequential composition. The definition can bedone in two steps. If a process is initially deterministic, we first translate it to its head normal form and then distribute”;” to each component of it. The distribution behaviour can be done by a new function subdistr(6) h f ([ ]; Q, [ ]) :− !.
h f (S ; Q, T ) :− h f (S , S 0 ), subdistr (S 0 ; Q, T ).

Below is the definition for subdistr. Here we only list some of the whole rules.
subdistr ([ ]; , [ ]).
subdistr ([P f or EB then (V = E) $ S ]; Q, [[P f or EB then (V = E) $ (S ; Q)]]).
subdistr ([@EB $ S ]; Q, [[@EB $ (S ; Q)]]).

2 If there is only one guarded choice in the summation, the summation can also be understood as a form of guarded choice.
3 In section 4 and section 6, assignment V := E is re-written as V = E when doing the animation.

12

subdistr ([#1 $ S ]; Q, [[#1 $ (S ; Q)]]).

For a nondeterministic process, it can be transformed into a set of guarded choices. Then the sequential composition of the nondeterministic process and Q can be transformed into a summation comprising of the sequential
composition of each guarded choice and Q.
h f (S 1 u S 2 ; Q, T ) :− summation (S 1 u S 2 , S ), distr(S ; Q, T ).

For each guarded choice in the achieved new summation, the subsequent behavior after the corresponding guard
can be dealt by introducing function ”distr”.
distr ([X]; Q, [X; Q]).
distr ([X|S ]; Q, T ) :− distr ([X]; Q, T 1 ), distr (S ; Q, T 2 ), append (T 1 , T 2 , T ).

Now we consider the generating of head normal form for parallel process S 1 kR S 2 . Firstly we need to calculate thecomponents which are initially deterministic for S 1 and S 2 respectively; i.e., each initially deterministic component
is represented by a guarded choice. This can be done by using the two summation functions shown below.
(7) h f (S 1 kR S 2 , T ) :− summation(S 1 , S 10 ), summation(S 2 , S 20 ), combination(S 10 kR S 20 , T ).
In the above definition, the head normal form of S 1 kR S 2 is the summation of a set of new guarded choice via thefunction combination. Here each new guarded choice is the parallel composition of one guarded choice from S 10 andanother guarded choice from S 20 . This can be processed by using the algebraic laws (mainly function npar) in section
4. Below is the definition of function combination.
combination([X] kR [Y], T ) :− npar(X kR Y, T ).
combination([X] kR [Y|S 2 ], T ) :− combination([X] kR [Y], T 1 ), combination([X] kR S 2 , T 2 ), append(T 1 , T 2 , T ).
combination([X|S 1 ] kR [Y|S 2 ], T ) :− combination([X] kR [Y|S 2 ], T 1 ), combination(S 1 kR [Y|S 2 ], T 2 ), append(T 1 , T 2 , T ).

Example 4.1
LetP=[]{[1]choice(true&(a = 10) a = 11}
k0.2 []{{@(b = 3) b = 0, @(b = 4) b = 6}[]{#1 b = 5}}

Then the query for the head normal form of P is in the form h f (P, NF) where P is the program text we introduced above and NF is a variable storing the head normal form. Here, the program P is the parallel composition of
assignGuardChoice and event time, and its head normal form is defined using expansion law (par-3-5) (given in the
appendix).
? − h f (P, NF).
NF = [[1 f or true then a = 10 $ (a = 11 k0.2 [[@b = 3 $ b = 0], [@b = 4 $ b = 6], [#1 $ b = 5]])],[@b = 3 $ ([[1 f or true then a = 10 $ a = 11]] k0.2 b = 0)],[@b = 4 $ ([[1 f or true then a = 10 $ a = 11]] k0.2 b = 6)]]

5. Deriving Operational Semantics from Algebraic Semantics
The traditional way of defining an operational semantics is to provide a set of individual transition steps directly. In
contrast to the standard style of defining operational semantics, this section derives the operational semantics from its
algebraic semantics for our probabilistic language. This approach aims to guarantee the consistency of the operational
and algebraic semantics for our language.
5.1. Transition Types
The operational semantics of a language is represented by transition relations. In our operational model, thetransitions are expressed in the form of Plotkin’s Structural Operational Semantics (SOS) [46]:βhP, σi −→ hP0 , σ0 iwhere, P stands for the program text that remains to be executed, and σ is the current state of the program.
The transitions can be classified into four kinds:
13

(1) The first kind of transition models the execution of an atomic action with certain probability.
chP, σi −→ p hP0 , σ0 iwhere, p stands for the probability for program P to perform the execution.
(2) The second type models the transition of a time delay. Time advances in unit steps.
1hP, σi −→ hP0 , σ0 i
(3) The third type models the selection of the two components for non-deterministic choice. It can be expressed as:τhP, σi −→ hP0 , σi(4) The fourth type models the triggered case of event @ b:v

hP, σi −→ hP0 , σi5.2. Derivation Strategy
The main purpose of this section is to derive the transition system for our probabilistic language from its algebraiclaws. This approach allows the operational semantics to be derived as theorems (see section 5.3), rather than being
presented as postulates or definitions. Firstly we give the derivation strategy.
Definition 5.1 (Derivation Strategy)L
Let HF (P) =i∈I Pi .
τ(1) If |I| > 1, then hP, σi −→ hPi , σi (i ∈ I).
(2) Otherwise,c(a) If HF (P) = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )},then hP, σi −→ pi hPi j , σ[ei j /xi j ]i, if bi j (σ)v(b) If HF (P) = []i∈I {@bi Pi }, then hP, σi −→ hPi , σi, if bi (σ)
V
1hP, σi −→ hP, σi, if i∈I ¬bi (σ)1(c) If HF (P) = []{#1 R}, then hP, σi −→ hR, σi.
(d) If HF (P) = []i∈I {[pi ] choice j∈J (bi j &(xi j := ei j ) Pi j )}[][]k∈K {@ck Qk },vthen hP, σi −→ hQk , σi, if ck (σ)
chP, σi −→ pi hPi j , σ[ei j /xi j ]i, if bi j (σ) ∧ (Vk∈K ¬ck (σ))(e) If P = []i∈I {@bi Pi }[]{#1 R},v

then hP, σi −→ hPi , σi if bi (σ)
V
1hP, σi −→ hR, σi if i∈I ¬bi (σ)¤

Item (1) indicates that if a program can be expressed as the summation of a set of processes which are initiallydeterministic, the program can make a nondeterministic selection among all these processes. Item (2) considers thetransition rules for the case that a program can be expressed as a guarded choice. This can be divided into five subcases
due to the types of guarded choice.
If a program can be expressed as a guarded choice comprising a set of assignment guarded components, then the
program can execute each assignment with the associated probability provided that the corresponding Boolean condition is satisfied. If a program can be expressed as a guarded choice composed of a set of event guarded components,
any event can be triggered provided that the event is satisfied. Meanwhile, if none of these events are satisfied, time
will advance one unit. If a program can only be expressed as a guarded choice composed of the time delay component,
only time advancing can be executed.
On the other hand, if a program can be expressed as a guarded choice composed of a set of assignment guarded
components and a set of event guard components, any event can be triggered provided that the event is satisfied.
Further, if none of these events are satisfied, any assignment can be executed with the associated probability provided
that its Boolean condition is satisfied. On the other hand, time cannot advance for a program under this case.
14

Finally, if a program is expressed as a guarded choice composed of a set of assignment guarded components andthe time delay component, any event can be triggered provided that the event is satisfied. On the other hand, if noneof the events are satisfied, time can advance one unit. The subsequent behaviour after one time unit elapses is just the
behaviour followed the time delay event.
5.3. Deriving Operational Semantics by Strict Proof
This subsection aims to derive the operational semantics for all the statements according to the derivation strategy.
Therefore, our operational semantics can be understood as consistent with its algebraic semantics.
Theorem 5.2
c

(1)
(2)

hx := e, σi −→1 hε, σ[e/x]ic
hif b then P else Q , σi −→1 hP, σi, if b(σ)(3)

hif b then P else Q , σi −→1 hQ, σi, if ¬b(σ)
chwhile b do P, σi −→1 hP ; while b do P, σi, if b(σ)

cchwhile b do P, σi −→1 hε, σi, if ¬b(σ)1(4)

h#n, σi −→ h#(n − 1), σi, where n > 1.

(5)

h#1, σi −→ hε, σiv
h@b P, σi −→ hP, σi, if b(σ)(6)

h@b P, σi −→ h@b P, σi, if ¬b(σ)
chP u p Q, σi −→ p hP, σi

1

1

c

hP u p Q, σi −→1−p hQ, σi
Proof The proof can be proceeded directly from the head normal form of each program and the derivation strategy.
Here we give the proof for (6). Others are similar. The head normal form of P u p Q are below:
HF (P u p Q) =d f []{ [p]choice{true&(x := x) P}, [1 − p]choice{true&(x := x) Q}}
By the derivation strategy 2(a), we can directly get the transition rules for P u p Q.
¤
The transitions in (1)(2)(3) model the case that a program does an atomic action with probability 1. For the timedelay statement, only time advancing can be performed. For an event guard, it can be immediately fired provided thatthe Boolean condition is satisfied. However, if the Boolean condition is not satisfied, time will advance one unit. Item
(6) models the transition for probabilistic nondeterministic choice. For P u p Q, the selection of P is with probabilityp, and the selection of Q is with probability 1 − p.
We can also have the transition rules for sequential composition, which are the same as those in a traditional
programming language. The proof is based on the head normal form of sequential composition and the derivation
strategy.
Theorem 5.3
ββ

If hP, σi −→ hP0 , σ0 i, then hP; Q, σi −→ hseq1(P0 , Q), σ0 i.
In order to simplify the later proof for theLtransition rules of other constructs, we introduce a function GC(P) for
program P based on HF (P). Let HF (P) =i∈I Pi . The definition of GC(P) can be defined as below:({P}
if |I| = 1
GC(P) =d f∪i∈I {Pi } if |I| > 1
Moreover, if P is initially deterministic, GC1(P) is introduced, which contains all the guarded components in HF (P).
Further, we define two functions:τstable(hP, σi) =d f ¬( hP, σi −→ ) andv

stableE(hP, σi) =d f ¬( hP, σi −→ )15

The notation stable(hP, σi) indicates that process P cannot perform the transition representing nondeterministic choice
under state σ, while stableE(hP, σi) indicates that process P cannot perform event-triggered transitions under state.
Now we consider the derivation of the transitions for nondeterministic choice. A nondeterministic process canperform a “τ” transition and directly reach to a stable state.
Theorem 5.4
ττ(1) If hP, σi −→ hP0 , σ0 i, then hP u Q, σi −→ hP0 , σ0 iτhQ u P, σi −→ hP0 , σ0 i
τ(2) If stable(hP, σi), then hP u Q, σi −→ hP, σ0 iτhQ u P, σi −→ hP, σ0 i
Proof Here we give the proof for (1). The proof for (2) is similar.
τhP, σi −→ hP0 , σ0 i
⇒ P0 ∈ GC(P) ∧ |GC(P)| > 1⇒ P0 ∈ GC(P) ∪ GC(Q) ∧ |GC(P) ∪ GC(Q)| > 1⇒{Derivation Strategy}{Set Calculus}{Derivation Strategy}τhP u Q, σi −→ hP0 , σ0 i¤

Now we explore the derivation of the transition rules for parallel composition. The approach is based on the fourtransition types of a program.
Theorem 5.5
τ(1) (a) If hP, σi −→ hP0 , σi and stable(hQ, σi),τthen hP k p1 Q, σi −→ hpar(P0 , Q, p1 ), σi.
τhQ k p1 P, σi −→ hpar(Q, P0 , p1 ), σi.
ττ(b) If hP, σi −→ hP0 , σ, i and hQ, σi −→ hQ0 , σi,τthen hP k p1 Q, σi −→ hpar(P0 , Q0 , p1 ), σiv(2) (a) If hP, σi −→ hP0 , σi and stable(hQ, σi) and stableE(hQ, σi),v

then hP k p1 Q, σi −→ hpar(P0 , Q, p1 ), σi.
v

hQ k p1 P, σi −→ hpar(Q, P0 , p1 ), σi.
vv(b) If hP, σi −→ hP0 , σi andhQ, σi −→ hQ0 , σi,vthen hP k p1 Q, σi −→ hpar(P0 , Q0 , p1 ), σic(3) If hP, σi −→ p2 hP0 , σ0 i and stable(hx, σi) and stableE(hx, σi) (x = P, Q),cthen hP k p1 Q, σi −→ p1 ×p2 hpar(P0 , Q, p1 ), σ0 ichQ k p1 P, σi −→(1−p1 )×p2 hpar(Q, P0 , p1 ), σ0 i
11(4) If hP, σi −→ hP0 , σ0 i and hQ, σi −→ hQ0 , σ0 i and stable(hx, σi) and stableE(hx, σi) (x = P, Q),1then hP k p1 Q, σi −→ hpar(P0 , Q0 , p1 ), σ0 i.
Proof Firstly we consider the proof for 1(a). The proof for 1(b) is similar.
τhP, σi −→ hP0 , σi
⇒ P0 ∈ GC(P) ∧ |GC(P)| > 1 ∧ |GC(Q)| = 1⇒ P0 k Q ∈ GC(P k p1 Q)⇒{Derivation Strategy}{HF for Parallel Composition}{Derivation Strategy}τhP k p1 Q, σi −→ hpar(P0 , Q, p1 ), σivSecondly, we consider the proof for 2(a). As hP, σi −→ hP0 , σi, this indicates that P is stable currently. From
the assumption, we also know that Q cannot perform τ transition and v transition. We can enumerate all the parallel
expansion cases. Here we only consider the proof for the case below.
16Let P = []k∈K {[qk ] choicel∈Lk (bkl &(xkl := ekl ) Pkl )}[][]m∈M {@cm Rm }Q = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Qi j )}From the expansion laws, we know
@ck par(Rm , Q, p1 ) ∈ GC1(P k p1 Q)
This indicates that the corresponding transition can be derived from the derivation strategy.
Thirdly, we consider the proof for item (3). We use the above example case for exploring the proof.
c

From hP, σi −→ hPkl , σ, i, we can have:∀m • (cm (σ) = false) ∧ bkl (σ)(1)[qk ] choicel∈Lk (bkl &(xkl := ekl ) Pkl ) ∈ GC1(P) ∧ ∀m • (@cm Rm ) ∈ GC1(P)(2)

By the parallel expansion laws, we know:[qk × p] choicel∈Lk (bkl &(xkl := ekl ) par(Pkl , Q, p)) ∈ GC1(P k p1 Q) ∧ ∀m • (@cm par(Rm , Q, p)) ∈ GC1(P k p1 Q) (3)Based on (1) and (3), we can derive the transition rule for item (3).
Finally, we consider the proof for item (4). We use the example case below for exploration.
P = []i∈I {@bi Pi }[]{#1 R},
Q = [] j∈J {@c j Q J }[]{#1 T }From the parallel expansion law, we can have:#1par(R, T, p1 ) ∈ GC1(P k p1 Q)
This indicates that P k Q can perform the required time delay transition.

¤

For the above derived transition rules for parallel composition, transition (1)(a) stands for the case that one component makes nondeterministic choice and another component is stable. The whole process also makes a nondeterministic choice under this case. However, if both components make nondeterministic choice, then the whole process canmake nondeterministic choice and the subsequent behaviour is the parallel composition of the remaining components.
Transition (1)(b) reflects this situation.
The second type stands for the event-fired case. The analysis is similar to the transitions of type (1). Transition(3) covers the case of performing an atomic action. If process P can perform an atomic action with probability p2 ,then process P k p1 Q and Q k p1 P can also perform the same atomic action with probability p1 × p2 and (1 − p1 ) × p2
respectively.
If both components can perform a time-advancing transition, then the whole parallel process can also let timeadvance. The aspect is reflected in transition (4).
This section has considered the derivation of an operational semantics from algebraic semantics for our proposed
probabilistic language. The derivation strategy is based on the head normal form of each process. A transition system(i.e., operational semantics) has been derived for programs based on the derivation strategy by strict proof. This gives
us a way to show the consistency of the algebraic semantics and operational semantics.
5.4. Equivalence of Derivation Strategy and Transition System
In the previous subsections, we have derived a set of transition rules according to a derivation strategy. The setof transition rules can be considered as a transition system (i.e., operational semantics) for our probabilistic language.
There remains an issue to be considered. The derivation strategy may derive more transitions, compared with ourtransition system (theorems 5.2 to 5.5). We want to show that the set of transitions derived from the derivation
strategy is the same as the set of transitions generated from our transition system. If so, we can say the derivation
strategy is equivalent to the transition system.
The advantage of this equivalence result is that we can use either the derivation strategy or the transition system
when working on the specific application of operational semantics. This will simplify the work of the application ofoperational semantics.
In order to study this equivalence issue, we need to prove the following items for every process.
17β(1) If transition hP, αi −→ hP0 , α0 i exists in the transition system, then it also exists in the derivation strategy.
β(2) If transition hP, αi −→ hP0 , α0 i exists in the derivation strategy, then it also exists in the transition system.
Item (1) above is correct because our transition system is derived from the derivation strategy. Now we consider (2)as a theorem to be proved.
βTheorem 5.6 If transition hP, αi −→ hP0 , α0 i exists in the derivation strategy, then it also exists in the transition
system.
Proof We can proceed our proof by structural induction. Here we only give the proof for parallel composition. For
simplicity, we give the proof for the following example case where both of the head normal forms of P and Q can be
expressed as a guarded choice respectively.
Let HF (P) = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )}[][]k∈K {@b̂k Rk }HF (Q) = []l∈L {[ql ] choicem∈Ml (clm &(ylm := flm ) Qlm )}[][]n∈N {@ĉn T n }Then
HF (P kr Q) = []i∈I {[r × pi ] choice j∈Ji (bi j &(xi j := ei j ) par(Pi j , Q, r))}[][]l∈L {[(1 − r) × ql ] choicem∈Ml (clm &(ylm := flm )par(P, Qlm , r))}[][]k∈K {@(b̂k ∧ ¬ĉ) par(Rk , Q, r)}[][]n∈N {@(ĉn ∧ ¬b̂) par(P, T n , r)}[][]k∈K∧n∈N {@(b̂k ∧ ĉn ) par(Rk , Qn , r)}where, b̂ = ∨k∈K b̂k and ĉ = ∨n∈N ĉn
In this case, from the derivation strategy, P can perform the following transitions:v(p-1) hP, σi −→ hRk , σi, if b̂k (σ)c(p-2) hP, σi −→ pi hPi j , σ[ei j /xi j ]i, if ¬b̂(σ) ∧ bi j (σ)

On the other hand, from the derivation strategy, Q can also perform similar transitions, shown below:v(q-1) hQ, σi −→ hT n , σi, if ĉn (σ)c(q-2) hQ, σi −→ql hQlm , σ[ flm /ylm ]i, if ¬ĉ(σ) ∧ clm (σ)

By structural induction, the above transitions for P and Q also exist in our transition. From HF (P kr Q) and thederivation strategy, P k Q can perform and only perform the following transitions, which are derived from the derived
strategy.
v(l-1) hP kr Q, σi −→ hpar(Rk , Q, r), σi, if b̂k (σ) ∧ ¬ĉ(σ)v(l-2) hP kr Q, σi −→ hpar(P, T n , r), σi, if ĉn (σ) ∧ ¬b̂(σ)v(l-3) hP kr Q, σi −→ hpar(Rk , T n , r), σi, if b̂(σ) ∧ ĉn (σ)c(l-4) hP kr Q, σi −→r×pi hpar(Pi j , Q, r), σ[ei j /xi j ]i, if ¬b̂(σ) ∧ ¬ĉ(σ) ∧ bi j (σ)c(l-5) hP kr Q, σi −→(1−r)×ql hpar(P, Qlm , r), σ[ flm /ylm ]i, if ¬b̂(σ) ∧ ¬ĉ(σ) ∧ clm (σ)

Now we want to show that the above transitions for P kr Q also exist in the transition system. Here we give the prooffor (l-1). Others are similar.

18v

hP, σi −→ hRk , σi exists in the derivation strategy and⇒ {By Structural Induction and PL}¬ĉ(σ)vhP, σi −→ hRk , σi exists in the transition system andstable(hQ, σi) ∧ stableE(hQ, σi)⇒ {Transition System}v

hP kr Q, σi −→ hpar(Rk , Q, r), σi exists in the transition system¤

Now we can have the main result of this section.
Theorem 5.7 Regarding the derived operational semantics for our probabilistic language, the derivation strategy isequivalent to the transition system.
This result demonstrates that the transitions from the derivation strategy are the same as those in the transition
system. It also shows that our transition system (operational semantics) for our probabilistic language is completewith respect to the derivation strategy in section 5.2.
6. Animation Approaches to Operational Semantics
In section 5.3,we have derived an operational semantics for PTSC, which forms a transition system of our language(theorem 5.2 to theorem 5.5). Now in section 6.1, we explore the animation of operational semantics for PTSC, whichis the execution version of the operational semantics. The correctness of the operational semantics can be checked byusing various test results.
Meanwhile, in section 5.2, we provided the derivation strategy for deriving operational semantics from algebraic
semantics. Now in section 6.2 we explore the corresponding mechanical derivation, which can automatically derive
the transitions of a program, as well as animate the execution of a program based on the derivation strategy. Based on
the simulated execution of the two animation approaches in section 6.1 and 6.2, the fact of Theorem 5.7 can be shownvia various test examples.
6.1. Animation of Operational Semantics for PTSC
6.1.1. Animation Strategy and Transition TypeNow we start to explore the animation of operational semantics for PTSC. For this aim, the transitions are expressed in the form below:[P, S igma] −[β]→ [P0 , S igma0 ]where, configuration [P, S igma] can be expressed as a list in Prolog. Here, P stands for the program text that remains
to be executed. S igma is the current state of the program, which is represented in the form of list storing the values ofprogram variables. −[β]→ stands for the transition type.
As mentioned before (see page 13), the transitions for PTSC can be classified into four kinds. The first type canbe encoded in Prolog as:[P, S igma] −[0 c0 , R]→ [P0 , S igma0 ].
where, 0 c0 stands for the transition where the atomic action is caused by the program itself and R stands for the
probability for program P to perform the execution.
For other three transitions when encoded in Prolog, we use the notations −[1]→, −[0 tau0 ]→ and −[0 v0 ]→ to stand1τv

for transitions −→, −→ and −→ respectively.
For animation, the transition for assignment V := E can be expressed as below.
S igma = S igma ⊗ (V = E).
[V = E, S igma] −[0 c0 , 1]→ [epsilon, S igma ]Here, ⊗ stands for the overriding operator. S igma ⊗ (V = E) stands for the new state, where the new value of V
overrides the previous value of V by expression E.
19

Similarly, we can also provide the animation for the transitions of conditional, iteration, nondeterministic choice,nondeterministic choice and sequential composition. In the subsequent sections we mainly focus on the animation for
the rules of guarded choice and parallel composition.
6.1.2. Guarded Choice
Guarded choice can perform assignment with the associated probability provided that its corresponding Boolean
condition is satisfied. The corresponding transition −[0 c0 , P]→ may appear in two types of guarded choice constructs.
One is the guarded choice composed of a set of assignment guarded components. For P f or EB then (V = E) $ S ,the program can execute assignment V := E with probability P when the corresponding condition EB is evaluatedtrue in the current state. The first two rules below reveal this case recursively. The other one is the guarded choicecomposed of assignment guarded components and event guarded components. And in this case, the event guarded
component has a relatively high priority, which means when both the conditions of event guarded component andthat of assignment guarded component are true in the current state, we only allow the event to be fired and do not allow performing assignment. To handle this, we design the third rule and add the ”/−[0 v0 ]→ ” term in conditional clauses.
EB $ (S igma) ∧ S igma = S igma ⊗ (V = E) ∧ [S 0 , S igma] /−[0 v0 ]→ [ , S igma][[[P f or EB then (V = E) $ S ]|S 0 ], S igma] −[0 c0 , P]→ [S , S igma ].
EB $ (S igma) ∧ [S 0 , S igma] −[0 c0 , P0 ]→ [S 1 , S igma ] ∧ [S 0 , S igma] /−[0 v0 ]→ [ , S igma][[[ P f or EB then ( V = E) $ S ] | S 0 ], S igma] −[0 c0 , P0 ]→ [S 1 , S igma ].
[S 0 , S igma] −[0 v0 ]→ [S 1 , S igma][[[ P f or EB then ( V = E) $ S ]|S 0 ], S igma] −[0 v0 ]→ [S 1 , S igma].

Here, condition EB $ (S igma) stands for the Boolean value of expression EB at the state S igma and the notation“/−[β]→” indicates that this transition cannot be performed in the current state. For configuration [ , S igma], it indicatesthat the program part can be of any form.
Now we consider the event firing transition. The corresponding transition −[0 v0 ]→ may appear in three types ofguarded choice. The first type is the guarded choice composed of a set of event guarded components. The second
type is the guarded choice composed of assignment guarded components and event guarded components. The last
rule above reveals this. The last type is the guarded choice composed of event guarded components and time delay
component. For the first and third type, the transitions can be divided into the following several cases.
EB $ (S igma)[[[@EB $ S ]| S 0 ], S igma] −[0 v0 ]→ [S , S igma].
∼ EB $ (S igma) ∧ [S 0 , S igma] −[0 v0 ]→ [S 10 , S igma][[[@EB $ S ]|S 0 ], S igma] −[0 v0 ]→ [S 10 , S igma].

For time delay transition, as the execution of assignment is instantaneous, the second, third and fifth type of guarded
choice can perform time delay transition among the five types of guarded choice. The corresponding transition −[1]→may appear in three cases. The first two transitions below model the time delay transition for the second type ofguarded choice (i.e., containing a set of event guarded components). The fourth transition models the time delaytransition for the guarded choice containing only time-delay component. The third transition models the fifth type ofguarded choice, i.e., containing event guarded components and time-delay component. If no events can be enabled in
the event guarded choice, time will advance.
∼ EB $ (S igma)[[[@EB $ S ]], S igma] −[1]→ [[[@EB $ S ]], S igma].
∼ EB $ (S igma) ∧ [S 0 , S igma] −[1]→ [S 0 , S igma][[[@EB $ S ]|S 0 ], S igma] −[1]→ [[[@EB $ S ]|S 0 ], S igma].
∼ EB $ (S igma) ∧ [S 0 , S igma] −[1]→ [S 1 , S igma] ∧ S 1 ∼= S 0[[[@EB $ S ]|S 0 ], S igma] −[1]→ [S 1 , S igma].
true[[[#1 $ S ]], S igma] −[1]→ [S , S igma].

20

6.1.3. Parallel Composition
Next, we consider probabilistic parallel composition. Once a parallel component has executed to termination, theterminating component will be eliminated and the whole parallel program will perform as the non-terminating parallel
component.
Firstly we consider the [0 tau0 ] transition. If one parallel component can perform [0 tau0 ] transition and anotherparallel component cannot perform [0 tau0 ] transition, the whole program can also perform [0 tau0 ] transition.
[S 1 , S igma] −[0 tau0 ]→ [epsilon, S igma] ∧ [S 2 , S igma] /−[0 tau0 ]→ [ , S igma][S 1 k P S 2 , S igma] −[0 tau0 ]→ [S 2 , S igma].
[S 2 , S igma] −[0 tau0 ]→ [epsilon, S igma] ∧ [S 1 , S igma] /−[0 tau0 ]→ [ , S igma][S 1 k P S 2 , S igma] −[0 tau0 ]→ [S 1 , S igma].
[S 1 , S igma] −[0 tau0 ]→ [S 10 , S igma] ∧ [S 2 , S igma] /−[0 tau0 ]→ [ , S igma] ∧ S 10 ∼= epsilon[S 1 kP S 2 , S igma] −[0 tau0 ]→ [S 10 kP S 2 , S igma].
[S 2 , S igma] −[0 tau0 ]→ [S 20 , S igma] ∧ [S 1 , S igma] /−[0 tau0 ]→ [ , S igma] ∧ S 20 ∼= epsilon[S 1 kP S 2 , S igma] −[0 tau0 ]→ [S 1 kP S 20 , S igma].

If both components make [0 tau0 ] transition, the whole process can make [0 tau0 ] transition and the subsequent behaviour is the parallel composition of the remaining components.
[S 1 , S igma] −[0 tau0 ]→ [S 10 , S igma] ∧ [S 2 , S igma] −[0 tau0 ]→ [S 20 , S igma] ∧ S 10 ∼= epsilon ∧ S 20 ∼= epsilon[S 1 kP S 2 , S igma] −[0 tau0 ]→ [S 10 kP S 20 , S igma].

If S 1 (or S 2 , or both of them) reaches to the terminating state after performing [0 tau0 ] transitions, the transition rulefor S 1 kP S 2 is similar.
The following rules cover the case of performing an atomic action with certain probability in parallel composition.
If process S 1 can perform an atomic action with probability X, parallel process S 1 kP S 2 and S 2 kP S 1 can also performthe same atomic action with probability X × P and (1−P) × X respectively. In parallel composition, we assume [0 tau0 ]transition and [0 v0 ] transition have high priority. This is reflected in the transitions below.
[S 1 , S igma] −[0 c0 , X]→ [S 10 , S igma ] ∧ S 10 ∼= epsilon ∧ [S 2 , S igma] /−[0 tau0 ]→ [ , S igma] ∧ [S 1 , S igma] /−[0 v0 ]→ [ , S igma][S 1 kP S 2 , S igma] −[0 c0 , X ∗ P]→ [S 10 kP S 2 , S igma ].
[S 2 , S igma] −[0 c0 , X]→ [S 20 , S igma ] ∧ S 20 ∼= epsilon ∧ [S 1 , S igma] /−[0 tau0 ]→ [ , S igma] ∧ [S 1 , S igma] /−[0 v0 ]→ [ , S igma][S 1 kP S 2 , S igma] −[0 c0 , (1−P) ∗ X]→ [S 1 kP S 20 , S igma ].

Here we only list the case that S 1 (or S 2 ) reaches to the non-terminating state after performing the atomic action
transition.
For [0 v0 ] and [1] transitions, the analysis for animation is similar.
Example 6.1
Let P be the process described in Example 4.1 (page 13). Now we consider the execution sequence using the operational semantics provided above. The query is posed in the form “trackOP[P, S igma].”. The animation result is displayed as below. The process at step 0 is still process P itself. In each execution step, for example [ P, [b = 4, a = 2] ],the second element stands for the current state for program variables, which is represented as a list. Here the notation[b = 4, a = 2] stands for the state, where the value of variable b is 4 and the value of a is 2.
? − trackOP[ P, [b = 4, a = 2] ].
0 − −− > [ P, [b = 4, a = 2]]
1 −[v ]→ [[[1 f or true then a = 10 $ a = 11]] k0.2 b = 6, [b = 4, a = 2]]
2 −[c, 0.8]→[[[1 f or true then a = 10 $ a = 11]], [b = 6, a = 2]]
3 −[c, 1]→[a = 11, [b = 6, a = 10]]
4 −[c, 1 ]→ [epsilon, [b = 6, a = 11]]2 −[c, 0.2]→[a = 11 k0.2 b = 6, [b = 4, a = 10]]3 −[c, 0.2]→ [b = 6, [b = 4, a = 11]]21

4 −[c, 1 ]→ [epsilon, [b = 6, a = 11]]3 −[c, 0.8]→ [a = 11, [b = 6, a = 10]]
4 −[c, 1 ]→ [epsilon, [b = 6, a = 11]]

From the displayed result, we know that there are three execution sequences leading to the terminating state.
6.2. Animation of Generating Operational Semantics from Algebraic Semantics
Section 5 considered the derivation of operational semantics from algebraic semantics for PTSC. A derivation
strategy has been provided based on the head normal form. Now we consider the animation of the derivation strategy
for deriving operational semantics from algebraic semantics.
Definition 6.2(1) If the head normal form of process P can be expressed as a guarded choice; i.e., it can be of form assignGuardChoice,eventGuardChoice, timeDelay, assign event and event time, then the transition rules for process P are the sameas the transition rules of its corresponding guarded choice.
(2) On the other hand, if the head normal form of process P cannot be described as one of the five types of guarded
choice (in other words, the head normal form is with a structure of summation), then process P can first do[0 tau0 ] transitions and reach to all the processes which are initially deterministic, and these processes can be
expressed as one of the five type guarded choices.
∼ pgc([X | L])[[X | L], S igma] −[0 tau0 ]→ [X, S igma].
L ∼= [ ] ∧ [L, S igma] −[0 tau0 ]→ [Y, S igma][[ | L], S igma] −[0 tau0 ]→ [Y, S igma].

Here, ∼ pgc([X | L]) indicates that the head normal form of [X | L] is not in the form of the five types of guarded
choice, which means it is a summation.
¤
For the transition rules of guarded choice (see page 14), they have already been formalized in section 5.2. The second
rule above stands for the τ transitions for a process if its head normal form is not of the form in the five types ofguarded choice.
Now we have two ways to achieve operational semantics for PTSC. The first approach is the transition systemitself (see section 6.1), which directly provides the transition rules for each statement. The second approach describedin this section is to derive the transition rules for each statement. The derivation strategy is based the head normal
form of a process and those parallel expansion laws. This section applies the animation approach in showing that theabove two approaches can achieve the same transitions for each statement. We use the example below to illustrate theanimation of operational semantics by the above two approaches.
Example 6.3
Let P be the program described in Example 4.1 (page 13) and Example 6.1 (page 21). In Example 6.1, we havealready considered the execution sequence of program P using the operational semantics. The animation results havealready been provided.
Now we consider the derivation of the operational semantics via algebraic semantics. The query is posted in theform “trackHFOP[P, S igma].”. The process at step 0 is the head normal form of P, i.e., NF is the head normal
form which has been explored in Example 5.1. For the derivation approach, there are also three execution sequencesleading to the terminating state.
? − trackHFOP[P, [b = 4, a = 2]].
0 − −− > [NF, [b = 4, a = 2]]
1 −[v ]→ [[[1 f or true then a = 10 $ a = 11]] k0.2 b = 6, [b = 4, a = 2]]
2 −[c, 0.8]→[[[1 f or true then a = 10 $ a = 11]], [b = 6, a = 2]]
3 −[c, 1]→[a = 11, [b = 6, a = 10]]
4 −[c, 1 ]→ [epsilon, [b = 6, a = 11]]2 −[c, 0.2]→[a = 11 k0.2 b = 6, [b = 4, a = 10]]22

3 −[c, 0.2]→ [b = 6, [b = 4, a = 11]]4 −[c, 1 ]→ [epsilon, [b = 6, a = 11]]3 −[c, 0.8]→ [a = 11, [b = 6, a = 10]]
4 −[c, 1 ]→ [epsilon, [b = 6, a = 11]]

The execution step for NF is based on the derivation strategy. Based on the above execution result, we know that thederived operational semantics for program P is the same as the original operational semantics (section 6.1).
7. Related Work
Shared-variable concurrency (SVC) is used to model concurrency via multi-threaded programs. de Rover et al.
have explored concurrency verification methods, including both compositional and noncompositional methods [48]. A
shared-variable concurrency language is introduced, where the concurrent execution is charactered by the interleaving
model. Verification methods have been studied, including assertion method, compositional proof methods and Hoare
logic method. However, their shared-variable language has not covered the reasoning about priority for scheduling
one thread over another, or more general probabilistic choice.
Probability in sequential programming has been studied by Morgan and his colleagues [35, 36, 37]. They explored
the abstraction and refinement for probabilistic processes using the weakest precondition (wp) approach. Hehnerstudied how probabilistic programming can be applied to the predicative style of programming [24, 22, 23]. Anotherstudy for probability approach is that probabilistic method has been explored for process algebra. Núñez extended
Henessey’s “testing semantics” for a variety of probabilistic processes [42, 43, 44]. Seidel studied probabilistic
communicating processes [49] by adding probability in Communicating Sequential Processes (CSP) [25]. In [56], we
proposed the model of PTSC, which integrates probability with time and shared-variable concurrency.
PTSC is designed for discrete event simulation with probability. Previously, we have studied various semantics[51, 58] for Hardware Description Language Verilog [29, 30]. It is a multithreaded discrete event simulation language
containing interesting features such as event-driven computation and shared-variable concurrency. We also exploredthe linking theories between various semantics for Verilog [51, 58]. However, this language does not have probability
feature.
The contribution of this paper is the linking of algebraic semantics and operational semantics for PTSC. Our approach is to derive the operational semantics from algebraic semantics, where mechanical methods have been applied.
For the linking of various semantics for Verilog [18, 53, 54, 58, 51], the derivation of one semantic representationfrom another has been explored. However, the mechanical approach for semantic linking has not been adopted.
Regarding the work of relating operational and algebraic semantics, Hoare and He have studied the derivationof operational semantics from the algebraic semantics [26, 27]. An operational semantics of CSP [25] was derived,
based on CSP’s algebraic laws according to a derivation strategy (called the action transition relation). An operationalsemantics of Dijkstra’s Guarded Command Language (abbreviated as GCL) was also derived based on GCL’s algebra
according to the derivation strategy (called the step relation). However, the languages does not contain probabilistic
and event features, and the mechanical approach has not been studied.
Our work for linking the semantics for PTSC can be regarded as the further exploration of Unifying Theories ofProgramming (UTP) [27]. UTP covers wide areas of fundamental theories of programming in a formalized style andacts as a consistent basis for principles of programming language. The UTP approach has been successfully appliedin studying the semantics and algebraic laws of programming languages. Probabilistic guarded command language isan extension of guarded command language with probabilistic choice. Its denotational semantics was formalized by
He, Seidel and McIver [21] under the UTP framework. A set of algebraic laws was achieved based on denotationalsemantics. New unification of probablity with standard computation has been studied in which a nonzero chance ofdisaster is treated as disasters [19].
The mechanical approach for the semantic linking in this paper is done using Prolog via animation. Bowen etal. encoded the operational semantics for Verilog using Prolog in a literate programming style [3, 4]. It enables thesemantics to be directly animated using a Prolog interpreter. In addition, it provides an extra check on the validity ofthe operational semantics.
For the semantic linking, several approaches have been investigated for the consistency between operational semantics and denotational semantics. Brookes has given a new denotational semantics for a shared-variable parallel
23

programming language [6]. The denotational semantics is proved to be fully abstract with respect to the operationalbased partial correctness behaviour. The consistency has also been investigated in the book Control Flow Semantics(abbreviated as CFS) [9]. CFS is devoted to studying the equivalence of operational semantics and denotationalsemantics for 27 languages using the theory of Metric Space. Hartog and his colleagues have studied the equivalence between operational and denotational semantics for a variety of probabilistic processes [11, 12, 13, 14] using
CFS approach. Although the equivalence can be solved, it is difficult to prove algebraic laws from the denotationalsemantics.
8. Conclusions
This paper has presented how an algebraic semantics links with an operational semantics for our proposed probabilistic language with time and shared-variable concurrency. The work is based on the unifying theories of programming, pioneered by Hoare and He [27]. This exploration includes both the theoretical and practical approaches.
• We have given the algebraic laws. Our approach is new, where a process can be expressed as either a guarded
choice, or the summation of a set of processes which are initially deterministic. Every guarded choice iscomposed of a set of guarded components. This approach with guarded choice gives us a way to sequentialize aprocess that also reflects the scheduling policy. This summation representation with guarded choice also gives
meaning for the program.
• We have studied the derivation of the operational semantics for our language from its algebraic semantics. We
have given the definition of the derivation strategy. Then a transition system (i.e., operational semantics) for our
language can be derived via the derivation strategy. This gives us confidence for the soundness and consistencyof the operational semantics with the algebraic semantics.
• We have investigated the relationship between the derivation strategy and the derived operational semantics.
We have proved that the derived operational semantics is equivalent to the derivation strategy. This tells us that
we can use either the derivation strategy or the derived operational semantics for the application of operationalsemantics. The result achieved here shows that our transition system (operational semantics) is complete withhead normal form.
Besides the above theoretical approach to the link between the operational semantics and algebraic semantics for
PTSC, we also considered the practical approach for the link. We have explored the animation of the link between
the two semantics for PTSC. The animated result supports to claim of the soundness and completeness of operationalsemantics with respect to the algebraic laws from various test results. Our animation approach is based on the Logic
Programming Language Prolog.
• We explored the algebraic laws for PTSC via mechanical approach. We mainly focused on the mechanicalgenerating of the parallel expansion laws. Our approach is based on the five types of guarded choice.
• We studied the mechanical generation of the head normal form for a program. The concept of head normal
form has been used to do the link between algebraic semantics and operational semantics for our consideredlanguage.
• We considered how to build the link between the operational semantics and algebraic semantics mechanically.
Our approach is to implement the theoretical derivation strategy for deriving operational semantics from algebraic semantics. For the derived operational semantics as a whole system, we also investigated its animation.
For the future, we are continuing to work on the linking theories for various semantics of programming languages[27, 51]. The denotational model for PTSC is much more challenging because of the three features. Similar theoreticaland practical approaches would also be interesting for other computation models, for example, probabilistic web
services [7, 31, 57]. Further, we are also interested in how our animation approach can be applied to system verification[1, 2, 32, 33].
Acknowledgement

This work is supported in part by National Basic Research Program of China (No. 2011CB302904), National

24

High Technology Research and Development Program of China (No. 2007AA010302), National Natural Science Foundation ofChina (No. 90718004 and No. 61061130541), Macau Science and Technology Development PEARL and EAE projects (No.
041/2007/A3 and No. 072/2009/A3) and UK EPSRC Project EP/G042322.

References[1] Apt KR (1981) Ten years of Hoare’s logic: A survey - part 1. ACM Transactions on Programming Languages and Systems 3(4):431–483[2] Apt KR (1984) Ten years of Hoare’s logic: A survey part II: Nondeterminism. Theoretical Computer Science 28[3] Bowen JP (2000) Combining operational semantics, logic programming and literate programming in the specification and animation of the
Verilog Hardware Description Language. In: Proc. IFM 2000: 2nd International Conference on Integrated Formal Methods, Springer-Verlag,
Lecture Notes in Computer Science, vol 1945, pp 277–296[4] Bowen JP, He J, Xu Q (2000) An animatable operational semantics of the Verilog Hardware Description Language. In: Proc. ICFEM 2000:
3rd IEEE International Conference on Formal Engineering Methods, IEEE Computer Society Press, pp 199–207[5] Brookes S (2006) A grainless semantics for parallel programs with shared mutable data. Electron Notes Theor Comput Sci 155:277–307[6] Brookes SD (1996) Full abstraction for a shared-variable parallel language. Information and Computation 127(2):145–163[7] Butler M, Ripon S (2005) Executable semantics for compensating CSP. In: Proc. EPEW 2005: International Workshop on Web Services andFormal Methods, Versailles, France, September 1–3, 2005, Springer-Verlag, Lecture Notes in Computer Science, vol 3670, pp 243–256[8] Clocksin WF, Mellish CS (2003) Programming in Prolog, 5th edn. Springer-Verlag[9] de Bakker J, de Vink E (1996) Control Flow Semantics. The MIT Press[10] De Boer FS (2007) A sound and complete shared-variable concurrency model for multi-threaded java programs. In: Proceedings of the
9th IFIP WG 6.1 international conference on Formal methods for open object-based distributed systems, Springer-Verlag, FMOODS’07, pp
252–268[11] den Hartog J (2002) Probabilistic extensions of semantic models. PhD thesis, Vrije University, The Netherlands[12] den Hartog J, de Vink E (1999) Mixing up nondeteminism and probability: A premliminary report. Electronic Notes in Theoretical Computer
Science 22[13] den Hartog J, de Vink E (2002) Verifying probabilistic programs using a Hoare like logic. International Journal of Foundations of Computer
Science 40(3):315–340[14] den Hartog J, de Vink E, de Bakker J (2001) Metric semantics and full abstractness for action refinement and probabilistic choice. Electronic
Notes in Theoretical Computer Science 40[15] Dijkstra EW (1968) The structure of the the-multiprogramming system. Commun ACM 11:341–346[16] Hansen PB (1972) Structured multiprogramming. Commun ACM 15:574–578[17] He J (1994) Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. The McGraw-Hill
International Series in Software Engineering[18] He J (2003) An algebraic approach to the Verilog programming. In: Proc. 10th Anniversary Colloquium of UNU/IIST, Lisbon, Portugal,
March 18-20, 2002, Springer, Lecture Notes in Computer Science, vol 2757, pp 65–80[19] He J, Sanders JW (2006) Unifying probability. In: Proc. UTP 2006: Unifying Theories of Programming, First International Symposium, UTP
2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Springer, Lecture Notes in Computer Science, vol 4010, pp 173–199[20] He J, Zhu H (2000) Formalising Verilog. In: Proc. ICECS 2000: IEEE International Conference on Electronics, Circuits and Systems, IEEE
Computer Society Press, pp 412–415[21] He J, Seidel K, McIver A (1997) Probabilistic models for the guarded command language. Science of Computer Programming 28(2-3):171–
192[22] Hehner ECR (1984) Predicative programming, part I. Communications of the ACM 27(2):134–143[23] Hehner ECR (1984) Predicative programming, part II. Communications of the ACM 27(2):144–151[24] Hehner ECR (2004) Probabilistic predicative programming. In: Proc. MPC 2004: 7th International Conference on Mathematics of Program
Construction, Stirling, Scotland, UK, July 12-14, 2004, Springer, Lecture Notes in Computer Science, vol 3125, pp 169–185[25] Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall International Series in Computer Science[26] Hoare CAR, He J (1993) From algebra to operational semantics. Information Processing Letters 45:75–80[27] Hoare CAR, He J (1998) Unifying Theories of Programming. Prentice Hall International Series in Computer Science[28] Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, Sørensen IH, Spivey JM, Sufrin B (1987) Laws of programming. Communications of the ACM 38(8):672–686[29] IEEE (1995) IEEE Standard Hardware Description Language based on the Verilog Hardware Description Language, vol IEEE Standard
1364-1995. IEEE
[30] IEEE (2001) IEEE Standard Hardware Description Language based on the Verilog Hardware Description Language, vol IEEE Standard
1364-2001. IEEE
[31] Leymann F (2001) Web Services Flow Language (WSFL 1.0). IBM, http://www-3.ibm.com/software/solutions/webservices/pdf/WSDL.pdf[32] Manna Z, Pnueli A (1992) The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag[33] Manna Z, Pnueli A (1995) Temporal Verification of Reactive Systems: Safety. Springer-Verlag[34] Manson J, Pugh W, Adve SV (2005) The java memory model. Principles of Programming Languages (POPL) pp 378–391[35] McIver A, Morgan C (2001) Partial correctness for probabilistic demonic programs. Theoretical Computer Science 266(1-2):513–541[36] McIver A, Morgan C (2004) Abstraction, Refinement and Proof of Probability Systems. Monographs in Computer Science, Springer[37] McIver A, Morgan C, Seidel K (1996) Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems
18(3):325–353[38] Motwani R, Raghavan P (1995) Randomized algorithms. Cambridge University Press25

[39] Ndukwu U, Sanders JW (2008) Reason about a distributed probabilistic system. Tech. Rep. 401, UNU/IIST, P.O. Box 3058, Macau SAR,
China[40] Ndukwu U, Sanders JW (2009) Reasoning about a distributed probabilistic system. In: Proc. CATS 2009: Fifteenth Australasian Symposiumon Computing: The Australasian Theory, Volume 94, Australian Computer Society, Wellington, New Zealand, pp 35–42[41] Nissanke N (1997) Realtime Systems. Prentice Hall International Series in Computer Science[42] Núñez M (2003) Algebraic theory of probabilistic processes. The Journal of Logic and Algebraic Programming 56:117–177[43] Núñez M, de Frutos-Escrig D (1996) Testing semantics for probabilistic LOTOS. In: Proc FORTE’95: IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995, Chapman & Hall, IFIP Conference Proceedings, vol 43, pp
367–382[44] Núñez M, de Frutos-Escrig D, Dı́az LFL (1995) Acceptance trees for probabilistic processes. In: Proc CONCUR’95: 6th International
Conference on Concurrency, Philadelphia, PA, USA, August, 1995, Springer, Lecture Notes in Computer Science, vol 962[45] Park S, Pfenning F, Thrun S (2005) A probabilistic language based upon sampling functions. In: Proc POPL 2005: 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, ACM, pp 171–182[46] Plotkin G (1981) A structural approach to operational semantics. Tech. Rep. 19, University of Aahus, also published in The Journal of Logic
and Algebraic Programming, volumes 60-61:17–139, 2004[47] Reynolds JC (2004) Toward a grainless semantics for shared-variable concurrency. In: In Proc. FSTTCS 2004, volume 3328 of LNCS,
Springer-Verlag, pp 35–48[48] de Roever WP, de Boer F, Hanneman U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press[49] Seidel K (1995) Probabilistic communicating processes. Theoretical Computer Science 152(2):219–249[50] Stoy J (1977) Denotational Semantics: The Scott-Strachey Approach to Programming Language. MIT Press[51] Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis, London South Bank University[52] Zhu H, He J (2000) A semantics of Verilog using Duration Calculus. In: Proc. International Conference on Software: Theory and Practice,
pp 421–432[53] Zhu H, Bowen JP, He J (2001) Deriving operational semantics from denotational semantics for Verilog. In: Proc. APSEC 2001: 8th AsiaPacific Software Engineering Conference, IEEE Computer Society Press, pp 177–184[54] Zhu H, Bowen JP, He J (2001) From operational semantics to denotational semantics for Verilog. In: Proc. CHARME 2001: 11th Advanced
Research Working Conference on Correct Hardware Design and Verification Methods, Springer-Verlag, Lecture Notes in Computer Science,
vol 2144, pp 449–464[55] Zhu H, He J, Bowen JP (2006) From operational semantics to denotational semantics for Verilog. In: Proc. ICECCS 2006: 11th IEEE
International Conference on Engineering of Complex Computer Systems, IEEE Computer Society Press, pp 139–151[56] Zhu H, Qin S, He J, Bowen JP (2006) Integrating probability with time and shared-variable concurrency. In: Proc SEW-30: 30th NASA/IEEE
Software Engineering Workshop, IEEE Computer Society, pp 179–189[57] Zhu H, He J, Pu G, Li J (2007) An operational approach to BPEL-like programming. In: Proc. SEW-31: 31st IEEE Software Engineering
Workshop, Baltimore, USA, IEEE Computer Society Press, pp 236–245[58] Zhu H, He J, Bowen JP (2008) From algebraic semantics to denotational semantics for verilog. Innovations in Systems and Software Engineering: A NASA Journal 4(4):341–360[59] Zhu H, Qin S, He J, Bowen JP (2009) PTSC: probability, time and shared-variable concurrency. Innovations in Systems and Software
Engineering: A NASA Journal 5(4):271–284

Appendix
As mentioned in section 3.3, there are fifteen parallel expansion laws. Five of them have already been presented
in the main text (section 3.3 and section 4.1). The rest are listed below.
(par-3-3) Let P = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )} and Q = []{#1 R}
Then P kr Q = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) par(Pi j , Q, r))}(par-3-4) Let P = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )} andQ = []k∈K {[qk ] choicel∈Lk (bkl &(xkl := ekl ) Qkl )}[][]m∈M {@cm Rm }Then P kr Q = []i∈I {[r × pi ] choice j∈Ji (bi j &(xi j := ei j ) par(Pi j , Q, r))}[][]k∈K {[(1 − r) × qk ] choicel∈Lk (bkl &(xkl := ekl ) par(P, Qkl , r)}[][]m∈M {@ck par(P, Rm , r)}(par-3-5) Let P = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )} and Q = []l∈L {@cl Ql }[]{#1 R}
Then P kr Q = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) par(Pi j , Q, r))}[][]l∈L {@cl par(P, Ql , r)}(par-3-7) Let P = []i∈I {@bi Pi } and Q = []{#1 R}
Then P kr Q = []i∈I {@bi par(Pi , Q, r)}[]{#1 par(P, R, r)}26

(par-3-8) Let P = []i∈I {@bi Pi } and Q = [] j∈J {[q j ] choicek∈K j (b jk &(x jk := e jk ) Q jk )}[][]l∈L {@cl Rl }Then P kr Q = [] j∈J {[q j ] choicek∈K j (bi j &(x jk := e jk ) par(P jk , Q, r))}[][]i∈I {@(bi ∧¬c) par(Pi , Q, r)}[][]l∈L {@(cl ∧¬b) par(P, Rl , r)}[][]i∈I∧l∈L {@(bi ∧cl ) par(Pi , Ql , r)}where, b = ∨i∈I bi and c = ∨l∈L cl(par-3-9) Let P = []i∈I {@bi Pi } and Q = [] j∈J {@c j Q j }[]{#1 R}
Then P kr Q = []i∈I {@(bi ∧ ¬c) par(Pi , Q, r)}[][] j∈J {@(c j ∧ ¬b) par(P, Q j , r)}[][]i∈I∧ j∈J {@(bi ∧ c j ) par(Pi , Q j , r)}[][]{#1 par(P, R, r)}where, b = ∨i∈I bi and c = ∨ j∈J c j(par-3-11) Let P = []{#1 T } and Q = []i∈I {[qi ] choice j∈Ji (b jk &(xi j := ei j ) Qi j )}[][]k∈K {@ck Rk }Then P kr Q = []i∈I {[qi ] choice j∈Ji (bi j &(xi j := ei j ) par(P, Qi j , r))}[][]k∈K {@ck par(P, Rk , r)}(par-3-12) Let P = []{#1 T } and Q = []i∈I {@bi Qi }[]{#1 R}
Then P kr Q = []i∈I {@bi par(P, Qi , r)}[]{#1 par(T, R, r)}(par-3-13) Let P = []i∈I {[pi ] choice j∈Ji (bi j &(xi j := ei j ) Pi j )}[][]k∈K {@bk Rk } andQ = []l∈L {[ql ] choicem∈Ml (clm &(xlm := elm ) Plm )}[][]n∈N {@cn T n }Then P kr Q = []i∈I {[r × pi ] choice j∈Ji (bi j &(xi j := ei j ) par(Pi j , Q, r))}[][]l∈L {[(1 − r) × ql ] choicem∈Ml (clm &(xlm := elm ) par(P, Qlm , r))}[][]k∈K {@(bk ∧ ¬c) par(Rk , Q, r)}[][]n∈N {@(cn ∧ ¬b) par(Rk , Q, r)}[][]k∈K∧n∈N {@(bk ∧ cn ) par(Rk , Qn , r)}where, b = ∨k∈K bk and c = ∨n∈N cn(par-3-15) Let P = []i∈I {@bi Pi }[]{#1 R} and Q = [] j∈J {@c j Q j }[]{#1 T }Then P kr Q = []k∈K {@(bi ∧ ¬c) par(Pi , Q, r)}[][] j∈J {@(c j ∧ ¬b) par(P, Q j , r)}[][]i∈I∧ j∈J {@(bi ∧ c j ) par(Pi , Q j , r)}[][]{#1 par(R, T, r)}where, b = ∨i∈I bi and c = ∨ j∈J c j

27