A complete axiomatic semantics for the CSP stable-failures model

Yoshinao Isobe

(AIST, Japan)

Traditionally, the various semantics of the process algebra CSP are
formulated in denotational style. For many CSP models, e.g., the
traces model, equivalent semantics have been given in operational
style. A CSP semantics in axiomatic style, however, has been
considered problematic in the literature.

In this paper we present a sound and complete axiomatic semantics for
CSP with unbounded nondeterminism over an alphabet of arbitrary
size.

This result is connected in various ways with our tool CSPProver: (1)
the CSP dialect under discussion is the input language of CSPProver;
(2) all theorems presented have been verified with CSPProver; (3)
CSPProver implements the given axiom system.

Tuesday 12th September 2006, 14:00
Robert Recorde Room
Department of Computer Science