A Complete Axiomatic Semantics for the CSP Stable-Failures Model

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 Csp-Prover: (1) the Csp dialect under discussion is the input language of Csp-Prover; (2) all theorems presented have been verified with Csp-Prover; (3) Csp-Prover implements the given axiom system.

• Type: Conference
• Year: 2006
• Where: CONCUR
• Authors: Yoshinao Isobe, Markus Roggenbach
• Keywords: CONCUR 2006, Csp Semantics, Distributed And Parallel Computing, Process Algebra Csp, Semantics