Computer Science – Logic in Computer Science
Scientific paper
2012-01-11
Computer Science
Logic in Computer Science
Scientific paper
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 the 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.
Deng Yuxing
Tiu Alwen
No associations
LandOfFree
Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-603693