SRC Research Report 38

Can fair choice be added to Dijkstra's calculus?.

Manfred Broy and Greg Nelson.

The paper studies the incorporation of a fair nondeterministic choice operator into a generalization of Dijkstra's calculus of guarded commands. The new operator is not monotonic for the orderings that are generally used for proving the existence of least fixpoints for recursive definitions. To prove the existence of a fixpoint it is necessary to consider several orderings at once, and to restrict the class of recursive definitions.

Back to the SRC Research Reports main page.

• PostScript compressed with UNIX compress -- 1024 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 864 Kbytes
  
• PostScript compressed with ZIP -- 864 Kbytes
  
• PostScript -- 1104 Kbytes
  
• Portable Document Format (PDF) -- 840 Kbytes