Browse Prior Art Database

A Complete Proof System for an Acceptance-Refusal Model of CSP

IP.com Disclosure Number: IPCOM000128284D
Original Publication Date: 1985-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 31 page(s) / 64K

Publishing Venue

Software Patent Institute

Related People

William G. Golsont: AUTHOR [+3]

Abstract

This paper presents a complete proof system for an acc ep tance- refusal model of the abstract version of Hoare's CSP defined by Brookes, Hoare and Roscoe. Their work interpreted the language in the failures model, which expresses what a process must refuse to do. This paper successfully incorporates ac- ceptances into this general framework, improving upon a previous attempt by Rounds and Brookes. While our model has some similarities to those above, the differences are more fundamental. Our model is constructed from first principles utilizing information systems, reflects an observational paradigm of process behavior which is a departure from those considered previously, and leads to a complete axiornatization of mcceptances and re- fusals over the entire language.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 8% of the total text.

Page 1 of 31

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

A Complete Proof System for an Acceptance-Refusal Model of CSP

William G. Golsont

Rice COMP TR85-19

April 1985 Department of Computer Science Rice University Houston, Texas 77251

t This research was supported in part by NSF grant DCR 84-08580. A Complete Proof System for an Acceptance-Refusal Model of CSP

William G. Gol8ont Department of Computer Science Rice University Houston, Texas 77251

Abstract

This paper presents a complete proof system for an acc ep tance- refusal model of the abstract version of Hoare's CSP defined by Brookes, Hoare and Roscoe. Their work interpreted the language in the failures model, which expresses what a process must refuse to do. This paper successfully incorporates ac- ceptances into this general framework, improving upon a previous attempt by Rounds and Brookes. While our model has some similarities to those above, the differences are more fundamental. Our model is constructed from first principles utilizing information systems, reflects an observational paradigm of process behavior which is a departure from those considered previously, and leads to a complete axiornatization of mcceptances and re- fusals over the entire language.

0. Introduction and Preliminaries

Recent reseaxch into establishing a semantics for concurrency that respects observational and operational intuitions began with Nfilner's CCS [Nlil]. His calculus contains a handful of basic combina, tors having straightforwaxd operational interpretations. The algebraic laws for the combinators are derived with the purpose of characterizing observational behavior. In [deNHI the behavior of processes is represented by performance on tests. Preorders are defined over processes based on the ability to pass tests and the ability not to fail them. Through these operationally defined relations, vaxious complete proof systems for COS and fully abstract denotational models are obtained.

Since its formulation, the CSP language [Hoa] has provided a standard to measure semantic theories. One mathematical model for an abstract version of CSP, the failures approach, appears in [BHR]. While the model is denotational in style, the underlying notion of a process, the nondeterministic transition system, is strictly an operational one. In an attempt to understand the interplay between the works of [deNH] and [B.'LU-Lj', de Nicola [deN] presents a proof system for a sublanguage of CSP based on the failures model, but was unable to axiomatize the full language. In [Bro], Brookes develops a complete proof system for the entire language based on an extension to the failure's model.

Rice University Page 1 Dec 31, 1985

Page 2 of 31

A Complete Proof System for an Acceptance-Refusal Model of CSP

The failures model deals with refusals, what a process must refuse to do in a given situation. The dual notion, acceptances, or what a process must do, has been investigated by Hennessy [Hen] and Rounds and Br...