We study relations between predicate transformers and multifunctions in a topological setting based on closure operators. We give topological definitions of safety and liveness predicates and using these predicates we define predicate transformers. State transformers are multifunctions with values in the collection of fixed points of a closure operator. We derive several isomorphisms between predicate transformers and multifunctions. By choosing different closure operators we obtain multifunctions based on the usual power set construction, on the Hoare, Smyth and Plotkin power domains, and based on the compact and closed metric power constructions. Moreover, they are all related by isomorphisms to the predicate transformers.
CITATION STYLE
Bonsangue, M. M., & Kok, J. N. (1994). Relating multifunctions and predicate transformers through closure operators. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 789 LNCS, pp. 822–843). Springer Verlag. https://doi.org/10.1007/3-540-57887-0_127
Mendeley helps you to discover research relevant for your work.