Markov Abstractions for Probabilistic Pi-Calculus

Hugh Anderson, Gabriel Ciobanu

Abstract


This paper presents a range of approaches to the analysis and development of program specifications that have been expressed in a probabilistic process algebra. The approach explores Markovian processes as a high-level abstraction tool to reason about system specifications. The abstractions include ones to check the structure of specifications, analyze the long-term stability of the system, and provide guidance to improve the specifications if they are found to be unstable. The approach could present interest to the formal methods and critical-systems development community, as it leads to an automatic analysis of some subtle properties of complex systems. We illustrate some aspects by analyzing the Monty Hall game, and a probabilistic protocol.

Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.22.317

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.22.317.314

Hosted By Universit├Ątsbibliothek TU Berlin.