Axiomatizing probabilistic processes: ACP with generative probabilities

This paper is concerned with finding complete axiomatizations of probabilistic processes. We examine this problem within the context of the process algebra ACP_I^- and obtain as our end-result the axiom system prACP_I^-, a probabilistic version of ACP which can be used to reason algebraically about the reliability and performance of concurrent systems. Our goal was to introduce probability into ACP in as simple a fashion as possible. Optimally, ACP should be the homomorphic image of the probabilistic version in which the probabilities are forgotten. We begin by weakening slightly ACP to obtain the axiom system ACP_I^-. The main difference between ACP and ACP_I^- is that the axiom x + δ = x, which does not yield a plausible interpretation in the generative model of probabilistic computation, is rejected in ACP_I^-. We argue that this does not aflect the usefulness of ACP_I^- in practice, and show how ACP can be reconstructed from ACP_I^- with a minimal amount of technical machinery. prACP_I^- is obtained from ACP_I^- through the introduction of probabilistic alternative and parallel composition operators, and a process graph model for prACP_I^-" based on probabilistic bisimulation is developed. We show that prACP_I^- is a sound and complete axiomatization of probabilistic bisimulation for finite processes, and that prACP_I^- can be homomorphically embedded in ACP_I^- as desired. Our results for ACP_I^- and prACP_I^- are presented in a modular fashion by first considering several subsets of the signatures. We concludc with a discussion about the suitability of an internal probabilistic choice operator in the context of prACP_I^-.