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.
Full Text:
PDFDOI: 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.