Acta Informatica 2015 DOI 10.1007/s00236-015-0221-6

CCS: It’s not Fair!

Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions

Rob van Glabbeek · Peter Höfner

It is our great pleasure to dedicate this paper to Walter Vogler on the occasion of his 60th birthday. We have combined two of Walter’s main interests: Petri nets and process algebra. In fact, we proved a result about Petri nets that had been proven before by Walter, but in a restricted form, as we discovered only after finishing our proof. We also transfer this result to the process algebra CCS. Beyond foundational research in the theory of concurrent systems, Walter achieved excellent results in related subjects such as temporal logic and efficiency. In addition to being a dedicated researcher, he is also meticulous in all of his endeavours, including his writing. As a consequence his scientific papers tend to contain no flaws, which is just one of the reasons that makes reading them so enjoyable. It’s fair to say: “CCS Walter!”—Congratulations and Continuous Success!

Abstract In the process algebra community it is sometimes suggested that, on some level of abstraction, any distributed system can be modelled in standard process-algebraic specification formalisms like CCS. This sentiment is strengthened by results testifying that CCS, like many similar formalisms, is Turing powerful and provides a mechanism for interaction. This paper counters that sentiment by presenting a simple fair scheduler—one that in suitable variations occurs in many distributed systems—of which no implementation can be expressed in CCS, unless CCS is enriched with a fairness assumption.

Since Dekker’s and Peterson’s mutual exclusion protocols implement fair schedulers, it follows that these protocols cannot be rendered correctly in CCS without imposing a fairness assumption. Peterson expressed this algorithm correctly in pseudocode without resorting to a fairness assumption, so it furthermore follows that CCS lacks the expressive power to accurately capture such pseudocode.

NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program.

R. J. van Glabbeek NICTA and UNSW. E-mail: rvg@cs.stanford.edu P. Höfner NICTA and UNSW. E-mail: Peter.Hoefner@nicta.com.au

Part I Motivation & Discussion

1 Background

In the process algebra community it is generally taken for granted that, on some level of abstraction, any distributed system can be modelled in standard processalgebraic specification formalisms like CCS [45].

Of course, if a distributed system has features related to time, probability, broadcast communication or anything else that is not innately modelled in CCS, yet essential to adequately describe the distributed system under consideration, appropriate extensions are needed, such as timed process algebras (e.g., [56,35,3, 43,16]), probabilistic process algebras (e.g., [34]) or calculi for broadcast communication (e.g., [54]). This paper is not concerned with such features.

The relative expressiveness of process algebras is a well-studied subject [58,50, 32], and in this area CCS-like process algebras are considered far from universally expressive. In [27] for instance it is pointed out that the parallel composition operator of CSP [11,36] cannot be expressed in CCS. The priority operator of [5] is a good example of an operator that cannot be expressed in any of the standard process algebras such as CCS, CSP, ACP [7] or LOTOS [9]. These results focus, however, on the possibility of expressing operators—composing a process out of one or more components—as CCS-contexts; they cast no doubt on the possibility of expressing actual processes in CCS.

Beside operators, it has also be shown that there exist examples of process specifications that cannot be faithfully rendered in CCS-like formalisms (cf. [26]). We will illustrate this in Section 3. In this paper we distinguish process specifications from actual processes that could in principle be implemented and executed. Again, the evidence presented casts no doubt on the possibility of expressing actual processes in CCS.

Incorporating these clarifications of our meaning, we expect that many concurrency experts feel that, up to an adequate level of abstraction, any reactive system can be rendered in CCS. This sentiment is strengthened by results testifying that CCS, like many similar formalisms, is Turing powerful [45]. As a manifestation of this, any computable partial function f : Σ^{∗} → Σ^{∗} over some finite alphabet Σ can be modelled by a CCS context P [ ], such that, for any input word w = a_{1}a_{2} … a_{n} ∈ Σ^{∗}, encoded as a CCS expression W := a_{1}.a_{2}. . . . .a_{n}.z.0 featuring an end-of-input marker z, the process P [W] computes forever without performing any visible actions if f(w) is undefined, and otherwise performs the sequence of visible actions f(w), followed by an end-of-output marker z.

It is sometimes argued that Turing machines are an inadequate formalism to capture interactive behaviour as displayed by today’s computers [62,41]. The main argument is that Turing machines are function-based and calculate, for a given finite input, one output; this paradigm does not do justice to the ongoing interactions between a reactive system and its environment. To add ongoing interactivity to Turing machines, interaction machines are proposed in [62], and formalised in [31] as persistent Turing machines. Likewise, [6] proposes reactive Turing machines. Since standard process algebras like CCS are already equipped with interaction primitives, they can surely also model computations on persistent or reactive Turing machines. All this strengthens the feeling that standard process algebras, such as CCS, are powerful enough to specify any distributed system.

2 Fairness Assumptions

Before presenting evidence that CCS and related formalisms cannot correctly specify every distributed system, some explanation is in order on our understanding of ‘correctly’. This is best illustrated by an example.

Consider the CCS agent identifier E with defining equation E =^{def} a.E + b.0. The question is whether this is a good rendering of a process that is guaranteed to eventually perform the action b. The answer depends on whether we incorporate a fairness assumption in the semantics of CCS. A strong fairness assumption requires that if a task (here b) is enabled infinitely often, but allowing interruptions during which it is not enabled, it will eventually be scheduled [25,42]. Making such an assumption allows us to infer that indeed the process E will eventually do a b.^{1}

It depends on the context of the application of CCS whether it is appropriate to make such fairness assumptions. For the verification of the alternating bit protocol, for instance, fairness assumptions are indispensable [8]. But in some situations they allow us to reach conclusions that are patently false. In the example above for instance, let a be an unsuccessful attempt to dial a number or an unreliable mobile phone, and b a successful one. The system E simply retries after each unsuccessful attempt. Whether it ever succeeds in performing b depends very much on how unreliable the phone is. If there is a fixed positive probability on success, the strong fairness assumption appears warranted. Yet, if the phone is completely dead, it is not, and the conclusion that we eventually succeed in dialling is false. In fact, when assuming strong fairness we loose the expressiveness to describe by a finite recursive specification like E a system such as the above interaction with the unreliable telephone that does allow an infinite run with only as.

As evidence that not every distributed system can be rendered correctly in CCS, we will describe a fair scheduler as a counterexample. Yet, our fair scheduler can be rendered in CCS very easily, if only we are willing to postulate a fairness property to support its correctness. However, considering the above example and the fact that we may reach wrong conclusions, this is a price we are not willing to pay.

Our fair scheduler is not merely an ‘artificial’ CCS specification; it is implemented in many working distributed systems, and (unlike the alternating bit protocol) its correctness should not be contingent on any fairness assumption whatsoever. This is another reason why we do not want to invoke fairness to achieve a correct rendering in CCS.

Yet, we do find it reasonable to equip CCS with two assumptions that are weaker than strong fairness, namely progress and justness. A progress assumption is what is needed to infer that the CCS process b.0 will eventually do a b, and a justness assumption allows us to infer that the parallel composition A|b.0 with A =^{def} a.A will eventually do a b. If our task is to specify in CCS a process B that will eventually do a b, then, when assuming strong fairness, the processes E, A|b.0 and b.0 are acceptable implementations of B. If we assume justness, but not fairness, this selection shrinks to A|b.0 and b.0, and if we only assume progress, we have to give up on A|b.0 as well. When not even assuming progress, B cannot be rendered in CCS at all. Assuming progress and justness only, A|b.0 models a process that will eventually do a b, whereas E can be used to characterise the above mentioned interaction with the unreliable telephone, which allows an infinite sequence of as only.

1 In [4] a form of reasoning using a particularly strong global fairness assumption was integrated in the axiomatic framework of ACP, and shown to be compatible with the notion of weak bisimulation commonly taken as the semantic basis for CCS.

So, when we claim that a fair scheduler cannot be implemented in CCS, we mean that it cannot be implemented in CCS+justness, CCS+progress or CCS without any progress assumption. It can be implemented in CCS+strong fairness, however.

To pinpoint the borderline, consider a weak fairness or justice assumption [25, 42]. This assumption requires that if a task, from some point onwards, is perpetually enabled, it will eventually be scheduled. What this means depends on our interpretation of ‘perpetual’. If ‘perpetual’ simply means ‘in each state’, then a weak fairness assumption is all that is needed to assure that the process E will eventually do a b.^{2} A weak fairness assumption in this sense is enough to correctly render a fair scheduler in CCS. If, on the other hand, the execution of the a-transition of E counts as a (short) interruption of the enabledness of b, then justice can be shown to coincide with justness [29]; as we will show, this is not enough to render a fair scheduler in CCS.

3 Specifications versus Actual Processes

Consider the system specification G expressed in CCS as A|B with A =^{def} a.A and B =^{def} b.B, but with the added requirement that all infinite executions should have infinitely many occurrences of a as well as b. Here a and b could be seen as two tasks that need to be scheduled again and again. The left-hand component A of the parallel composition tries to perform task a infinitely often, and the righthand component tries to perform task b infinitely often. The process A|B by itself, as specified in CCS, is normally deemed equivalent to the process C, defined by C =^{def} a.C + b.C, and—in the absence of a justness or fairness assumption—offers no guarantee that a single b will ever happen. It could be that, due to unfortunate scheduling, at each time a choice is made, task a is chosen. The challenge in specifying the fair version G of this process in CCS is how to ensure that sooner or later a b will happen, without simply invoking a fairness or justness assumption, and without setting any fixed limit on the number of as that can happen beforehand.

Accordingly, solutions have appeared in the literature that change the operational semantics of CCS in such a way that A|B will surely do a b eventually. In [52] for instance, parallel operators ∥_{m} are used that, each time a b occurs, nondeterministically select a number m and guarantee that from that point onwards at most m occurrences of a happen before the next b. Another solution along these lines is proposed in [17], whereas [13] solves the problem by harvesting the power added by the treatment of time in the timed process algebra PAFAS [16].

In relation to the above challenge it would be trivial to specify some process that makes sure that tasks a and b are each scheduled infinitely often; a particularly simple way to achieve this is through the CCS specification D, given by D =^{def} a.b.D; that is, to alternate each of the two tasks. This is a round-robin solution. It could be seen as a particular implementation of G. The reason that such a solution is not chosen is that it fails to capture the full generality of the original specification, in which arbitrary many as may come between any two bs.

2 The process E′ with E′ =^{def} a.a.E′ + b.0 on the other hand really needs strong fairness.

Any real-life implementation of G on a physical computer is unlikely to capture the full generality of its specification, but rather goes a few steps towards the round-robin solution. For this reason, one could argue that G does not constitute an example of a distributed system that cannot be rendered in CCS, but rather one of a specification that cannot be rendered in CCS. As such, it falls out of the scope of this paper.

4 Our Contributions

This paper counters the sentiment that CCS-like process algebras are powerful enough to represent arbitrary distributed systems by presenting a particularly simple system of which no implementation can be expressed in CCS. The reason we use CCS is that it is among the most well-known standard process algebras, while having a fairly easy to explain syntax and semantics. However, we believe the same result, with essentially the same proof, could be obtained for COSY [40], CSP [11,36], ACP [7], LOTOS [9], μCRL [33], the π-calculus [46], etc.

Our system is a fair scheduler. It can receive two kinds of requests r_{1} and r_{2} from its environment on separate channels, and is guaranteed to perform a task— granting the request—in response. Our fairness requirement rules out a scheduler that may fail to ever grant a request of type r_{1} because it is consistently busy granting requests r_{2}.

Such schedulers occur (in suitable variations) in many distributed systems. Examples are First in First out^{3}, Round Robin, and Fair Queueing scheduling algorithms^{4} as used in network routers [47,48] and operating systems [38], or the Completely Fair Scheduler,^{5} which is the default scheduler of the Linux kernel since version 2.6.23.

If F stands for the most general specification of our scheduler, our claim entails that F cannot be rendered in CCS. However, accurately expressing F in CCS can be seen as a luxury problem. Here we would accept any implementation of F, under the broadest definition of implementation that makes sense for this problem—a round-robin solution for instance would be totally acceptable—and what we show is that even that is impossible.

As is common, we employ a version of CCS that allows the use of arbitrary sets of recursive equations to define processes. As is trivial to show, any labelled transition system, computable or not, can be modelled up to strong bisimulation equivalence as an expression in this language. Hence, our result implies that no implementation of the fair scheduler F can be modelled as a labelled transition system modulo strong bisimulation equivalence.

In this paper we will use a semantics of CCS incorporating a justness assumption. It distinguishes the strongly bisimilar systems A|B and C mentioned above, on grounds that A|B can be understood to always perform infinitely many as as well as bs, whereas C might perform an infinite sequence of bs while discarding the a-option all the time. This semantics increases the power of CCS in specifying fair schedulers, and thereby strengthens our result that no implementation of the fair scheduler F can be expressed. It thereby becomes stronger than the result that no implementation of F can be rendered as a labelled transition system modulo strong bisimulation equivalence.

3 Also known as First Come First Served (FCFS)

4 http://en.wikipedia.org/wiki/Scheduling_(computing)

5 http://en.wikipedia.org/wiki/Completely_Fair_Scheduler

To prove our result, we show that our fair scheduler cannot be expressed in terms of safe Petri nets. The result for CCS then follows by reduction: an adequate Petri net semantics of CCS shows that if the scheduler could be expressed in CCS, it could also be expressed as a Petri net.

