Characterisations of testing preorders for a finite probabilistic -calculus

DOI10.1007/S00165-012-0238-3zbMATH Open1259.68143arXiv1201.2258OpenAlexW2122967890MaRDI QIDQ1941882FDOQ1941882

Authors: Alwen Tiu, Yuxin Deng 

Publication date: 22 March 2013

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

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.

Full work available at URL: https://arxiv.org/abs/1201.2258

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)

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)

Cites Work

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

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)