Under consideration for publication in Formal Aspects of Computing Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus

Abstract. We consider two characterisations of the may and must testing preorders for a probabilistic extension of the finite pi-calculus: one based on notions of probabilistic weak simulations, and the other on a probabilistic extension of a fragment of Milner-Parrow-Walker modal logic for the pi-calculus. We base our notions of simulations on similar concepts used in previous work for probabilistic CSP. However, unlike the case with CSP (or other non-value-passing calculi), there are several possible definitions of simulation for the probabilistic pi-calculus, which arise from different ways of scoping the name quantification. We show that in order to capture the testing preorders, one needs to use the “earliest ” simulation relation (in analogy to the notion of early (bi)simulation in the non-probabilistic case). The key ideas in both characterisations are the notion of a “characteristic formula ” of a probabilistic process, and the notion of a “characteristic test ” for a formula. As in an earlier work on testing equivalence for the pi-calculus by Boreale and De Nicola, we extend the language of the pi-calculus with a mismatch operator, without which the formulation of a characteristic test will not be possible