Priorities in tock-CSP

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.


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 Pri ≤ (P ) operator that can be used to prioritise events according to a partial order ≤. 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.
Process R offers an external choice (✷) between behaving as a prefixing (→) on a or b, followed by immediate Email addresses: pedro.ribeiro@york.ac.uk (Pedro Ribeiro), james.baxter@york.ac.uk (James Baxter), ana.cavalcanti@york.ac.uk (Ana Cavalcanti) termination (Skip). Prioritising R, with a < b yields the process b → 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 τ , the internal action, and , which signals termination, over tock . Pri ≤ 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 Pri ≤ has an intuitive operational semantics.
However, for Pri ≤ to be congruent over denotational models of CSP, namely the finite-linear (F L [1]) and refusal testing (RT [11,12]) models, the partial order needs to be constrained [8]. Thus, FDR actually implements a constrained form of Pri ≤ , where, for example, and τ are maximal in the order. However, this is insufficient for Pri ≤ to be congruent over weaker models such as -tock [13] and the stable-failures (F [1]). Process S makes an internal choice (⊓) between offering events a, or b, and terminating, or waiting a time unit (Wait 1) and then behaving as S again, specified using sequential composition ( ; ). 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 F model does not 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 → Skip ⊓ (Wait 1 ; priT ), whereas the prioritisation of S bears no effect. The incongruence arises as a result of Pri ≤ being defined over F L, where it distributes over internal choice. To reason about priorities in other models we need different definitions for Pri ≤ .
In this paper we calculate a definition of Pri ≤ for tock -CSP via a stepwise Galois connection between the F L 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 F L 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 F L. In Section 3 we formally define F L. In Section 4 we define a Galois connection between a specialisation of F L, which includes tock as event, and calculate the induced definition of Pri ≤ . We conclude in Section 5.

Models
Here we describe the -tock and F L models by summarizing material from [13] and [1].

-tock
The -tock model is defined in terms of a set Σ of events, not including and tock . The complete set is defined as Σ tock . The semantics of processes is a set of sequences of observations of type Obs, defined below. An observation is either an event in Σ tock , or the refusal of some subset of Σ tock , so Obs has two constructor functions evt and ref .
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.
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 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 .

Finite-linear
The F L model is characterised in [1] by finite sequences A 0 , e 0 , . . . , A i , e i , A i+1 of alternating acceptances A i and events e i . An acceptance is either a set, recording the events being offered, or null (•) 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 •. Valid sequences end in an acceptance, or • followed by . The healthiness conditions of F L 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 • to precede a stable acceptance set, so that • and •, e 0 , • are prefixes of A 0 , e 0 , A 1 , for example. Crucially, and unlike other CSP models, there is no upward-closure of acceptance sets.

Formalising the F L model
In Section 3.1 we define a recursive data type to capture F L traces. In Section 3.2 we formalise the healthiness conditions. Finally, in Section 3.3 we formally define Pri ≤ . While Roscoe [1] characterises the F L 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).

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 • and aset , respectively, where is the Z [16] syntax for constructors.
Definition 3. Acc ::= • | aset P Σ tock We also define: e ∈ F L A to be true exactly when A is the result of applying aset B for some set B and e ∈ B ; and a prefix order on Acc, where • is the least element, and aset A ≤ 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 Σ tock .

Definition 4 (Acceptance-event).
Aev : Acc × Σ tock ∀ B : P Σ tock ; (aset B , e) : Aev • e ∈ B An acceptance-event pair (aset B , e) is valid exactly when e is a member of set B . A pair (•, e) imposes no condition on e. Next we define the type of nonempty traces for F L as FL, a recursive data type with two constructors, acc and aev . The function acc takes a single acceptance while aev takes an acceptance-event pair and an FL trace. Processes in F L are defined by a set of FL traces, effectively finite non-empty sequences ending in an acceptance. Unlike the original presentation of F L, we consider as a regular event. This simplifies the type definition of FL and allows us to give a general account of Pri ≤ where can be prioritised.
To facilitate presentation we abbreviate acc A as A F L , and aev ((A, e), ρ) as (A, e) # ρ. Furthermore a recursive application of # a number of times, such as (A 0 , e 0 ) # (. . . # A i ) is abbreviated as (A 0 , e 0 ), . . . , A i F L . This is a typical approach to encoding finite lists via recursive data types.

