Modeling Nondeterminism in Program Semantics using Lifted Binary Multirelations

Title:	Modeling Nondeterminism in Program Semantics using Lifted Binary Multirelations
Author:	Saladi, Srikanth
Description:	Predicate Transformers have been known to model angelic and demonic nondeterminism. However, conventional relational models do not exist to model both kinds of nondeterminism simultaneously. Recent theories have been shown to model both angelic and demonic nondeterminism using binary multirelations which are equivalent to monotone predicate transformers. In this thesis, we model both kinds of nondeterminism using lifted multirelations, which are relations between power sets. The correspondence between the set of relations, set of binary multirelations and the set of lifted multirelations is established using Galois connections. With the help of the above investigations, we list the properties of this lifted binary multirelational model to define the semantics of a program. We define how angelic and demonic nondeterminism can be modeled in this relational model. We then list a few operations for the angelic and demonic nondeterminism. We further define a semantics of program and specification constructs for extensions of Dijkstra’s guarded command language. We then state the properties of binary multirelations in terms of lifted binary multirelations.
Permanent Link:	http://rave.ohiolink.edu/etdc/view?acc_num=kent1176115099 http://hdl.handle.net/2374.OX/17775
Date:	2007

Files in this item

Files	Size	Format	View
There are no files associated with this item.