AXIOMATIZING PROBABILISTIC PROCESSES - ACP WITH GENERATIVE PROBABILITIES

This paper is concerned with finding complete axiomatizations of proba bilistic processes. We examine this problem within the context of the process algebra ACP and obtain as our endresult the axiom system prACP (-), a version of ACP whose main innovation is a probabilistic asynchr onous interleaving operator. Our goal was to introduce probability int o ACP in as simple a fashion as possible, Optimally, ACP should be the homomorphic image of the probabilistic version in which the probabili ties are forgotten, We begin by weakening slightly ACP to obtain the a xiom system ACP(-),. The main difference between ACP and ACP(-), is th at the axiom x + delta = x, which does not yield a plausible interpret ation in the generative model of probabilistic computation, is rejecte d in ACP(-),. We argue that this does not affect the usefulness of ACP , in practice, and show how ACP can be reconstructed from ACP, with a minimal amount of technical machinery, prACP, is obtained from ACP, th rough the introduction of probabilistic alternative and parallel compo sition operators, and a process graph model for pr ACP, based on proba bilistic bisimulation is developed. We show that pr ACP, is a sound an d complete axiomatization of probabilistic bisimulation for finite pro cesses, and that prACP, can be homomorphically embedded in ACP, as des ired. Our results for ACP, and prACP, are presented in a modular fashi on by first considering several subsets of the signatures, We conclude with a discussion about adding an iteration operator to pr ACP(-),. ( C) 1995 Academic Press, Inc.