The reason we resort to Petri nets to prove our main theorem is that Petri nets offer a structural characterisation of what it means for a transition to be continuously enabled in a run of the represented system from some state onwards. This is exploited in the proofs of Lemmas 1–4. It would be much harder to prove their counterparts directly in terms of the labelled transition system of CCS.

In different formulations, our impossibility result for Petri nets was established earlier by Vogler in [60] and by Kindler & Walter in [37], but in both cases side conditions were imposed that inhibit lifting these results to CCS. The proof of [60, Lemma 6.1] considers only finite Petri nets. The argument would extend to finitely branching nets, but not to all Petri nets that arise as the semantics of CCS expressions. The proof of [37] is restricted to Petri nets that interact with their environment through an interface of a particular shape, and it is not a priori clear that this does not cause a loss of generality. However, in Section 13 we study a similar interface in the context of CCS and show that it does not limit generality.

Although our fair scheduler cannot be expressed in a standard process algebra like CCS, we believe there are many extensions in the literature in which this can be done quite easily. In Section 11 for instance, we specify it in a formalism that could be called CCS+LTL. The use of a priority operator appears to be sufficient as well.

5 Peterson’s and Dekker’s Mutual Exclusion Protocols

Since Peterson’s and Dekker’s mutual exclusion protocols yield instances of our fair scheduler, it follows that these protocol cannot be rendered correctly in CCS without imposing a fairness assumption. Nevertheless, implementations of these algorithms in CCS or similar formalisms occur frequently in the literature, and almost never a fairness assumption is invoked. Moreover, for each of these two protocols, its various renderings differ only in insignificant details. Our result implies that these common renderings cannot be correct. Usually, only safety properties of these protocols are shown: never are two processes simultaneously in the critical section. The problem is with the liveness property: any process that is ready to enter the critical section will eventually do so. We found four papers that claim to establish essentially this property, of which only one invokes a fairness assumption. We will indicate in which way the other three do not establish the right liveness property.

Peterson expressed his protocol correctly in pseudocode without resorting to a fairness assumption, although progress and justness are assumed implicitly. It follows that Peterson’s pseudocode does not admit an accurate translation into CCS. We pinpoint the problem in this paper.

6 Overview

In Part I we discussed (informally) the goal we set out to achieve, and why we believe it is important and surprising at the same time.

Part II formalises our results, while providing explanations of the choices made in this formalisation. In particular, Section 7 presents an informal description of our fair scheduler F. Section 8 presents CCS. Section 9 makes a progress assumption on the semantics of CCS and argues that it is useful to set apart a set of non-blocking actions. Section 10 formalises the justness assumption discussed above and presents a semantics of CCS in which a process P is modelled as a state in a labelled transition system together with a set of (possibly infinite) paths in that transition system starting from P that model its valid runs. Section 11 gives a formal specification of F. Since we aim to show that no implementation of F can be specified in CCS, the specification of F cannot be given in CCS either. Instead we specify F as a CCS expression augmented with a fairness specification. This follows the traditional approach of TLA [39] and other formalisms [24], “in which first the legal computations are specified, and then a fairness notion is used to exclude some computations which otherwise would be legal” [2]. In Section 12 we state our main result, saying that no fair scheduler—that is: no implementation of F—can be expressed in CCS. Section 13 reformulates this result, so that it is independent of the concept of an action being perpetually enabled in a run of the represented system. In Section 14 we conclude that mutual exclusion protocols, like the algorithms from Dekker or Peterson, cannot be rendered correctly in CCS without imposing a fairness condition. We also investigate the apparent contradiction with the fact that several research papers claim to achieve exactly this. We end this section with a result by Corradini, Di Berardini & Vogler, showing where a fairness assumption is needed for a rendering of Dekker’s protocol in a process algebra to be correct.

Part III deals with proving our main result. In Section 15 we formulate our claim that no fair scheduler can be modelled as a safe Petri net. This claim is proven in Section 16. In Section 17 an operational Petri net semantics of CCS is presented, following the work of Degano, De Nicola & Montanari. From this, the proof of our main result is obtained in Section 18. A few concluding remarks are made in Section 19.

Part II Formalisation

7 A Fair Scheduler

Our fair scheduler is a reactive system with two input channels: one on which it can receive requests r_{1} from its environment and one on which it can receive requests r_{2}. We allow the scheduler to be too busy shortly after receiving a request r_{i} to accept another request r_{i} on the same channel. However, the system will always return to a state where it remains ready to accept the next request r_{i} until r_{i} arrives. In case no request arrives it remains ready forever. The environment is under no obligation to issue requests, or to ever stop issuing requests. Hence for any numbers n_{1} and n_{2} ∈ IN ∪{∞} there is at least one run of the system in which exactly that many requests of type r_{1} and r_{2} are received.

\begin{matrix}α.P ⟶^{α} P & & \frac{P_{j} ⟶^{α} P′}{∑_{i∈I} P_{i} ⟶^{α} P′} (j ∈ I) \\ \frac{P ⟶^{α} P′}{P |Q ⟶^{α} P′|Q} & \frac{P ⟶^{a} P′, Q ⟶^{ā} Q′}{P |Q ⟶^{τ} P′|Q′} & \frac{Q ⟶^{α} Q′}{P |Q ⟶^{α} P |Q′} \\ \frac{P ⟶^{α} P′}{P \a ⟶^{α} P′\a} (a ≠ α ≠ ā) & \frac{P ⟶^{α} P′}{P [f] ⟶^{f(α)} P′[f]} & \frac{P ⟶^{α} P′}{A ⟶^{α} P′} (A =^{def} P) \end{matrix}

Table 1 Structural operational semantics of CCS

Every request r_{i} asks for a task t_{i} to be executed. The crucial property of the fair scheduler is that it will eventually grant any such request. Thus, we require that in any run of the system each occurrence of r_{i} will be followed by an occurrence of t_{i}. In Linear-time Temporal Logic (LTL) [53] this can be stated as

G(r_{i} ⇒ F(t_{i})) , i ∈ {1, 2} .

Note that it may happen that the environment issues request r_{1} three times in a row before the scheduler got a change to schedule task t_{1}. In that case the scheduler may fulfil its obligation by scheduling task t_{1} just once. Hence it need not keep a counter of outstanding requests.^{6}

We are not interested in implementations of the scheduler that just schedule both tasks infinitely often without even listening to the requests. Hence we require that in any partial run of the scheduler there may not be more occurrences of t_{i} than of r_{i}, for i = 1, 2.

The last requirement is that between each two occurrences of t_{i} and t_{j} for i, j ∈ {1, 2} an intermittent activity e is scheduled.^{7} This requirement will rule out fully concurrent implementations, in which there are parallel components for task t_{1} and task t_{2} that do not interact in any way.

8 The Calculus of Communicating Systems

The Calculus of communicating systems (CCS) [45] is parametrised with sets A of names and K of agent identifiers; each A ∈ K comes with a defining equation A =^{def} P with P being a CCS expression as defined below. The set Ā of co-names is Ā:= {ā | a ∈ A }, and the set H of handshake actions is H := A ·^{∪} Ā, the disjoint union of the names and co-names. The function ¯. is extended to H by declaring ¯ ā := a. Finally, Act := H ·^{∪} {τ} is the set of actions. Below, a, b, c range over H , α, β over Act and A over K . A relabelling is a function f : H → H satisfying f(ā) = \overline{f(a)}; it extends to Act by f(τ) := τ. The set T_{CCS} of CCS expressions is the smallest set including:

6 This relaxed requirement only serves to increase the range of acceptable schedulers, thereby strengthening our impossibility result. It by no means rules out a scheduler that schedules task t_{1} exactly once for each request r_{1} received.

7 Our specification places no restrictions on the presence or absence of any additional occurrences of e. This again increases the range of acceptable implementations.

A agent identifier  α.P prefixing  ∑_{i∈I} P_{i} choice
P |Q parallel composition  P \a restriction  P [f]  relabelling

for P, P_{i}, Q ∈ T_{CCS}, index sets I, and relabellings f. We write P_{1}+P_{2} for ∑_{i∈I} P_{i} if I = {1, 2}, and 0 if I = ∅. The semantics of CCS is given by the labelled transition relation → ⊆ T_{CCS} × Act × T_{CCS}, where the transitions P ⟶^{α} Q are derived from the rules of Table 1. The pair ⟨T_{CCS}, →⟩ is called the labelled transition system (LTS) of CCS.

9 The Necessity of Output Actions

Before attempting to specify our scheduler in CCS, let us have a look at a simpler problem: the same scheduler, but with only one type of request r, and one type of task t to be scheduled. A candidate CCS specification of such a scheduler is the process F_{0}, defined by

F_{0} =^{def} r.e.t.F_{0} .

As stated in Section 7, the scheduler is called fair if every request r is eventually followed by the requested task t; so we want to ensure the property G(r ⇒ F(t)).^{8} However, we cannot guarantee that this property actually holds for process F_{0}. The reason is that the process might remain in the state s reached by taking transition e without ever performing the action t. In any formalism that allows to remain in a state even when there are enabled actions, no useful liveness property about processes can ever be guaranteed. One therefore often makes a progress assumption, saying that the system will not idle as long as it can make progress. Armed with this assumption, it appears fair to say that the process F_{0} satisfies the required property G(r ⇒ F(t)).

However, by symmetry, the same line of reasoning would allow us to derive that F_{0} satisfies G(t ⇒ F(r)), i.e. each execution of t will be followed by a new request. Yet, this is something we specifically do not want to assume: the action r is meant to be fully under the control of the environment, and it may very well happen that at some point the environment stops making further requests. A particular instance of this is when the environment is modelled by a CCS context such as (r̄.0| )\r; in this context the process F_{0} will receive the request r only once.

Hence, we reject the validity of G(t ⇒ F(r)) based on environments such as (r̄.0| )\r. However, the same reasoning allows environments such as (r̄.t̄.r̄.0| )\r\t that do not allow the task t to be executed more than once. The existence of such environments totally defeats our scheduler, or any other one.

Thus, for a fair scheduler to make sense, we need to consider environments that have full control over the action r but cannot sabotage the mission of our scheduler by disallowing tasks t and e. We formalise this by calling t and e output actions. An output action [23, Section 9.1] is an activity of our system that cannot be stopped by its environment; or, equivalently, considering an action t to be output means that we choose not to consider environments that can block t. In our schedulers, t and e are output actions, whereas r is not.

8 When assuming that this formula holds, F_{0} trivially satisfies the other properties required in Section 7: the system will always return to a state where it remains ready to accept the next request r until it arrives; in any partial run there are no more occurrences of t than of r, and between each two occurrences of t the action e is scheduled.

Let CCS^{!} be the variant of CCS that is parametrised not only by sets A of names and K of agent identifiers, but also by a set O of output actions. The only further difference with CCS of Section 8 is that Act := H ·^{∪} O ·^{∪} {τ}, and a relabelling f extends to Act by f(α) := α for all α ∈ O ·^{∪} {τ}. CCS^{!} can be seen as an extension of CCS with output actions, but it can just as well be seen as a restriction of CCS in which for some of the names there are no co-names and no restriction operators.

It should be noted that CCS already features the concept of an internal action, namely τ, of which it is normally assumed that it cannot be blocked by the environment. Yet, for the purpose of specifying our scheduler, the rôle of the output action t cannot be played by τ, for the internal action is supposed to be unobservable and is easily abstracted away. Output actions share the feature of internal actions that whether they occur or not is determined by the internal work of the specified system only; yet at the same time they are observable by the environment in which the system is running.^{9} An action in O ·^{∪} {τ}—so an output or internal action—is also called a non-blocking action.

Now we formulate our progress assumption[23,29]:

Any process in a state that admits an non-blocking action will eventually perform an action.

LTL formulas are deemed to hold for a process P if they hold for all complete paths of P in the labelled transition system of CCS^{!}. Here a path of P is an alternating sequence of states and transitions, starting from the state P and either being infinite or ending in a state, such that each transition in the sequence goes from the state before to the state after it, and a finite path is complete iff it does not end in a state that enables a non-blocking action; completeness of infinite paths is discussed in the next sections. For further details, see [23, Section 9.1] or [29].

Assuming progress, the scheduler F_{0} =^{def} r.e.t.F_{0} satisfies G(r ⇒ F(t)) because on each complete path every r is followed by a t. Hence F_{0} is fair w.r.t. the simpler problem.

10 A Just Semantics of Parallelism

In the previous section we considered a scheduler that was significantly simpler than the one of Section 7, and were able to specify it in CCS^{!} by F_{0} =^{def} r.e.t.F_{0}, with output actions t and e. However, in order to ensure that our specification was formally correct, we needed to introduce the concept of an output action, and made a progress assumption on the semantics of the language.

In this section, we consider again a simplification of the scheduler of Section 7, and once more succeed in specifying it in CCS^{!}. Again we need to make an assumption about the semantics of CCS^{!} in order to ensure that our specification is formally correct.

9 The output and internal actions of CCS^{!} are similar to the output and internal action of I/O automata [44]. However, the remaining actions of I/O automata are input actions that are totally under the control of the environment of the modelled system. In CCS, on the other hand, the default type of action is a synchronisation that can happen only in cooperation between a system and its environment.

Both assumptions increase the range of correct CCS specifications and thereby make the promised result on the absence of any CCS specification of a scheduler as described in Section 7 more challenging.

Consider a scheduler as described in Section 7, but without the last requirement about the intermittent activity e. A candidate CCS^{!} specification is the process

