# Translating between models of concurrency

## TL;DR

This paper introduces a method to transform refinement questions across various finite observational models of CSP into trace refinement tests using a priority operator, enhancing practical verification tools.

## Contribution

It generalizes the use of the priority operator to any rational finite observational model, enabling broader refinement checking capabilities in tools like FDR4.

## Key findings

- Transform refinement questions into trace refinement tests
- Generalize to any rational finite observational model
- Enable practical refinement checking in Timed CSP

## Abstract

Hoare's Communicating Sequential Processes (CSP) admits a rich universe of semantic models closely related to the van Glabbeek spectrum. In this paper we study finite observational models, of which at least six have been identified for CSP, namely traces, stable failures, revivals, acceptances, refusal testing and finite linear observations. We show how to use the recently-introduced \emph{priority} operator to transform refinement questions in these models into trace refinement (language inclusion) tests. Furthermore, we are able to generalise this to any (rational) finite observational model. As well as being of theoretical interest, this is of practical significance since the state-of-the-art refinement checking tool FDR4 currently only supports two such models. In particular we study how it is possible to check refinement in a discrete version of the Timed Failures model that supports Timed CSP.