Process algebra with interleaving probabilistic parallel composition
Suzana Andova · TU/e Research Portal · 1999
In this paper we present a probabilistic version of the axiom system A CP appropriate for the (algebraic) formal description of pIobabilisti.cprocesses.The proposed formalism is built in a modular way, first Basic Process Algebra (prBPA) is constructed which afterwards is extended by parallel composition (prACP).Probabilities are introduced by an operator for internal probabilistic choice.In this way prACP contains both non-deterministic and probabilistic choice operators.Combining these two operators leads to the situation where the idem potency law with respect to the alternative composition does not hold anymore, so the axiom x + x = x is weakened to hold only for atomic actions.In defining the operational semantics for prBPA and prACP, we use the alternating approach, where two types of transitions are allowed, probabilistic and action transitions.In order to construct a complete term model for our process algebras we use a term deduction system over a larger signature than the signature of prBPA and p1A CP, respectively.We show that probabilistic (strong) bisimulation as proposed by Larsen and Skou is a congruence and prove the soundness and completeness of the presented term model.As an example of the application of prA CP we consider the Alternating Bit Protocol with unreliable communication channels. Basic Process Algebra(let ITk = l."~" for 2::; k ::; n -1) = Xl tI-" (X2t1-a, ... Xj tl-aiXj+l ... tlon _, xn) (by IH)(where Pk = l~~' for 3::; k::; n-l,k ij) , == (Xl tt-" j Xj) U7J"I+O"j-1flOj (Xatlp3 ... tlpj_1X2tt-p2Xj+l ... ttpn _ 1 X n ) 11"1 +.,.J ""I u"j