F_{1}|F_{2}, defined by F_{i} =^{def} r_{i}.t_{i}.F_{i} , i ∈ {1, 2}.

Here, and throughout this paper, t_{i} (like e) is an output action and r_{i} is not. For this scheduler to be fair, it has to satisfy G(r_{i} ⇒ F(t_{i})) for i = 1, 2.^{10} By the reasoning of the previous section the process F_{i} satisfies the temporal formula G(r_{i} ⇒ F(t_{i})) for i = 1, 2. It is tempting to conclude that obviously their parallel composition F_{1}|F_{2} satisfies both of these requirements. Yet, the system run r_{1}(r_{2}t_{2})^{ω}—that after performing one action from F_{1} performs infinitely many actions from F_{2} without interleaving any further actions from F_{1}—could be considered a counterexample.

Here we take the point of view that no amount of activity of F_{2} can prevent F_{1} from making progress. The system F_{1}|F_{2} simply does not have a run r_{1}(r_{2}t_{2})^{ω}. The corresponding path from the state F_{1}|F_{2} in the LTS of CCS^{!} is no more than an artifact of the use of interleaving semantics. In general, we make the following justness assumption [29]:

If a combination of components in a parallel composition is in a state that admits a non-blocking action, then one (or more) of them will eventually partake in an action.

Thus justness guarantees progress of all components in a parallel composition, and of all combinations of such components. In the CCS^{!} expression ((P |Q)\a)|R with P =^{def} a.P + c.P, Q =^{def} ā.Q and R =^{def} b.R + c̄.R for instance there is a state where P admits an action c ∈ H with c ≠ a and R admits an action c̄. Thereby, the combination of these components admits an action τ. Our justness assumption now requires that either P or R will eventually partake in an action. This could be the τ-action obtained from synchronising c and c̄, but it also could be any other action involving P or R. In each case the system will (at least for an instant) cease to be in a state where that synchronisation between P and R is enabled. Note that progress is a special case of justness, obtained by considering any process as the combination of all its parallel components.

In [29] we formalised the justness assumption as follows. Any transition P |Q ⟶^{α} R derives, through the rules of Table 1, from

– a transition P ⟶^{α} P′ and a state Q, where R = P′|Q,

– two transitions P ⟶^{α_{1}} P′ and Q ⟶^{α_{2}} Q′, where R = P′|Q′,

– or from a state P and a transition Q ⟶^{α} Q′, where R = P |Q′. This transition/state, transition/transition or state/transition pair is called a decomposition of P |Q ⟶^{α} R; it need not be unique, as we will show in Example 1 below. Now a decomposition of a path η of P |Q into paths η_{1} and η_{2} of P and Q, respectively, is obtained by decomposing each transition in the path, and concatenating all left-projections into a path of P and all right-projections into a path of Q. Here it could be that η is infinite, yet either η_{1} or η_{2} (but not both) are finite. Again, decomposition of paths need not be unique.

10 When assuming that these formulas hold, F_{1}|F_{2} trivially satisfies the other properties required of it: the system will always return to a state where it remains ready to accept the next request r_{i} until it arrives—hence for any numbers n_{1} and n_{2} ∈ IN ∪{∞} there is at least one run of the system in which exactly that many requests of type r_{1} and r_{2} are received—and in any partial run there are no more occurrences of t_{i} than of r_{i}.

Similarly, any transition P [f] ⟶^{α} R stems from a transition P ⟶^{β} P′, where R = P′[f] and α = f(β). This transition is called a decomposition of P [f] ⟶^{α} R. A decomposition of a path η of P [f] is obtained by decomposing each transition in the path, and concatenating all transitions so obtained into a path of P. A decomposition of a path of P \c is defined likewise.

Definition 1 Y-justness, for Y ⊆ H ,^{11} is the largest family of predicates on the paths in the LTS of CCS^{!} such that

– a finite Y-just path ends in a state that admits actions from Y only;

– a Y-just path of a process P |Q can be decomposed into an X-just path of P and a Z-just path of Q such that Y ⊇X∪Z and X∩Z̄ =∅—here Z̄:={c̄ | c∈Z};

– a Y-just path of P \c can be decomposed into a Y ∪{c, c̄}-just path of P;

– a Y-just path of P [f] can be decomposed into an f^{−1}(Y)-just path of P;

– and each suffix of a Y-just path is Y-just. A path η is just if it is Y-just for some Y ⊆ H . It is a-enabled for an action a ∈ H if a ∈ Y for all Y such that η is Y-just.

Intuitively, a Y-just path models a run in which Y is an upper bound of the set of labels of abstract transitions^{12} that from some point onwards are continuously enabled but never taken. Here an abstract transition with a label from H is deemed to be continuously enabled but never taken iff it is enabled in a parallel component that performs no further actions. Such a run can actually occur if the environment from some point onwards blocks the actions in Y.

The last clause in the second requirement prevents an X-just path of P and a Z-just path of Q to compose into an X∪Z-just path of P |Q when X contains an action a and Z the complementary action ā. The reason is that no environment can block both actions for their respective components, as nothing can prevent them from synchronising with each other. The fifth requirement helps characterising processes of the form b.0 + (A|b.0) and a.(A|b.0), with A =^{def} a.A. Here, the first transition ‘gets rid of’ the choice and of the leading action a, respectively, and reduces the justness of paths of such processes to their suffixes.

A complication in understanding Definition 1 is that a single path could be seen as modelling different system runs of which one could be considered just, respectively a-enabled, and the other not.

Example 1 Consider the process B|B defined by B =^{def} b.B. The only transition of this process is B|B ⟶^{b} B|B, so B|B has exactly one infinite path η, obtained by repeating this transition infinitely often. Assuming that b is an output action, one may wonder if η should count as being just. In case all transitions in η originate from the left component, the b-transition of the right component is continuously enabled but never taken. This does not correspond to a (just) run of the represented system. However, in case η alternates transitions from each component, it does model a (just) run. The mere fact that a b-transition is enabled on every state of η has no bearing on the matter. Now Definition 1 considers η just, on grounds of the fact that it models some (just) run.

11 By definition Y does not contain non-blocking action.

12 The CCS process a.0|b.0 has two transitions labelled a, namely a.0|b.0 ⟶^{a} 0|b.0 and a.0|0 ⟶^{a} 0|0. The only difference between these two transitions is that one occurs before the action b is performed by the parallel component and the other afterwards. In [29] we formalise a notion of an abstract transition that identifies these two concrete transitions.

If in this example b is a handshake action, the path η models a (just) run in which a b-labelled abstract transition is continuously enabled but never taken; but it also models a (just) run in which no transition is continuously enabled but never taken. According to Definition 1, η counts as ∅-just, and thus is not deemed b-enabled. Intuitively, a path is b-enabled iff on all runs modelled by that path a transition labelled b is continuously enabled but never taken. ⊓ ⊔

Now a just path, as defined above, is our default definition of a complete path, as contemplated at the end of Section 9. Indeed, a finite path is just iff it does not end in a state from which a non-blocking action is possible [29].

Thus, our semantics of a CCS^{!} process P consists of the state P in the LTS of CCS^{!} together with the set of complete paths in that LTS starting from P [23, 29]. LTL formulas hold for P iff they are valid on all complete paths of P.

Here we employ a just semantics of CCS^{!} by taking the just paths to be the complete ones. This way F_{0} is a correct specification of the scheduler required in Section 9 and F_{1}|F_{2} is a correct specification of the scheduler required above.

11 Formal Specification of the Fair Scheduler

We now provide a formal specification of the scheduler described in Section 7. Since the aim of this paper is to show that this cannot be done in CCS^{!} (and thus certainly not in CCS) we need a different formalism for this task. Here we follow the traditional approach of TLA [39] and several other frameworks [24], “in which first the legal computations are specified, and then a fairness notion is used to exclude some computations which otherwise would be legal” [2]. Following [29], we use CCS^{!} for the first step and LTL for the second.

Thus, in this section we specify a process as a pair of a CCS^{!} expression P and a set F of LTL formulas, called a fairness specification. The semantics of P consists of the state P in the LTS of CCS^{!} together with the set of just paths in that LTS starting from P. The formulas of F are evaluated on the paths of P and any path that satisfies all formulas of F is called fair. Now the semantics of the entire specification (P, F) is the state P in the LTS of CCS^{!} together with the set of complete paths of P, defined as those paths that are both just and fair. In [23, 29] a consistency requirement is formulated that should hold between P and F.

Now a fair scheduler as described in Section 7 can be specified by the CCS^{!} process (I_{1} | G | I_{2})\c_{1}\c_{2}, where

I_{i} =^{def} r_{i}.c̄_{i}.I_{i} (i ∈ {1, 2}) and G =^{def} c_{1}.t_{1}.e.G + c_{2}.t_{2}.e.G ,

augmented with the fairness specification ⋀_{i=1,2} G(r_{i} ⇒ F(t_{i})).

Here the first requirement of Section 7 is satisfied by locating the two channels receiving the requests r_{1} and r_{2} on different parallel components I_{1} and I_{2}. This way, after performing, say, r_{1}, the system—component I_{1} to be precise—will always return to a state where it remains ready to accept the next request r_{1} until it arrives, independent of occurrences of r_{2}. The (non-output) actions c_{i} are used to communicate the request from the processes I_{i} to a central component G, which then performs the requested action t_{i}.

The second requirement of Section 7 is enforced by the fairness specification, and the last two requirements of Section 7 are met by construction: in any partial run there are no more occurrences of t_{i} than of r_{i}, and between each two occurrences of t_{i} and t_{j} for i, j ∈ {1, 2} the intermittent action e is scheduled.

12 Fair Schedulers Cannot be Rendered in CCS^{!}—Formalisation

In this section we formulate the main result of the paper, namely that no scheduler as described in Sections 7 and 11 can be specified in CCS^{!}. Since we already showed that it can be specified in CCS^{!} augmented with a fairness specification, here, and in the rest of the paper, we confine ourselves to CCS^{!} without fairness specifications. Thus, our notion of a complete path is (re)set to that of a just path, as specified in Definition 1.

Theorem 1 There does not exist a CCS^{!} expression F such that:

1. any complete path of F that has finitely many occurrences of r_{i} is r_{i}-enabled;

2. on each complete (= just) path of F, each r_{i} is followed by a t_{i};

3. on each finite path of F there are no more occurrences of t_{i} than of r_{i}; and 4. between each two occurrences of t_{i} and t_{j} (i, j ∈ {1, 2}) an action e occurs.

Requirements 1–4 exactly formalise the four requirements described in Section 7. We proceed to show that none of them can be skipped.

The CCS^{!} process F_{1}|F_{2} of Section 10 satisfies Requirements 1, 2 and 3. It does not satisfy Requirement 4, due to the partial run r_{1}r_{2}t_{1}t_{2}.

The CCS^{!} process E_{1}|G_{1}|E_{2} with E_{i} =^{def} r_{i}.E_{i} for i=1, 2 and G_{1} =^{def} t_{1}.e.t_{2}.e.G_{1}

satisfies Requirements 1, 2 and 4. It does not satisfy Requirement 3, due to the partial run consisting of the single action t_{1}.

The CCS^{!} process E_{1}|E_{2} satisfies Requirements 1, 3 and 4, but not 2.

Finally, the process G_{2} given by G_{2} =^{def} r_{1}.t_{1}.e.G_{2} + r_{2}.t_{2}.e.G_{2} satisfies Requirements 2, 3 and 4. However, it does not satisfy Requirement 1, because it allows the ∅-just path (r_{2}t_{2}e)^{ω} with no occurrences of r_{1}. This path models a run in which the system never reaches a state where it remains ready to accept the next request r_{1}.

The proof of Theorem 1 will be the subject of Part III.

13 A Characterisation of Fair Schedulers without a-enabling

Below we will show that without loss of generality we may assume any fair scheduler to have a specific form. If it has that form, Requirement 1 is redundant. Hence Requirement 1 can be replaced by requiring that the scheduler is of that form. This variant of our result appeared as a conjecture in [29].

For any CCS^{!} expression F, let F̂ := (I_{1} | F [f] | I_{2})\c_{1}\c_{2} with I_{i} =^{def} r_{i}.c̄_{i}.I_{i} for i ∈ {1, 2}, where f is an injective relabelling with f(r_{i}) = c_{i} for i = 1, 2, and r_{1}, r_{2}, r̄_{1}, r̄_{2} ∉ f(H ). By the definition of relabelling (cf. Section 9), f(t_{i}) = t_{i} and f(e) = e.

Theorem 2 A process F meets Requirements 1–4 of Theorem 1 iff F̂ meets these requirements, which is the case iff F̂ meets Requirements 2–4.

Proof Suppose F satisfies Requirements 1–4.

1. To show that F̂ satisfies Requirement 1 (with i:= 1; the other case follows by symmetry), it suffices to show that each occurrence of r_{1} in a just path of F̂, which corresponds to an occurrence of r_{1} in the subprocess I_{1}, is followed by an occurrence of c̄_{1} in I_{1}. So assume, towards a contradiction, that on a just path η of F̂ an occurrence of r_{1} is not followed by an occurrence of c̄_{1} in the subprocess I_{1}. By Definition 1 η must be Y-just for some Y ⊆ H . So η can be decomposed into an X-just path η_{1} of I_{1}, a Z-just path η_{0} of F [f] and a W -just path η_{2} of I_{2} for certain X, Z, W ⊆ H . By assumption, c̄_{1} ∈ X. Moreover, η_{0} can be decomposed into an f^{−1}(Z)-just path η_{F} of F. Since in F̂ the c_{1} of F [f] requires synchronisation with the c̄_{1} of I_{1}, and η_{1} has only finitely many occurrences of c̄_{1}, it follows that η_{0} has only finitely many occurrences of c_{1}, and thus that η_{F} has only finitely many occurrences of r_{1}. Since F satisfies Requirement 1, saying that the system will always return to a state where it remains ready to accept the next request r_{1} until it arrives, r_{1} ∈ f^{−1}(Z). Hence c_{1} ∈ Z. By Definition 1, this contradicts the justness of η.

