Multivalued Possibilities Mappings

Abstract
Ion mappings are one of the major tools used to construct correctness proofs for concurrent algorithms. Several examples are given of situations in which it is useful to allow the abstraction mappings to be multivalued. The examples involve algorithm optimization, algorithm distribution, and proofs of time bounds. Abstraction mappings are one of the major tools that the author and colleagues use to construct correctness proofs for concurrent (including distributed) algorithms. In this paper, she tries to make one major point about such mappings: that it is useful to allow them to be multivalued. That is, often when one maps a low-level algorithm L to a high- level algorithm H, one would like to allow several states of H to correspond to a single state of L. I believe that any useful framework for describing abstraction mappings should include the ability to describe multivalued mappings.

This publication has 0 references indexed in Scilit: