# A Branching Time Model of CSP

## TL;DR

This paper introduces a new, more refined branching time model of CSP based on divergence-preserving coupled similarity, which is a congruence for CSP operators and aligns with strong bisimilarity on certain systems.

## Contribution

It presents a novel semantic equivalence for CSP that is finer than previous models and provides a complete axiomatisation for recursion-free terms.

## Key findings

- The new model is finer than all previous CSP models.
- The equivalence is a congruence for CSP operators.
- A complete axiomatisation is achieved for recursion-free terms.

## Abstract

I present a branching time model of CSP that is finer than all other models of CSP proposed thus far. It is obtained by taking a semantic equivalence from the linear time - branching time spectrum, namely divergence-preserving coupled similarity, and showing that it is a congruence for the operators of CSP. This equivalence belongs to the bisimulation family of semantic equivalences, in the sense that on transition systems without internal actions it coincides with strong bisimilarity. Nevertheless, enough of the equational laws of CSP remain to obtain a complete axiomatisation for closed, recursion-free terms.