2. Above we have shown that each occurrence of r_{1} in a just path of F̂, which corresponds to an occurrence of r_{1} in the subprocess I_{1}, is followed by an occurrence of c̄_{1} in I_{1}. This occurrence of c̄_{1} in I_{1} must be a synchronisation with an occurrence of c_{1} in F [f], and by Requirement 2 for F each occurrence of c_{1} in F [f] is followed by an occurrence of t_{1} in F [f], and hence in F̂.

3. By Requirement 3 for F, on each finite path from F [f] there are no more occurrences of t_{1} than of c_{1}. Moreover, on each finite path from I_{1} there are no more occurrences of c̄_{1} than of r_{1}. Since in F̂ each occurrence of c_{1} in F [f] needs to synchronise with an occurrence of c̄_{1} in I_{1}, it follows that on each finite path from F̂ there are no more occurrences of c̄_{1} than of r_{1}.

4. Requirement 4 holds for F̂ because it holds for F.

Now assume that F̂ satisfies Requirements 2–4.

1. Suppose that F would fail Requirement 1, say for i = 1. Then it has a Z-just path with r_{1} ∉ Z. Therefore F [f] has an f(Z)-just path with c_{1} ∉ f(Z). This path can be synchronised with a c̄_{1}-just path of I_{1} into a just path of F̂ in which an occurrence of r_{1} follows the last occurrence of t_{1}, thereby violating Requirement 2 for F̂.

2. Suppose that F would fail Requirement 2, say for i = 1. Then it has a just path with an occurrence of r_{1} past the last occurrence of t_{1}. Therefore F [f] has a Z-just path with r̄_{1} ∉ Z and an occurrence of c_{1} past the last occurrence of t_{1}. This path can be synchronised with a r_{1}-just path of I_{1} into a just path of F̂ in which an occurrence of r_{1} follows the last occurrence of t_{1}, thereby violating Requirement 2 for F̂.

3. Suppose F had a finite path with more occurrences of t_{1} than of r_{1}, then through synchronisation a finite path of F̂ could be constructed with more occurrences of t_{1} than of r_{1}.

4. Requirement 4 holds for F because it holds for F̂. ⊓ ⊔

\underline{Process A} repeat forever

ℓ_{1} noncritical section
ℓ_{2} readyA := true
ℓ_{3} turn := B
ℓ_{4} await (readyB = false ∨ turn = A)
ℓ_{5} critical section
ℓ_{6} readyA := false

\underline{Process B} repeat forever

m_{1} noncritical section
m_{2} readyB := true
m_{3} turn := A
m_{4} await (readyA = false ∨ turn = B)
m_{5} critical section
m_{6} readyB := false

Fig. 1 Peterson’s algorithm (pseudocode)

Recall that G_{2}, given by G_{2} =^{def} r_{1}.t_{1}.e.G_{2} + r_{2}.t_{2}.e.G_{2}, satisfies Requirements 2–4. Converting this G_{2} to the process Ĝ_{2} of the form (I_{1} | G | I_{2})\c_{1}\c_{2}, as defined above, results in the specification of Section 11 without the additional fairness specification, and hence in the loss of Requirement 2.

14 (In)Correct Correctness Proofs of Peterson’s and Dekker’s Protocols

It is widely accepted that Peterson’s mutual exclusion protocol [51] implements a fair scheduler, and that implementing Peterson’s algorithm in a CCS-like language should be easy. In fact Peterson’s algorithm has been specified in CCS-like languages several times, e.g. [61,10,59,1]. All these papers present essentially the same rendering of Peterson’s algorithm in CCS or some other progress algebra, differing only in insignificant implementation details. This seems to contradict our main result (Theorem 1).

Peterson’s Mutual Exclusion Protocol deals with two concurrent processes A and B that want to alternate critical and noncritical sections. Each of these processes will stay only a finite amount of time in its critical section, although it is allowed to stay forever in its noncritical section. The purpose of the algorithm is to ensure that they are never simultaneously in the critical section, and to guarantee that both processes keep making progress. Pseudocode is depicted in Figure 1.

The processes use three variables. The Boolean variable readyA can be written by process A and read by process B, whereas readyB can be written by B and read by A. By setting readyA to true, process A signals to process B that it wants to enter the critical section. The variable turn is a shared variable: it can be written and read by both processes. Its use is the brilliant part of the algorithm. Initially readyA and readyB are both false and turn = A.

Peterson’s algorithm implements a mutual exclusion protocol and hence should satisfy the safety property that at any time only one process accesses the critical system, i.e.

G(¬((ℓ_{4} ∨ ℓ_{5}) ∧ (m_{4} ∨ m_{5}))) .

Here, ℓ_{i} and m_{j} refer to line numbers of the pseudocode (Figure 1). As convention we assume that line numbers refer to a state in the execution of the code where the command of the line has already been executed. Most papers, including [10, 1], concentrate on the issue of mutual exclusion only, and that is done correctly in the CCS rendering. When safety properties are considered only, no fairness or progress assumption is needed: in the worst case some (or all) processes do not progress and hence never enter the critical section—the safety property still holds.

As usual, a safety property should therefore be accompanied with a liveness property. In case of Peterson’s protocol such a property is that any process that wants to enter the critical section will at some point reach the critical section. We consider two possibilities to characterise this property:

G(ℓ_{1} ⇒ F(ℓ_{4})) , and G(ℓ_{2} ⇒ F(ℓ_{4})) .^{13}

Both properties have the form G(r_{1} ⇒ F(t_{1}))—the property discussed in this paper—ℓ_{4} indicates that the process enters the critical section. Both ℓ_{1} and ℓ_{2} could play the rôle of the grant request r_{1}. Although it seems surprising, we will show that there is a fundamental difference between these two formulas.

To show how Peterson’s algorithm yields an instance of our fair scheduler, we consider the action t_{1} to be taken when an execution passes through state ℓ_{4}, thereby interpreting t_{1} as granting access to the critical section. The action e is taken when the execution passes through state ℓ_{5}, marking the exit of the critical section. Peterson’s code, in combination with the mutual exclusion property, ensures that Requirement 4 of our fair scheduler is satisfied. We consider r_{1} to be taken when an execution passes through state ℓ_{1}, so that the liveness property G(ℓ_{1} ⇒ F(ℓ_{4})) ensures Requirement 2. Requirement 1 is satisfied, because as soon as the environment of the protocol leaves the noncritical section, thereby getting ready to enter the critical one, the protocol is considered to take the action r_{1}. Finally, Requirement 3 is obviously ensured by Peterson’s code.

In combination with this insight, our main result (Theorem 1) entails that the rendering of Peterson’s algorithm in CCS found in the literature cannot be correct, as long as the semantics of CCS is fortified with at most justness. To prove liveness of Peterson’s protocol, at least weak fairness is required.^{14} In the literature we found only two papers that investigate liveness properties of this protocol: [61] and [59]. Neither of these papers employs fairness or justness properties.

Walker [61] tries to prove the correctness of Peterson’s algorithm by automatic methods. He succeeds for the safety property, but could not establish the liveness property in full generality; however Walker succeeded in proving it when restricting attention to runs in which infinitely many visible actions occur. This appears to be Walker’s method of imposing a progress assumption. Although this is strictly speaking not in contradiction with our results, our proofs trivially extend to the case of considering only runs in which infinitely many visible actions occur. Hence Walker’s result seems to be in contradiction to Theorem 1. A detailed analysis reveals that Walker uses line ℓ_{2} as request action to indicate interest to enter the critical section. So he shows that G(ℓ_{2} ⇒ F(ℓ_{4})). That means that the shared variable readyA must be set—only then ℓ_{2} evaluates to true. His request action is set right after setting this variable. However, following our proof, the reason that the CCS rendering of Peterson does not work, is that it is possible that process A never gets a change to set the shared variable readyA to true, because the other process is too busy reading it all the time (even when it enters the critical section between any two reads). So, it is a possible scenario that process A will never execute line ℓ_{2}, although it wants to enter the critical section.

13 We only give the liveness property for process A; the one for process B is similar.

14 Whether weak fairness suffices depends on the interpretation of enabledness (cf. Section 2)

In Peterson’s original thinking, process B could not prevent process A from writing by reading a shared variable; but in the CCS model this is quite possible: the read action can only be represented as a transition that is in conflict with the write action; only after this transition is taken does the process return to a state where the write is enabled. So when Walker [61] establishes G(ℓ_{2} ⇒ F(ℓ_{4})) he merely shows that when the first hurdle is taken successfully the process will surely enter the critical section. What he cannot establish is that a process that is ready to enter the critical section will succeed in setting readyA. The correct modelling of Peterson’s liveness property thus places action r_{1} before setting the variable readyA to true, i.e.

G(ℓ_{1} ⇒ F(ℓ_{4})) .

In terms of our description of a fair scheduler, the action r_{1} of Walker (at position ℓ_{2}) does not meet Requirement 1.

The analysis of the work of Walker shows that there is a fine line between correct and incorrect modelling. In fact it looks reasonable to prove G(ℓ_{2} ⇒ F(ℓ_{4})) instead of G(ℓ_{1} ⇒ F(ℓ_{4})). There is no formal way to avoid such mistakes; only careful (informal) reasoning.

Roughly the same modelling, but in which the request r_{1} is identified with setting the shared variable readyA to true, occurs in Valmari & Setälä [59]. The consequences are the same.

Dekker’s mutual exclusion protocol [20,21] is another well-known algorithm that implements a fair scheduler. We found two papers in the literature that analyse liveness of this protocol.

Esparza & Burns [22] follow in the footsteps of Walker and prove the correctness of Dekker’s mutual exclusion algorithm in the Box Calculus without postulating a fairness assumption. According to our results, this is impossible as well. Indeed, as in [59], Esparza & Burns model the request r_{1} to be the action of setting a shared variable, which again violates the property that a process that wants to enter the critical section can always succeed at least in making a request to that effect.

Corradini, Di Berardini & Vogler [14] specify Dekker’s algorithm in the CCSlike process algebra PAFAS. They also prove the correctness of the algorithm. This paper models the relevant liveness properties correctly, as far as we can see, but explicitly makes different assumptions on the driving force that keeps the system running. First they consider a notion of ‘fairness of actions’ that appears to be similar to our justness assumption,^{15} and they show that their model of Dekker’s protocol fails to have the required liveness property. This result is entirely consistent with ours. In fact we generalise their negative result about the correctness of a particular rendering in PAFAS of a particular protocol for mutual exclusion to a general statement quantifying of all renderings of all such protocols.

Next they consider a stronger notion of fairness called ‘fairness of components’, stemming from [18], and, under this assumption, establish the correctness of the algorithm.^{16} The present paper augments this result by saying that a fairness notion as strong as ‘fairness of components’ is actually needed.

15 It differs in a crucial way, however, namely by treating each action as output. As a consequence, under fairness of actions the process F_{1}|F_{2} of Section 10 is guaranteed to perform each of the actions r_{1} and r_{2} infinitely often. To model a protocol where the action r_{i} is not forced to occur, a τ-loop is inserted at each location where r_{i} is enabled.

In Part I we pointed out that our result holds for CCS+justness, CCS+progress and CCS without any progress assumption. However a fair scheduler can be implemented when a fairness assumption is assumed; fairness of components appears to be sufficient.

Part III Proofs

15 Fair Schedulers Cannot be Rendered in Petri Nets—Formalisation

This section introduces Petri nets and rephrases Theorem 1 in terms of Petri nets. We inherit the sets Act of actions and H ⊆ Act of handshaking communications from Section 8, and the set O of output actions from Section 9.

A multiset over a set X is a function A: X → IN, i.e. A ∈ IN^{X}. The function ∅: X → IN, given by ∅(x) := 0 for all x ∈ X, is the empty multiset over X. x ∈ X is an element of A, notation x ∈ A, iff A(x) > 0. For multisets A and B over X we write A ≤ B iff A(x) ≤ B(x) for all x ∈ X; A ∩ B denotes the multiset over X with (A ∩ B)(x) := min(A(x), B(x)), A + B denotes the multiset over X with (A + B)(x) := A(x) + B(x), and A − B is only defined if B ≤ A and then denotes the multiset over X with (A − B)(x) := A(x) − B(x). A multiset A with A(x) ≤ 1 for all x is identified with the (plain) set {x | A(x)=1}.

Definition 2 A (labelled) Petri net (over Act) is a tuple N = (S, T, F, M_{0}, ℓ) with – S and T disjoint sets (of places and transitions),

– F : ((S × T) ∪ (T × S)) → IN (the flow relation including arc weights),

– M_{0} : S → IN (the initial marking), and

– ℓ : T → Act (the labelling function).

When a Petri net represents a concurrent system, a global state of this system is given as a marking, a multiset M of places. The initial state is M_{0}.

