Paper: Specification and refinement of probabilistic processes (at LICS 1991)

Authors: Bengt Jonsson Kim G. Larsen

Abstract

A formalism for specifying probabilistic transition systems, which constitute a basic semantic model for description and analysis of, e.g. reliability aspects of concurrent and distributed systems, is presented. The formalism itself is based on transition systems. Roughly a specification has the form of a transition system in which transitions are labeled by sets of allowed probabilities. A satisfaction relation between processes and specifications that generalizes probabilistic bisimulation equivalence is defined. It is shown that it is analogous to the extension from processes to modal transition systems given by K. Larsen and B. Thomsen (1988). Another weaker criterion views a specification as defining a set of probabilistic processes; refinement is then simply containment between sets of processes. A complete method for verifying containment between specifications, which extends methods for deciding containment between specifications, which extends methods for deciding containment between finite automata or tree acceptors, is presented

BibTeX

  @InProceedings{JonssonLarsen-Specificationandref,
    author = 	 {Bengt Jonsson and Kim G. Larsen},
    title = 	 {Specification and refinement of probabilistic processes},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {266--277},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }