Characterisations of testing preorders for a finite probabilistic -calculus

DOI10.1007/S00165-012-0238-3MaRDI QIDQ1941882zbMATH OpenOpenAlexFDO

Authors Alwen Tiu, Yuxin Deng

Publication date 22 March 2013

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1201.2258, http://hdl.handle.net/1885/65851

zbMATH Keywords

modal logicbisimulationtesting semanticsprobabilistic {\(\pi\)}-calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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 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.

Recommendations

• Characterising Testing Preorders for Finite Probabilistic Processes
• Testing Finitary Probabilistic Processes
• Testing preorders for probabilistic processes.
• Testing preorders for probabilistic processes can be characterized by simulations
• Characterising probabilistic processes logically (extended abstract)

Cites work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3765109 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 1512615 (Why is no real title available?)
• A calculus of mobile processes. II
• A framework for analyzing probabilistic protocols and its application to the partial secrets exchange
• A testing scenario for probabilistic processes
• Bisimulation for higher-order process calculi
• Branching time and abstraction in bisimulation semantics
• Characterising Testing Preorders for Finite Probabilistic Processes
• Late and early semantics coincide for testing
• Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
• Modal logics for mobile processes
• On the bisimulation proof method
• Reactive, generative, and stratified models of probabilistic processes
• Remarks on testing probabilistic processes
• Scalar Outcomes Suffice for Finitary Probabilistic Testing
• Testing Finitary Probabilistic Processes
• Testing equivalence for mobile processes
• Testing equivalences for processes
• The \(\pi\)-calculus: A theory of mobile processes

Cited in

(4)

• Testing preorders for probabilistic processes can be characterized by simulations
• Testing Finitary Probabilistic Processes
• Characterising Testing Preorders for Finite Probabilistic Processes
• A behavioural theory for a \(\pi\)-calculus with preorders

This page was built for publication: Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1941882)