Paper Info
Title
A complete axiomatic semantics for the CSP stable-failures model
Abstract
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.
Year
DOI
Venue
2006
10.1007/11817949_11
CONCUR
Keywords
Field
DocType
csp model,axiomatic style,csp stable-failures model,various semantics,process algebra csp,csp dialect,denotational style,tool csp-prover,csp semantics,equivalent semantics,complete axiomatic semantics,process algebra
Discrete mathematics,Operational semantics,Programming language,Axiomatic semantics,Concurrency,Axiom,Computer science,Denotational semantics,Proof theory,Theoretical computer science,Process calculus,Unbounded nondeterminism
Conference
Volume
ISSN
ISBN
4137
0302-9743
3-540-37376-4
Citations 
PageRank 
References 
9
0.57
5
Authors
2
Name
Order
Citations
PageRank
Yoshinao Isobe1587.84
Markus Roggenbach229432.63