Trace and Stable Failures Semantics for CSP-Agda

Bashar Igried
(Dept. of Computer Science, Swansea University)
Anton Setzer
(Dept. of Computer Science, Swansea University)

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.

In Ekaterina Komendantskaya and John Power: Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types (CoALP-Ty'16), Edinburgh, UK, 28-29 November 2016, Electronic Proceedings in Theoretical Computer Science 258, pp. 36–51.
Published: 13th September 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: