{'fraction_non_alphanumeric': 0.03956300072833212, 'fraction_numerical': 0.00471959213401311, 'mean_word_length': 4.130941704035874, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Models for CSP with availability information

We consider models of CSP based on recording what events are available as possible alternatives to the events that are actually performed. We present many different varieties of such models. For each, we give a compositional semantics, congruent to the operational semantics, and prove full abstraction and no-junk results. We compare the expressiveness of the different models.


Introduction
In this paper we consider a family of semantic models of CSP [13] that record what events a process makes available as possible alternatives to the events that are actually performed. For example, the models will distinguish a → STOP ✷ b → STOP and a → STOP ⊓ b → STOP: the former offers its environment the choice between a and b, so can make a available before performing b; however the latter decides internally whether to offer a or b, so cannot make a available before performing b.
A common way of motivating process algebras (dating back to [8]) is to view a process as a black box with which the observer interacts. The models in this paper correspond to that black box having a light for each event that turns on when the event is available (as in [5,4]); the observer can record which lights turn on in addition to which events are performed.
I initially became interested in such models by considering message-passing concurrent programming languages that allow code to test whether a channel is ready for communication without actually performing the communication. In [7], I considered the effect of extending CSP with a construct "if ready a then P else Q" that tests whether the event a is ready for communication (i.e., whether this process's environment is ready to perform a), acting like P or Q appropriately. The model in [7] recorded what events were made available by a process, in addition to the events actually performed. We investigate such models more fully in this paper. We show that -even without the above construct-there are many different variations, with different expressive power.
By convention, a denotational semantic model of CSP is always compositional, i.e., the semantics of a composite process is given in terms of the semantics of its components. Further, there are several other desirable properties of semantic models: Congruence to the operational semantics The denotational semantics can either be extracted from the operational semantics, or calculated compositionally, both approaches giving the same result; Full abstraction The notion of semantic equivalence corresponds to some natural equivalence, typically defined in terms of testing; No-junk The denotational semantic domain corresponds precisely to the semantics of processes: for each element of the semantic domain, we can construct a corresponding process.
Each of the semantic models in this paper satisfies these properties. In Section 2 we describe our basic model. We formalise the notion of availability of events in terms of the standard operational semantics. We then formalise the denotational semantic domain, and explain how to extract denotational information from the semantics. We then give a congruent compositional denotational semantics, and prove full abstraction and no-junk results.
In Section 3 we describe variations on the basic model, in two dimensions: one dimension restricts the number of observations of availability between successive standard events; the other dimension allows the simultaneous availability of multiple events to be recorded. For each resulting model, we describe compositional semantics, and full abstraction and no-junk results (we omit some of the details because of lack of space, and to avoid repetition). We then study the relative expressive power of the models.
Finally, in Section 4, we discuss various aspects of our models, some additional potential models, and some related work.
Overview of CSP We give here a brief overview of the syntax and semantics of CSP; for simplicity and brevity, we consider a fragment of the language in this paper. We also give a brief overview of the Traces and Stable Failures Models of CSP. For more details, see [6,13].
CSP is a process algebra for describing programs or processes that interact with their environment by communication. Processes communicate via atomic events, from some set Σ. Events often involve passing values over channels; for example, the event c.3 represents the value 3 being passed on channel c.
The simplest process is STOP, which represents a deadlocked process that cannot communicate with its environment. The process div represents a divergent process that can only perform internal events.
The process a → P offers its environment the event a; if the event is performed, it then acts like P. The process c?x → P is initially willing to input a value x on channel c, i.e. it is willing to perform any event of the form c.x; it then acts like P (which may use x). Similarly, the process ?a : A → P is initially willing to perform any event a from A; it then acts like P (which may use a).
The process P ✷ Q can act like either P or Q, the choice being made by the environment: the environment is offered the choice between the initial events of P and Q. By contrast, P ⊓ Q may act like either P or Q, with the choice being made internally, not under the control of the environment; ⊓ x:X P x nondeterministically acts like any P x for x in X. The process P ⊲ Q represents a sliding choice or timeout: it initially acts like P, but if no event is performed then it can internally change state to act like Q.
The process P A B Q runs P and Q in parallel; P is restricted to performing events from A; Q is restricted to performing events from B; the two processes synchronise on events from A ∩ B. The process P ||| Q interleaves P and Q, i.e. runs them in parallel with no synchronisation.
The process P \ A acts like P, except the events from A are hidden, i.e. turned into internal, invisible events, denoted τ, which do not need to synchronise with the environment. The process P[[R]] represents P where events are renamed according to the relation R, i.e., P[[R]] can perform an event b whenever P can perform an event a such that a R b.
Recursive processes may be defined equationally, or using the notation µ X • P, which represents a process that acts like P, where each occurrence of X represents a recursive instantiation of µ X • P.
Prefixing (→) binds tighter than each of the binary choice operators, which in turn bind tighter than the parallel operators.
CSP can be given both an operational and denotational semantics. The denotational semantics can either be extracted from the operational semantics, or defined directly over the syntax of the language; see [13]. It is more common to use the denotational semantics when specifying or describing the behaviours of processes, although most tools act on the operational semantics. A trace of a process is a sequence of (visible) events that a process can perform. If tr is a trace, then tr ↾ A represents the restriction of tr to the events in A, whereas tr \ A represents tr with the events from A removed; concatenation is written " ⌢ "; A * represents the set of traces with events from A. A stable failure of a process P is a pair (tr, X), which represents that P can perform the trace tr to reach a stable state (i.e. where no internal events are possible) where X can be refused, i.e., where none of the events of X is available.

Availability information
In this section we consider a model that record that particular events are available during an execution. We begin by extending the operational semantics so as to formally define this notion of availability. We then define our semantic domain -traces containing both standard events and availability informationwith suitable healthiness conditions. We then present compositional trace semantics, and show that it is congruent to the operational semantics. Finally, we prove full abstraction and no-junk results.
We write offer a to record that the event a is offered by a process, i.e. a is available. We augment the operational semantics with actions to record such offers (we term these actions, to distinguish them from standard events). Formally, we define a new transition relation −−⊲ from the standard transition relation −→ (see [13,Chapter 7]) by: Note that the transitions corresponding to offer actions do not change the state of the process.
We now consider an appropriate form for the denotational semantics. One might wonder whether it is enough to record availability information only at the end of a trace (by analogy to the stable failures model). However, a bit of thought shows that such a model would be equivalent to the standard Traces Model: a process can perform the trace tr ⌢ offer a precisely if it can perform the standard trace tr ⌢ a .
We therefore record availability information throughout the trace. For convenience, for A ⊆ Σ, we define We define an availability trace to be a sequence tr in (Σ † ) * . We can extract the traces (of Σ † actions) from the operational semantics (following the approach in [13, Chapter 7]):

Example 2
The process a → STOP ✷ b → STOP has the availability trace offer a, b . However, the process a → STOP ⊓ b → STOP does not have this trace. This model therefore distinguishes these two processes, unlike the standard Traces Model.
Note in particular that we may record the availability of events in unstable states (where τ events are available), by contrast with models like the Stable Failures Model that record (un)availability information only in stable states. The following example contrasts the two models.

Example 3
The processes a → STOP and a → STOP ⊓ STOP are distinguished in the Stable Failures Model, since the latter has stable failure ( , {a}); however they have the same availability traces.
The processes (a → STOP ⊲ b → STOP) ⊓ (b → STOP ⊲ a → STOP) and a → STOP ⊓ b → STOP are distinguished in the Availability Traces Model, since only the former has the availability trace offer a, b ; however, they have the same stable failures.
The availability-traces of process P are then {tr | P tr =⇒}. The following definition captures the properties of this model.

Definition 4
The Availability Traces Model A contains those sets T ⊆ (Σ † ) * that satisfy the following conditions: 1. T is non-empty and prefix-closed. 2. offer actions can always be remove from or duplicated within a trace: 3. If a process can offer an event it can perform it: tr ⌢ offer a ∈ T ⇒ tr ⌢ a ∈ T. 4. If a process can perform an event it can first offer it: tr ⌢ a ⌢ tr ′ ∈ T ⇒ tr ⌢ offer a, a ⌢ tr ′ ∈ T.
Lemma 5 For all processes P, {tr | P tr =⇒} is an element of the Availability Traces Model, i.e., satisfies the four healthiness conditions.

Compositional traces semantics
We now give compositional rules for the traces of a process. We write traces A [[P]] for the traces of P 1 . Below we will show that these are congruent to the operational definition above.
STOP and div are equivalent in this model: they can neither perform nor offer standard events. The process a → P can initially signal that it is offering a; it can then perform a, and continue like P.
The process P ⊲ Q can either perform a trace of P, or can perform a trace of P with no standard events, and then (after the timeout) perform a trace of Q. The process P ⊓ Q can perform traces of either of its components; the semantics of replicated nondeterministic choice is the obvious generalisation.
Before the first visible event, the process P ✷ Q can perform an offer a action if either P or Q can do so. Let tr ||| tr ′ be the set of ways of interleaving tr and tr ′ (this operator is defined in [13, page 67]). The three sets in the definition below correspond to the cases where (a) neither process performs any visible events, (b) P performs at least one visible event (after which, Q is turned off), and (c) the symmetric case where Q performs at least one visible event.
In a parallel composition of the form P A B Q, P is restricted to actions from A † , and Q is restricted to actions from B † . Further, P and Q must synchronise upon both standard events from A ∩ B and offers of events from A ∩ B. We write tr P (A∩B) † tr Q for the set of ways of synchronising tr P and tr Q on actions 1 We include the subscript "A" in traces A [[P]] to distinguish this semantics from the standard traces semantics, traces from (A ∩ B) † (this operator is defined analogously to in [13, page 70]). The semantics of interleaving is similar.
The semantic equation for hiding of A captures that offer A actions are blocked, and A events are internalised. For relational renaming, we lift the renaming to apply to offer actions, i.e. (offer a) R (offer b) if and only if a R b; we then lift the relation to traces by pointwise application. The semantic equation is then a further lift of R.
We now consider the semantics of recursion. Our approach follows the standard method using complete partial orders; see, for example, [ Hence from Tarski's Theorem, each mapping F definable using the operators of the language has a least fixed point given by n 0 F n (div). This justifies the following definition.
The following theorem shows that the two ways of capturing the traces are congruent; it can be proved by a straightforward structural induction.

Full abstraction
We can show that this model is fully abstract with respect to a form of testing in the style of [10]. We consider tests that may detect the availability of events. Following [7], we write ready a & T for a test that tests whether a is available, and if so acts like the test T. We also allow a test SUCCESS that represents a successful test, and a simple form of prefixing. Formally, tests are defined by the grammar: We consider testing systems comprising a test T and a process P, denoted T P. We define the semantics of testing systems by the rules below; ω indicates that the test has succeeded, and Ω represents a terminated testing system.

SUCCESS P
We say that P may pass the test T, denoted P may T, if T P can perform ω (after zero or more τs). We now show that if two processes are denotationally different, we can produce a test to distinguish them, i.e., such that one process passes the test, and the other fails it. Let tr ∈ (Σ † ) * . We can construct a test T tr that detects the trace tr.
The following lemma can be proved by a straightforward induction on the length of tr: Proof: Let tr be a trace. We can construct a process P tr as follows: Then the traces of P tr are just tr and those traces implied from tr by the healthiness conditions of Definition 4. Formally, we can prove this by induction on tr. For example: • The traces of P a ⌢ tr are prefixes of traces of the form 2 (offer a) k⌢ a ⌢ tr ′ , where k 0 and tr ′ is a trace of P tr . Hence (by the inductive hypothesis) tr ′ is implied from tr by the healthiness conditions. Thus a ⌢ tr ′ is implied from a ⌢ tr. Finally (offer a) k⌢ a ⌢ tr ′ is implied from a ⌢ tr by k applications of healthiness condition 4. • The traces of P offer a ⌢ tr are of two forms: -Prefixes of traces of the form (offer a) k⌢ a , which is implied from offer a by healthiness conditions 2 and 3. -Traces of the form (offer a) k⌢ tr ′ where tr ′ is a trace of P tr . Hence (by the inductive hypothesis) tr ′ is implied from tr by the healthiness conditions. And so (offer a) k⌢ tr ′ is implied from offer a ⌢ tr by healthiness condition 2.
Then P = ⊓ tr∈T P tr is such that traces A [[P]] = T.
✷ 2 We write (offer a) k to denote a trace containing k copies of offer a.

Variations
In this section we consider variations on the model of the previous section, extending the models along essentially two different dimensions. We first consider models that place a limit on the number of offer actions between consecutive standard events. We then consider models that record the availability of sets of events. Finally we combine these two variations, to produce a hierarchy of different models with different expressive power (illustrated in Figure 1). For each variant, we sketch how to adapt the semantic model and full abstraction result from Section 2. We concentrate on discussing the relationship between the different models.

Bounded availability actions
Up to now, we have allowed arbitrarily many offer actions between consecutive standard events. It turns out that we can restrict this. For example, we could allow at most one offer action between consecutive standard events (or before the first event, or after the last event). This model is more abstract than the previous; for example, it identifies the processes whereas the previous model distinguished them by the trace offer a, offer b, c . More generally, we define the model that allows at most n offer actions between consecutive standard events. Let Obs n be the set of availability traces with this property. Then the model A n is the restriction of A to Obs n , i.e., writing traces A,n for the semantic function for A n , we have traces A,n [[P]] = traces A [[P]] ∩ Obs n . In particular, A 0 is equivalent to the standard traces model.
The following example shows that the models become strictly more refined as n increases; further, the full Availability Traces Model A is finer than each of the approximations A n .

Example 13 Consider the processes
Suppose n is non-zero and even (the case of odd n is similar). Processes P n and P n+1 can be distinguished in model A n and model A , since only P n+1 has the trace offer a, offer b, offer a, offer b, . . . , offer a, offer b, a with n offer actions. However, these processes are equal in model A n−1 .
Following Roscoe [15], we write M M ′ if model M ′ is finer (i.e. distinguishes more processes) than model M, and ≺ for the corresponding strict relation. The above example shows It is easy to see that these models are all compositional: in all the semantic equations, the presence of a trace from Obs n in a composite process is always implied by the presence of traces from Obs n in the subcomponents. It is important, here, that the number of consecutive offers is downwards-closed: the same result would not hold if we considered a model that includes exactly n offer actions between successive standard events, for in an interleaving P ||| Q, a sequence of n consecutive offers may be formed from k offers of P and n − k offers of Q.
In some cases, the semantic equations have to be adapted slightly to ensure the traces produced are indeed from Obs n , for example: The healthiness conditions need to be adapted slightly to reflect that only traces from Obs n are included. For example, condition 4 becomes 4 ′ . tr ⌢ a ⌢ tr ′ ∈ T ∧ tr ⌢ offer a, a ⌢ tr ′ ∈ Obs n ⇒ tr ⌢ offer a, a ⌢ tr ′ ∈ T. Finally, the full abstraction result still holds, but the tests need to be restricted to include at most n successive ready tests. And the no-junk result still holds.

Availability sets
The models we have considered so far have considered the availability of a single event at a time. If we consider the availability of a set of events, can we distinguish more processes? The answer turns out to be yes, but only with processes that can either diverge or that exhibit unbounded nondeterminism (a result which was surprising to me).
We will consider actions of the form offer A, where A is a set of events, representing that all the events in A are simultaneously available. We can adapt the derived operational semantics appropriately: For convenience, we define Traces will then be from (Σ P † ) * . We can extract traces of this form from the derived operational semantics as in Definition 1 (writing tr −→ P and tr =⇒ P for the corresponding relations). We call this model the Availability Sets Traces Model, and will sometimes refer to the previous model as the Singleton Availability Traces Model, in order to emphasise the difference. Definition 14 The Availability Sets Traces Model A P contains those sets T ⊆ (Σ P † ) * that satisfy the following conditions. 1. T is non-empty and prefix-closed. 2. offer actions can always be removed from or duplicated within a trace: 3. If a process can offer an event it can perform it:

If a process can perform an event it can first offer it:
tr ⌢ a ⌢ tr ′ ∈ T ⇒ tr ⌢ offer{a}, a ⌢ tr ′ ∈ T.

The offers of a process are subset-closed
6. Processes can always offer the empty set tr ⌢ tr ′ ∈ T ⇒ tr ⌢ offer{} ⌢ tr ′ ∈ T.

Lemma 15
For all processes P, {tr | P tr =⇒ P } is an element of the Availability Sets Traces Model.

Compositional semantics We give below semantic equations for the Availability Sets Traces Model.
Most of the clauses are straightforward adaptations of the corresponding clauses in the Singleton Availability Traces Model. For the parallel operators and external choice, we define an operator X P such that tr X P tr ′ gives all traces resulting from traces tr and tr ′ , synchronising on events and offers of events from X. The definition is omitted due to space restrictions. For relational renaming, we lift the renaming to apply to offer actions, by forming the subset-closure of the relational image: We again lift it to traces pointwise.
The semantic clauses are as follows.  Given tr ∈ (Σ P † ) * , we can construct a test T tr that detects the trace tr as follows.
The full abstraction proof then proceeds precisely as in Section 2.
We can prove a no-junk result as in Section 2. Given trace tr, we can construct a process P tr as follows: Then the traces of P tr are just tr and those traces implied from tr by the healthiness conditions.
Again, given an element T from the Availability Sets Traces Model, we can define P = ⊓ tr∈T P tr ; then

Distinguishing power
We now consider the extent to which the Availability Sets Model can distinguish processes that the Singleton Availability Model can't.

Example 17 The Availability Sets Traces Model distinguishes the processes
since just P has the trace offer{a, b} . However, these are equivalent in the Singleton Availability Traces Model; in particular, both can perform arbitrary sequences of offer a and offer b actions initially.
The process Q above can diverge (i.e., perform an infinite number of internal τ events corresponding to timeouts). We can obtain a similar effect without divergence, but using unbounded nondeterminism.

Example 18 Consider
Then P (from the previous example) and Q ′ are distinguished in the Availability Sets Traces Model but not the Singleton Availability Traces Model.
For finitely nondeterministic, non-divergent processes, it is enough to consider the availability of only finite sets, since such a process can offer an infinite set A iff and only if it can offer all its finite subsets. However, for infinitely nondeterministic processes, one can make more distinctions by considering infinite sets. Proposition 20 If P and Q are non-divergent, finitely nondeterministic processes, that are equivalent in the Singleton Availability Model, then they are equivalent in the Availability Sets Model.

Example 19 Let
Proof: Suppose, for a contradiction, that P and Q are non-divergent and finitely deterministic, are equivalent in the Singleton Availability Model, but are distinguished in the Availability Set Model. Then, without loss of generality, there are traces tr and tr ′ , and set of events A such that tr ⌢ offer A ⌢ tr ′ is a trace of P but not of Q. By the discussion in the previous paragraph, we may assume, without loss of generality, that A is finite, say A = {a 1 , . . . , a n }. Since Q is non-divergent and finitely-nondeterministic, there is some bound, k say, on the number of consecutive τ events that it can perform after tr. Since P can offer all of A after tr, it can also offer any individual events from A, sequentially, in an arbitrary order. In particular, it has the singleton availability trace tr ⌢ offer a 1 , . . . , offer a n k+1⌢ tr ′ .
Since P and Q are, by assumption, equivalent in the Singleton Availability model, Q also has this trace. Q must perform at most k τ events within the sub-trace offer a 1 , . . . , offer a n k+1 . This tells us that there is a sub-trace within that, of length n, containing no τ events. Within this sub-trace there are no state changes (i.e., there are only self-loops corresponding to the offer actions), and so all the a i are offered in the same state. Hence tr ⌢ offer A ⌢ tr ′ is an availability set trace of Q, giving a contradiction. ✷

Bounded sets
We can consider some variants on the Availability Sets Traces Model. First, let us consider the model A k that places a limit of size k upon availability sets. It is reasonable straightforward to produce compositional semantics for such models, and to adapt the full abstraction and no-junk results. It is perhaps surprising that such a semantics is compositional, since a similar result does not hold for stable failures [1] (although it is conjectured in [15] that this does hold for acceptances).
Clearly, A 1 ≡ A , and A 0 ≡ T (the standard traces model). Examples 17 and 18 show that A 2 is finer that A 1 . We can generalise those examples to show that each model A k is finer than A k−1 .

Example 21
Let A k be a set of size k. Consider P k = ?a : A k → STOP, Then P k and Q k are distinguished in A k since only P k has the trace offer A k . However they are equivalent in A k−1 : in particular, both can initially perform any trace of offers of size k − 1.
The limit of the models A k considers arbitrary finite availability sets; we term this A F . The model A F distinguishes the processes P k and Q k from Example 21, for all k, so is finer than each of the models with bounded availability sets. As shown by Example 19, A F is coarser than A P .
In fact, for an arbitrary infinite cardinal κ, we can consider the model A κ that places a limit of size κ upon availability sets. Example 19 showed that considering finite availability sets distinguishes fewer processes than allowing infinite availability sets, i.e. A F ≺ A κ . The following example shows that the models become finer as κ increases.

Example 22
Pick an infinite cardinal κ, and pick alphabet Σ such that card(Σ) κ. Then the processes P κ = ⊓ A⊆Σ,card(A)=κ ?a : A → STOP, Q κ = ⊓ A⊆Σ,card(A)<κ ?a : A → STOP are distinguished by the model A κ , since only P κ can offer sets of size κ. However, for λ < κ, they are not distinguished by the model A λ ; for example, if P κ has the trace offer A 1 , . . . , offer A n in A λ , then card(A i ) λ < κ, for each i; but also A = n i=1 A i has card(A) λ < κ, so Q κ can perform this trace by picking A in the nondeterministic choice.
(In fact, this example shows that these models -like the cardinals-form a proper class, rather than a set!) In most applications, the alphabet Σ is countable; these models then coincide for processes with such an alphabet. The model A P distinguishes the processes P κ and Q κ from Example 22, for all κ, so is finer than each of the models A κ . Summarising:

Combining the variations
We can combine the ideas from Sections 3.1 and 3.2 to produce a family of models A k n , where: • k is either a natural number k or infinite cardinal κ, indicating an upper bound on the size of availability sets, or the symbol F indicating arbitrary finite availability sets are allowed, or the symbol P indicating arbitrary availability sets are allowed; • n is either a natural number n, indicating an upper bound on the number of availability sets between successive standard events, or the symbol F indicating any finite number is allowed.
If k = 0 or n = 0 then A k n is just the standard traces model. Further, A n ≡ A 1 n and A k ≡ A k F . We can show that this family is ordered as the natural extension of the earlier (one-parameter) families; the relationship between the models is illustrated in Figure 1. In particular, these models are distinct for n, k = 0. We can re-use several of the earlier examples to this end. Example 13 shows that for Let A 1 , . . . , A n , {a} be a partition of A, where each A i is of size k. Then offer A 1 , . . . , offer A n , a is a trace of P but not of Q, so these processes are distinguished by A k n . However, the two processes are equivalent in A k−1 n . Hence A k−1 n ≺ A k n . Further, A F n distinguishes these processes, for all (finite) n and k, so A k n ≺ A F n . Example 19 shows that A F n ≺ A κ n for each infinite cardinal κ and for each n. Further, Example 22 shows that if λ < κ are two infinite cardinals, then A λ n ≺ A κ n ≺ A P n .

Discussion
Simulation and model checking The models described in this paper are not supported by the model checker FDR [12,2]. However, it is possible to simulate the semantics, using a fresh event offer.A to This simulation process, then, has the same traces as the original process in the Availability Sets Model, but with each offer A action replaced by offer.A. The semantics in each of the other models can be obtained by restricting the size or number of offer events.
In [16], Roscoe shows that any operational semantics that is CSP-like, in a certain sense, can be simulated using standard CSP operators. One can define the operational semantics of the corrent paper in a way that makes them CSP-like, in this sense. Roscoe's simulation is supported by a tool by Gibson-Robinson [3], which has been used to automate the simulation of the Singleton Availability Model and Availability Sets Model. This opens up the possibility of using FDR to perform analyses in these models.

Related and further models
In [15], Roscoe investigates the hierarchy of finite linear observation models of CSP. All of these models record availability or unavailability of events only in stable states (if at all), unlike the models of this paper. Example 3 shows that the Singleton Availability Model is incomparable with the Stable Failures Model. In fact, this example shows that all of the models in this paper except the Traces Model are incomparable with all of the models in Roscoe's hierarchy except the Traces Model (so including the Ready Trace Model [11] and the Refusal Testing Model [9]); it is, perhaps, surprising that the hierarchies are so unrelated.
We believe that we could easily adapt our models to extend any of the finite linear observation models from [15], so as to obtain a hierarchy similar to that in Figure 1: in effect, the consideration of availability information is orthogonal to the finite linear observations hierarchy. Further, we have not considered divergences within this paper. We believe that it would be straightforward to extend this work with divergences, either building models that are divergence-strict (like the traditional Failures-Divergences Model [6,13]), or non-divergence-strict (like the model in [14]).
In [5,4], van Glabbeek considers a hierarchy of different semantic models in the linear timebranching time spectrum. Several of the models correspond to standard finite linear observation models, discussed above. One other model of interest is simulation.
Definition 24 [5] A simulation is a binary relation R on processes such that for all events a, if P R Q and P a −→ P ′ , then for some Q ′ , Q a −→ Q ′ and P ′ R Q ′ . Process P can be simulated by Q, denoted P ⊂ → Q if there is a simulation R with P R Q. P and Q are similar if P ⊂ → Q and Q ⊂ → P.
If P ⊂ → Q and P tr −→ P then one can show that Q tr −→ P , by induction on the length of tr. Hence if P and Q are similar, they are equivalent in the Availability Sets Traces Model, and hence all our other models. Simulation is strictly finer than our models, since it distinguishes A further possible class of models that we hope to investigate would record events that were available as alternatives to the events that were actually performed, and that were available from the same state as the events that were performed. For example, such a model would distinguish since P can perform a, c , with b available from the state where a was performed; but Q does not have such a behaviour. Note that these two processes are equivalent in all the other availability models in this paper.
Two further possible directions in which this work could be extended would be (A) to record what events are not available, or (B) to record the complete set of events that are available. We see considerable difficulties in producing such models. To see why, consider the process a → P. There are two different ways of viewing this process (which amount to different operational semantics for this process): • One view is that the event a becomes availability immediately. With this view: in model A, one cannot initially observe the unavailability of a; in model B, the initial complete availability set is {a}. However, under this view, the fixed point theory does not work as required, since div is not the bottom element of the subset ordering: in model A, div has a initially unavailable; in model B, div's initial complete availability set is {}; these are both behaviours not exhibited by a → P.
Further, under this view, nondeterminism is not idempotent, since, for example, a → P ⊓ a → P has a unavailable initially; one consequence is that the proof of the no-junk result cannot be easily adapted to this view.
• The other view is that a → P takes some time to make the event a available: initially a is unavailable, but an internal state change occurs to make a available. With this view: in model A, one can initially observe the unavailability of a; in model B, the initial complete availability set is {}.
However, under this view, it turns out that the state of a → P after the a has become available cannot be expressed in the syntax of the language; this means that the proof of the no-junk result cannot be easily adapted to this view. (Proving a full abstraction result is straightforward, though.) As noted in the introduction, in [7] we considered models for an extended version of CSP with a construct "if ready a then P else Q". This construct tests whether or not its environment offers a, so the model has much in common with model A above (and was built following the second view). As such, it did not have a no-junk result. Further, it did not have a full abstraction result, since it distinguished if ready a then P else P and P, but no reasonable test would distinguish these processes.