Deriving Relationship Between Semantic Models - An Approach for cCSP

TL;DR

This paper establishes a formal connection between operational and denotational semantics for cCSP by deriving traces from operational rules and proving their correspondence, strengthening the language's formal foundation.

Contribution

It presents a novel method to derive denotational semantics from operational semantics for cCSP, demonstrating their equivalence.

Findings

Operational and trace semantics are shown to be equivalent for cCSP

Traces are extracted from operational rules using induction

The approach enhances the formal understanding of cCSP semantics

Abstract

Formal semantics offers a complete and rigorous definition of a language. It is important to define different semantic models for a language and different models serve different purposes. Building equivalence between different semantic models of a language strengthen its formal foundation. This paper shows the derivation of denotational semantics from operational semantics of the language cCSP. The aim is to show the correspondence between operational and trace semantics. We extract traces from operational rules and use induction over traces to show the correspondence between the two semantics of cCSP.