Metric Predicate Transformers: Towards a Notion of Refinement for Concurrency

摘要

For two parallel languages with recursion a compositional weakest preconditionsemantics is given using two new metric resumption domains. The underlying domains are characterized by domain equations involving functors that deliver 'observable' and 'safety' predicate transformers. Further a refinement relation is defined for this domains and illustrated by rules dealing with concurrent composition. It turns out, by extending the classical duality of predicate vs. state transformers, that the weakest precondition semantics for the parallel languages is isomorphic to the standard metric state transformers semantics. Moreover, the proposed refinement relation on the predicate transformer domain will correspond to the familiar notion of simulation in the state transformer domain.