Monotone predicate transformers as Up-closed multirelations

Simple item page
dc.contributor.authorRewitzky I.
dc.contributor.authorBrink C.
dc.date.accessioned2011-05-15T16:02:06Z
dc.date.available2011-05-15T16:02:06Z
dc.date.issued2006
dc.description.abstractIn the study of semantic models for computations two independent views predominate: relational models and predicate transformer semantics. Recently the traditional relational view of computations as binary relations between states has been generalised to multirelations between states and properties allowing the simultaneous treatment of angelic and demonic nondeterminism. In this paper the two-level nature of multirelations is exploited to provide a factorisation of up-closed multirelations which clarifies exactly how multirelations model nondeterminism. Moreover, monotone predicate transformers are, in the precise sense of duality, up-closed multirelations. As such they are shown to provide a notion of effectivity of a specification for achieving a given postcondition. © Springer-Verlag Berlin Heidelberg 2006.
dc.description.versionConference Paper
dc.identifier.citationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.identifier.citation4136 LNCS
dc.identifier.issn3029743
dc.identifier.urihttp://hdl.handle.net/10019.1/12308
dc.subjectBinary codes
dc.subjectData structures
dc.subjectMathematical models
dc.subjectMathematical transformations
dc.subjectSemantics
dc.subjectTheorem proving
dc.subjectBinary relations
dc.subjectMultirelations
dc.subjectNondeterminism
dc.subjectComputation theory
dc.titleMonotone predicate transformers as Up-closed multirelations
dc.typeConference Paper
Files
Collections
Stellenbosch University - Scopus Publications