The behaviour of a Petri net is defined by the possible moves between markings M and M′, which take place when a transition u fires. In that case, u consumes F (s, u) tokens from each place s. Naturally, this can happen only if M makes all these tokens available in the first place. Moreover, u produces F (u, s) tokens in each s. Definition 3 formalises this notion of behaviour.

Definition 3 Let N = (S, T, F, M_{0}, ℓ) be a Petri net and u ∈ T. The multisets •u, u^{•} : S → IN are given by^{•}u(s) = F (s, u) and u^{•}(s) = F (u, s) for all s∈S;^{17} the elements of ^{•}u and u^{•} are called pre- and postplaces of u, respectively. Transition u ∈ T is enabled from the marking M ∈ IN^{S}—notation M[u⟩—if ^{•}u ≤ M. In that case firing u yields the marking M′ := M −^{•}u + u^{•}—notation M[u⟩M′.

16 Fairness of components is a form of weak fairness, requiring that if a component from some point onwards is enabled in each state, an action from that component will eventually be scheduled. Here a component is enabled if an action from that component is enabled, possibly in synchronisation with an action from outside that component. Under this notion of fairness, the system E from Section 2, defined by E =^{def} a.E + b.0, is not ensured to do a b eventually.

However, the composition (E|b̄.c.0)\b is ensured to do a c eventually, because the component b̄.c.0 is enabled in every state.

17 Here, we slightly deviate from standard notation [57], where ^{•}u and u^{•} are usually plain sets, obtained from our multisets by abstracting from the multiplicities of their elements. We prefer to retain this information, so as to shorten various formulas.

A path π of a Petri net N is an alternating sequence M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} … of markings and transitions, starting from the initial marking M_{0} and either being infinite or ending in a marking M_{n}, such that M_{k}[u_{k}⟩M_{k+1} for all k (<n). An action α ∈ Act occurs on a path π if there is a transition u_{i} with ℓ(u_{i}) = α. A marking is reachable if it occurs in such a path. The Petri net N is safe if all reachable markings M are plain sets, meaning that M(s) ≤ 1 for all places s. It is a structural conflict net [28] if ^{•}u + ^{•}v ≤ M ⇒ ^{•}u ∩ ^{•}v = ∅ for all reachable markings M and all transitions u and v. Note that any safe Petri net is a structural conflict net. In this paper we restrict attention to structural conflict nets with the additional assumptions that ^{•}u = ∅ for no transition u, and that all reachable markings are finite. In the remainder we refer to these structures as nets. For the purpose of establishing Theorem 1 we could just as well have further restricted attention to safe Petri nets whose reachable markings are finite.

On a path π = M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} … a transition v is continuously enabled from position k onwards if M_{k}[v⟩ and^{•}v∩^{•}u_{i} = ∅ for all i>k. This implies that^{•}v ≤ M_{i} for all i ≥ k. If such a transition v exists we say that π is ℓ(v)-enabled. A path is just or complete if it is o-enabled for no non-blocking action o ∈ O ∪ {τ}.

Now we have all the necessary definitions to state that our fair scheduler cannot be realised as a net.

Theorem 3 There does not exist a net N such that:

1. any complete path of N that has finitely many occurrences of r_{i} is r_{i}-enabled;

2. on each complete (= just) path of N, each r_{i} is followed by a t_{i};

3. on each finite path of N there are no more occurrences of t_{i} than of r_{i}; and 4. between each two occurrences of t_{i} and t_{j} (i, j ∈ {1, 2}) an action e occurs.

In the proof of this theorem we do not use the restriction that N is a structural conflict net. However, for general Petri nets our definition of a transition that from some points onwards is continuously enabled is not convincing. A better definition would replace the requirement ^{•}v ∩^{•}u_{i} = ∅ for all i > k by ^{•}v +^{•}u_{i+1} ≤ M_{i} for all i ≥ k. On structural conflict nets the two definitions are equivalent. On general Petri nets with finite reachable markings and ∀u.^{•}u ≠ ∅ Theorem 3 still holds when employing our earlier definition of being continuously enabled, but that definition arguably leads to Requirement 1 being an overly restrictive formalisation of the first requirement of Section 7.

In [60] and in [37] mutex problems are presented that cannot be solved in terms of Petri nets. These results are almost equivalent to Theorem 3, but, as discussed in the Section 4, lack the generality needed to infer Theorem 1 from Theorem 3.

16 Fair Schedulers Cannot be Rendered in Petri Nets—Proof

In this section we suppose that there exists a net N meeting the requirements of Theorem 3. We establish various results about this hypothetical net N, ultimately leading to a contradiction. This will constitute the proof of Theorem 3.

16.1 Embellishing Paths into Complete Paths

A firing sequence of N is a sequence σ = u_{1}u_{2}u_{3} … of transitions such that there exists a path π = M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} … of N. Note that π is uniquely determined by σ (and M_{0}); we call it ph(σ). Likewise, σ is determined by π, and we call it fs(π).

A firing sequence σ′ = v_{1}v_{2}v_{3} … embellishes a firing sequence σ = u_{1}u_{2}u_{3} … iff σ′ can be obtained out of σ through insertion of non-blocking transitions; that is, if there exists a monotone increasing function f : IN → IN—thus satisfying i < j ⇒ f(i) < f(j)—with v_{f(i)} = u_{i} for all i > 0 and ℓ(v_{j}) ∈ O ∪ {τ} for any index j not of the form f(i). A path π′ embellishes a path π iff fs(π′) embellishes fs(π).

Given a firing sequence σ = u_{1}u_{2} … of length ≥k and a transition w, let σ⊕_{k} w denote the sequence u_{1}u_{2} … u_{k}wu_{k+1}u_{k+2} … obtained by inserting w in σ at position k.

Lemma 1 Let σ be a firing sequence of length ≥k and w a transition that on ph(σ) is continuously enabled from position k onwards. Then σ ⊕_{k} w is a firing sequence.

Proof Let ph(σ) = M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} . . .. Define M′_{i} := M_{i} − ^{•}w + w^{•} for i ≥ k. Then M_{0}u_{1}M_{1}u_{2} … u_{k}M_{k}wM′_{k}u_{k+1}M′_{k+1}u_{k+2} … is again a path of N, using that •w ≤ M_{i} and ^{•}u_{i+1} ≤ M_{i} −^{•}w for all i ≥ k. ⊓ ⊔

If π is a path and w a transition that on π is continuously enabled from position k onwards, then π ⊕_{k} w abbreviates ph(fs(π) ⊕_{k} w).

A path π = M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} … of N is (k, n)-incomplete if k is the smallest number such that there is a transition w with ℓ(w) ∈ O ∪ {τ}—called a witness of the (k, n)-incompleteness of π—that is continuously enabled from position k onwards, and n is the number of places s of N such that s ∈^{•}w for a witness w of the (k, n)-incompleteness of π. Since the reachable marking M_{k} is always finite, so are the numbers n. Note that a path is (k, n)-incomplete for some finite k and n iff it is not complete; henceforth we call a complete path (∞, 0)-incomplete. If a path π is (k, n)-incomplete, and a path ρ is (h, m)-incomplete, then we call ρ less incomplete than π if ρ has the same prefix up to position k as π and either h > k or h = k ∧ m < n.

Lemma 2 Let i ≥ 0, π be a (k, n)-incomplete path of the net N with at least k+i transitions, and w a witness of the (k, n)-incompleteness of π. Then π ⊕_{k+i} w is less incomplete than π.

Proof Suppose π ⊕_{k+i} w is (h, m)-incomplete with h ≤ k, and let v be a witness of the (h, m)-incompleteness of π ⊕_{k+i} w. Then on π ⊕_{k+i} w the transition v is continuously enabled from position h onwards. Let M_{h} be the marking occurring at position h in π, or equivalently in π ⊕_{k+i} w. Then ^{•}v ≤ M_{h} and ^{•}v ∩^{•}u = ∅ for all transitions u occurring in π ⊕_{k+i} w past position h. This includes all transitions u occurring in π past position h, so v is continuously enabled from position h onwards also on π. It follows that h = k and any witness of the (k, m)-incompleteness of π⊕_{k+i}w is also a witness of the witness of the (k, n)-incompleteness of π. Moreover, •v ∩^{•}w = ∅, and since ^{•}w ≠ ∅ this implies m < n. ⊓ ⊔

Lemma 3 Any infinite path in N is embellished by a complete path.

Proof Let π be the given path. We build a sequence π_{i} of paths in N that all embellish π, such that, for all i, π_{i+1} is less incomplete than π_{i} and the first 2i transitions of π_{i} and π_{i+1} are the same.

We start by taking π_{0} to be π. If at any point we hit a path π_{i} that is complete, our work is done. Otherwise, given the (k, n)-incomplete path π_{i}, for some k and n, pick a witness w of the (k, n)-incompleteness of π_{i} and take π_{i+1}:=π_{i}⊕_{k+2i}w. This path exists by Lemma 1, since w is continuously enabled from position k onwards, and hence also from position k + 2i onwards. By construction π_{i+1} embellishes π_{i} and hence π. By Lemma 2 π_{i+1} is less incomplete than π_{i}. Moreover, the first 2i transitions of π_{i} and π_{i+1} are the same.

If at no point we hit a path π_{i} that is complete, let ρ := lim_{i→∞} π_{i}. This limit clearly exists: for any i∈IN the first 2i transitions of ρ are the first 2i transitions of π_{i} (and thus also of π_{j} for any j>i). We show that ρ is complete and embellishes π.

For the latter property, the i^{th} transition u_{i} of π must also occur in π_{i}, and no further than at position 2i, for π_{i} is an embellishment of π obtained by adding only i transitions. As in the sequence (π_{j})_{j=0}^{∞} past index i no further changes occur in the first 2i transitions, the transition u_{i} also occurs in ρ. Given the construction, this implies that ρ embellishes π. The same argument shows that ρ embellishes π_{i} for each i ∈ IN.

Now suppose that ρ is incomplete. Then there is a non-blocking transition w that on ρ, from some position k onwards, is continuously enabled. Let i ∈ IN be an index such that π_{i} is (k, n)-incomplete for some k > h. Such an i must exist, as the members of (π_{i})_{i=0}^{∞} become less incomplete with increasing i. Let M_{h} be the marking occurring at position h in ρ. Then M_{h} also occurs at position h in π_{i}, as the first k + 2i transitions of π_{i} are the same for all π_{j} with j ≥ i, and thus for ρ. Now ^{•}w ≤ M_{h} and ^{•}w ∩^{•}u = ∅ for all transitions u occurring in ρ past position h. Since ρ embellishes π_{i}, this includes all transitions u occurring in π_{i} past position h, so w is continuously enabled from position h onwards also on π_{i}, contradicting the (k, n)-incompleteness of π_{i}. ⊓ ⊔

Lemma 4 Any finite path in N can be extended to a complete path in N, such that all transitions in the extension have labels in O ∪ {τ}.

Proof This is a simpler variant of the previous proof. Let π be the given path. We build a sequence π_{i} of paths in N that all extend π, such that, for all i, π_{i+1} is less incomplete than π_{i} and extends π_{i} by one transition.

We start by taking π_{0} to be π. If at any point we hit a path π_{i} that is complete, our work is done. Otherwise, given the (k, n)-incomplete path π_{i}, for some k and n, pick a witness w of the (k, n)-incompleteness of π_{i} and obtain π_{i+1} := ph(fs(π_{i})w) by appending transition w to π_{i}. By construction π_{i+1} extends π_{i} by one nonblocking transition and hence extends π. By Lemma 2 π_{i+1} is less incomplete than π_{i}.

If at no point we hit a path π_{i} that is complete, let ρ := lim_{i→∞} π_{i}. Clearly, ρ extends π. That ρ is complete follows exactly as in the previous proof. ⊓ ⊔

16.2 Paths of the Hypothetical Fair Scheduler

Lemma 5 Our hypothetical net N has a path with no occurrences of (transitions labelled) r_{1}, but infinitely many occurrences of r_{2}.

Proof We construct an infinite sequence (π_{k})_{k=0}^{∞} of finite paths of N, such that π_{k} has no occurrences of r_{1} and exactly k occurrences of r_{2}, and such that π_{k} is a prefix of π_{k+1} for all k ∈ IN. The limit of this sequence will be the required path.

π_{0} is the trivial path, consisting of the initial marking M_{0} only.

Now assume we have constructed a path π_{k} as required. By Lemma 4 π_{k} can be extended into a complete path π′_{k} that has no occurrences of r_{1} and exactly k occurrences of r_{2}. Since π′_{k} is complete, it must be r_{2}-enabled by Requirement 1. Hence there is a finite prefix π′′_{k} of π′_{k}, still extending π_{k}, such that a transition v with ℓ(v) = r_{2} is enabled in the last state of π′′_{k}. Obtain p_{k+1} by extending π′′_{k} with v. ⊓ ⊔

Lemma 6 N has a path with exactly one occurrence of r_{1}, none of t_{1}, and infinitely many occurrences of t_{2}.

Proof Let π be the path found by Lemma 5. By Lemma 3 this path is embellished by a complete path π′, that thus has no occurrences of r_{1} and infinitely many of r_{2}. By Requirement 2 π′ has infinitely many occurrences of t_{2}, and by Requirement 3 it has no occurrences of t_{1}. By Requirement 1 π′ is r_{1}-enabled. Let w be a transition labelled r_{1} that is on π is continuously enabled from position k onwards. By Lemma 1 N has a path π ⊕_{k} w, obtained from π′ by inserting transition w in position k. That path has exactly one occurrence of r_{1}, none of t_{1}, and infinitely many of t_{2}. ⊓ ⊔

Lemma 7 N has a t_{1}-enabled path with infinitely many occurrences of t_{2}.

Proof Let π be the path found by Lemma 6. We build a sequence π_{i} of paths in N that all embellish π and do not contain t_{1}, such that, for all i, π_{i+1} is less incomplete than π_{i} and the first 2i transitions of π_{i} and π_{i+1} are the same. Since the π_{i} embellish π, they have exactly one occurrence of r_{1}, and infinitely many of t_{2}. Moreover, by Requirement 2, none of the π_{i} can be complete.

We start by taking π_{0} to be π. If at any point we hit a path π_{i} that is t_{1}-enabled, our work is done. Otherwise, given the (k, n)-incomplete path π_{i}, for some k and n, pick a witness w of the (k, n)-incompleteness of π_{i} and take π_{i+1}:=π_{i}⊕_{k+2i}w. This path exists by Lemma 1, since t is continuously enabled from position k onwards, and hence also from position k + 2i onwards. Note that ℓ(w) ≠ t_{1}, since π_{i} is not t_{1}-enabled. Hence π_{i+1} does not contain t_{1}. By construction π_{i+1} embellishes π_{i} and hence π. By Lemma 2 π_{i+1} is less incomplete than π_{i}. Moreover, the first 2i transitions of π_{i} and π_{i+1} are the same.

If at no point we hit a path π_{i} that is t_{1}-enabled, let ρ := lim_{i→∞} π_{i}. Exactly as in the proof of Lemma 3 it follows that ρ is complete and embellishes π. Since t_{1} does not occur on any of the π_{i}, it does not occur on ρ. However, r_{1} does occur on ρ, since it occurred on π. This is in contradiction with Requirement 2. Therefore, the assumption that at no point we hit a path π_{i} that is t_{1}-enabled must be wrong. ⊓ ⊔

Proof of Theorem 3 Let π be the path found in Lemma 7. It must have a finite prefix π′ ending with an occurrence of t_{2}, such that a transition w labelled t_{1} is enabled it the last state of π′. Extending π′ with w yields a finite path of N violating Requirement 4. ⊓ ⊔ 17 An Operational Petri Net Semantics of CCS

This section presents an operational Petri net semantics of CCS^{!}, following Degano, De Nicola & Montanari [19]. It associates a Petri net [[P]] with each CCS^{!} expression P. We establish that this Petri net is safe, all its reachable marking are finite, and there are no transitions u with ^{•}u = ∅; hence it is one of the nets considered in Section 15. In Section 18 we will show that if a CCS^{!} expression F satisfies the four requirements of Theorem 1 then the Petri net [[F]] satisfies the four requirements of Theorem 3. As a result, Theorem 1 will follow from Theorem 3.

The standard operational semantics of CCS^{!}, presented in Section 8, yields one big labelled transition system for the entire language. Each individual CCS^{!} expression P appears as a state in this LTS. If desired, a process graph—an LTS enriched with an initial state—for P can be extracted from this system-wide LTS by appointing P as the initial state, and optionally deleting all states and transitions not reachable from P. In the same vein, an operational Petri net semantics yields one big Petri net for the entire language, but without an initial marking. We call such a Petri net unmarked. Each process P ∈ T_{CCS^{!}} corresponds to a marking dec(P) of that net. If desired, a Petri net for P can be extracted from this system-wide net by appointing dec(P) as its initial marking, and optionally deleting all places and transitions not reachable from dec(P).

The set G_{CCS^{!}} of places in the net—the grapes of [19]—is the smallest set including:

A  agent identifier
α.P prefixing  ∑_{i∈I} P_{i} choice  μ\a restriction
μ| left parallel component  |μ  right component  μ[f] relabelling

for A∈K, α∈Act, P, P_{i} ∈T_{CCS^{!}}, a∈H , μ∈G_{CCS^{!}}, index sets I, and relabellings f. The mapping dec : T_{CCS^{!}} → P(G_{CCS^{!}}) decomposing a process expression into a set of grapes is inductively defined by:

\begin{matrix}dec(α.P)  = & \{α.P \} & dec(A) = & \{A\} \\ dec(∑_{i∈I} P_{i}) = & \{∑_{i∈I} P_{i}\} & dec(P |Q) = & dec(P)| ∪ |dec(Q) \\ dec(P \a)  = & dec(P)\a & dec(P [f]) = & dec(P)[f] \end{matrix}

Here H[f], H\a, H| and |H are understood element by element; e.g. H[f] = {μ[f] | μ ∈ H}. Moreover the binding is important, meaning that (|H)| ≠ |(H|).

We construct the unmarked Petri net (S, T, F, ℓ) of CCS^{!} with S := G_{CCS^{!}}, specifying the triple (T, F, ℓ) as a ternary relation → ⊆ IN^{S} ×Act×IN^{S}. An element H ⟶^{α} J of this relation denotes a transition u ∈ T with ℓ(u) = α such that ^{•}u = H and u^{•} = J. The transitions H ⟶^{α} J are derived from the rules of Table 2.

