Logic in Computer Science (LICS 1995)

Paper: Compositional Testing Preorders for Probabilistic Processes (at LICS 1995)

Authors: Bengt Jonsson Wang Yi

Abstract

Transition systems are well-established as a semantic model for distributed systems. There are widely accepted preorders that serve as criteria for refinement of a more abstract transition system to a more concrete one. To reason about probabilistic phenomena such as failure rates, we need to extend models and methods that have proven successful for non-probabilistic systems to a probabilistic setting. In this paper, we consider a model of probabilistic transition systems, containing probabilistic choice and nondeterministic choice as independent concepts. We present a notion of testing for these systems. Our main contributions are denotational characterizations of the testing preorders. The characterizations are given in terms of chains for may-testing and refusal chains for must-testing, that are analogous to traces and failures in denotational models of CSP. Refinement corresponds to inclusion between chains and refusal chains modulo closure operations. The preorders are shown to be compositional. We also show that when restricted to non-probabilistic systems, these preorders collapse to the standard simulation and refusal- simulation.

BibTeX

  @InProceedings{JonssonWangYi-CompositionalTestin,
    author = 	 {Bengt Jonsson and Wang Yi},
    title = 	 {Compositional Testing Preorders for Probabilistic Processes},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {431-441},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }