# Priorities in tock-CSP

## TL;DR

This paper develops a denotational semantics for prioritisation in tock-CSP, enabling sound reasoning about timed behaviours and refinement, supported by mechanisation in Isabelle/HOL.

## Contribution

It introduces a denotational definition for prioritisation in tock-CSP, establishing a Galois connection to ensure sound, compositional reasoning about timed processes.

## Key findings

- A Galois connection between models is established.
- A denotational semantics for prioritisation is developed.
- Mechanised proofs are provided in Isabelle/HOL.

## Abstract

The $tock$-CSP encoding embeds a rich and flexible approach to modelling discrete timed behaviours in CSP where the event $tock$ is interpreted to mark the passage of time. The model checker FDR provides tailored support for $tock$-CSP, including a prioritisation operator that has typically been used to ensure maximal progress, where time only advances after internal activity has stabilised. Prioritisation may also be used on its own right as a modelling construct. Its operational semantics, however, is only congruent over the most discriminating semantic model of CSP: the finite-linear model. To enable sound and compositional reasoning in a $tock$-CSP setting, we calculate a denotational definition for prioritisation. For that we establish a Galois connection between a specialisation of the finite-linear model, with $tock$ and $\checkmark$, that signals termination, as special events, and $\checkmark$-$tock$-CSP, a model for $tock$-CSP that captures termination, deadlines, and is adequate for reasoning about timed refinement. Our results are mechanised using Isabelle/HOL.