Henceforth, we write M [α⟩ M′, for markings M, M′ ∈ IN^{G_{CCS^{!}}} and α ∈ Act, if there exists a transition u with M[u⟩M′ and ℓ(u) = α. In that case M = H + K and M′ = J + K for multisets of places H, J, K : G_{CCS^{!}} → IN with H ⟶^{α} J.

The following theorem says that function dec is a strong bisimulation ([45]) between the LTS and the unmarked Petri net of CCS^{!}. Since markings of the form dec(R) are plain sets (rather than multisets), it also follows that the Petri net of each CCS^{!} expression is safe.

Theorem 4 If R ⟶^{α} R′ for R, R′ ∈ T_{CCS^{!}} and α ∈ Act then dec(R) [α⟩ dec(R′). Moreover, if dec(R)[α⟩M then there is a R′∈T_{CCS^{!}} with R ⟶^{α} R′ and dec(R′)=M.

\begin{matrix}\{α.P \} ⟶^{α} dec(P) & \frac{(dec(P_{j})−K) ⟶^{α} J}{\{∑_{i∈I} P_{i}\} ⟶^{α} J + K} (j ∈ I, K ≤ dec(P_{j})) \\ \frac{H ⟶^{α} J}{H| ⟶^{α} J|} & \frac{H ⟶^{a} J K ⟶^{ā} L}{H| + |K ⟶^{τ} J| + |L} & \frac{H ⟶^{α} J}{|H ⟶^{α} |J} \\ \frac{H ⟶^{α} J}{H\a ⟶^{α} J\a} (a ≠ α ≠ ā) & \frac{H ⟶^{α} J}{H[f] ⟶^{f(α)} J[f]} & \frac{(dec(P)−K) ⟶^{α} J}{\{A\} ⟶^{α} J + K} (\begin{matrix}A =^{def} P \\ K≤dec(P) \end{matrix}) \end{matrix}

Table 2 Operational Petri net semantics of CCS^{!}

Proof The first statement follows by induction on the derivability of the transition R ⟶^{α} R′ from the rules of Table 1. We only spell out two representative cases; the others are similar or straightforward.

– Suppose P |Q ⟶^{α} P′|Q because P ⟶^{α} P′. By induction dec(P) [α⟩ dec(P′). Hence dec(P) = H + K and dec(P′) = J + K for (multi)sets H, J, K ⊆ G_{CCS^{!}} with H ⟶^{α} J. By Table 2 we obtain H| ⟶^{α} J|. Hence

dec(P |Q) = dec(P)| + |dec(Q)
= H| + K| + |dec(Q)
[α⟩ J| + K| + |dec(Q)
= dec(P′)| + |dec(Q)
= dec(P′|Q) .

– Suppose A =^{def} P and A ⟶^{α} P′ since P ⟶^{α} P′. By induction dec(P) [α⟩ dec(P′). Hence dec(P) = H + K and dec(P′) = J + K for sets H, J, K ⊆ G_{CCS^{!}} with

dec(P)−K = H ⟶^{α} J. By Table 2, dec(A) = {A} ⟶^{α} J + K = dec(P′).

The second statement can be reformulated as

if (dec(R)−K) ⟶^{α} J with K ≤ dec(R)

then there is a R′ ∈ T_{CCS^{!}} with R ⟶^{α} R′ and dec(R′) = J+K.

for R ∈T_{CCS^{!}} and K, J : G_{CCS^{!}} → IN. We prove it by induction on the derivability of the transition dec(P)−K ⟶^{α} J from the rules of Table 2.

– Suppose dec(R)−K = {α.P } ⟶^{α} dec(P). Since the only set dec(R) containing α.P is {α.P }, we have K = ∅, J = dec(P) and R = α.P. Take R′ := P.

– Suppose dec(R) − K′ = H[f] ⟶^{f(α)} J[f] because H ⟶^{α} J. Then R must have the form P [f], so that dec(R) = dec(P)[f], and K′ must have the form K[f]. Thus dec(P) − K = H ⟶^{α} J, and by induction there is a P′ ∈ T_{CCS^{!}} with P ⟶^{α} P′ and dec(P′) = J + K. By Table 1, R = P [f] ⟶^{α} P′[f]. Moreover, dec(P′[f]) = dec(P′)[f] = J[f] + K[f] = J[f] + K′.

– The case for restriction proceeds likewise.

– Suppose dec(R) − K′ = H| ⟶^{α} J| because H ⟶^{α} J. Then R must have the form P |Q, and K′ = (dec(P)| − H|) + |dec(Q) = K| + |dec(Q), where K := dec(P) − H. Thus dec(P) − K = H ⟶^{α} J, so by induction there is a P′ ∈T_{CCS^{!}} with P ⟶^{α} P′ and dec(P′)=J +K. By Table 1, R = P |Q ⟶^{α} P′|Q. Moreover, dec(P′|Q) = dec(P′)| + |dec(Q) = J| + K| + |dec(Q) = J| + K′.

– Suppose dec(R)−K′ = H|+|K ⟶^{τ} J|+|L because H ⟶^{a} J and K ⟶^{ā} L. Then R has the form P |Q, and K′ = (dec(P)| − H|) + (|dec(Q) − |J) = K_{1}| + |K_{2},

where K_{1} := dec(P) − H and K_{2} := dec(Q) − J. Thus dec(P) − K_{1} = H ⟶^{a} J

and dec(Q) − K_{2} = J ⟶^{ā} L, so by induction there are P′, Q′ ∈ T_{CCS^{!}} with

P ⟶^{a} P′, dec(P′) = J + K_{1}, Q ⟶^{ā} Q′ and dec(Q′) = L + K_{2}. By Table 1,

R = P |Q ⟶^{τ} P′|Q′. Moreover, dec(P′|Q′) = dec(P′)| + |dec(Q′) = J| + K_{1}| +

|L + |K_{2} = J| + |L + K′.

– The case for the last rule for parallel composition follows by symmetry.

– Suppose dec(R) − K′ = {∑_{i∈I} P_{i}} ⟶^{α} J + K because (dec(P_{j})−K) ⟶^{α} J for

some j ∈I. Since the only set dec(R) containing ∑_{i∈I} P_{i} is {∑_{i∈I} P_{i}}, we have K′ = ∅ and R = ∑_{i∈I} P_{i}. By induction, there is a P′_{j} ∈ T_{CCS^{!}} with P_{j} ⟶^{α} P′_{j}

and dec(P′_{j}) = J+K. By Table 1, R = ∑_{i∈I} P_{i} ⟶^{α} P′_{j}.

– The case for recursion (agent identifiers) goes likewise. ⊓ ⊔

A trivial induction shows that there are no transitions without preplaces. The following lemma implies that all reachable markings are finite, so that the Petri nets of CCS^{!} expressions have all the properties of nets imposed in Section 15.

Lemma 8 For any P ∈ T_{CCS^{!}} the set dec(P) is finite.

Proof A straightforward induction. ⊓ ⊔

The above operational Petri net semantics of CCS has the disadvantage that initial concurrency in expressions of the form ∑_{i∈I} P_{i} or A is not represented [19]. Although this Petri net semantics matches the LTS semantics of CCS up to strong (interleaving) bisimilarity—and thereby also the standard denotational Petri net semantics of CCS-like operators [30]—, it does not match the standard denotational Petri net semantics up to semantic equivalences that take concurrency explicitly into account. For this reason Olderog [49] provides an alternative operational Petri net semantics that is more accurate in this sense. However, the work of Olderog does not generalise in a straightforward way to the infinite sum construct of CCS, and to unguarded recursion. In fact, a safe Petri net that accurately models the concurrent behaviour of the CCS process ∑_{i∈IN}(a_{i}.0|b_{i}.0) would need an uncountable initial marking, and hence falls outside the class of nets we handle in Section 15. Since the accurate modelling of concurrency is not essential for this paper, we therefore use the semantics of [19].

18 Fair Schedulers Cannot be Rendered in CCS^{!}—Proof

Lemma 9 The mapping dec : T_{CCS^{!}} → P(G_{CCS^{!}}) is injective.

Proof A straightforward induction on the structure of the elements in T_{CCS^{!}}. ⊓ ⊔

Lemma 10 Let P ∈ T_{CCS^{!}}. For any path π = dec(P)u_{1}M_{1}u_{2}M_{2}u_{3} … in the unmarked Petri net of CCS^{!} there is a unique path π̂ = P ⟶^{α_{1}} P_{1} ⟶^{α_{2}} P_{2} ⟶^{α_{3}} … of the same (finite or infinite) length in the LTS of CCS^{!} with dec(P_{i}) = M_{i} and ℓ(u_{i}) = α_{i} for all i.

Proof A straightforward induction on i, using Theorem 4 and Lemma 9. ⊓ ⊔ The following observations are based directly on Table 2 and the definition of dec.

Observation 1 Let dec(P |Q) [u⟩ M. Then M has the form dec(P′|Q′) and either – Q=Q′ and dec(P) [v⟩ dec(P′) for a v∈T with ℓ(v)=ℓ(u), ^{•}u=^{•}v| and u^{•} =v^{•}|,

– P =P′ and dec(Q) [w⟩ dec(Q′) for a w∈T with ℓ(w)=ℓ(u),^{•}u=|^{•}w and u^{•}=|w^{•},

– or dec(P) [v⟩ dec(P′) and dec(Q) [w⟩ dec(Q′) for v, w ∈ T with ℓ(v) = c ∈ H , ℓ(w) = c̄, ^{•}u =^{•}v| + |^{•}w and u^{•} = v^{•}| + |w^{•}.

For each such transition u, the transitions v and w discovered above are called the left- and right-projections of u, respectively, when they exist. Hence any path π starting from a marking dec(P |Q) can be uniquely decomposed into a path π_{1} starting from dec(P) and a path π_{2} starting from dec(Q), notation π ⇛ π_{1}|π_{2}. The path π_{1} fires all existing left-projections of the transitions in π, in order, and π_{2} its right-projections.

Lemma 11 If π ⇛ π_{1}|π_{2} and π_{1} is α-enabled, then so is π.

Proof Let π_{1} = M′_{0}v_{1}M′_{1}v_{2}M′_{2}v_{3} … be α-enabled. Then there is a h ≥ 0 and a transition v with ℓ(v) = α such that M′_{h}[v⟩ and ^{•}v ∩ ^{•}v_{i} = ∅ for all i > h. Let π = M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} . . .. Let k ≥ h be such that v_{0} … v_{h} is the sequence of existing left-projections of u_{1} … u_{k}. The marking M_{k} has the form dec(P_{k}|Q_{k}) = dec(P_{k})| ·^{∪} |dec(Q_{k}) with M′_{h} = dec(P_{k}). Since ^{•}v ≤ dec(P_{k}), by Table 2 there exists a transition v′ with ℓ(v′) = α and ^{•}v′ = ^{•}v| ≤ dec(P_{k})| ≤ M_{k}. So M_{k}[v′⟩. Moreover, since ^{•}v ∩^{•}v_{i} = ∅ for all i > h we have ^{•}v′ ∩^{•}u_{i} = ∅ for all i > k. It follows that π is α-enabled. ⊓ ⊔

Lemma 12 If π ⇛ π_{1}|π_{2}, π_{1} is c-enabled and π_{2} is c̄-enabled, for some c ∈ H , then π is τ-enabled.

Proof Let π = M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} . . .. Since π ⇛ π_{1}|π_{2}, each marking M_{i} has the form dec(P_{i}|Q_{i}) = dec(P_{i})| ·^{∪} |dec(Q_{i}). By the same reasoning as in the previous proof, there is a k_{1} ≥ 0 and a transition v with ℓ(v) = c such that ^{•}v ≤ dec(P_{i}) and ^{•}v| ∩ ^{•}u_{i} = ∅ for all i ≥ k_{1}. Likewise, there is a k_{2} ≥ 0 and a transition w with ℓ(w) = c̄ such that ^{•}w ≤ dec(Q_{i}| and |^{•}w ∩^{•}u_{i} = ∅ for all i ≥ k_{2}.

Let k = max(k_{1}, k_{2}). By the fourth rule of Table 2 there is a transition u with ℓ(u)=τ and ^{•}u=^{•}v|+|^{•}w≤M_{k} and ^{•}u∩^{•}u_{i} =∅ for all i > k. So π is τ-enabled. ⊓ ⊔

Observation 2 Let dec(P \c) [u⟩ M. Then M has the form dec(P′\c) and we have dec(P) [v⟩ dec(P′) for a v ∈ T with ℓ(v) = ℓ(u), ^{•}u =^{•}v\c and u^{•} = v^{•}\c.

For each such transition u, the transition v discovered above is called the projection of u. Hence any path π starting from a marking dec(P)\c can be uniquely decomposed into a path π′ starting from dec(P), notation π ⇛ π′\c. The path π′ fires all the projections of the transitions in π, in order.

Lemma 13 If π ⇛ π′\c and π′ is α-enabled with c ≠ α ≠ c̄, then π is α-enabled.

Proof Let π′ = M′_{0}v_{1}M′_{1}v_{2}M′_{2}v_{3} … be α-enabled. Then there is a k ≥ 0 and a transition v with ℓ(v) = α such that M′_{k}[v⟩ and ^{•}v ∩ ^{•}v_{i} = ∅ for all i > k. Let π = M_{0}u_{1}M_{1}u_{2}M_{2}u_{3} . . .. The marking M_{k} has the form dec(P_{k}\c) = dec(P_{k})\c with M′_{k} = dec(P_{k}). Since ^{•}v ≤ dec(P_{k}) and c ≠ α ≠ c̄, by Table 2 there exists a transition v′ with ℓ(v′) = α and ^{•}v′ = ^{•}v\c ≤ dec(P_{k})\c = M_{k}. So M_{k}[v′⟩. Moreover, since ^{•}v ∩^{•}v_{i} = ∅ for all i > k we have ^{•}v′ ∩^{•}u_{i} = ∅ for all i > k. It follows that π is α-enabled. ⊓ ⊔ Observation 3 Let dec(P [f]) [u⟩ M. Then M has the form dec(P′[f]) and we have dec(P) [v⟩ dec(P′) for a v ∈ T with f(ℓ(v)) = ℓ(u), ^{•}u =^{•}v[f] and u^{•} = v^{•}[f].

For each such transition u, the transition v discovered above is called a projection of u—it need not be unique. Hence any path π starting from a marking dec(P)\c can be decomposed into a path π′ starting from dec(P), notation π ∈ π′[f]. The path π′ fires projections of the transitions in π, in order.

Lemma 14 If π ∈ π′[f] and π′ is α-enabled, then π is f(α)-enabled.

Proof Just as the proof of Lemma 13. ⊓ ⊔

Observation 4 Let π be a path in the unmarked Petri net of CCS^{!}. Then π ⇛ π_{1}|π_{2} implies that π̂_{1}|π̂_{2} is a decomposition of π̂ (c.f. Page 12). Likewise, if π ⇛ π′\c or π ∈ π′[f] then π′ is a decomposition of π̂.

Proposition 1 Let π be a path in the unmarked Petri net of CCS^{!}. If Y includes all actions α ∈ Act for which π is α-enabled, and Y ⊆ H , then π̂ is Y-just.

Proof Define a path η in the LTS of CCS^{!} to be Y-just_{en}, for Y ⊆ Act, if η has the form π̂ for π a path in the unmarked Petri net of CCS^{!}, and Y includes all actions α ∈ Act for which π is α-enabled. Note that if η is Y-just_{en}, it is also Y′-just_{en} for any Y ⊆ Y′ ⊆ Act. We show that the family of predicates Y-justness_{en}, for Y ⊆ H, satisfies the five requirements of Definition 1.

– Let π̂ be a finite Y-just_{en} path. Suppose the last state Q of π̂ admits an action α ∉ Y, Then, using Theorem 4, the last marking dec(Q) of π enables a transition labelled α. Thus π is α-enabled, contradicting the Y-justness_{en} of π.

– Suppose π̂ is a Y-just_{en} path of a process P |Q with Y ⊆H. Then Y includes all actions α ∈ Act for which π is α-enabled. Let π_{1} and π_{2} be the paths such that π ⇛ π_{1}|π_{2}. By Observation 4 π̂ can be decomposed into the paths π̂_{1} of P and π̂_{2} of Q. Let X ⊆ Act be the set of actions α for which π_{1} is α-enabled, and let Z ⊆ Act be the set of actions α for which π_{2} is α-enabled. By definition, π̂_{1} is X-just_{en} and π̂_{2} is Z-just_{en}. If π_{1} is α-enabled then π is α-enabled by Lemma 11. This implies that X ⊆ Y. In the same way it follows that Z ⊆ Y. Now suppose X ∩ Z̄ ≠ ∅. Then π_{1} is cenabled and π_{2} is c̄-enabled, for some c ∈ H . So, by Lemma 12, π is τ-enabled, in contradiction with τ ∉ Y ⊆ H . We therefore conclude that X ∩ Z̄ = ∅.

– Suppose π̂ is a Y-just_{en} path of a process P \c. Then Y includes all actions α ∈ Act for which π is α-enabled. Let π′ be the path such that π ⇛ π′\c. By Observation 4 π̂ is a decomposition of the path π′ of P. Let X ⊆ Act be the set of actions α for which π′ is α-enabled. If π′ is α-enabled with c ≠ α ≠ c̄ then π is α-enabled by Lemma 13. This implies that X \ {c, c̄} ⊆ Y and hence X ⊆ H . It follows that π′ is X-just_{en}, and hence Y ∪{c, c̄}-just_{en}.

– Suppose π̂ is a Y-just_{en} path of a process P [f]. Then Y includes all actions α ∈ Act for which π is α-enabled. Let π′ be a path such that π ∈ π′[f]. By Observation 4 π̂ is a decomposition of the path π′ of P. Let X ⊆ Act be the set of actions α for which π′ is α-enabled. If π′ is α-enabled then π is f(α)-enabled by Lemma 14. This implies that f(X) ⊆ Y. It follows that π′ is X-just_{en}, and hence f^{−1}(Y)-just_{en}.

– Suppose π′ is a suffix of an Y-just_{en} path π. Then Y includes all actions α∈Act for which π is α-enabled, and thus all α for which π′ is α-enabled. Hence π′ is Y-just_{en}.

Since Y-justness is the largest family of predicates that satisfies those requirements, Y-justness_{en} implies Y-justness. ⊓ ⊔

Corollary 1 Let π be a path starting from dec(P) in the unmarked Petri net of CCS^{!}. If π is complete, then so is π̂. Moreover, if π̂ is a-enabled, for a ∈ H , then so is π. ⊓ ⊔

Proof of Theorem 1 Suppose there does exist a CCS^{!} expression F as considered in Theorem 1. Then it suffices to show that [[F]] is a net N as considered in Theorem 3. Thus, we show that [[F]] satisfies the four properties of Theorem 3.

1. Let π be a complete path of [[F]] that has finitely many occurrences of r_{i}. By Lemma 10 π̂ is a path of F that has finitely many occurrences of r_{i}. By Corollary 1 it is complete. By Requirement 1 of Theorem 1, π̂ is r_{i}-enabled. So by Corollary 1, π is r_{i}-enabled.

2. Let π be a complete path of [[F]]. Then π̂ is a complete path of [[F]]. By Requirement 2 of Theorem 1, on π̂ each r_{i} is followed by a t_{i}. Using Lemma 10, the same holds for π.

3. Let π be a finite path of [[F]]. Then π̂ is a path of F. By Requirement 3 of Theorem 1, on π̂, and thus on π, are no more occurrences of t_{i} than of r_{i}.

4. Let π be a path of [[F]], featuring two occurrences of t_{i} and t_{j} (i, j ∈ {1, 2}). These occurrences also occur on π̂. By Requirement 4 of Theorem 1, an action e occurs between them. ⊓ ⊔

19 Concluding Remarks

This paper presented a simple fair scheduler—one that in suitable variations occurs in many distributed systems—of which no implementation can be expressed in CCS. In particular, Dekker’s and Peterson’s mutual exclusion protocols cannot be rendered correctly in CCS. These conclusions remain true if CCS is extended with progress and certain fairness assumptions, namely justness as presented in this paper. However, as shown in [14], it is possible to correctly render Dekker’s protocol—and thereby a fair scheduler—in CCS enriched with a stronger fairness assumption. We argue, however, that such fairness assumptions should not be made lightly, as in certain contexts they allow the derivation of false results.

It does not appear hard to extend CCS with an operator that enables expressing this fair scheduler without relying on a fairness assumption. In [29] for instance we give a simple specification of a fair scheduler in an extension of CCS with broadcast communication. In [15] it is shown that it suffices (for the correct specification of Dekker’s algorithm) to extend a CCS-like process algebra with non-blocking reading actions. A priority mechanism [12] would also be sufficient.

Let ▷ for instance be a +-like operator that schedules an action from its left argument if possible, and otherwise runs its right argument. Then F̂_{1}, with

F_{1} =^{def} (r_{1}.t_{1}.e.F_{2}) ▷ (τ.F_{2}) and F_{2} =^{def} (r_{2}.t_{2}.e.F_{1}) ▷ (τ.F_{1})

appears to be a fair scheduler. Here ˆ · is the CCS-context specified in Section 13.

F is basically a round-robin scheduler which checks whether r_{1} is enabled; if so, it performs the sequence r_{1}.t_{1}.e; if not, it does an internal action and tries to perform r_{2}.

An interesting question is what kind of extension of CCS is needed to enable specifying all processes of this kind. It appears that the formalism CCS+LTL that we employed in Section 11 to specify our fair scheduler can be used to specify a wide range of similar systems. Such a specification combines a CCS specification with a fairness component, consisting of a set of LTL formulas that narrows down the complete paths of the specified process. An intriguing challenge is to find an extension of CCS, say by means of extra operators, that makes the fairness component redundant, i.e. an extension such that any CCS+LTL process can be expressed in the extended CCS without employing a fairness component.

For certain properties of the form (⋁_{i} GFa_{i}) ⇒ (⋁_{j} GFb_{j}) where the a_{i} and b_{i} are action occurrences—hence for specific strong fairness properties—one can define a fairness operator that transforms a given LTS into a LTS that satisfies the property [55]. This is done by eliminating all the paths that do not satisfy the property via a carefully designed parallel composition. The fairness operator can be expressed in a variant of the process algebra CSP. The question above asks whether something similar can be done, in a more expressive process algebra, for arbitrary LTL properties, or perhaps for a larger class of fairness properties.

Acknowledgements We gratefully thank the anonymous referees. Their reports showed deep insights in the material, and helped a lot to improve the quality of the paper. In particular, the link between our fair scheduler and Peterson’s mutual exclusion protocol was made by one of the referees.

References

1. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Modelling mutual exclusion algorithms. In: Reactive Systems: Modelling, Specification and Verification, pp. 142–158. Cambridge

University Press (2007). doi:10.1017/CBO9780511814105.008

2. Apt, K.R., Francez, N., Katz, S.: Appraising fairness in languages for distributed programming. Distributed Computing 2(4), 226–241 (1988). doi:10.1007/BF01872848

3. Baeten, J.C.M., Bergstra, J.A.: Discrete time process algebra. Formal Aspects of Computing 8(2), 188–208 (1996). doi:10.1007/BF01214556

4. Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: On the consistency of Koomen’s fair abstraction rule. Theoretical Computer Science 51(1/2), 129–176 (1987). doi:10.1016/

0304-3975(87)90052-1

5. Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Ready-trace semantics for concrete process algebra with the priority operator. Computer Journal 30(6), 498–506 (1987). doi:10.

1093/comjnl/30.6.498

6. Baeten, J.C.M., Luttik, B., van Tilburg, P.: Reactive Turing machines. In: O. Owe, M. Steffen, J.A. Telle (eds.) Fundamentals of Computation Theory, pp. 348–359 (2011). doi:10.

1007/978-3-642-22953-4_30

7. Bergstra, J.A., Klop, J.W.: Algebra of communicating processes. In: J.W. de Bakker, M. Hazewinkel, J.K. Lenstra (eds.) Mathematics and Computer Science, CWI Monograph 1, pp. 89–138. North-Holland (1986)

8. Bergstra, J.A., Klop, J.W.: Verification of an alternating bit protocol by means of process algebra. In: W. Bibel, K.P. Jantke (eds.) Mathematical Methods of Specification and Synthesis of Software Systems ’85, LNCS, vol. 215, pp. 9–23. Springer (1986). doi:10.

1007/3-540-16444-8_1

9. Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks 14, 25–59 (1987). doi:10.1016/0169-7552(87)90085-7 10. Bouali, A.: Weak and branching bisimulation in Fctool. Research Report RR-1575, Inria-

Sophia Antipolis (1992). URL https://hal.inria.fr/inria-00074985/document

11. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984). doi:10.1145/828.833

12. Cleaveland, R., Lüttgen, G., Natarajan, V.: Priority in process algebra. In: J.A. Bergstra, A. Ponse, S.A. Smolka (eds.) Handbook of Process Algebra, chap. 12, pp. 711–765. Elsevier

(2001). doi:10.1016/B978-044482830-9/50030-8

13. Corradini, F., Di Berardini, M.R., Vogler, W.: Fairness of actions in system computations. Acta Informatica 43(2), 73–130 (2006). doi:10.1007/s00236-006-0011-2

14. Corradini, F., Di Berardini, M.R., Vogler, W.: Liveness of a mutex algorithm in a fair process algebra. Acta Informatica 46(3), 209–235 (2009). doi:10.1007/s00236-009-0092-9

15. Corradini, F., Di Berardini, M.R., Vogler, W.: Time and fairness in a process algebra with non-blocking reading. In: M. Nielsen, A. Kucera, P.B. Miltersen, C. Palamidessi, P. Tuma, F.D. Valencia (eds.) Theory and Practice of Computer Science (SOFSEM’09), LNCS, vol. 5404, pp. 193–204. Springer (2009). doi:10.1007/978-3-540-95891-8_20

16. Corradini, F., Vogler, W., Jenner, L.: Comparing the worst-case efficiency of asynchronous systems with PAFAS. Acta Informatica 38(11/12), 735–792 (2002). doi:10.

1007/s00236-002-0094-3

17. Costa, G., Stirling, C.: A fair calculus of communicating systems. Acta Informatica 21,

417–441 (1984). doi:10.1007/BF00271640

18. Costa, G., Stirling, C.: Weak and strong fairness in CCS. Information and Computation

73(3), 207–244 (1987). doi:10.1016/0890-5401(87)90013-7

19. Degano, P., De Nicola, R., Montanari, U.: CCS is an (augmented) contact free C/E system. In: M.V. Zilli (ed.) Mathematical Models for the Semantics of Parallelism, LNCS, vol. 280, pp. 144–165. Springer (1987). doi:10.1007/3-540-18419-8_13

20. Dijkstra, E.W.: Over de sequentialiteit van procesbeschrijvingen (1962 or 1963). URL

http://www.cs.utexas.edu/users/EWD/ewd00xx/EWD35.PDF. Circulated privately

21. Dijkstra, E.W.: Cooperating sequential processes. In: F. Genuys (ed.) Programming Languages: NATO Advanced Study Institute, pp. 43–112. Academic Press (1968)

22. Esparza, J., Bruns, G.: Trapping mutual exclusion in the box calculus. Theoretical Computer Science 153(1-2), 95–128 (1996). doi:10.1016/0304-3975(95)00119-0

23. Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Tech. Rep. 5513, NICTA (2013). Available at http://arxiv.org/abs/1312.7645

24. Francez, N.: Fairness. Springer (1986). doi:10.1007/978-1-4612-4886-6

25. Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: P.W. Abrahams, R.J. Lipton, S.R. Bourne (eds.) Principles of Programming Languages (POPL ’80), pp. 163–173. ACM (1980). doi:10.1145/567446.567462

26. van Glabbeek, R.J.: On specifying timeouts. In: L. Aceto, A.D. Gordon (eds.) Short Contributions from the Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond, ENTCS, vol. 162, pp. 112–113. Elsevier (2005). doi:10.1016/j.entcs.

2005.12.083

27. van Glabbeek, R.J.: Musings on encodings and expressiveness. In: B. Luttik, M.A. Reniers (eds.) Proceedings Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, EPTCS, vol. 89, pp. 81–98. Open Publishing Association (2012). doi:10.4204/EPTCS.89.7

28. van Glabbeek, R.J., Goltz, U., Schicke, J.W.: Abstract processes of place/transition systems. Information Processing Letters 111(13), 626–633 (2011). doi:10.1016/j.ipl.2011.

03.013

29. van Glabbeek, R.J., Höfner, P.: Progress, fairness and justness in process algebra. CoRR

abs/1501.03268 (2015). URL http://arxiv.org/abs/1501.03268

30. van Glabbeek, R.J., Vaandrager, F.W.: Petri net models for algebraic theories of concurrency. In: J.W.d. Bakker, A.J. Nijman, P.C. Treleaven (eds.) Parallel Architectures and Languages Europe (PARLE’97), Vol. II: Parallel Languages, LNCS, vol. 259, pp. 224–242.

Springer (1987). doi:10.1007/3-540-17945-3_13

31. Goldin, D.Q., Smolka, S.A., Attie, P.C., Sonderegger, E.L.: Turing machines, transition systems, and interaction. Information and Computation 194(2), 101–128 (2004). doi:10.

1016/j.ic.2004.07.002

32. Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Information and Computation 208(9), 1031–1053 (2010). doi:10.1016/j.ic.2010.

05.002

33. Groote, J.F., Ponse, A.: The syntax and semantics of μCRL. In: A. Ponse, C. Verhoef, S.F.M. van Vlijmen (eds.) Algebra of Communicating Processes ’94, Workshops in Computing, pp. 26–62. Springer (1995). doi:10.1007/978-1-4471-2120-6_2

34. Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabitilies. In: Real-Time Systems Symposium (RTSS ’90), pp. 278–287. IEEE Computer

Society (1990). doi:10.1109/REAL.1990.128759

35. Hennessy, M., Regan, R.: A process algebra for timed systems. Information and Computation 117(2), 221–239 (1995). doi:10.1006/inco.1995.1041

36. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)

37. Kindler, E., Walter, R.: Mutex needs fairness. Inf. Process. Lett. 62(1), 31–39 (1997).

doi:10.1016/S0020-0190(97)00033-1

38. Kleinrock, L.: Analysis of a time-shared processor. Naval Research Logistics Quarterly

11(1), 59–73 (1964). doi:10.1002/nav.3800110105

39. Lamport, L.: The temporal logic of actions. ACM Trans. Programming Languages and Systems 16(3), 872–923 (1994). doi:10.1145/177492.177726

40. Lauer, P.E., Torrigiani, P.R., Shields, M.W.: COSY - a system specification language based on paths and processes. Acta Informatica 12, 109–158 (1979). doi:10.1007/BF00266047

41. van Leeuwen, J., Wiedermann, J.: Beyond the Turing limit: Evolving interactive systems. In: L. Pacholski, P. Ruzicka (eds.) Theory and Practice of Informatics (SOFSEM ’01), LNCS, vol. 2234, pp. 90–109. Springer (2001). doi:10.1007/3-540-45627-9_8

42. Lehmann, D.J., Pnueli, A., Stavi, J.: Impartiality, justice and fairness: The ethics of concurrent termination. In: S. Even, O. Kariv (eds.) Automata, Languages and Programming (ICALP), LNCS, vol. 115, pp. 264–277. Springer (1981). doi:10.1007/3-540-10843-2_22

43. Lüttgen, G., Vogler, W.: A faster-than relation for asynchronous processes. In: K.G. Larsen, N. M. (eds.) Concurrency Theory (CONCUR ’01), LNCS, vol. 2154, pp. 262–276.

Springer (2001). doi:10.1007/3-540-44685-0_18

44. Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quarterly 2(3), 219–246 (1989). Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands

45. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

46. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part I + II. Information and Computation 100(1), 1–77 (1992). doi:10.1016/0890-5401(92)90008-4

47. Nagle, J.: On packet switches with infinite storage. RFC 970, Network Working Group

(1985). URL http://tools.ietf.org/rfc/rfc970.txt

48. Nagle, J.: On packet switches with infinite storage. IEEE Trans. Communications 35(4),

435–438 (1987). doi:10.1109/TCOM.1987.1096782

49. Olderog, E.-R..: Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship. No. 23 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1991)

50. Parrow, J.: Expressiveness of process algebras. ENTCS 209, 173–186 (2008). doi:10.1016/

j.entcs.2008.04.011

51. Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Let-

ters 12(3), 115–116 (1981). doi:10.1016/0020-0190(81)90106-X

52. Plotkin, G.D.: A powerdomain for countable non-determinism (extended abstract). In: M. Nielsen, E.M. Schmidt (eds.) Automata, Languages and Programming (ICALP ’82), LNCS, vol. 140, pp. 418–428. Springer (1982). doi:10.1007/BFb0012788

53. Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (FOCS ’77), pp. 46–57. IEEE (1977). doi:10.1109/SFCS.1977.32

54. Prasad, K.V.S.: A calculus of broadcasting systems. Science of Computer Programming

25(2-3), 285–327 (1995). doi:10.1016/0167-6423(95)00017-8

55. Puhakka, A., Valmari, A.: Liveness and fairness in process-algebraic verification. In: K.G. Larsen, M. Nielsen (eds.) Concurrency Theory (CONCUR’01), LNCS, vol. 2154, pp. 202–

217. Springer (2001). doi:10.1007/3-540-44685-0_14

56. Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. In: L. Kott (ed.) Automata, Languages and Programming (ICALP ’86), LNCS, vol. 226, pp. 314–323. Springer (1986). doi:10.1007/3-540-16761-7_81

57. Reisig, W.: Petri nets – an introduction. EATCS Monographs on Theoretical Computer Science, Volume 4. Springer (1985). doi:10.1007/978-3-642-69968-9

58. Vaandrager, F.W.: Expressiveness results for process algebras. In: J.W. de Bakker, W.P. de Roever, G. Rozenberg (eds.) Proceedings REX Workshop on Semantics: Foundations and Applications, LNCS, vol. 666, pp. 609–638. Springer (1993). doi:10.1007/

3-540-56596-5_49

59. Valmari, A., Setälä, M.: Visual verification of safety and liveness. In: M. Gaudel, J. Woodcock (eds.) Industrial Benefit and Advances in Formal Methods (FME’96), LNCS, vol. 1051, pp. 228–247. Springer (1996). doi:10.1007/3-540-60973-3_90

60. Vogler, W.: Efficiency of asynchronous systems, read arcs, and the MUTEX-problem. Theor. Comput. Sci. 275(1-2), 589–631 (2002). doi:10.1016/S0304-3975(01)00300-0

61. Walker, D.J.: Automated analysis of mutual exclusion algorithms using CCS. Formal Aspects of Computing 1(1), 273–292 (1989). doi:10.1007/BF01887209

62. Wegner, P.: Why interaction is more powerful than algorithms. Commununications of the ACM 40(5), 80–91 (1997). doi:10.1145/253769.253801