Sciweavers

LPAR
2004
Springer

Knowledge-Based Synthesis of Distributed Systems Using Event Structures

13 years 9 months ago
Knowledge-Based Synthesis of Distributed Systems Using Event Structures
Abstract. To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck [15] then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.
Mark Bickford, Robert L. Constable, Joseph Y. Halp
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where LPAR
Authors Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
Comments (0)