Markov Abstractions for Probabilistic Pi-Calculus

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.