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.

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.

Tables

Table 1. Table 1: The healthiness conditions of ℱ ​ ℒ ℱ ℒ \mathcal{FL} .

Name	Definition
$\mathrm{𝐅𝐋𝟎}\left(P\right)$	$P\ne \varnothing$
$\mathrm{𝐅𝐋𝟏}\left(P\right)$	$\rho \le \sigma \wedge \sigma \in P\Rightarrow \rho \in P$
$\mathrm{𝐅𝐋𝟐}\left(P\right)$	$\rho {}_{ℱℒ}⟨A{⟩}_{ℱℒ}\in P\wedge e{\in }_{ℱℒ}A$ $\Rightarrow \rho {}_{ℱℒ}⟨(A,e),\bullet {⟩}_{ℱℒ}\in P$
$\mathrm{𝐅𝐋𝟑}\left(P\right)$	$P\subseteq FL$

Equations

$$S$$

$$T$$

$$\offinterlineskip\halign to=433.62pt{\strut{\color{ZedBoxColor}\vrule width\arrayrulewidth}\hskip\zedleftsep{$\color{ZedColor}\@zlign#$}\hfil\cr[rgb]{1,0.39,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.39,0.13}\pgfsys@color@cmyk@stroke{0}{0.61}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.61}{0.87}{0}\vrule width=0.4pt}\hskip 10.00002pt{$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Aev : Acc \times\Sigma^{\tick}_{tock} \crcr\hbox{\color[rgb]{1,0.39,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.39,0.13}\pgfsys@color@cmyk@stroke{0}{0.61}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.61}{0.87}{0}\vrule height=3.0pt,width=0.4pt}\cr\hbox{\color[rgb]{1,0.39,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.39,0.13}\pgfsys@color@cmyk@stroke{0}{0.61}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.61}{0.87}{0}\vrule height=0.4pt,width=60.00009pt}\cr\hbox{\color[rgb]{1,0.39,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.39,0.13}\pgfsys@color@cmyk@stroke{0}{0.61}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.61}{0.87}{0}\vrule height=3.0pt,width=0.4pt}\cr[rgb]{1,0.39,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.39,0.13}\pgfsys@color@cmyk@stroke{0}{0.61}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.61}{0.87}{0}\vrule width=0.4pt}\hskip 10.00002pt{$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathop{\mathstrut{\forall}}\nolimits B : \mathop{\mathstrut{\mathbb{P}}}\nolimits\Sigma^{\tick}_{tock}; (aset\penalty 10000\ B,e) : Aev @ e \in B \crcr}$$

$$\mathbf{Pr}{\mathbf{i}}_{\le }(P)\widehat{=}\{\rho ,\sigma :FL|\rho {\mathbf{pri}}_{\le }\sigma \wedge \sigma \in P@\rho \}$$

$$traces(\mathbf{Pr}{\mathbf{i}}_{\le }(R))$$

$${\mathbf{Pri}}_{\le }\circ {\mathbf{Pri}}_{\le }(P)={\mathbf{Pri}}_{\le }(P)$$

$${\mathbf{Pri}}_{\le }(P{\sqcap }_{\mathcal{F}\mathcal{L}}Q)={\mathbf{Pri}}_{\le }(P){\sqcap }_{\mathcal{F}\mathcal{L}}{\mathbf{Pri}}_{\le }(Q)$$

$${\mathbf{Pri}}_{\le }(a{\to }_{\mathcal{F}\mathcal{L}}P)=a{\to }_{\mathcal{F}\mathcal{L}}{\mathbf{Pri}}_{\le }(P)$$

$$\displaystyle\href https://github.com/robo-star/tick-tock-CSP/blob/master/TickTock-FL/TickTock_Max_FL.thy#L170(P)$$

$$\displaystyle\href https://github.com/robo-star/tick-tock-CSP/blob/master/TickTock-FL/TickTock_Max_FL.thy#L298(P)$$

$$T=\left(\begin{array}{rl}& (a\to \mathbf{Skip}\sqcap (\mathbf{Wait}1;T))\\ \square & (b\to \mathbf{Skip}\sqcap (\mathbf{Wait}1;T))\end{array}\right)$$

$${\mathbf{Pr}{\mathbf{i}}_{\mathbf{TT}}}_{\le }(P)\widehat{=}fl2tt\circ {\mathbf{Pri}}_{\le }\circ tt2fl(P)$$

Full text

††journal: Information Processing Letters

1 Introduction

Process algebras like CSP [1] enable modelling of reactive systems via named events that correspond to atomic and instantaneous interactions of interest. To specify budgets and deadlines, and to reason about liveness and safety over time, an explicit notion of time is required. Roscoe introduced the $tock$-CSP encoding, where an event $tock$ is used to mark the passage of discrete time. Extensive use of $tock$-CSP has been reported [2, 3, 4, 5, 6].

The CSP model-checker FDR [7] has operators tailored for $tock$-CSP. In addition, it implements a $\mathbf{Pri_{\leq}}(P)$ operator that can be used to prioritise events according to a partial order $\leq$. The behaviour is that of $P$, but changed so that whenever events $a$ and $b$ are available, then if $b$ is of strictly higher priority than $a$, that is, $a<b$, then $a$, and the behaviour following $a$, is pruned.

Example 1**.**

$R=a\mathrel{\rightarrow}\mathbf{Skip}\mathrel{\Box}b\mathrel{\rightarrow}\mathbf{Skip}$. Process $R$ offers an external choice () between behaving as a prefixing ($\mathrel{\rightarrow}$) on $a$ or $b$, followed by immediate termination ($\mathbf{Skip}$). Prioritising $R$, with $a<b$ yields the process $b\mathrel{\rightarrow}\mathbf{Skip}$.∎

Prioritisation can be used in FDR to enforce maximal progress, that is, that time can only advance after internal activity has stabilised, by prioritising $\tau$, the internal action, and , which signals termination, over $tock$. $\mathbf{Pri_{\leq}}$ also endows CSP with extra expressivity [8], and has been applied also in abstraction techniques [9], reducing refinement in different CSP semantics to traces refinement [10], or as a modelling construct on its own [5, 6].

The operator $\mathbf{Pri_{\leq}}$ has an intuitive operational semantics. However, for $\mathbf{Pri_{\leq}}$ to be congruent over denotational models of CSP, namely the finite-linear ($\mathcal{FL}$ [1]) and refusal testing ($\mathcal{RT}$ [11, 12]) models, the partial order needs to be constrained [8]. Thus, FDR actually implements a constrained form of $\mathbf{Pri_{\leq}}$, where, for example, and $\tau$ are maximal in the order. However, this is insufficient for $\mathbf{Pri_{\leq}}$ to be congruent over weaker models such as -$tock$ [13] and the stable-failures ($\mathcal{F}$ [1]).

Example 2**.**

[TABLE]

Process $S$ makes an internal choice ($\mathrel{\sqcap}$) between offering events $a$, or $b$, and terminating, or waiting a time unit ($\mathbf{Wait}\,1$) and then behaving as $S$ again, specified using sequential composition ($\,\mathchar 24635\relax\;$). Process $T$ also makes an internal choice, but the choice between $a$ and $b$ is external. Although it may seem that $T$ is more deterministic than $S$, deadlocking for a time unit, before making an internal choice again that may lead to the refusal of $a$ and $b$, is a possibility for $T$. The -$tock$ model does not distinguish $S$ and $T$, just like the $\mathcal{F}$ model does not distinguish $a\mathrel{\rightarrow}\mathbf{Skip}\mathrel{\sqcap}b\mathrel{\rightarrow}\mathbf{Skip}\mathrel{\sqcap}\mathbf{Stop}$ and $(a\mathrel{\rightarrow}\mathbf{Skip}\mathrel{\Box}b\mathrel{\rightarrow}\mathbf{Skip})\mathrel{\sqcap}\mathbf{Stop}$.

However, prioritising $S$ and $T$, with $a<b$, assuming and $tock$ are maximal in the order and that $tock$ is not prioritised over $b$, yields different results. $T$ becomes equal to a process $priT=b\mathrel{\rightarrow}\mathbf{Skip}\mathrel{\sqcap}(\mathbf{Wait}\,1\,\mathchar 24635\relax\;priT)$, whereas the prioritisation of $S$ bears no effect. The incongruence arises as a result of $\mathbf{Pri_{\leq}}$ being defined over $\mathcal{FL}$, where it distributes over internal choice. To reason about priorities in other models we need different definitions for $\mathbf{Pri_{\leq}}$.∎

In this paper we calculate a definition of $\mathbf{Pri_{\leq}}$ for $tock$-CSP via a stepwise Galois connection between the $\mathcal{FL}$ model and the -$tock$ model [13], the only sound model for $tock$-CSP that can be used to reason about timed refinement, and that captures deadlines, termination and erroneous Zeno behaviour. It is a faithful account of the $tock$-CSP dialect and is mechanised in Isabelle/HOL [14]. Included in this work is a mechanisation of the $\mathcal{FL}$ model, that handles termination, via the special event , and a specialisation that includes $tock$.

This paper is structured as follows. In Section 2.1 we describe -$tock$ and $\mathcal{FL}$. In Section 3 we formally define $\mathcal{FL}$. In Section 4 we define a Galois connection between a specialisation of $\mathcal{FL}$, which includes $tock$ as event, and calculate the induced definition of $\mathbf{Pri_{\leq}}$. We conclude in Section 5.

2 Models

Here we describe the -$tock$ and $\mathcal{FL}$ models by summarizing material from [13] and [1].

2.1 -$tock$

The -$tock$ model is defined in terms of a set $\Sigma$ of events, not including and $tock$. The complete set is defined as $\Sigma_{tock}$. The semantics of processes is a set of sequences of observations of type $Obs$, defined below. An observation is either an event in $\Sigma_{tock}$, or the refusal of some subset of $\Sigma_{tock}$, so $Obs$ has two constructor functions $evt$ and $ref$.

Definition 1.

$Obs::=evt\langle\!\langle\Sigma_{tock}\rangle\!\rangle|ref\langle\!\langle\mathop{\mathstrut{\mathbb{P}}}\nolimits\Sigma_{tock}\rangle\!\rangle$**

The type of valid traces is defined as $TT$, which is the set of all sequences $t$ with elements of type $Obs$ that satisfy three conjuncts, defined below.

Definition 2.

$\begin{aligned} &TT==\{t:\mathop{\mathrm{seq}}Obs|\mathop{\mathstrut{\forall}}\nolimits i:\mathop{\mathrm{dom}}t@\\ &\begin{aligned} &i<\#t\mathrel{\Rightarrow}t(i)\neq evt\,\tick\mathrel{\wedge}\\ &(i<\#t\mathrel{\wedge}t(i)\in\mathop{\mathrm{ran}}ref)\mathrel{\Rightarrow}t(i+1)=evt\,tock\mathrel{\wedge}\\ &t(i)=evt\,tock\mathrel{\Rightarrow}(i>1\mathrel{\wedge}t(i-1)\in\mathop{\mathrm{ran}}ref)\end{aligned}\}\end{aligned}$**

The first conjunct ensures that can only appear as the last event of $t$. The second conjunct requires that every refusal before the last ($i<\#t$) is followed by a $tock$. Finally, the third conjunct ensures that every $tock$ is preceded by a refusal.

The healthiness conditions of -$tock$ [13], whose composition is named $\mathbf{TT}$, ensure properties of the standard models of CSP in the context of $TT$ traces. Namely, the empty trace is an observation of every process; prefix closure and subset closure of refusals; and an event that cannot be performed is refused. Finally, whenever there is a stable refusal in a trace, then there is always at least one (other) trace where the refusal includes .

2.2 Finite-linear

The $\mathcal{FL}$ model is characterised in [1] by finite sequences $\mathord{\langle}A_{0},e_{0},\ldots,A_{i},e_{i},A_{i+1}\mathord{\rangle}$ of alternating acceptances $A_{i}$ and events $e_{i}$. An acceptance is either a set, recording the events being offered, or null ($\bullet$) indicating the impossibility to observe such a set because of instability. An event $e_{i}$ necessarily belongs to $A_{i}$ if $A_{i}$ is not $\bullet$. Valid sequences end in an acceptance, or $\bullet$ followed by . The healthiness conditions of $\mathcal{FL}$ ensure prefix closure, and require that, whenever an acceptance $A_{i}$ is observed, then any events in $A_{i}$ can also be performed.

The prefix relation for sequences in this model allows $\bullet$ to precede a stable acceptance set, so that $\mathord{\langle}\bullet\mathord{\rangle}$ and $\mathord{\langle}\bullet,e_{0},\bullet\mathord{\rangle}$ are prefixes of $\mathord{\langle}A_{0},e_{0},A_{1}\mathord{\rangle}$, for example. Crucially, and unlike other CSP models, there is no upward-closure of acceptance sets.

3 Formalising the $\mathcal{FL}$ model

In Section 3.1 we define a recursive data type to capture $\mathcal{FL}$ traces. In Section 3.2 we formalise the healthiness conditions. Finally, in Section 3.3 we formally define $\mathbf{Pri_{\leq}}$. While Roscoe [1] characterises the $\mathcal{FL}$ model and studies in depth its relationship to other CSP models, here we define its data model and healthiness conditions with the level of formality required to mechanise it (as an Isabelle theory as presented in [15], for example).

3.1 Model

An acceptance is either a null acceptance or a set of events. It is defined by the type $Acc$, which has two constructor functions $\bullet$ and $aset$, respectively, where $\langle\!\langle\leavevmode\vbox{\hrule width=5.0pt}\rangle\!\rangle$ is the Z [16] syntax for constructors.

Definition 3.

$Acc::=\bullet|aset\langle\!\langle\mathop{\mathstrut{\mathbb{P}}}\nolimits\Sigma_{tock}\rangle\!\rangle$**

We also define: $e\in_{\mathcal{FL}}A$ to be $true$ exactly when $A$ is the result of applying $aset\,B$ for some set $B$ and $e\in B$; and a prefix order on $Acc$, where $\bullet$ is the least element, and $aset\,A\leq aset\,A$, which can be lifted to define the prefix order on $FL$ traces.

An acceptance followed by an event is a pair of type $Aev$ associating elements of $Acc$ to $\Sigma_{tock}$.

Definition 4 (Acceptance-event).

[TABLE]

An acceptance-event pair $(aset\,B,e)$ is valid exactly when $e$ is a member of set $B$. A pair $(\bullet,e)$ imposes no condition on $e$. Next we define the type of non-empty traces for $\mathcal{FL}$ as $FL$, a recursive data type with two constructors, $acc$ and $aev$.

Definition 5.

$FL::=acc\langle\!\langle Acc\rangle\!\rangle|aev\langle\!\langle Aev\times FL\rangle\!\rangle$**

The function $acc$ takes a single acceptance while $aev$ takes an acceptance-event pair and an $FL$ trace. Processes in $\mathcal{FL}$ are defined by a set of $FL$ traces, effectively finite non-empty sequences ending in an acceptance. Unlike the original presentation of $\mathcal{FL}$, we consider as a regular event. This simplifies the type definition of $FL$ and allows us to give a general account of $\mathbf{Pri_{\leq}}$ where can be prioritised.

To facilitate presentation we abbreviate $acc\,A$ as $\mathord{\langle}A\mathord{\rangle}_{\mathcal{FL}}$, and $aev\,((A,e),\rho)$ as $(A,e)\,\#\,\rho$. Furthermore a recursive application of $\#$ a number of times, such as $(A_{0},e_{0})\,\#\,(\ldots\,\#\,A_{i})$ is abbreviated as $\mathord{\langle}(A_{0},e_{0}),\ldots,A_{i}\mathord{\rangle}_{\mathcal{FL}}$. This is a typical approach to encoding finite lists via recursive data types.

3.2 Healthiness conditions

The healthiness conditions are listed in Section 3.2. The first, $\mathbf{FL0}$, although not listed in [1, p.257], is required to ensure that every process has some behaviour. Together with $\mathbf{FL1}$ (adopted from [1]), which ensures prefix closure, $\mathbf{FL0}$ ensures that every process has at least the trace $\mathord{\langle}\bullet\mathord{\rangle}_{\mathcal{FL}}$.

The next condition $\mathbf{FL2}$ from [1] is restated using $\in_{\mathcal{FL}}$ and a concatenation operator \mathbin{\smash{\raise 3.44444pt\hbox{\smallfrown}}}_{\mathcal{FL}} that is closed under $FL$, unlike the general sequence concatenation operator. $\mathbf{FL2}$ states that whenever a trace $\rho$ concatenated with an acceptance $A$ is in $P$, then for every event $e$ in $A$ there must be a trace in $P$ that performs $e$. It is the result of concatenating $\rho$ with the trace consisting of the acceptance-event pair $(A,e)$ followed by $\bullet$.

To ensure is only possible after $\bullet$ as the very last event of a trace, $\mathbf{FL3}$ requires valid traces to be in a set $FL$. It consists of $FL$ traces where is not offered in any acceptance and, if appears, it is as the last event followed by $\bullet$.

The $\mathcal{FL}$ model forms a complete lattice under the refinement order defined by subset inclusion. The top is the process $\mathbf{div}$ whose only observation is the trace $\mathord{\langle}\bullet\mathord{\rangle}_{\mathcal{FL}}$, while the bottom is $FL$, the set of all possible observations: the process $\mathbf{Chaos}(\Sigma)$.