A Complete Axiomatic Semantics for the CSP Stable-Failures Model | Zendy

Yoshinao Isobe | Zendy; Markus Roggenbach | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Complete Axiomatic Semantics for the CSP Stable-Failures Model

Author(s) -

Yoshinao Isobe,

Markus Roggenbach

Publication year - 2006

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-37376-4

DOI - 10.1007/11817949_11

Subject(s) - axiom , gas meter prover , computer science , denotational semantics , programming language , semantics (computer science) , automated theorem proving , operational semantics , process calculus , axiomatic semantics , theoretical computer science , algebra over a field , algorithm , mathematics , mathematical proof , pure mathematics , geometry

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research