Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


kent1176115099.pdf (322.58 KB)

ETD Abstract Container

Abstract Header

Modeling Nondeterminism in Program Semantics using Lifted Binary Multirelations

Saladi, Srikanth
http://rave.ohiolink.edu/etdc/view?acc_num=kent1176115099

Abstract Details

2007, MS, Kent State University, College of Arts and Sciences / Department of Computer Science.
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.
Austin Melton (Advisor)
35 p.
Computer Science
Nondeterminism; Lifted Binary Multirelations

Recommended Citations

Citations

  • Saladi, S. (2007). Modeling Nondeterminism in Program Semantics using Lifted Binary Multirelations [Master's thesis, Kent State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=kent1176115099

    APA Style (7th edition)

  • Saladi, Srikanth. Modeling Nondeterminism in Program Semantics using Lifted Binary Multirelations. 2007. Kent State University, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=kent1176115099.

    MLA Style (8th edition)

  • Saladi, Srikanth. "Modeling Nondeterminism in Program Semantics using Lifted Binary Multirelations." Master's thesis, Kent State University, 2007. http://rave.ohiolink.edu/etdc/view?acc_num=kent1176115099

    Chicago Manual of Style (17th edition)

kent1176115099
735
© 2007, all rights reserved.
This open access ETD is published by Kent State University and OhioLINK.