Isomorphisms between predicate and state transformers

Abstract

We study the relation between state transformers based on directed complete partial orders and predicate transformers. Concepts like ‘predicate’, ‘liveness’, ‘safety’ and ‘predicate transformers’ are formulated in a topological setting. We treat state transformers based on the Hoare, Smyth and Plotkin power domains and consider continuous, monotonic and unrestricted functions. We relate the transformers by isomorphisms thereby extending and completing earlier results and giving a complete picture of all the relationships.