• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Correctness and Refinement of Dually Nondeterministic Programs

Orieta Celiku, Joakim von Wright, Correctness and Refinement of Dually Nondeterministic Programs. TUCS Technical Reports 516, Turku Centre for Computer Science, 2003.

Abstract:

In this paper we extend different reasoning methods from traditional
(demonic) programs to programs with both demonic and angelic
nondeterminism. In particular, we discuss correctness proofs, and
refinement of programs while reducing angelic nondeterminism (into
demonic nondeterminism or determinism). As expected, reducing
angelic nondeterminism is generally not a refinement; however, when
context is taken into consideration, it can result in refinement. We
also show how correctness proofs can be used to implement a winning
strategy for the angel (when such a strategy exists).

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tCevo03a,
  title = {Correctness and Refinement of Dually Nondeterministic Programs},
  author = {Celiku, Orieta and Wright, Joakim von},
  number = {516},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2003},
  ISBN = {952-12-1139-3},
}

Belongs to TUCS Research Unit(s): Learning and Reasoning Lab

Edit publication