Name
Definition

Healthiness conditions
The healthiness conditions are listed in Table 1. The first, FL0, although not listed in [1, p.257], is required to ensure that every process has some behaviour. Together with FL1 (adopted from [1]), which ensures prefix closure, FL0 ensures that every process has at least the trace • F L .
The next condition FL2 from [1] is restated using ∈ F L and a concatenation operator F L that is closed under FL, unlike the general sequence concatenation operator. FL2 states that whenever a trace ρ 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 ρ with the trace consisting of the acceptance-event pair (A, e) followed by •.
To ensure is only possible after • as the very last event of a trace, 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 •.
The F L model forms a complete lattice under the refinement order defined by subset inclusion. The top is the process div whose only observation is the trace • F L , while the bottom is FL , the set of all possible observations: the process Chaos(Σ).

Prioritise
The semantics of Pri ≤ (P ) is defined in [8] pointwise over the FL traces of P as follows.
It is the set of traces ρ related by pri ≤ to a trace σ drawn from P , that is, a trace ρ is a possible prioritisation of σ. The relation pri ≤ is a fully specified version of that presented in [8], generalised to cater for any event, including , and defined inductively in Definition 7 as required for mechanical reasoning.
Observe that pri p is parametric over an arbitrary partial order p on events. Before explaining the definition, we illustrate the calculation of traces ρ, as related by pri ≤ , from traces σ of process R (of Example 1), assuming a < b and that is maximal in the order. The set of traces of R is presented below, as well as those of Pri ≤ (R), where we omit the F L subscripts. We observe that the result is independent of whether b is maximal in the order.
We have traces: aset {a, b} recording that both events a and b are stably offered, and traces such as (aset {a, b}, a), (•, ), • recording that after stably offering both events, and performing event a, then termination, encoded by happens unstably, and similarly for event b; and finally traces that complete the prefix closure as required by FL1.
Prioritisation of R with a < b, as previously discussed in Section 1, leads to pruning the behaviours of the prefixing on a. The traces of Pri ≤ (R) are those related to the traces of R by pri ≤ .
The trace • is related to itself as it is a valid observation of every process in F L. The trace aset {b} is related to aset {a, b} , as {b} is the set obtained by eliminating events in {a, b} for which an event of strictly higher priority is also in the set, namely a is eliminated as b is of higher priority. Similarly, the trace (aset  pri In general, a trace A is related to Z by pri p , whenever A is priacc p (Z ), specified below, that defines the result of prioritising an acceptance Z . In Example 3 above, we have that priacc ≤ (aset {a, b}) = aset {b}.
Definition 8. priacc Formally, priacc p (•) is •, whereas for an acceptance set Z , priacc p (aset Z ) is the acceptance set of events in Z for which no event b of strictly higher priority, according to the order p, exists in Z . A trace (A, e) # ρ is related to (Z , e) # σ by pri p exactly when A is a prefix of the acceptance permitted by prioritisation, as defined by priacc p (Z ), ρ is related to σ by pri p , and if the event e is not maximal in the partial order p, where max (p, e) = ¬ ∃ x • e < p x , that is, no other event has strictly higher priority than e, then e must be in the acceptance permitted by prioritisation. In other words, events of maximal priority are never eliminated, whereas those for which an event of higher priority exists need to be in the resulting acceptance set obtained via the intersection. In particular, if Z is • and e is not maximal, then it is not related by pri p . Although our definition of pri p is rather concise, we have established using our mechanisation that it is equivalent to that of Roscoe [8].
A formal definition for pri ≤ suitable for mechanical reasoning enables key results about Pri ≤ to be established, namely that it is monotonic and closed under the healthiness conditions. Using our mechanisation we have established the following novel results where the subscript F L indicates that these are operators of the F L model.
The first result in Lemma 1 establishes that Pri ≤ is idempotent; the second that it distributes through internal choice; and the third that it distributes through prefixing. It also distributes through sequential composition, as established next.

Lemma 2.
Provided has maximal priority, In this case must be maximal in the order, as otherwise the possibility for P to terminate could be eliminated. More interestingly, the prioritisation of an external choice between prefixings on events a and b, where a < b, is the prioritisation of the prefixing on b, with any behaviour following on from a pruned, as established by the lemma.
Proof of this, and other key results, is available 1 .
Our formalisation of F L and Pri ≤ are used next to calculate a definition for Pri ≤ in -tock .

Galois connection
The key to defining a Galois connection between F L and -tock is relating FL traces, which record acceptances before every event, and TT traces, which instead record subset-closed refusals, and only before tock events or at the end of a trace, as previously discussed in Section 2.1. We define the Galois connection stepwise to simplify proofs. In Section 4.1 we first consider a Galois connection between F L and a variant of -tock where refusals sets are not subset closed; instead they are maximal: they record exactly what is refused. In the following Section 4.2 we define a Galois connection with full -tock by completing the subset closure of refusals. Fig. 1, which is explained as we discuss each step, provides a depiction of the connections. Finally, in Section 4.3, we present the result of calculating the induced definition of Pri ≤ for -tock .

From F L-tock to maximal -tock
The pair of functions fl 2ttm and ttm2fl , mapping between F L-tock and the maximal variant oftock , labelled as TTM in Fig. 1, is defined below.
The function fl 2ttm is defined as the set of traces obtained by applying fl 2ttobs, a total non-injective function from FL to TT traces, defined next, to every trace ρ in P . The inverse mapping ttm2fl is uniquely defined in terms of fl 2ttm, and is the distributed union over the set of FL processes that can be mapped via fl 2ttm to be a subset of P . This construction is standard for Galois connections where one adjoint uniquely defines the other. The function fl 2ttobs is defined as follows. It maps: the null trace • F L to the empty trace , since -tock does not record instability; and every trace whose only element is an acceptance set aset A to a singleton trace consisting of a refusal obtained as the set complement of A. The mapping of an acceptance-event pair followed by a trace ρ is split into three cases: (1) acceptances a preceding regular events e, other than tock , are mapped to a trace evt e whose only element is the event e, concatenated with the result of applying fl 2ttobs to ρ, since -tock does not record refusals before such events; (2) for the same reason, null acceptances preceding tock are mapped to the empty trace; (3) acceptance sets preceding tock are mapped to a trace consisting of a refusal set, obtained as the complement of A, followed by the event tock , concatenated with the application of fl 2ttobs to ρ.
The functional application of fl 2ttm to a healthy process P satisfies nearly all the healthiness conditions of -tock , as established by Lemma 4. It also satisfies extra healthiness conditions, defined below. They are relevant to obtain the final Galois connection in the next section. Namely, fl 2ttm(P ) satisfies TT0 and TT2-4, but not TT1 [13], which requires subset closure of refusals. This is expected, as fl 2ttobs is a function. (The subset closure of refusals is completed by the connection in Section 4.2.) Instead, we have prefixclosure of sequences, ensured by a healthiness condition we call TT1w, a weaker form of TT1 that does not enforce subset closure of refusals.
In addition, refusals are maximal, and so fl 2ttm(P ) satisfies the additional conditions TTM1-3 listed in Table 2. TTM1 requires that every event e that is not refused can be performed. TTM2 is similar, but requires tock to happen after the refusal. TTM3 requires that P is a subset of TT , the set of all traces where every refusal contains . The three conditions, together named TTM (see Fig. 1), characterise the set of -tock processes whose refusal sets contain exactly the events refused.
Since fl 2ttm is monotonic with respect to the refinement order, and ttm2fl is closed under the healthiness conditions of FL, we have a Galois connection between F L-tock and maximal -tock .
Next we focus on the subset closure of refusals to complete the Galois connection.

Subset-closure of refusals leading to full -tock
Completing the subset closure of refusal sets in -tock is achieved by the function mkTT 1.

Name
Definition Definition 11.
With mkTT 1(P ), we have the union of P with a set of traces ρ related by , the prefix relation on -tock traces defined in [13], to σ drawn from P . The other adjoint is unTT 1 and is uniquely defined in terms of mkTT 1. It is the distributed union over processes Q (where Q satisfies TTM and TT1w) and whose mapping via mkTT 1(Q ) is a subset of P . In other words, unTT 1 undoes the subset closure of refusals resulting from mkTT 1, yielding a process whose refusals are maximal, as defined by TTM, and whose traces are prefix-closed under TT1w.
Thus, we have a Galois connection between maximal -tock , labelled as TTM in Fig. 1, and full -tock . Next, we compose both connections to obtain a Galois connection between F L and -tock , depicted in Fig. 1 by the dashed arrows.
The function fl 2tt (P ) maps F L processes totock . In the opposite direction we have tt 2fl .

Prioritise for -tock
Similar to the definition of Pri ≤ , which is pointwise over FL traces using a relation pri, we have a similar characterisation for Pri TT≤ as defined next.
The traces of Pri TT≤ is the set of TT traces ρ related to a trace σ, from P , by a parametric relation pri TT[≤, ,P ] , specified in Definition 14, that takes three parameters: the partial order ≤ over events in Σ tock ; the empty sequence , and P .
For a trace σ, prioritisation needs to take into account, at each point in σ where an event is present, the refusal sets that can be observed just before it, as well as whether other events can be performed. So the second parameter of pri TT is the trace considered so far in the process specified as the third parameter. In the initial case, when considering σ, the trace considered so far is the empty sequence. Before explaining the formal definition, we illustrate the calculation of Pri TT≤ (T ) (from Example 2), where a < b, and tock have maximal priority, and ¬ b < tock . The trace is related to itself as it is a valid trace of every process (see 1 in Definition 14). The trace ref { } is related to itself, and every trace whose only refusal is a subset of { } is also related to it because of subset closure (see 2 ). Similarly, ref {a, b, } is related to itself, and to traces whose only refusal is a subset of {a, b, }. The trace evt a is equally related to itself (see 4 ), as although a is not maximal, the presence of the trace ref {a, b, } indicates that b could be refused, in which case a is possible on its own, and thus prioritisation has no effect. Similarly evt b is related to itself as b is prioritised over a, can only happen unstably, and tock is assumed not to be prioritised over b. The traces evt b, evt and evt a, evt are similarly related to themselves, given that has maximal priority. Finally, because tock is maximal, priref (p, σ, Q , S ), which is specified below. It defines a refusal set containing all the events of S as well as those disallowed by prioritisation, according to the order p, given that the trace preceding ref S in Q is σ. For example, the result of applying priref (p, , T , ∅) is {a}, assuming a < p b, as event b can be performed in T , but is of higher priority than a and b is not in the empty set. Initially, in the context of Pri TT , σ is the empty trace.
The function priref is defined as the union of S and two sets: the set of events e of strictly lower priority than tock , according to the order p, if the trace σ concatenated with the trace where the refusal S followed by tock is in Q ; and the set of events e such that there is some event b of strictly higher priority than e, which is not tock nor and is not in S , but that can be performed in Q after trace σ as σ evt b . Thus, to ascertain whether an event e can be refused because of prioritisation, it is necessary to determine whether an event of higher priority, other than , that is not refused in S can be performed after trace σ. The reason is excluded from the comparison is because it is an unstable event, and so it is never in a genuine offer to the environment. To illustrate this point, we consider the process in the following example.
In addition to e being offered stably, we have the possibility that process K terminates. Assuming f < p , applying priref (p, , K , ∅) would result in the set {f } if f could be compared with in priref . Because is never a genuine option for the environment, however, it is incorrect to compare it with events of lower priority. Moreover, as illustrated in this example, the set of traces induced by such a definition of priref (p, , K , ∅) would be unhealthy, as no refusal set f , could be obtained by applying priref to an initial refusal of K (see Section 2.1). The final case 4 in Definition 14 specifies that a trace evt e ρ 0 is related to evt e ρ 1 by pri TT[p,σ,Q] , whenever ρ 0 is related to ρ 1 by pri TT[p,σ evt e ,Q] and, if e is not maximal in the priority order p, then it is not and there is some refusal Z observable after σ in Q , such that application of priref (p, σ, Q , Z ) does not lead to e being refused. For example, trace evt a from process T is related to itself when considering a < p b, as although a is not maximal there is a trace ref {b} in T , by subset closure, where the application of priref (p, , T , {b}) yields {b}. In words, if e is maximal then the trace is related, and in particular, if appears in a trace it must be maximal. Otherwise, if e is neither maximal nor , then it must be the case that application of priref to Q indicates that e can be chosen; not refused.
Thus, events that are not maximal are not discarded by prioritisation if, at the same time, events of higher priority can be refused. We consider, an alternative presentation of T , by distributing the internal choice over the external choice.
This clearly shows the possibility for a to be stably offered for a time unit, if the first internal choice is decided in favour of a, while the second internal choice is made in favour of a delay. Thus, before the first time unit has elapsed, there is the possibility that no b is on offer, and thus prioritisation is ineffective at that point. Another presentation of T is exactly S , which, as discussed in Section 1, has the same semantics as T in -tock , but not in F L. This is inherently related to algebraic properties enjoyed by -tock processes, which are consistent with the F model within a time unit.
Our main result is that the Pri TT≤ operator of -tock is exactly that induced by the Galois connection with F L as established next. Theorem 1. Provided P is TT-healthy, Pri TT≤ (P ) = fl 2tt • Pri ≤ • tt 2fl (P ) For a -tock process P , Pri TT≤ (P ) can be obtained by mapping P into F L, via tt 2fl , then ap-plying the prioritisation operator of F L, and finally mapping the result into -tock via fl 2tt .

Conclusions
To endow -tock with a prioritise operator consistent with Pri ≤ of F L, we have established a Galois connection between F L and -tock , and calculated an induced definition. With that, we have a definition that is by construction monotonic and healthy. It is strictly not pointwise because prioritisation of events in a trace needs to take into account other refusal sets reachable at the same point.
The formalisation of F L, although presented here in terms of a set Σ tock , is fully parametric in our mechanisation in Isabelle/HOL, and thus depends only on Σ. The mechanisation of the F L model is layered. We have a faithful mechanisation of F L, built stepwise to consider termination, and discrete time, by including and tock incrementally. The algebraic laws from Section 3 for Pri ≤ are novel, and more importantly are applicable to RT as a consequence of Roscoe [1]'s results on the hierarchy of CSP semantic models. Congruence of the operational semantics of Pri ≤ over that model, however, requires further restrictions to the order [8], including that is maximal, enforced, for example, when model-checking with FDR.
Effectively, Pri TT≤ can look into nondeterministic choices unlike other CSP operators. This presents challanges for its implementation in FDR. It is known that Pri ≤ cannot be specified via combinators, as used in FDR, and instead an extended theory of combinators is required [8]. Thus, Pri ≤ is actually implemented in FDR as a function that operates over an LTS, rather than via combinator semantics. A practical strategy for implementing Pri TT≤ in FDR, for example, may require some form of bisimulation, or search, to examine refusals reachable by sequences of τ transitions from each state being prioritised in the LTS.
A denotational definition for Pri TT enables algebraic properties to be explored. It is in our plans to propose laws in support of a refinement approach to verification of robotic simulations [6], where prioritisation is used as part of capturing the assumptions routinely made by roboticists in simulations.
Finally, the semantic model -tock is somewhere between F and RT in terms of expressivity, as indicated by the way refusals are recorded. Our results are likely to be enlightening in the calculation of a counterpart of Pri ≤ for F as well.