TY - GEN
T1 - Process algebra with probabilistic choice
AU - Andova, S.
PY - 1999
Y1 - 1999
N2 - Published results show that various models may be obtained by combining parallel composition with probability and with or without non-determinism. In this paper we treat this problem in the setting of process algebra in the form of ACP. First, probabilities are introduced by an operator for the internal probabilistic choice. In this way we obtain the Basic Process Algebra with probabilistic choice prBPA. After-wards, prBPA is extended with parallel composition to ACP p + . We give the axiom system for ACP p + and a complete operational semantics that preserves the interleaving model for the dynamic concurrent processes. Considering the PAR protocol, a communication protocol that can be used in the case of unreliable channels, we investigate the applicability of ACP p + . Using in addition only the priority operator and the preabstraction operator we obtain a recursive specification of the behaviour of the protocol that can be viewed as a Markov chain.
AB - Published results show that various models may be obtained by combining parallel composition with probability and with or without non-determinism. In this paper we treat this problem in the setting of process algebra in the form of ACP. First, probabilities are introduced by an operator for the internal probabilistic choice. In this way we obtain the Basic Process Algebra with probabilistic choice prBPA. After-wards, prBPA is extended with parallel composition to ACP p + . We give the axiom system for ACP p + and a complete operational semantics that preserves the interleaving model for the dynamic concurrent processes. Considering the PAR protocol, a communication protocol that can be used in the case of unreliable channels, we investigate the applicability of ACP p + . Using in addition only the priority operator and the preabstraction operator we obtain a recursive specification of the behaviour of the protocol that can be viewed as a Markov chain.
U2 - 10.1007/3-540-48778-6_7
DO - 10.1007/3-540-48778-6_7
M3 - Conference contribution
SN - 3-540-66010-0
T3 - Lecture Notes in Computer Science
SP - 111
EP - 129
BT - Formal Methods for Real-Time and Probabilistic Systems (Proceedings ARTS'99, Bamberg, Germany, May 26-28, 1999)
A2 - Katoen, J.P.
PB - Springer
CY - Berlin
ER -