Trace and Stable Failures Semantics for CSP-Agda

TL;DR

This paper formalizes trace and stable failures semantics for CSP within the Agda proof assistant, enabling modular process development and verified refinement relations in a coinductive, monadic setting.

Contribution

It implements and verifies trace and stable failures semantics for CSP in Agda, adapting to the monadic framework and providing formal proofs of key properties.

Findings

Proof of commutativity of external choice under trace semantics

Refinement w.r.t. stable failures is a partial order

All proofs are type checked in Agda

Abstract

CSP-Agda is a library, which formalises the process algebra CSP in the interactive theorem prover Agda using coinductive data types. In CSP-Agda, CSP processes are in monadic form, which sup- ports a modular development of processes. In this paper, we implement two main models of CSP, trace and stable failures semantics, in CSP-Agda, and define the corresponding refinement and equal- ity relations. Because of the monadic setting, some adjustments need to be made. As an example, we prove commutativity of the external choice operator w.r.t. the trace semantics in CSP-Agda, and that refinement w.r.t. stable failures semantics is a partial order. All proofs and definitions have been type checked in Agda. Further proofs of algebraic laws will be available in the CSP-Agda repository.