Paper dedicated to Jos Baeten, at the occasion of his retirement.

\begin{matrix}c \\ ◯ \end{matrix} R.J. van Glabbeek

This work is licensed under the

Creative Commons Attribution License.

Failure Trace Semantics for a Process Algebra with Time-outs

Rob van Glabbeek

Data61, CSIRO, Sydney, Australia School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

                                     rvg@cs.stanford.edu

This paper extends a standard process algebra with a time-out operator, thereby increasing its absolute expressiveness, while remaining within the realm of untimed process algebra, in the sense that the progress of time is not quantified. Trace and failures equivalence fail to be congruences for this operator; their congruence closure is characterised as failure trace equivalence.

1 Motivation

This work has four fairly independent motivations, in the sense that it aims to provide a common solution to four different problems. How it yields a solution to the last two of these problems is left for future work, however.

1.1 The passage of time in processes modelled as labelled transition systems

The standard semantics of untimed non-probabilistic process algebras is given in terms of labelled transition systems (LTSs), consisting of a set of states, with action-labelled transitions between them. The behaviour of a system modelled as a state in an LTS can be visualised as a token, starting in this initial state, that travels through the LTS by following its transitions. A question that has plagued me since I first heard of this model, in December 1984, is where exactly (and how) does time progress when this token travels: in the states, during the transitions, or maybe both?

In some sense this question is more of a philosophical than an practical nature. Process algebra has flourished, without any convincing answer to this question sitting in its way.

One reasonable attitude is that in untimed progress algebra we abstract from time, which makes the entire question meaningless. While this does make sense, I still desire seeing an untimed process as a special case of a timed process, one where any period of time that might be specified in a timed formalism is instantiated by a nondeterministic choice allowing any amount of time. Such a point of view would certainly assist in relating timed and untimed process algebras. It is from this perspective that my question is in need of an answer.

The common answer given by the process algebra community is that there is no need to model transitions that take time, for a durational transition can simply be modelled as a pair of instantaneous transitions with a time-consuming state in between. Here I follow this train of thought, and regard transitions as occurring instantaneously. This implies that time must elapse in states, if at all.

Now visualise a system reaching a state s in an LTS, that has a single outgoing transition u leading to a desired goal state. Assume, moreover, that this transition cannot be blocked by the environment. A fundamental assumption made in most process algebraic formalisms is that the system will eventually reach this goal state, that is, that it will not stay forever in state s. In [17] this assumption is called progress. Without it it is not possible to prove meaningful liveness properties [24], saying that “something [good] must eventually happen”.

When our LTS would model all activities of the represented system, it is hard to believe how the system, upon reaching state s, comes to a rest, spends a finite amount of time in state s while doing nothing whatsoever, and then suddenly, and without any clear reason, takes the transition to the desired goal state. It appears more plausible that if we allow the system to stay in state s for a finite amount of time, it can (and perhaps even must) stay there for an infinite amount of time.

The way out of this paradox is that our system, being discrete, necessarily abstracts from a lot of activity. The abstracted activity that is relevant for the visit of the system to state s must be some durational activity, an amount of work to be done, that for a while sits in the way of taking transition u. As soon as that work is done, and nothing further sits in the way, transition u takes place.

In this paper this abstracted activity is made explicit, in the shape of a time-out transition ⟶^{t}. Similar to the internal transition ⟶^{τ}, modelling the occurrence of an instantaneous action from which we abstract, the time-out transition ⟶^{t} models the end of a time-consuming activity from which we abstract. A state s in which the system is supposed to spend some time—a positive and finite, but otherwise unquantified amount—can now be modelled as a pair of states s_{1} and s_{2} with a time-out transition between them; the outgoing transitions of s are then moved to s_{2}. Time will be spent in state s_{1} only, where some abstracted time-consuming activity takes place. The only thing in the model that testifies to this activity is the time-out transition s_{1} ⟶^{t} s_{2}, that is guaranteed to occur as soon as the time-consuming work is done. Immediately afterwards, the system will take one of the outgoing transitions of s_{2}, unless they are all blocked by the environment in which our reactive system is running.

An alternative proposal on how systems spend finite amounts of time in states is essentially due to Milner [26]. It says that the states in an LTS model reactive systems that merely react on stimuli from the environment. This reaction may be instantaneous, but the environment itself takes time between issuing stimuli. Usually, each outgoing transition of a state s is labelled by a visible action a, and only when the environment chooses to synchronise on channel a will such a transition occur. Normally, it may take a while before the environment is ready to synchronise with any outgoing transition of state s, and this is exactly what accounts for the time spent in state s. A special case occurs when state s has an outgoing τ-transition. Since such transitions do not require synchronisation with the environment, it appears that the represented system is not allowed to linger in such a state.

The current paper combines the time-out transitions proposed above with the reactive viewpoint adopted by Milner. So any time the system spends in a state is either due to the environment not allowing an outgoing transition, or the system waiting for a time-out transition to occur (or both).

Admitting time-out transitions in an LTS not only allows the specification of states in which the system spends a positive but finite amount of time, as described above; it also allows the specification of states in which the system spends no time whatsoever, unless forced by the environment—this is achieved by not using any time-out transitions leaving that state. Moreover, we can model states s in which some outgoing transitions have to wait for a time-out to occur, and others do not.^{1} This is done by modelling s as s_{1} ⟶^{t} s_{2}, were the outgoing transitions of s_{2} have to wait for the time-out, and the ones of s_{1} do not. In that case the time-out will occur only if the environment fails to synchronise in time with any of the outgoing transitions from s_{1}. This implements a priority mechanism, in which from the system’s perspective the outgoing transitions of s_{1} have priority over the ones of s_{2}.

1Enriching the model with this kind of of states is not merely a luxury in which I indulge; such states arise naturally through parallel composition. In my interleaving semantics it will turn out that t.a∥t.b ⟶^{t} a∥t.b = a.t.b + t.(a.b + b.a).

1.2 Failure trace semantics

In [9, 7] I classified many semantic equivalences on processes, and proposed testing scenarios for these semantics in terms of button-pushing experiments on reactive and generative machines, such that two processes are inequivalent iff their difference can be detected through the associated testing scenario. Figure 1 shows the various equivalences in the absence of internal transitions τ (or t). For equivalences such as simulation equivalence (point S in Figure 1), or bisimilarity (B), the testing scenarios require a replication facility, allowing the experimenter to regularly make copies of a system in its current state, and expose each of those copies to further tests. This facility could be regarded as fairly unrealistic, in the sense that one would not expect an actual implementation of such a facility to be available. When one takes this opinion, (bi)similarity makes distinctions between processes that are not well justified. Likewise, readiness equivalence (R^{∗}) has a testing scenario that allows us, in certain states, to see the menu of all available actions the environment (= tester) can synchronise with. It may be deemed unrealistic to assume such a menu to be generally available. Or for systems in which such a menu is available, one might say that it has to be specified as part of the system behaviour, so that we do not need it explicitly in a testing scenario. When one takes this opinion, readiness equivalence, and its finer variants, also makes distinctions between processes that are not well justified.

Following this line of reasoning, the finest (= most discriminating) semantic equivalence that does have a realistic testing scenario is failure trace semantics (F T). Its testing scenario allows the tester to control which actions may take place (are available for synchronisation) and which are not. It also allows the tester to record sequences of actions that take place during a run of the system, interspersed with periods of idling, where each idle period is annotated with the set of actions made available for synchronisation by the tester during this period. Such a sequence is a failure trace, and two systems are distinguished iff one has a failure trace that the other has not. In Figure 1 two variants of failure trace equivalence are recorded (F T^{∗} and F T^{∞}), depending on whether one only allows finite observations, leading to partial failure traces, or also infinite ones.

Failures semantics (F^{∗}) is the default semantics of the process algebra CSP [4, 23]. It is coarser than failure trace semantics, in the sense that it makes more identifications. Its testing scenario is the variant of the one for failure trace semantics described above, in which the environment/tester cannot alter the set of allowed actions once the system idles (= reaches a state of deadlock). Thus, when two systems are failures inequivalent, one can think of an environment such that when placed in that environment one of them deadlocks and the other does not. An important insight is that such an environment can always be built from some basic process algebraic operators. So when P are Q are failures inequivalent, there is process algebraic context C[ ], such that C[P] has a deadlock which C[Q] has not (or vise versa).

Given that two processes P are Q are failure trace inequivalent iff, under a realistic testing scenario, an environment can see their difference, one would expect, analogously to the situation with failures semantics, that one can build an environment from process algebraic operators that exploits that difference, i.e., that one can find a context C[ ], such that the difference between C[P] and C[P] becomes much more tangible. However, standard process algebras lack the expressiveness to achieve this.

So far the search for suitable process algebraic operators that allow us to exploit the difference between failure trace inequivalent processes has not born fruit. Most operators fall short in doing so, whereas others have too great a discriminating power. A prime example of the latter is the priority operator of Baeten, Bergstra & Klop [2]. It allows building contexts that distinguish processes whenever they are ready trace equivalent. Here ready trace semantics (RT^{∗}) is a bit finer than failure trace semantics (F T^{∗}). When analysing how priority operators distinguish processes that are failure trace equivalent, one finds that the priority operator in fact has unrealistic powers, and is not likely implementable.

The present paper shows that the addition of a time-out operator to a standard process algebra suffices to exploit the difference between failure trace inequivalent processes. Here the time-out operator is simply an instance of the traditional action prefixing operator α. , taking for α the time-out action t. I show that with this operator one can build, for any two failure trace inequivalent processes P and Q, a context C[ ] such that C[P] and C[P] are trace inequivalent. In fact, P and Q can be distinguished with may testing, as proposed by De Nicola & Hennessy [6]. Without the time-out operator, may testing merely distinguishes processes when they are trace inequivalent.

1.3 Capturing liveness properties while assuming justness

In [14] I present a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. The reason is that fairness assumptions, while indispensable for some applications, in many situations lead to false conclusions [17, 14]. Merely assuming progress, on the other hand, is often insufficient to obtain intuitively valid liveness properties. As an alternative to fairness assumptions, [17] proposes the weaker assumption of justness, that does not lead to false conclusions.

As pointed out in [14], when assuming justness but not fairness, liveness properties are not preserved by strong bisimilarity, let alone by any of the other equivalences in the linear time – branching time spectrum. An adequate treatment of liveness therefore calls for different semantic equivalences, ones that do not make all the identifications of strong bisimilarity.

Whereas adapting the notion of bisimilarity to take justness considerations properly into account is far from trivial, it appears that a version of failure trace semantics that preserves liveness properties when assuming justness but not fairness comes naturally, and is in a denotational approach to semantics hard to avoid. Here it is crucial that the semantics is based on complete failure traces, modelling potentially infinite observations of systems.

The present paper paves the way for such an approach by considering partial failure traces. This yields a semantic equivalence that is coarser than strong bisimilarity, and can be justified from an operational point of view, although it completely fails to respect liveness properties. The move from partial to complete failure trace equivalence is left for future work.

1.4 Absolute expressiveness

In comparing the expressiveness of process algebraic languages, an important distinction between absolute and relative expressiveness is made [30]. Relative expressiveness deals with the question whether an operator in one language can be faithfully mimicked by a context or open term in another. It is usually studied by means of valid encodings between languages [20, 13]. As there is a priori no upper bound on how convoluted an operator one can add to a process algebra, it may not be reasonable to aim for a universally expressive language, in which all others can be expressed, unless a thorough discipline is proclaimed on which class of operators is admissible.

Absolute expressiveness deals with the question whether there are systems that can be denoted by a closed term in one language but not in another. It can for instance be argued that up to strong bisimilarity the absolute expressiveness of a standard process algebra like CCS with guarded recursion is not decreased upon omitting the parallel composition (although its relative expressiveness surely is). Namely, up to strong bisimilarity, each transition system that can be denoted by a closed CCS expression can already be denoted by such a CCS expression that does not employ parallel composition. This consideration occurs in the proof of Theorem 1. When using absolute expressiveness, the goal of a universally expressive process algebra becomes much less unrealistic. In fact, when not considering time, probabilities, or other features that are alien to process algebras like CCS, it could be argued, and is perhaps widely believed, that the version of CCS with arbitrary infinite sums and arbitrary systems of recursive equations is already universally expressive. The reason is that all that can be expressed by CCS-like languages are states in LTSs, and up to strong bisimilarity, each state in each LTS can already be denoted by such a CCS expression.

This conclusion loses support when factoring in justness, as discussed in Section 1.3, for in this setting strong bisimilarity becomes too coarse an equivalence to base a theory of expressiveness upon. In fact, the idea that standard process algebras like CCS are universally expressive has been challenged in [10] and [16], where concrete and useful distributed systems are proposed that can not be modelled in such languages. In [10] this concerns a system that stops executing a repeating task after a time-out goes off, whereas the systems considered in [16] are fair schedulers and mutual exclusion protocols. In both cases a proper treatment of justness appears to be a prerequisite for the correct modelling of such systems, and for this reason this task falls outside the scope of the current paper. However, additionally, both examples need something extra beyond what CCS has to offer, and both papers indicate that a simple priority mechanism would do the job.

The current paper offers such a simple priority mechanism, and thereby paves the way for expressing the systems that have been proposed as witnesses for the lack of universal expressiveness of standard process algebras.

2 The process algebra CCSP_{t}

Let A and V be countably infinite sets of visible actions and variables, respectively. The syntax of CCSP_{t} is given by

E ::= 0 | α.E | E + E | E ∥_{S} E | τ_{I}(E) | R(E) | X | ^{/} \X|S^{\} / (with X ∈ V_{S})

with α ∈ Act := A ⊎ {τ, t}, S, I ⊆ A, R ⊆ A × A, X ∈ V and S a recursive specification: a set of equations {Y = S_{Y} | Y ∈ V_{S}} with V_{S} ⊆ V (the bound variables of S) and S_{Y} a CCSP_{t} expression.

The constant 0 represents a process that is unable to perform any action. The process α.E first performs the action α and then proceeds as E. The process E + F will behave as either E or F. ∥_{S} is a partially synchronous parallel composition operator; actions a ∈ S must synchronise—they can occur only when both arguments are ready to perform them—whereas actions α ∉ S from both arguments are interleaved. τ_{I} is an abstraction operator; it conceals the actions in I by renaming them into the hidden action τ. The operator R is a relational renaming: it renames a given action a ∈ A into a choice between all actions b with (a, b) ∈ R. I require that all sets {b | (a, b) ∈ R} are finite. Finally, ^{/} \X|S^{\} / represents the X-component of a solution of the system of recursive equations S. A CCSP_{t} expression E is closed if every occurrence of a variable X is bound, i.e., occurs in a subexpression ^{/} \Y |S^{\} / of E with X ∈ V_{S}.

The interleaving semantics of CCSP_{t} is given by the labelled transition relation → ⊆ ℙ × Act × ℙ on the set ℙ of closed CCSP_{t} terms or processes, where the transitions P ⟶^{a} Q are derived from the rules of Table 1. Here ^{/} \E|S^{\} / for E an expression and S a recursive specification denotes the expression E in which ^{/} \Y |S^{\} / has been substituted for the variable Y, for all Y ∈ V_{S}.

The language CCSP is a common mix of the process algebras CCS [26] and CSP [4, 23]. It first appeared in [27], where it was named following a suggestion by M. Nielsen. The family of parallel composition operators ∥_{S} stems from [28], and incorporates the two CSP parallel composition operators from [4]. The relation renaming operators R( ) stem from [35]; they combine both the (functional)

Table 1: Structural operational interleaving semantics of CCSP_{t}

\begin{matrix}α.x ⟶^{α} x  \frac{x ⟶^{α} x′}{x + y ⟶^{α} x′}  \frac{y ⟶^{α} y′}{x + y ⟶^{α} y′}  \frac{x ⟶^{α} x′}{R(x) ⟶^{β} R(x′)} (\begin{matrix}α=β=τ \\ ∨ α=β=t \\ ∨ (α,β)∈R \end{matrix}) \\ \frac{x ⟶^{α} x′}{x ∥_{S} y ⟶^{α} x′ ∥_{S} y} (α ∉ S) & \frac{x ⟶^{a} x′ y ⟶^{a} y′}{x ∥_{S} y ⟶^{a} x′ ∥_{S} y′} (a ∈ S) & \frac{y ⟶^{α} y′}{x ∥_{S} y ⟶^{α} x ∥_{S} y′} (α ∉ S) \\ \frac{x ⟶^{α} x′}{τ_{I}(x) ⟶^{α} τ_{I}(x′)} (α ∉ I) & \frac{x ⟶^{a} x′}{τ_{I}(x) ⟶^{τ} τ_{I}(x′)} (a ∈ I) & \frac{^{/} \S_{X}|S^{\} / ⟶^{α} y}{^{/} \X|S^{\} / ⟶^{α} y} \end{matrix}

renaming operators that are common to CCS and CSP, and the inverse image operators of CSP. The remaining constructs are common to CCS and CSP. The syntactic form of inaction 0, action prefixing α.E and choice E+F follows CCS, whereas the syntax of abstraction τ_{I}( ) and recursion ^{/} \X|S^{\} / follows ACP [3]. The only addition by me is the prefixing operator t. ; so far it is merely an action that admits no synchronisation, concealment, or renaming.

Definition 1 A strong bisimulation is a symmetric relation R on ℙ, such that, for all (P, Q) ∈ R and α ∈ Act,

• if P ⟶^{α} P′ then Q ⟶^{α} Q′ for some Q′ with P′RQ′.

Two processes P, Q ∈ ℙ are strongly bisimilar, P \underline{↔} Q, if P RQ for some strong bisimulation R.

Strong bisimilarity lifts in the standard way to open CCSP_{t} expressions, containing free with variables: E \underline{↔} F iff P \underline{↔} Q for each pair of closed substitution instances P and Q of E and F.

The common strong bisimulation semantics of process algebras like CCSP_{t} interprets closed expressions as \underline{↔}-equivalence classes of processes, thereby identifying strongly bisimilar processes. Operators, or more generally open terms E, then denote n-ary operations on such equivalences classes, with n the number of free variables occurring in E. To make sure that the meaning of the operators is independent of the choice of representative processes within their equivalences classes, it is essential that \underline{↔} is a congruence for all n-ary operators f:

• if P_{i} \underline{↔} Q_{i} for all i = 1, …, n then f(P_{1}, …, P_{n}) \underline{↔} f(Q_{1}, …, Q_{n}).

This property holds for CCSP_{t} since the structural operation semantics of the recursion-free fragment of the language, displayed in Table 1, fits the tyft/tyxt format of [21]. Likewise, to make sure that also the meaning of the recursion construct is independent of the choice of representative expressions within their equivalences classes, \underline{↔} needs to be full congruence for recursion [12]:

• if S_{Y} \underline{↔} S′_{Y} for all Y ∈ V_{S} = V_{S′} then ^{/} \X|S^{\} / \underline{↔} ^{/} \X|S′^{\} /

for all recursive specifications S and S′ and variables X with X ∈ V_{S} = V_{S′}. Again, this property holds since the semantics of Table 1 fits the tyft/tyxt format with recursion of [12].

Definition 2 Given a recursive specification S, write X ⟶^{u} Y, for variables X, Y ∈ V_{S}, if Y occurs in the expression S_{X} outside of all subexpressions α.E of S_{X}. S is guarded iff there is no infinite chain X_{0} ⟶^{u} X_{1} ⟶^{u} X_{2} ⟶^{u} . . .. A process is guarded if all recursive specifications called by it are guarded.

Often, one restricts attention to guarded processes. The axioms of Table 2 are sound for \underline{↔}, meaning that writing \underline{↔} for =, and substituting arbitrary expressions for the variables x, y, z, or the meta-variables

Table 2: A complete axiomatisation for strong bisimilarity on guarded CCSP_{t} processes

x + (y + z) = (x + y) + z  τ_{I}(x + y) = τ_{I}(x) + τ_{I}(y)  R(x + y) = R(x) + R(y)
x + y = y + x  τ_{I}(α.x) = α.τ_{I}(x)  if α ∉ I R(τ.x) = τ.R(x)
x + x = x  τ_{I}(α.x) = τ.τ_{I}(x)  if α ∈ I  R(t.x) = t.R(x)
x + 0 = 0  ^{/} \X|S^{\} / = ^{/} \S_{X}|S^{\} /  R(a.x) = ∑_{{b|(a,b)∈R}} b.R(x)

If P = ∑_{i∈I} α_{i}.P_{i} and Q = ∑_{j∈J} β_{j}.Q_{j} then

P ∥_{S} Q = ∑_{i∈I, α_{i}∉S} α_{i}.(P_{i} ∥_{S} Q) + ∑_{j∈J, β_{j} ∉S} β_{j}.(P ∥_{S} Q_{j}) + ∑_{i∈I, j∈J, α_{i}=β_{j}∈S}α_{i}.(P_{i} ∥_{S} Q_{j})

Recursive Specification Principle (RSP)  S ⇒ X = ^{/} \X|S^{\} /  (S guarded)

P_{i} and Q_{j}, turns them into true statements. In these axioms α, β range over Act and a, b over A. All axioms involving variables are equations. The axiom involving P and Q is a template that stands for a family of equations, one for each fitting choice of P and Q. This is the CCSP_{t} version of the expansion law from [26]. The axiom ^{/} \X|S^{\} / = ^{/} \S_{X}|S^{\} / is the Recursive Definition Principle (RDP) [3]. It says that recursively defined processes ^{/} \X|S^{\} / satisfy their set of defining equations S. In particular, this entails that each recursive specification has a solution. The axiom RSP [3] is a conditional equation, with as antecedents the equations of a guarded recursive specification S. It says that the X-component of any solution of S—a vector of processes substituted for the variables V_{S}—equals ^{/} \X|S^{\} /. This is equivalent to the statement that the solutions of guarded recursive specifications must be unique.

Theorem 1 For guarded P, Q ∈ ℙ, one has P \underline{↔} Q iff P = Q is derivable from the axioms of Table 2.

Proof Sketch: “If”, the soundness of the axiomatisation of Table 2, is an immediate consequence of the soundness of the individual axioms.

“Only if”, the completeness of the axiomatisation: Using the axioms from the first box of Table 2 any guarded CCSP_{t} process P can be brought in the form ∑_{i∈I} α_{i}.P_{i}—a head normal form. In fact, {(α_{i}, P_{i}) | i ∈ I} can be chosen to be {(α_{i}, P_{i}) | P ⟶^{α} P_{i}}. Given a process P, let reach(P) be the smallest set of processes containing P, such that R ⟶^{α} R′ with R ∈ reach(P) implies R′ in reach(P). Now dedicate to each R ∈ reach(P) a variable X_{R}, and consider the recursive specification S with V_{S} the set of all those variables, and as equations X_{R} = ∑_{k∈K} α_{k}.X_{R_{k}}, using the head normal form of R. Using RSP, we derive P = ^{/} \X_{P} |S^{\} /. Likewise, we can derive Q = ^{/} \X_{Q}|S′^{\} / for a recursive specification S′, consisting of equations of the form X_{S} = ∑_{l∈L} β_{l}.X_{S_{l}}.

Once we have two such recursive specifications, as described for instance in [26] we can create a combined recursive specification S′′ such that both P and Q are the X-components of solutions of S′′. With RSP one then derives P = Q. □

The above proof idea stems from Milner [26] and can be found in various places in the literature, but always applied to finite-state processes, or some other restrictive subset of a calculus like CCSP_{t}. Since the set of true statements P \underline{↔} Q, with P and Q processes in a process algebra like CCSP_{t}, is wellknown to be undecidable, and even not recursively enumerable, it was widely believed that no sound and complete axiomatisation of strong bisimilarity could exist. Only in March 2017, Kees Middelburg [25] observed (in the setting of the process algebra ACP [3]) that the above standard proof applies verbatim to arbitrary guarded processes. His result does not contradict the non-enumerability of the set of true statements P \underline{↔} Q, due to the fact that RSP is a proof rule with infinitely many premises.

3 Adding a time-out to CCSP

The process algebra CCSP, just like CCS, CSP and ACP, is an untimed process algebra, meaning that its semantics abstracts from a quantification of the amounts of time that elapse during or between the execution of the actions. Untimed process algebras do not deny that the execution of processes takes time; they abstract from timing merely in not specifying how much time elapses here and there. An untimed process could therefore be seen as a timed process, in which each occurrence of a particular period of time is replaced by a nondeterministic choice allowing any amount of time.

From this perspective, one could wonder whether time elapses during the execution of the actions α ∈ Act, or between the actions, that is, in the states. In some works, notably [18], it is assumed that time happens during the execution of actions. This leads to a rejection of equations like a∥b = a.b + b.a,^{2} which are fundamental for interleaving semantics [26, 4, 23, 3, 28], for the left-hand side allows an overlap in time of the actions a and b, whereas the right-hand side does not. The default opinion, however, is that the execution of actions is instantaneous, so that time must elapse between the actions. The following formulation of this assumption is taken from Hoare [23, Page 24]:

The actual occurrence of each event in the life of an object should be regarded as an instantaneous or an atomic action without duration. Extended or time-consuming actions should be represented by a pair of events, the first denoting its start and the second denoting its finish.

In [19] it is pointed out that simply replacing each occurrence of a durational action α by a sequence α^{+}.α^{−} of two instantaneous actions, one denoting the start and one the end of α, is insufficient to adequately capture the durational nature of actions—it even makes a difference whether actions are split into two or into three parts. The problem arises from the possibility that two actions α may occur independently in parallel, and the above splitting allows for the possibility that the end of one such action is confused with the end of the other. A possible solution is to model a durational action α as a process ∑_{i∈I} α_{i}^{+}.α_{i}^{−}, where each start action α^{+} is equipped with a tag i ∈ I that has to be matched by the corresponding end action α^{−}. When the choice I of tags is large enough, this suffices to model durational actions in terms of instantaneous actions and durational states. It is for that reason that in the present paper I focus on time elapsing in states only.

Let s be the state between the a- and τ-transitions in the process a.τ.P. Assume that time may elapse in state s, in the sense that after the execution of a and before the execution of τ, the modelled system, for some positive amount of time, does nothing whatsoever. Then it is hard to imagine what could possibly trigger the system to resume activity after this amount of time. A system that does nothing whatsoever may be regarded as dead, and remains dead.

The philosophy of Milner [26] appears to be that once a system reaches state s, it will proceed with the τ-transition immediately. However, once it reaches a state ∑_{i∈I} a_{i}.P_{i}, where the a_{i} are visible actions, it remains idle until the environment of the system triggers the execution of one of the actions a_{i}. The system is reactive, in the sense that visible actions occur only in reaction to stimuli from the environment. The latter could be modelled as the environment being a user of the system that may press buttons labelled a, for a ∈ A. In a state where the system is not able to engage in an a-transition, the user may exercise pressure on the a button, but it will not go down. In this philosophy, all time that elapses is due to the system waiting on its environment.

An unsatisfactory aspect of the above philosophy is that there is an asymmetry between a system and its environment. The latter can spontaneously cause delays, but the former may delay only in reaction to the latter. When we would model the environment also as a closed process algebraic expression, and put it in parallel with the system, in such a way that no action depends on triggers from outside the system/environment composition, then the resulting composition performs all its actions instantaneously, possibly until it reaches a deadlock, from which it cannot recover.

2I abbreviate a.0 by a and ∥_{∅} by ∥. Moreover, + binds weaker than a. , and ∥_{S} binds weakest of all.

The present paper offers an alternative account on the passage of time, with a symmetric view on systems and their environments. In fact, it tries to be as close as possible to the philosophy of Milner described above, but adds the expressiveness to model delays caused by a system rather than its environment. Here there are two overriding design decisions. First, amounts of time will not be quantified, for I aim to remain in the realm of untimed process algebras. Second, the assumption of progress [17] needs to be maintained. Progress says that from state s above one will sooner or later reach the process P, i.e., an infinite amount of waiting is ruled out. This assumption is essential for the formulation and verification of liveness properties, saying that a system will reach some goal eventually [17].

Following [9, 7], I explicitly allow the environment of a system to exercise pressure on multiple buttons at the same time. The actions for which, at a given time, the environment is exercising pressure, are allowed at this time, whereas the others are blocked. Instead of a model with buttons, one may imagine a model with switches for each visible action, where the environment, at discrete points in time, can toggle the switches of any action between allowed and blocked. In particular the occurrence of a visible action may trigger the environment to rearrange it switches.

To model time elapsing in a state, I assume that the state may be equipped with one of more timeouts. A time-out is a kind of clock that performs some internal activity, from which I abstract, and at the end of this activity emits a signal that causes a state-change. The time-out always runs for an unspecified, but positive and finite amount of time. For each time-out of a state there is an outgoing transition labelled t that models this state-change. A t-transition is not observable by the environment. So, apart from the associated time-out, it is similar to a τ-transition.

The state a.P + b.Q + t.R, for instance, has one outgoing t-transition, corresponding with one time-out. If, upon reaching this state, the environment is allowing one of a or b, this action will happen immediately, reaching the follow-up state P or Q; in case the environment allows both a and b, the choice between them is made nondeterministically, i.e., by means that are not part of my model. If, upon reaching the state a.P + b.Q + t.R, the environment is not allowing a or b, the system idles, until either the environment changes and allows a or b after all, or the time-out goes off, triggering the t-transition.

A state like a.P + t.Q + t.R simply has two time-outs; which one goes off first is not predetermined. If the transition to R occurs, the other time-out is simply discarded. A state like a.P + b.Q has no time-outs. Upon reaching this state the system idles until the environment allows a or b to happen.

Note that in a.P + b.Q + t.R the action t should not be seen as a durational τ-action, for that would suggest that as soon as that action starts, one has lost the option to perform a or b. Instead, the options a and b remain open until the instantaneous transition to R occurs.

The expressive power of time-outs

To model that a process like a.τ.P simply spends some time in the state s right before the τ-action, one could write a.t.τ.P. Furthermore, a durational action α, contemplated above, could be modelled as ∑_{i∈I} α_{i}^{+}.t.α_{i}^{−}. Both uses do not involve placing a process t.P in a +-context. The latter is useful for modelling a simple priority mechanism. Suppose one wants to model a process like a.P +b.Q, which can react on a- and b-stimuli from the environment. However one has a preference for a.P, in the sense that if the environment allows both possibilities, a.P should be chosen. This can be modelled as a.P + t.b.Q or a.P + t.(a.P + b.Q). In an environment allowing both a and b, this system will perform a.P. But in an environment just allowing b, first some idling occurs, and then b.Q.

Three crucial laws

The most fundamental law concerning time-outs, which could be added as an axiom to Table 2, is

τ.P + t.Q = τ.P .  (1)

It says that a choice between τ.P and t.Q will always be resolved in favour of τ.P, because the τ-action is not contingent on the environment and thus can happen immediately, before the time-out associated with t.Q has a chance to go off.

A process t.(τ.P + b.Q) will, after waiting for some time, make a choice between τ.P and b.Q. In case the environment allows b, this choice is nondeterministic. In case the environment blocks b at the time the time-out associated with the t-transition goes off, the system will immediately take the τ.P branch, thereby discarding b.Q. Henceforth I will substitute τ_{{b}}(P) for P, to indicate that this is a process that cannot perform a b-action. Now consider two such processes placed in parallel, synchronising on the action b. Each of these processes acts as the environment in which the other will be placed. In this paper I assume that here the synchronisation on b can not occur:

t.(τ.τ_{{b}}(P) + b.Q) ∥_{{b}} t.(τ.τ_{{b}}(S) + b.T) = t.τ.τ_{{b}}(P) ∥_{{b}} t.τ.τ_{{b}}(S) .  (2)

Intuitively, the reason is that the time-outs on the left and on the right go off at random points in real time. I explicitly assume no causal link of any kind between the relative timing of these events. Hence the probability that the two time-outs go off at the very same moment is 0, and this possibility can be discarded. So either the left-hand side in the parallel composition reaches the state L := τ.τ_{{b}}(P)+b.Q before the right-hand process reaches the state R := τ.τ_{{b}}(S) + b.T, or vice versa. For reasons of symmetry I only consider the former case. When the state L is reached, the environment of that process is not yet ready to synchronise on b, so τ.τ_{{b}}(P) will happen instead. This forces the right-hand side, when reaching the state R, to choose τ.τ_{{b}}(S), for τ_{{b}}(P) cannot synchronise on b.

Algebraically, (2) can be derived from (1) and the axioms of Table 2, when taking for granted the obvious identity τ_{{b}}(x)∥_{{b}}t.(y+b.z) = τ_{{b}}(x)∥_{{b}}t.y (whose closed instances with guarded recursion are derivable from the axioms of Table 2):

t.L ∥_{{b}} t.R =^{(Expansion Law)}

t. (L ∥_{{b}} t.R) + t. (t.L ∥_{{b}} R) =^{(Expansion Law)}

t. (τ. (τ_{{b}}(P) ∥_{{b}} t.R) + t. (L ∥_{{b}} R)) + t. (t.L ∥_{{b}} R) =^{(1)}

t. (τ. (τ_{{b}}(P) ∥_{{b}} t.R)) + t. (t.L ∥_{{b}} R) =^{(obvious identity; same reasoning on the right)}

t. (τ. (τ_{{b}}(P) ∥_{{b}} t.τ.τ_{{b}}(S))) + t. (τ. (t.τ.τ_{{b}}(P) ∥_{{b}} τ_{{b}}(S))) =^{(same way back)}

t.τ.τ_{{b}}(P) ∥_{{b}} t.τ.τ_{{b}}(S) .

To reject (2) one would need to take into account seriously the possibility that the two time-outs take exactly equally long. This corresponds to the addition of the rule

\frac{x ⟶^{t} x′ y ⟶^{t} y′}{x ∥_{S} y ⟶^{t} x′ ∥_{S} y′}

to the structural operational semantics of CCSP_{t}, and the summand + ∑_{i∈I, j∈J, α_{i}=β_{j}=t} t.(P_{i} ∥_{S} Q_{j}) to the expansion law of CCSP_{t}. While this could very well lead to an interesting alternative treatment of timeouts, I will not pursue this option here.

Another law, that could also be added as an axiom to Table 2, is

a.P + t.(Q + τ.R + a.S) = a.P + t.(Q + τ.R) .  (3)

When the process a.P + t.(Q + τ.R + a.S) runs in an environment that allows a, the summand t.(Q + τ.R + a.S) will not be taken, so it does not matter if there is a summand a.S after the t-action. And when this process runs in an environment that keeps blocking a long enough, the summand a.S will not be taken. So the only way to execute a.S is in an environment that initially blocks a, but then makes a change to allow a. In this case we need to consider two independently chosen points in time: time t_{e} where the environment starts allowing a, and time t_{s} where the time-out goes off that makes the system take the (unobservable) t-transition to the state Q + τ.R + a.S. Following the same reasoning as for law (2), the probability that t_{e} = t_{s} is 0, so this possibility can be ignored. In case t_{e} occurs before t_{s}, the system will never reach the state Q + τ.R + a.S. In case t_{e} occurs after t_{s}, the system will, in state Q + τ.R + a.S, choose τ.R (or a branch from Q) over a.S. In either case, the summand a.S can just as well be omitted.

Time guardedness

CCSP_{t} allows expressions such as ^{/} \X|X = τ.X^{\} / or ^{/} \X|X = a.X^{\} / where infinitely many actions could happen instantaneously. When this is felt as a drawback, one could impose syntactic restrictions on the language to rule out such behaviour. The following is an example of such a restriction.

Definition 3 Given a recursive specification S, write X ⟶^{tu} Y, for variables X, Y ∈ V_{S}, if Y occurs in expression S_{X} outside of all subexpressions t.E of S_{X}. S is time guarded iff there is no infinite chain X_{0} ⟶^{tu}X_{1} ⟶^{tu}. . .. A process is time guarded if all recursive specifications called by it are time guarded.

Clearly, the time guarded CCSP_{t} expressions, a subset of the guarded CCSP_{t} expressions, allow only finitely many actions to occur between any two time-out transitions.

4 Trace and failures equivalence fail to be congruences

The paper [9] presents a spectrum of semantic equivalences on processes encountered in the literature. It only deals with concrete processes, not featuring the internal action τ. Of course, the time-out action t does not occur in [9] either. Figure 1 reproduces the spectrum of [9, Figure 9], while omitting those semantic equivalences that fail to be congruences for the τ-free fragment of CCSP—those were coloured red in [9, Figure 9].

(Strong) bisimilarity (B) [26, 29], cf. Definition 1, is the finest semantics of Figure 1, i.e., making the fewest identifications between processes, or yielding the smallest equivalence classes. It sits at the branching time side of the spectrum, as it distinguishes processes based on the timing of choices between different execution sequences, e.g., a.(b.c + b.d) ≠ a.b.c + a.b.d.

(Partial) trace semantics (T^{∗}) [22] is the coarsest semantics of Figure 1, i.e., making the most identifications. It sits at the linear time side of the spectrum, as it abstracts a process into the sequences of action occurrences that can be observed during its runs, its traces, and identifies two processes when they have the same traces.

Failures semantics (F^{∗}) is the default semantics of the process algebra CSP [4, 23]. When restricting to concrete processes, its falls neatly between T^{∗} and B. Similar to bisimulation semantics, failures semantics rejects the equation a.(b + c) = a.b + a.c that holds in trace semantics. The main reason for

T^{∗} F^{∗}  R^{∗} F T^{∗} RT^{∗} RS^{∗}_{FS_{∗}} S^{∗}  PF^{∗}  T^{∞} F^{∞} R^{∞} F T^{∞} RT^{∞} RS 2S B S  _{PF^{∞}} RS^{ω} 2S^{ω} B^{ω} S^{ω}

Figure 1: The linear time – branching time spectrum [9]

doing so is that in an environment where action c remains blocked, the left-hand side will surely do the b-action, whereas the right-hand side may deadlock instead. However, no such argument distinguishes a.(b.c + b.d) and a.b.c + a.b.d, and hence these processes are identified in failures semantics.

Failure trace semantics (F T^{∗}) was proposed in [9], and first presented in [1], as the natural completion of the square suggested by failures, readiness [28] and ready trace semantics [2]. For finitely branching processes it coincides with refusal semantics, introduced by Phillips in [31]. Like failure semantics it rejects the identity a.(b + c) = a.b + a.c, but accepts a.(b.c + b.d) = a.b.c + a.b.d. The standard example of two processes that are failures equivalent but not failure trace equivalent is displayed in Figure 2.

a  a c  c b  f d  e a.(b + c.d) + a.(f + c.e)  =_{F} ≠_{F T} =_{R} ≠_{RT}  a a  c c  f b  d e a.(b + c.e) + a.(f + c.d)

Figure 2: Failures and ready equivalent, but not failure trace or ready trace equivalent [9]

The following argument shows that neither trace nor failures equivalence are congruences for the operators of CCSP_{t}. That is, there are failures equivalent processes P and Q (that are therefore certainly trace equivalent) and a recursion-free CCSP_{t}-context C[ ] such that C[P] and C[P] are trace inequivalent.

Example 1 Take P := a.(b + c.d) + a.(f + c.e) and Q := a.(b + c.e) + a.(f + c.d). Use the context C[ ] := τ_{{a,b,c}}(a.(b + t.c) ∥_{{a,b,c,f}} ). Then only C[Q] can ever perform the action d. Namely, the context, enforcing synchronisation on the actions a, b, c and f, implements a priority of b over c (while blocking f altogether); whenever its argument process P or Q faces a choice between a b- and a c-transition, within this context it must take the b-transition. This explains why C[P] can never reach the action d. The abstraction operator τ_{{a,b,c}} is not redundant, although τ_{{b}} would have worked as well. Without such an operator, the process C[P] might run in an environment in which b is blocked, and here the d could occur after all.

Interestingly, I could make this argument without even providing definitions of trace and failures equivalence on LTSs that feature time-out transitions. The only two things we need to know about such equivalences are that they must (a) distinguish a process that can never do the action d from one that can, and (b) identify the two processes of Figure 2. Property (b) is satisfied when merely requiring that on concrete process (without τ and t) these equivalences agree with the definitions in [9]. The argument is thus also independent of the question how these equivalences are extended to a setting with the hidden action τ.

The same example, with its above analysis, also shows that ready equivalence (R^{∗}) fails to be a congruence for CCSP_{t}, for it also identifies the processes P and Q.

In Figure 1 I have coloured red all those semantics that can be seen to fail the congruence requirement by a similar argument. For the infinitary versions of trace, failures and readiness semantics (T^{∞}, F^{∞} and R^{∞}), the same example applies. For possible-futures equivalence (P W^{∗} and P W^{∞}) one takes as witness the two processes of [9, Counterexample 7], in combination with the obvious context that gives priority of b over a as well as c. Simulation equivalence (S) and its finitary variants (S^{∗} and S^{ω}) make the identification a.b + a = a.b [9, Counterexample 2]. Using this, the following argument shows that these semantics also fail to be congruences for CCSP_{t}.

Example 2 Take P := a.b + a and Q = a.b, and use the context C[ ] := τ_{{a,b}}(a.(b + t.d) ∥_{{a,b}} ). Then only C[P] can ever perform the action d. Here d can be done by the context only, rather than by the processes P or Q. However, after synchronising on a, the context will proceed towards d only when the environment of b + t.d, which is the process P or Q synchronising on b, blocks the b-transition. This is possible for P but not for Q. In this example the possibility to deadlock (or the impossibility to perform a certain action) is made observable through a context.

It follows that failure trace semantics is in fact the coarsest semantics reviewed in [9] that could be a congruence for the operators of CCSP_{t}. By the arguments in Section 1.2 it also is the finest semantics with a convincing testing scenario, in the sense that all finer semantics make distinctions that are hard to justify. Together, this tells us that failure trace semantics may be the only reasonable semantics for CCSP_{t}.

The next section proposes an extension of the definition of failure trace semantics (in [9] only given for concrete processes, without the special actions τ and t) to arbitrary LTSs featuring τ and t, and thereby to CCSP_{t}. Of course on LTSs with τ but without t it coincides with the definition given in [7].

Then Section 6 shows that, when restricting the choice operator + of CCSP_{t} to guarded choice, failure trace equivalence is in fact a congruence for the operators of CCSP_{t}. To obtain a congruence for the +, a rooted version of failure trace equivalence is defined that records more information on the behaviour of process around their initial states. This situation is the same as for weak bisimilarity [26] and virtually all other semantic equivalences that partially abstract from the hidden action τ.

In Section 8 I then show that for any two failure trace inequivalent processes P and Q one can find a recursion-free CCSP_{t}-context C[ ] such that C[P] and C[P] are trace inequivalent. This means that the arguments from Examples 1 and 2 not only apply to the semantics surveyed in [9], but in fact to any semantics that is incomparable with or coarser than failure trace semantics.

5 Partial failure trace semantics of CCSP_{t}

A finite failure trace is a sequence σ ∈ (A ∪ P(A))^{∗} of actions and sets of actions. It represents an observation of a system. Each action a ∈ A occurring in σ represents the observation of the instantaneous occurrence of that action. Each set X ⊆ A occurring in σ represents the observation of a period of idling (meaning that no actions occur) during which the environment allows (i.e., is ready to synchronise with) exactly the actions in X. Such a set is called a refusal set [4, 9], because it it corresponds with an offer X from the environment that is refused by the system. A partial failure trace σ⊤ consists of a finite failure trace σ followed by the tag ⊤. It represents a partial observation of a system. The symbol ⊤ indicates the act, on the part of the observer, of ending the observation.

Table 3: Operational failure trace semantics of CCSP_{t}

⊤ ∈ F T^{∗}(x)  \frac{x ⟶^{a} y ρ ∈ F T^{∗}(y)}{aρ ∈ F T^{∗}(x)}  \frac{x ⟶^{τ} y ρ ∈ F T^{∗}(y)}{ρ ∈ F T^{∗}(x)}

\frac{\begin{matrix}x−↛^{α} for all α ∈ X ∪ \{τ\} \\ ρ ∈ F T^{∗}(x) \end{matrix}}{Xρ ∈ F T^{∗}(x)}  \frac{\begin{matrix}x−↛^{α} for all α ∈ X ∪ \{τ\} \\ x ⟶^{t} y Xρ ∈ F T^{∗}(y) \end{matrix}}{Xρ ∈ F T^{∗}(x)}  \frac{\begin{matrix}x−↛^{α} for all α ∈ X ∪ \{τ\} \\ x ⟶^{t} y aρ ∈ F T^{∗}(y) \end{matrix}}{Xaρ ∈ F T^{∗}(x)} (a ∈ X)

Table 3 derives the set F T^{∗}(P) of partial failure traces of a process P. Here concatenation of sequences is denoted by juxtaposition. The first rule testifies that it is always possible to end the observation and just record ⊤. The next two rules say that visible actions are observed, whereas hidden actions are not. The fourth rule says that, when the environment allows the set of actions X, idling in a given state x is possible iff from that state no actions a ∈ X, nor the hidden action τ, can occur. These four rules stem in essence from [9, 7]. The last two rules deal with the time-out t. To follow a transition x ⟶^{t} y, the system must be idling in state x until the time-out occurs. Let X be the set of actions allowed by the environment at this time. As explained with Law (3), I ignore the possibility that the environment changes the set of allowed actions at the exact same time as the occurrence of the time-out. So right after the time-out occurs, X is still the set of actions allowed by the environment. At this time there are two possibilities. Either the system keeps idling, namely when none of the actions from X can occur in state y; or the system performs one of the actions a ∈ X (possibly after some τ-transitions). These two possibilities correspond with the remaining two rules.

Definition 4 Processes P, Q∈ℙ are partial failure trace equivalent, P ≡_{F T}^{∗} Q, iff F T^{∗}(P)=F T^{∗}(Q).

A path-based characterisation of partial failure traces

Definition 5 A finite path π : P_{0} ⟶^{α_{1}} P_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{ℓ}} P_{ℓ} is an alternating sequence of states/processes and transitions, starting and ending with a state, each transition going from the state before it to the state after it. One says it is a path of P ∈ ℙ if its first state P_{0} is P.

A process P ∈ ℙ is stable, notation stable(P), if P −↛^{τ}, i.e., if it has no outgoing τ-transitions. The set I(P) of initial visible actions of a process P is {a ∈ A | P ⟶^{a}}, provided P is stable. Here

P ⟶^{a} means that P ⟶^{a} Q for some Q ∈ ℙ. If P is unstable, I(P) := ⊥.

The concrete ready trace crt(π) of a finite path π as above is I(P_{0})α_{1}I(P_{1})α_{2} ⋯ α_{ℓ}I(P_{ℓ}). The (abstract) ready trace rt(π) of π is obtained from crt(π) by leaving out all occurrences of τ and ⊥.

Note that each partial failure trace σ of a process P is generated by a path π of P, and is in fact completely determined by rt(π). Each occurrence of action a in σ originates from a transition ⟶^{a} occurring in π (by application of the second rule of Table 3) and each occurrence of a refusal set X in σ originates (by application of the fourth or sixth rule) from a stable process P_{i} in π such that I(P_{i}) ∩ X = ∅. The last symbol ⊤ of σ originates from the last state P_{ℓ} of π (by application of the first rule). The mapping from the action occurrences in σ to the A-labelled transitions in π must be bijective, and any two elements (actions, refusal sets or ⊤) of σ occur in the same order in σ as their originators occur in π.

Let ξ be the occurrence of an action, refusal set or ⊤ in σ, originating from ⟶^{α_{j}} or P_{j}. If ξ is the first element of σ, the realm of ξ is the prefix of π ending in P_{j}. In case a or Y is the symbol in σ preceding ξ, with a originating from ⟶^{α_{i}} or Y originating from P_{i}, then j ≥ i and the realm of ξ is the subpath P_{i} ⟶^{α_{i+1}} ⋯ ⟶^{α_{j}} P_{j}. Thus, σ partitions π into realms, with each two adjacent realms having exactly one state in common.

Each transition in the realm of ⊤ must be labelled τ, matching an application of the third rule of Table 3. Each transition ⟶^{α_{k}} in the realm of a refusal set X must be labelled t or τ, matching applications of the third and fifth rules; if α_{k} = t then P_{k−1} must be stable and I(P_{k−1}) ∩ X = ∅. Only the first transition in the realm of an action occurrence a could be labelled t; if it is then in σ action a is preceded with a refusal set X such that a ∈ X. This matches an application of the sixth rule.

In particular, a path featuring a t-labelled transition leaving from an unstable state does not generate any partial failure traces.

System- versus environment-ended periods of idling

Observation 1 σXρ ∈ F T^{∗}(P) ⇔ σXXρ ∈ F T^{∗}(P).

An occurrence of a set X in a partial failure trace σ denotes a period p of idling, during which X is the set of actions allowed by the environment. During period p the system idles because none of the actions in X is enabled by the system, and none of the others is allowed by the environment. Such a period can end in exactly two ways: either by a time-out within the modelled system, or by the environment changing the set of actions it allows. The latter can be thought of as the occurrence of time-out outside the modelled system. In this paper I ignore the possibility that a time-out within the system occurs at the exact same moment as a time-out outside the system. Hence there can never be ambiguity on which party ends a period of idling.

I will now show how from the shape of a partial failure trace one can deduce which party ends a given period of idling. If, within σ, X is followed by a set Y ≠ X, the period p is followed by a period q of idling, this time with Y the set of actions allowed by the environment. The transfer from period p to period q must therefore be triggered by the environment, namely by changing the set of actions it allows to occur. If, within σ, X is followed by an action a ∈ X, the state of the system in which action a occurs must be different from the state of the system in which X is refused, and action a not enabled. It follows that period p must be ended by a time-out occurring within the system. If, within σ, X is followed by an action a ∉ X, period p must be ended by the environment. For if the set of actions allowed by the environment is not changed after period p, the action a ∉ X would still not be allowed.

Definition 6 An occurrence of X in a partial failure trace σ is system-ended iff within σ, X is followed by an action a ∈ X.

6 Congruence properties

In this section I show that partial failure trace equivalence is a congruence for the operators of CCSP_{t}, with the exception of the choice operator +. I also characterise the coarsest equivalence included in ≡_{F T}^{∗} that also is a congruence for +.

Definition 7 Let F ⊆ (A ∪ P(A))^{∗}⊤, meaning F is a set of partial failure traces with the end tag ⊤. Then col(F) is the smallest set containing F such that σXXρ ∈ col(F) ⇒ σXρ ∈ col(F).

Theorem 2 ≡_{F T}^{∗} is a congruence for the parallel composition operators ∥_{S}.

Proof: I need to show that P ≡_{F T}^{∗} P′ and Q ≡_{F T}^{∗} Q′ implies P ∥_{S} Q ≡_{F T}^{∗} P′ ∥_{S} Q′. This is equivalent to showing that F T^{∗}(P ∥_{S} Q) is completely determined by F T^{∗}(P), S and F T^{∗}(Q).

Below I define, for each S ⊆ A, a binary operator ∥_{S} that takes as arguments sets of partial failure traces, and produces again a set of partial failure traces. In the appendix—Proposition 1—I prove that

F T^{∗}(P ∥_{S} Q) = col(F T^{∗}(P) ∥_{S} F T^{∗}(Q)) .  (4)

This yields Theorem 2. □

In order to define the operator ∥_{S}, I analyse how a partial failure trace of P ∥_{S} Q decomposes into partial failure traces of P and Q.

Definition 8 A decomposition of a partial failure trace σ = σ_{1}σ_{2} ⋯ σ_{n}⊤ ∈ (A ∪ P(A))^{∗}⊤ w.r.t. a set S ⊆ A is a pair σ_{L}, σ_{R} of partial failure traces, obtained by leaving out all ⋆-elements from sequences σ^{L} = σ_{1}^{L}σ_{2}^{L} ⋯ σ_{n}^{L}⊤ and σ^{R} = σ_{1}^{R}σ_{2}^{R} ⋯ σ_{n}^{R}⊤ ∈ (A ∪ {⋆} ∪ P(A))^{∗}⊤, such that, for all i = 1, …, n,

• if σ_{i} ∈ A \ S then either σ_{i}^{L} = σ_{i} and σ_{i}^{R} = ⋆, or σ_{i}^{R} = σ_{i} and σ_{i}^{L} = ⋆,

• if σ_{i} ∈ S then σ_{i}^{L} = σ_{i}^{R} = σ_{i}, and

• if σ_{i} ∈ P(A) then σ_{i}^{L} ∈ P(A) and σ_{i}^{R} ∈ P(A).

This decomposition is valid if, for each i = 1, …, n for which σ_{i} ∈ P(A), one has

σ_{i} is system-ended in σ ⇔ ((σ_{i}^{L} is system-ended in σ_{L}) ∨ (σ_{i}^{R} is system-ended in σ_{R}))  (5)
¬((σ_{i}^{L} is system-ended in σ_{L}) ∧ (σ_{i}^{R} is system-ended in σ_{R}))  (6)
σ_{i}^{L} \ S = σ_{i} \ S = σ_{i}^{R} \ S  and (σ_{i}^{L} ∩ S) ∪ (σ_{i}^{R} ∩ S) = σ_{i} ∩ S .  (7)

For F, G ⊆ (A ∪ P(A))^{∗}⊤ sets of partial failure traces, let F ∥_{S} G ⊆ (A ∪ P(A))^{∗}⊤ be the set of partial failure traces σ, such that for some valid decomposition one has σ_{L} ∈ F and σ_{R} ∈ G.

Definition 8 says that in any partial failure trace σ ∈ F T^{∗}(P ∥_{S} Q), each occurrence of an action a ∉ S in σ must stem from either P or Q, whereas each occurrence of an action a ∈ S must stem from both. A set X occurring in σ denotes a period of idling; necessarily both P and Q idle during this period. I justify (5)–(7) informally below; formally, these requirements are fully justified by the fact that they allow me to prove (4).

In a parallel composition P ∥_{S} Q there are three parties that can block actions, or end idle periods: P, Q and the global environment E of the composition. The environment of P consists of Q and E.

An idle period of P ∥_{S} Q ends through a single time-out. If this timeout occurs in P ∥_{S} Q itself, rather then in its environment, it must occur in exactly one of the components P and Q. And if the time-out stems from the environment it occurs in neither component. This explains conditions (5) and (6).

An action a ∉ S can, from the perspective of one component, not be blocked by the other component. So it is blocked by the environment of that component iff it is blocked by the environment E of the parallel composition. Hence a ∈ σ_{i}^{L} ⇔ a ∈ σ_{i} ⇔ a ∈ σ_{i}^{R}. This gives the first formula of (7).

An action a ∈ S requires cooperation of all three parties, P, Q and E, so it can be blocked by any of them. If such an action is in σ_{i}^{L} (resp. σ_{i}^{R}), it is not blocked by the environment of P (resp. Q), and thus certainly not by E. This gives direction ⊆ of the second formula of (7).

To justify the other direction, note that each set X occurring in a partial failure trace of a process R corresponds with path R_{0} ⟶^{α_{1}} R_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} R_{n} (its realm), where R_{0} is reachable from R, such that (i) all α_{j} are either τ or t, and (ii) for each j ∈ {0, …, n−1} such that α_{j+1} = t, and also for j = n, one has R_{j} −↛^{β} for all β ∈ X ∪{τ}. In the special case that R = P ∥_{S} Q, and where X(= σ_{i}) is decomposed into X_{L}(= σ_{i}^{L}) and X_{R}(= σ_{i}^{R}), each such R_{j} has the form P_{j} ∥_{S} Q_{j}, with P_{j} −↛^{β} for β ∈ X_{L} ∪ {τ} and Q_{j} −↛^{β} for β ∈ X_{R} ∪ {τ}. Since, for a ∈ S, P_{j} ∥_{S} Q_{j} −↛^{a} iff either P_{j} −↛^{a} or Q_{j} −↛^{a}, one can always choose the decomposition of X into X_{L} and X_{R} in such a way that a ∈ X implies a ∈ X_{L} ∨ a ∈ X_{R}. This gives direction ⊇ of the second formula of (7).

There is one circumstance, however, where the above argument breaks down, namely if different choices of j ∈ {0, …, n} give rise to a different decomposition of X into X_{L} and X_{R}. However, in such a case one can simply write the occurrence of X as XX … X, such that now each occurrence of X has a unique decomposition. The original failure trace is then recovered by the closure operator col in (4).

The following example shows the necessity of Condition (5).

Example 3 Consider the process a ∥_{∅} t.b. Here {b}a⊤ ∈ F T^{∗}(a) and {b}b⊤ ∈ F T^{∗}(t.b). So without Condition (5) one would obtain {b}ab⊤ ∈ F T^{∗}(a ∥_{∅} t.b). Yet a ∥_{∅} t.b has no such partial failure trace.

Two similar examples, without and with synchronisation, show the necessity of Condition (6).

Example 4 Consider the process t.a ∥_{∅} t.b. Here {a, b}a⊤ ∈ F T^{∗}(t.a) and {a, b}b⊤ ∈ F T^{∗}(t.b). So without Condition (6) one would obtain {a, b}ab⊤ ∈ F T^{∗}(t.a ∥_{∅} t.b). Yet t.a ∥_{∅} t.b has no such partial failure trace.

Example 5 Consider the process t.(τ + b) ∥_{{b}} t.(τ + b). Here {b}b⊤ ∈ F T^{∗}(t.(τ + b)). So without Condition (6) one would obtain {b}b⊤ ∈ F T^{∗}(t.(τ + b) ∥_{{b}} t.(τ + b)). Yet, as explained at (2), t.(τ + b) ∥_{{b}} t.(τ + b) has no such partial failure trace.

The next example shows that the operation col in (4) cannot be omitted.

Example 6 One has σ := {b}{b}a⊤ ∈ F T^{∗}(b + t.a) ∥_{{a,b}} F T^{∗}(t.(b + t.a)), taking σ_{L} := ∅{b}a⊤ and σ_{R} := {b}∅a⊤. Namely ⊤ ∈ F T^{∗}(0), a⊤ ∈ F T^{∗}(a), {b}a⊤ ∈ F T^{∗}(a), ∅{b}a⊤ ∈ F T^{∗}(a), so ∅{b}a⊤ ∈ F T^{∗}(b + t.a), and ∅a⊤ ∈ F T^{∗}(a), ∅a⊤ ∈ F T^{∗}(b + t.a), ∅a⊤ ∈ F T^{∗}(t.(b + t.a)), so {b}∅a⊤ ∈ F T^{∗}(t.(b + t.a)). Yet {b}a⊤ ∉ F T^{∗}(b + t.a) ∥_{{a,b}} F T^{∗}(t.(b + t.a)).

Theorem 3 ≡_{F T}^{∗} is a congruence for the abstraction operators τ_{I}.

Proof: A partial failure trace ρ survives abstraction from I ⊆ A iff (i) each set X occurring in ρ satisfies I ⊆ X, (ii) each subsequence Xc_{0} … c_{n}Y with c_{0}, …, c_{n} ∈ I satisfies X = Y, and (iii) each subsequence Xc_{0} … c_{n}a with c_{0}, …, c_{n} ∈ I and a ∉ I satisfies a ∈ X. If this is the case, then τ_{I}(ρ) is the result of contracting any subsequence Xc_{0} … c_{n}X of ρ to X, and omitting all remaining occurrences of actions c ∈ I. If this is not the case τ_{I}(ρ) is undefined. Let σ ∪ I denote the partial failure trace obtained from a partial failure trace σ by replacing each occurrence of X in σ by X ∪ I. I claim that

σ ∈ F T^{∗}(τ_{I}(P)) ⇔ ∃ρ ∈ F T^{∗}(P). τ_{I}(ρ) = σ ∪ I .  (8)

This shows that F T^{∗}(τ_{I}(P)) is completely determined by F T^{∗}(P) and I, which yields Theorem 3. A formal proof of (8) is given in the appendix—Proposition 2. □

Intuitively, an occurrence of X in σ denotes a period of idling in which X is the set of actions allowed by the environment E of τ_{I}(P). The environment E_{P} of P when P is placed in a τ_{I}( )-context always allows the actions from I, and for the rest is like E. This explains (i) and the use of σ ∪ I in (8). Conditions (ii) and (iii) express that the instantaneous occurrence of a sequence of internal actions does not constitute an opportune moment for the environment to change its mind on which actions are allowed. Since c_{0} ∈ X (by (i)), the period X of idling ends through a time-out action of the system, right before the occurrence of c_{0}. Whereas in P the action c_{0} could synchronise with the environment, and thus cause a change in the set of allowed actions, this option is no longer available for τ_{I}(P). So after the sequence of internal actions, the same set of actions X is allowed by the environment, either resulting in further idling, or in the execution of an action a ∈ X.

An occurrence of X in σ imposes the requirement on some reachable states τ_{I}(P′) of τ_{I}(P) that τ_{I}(P′) −↛^{α} for all α ∈ X ∪ {τ}. It is satisfied iff P′ −↛^{α} for all α ∈ X ∪ I ∪ {τ}. The particular way of hiding actions c ∈ I in τ_{I}(ρ), together with Conditions (ii) and (iii), exactly matches the two rules for bridging a time-out transition in Table 3.

Theorem 4 ≡_{F T}^{∗} is a congruence for the relational renaming operators R.

Proof: For X ⊆ A, let R^{−1}(X) := {a ∈ A | ∃b ∈ X. (a, b) ∈ R}. Furthermore, let R^{−1}(σ) denote the set of partial failure traces obtained from σ by (i) replacing each occurrence of a set X by the set R^{−1}(X), and (ii) replacing each occurrence of an action b by some action a with (a, b) ∈ R, subject to the condition that if the occurrence of b is preceded by an occurrence of a set X, then b ∈ X iff a ∈ R^{−1}(X). Now, as shown by Proposition 3 in the appendix,

σ ∈ F T^{∗}(R(P)) ⇔ ∃ρ ∈ F T^{∗}(P). ρ ∈ R^{−1}(σ) .  (9)

The side condition ensures that for each period of idling, the party that ends it (system or environment) does not differ between σ and ρ. This shows that F T^{∗}(R(P)) is completely determined by R and P, which yields Theorem 4. □

The following example shows that the side condition in the definition of R^{−1}(σ) cannot be omitted.

Example 7 Let P = t.a and R = {(a, b), (a, c)}. Then ρ = {a}a⊤ ∈ F T^{∗}(P), so without the side condition one would obtain σ = {b}c⊤ ∈ F T^{∗}(R(P)). However, R(P) has no such failure trace, for if the environment allows just b when the time-out occurs, R(P) will proceed with b rather than c.

Rooted partial failure trace semantics

Partial failure trace equivalence, however, like all default equivalences that abstract from internal activity [26], fails to be a congruence for the choice operator +. In particular, F T^{∗}(b) = F T^{∗}(τ.b), yet F T^{∗}(a + b) ≠ F T^{∗}(a + τ.b), for only a + τ.b has a partial failure trace {a}⊤, and only a + b has a partial failure trace ∅a⊤. The classical way to solve this problem for languages like CCSP is to add one bit of information to the semantics of processes. Two CCSP processes could be called partial failure trace congruent iff F T^{∗}(P) = F T^{∗}(Q) ∧ stable(P) ⇔ stable(Q). This turns out to be a congruence for CCSP, and moreover the coarsest congruence finer than partial failure trace equivalence. In the presence of time-outs this one-bit modification of partial failure trace equivalence is insufficient, for F T^{∗}(t.b) = F T^{∗}(t.t.b), yet F T^{∗}(a+t.b) ≠ F T^{∗}(a+t.t.b). Namely, only a+t.t.b has a partial failure trace {b}{a, b}b.

To make partial failure trace equivalence a congruence, one needs additionally to keep track of partial failure traces of the form Xσ that are lifted by the fifth rule of Table 3 through an initial t-transition. I also use an additional bit, telling that a stable state is reachable along a nonempty path of τ-transitions.

Definition 9 Let F T^{r∗}(P) :=

F T^{∗}(P) \begin{matrix}∪ \{stab | P −↛^{τ}\} ∪ \{tXσ | ∃P′. P ⟶^{t} P′ ∧ Xσ ∈ F T^{∗}(P′) ∧ P −↛^{τ} ∧ I(P) ∩ X = ∅\} \\ ∪ \{poststab | P ⟶^{τ} ∧ ∅⊤ ∈ F T^{∗}(P)\}. \end{matrix}

Processes P, Q ∈ ℙ are rooted partial failure trace equivalent, P ≡_{F T}^{r∗} Q, iff F T^{r∗}(P) = F T^{r∗}(Q).

One has t.b ≢_{F T}^{r∗} t.t.b because t{a, b}b ∈ F T^{r∗}(t.t.b) but t{a, b}b ∉ F T^{r∗}(t.b).

For the purpose of defining ≡_{F T}^{r∗}, the poststab bit is redundant, as it is clearly determined by the other elements of F T^{r∗}(P). However, it will turn out to be useful in defining a rooted partial failure trace preorder ⊑_{F T}^{r∗} in Section 7.

Observation 2 Rooted partial failure trace equivalence is finer than partial failure trace equivalence.

Let ini_{Z}(F), for Z⊆A and F ⊆(A∪P(A))^{∗}⊤, be the least set such that (a) F ⊆ini_{Z}(F), (b) ⊤∈ini_{Z}(F), and (c) if σ ∈ ini_{Z}(F) and X ∩ Z = ∅ then Xσ ∈ ini_{Z}(F). It represents the set of partial failure traces of a stable process P derivable by the first and fourth rule of Table 3 when F ⊆ F T^{∗}(P) and I(P) = Z.

Theorem 5 Rooted partial failure trace equivalence (≡_{F T}^{r∗}) is a congruence for the operators of CCSP_{t}.

Proof: It suffices to show that F T^{r∗}(P + Q) is fully determined by F T^{r∗}(P) and F T^{r∗}(Q), that F T^{r∗}(α.P) is fully determined by α and F T^{r∗}(P), and similarly for F T^{r∗}(P ∥_{S} Q), F T^{r∗}(τ_{I}(P)) and F T^{r∗}(R(P)). The following equations establish this.

F T^{r∗}(a.P) = ini_{{a}}({aσ | σ ∈ F T^{∗}(P)}) ∪ {stab }  (10)
F T^{r∗}(τ.P) = F T^{∗}(P) ∪ {poststab | ∅⊤ ∈ F T^{∗}(P)}  (11)

F T^{r∗}(t.P) = ini_{∅}({Xσ | Xσ ∈ F T^{∗}(P)} ∪ {Xaσ | aσ ∈ F T^{∗}(P) ∧ a ∈ X})

∪ {stab } ∪ {tXσ | Xσ ∈ F T^{∗}(P)}

(12)

F T^{r∗}(P + Q) = \begin{cases}F T^{r∗}(P) ∪ F T^{r∗}(Q) & if ¬stable(P) ∧ ¬stable(Q) \\ \{aσ | aσ ∈ F T^{r∗}(P)\} ∪ F T^{r∗}(Q) & if stable(P) ∧ ¬stable(Q) \\ F T^{r∗}(P) ∪ \{aσ | aσ ∈ F T^{r∗}(Q)\} & if ¬stable(P) ∧ stable(Q) \\ ini_{I(P)∪I(Q)}(H) ∪ \{stab \} ∪ K & if stable(P) ∧ stable(Q) \end{cases}  (13)

F T^{r∗}(P ∥_{S} Q) = col(F T^{r∗}(P) ∥_{S} F T^{r∗}(Q))  (14)

F T^{r∗}(τ_{I}(P)) = {σ | (stab ≠ σ ≠ poststab ) ∧ ∃ρ ∈ F T^{r∗}(P). τ_{I}(ρ) = σ ∪ I}

∪ {stab | stab ∈ F T^{r∗}(P) ∧ I(P) ∩ I = ∅}

∪ \{poststab | \begin{matrix}(∃c_{0}c_{1} … c_{n}I⊤ ∈ F T^{r∗}(P) where n ≥ 0 and all c_{i} ∈ I) \\ ∨ (poststab ∈ F T^{r∗}(P) ∧ I⊤ ∈ F T^{r∗}(P))\} \end{matrix}

(15)

F T^{r∗}(R(P)) = {σ | ∃ρ ∈ F T^{r∗}(P). ρ ∈ R^{−1}(σ)}  (16)

Here H := \begin{matrix}\{aσ | aσ ∈ F T^{r∗}(P) ∪ F T^{r∗}(Q)\} ∪ \\ \{Xσ | tXσ ∈ F T^{r∗}(P) ∪ F T^{r∗}(Q) ∧ (I(P) ∪ I(Q)) ∩ X = ∅\} ∪ \\ \{Xaσ | Xaσ ∈ F T^{r∗}(P) ∪ F T^{r∗}(Q) ∧ a ∈ X ∧ (I(P) ∪ I(Q)) ∩ X = ∅\} \end{matrix}

and K = {tXσ | tXσ ∈ F T^{r∗}(P) ∪ F T^{r∗}(Q) ∧ (I(P) ∪ I(Q)) ∩ X = ∅}.

The first four equations follow immediately from Definition 9 and Table 3. In (12) the argument of ini_{∅} generates the partial failure traces contributed by the fifth and sixth rule of Table 3; the operation ini_{∅} then closes this set under applications of the first and fourth rule. In the fourth case of (13), the three lines of H generate the partial failure traces contributed by the second, fifth and sixth rule of Table 3, respectively; the operation ini_{I(P)∪I(Q)} then closes this set under applications of the first and fourth rule.

To see that (10)–(13) fulfil their intended purpose, note that F T^{∗}(P) is fully determined by F T^{r∗}(P), namely by dropping the bits stab and poststab , and all traces tσ. Moreover stable(P) holds iff stab ∈ F T^{r∗}(P) and for stable P the set I(P) can be computed by I(P) = {a ∈ A | ∃σ. aσ ∈ F T^{r∗}(P)}.

To explain (14), the definition of decomposition needs to be extended to rooted partial failure traces tXσ. In the first bullet-point of Definition 8, “σ_{i} ∈ A \ S” should now be read as “σ_{i} ∈ (A \ S) ∪ {t}”. The definition of F ∥_{S} G is unchanged, except that rooted partial failure traces tXσ are dropped from F ∥_{S} G unless stab ∈ F and stab ∈ G; furthermore stab is deemed to be in F ∥_{S} G iff it is in both F and G, and poststab is deemed to be in F ∥_{S} G if either poststab ∈ F ∧ poststab ∈ G, or poststab ∈ F ∧ stab ∈ G, or stab ∈ F ∧ poststab ∈ G. Moreover, the operator col extends to sets of rooted partial failure traces. In the appendix it is shown that with these definitions (14) holds—see Proposition 4.

In (15), the concept “survives abstraction from I ⊆ A” from the proof of Theorem 3 is applied verbatim to rooted partial failure traces tXσ, as is the operation τ_{I}. The validity of (15) is shown in the appendix—Proposition 5.

In (16), the operator R^{−1} extends verbatim to rooted partial failure traces. The validity of (15) is shown in the appendix—Proposition 6. □

As remarked in [8], the countable choice operator ∑_{i∈ℕ} P_{i} is expressible in terms of the binary choice operator + and recursion: ∑_{i∈ℕ} P_{i} = ^{/} \X_{0}|S^{\} /, where X_{i} = P_{i} + X_{i+1} for i ∈ ℕ. An equation similar to (13) shows that ≡_{F T}^{r∗} also is a congruence for the countable choice.

Theorem 6 Rooted partial failure trace equivalence (≡_{F T}^{r∗}) is the largest congruence for the operators of CCSP_{t} that is included in ≡_{F T}^{∗}.

Proof: In view of Observation 2 and Theorem 5 it suffices to find, for any two rooted partial failure trace inequivalent processes P ≢_{F T}^{r∗} Q, a CCSP_{t}-context C such that C(P) ≢_{F T}^{∗} C(Q).

First of all, one can apply a bijective renaming operator on P and Q, mapping A to A \ {f} for some action f ∈ A. Consequently, I may assume that f is fresh in the sense that for each process R reachable from P or Q one has R−↛^{f}. For any such R one has σXρ ∈ F T^{∗}(R) ⇔ σ(X∪{f})ρ ∈ F T^{∗}(R). (*)

Let σ ∈ F T^{r∗}(Q) \ F T^{r∗}(P). (The other case proceeds by symmetry.) The only relevant cases are that σ = (post) stab or σ = tXρ, since in all other cases one immediately has σ ∈ F T^{∗}(Q) \ F T^{∗}(P).

Let σ = stab , that is, Q is stable but P is not. Then ∅f⊤ ∈ F T^{∗}(Q + f) but ∅f⊤ ∉ F T^{∗}(P + f). So it suffices to take the context C( ) = + f.

Now let σ = tXρ. So Q−↛^{α} for all α ∈ X ∪ {τ}, Q ⟶^{t} Q′ and Xρ ∈ F T^{∗}(Q′). I may assume that P is stable, as the case that Q is stable but P is not has been treated already. By Observation 1 one has XXρ ∈ F T^{∗}(Q′), and (*) yields X^{−}X^{+}ρ ∈ F T^{∗}(Q′), where X^{−} := X \ {f} and X^{+} := X ∪ {f}. The fifth rule of Table 3 gives X^{−}X^{+}ρ ∈ F T^{∗}(Q+f), using that Q+f−↛^{α} for all α ∈ X^{−} ∪ {τ}. It suffices to show that X^{−}X^{+}ρ ∉ F T^{∗}(P +f), for then the context C( ) = + f finishes the proof.

So assume, towards a contradiction, that X^{−}X^{+}ρ ∈ F T^{∗}(P +f). This could not have been derived by the fourth rule of Table 3, since surely X^{+}ρ ∉ F T^{∗}(P +f). Hence the fifth rule must have been used,

so that P −↛^{α} for all α ∈ X ∪ {τ}, P ⟶^{t} P′ and X^{−}X^{+}ρ ∈ F T^{∗}(P′). Now XXρ ∈ F T^{∗}(P′) by (*),

and Xρ ∈ F T^{∗}(P′) by Observation 1. Therefore tXρ ∈ F T^{r∗}(P), yielding the required contradiction. Finally, let σ = poststab . Then {f}⊤ ∈ F T^{∗}(Q + f), yet {f}⊤ ∉ F T^{∗}(P + f). □

In the quest for a congruence, an alternative solution to changing partial failure trace equivalence into rooted partial failure trace equivalence, is to restrict the expressiveness of CCSP_{t}. Let CCSP_{t}^{g} be the version of CCSP_{t} where the binary operator + is replaced by guarded sums ∑_{i=1}^{n} α_{i}.P_{i}, for n∈ℕ∪{∞}. Here each guarded sum ∑_{i=1}^{n} α_{i}. counts as a separate n-ary operator. The constant 0 and action prefixing α.P are the special cases with n = 0 and n = 1. The congruence property for guarded sums demands that P_{i} ≡_{F T}^{∗} Q_{i} for i = 1, …, n implies ∑_{i=1}^{n} α_{i}.P_{i} = ∑_{i=1}^{n} α_{i}.Q_{i}. That this holds is an immediately consequence of Theorem 7 below.

7 Partial failure trace preorders

Here I introduce (rooted) partial failure trace preorders ⊑_{F T}^{∗} and ⊑_{F T}^{r∗} in such a way that (rooted) partial failure trace equivalence is its kernel, i.e., P ≡_{F T}^{∗} Q ⇔ (P ⊑_{F T}^{∗} Q ∧ Q ⊑_{F T}^{∗} P) and, likewise, P ≡_{F T}^{r∗} Q ⇔ (P ⊑_{F T}^{r∗} Q ∧ Q ⊑_{F T}^{r∗} P). These preorders should be defined in such a way that they are precongruences.

Definition 10 Write P ⊑_{F T}^{∗} Q, for processes P, Q ∈ ℙ, iff F T^{∗}(P) ⊇ F T^{∗}(Q).

The orientation of the symbol ⊑_{F T}^{∗} aligns with that of the safety preorder, discussed in the next section. The following proposition says that the preorder ⊑_{F T}^{∗} is a precongruence for the operators of CCSP_{t}^{g}, or that recursion-free CCSP_{t}^{g}-contexts are monotone w.r.t. ⊑_{F T}^{∗}.

Theorem 7 Let C be a unary recursion-free CCSP_{t}^{g}-context. If P ⊑_{F T}^{∗} Q then C(P) ⊑_{F T}^{∗} C(Q).

Proof: Let G := ∑_{i∈I} α.P_{i}. In case α_{i} ≠ τ for all i ∈ I, then (10)–(13) imply (or generalise to)

F T^{∗}(G) = ini_{I(G)}( ⋃_{\begin{matrix}i∈I \\ α_{i}∈A \end{matrix}}\{α_{i}σ | σ ∈ F T^{∗}(P_{i})\} ∪ ⋃_{\begin{matrix}i∈I \\ α_{i}=t \end{matrix}} (\begin{matrix}\{Xσ | Xσ ∈ F T^{∗}(P_{i}) ∧ I(G) ∩ X = ∅\} ∪ \\ \{Xaσ | aσ ∈ F T^{∗}(P_{i}) ∧ I(G) ∩ X = ∅ ∧ a ∈ X\} \end{matrix})).

Here I(G) := {α_{i} | i ∈ I} \ {t}. Moreover, if α_{i} = τ for at least one i ∈ I, then

F T^{∗}(G) = ⋃_{\begin{matrix}i∈I \\ α_{i}∈A \end{matrix}}\{α_{i}σ | σ ∈ F T^{∗}(P_{i})\} ∪ ⋃_{\begin{matrix}i∈I \\ α_{i}=τ \end{matrix}} F T^{∗}(P_{i}) .

There equations immediately imply the monotonicity of the guarded choice operators w.r.t. ⊑_{F T}^{∗}. The monotonicity of ∥_{S}, τ_{I} and R follows from Properties (4), (8) and (9). □

Definition 11 Write P ⊑_{F T}^{r∗} Q, for P, Q ∈ ℙ, iff F T^{r∗}(P) ⊇ F T^{r∗}(Q).

In this definition, the poststab bit of Definition 9 plays a crucial rôle. Without it, we would have b ⊑_{F T}^{r∗} τ.b, since F T^{r∗}(b) = F T^{r∗}(τ.b) ⊎ {stab }. This would cause a failure of monotonicity, as a + b ⋢_{F T}^{r∗} a + τ.b, for only the latter process has a partial failure trace {a}⊤. With the poststab bit one obtains b ⋢_{F T}^{r∗} τ.b, since poststab ∈ F T^{r∗}(τ.b), yet poststab ∉ F T^{r∗}(b). The preorder ⊑_{F T}^{r∗} still relates processes of which only one is stable; for instance b ⊑_{F T}^{r∗} ^{/} \X|X = b + τ.X^{\} /.

Lemma 1 If P ⊑_{F T}^{r∗} Q (or P ⊑_{F T}^{∗} Q) and P and Q are both stable, then I(P) = I(Q).

Proof: If a ∈ I(Q) then a⊤ ∈ F T^{r∗}(Q) ⊆ F T^{r∗}(P), so a ∈ I(P). Moreover, if a ∉ I(Q) then {a}⊤ ∈ F T^{r∗}(Q) ⊆ F T^{r∗}(P), so a ∉ I(P). □

Theorem 8 Let C be a unary recursion-free CCSP_{t}-context. If P ⊑_{F T}^{r∗} Q then C(P) ⊑_{F T}^{r∗} C(Q).

Proof: The monotonicity of ∥_{S}, τ_{I} and R follows from Properties (14)–(16), using Lemma 1. The monotonicity of α. follows from (10)–(12), using that F T^{r∗}(P) ⊇ F T^{r∗}(Q) implies F T^{∗}(P) ⊇ F T^{∗}(Q).

The monotonicity of + can be formulated as P ⊑_{F T}^{r∗} Q ⇒ P + R ⊑_{F T}^{r∗} Q + R (the requirement R + P ⊑_{F T}^{r∗} R + Q then follows by symmetry). So let P ⊑_{F T}^{r∗} Q, i.e., F T^{r∗}(P) ⊇ F T^{r∗}(Q).

• Let ¬stable(P) and ¬stable(R). Then stab ∉ F T^{r∗}(P) ⊇ F T^{r∗}(Q), so ¬stable(Q). Hence

F T^{r∗}(P + R) = F T^{r∗}(P) ∪ F T^{r∗}(R) ⊇ F T^{r∗}(Q) ∪ F T^{r∗}(R) = F T^{r∗}(Q + R).

• The case ¬stable(P) and stable(R) proceeds likewise.

In all remaining cases I assume stable(P). Note that poststab ∉ F T^{r∗}(P) ⊇ F T^{r∗}(Q).

• Let stable(Q) and ¬stable(R). Then F T^{r∗}(P + R) = {aσ | aσ ∈ F T^{r∗}(P)} ∪ F T^{r∗}(R) ⊇ {aσ | aσ ∈ F T^{r∗}(Q)} ∪ F T^{r∗}(R) = F T^{r∗}(Q + R).

• Let ¬stable(Q) and ¬stable(R). Now all σ ∈ F T^{r∗}(Q) must have the form ⊤ or aζ. Namely if Xζ ∈ F T^{r∗}(Q) then one would have poststab ∈ F T^{r∗}(Q). Hence

F T^{r∗}(P + R) = {aσ | aσ ∈ F T^{r∗}(P)} ∪ F T^{r∗}(R) ⊇ F T^{r∗}(Q) ∪ F T^{r∗}(R) = F T^{r∗}(Q + R).

• Let stable(Q) and stable(R). Then I(P) = I(Q) by Lemma 1. Using this, the desired monotonicity property follows from the fourth case of (13).

• Let ¬stable(Q) and stable(R). Again all σ ∈ F T^{r∗}(Q) must have the form ⊤ or aζ. Let H and K be as in (13), but with R substituted for Q. Now F T^{r∗}(P +R) = ini_{I(P)∪I(Q)}(H)∪{stab }∪K ⊇ H ∪ {⊤} ⊇ F T^{r∗}(Q) ∪ {aσ | aσ ∈ F T^{r∗}(R)} = F T^{r∗}(Q + R). □

Theorem 9 ⊑_{F T}^{r∗} is the largest precongruence for the operators of CCSP_{t} that is included in ⊑_{F T}^{∗}.

Proof: Theorem 8 shows that ⊑_{F T}^{r∗} is a precongruence for the operators of CCSP_{t}. By Definition 9, ⊑_{F T}^{r∗} is included in ⊑_{F T}^{∗}, i.e., P ⊑_{F T}^{r∗} Q implies P ⊑_{F T}^{∗} Q. Thus it suffices to find, for any two processes P and Q with P ⋢_{F T}^{r∗} Q, a CCSP_{t}-context C such that C(P) ⋢_{F T}^{∗} C(Q). This proceeds exactly as in the proof of Theorem 6. Of course the symmetric case “σ ∈ F T^{r∗}(P) \ F T^{r∗}(Q)” is skipped, as it is not needed here. □

8 The coarsest precongruence respecting safety properties

In [11] I proposed a way to define refinement preorders ⊑ on processes, where P ⊑ Q says that for all practical purposes under consideration, Q is at least as suitable as P, i.e., it will never harm to replace P by Q. In the stepwise design of systems, P may be closer to a specification, and Q to an implementation. Each such a refinement preorder also yields a semantic equivalence ≡, with P ≡ Q saying that for practical purposes P and Q are equally suitable; i.e., one can be replaced by the other without untoward side effects. Naturally, P ≡ Q iff both P ⊑ Q and Q ⊑ P.

The method of [11] equips the choice of ⊑ with two parameters: a class G of good properties of processes, ones that may be required of processes in a given range of applications, and a class O of useful operators for combining processes. The first requirement on ⊑ is P ⊑ Q ⇒ ∀φ ∈ G . (P ⊧ φ ⇒ Q ⊧ φ) where P ⊧ φ denotes that process P has the property φ. If this holds, ⊑ respects or preserves the properties in G. The second requirement is that ⊑ is a precongruence for O: P ⊑ Q ⇒ C[P] ⊑ C[Q] for any context C[ ] built from operators from O. Given the choice of G and O, the preorder recommended by [11] is the coarsest, or largest, one satisfying both requirements. This preorder is called fully abstract w.r.t. G and O, and is characterised by

P ⊑ Q ⇔ ∀O-context C[ ]. ∀φ ∈ G . (C[P] ⊧ φ ⇒ C[Q] ⊧ φ).

The corresponding semantic equivalence identifies processes only when this is enforced by the two requirements above.

Naturally, increasing the class O of operators makes the resulting fully abstract preorder finer, or smaller. The same holds when increasing the class G of properties. In [11] I employed a class O of operators that was effectively equivalent to the operators of CCSP^{g}. Here I use the operators of CCSP_{t}^{g}, thus adding time-outs. In this section, following [11, Section 3], I take as class G of good properties the safety properties, saying that something bad will never happen. What exactly counts as a safety property could be open to some debate. However, the canonical safety property, proposed in [11], is definitely in this class. I first characterise the preorder ⊑_{safety} that is fully abstract w.r.t. the operators of CCSP_{t}^{g} and this single safety property. It turns out to be ⊑_{F T}^{∗}. Then I argue that adding any other safety properties to the class G could not possible make the resulting preorder any finer. An immediately corollary of this and Theorem 9 is that ⊑_{F T}^{r∗} is fully abstract for the operators of CCSP_{t} and the class of safety properties.

Full abstraction w.r.t. the canonical safety property

To formulate the canonical safety property, assume that the alphabet A of visible actions contains one specific action b, whose occurrence is bad. The property now says that b will never happen.

Definition 12 A process P satisfies the canonical safety property, notation P ⊧ safety(b), if no partial failure trace of P contains the action b.

Lemma 2 If aη ∈ F T^{∗}(P) then P ⟶^{a} or P ⟶^{τ}.

Proof: That aη ∈ F T^{∗}(P) can be derived only from the second or third rule of Table 3. □

Corollary 1 If Xaη ∈ F T^{∗}(P) is obtained from the fourth rule of Table 3, then a ∉ X.

Proof: The fourth rule requires that P −↛^{α} for all α ∈ X ∪ {τ}, and that aη ∈ F T^{∗}(P). The latter implies P ⟶^{a} or P ⟶^{τ} by Lemma 2. So P ⟶^{a} and a ∉ X. □

As encountered already in the proof of Theorem 6, I call an action b fresh for a process P if for each process R reachable from P one has R−↛^{b}. In that case P ⊧ safety(b). I call it fresh for a partial failure trace σ ∈ (A ∪ P(A))^{∗}⊤ if b does not occur in σ, either as action or inside a refusal set in σ.

Theorem 10 For each σ ∈ (A ∪ P(A))^{∗}⊤ for which b is fresh, there exists a CCSP_{t}^{g} process T_{σ} such

that τ_{A\{b}}(T_{σ} ∥_{A\{b}} P) |̸= safety(b) ⇔ σ ∈ F T^{∗}(P)

for each CCSP_{t}^{g} process P for which b is fresh.

Proof: Let B := A\{b}, the set of all visible actions except b. Define T_{σ} with structural induction on σ:

T_{⊤} := t.b T_{cρ} := τ + c.T_{ρ} T_{Xη} := t.T_{η} + ∑_{a∈X} a T_{Xdρ} := t.(d.T_{ρ} + ∑_{a∈X\{d}} a) + ∑_{a∈X} a

where, c, d ∈ B, X ⊆ B, d ∈ X, and η is not of the form dρ with d ∈ X. Note that τ_{B}(T_{σ} ∥_{B} P) |̸= safety(b) iff there is a path π := τ_{B}(T_{ρ} ∥_{B} P) ⟶^{α_{1}} Q_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} Q_{ℓ} ⟶^{b} Q′, and this path gives rise to a partial failure trace βb⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)) by application of the rules of Table 3. Due to the operator τ_{B}, each of the α_{i} must be τ or t.

To obtain “⇒” I assume τ_{B}(T_{σ} ∥_{B} P) |̸= safety(b) and apply structural induction on σ.

• Let σ = ⊤. Then σ ∈ F T^{∗}(P) for all P.

• Let σ = cρ. For the process τ_{B}(T_{σ} ∥_{B} P) to ever reach a b-transition, the component T_{σ} = τ +c.T_{ρ} must take the c-transition to T_{ρ}. So the beginning of π must have the form

τ_{B}(T_{σ} ∥_{B} P) ⟶^{α_{1}} τ_{B}(T_{σ} ∥_{B} P_{1}) ⟶^{α_{2}} ⋯ ⟶^{α_{n}} τ_{B}(T_{σ} ∥_{B} P_{n}) ⟶^{τ} τ_{B}(T_{ρ} ∥_{B} P′)

for some n ≥ 0, where τ_{B}(T_{ρ} ∥_{B} P′) |̸= safety(b). Let P_{0} := P. All of these α_{i} must be τ, for t-transitions lose out from the outgoing τ-transition from τ_{B}(T_{σ} ∥_{B} P_{i−1}). Technically, if α_{i} = t, for 1 ≤ i ≤ n, then the fifth and sixth rules of Table 3 do not allow any partial failure trace of τ_{B}(T_{ρ} ∥_{B} P_{i}) to give rise to a partial failure trace of τ_{B}(T_{σ} ∥_{B} P_{i−1}). The above path must stem from a path

T_{σ} ∥_{B} P ⟶^{β_{1}} T_{σ} ∥_{B} P_{1} ⟶^{β_{2}} ⋯ ⟶^{β_{n}} T_{σ} ∥_{B} P_{n} ⟶^{c} T_{ρ} ∥_{B} P′

that in turns stems from a path P ⟶^{β_{1}} P_{1} ⟶^{β_{2}} ⋯ ⟶^{β_{n}} P_{n} ⟶^{c} P′. All of these β_{i} must be τ, as the synchronisation on B stops all visible actions stemming from P. By induction ρ ∈ F T^{∗}(P′). The second and third rules of Table 3 yield σ ∈ F T^{∗}(P).

• Let σ = Xη, where X ⊆ B and η is not of the form dρ with d ∈ X. For the process τ_{B}(T_{σ} ∥_{B} P) to ever reach a b-transition, the component T_{σ} = t.T_{η} + ∑_{a∈X} a must take the t-transition to T_{η}. So the beginning of π must have the form

τ_{B}(T_{σ} ∥_{B} P) ⟶^{α_{1}} τ_{B}(T_{σ} ∥_{B} P_{1}) ⟶^{α_{2}} ⋯ ⟶^{α_{n}} τ_{B}(T_{σ} ∥_{B} P_{n}) ⟶^{t} τ_{B}(T_{η} ∥_{B} P_{n})

for some n ≥ 0, where τ_{B}(T_{η} ∥_{B} P_{n}) |̸= safety(b). By induction η ∈ F T^{∗}(P_{n}). As above, again using that visible actions from P are blocked by ∥_{B}, it must be that P ⟶^{α_{1}} P_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} P_{n}. I proceed with induction on n. Base case: It must be that P = P_{n}−↛^{α} for all α ∈ X ∪ {τ}, for otherwise τ_{B}(T_{σ} ∥_{B} P_{n}) would have an outgoing τ-transition that wins from the t-transition to τ_{B}(T_{η} ∥_{B} P_{n}). The fourth rule of Table 3 yields σ ∈ F T^{∗}(P). Induction step: By induction σ ∈ F T^{∗}(P_{1}). In case α_{1} = τ one obtains σ ∈ F T^{∗}(P) by the third rule of Table 3. In case α_{1} = t, it must be that P −↛^{α} for all α ∈ X ∪ {τ}, for otherwise τ_{B}(T_{σ} ∥_{B} P) would have an outgoing τ-transition that wins from the t-transition to τ_{B}(T_{σ} ∥_{B} P_{1}). The fifth rule of Table 3 yields σ ∈ F T^{∗}(P).

• Let σ = Xdρ with d ∈ X. Writing R for d.T_{ρ} + ∑_{a∈X\{d}} a, the first part of π must have the form

τ_{B}(T_{σ} ∥_{B} P) ⟶^{α_{1}} τ_{B}(T_{σ} ∥_{B} P_{1}) ⟶^{α_{2}} ⋯ ⟶^{α_{n}} τ_{B}(T_{σ} ∥_{B} P_{n}) ⟶^{t} τ_{B}(R ∥_{B} P_{n})

τ_{B}(R ∥_{B} P_{n}) ⟶^{α_{n+1}} τ_{B}(R ∥_{B} P_{n+1}) ⟶^{α_{n+2}} ⋯ ⟶^{α_{m}} τ_{B}(R ∥_{B} P_{m}) ⟶^{τ} τ_{B}(T_{ρ} ∥_{B} P′)

for some m ≥ n ≥ 0, where τ_{B}(T_{ρ} ∥_{B} P′) |̸= safety(b). By induction ρ ∈ F T^{∗}(P′). As above,

it must be that P ⟶^{α_{1}} P_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} P_{n} ⟶^{α_{n+1}} P_{n+1} ⟶^{α_{n+2}} ⋯ ⟶^{α_{m}} P_{m} ⟶^{d} P′. Necessarily,

P_{n}−↛^{α} for all α ∈ X ∪ {τ}, for otherwise τ_{B}(T_{σ} ∥_{B} P_{n}) would have an outgoing τ-transition that wins from the t-transition to τ_{B}(R ∥_{B} P_{n}). In particular, P_{n}−↛^{d}, whereas P_{m}⟶^{d}, so n ≠ m. Moreover, α_{n+1} = t, for α_{n+1} = τ contradicts with P_{n}−↛^{τ}. Let k ≤ m be the highest index such that α_{k} = t. Then dρ ∈ F T^{∗}(P_{k}), by the second and third rules of Table 3. For each index i with α_{i} = t one must have P_{i−1}−↛^{α} for all α ∈ X ∪ {τ}, for the same reason as above. The sixth rule of Table 3 yields Xdρ ∈ F T^{∗}(P_{k−1}). Successive applications of the third and fifth rules yield Xdρ ∈ F T^{∗}(P_{j}) for all j < k, so in particular σ ∈ F T^{∗}(P).

To obtain “⇐”, I will show that σ ∈ F T^{∗}(P) implies Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)). Here A is the set of all visible actions. In doing so, I apply induction on the derivation of σ ∈ F T^{∗}(P).

Suppose σ = ⊤ ∈ F T^{∗}(P) is derived from the first rule of Table 3. Since T_{σ} = t.b.0 one has

τ_{B}(T_{σ} ∥_{B} P) ⟶^{t} τ_{B}(b.0 ∥_{B} P) ⟶^{b} τ_{B}(0 ∥_{B} P). Hence Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)), using the first,

second and sixth rules of Table 3, and using that τ_{B}(T_{σ} ∥_{B} P)−↛^{α} for all α ∈ A ∪ {τ}.

Suppose σ = cρ ∈ F T^{∗}(P) is derived from the second rule of Table 3. Then P ⟶^{c} P′ and

ρ ∈ F T^{∗}(P′). By induction, Ab⊤ ∈ F T^{∗}(τ_{B}(T_{ρ} ∥_{B} P′)). Since τ_{B}(T_{σ} ∥_{B} P) ⟶^{τ} τ_{B}(T_{ρ} ∥_{B} P′), it

follows with the third rule of Table 3 that Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)).

Suppose σ ∈ F T^{∗}(P) is derived from the third rule of Table 3. Then P ⟶^{τ} P′ and σ ∈ F T^{∗}(P′). By induction, Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P′)). Since τ_{B}(T_{σ} ∥_{B} P) ⟶^{τ} τ_{B}(T_{σ} ∥_{B} P′), it follows with the third rule of Table 3 that Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)).

Suppose σ =Xη ∈F T^{∗}(P) is derived from the fourth rule of Table 3. Then P −↛^{α} for all α∈X ∪{τ} and η ∈ F T^{∗}(P). In the special case that η = dρ, by Corollary 1 d ∉ X. By induction Ab⊤ ∈

F T^{∗}(τ_{B}(T_{η} ∥_{B} P)). Since τ_{B}(T_{σ} ∥_{B} P) ⟶^{t} τ_{B}(T_{η} ∥_{B} P), and τ_{B}(T_{σ} ∥_{B} P)−↛^{α} for all α ∈ A ∪ {τ},

the fifth rule of Table 3 yields Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)).

Suppose σ = Xη ∈ F T^{∗}(P) is derived from the fifth rule of Table 3. Then P −↛^{α} for all α ∈ X ∪ {τ},

P ⟶^{t} P′ and σ ∈ F T^{∗}(P′). So τ_{B}(T_{σ} ∥_{B} P)−↛^{α} for all α ∈ A ∪ {τ}, and Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P′))

by induction. Since τ_{B}(T_{σ} ∥_{B} P) ⟶^{t} τ_{B}(T_{σ} ∥_{B} P′), the fifth rule yields Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)).

Suppose σ=Xdρ∈F T^{∗}(P) is derived from the sixth rule of Table 3. Then P −↛^{α} for all α∈X ∪{τ},

d∈X, P ⟶^{t} P′ and dρ ∈ F T^{∗}(P′). So τ_{B}(T_{σ} ∥_{B} P)−↛^{α} and τ_{B}(R∥_{B} P)−↛^{α} for all α ∈ A∪{τ}, where

R := d.T_{ρ} + ∑_{a∈X\{d}} a. By induction Ab⊤ ∈ F T^{∗}(τ_{B}(T_{dρ} ∥_{B} P′)). As τ_{B}(T_{σ} ∥_{B} P) ⟶^{t} τ_{B}(R ∥_{B} P)

⟶^{t} τ_{B}(R ∥_{B} P′), two applications of the fifth rule of Table 3 yield Ab⊤ ∈ F T^{∗}(τ_{B}(T_{σ} ∥_{B} P)). □

Corollary 2 ⊑_{F T}^{∗} is fully abstract w.r.t. the operators of CCSP_{t}^{g} and the canonical safety property.

Proof: By Theorem 7, ⊑_{F T}^{∗} is a precongruence for the operators of CCSP_{t}^{g}. By definition, P ⊑_{F T}^{∗} Q implies P ⊧ safety(b) ⇒ Q ⊧ safety(b). It remains to show that ⊑_{F T}^{∗} is the coarsest preorder with these properties. To this end it suffices to find for any processes P and Q with P ⋢_{F T}^{∗} Q a recursion-free CCSP_{t}^{g}-context C[ ] such that C[P] ⊧ safety(b), yet C[Q] |̸= safety(b).

So assume P ⋢_{F T}^{∗} Q. By applying a bijective renaming operator on P and Q, mapping A to A\{b}, I may assume that b is fresh for P and Q. Take σ ∈ F T^{∗}(Q) \ F T^{∗}(P). By Property (*) in the proof of Theorem 6 I may assume that b is fresh for σ. Now Theorem 10 yields τ_{A\{b}}(T_{σ} ∥_{A\{b}} P) ⊧ safety(b), yet τ_{A\{b}}(T_{σ} ∥_{A\{b}} Q) |̸= safety(b). □

Full abstraction w.r.t. general safety properties

The above says that the unique preorder ⊑_{safety} that is fully abstract w.r.t. the operators of CCSP_{t}^{g} and the canonical safety property coincides with ⊑_{F T}^{∗}. Without the time-out operator, ⊑_{safety} would be way less discriminating, and coincides with reverse weak partial trace inclusion [11]. I now check whether one could get an even finer preorder than ⊑_{F T}^{∗} by also considering other safety properties.

To arrive at a general concept of safety property for LTSs, the paper [11] assumes that some notion of bad is defined. This induces the safety property saying that this bad thing will never happen. To judge whether a process P satisfies this safety property, one should judge whether P can reach a state in which one would say that this bad thing had happened. But all observable behaviour of P that is recorded in an LTS until one comes to such a verdict, is the sequence of visible actions performed until that point. Thus the safety property is completely determined by the set sequences of visible actions that, when performed by P, lead to such a judgement. Therefore, [11] proposes to define the concept of a safety property in terms of such a set: a safety property is given by a set B ⊆ A^{∗} of bad partial traces. A process P satisfies this property, notation P ⊧ safety(B), if P has no partial trace in B. It follows immediately from this definition that partial trace equivalent processes satisfy the same safety properties of this kind.

The present paper allows for a stronger concept of safety property. Here the observable behaviour of a process that is recorded until one comes to the verdict that something bad has happened can be modelled as a partial failure trace. Based on this, my definition is analogous to the one in [11]: Definition 13 A safety property of CCSP_{t} processes is given by a set B ⊆ (A∪P(A))^{∗}⊤ of bad partial failure traces. A process P satisfies this property, notation P ⊧ safety(B), if F T^{∗}(P) ∩ B = ∅. It follows immediately that ⊑_{F T}^{∗} respects all safety properties. Consequently, as in [11], for the definition of ⊑_{safety} it does not matter whether all safety properties are considered, or only the canonical one.

Trace equivalence and its congruence closure

A possible definition of a (weak) partial trace is simply a partial failure trace from which all refusal sets have been omitted. Define two processes to be (weak) (partial) trace equivalent iff they have the same partial traces. Now Corollary 2 implies that ≡_{F T}^{∗} is the congruence closure of trace equivalence, that is, the coarsest congruence for the operators of CCSP_{t} that is finer than trace equivalence.

May testing

May testing was proposed by De Nicola & Hennessy in [6] for the process algebra CCS. Translated to CCSP_{t} it works as follows. A test is a CCSP_{t} process that instead of visible actions from the alphabet A, uses visible actions from the alphabet A ⊎ {ω}, where ω is a fresh action reporting “success”. A process P may pass a test T iff τ_{A}(T ∥_{A} P) has some partial failure trace βω⊤, or, equivalently, has a partial trace containing the action ω. A process with such a trace represents a system with an execution that eventually reports success. Now define the preorder ⊑_{may} on CCSP_{t} processes by

P ⊑_{may} Q iff each test T that P may pass, may also be passed by Q.

May testing contrasts with must testing, which requires that each execution leads to a state that can report success.

Theorem 11 P ⊑_{may} Q iff Q ⊑_{F T}^{∗} P.

Proof: Note that R has some partial failure trace βω⊤ iff R |̸= safety(ω). Using this, Theorem 11 is an immediately consequence of Theorem 10, with ω in the rôle of b. The side conditions of b being fresh in Theorem 10 are redundant in this context, as ω is fresh by construction. □

So the may-preorder is the converse of the safety preorder. This is related to calling ω a success action, instead of b a bad action. The may-preorder preserves the property that a process can do something good, whereas the safety preorder preserves the property that a process can not so something bad.

9 Conclusion

This paper extended the model of labelled transition systems with time-out transitions s_{1} ⟶^{t} s_{2}. Such a transition is assumed to be instantaneous and unobservable by the environment, just like a transition s_{1} ⟶^{τ} s_{2}, but becomes available only a positive but finite amount of time after the represented system reaches state s_{1}. This extension allows the implementation of a simple priority mechanism, thereby increasing the expressiveness of the model.

To denote such labelled transition systems I extended the standard process algebra CCSP with the action prefixing operator t. . Many semantic preorders ⊑ have been defined on labelled transition systems, and thereby on the expressions in CCSP and other process algebras. P ⊑ Q says that process Q is a refinement of process P, where P is closer to the specification of a system, and Q to its implementation. The least one may wish to require from such a preorder is

(1) that it is a precongruence for the static operators of CCSP: partially synchronous parallel composition, renaming, and abstraction by renaming visible actions into the hidden action τ,

(2) and that it respects (basic) safety properties, meaning that any safety property of a process P also

holds for its refinements Q. The coarsest preorder with these properties is well known to be the reverse weak partial trace inclusion (see e.g. [11]). Accordingly, weak partial trace inclusion is the preorder generated by may testing [6].

After the extension with time-out transitions, the weak partial trace preorder is no longer a precongruence for the static operators of CCSP. I here characterised the coarsest preorder satisfying (1) and (2) above as the partial failure trace preorder. Again, its converse is the preorder generated by may testing. All the above also applies to semantic equivalences, arising as the kernels of these preorders.

To obtain a (pre)congruence for all CCSP operators, including the CCS choice +, one needs to use a rooted version of the partial failure trace preorder, as is common in the study of preorders that abstract from the hidden action τ.

The work reported here remains in the realm of untimed process algebra, in the sense that the progress of time is not quantified. In the study of Timed CSP [32, 5, 34, 33], similar work has been done in a setting where the progress of time is quantified. Also there a form of failure trace semantics was found to be the right equivalence, and the connection with may testing was made in [34]. Since the bookkeeping of time in [32, 5, 34, 33] is strongly interwoven with the formalisation of failure traces, it is not easy to determine whether my semantics can in some way be seen as a abstraction of the one for Timed CCSP, for instance by instantiating each quantified passage of time with a nondeterministic choice allowing any amount of time. This appears to be a question worthy of further research. A contribution of the present work is that the transformation of a failures based semantics of CSP [4, 23] to a failure trace based semantics of Timed CSP [32, 5, 34, 33] is not really necessitated by quantification of time—often seen as the main difference between CSP and Timed CSP—but rather by the introduction of a time-out operator (quantified or not).

Future work includes proving a congruence result for recursion, finding complete axiomatisations, and extending the approach from partial to complete failure traces, so that liveness properties will be respected. In that setting the expressiveness questions of Section 1.4 can be studied. The adaption of strong bisimilarity to the setting with time-out transitions is studied in [15].

28 Failure Trace Semantics for a Process Algebra with Time-outs

References

[1] J.C.M. Baeten (1986): Procesalgebra. Programmatuurkunde, Kluwer, Deventer. In Dutch.

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

[3] J.C.M. Baeten & W.P. Weijland (1990): Process Algebra. Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, doi:10.1017/ CBO9780511624193 .

[4] S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599, doi:10.1145/ 828. 833 .

[5] J. Davies & S.A. Schneider (1995): A brief history of Timed CSP. Theoretical Computer Science 138, pp.

243–271, doi:10.1016/ 0304-3975(94)00169-J .

[6] R. De Nicola & M. Hennessy (1984): Testing equivalences for processes. Theoretical Computer Science 34,

pp. 83–133, doi:10.1016/ 0304-3975(84)90113-0 .

[7] R.J. van Glabbeek (1993): The Linear Time – Branching Time Spectrum II; The semantics of sequential systems with silent moves. In E. Best, editor: Proceedings 4^{th} International Conference on Concurrency Theory, CONCUR’93, LNCS 715, Springer, pp. 66–81, doi:10.1007/ 3-540-57208-2_6.

[8] R.J. van Glabbeek (1994): On the expressiveness of ACP (extended abstract). In A. Ponse, C. Verhoef & S.F.M. van Vlijmen, editors: Proceedings First Workshop on the Algebra of Communicating Processes, ACP’94, Workshops in Computing, Springer, pp. 188–217, doi:10.1007/ 978-1-4471-2120-6_8.

[9] R.J. van Glabbeek (2001): The Linear Time – Branching Time Spectrum I; The Semantics of Concrete, Sequential Processes. In J.A. Bergstra, A. Ponse & S.A. Smolka, editors: Handbook of Process Algebra,

chapter 1, Elsevier, pp. 3–99, doi:10.1016/ B978-044482830-9/  50019-9 .

[10] R.J. van Glabbeek (2005): On Specifying Timeouts. In L. Aceto & A.D. Gordon, editors: Short Contributions from the Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond, PA’05, Electronic Notes in Theoretical Computer Science 162, Elsevier, pp. 112–113, doi:10.1016/ j.entcs. 2005. 12.

083 .

[11] R.J. van Glabbeek (2010): The Coarsest Precongruences Respecting Safety and Liveness Properties. In C.S. Calude & V. Sassone, editors: Proceedings 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS’10); held as part of the World Computer Congress, IFIP 323, Springer, pp. 32–52,

doi:10.1007/ 978-3-642-15240-5_3 . Available at http:// arxiv. org/ abs/ 1007. 5491 .

[12] R.J. van Glabbeek (2017): Lean and Full Congruence Formats for Recursion. In: Proceedings 32^{nd} Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’17, IEEE Computer Society Press, doi:10.

1109/ LICS. 2017. 8005142 . Available at https:// arxiv. org/ abs/ 1704. 03160 .

[13] R.J. van Glabbeek (2018): A Theory of Encodings and Expressiveness. Technical Report, Data61, CSIRO. Available at https:// arxiv. org/ abs/ 1805. 10415 . Extended abstract in: C. Baier and U. Dal Lago, editors: Proceeding 21st International Conference on Foundations of Software Science and Computational Structures, FoSSaCS’18; held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’18, LNCS 10803, Springer, pp. 183-202, doi:10.1007/ 978-3-319-89366-2_10.

[14] R.J. van Glabbeek (2019): Ensuring liveness properties of distributed systems: Open problems. Journal of Logical and Algebraic Methods in Programming 109:100480, doi:10.1016/ j.jlamp. 2019. 100480 .

Available at http:// arxiv. org/ abs/ 1912. 05616 .

[15] R.J. van Glabbeek (2020): Reactive Bisimulation Semantics for a Process Algebra with Time-Outs. In I. Konnov & L. Kovács, editors: Proceedings 31st International Conference on Concurrency Theory, CONCUR’20, Leibniz International Proceedings in Informatics (LIPIcs) 171, Schloss Dagstuhl–Leibniz-Zentrum für Infor-

matik, doi:10.4230/ LIPIcs. CONCUR. 2020. 6.

[16] R.J. van Glabbeek & P. Höfner (2015): CCS: It’s not fair! Fair schedulers cannot be implemented in CCSlike languages even under progress and certain fairness assumptions. Acta Informatica 52(2-3), pp. 175–205,

doi:10.1007/ s00236-015-0221-6 . Available at http:// arxiv. org/ abs/ 1505. 05964 .

R.J. van Glabbeek 29

[17] R.J. van Glabbeek & P. Höfner (2019): Progress, Justness and Fairness. ACM Computing Surveys 52(4):69,

doi:10.1145/ 3329125 . Available at https:// arxiv. org/ abs/ 1810. 07414 .

[18] R.J. van Glabbeek & F.W. Vaandrager (1987): Petri net models for algebraic theories of concurrency (extended abstract). In J.W. de Bakker, A.J. Nijman & P.C. Treleaven, editors: Proceedings PARLE, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, June 1987, Vol. II: Parallel Languages, LNCS 259, Springer, pp. 224–242, doi:10.1007/ 3-540-17945-3_13.

[19] R.J. van Glabbeek & F.W. Vaandrager (1997): The Difference Between Splitting in n and n+1. Information and Computation 136(2), pp. 109–142, doi:10.1006/ inco. 1997. 2634 .

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

[21] J.F. Groote & F.W. Vaandrager (1992): Structured Operational Semantics and Bisimulation as a Congruence. Information and Computation 100(2), pp. 202–260, doi:10.1016/ 0890-5401(92)90013-6 .

[22] C.A.R. Hoare (1980): Communicating sequential processes. In R.M. McKeag & A.M. Macnaghten, editors: On the construction of programs – an advanced course, Cambridge University Press, pp. 229–254.

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

[24] L. Lamport (1977): Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), pp. 125–143, doi:10.1109/ TSE. 1977. 229904 .

[25] K. Middelburg (2017): Personal communication.

[26] R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer, 1980, doi:10.1007/3-540-10235-3.

[27] E.-R. Olderog (1987): Operational Petri net semantics for CCSP. In G. Rozenberg, editor: Advances in Petri Nets 1987, LNCS 266, Springer, pp. 196–223, doi:10.1007/ 3-540-18086-9_27 .

[28] E.-R. Olderog & C.A.R. Hoare (1986): Specification-oriented semantics for communicating processes. Acta Informatica 23, pp. 9–66, doi:10.1007/ BF00268075 .

[29] D.M.R. Park (1981): Concurrency and automata on infinite sequences. In P. Deussen, editor: 5^{th} GI Conference, LNCS 104, Springer, pp. 167–183, doi:10.1007/ BFb0017309 .

[30] J. Parrow (2008): Expressiveness of Process Algebras. Electronic Notes in Theoretical Computer Science

209, pp. 173–186, doi:10.1016/ j.entcs. 2008. 04.011 .

[31] I.C.C. Phillips (1987): Refusal testing. Theoretical Computer Science 50, pp. 241–284, doi:10.1016/

0304-3975(87)90117-4 .

[32] G.M. Reed & A.W. Roscoe (1987): Metric Spaces as Models for Real-Time Concurrency. In M.G. Main, A. Melton, M.W. Mislove & D.A. Schmidt, editors: Proceedings 3rd Workshop on Mathematical Foundations of Programming Language Semantics, Tulane University, New Orleans, Louisiana, USA, April 1987, LNCS 298, Springer, pp. 331–343, doi:10.1007/ 3-540-19020-1_17.

[33] G.M. Reed & A.W. Roscoe (1999): The Timed Failures-Stability Model for CSP. Theoretical Computer Science 211(1-2), pp. 85–127, doi:10.1016/ S0304-3975(98)00214-X .

[34] S.A. Schneider (1995): An Operational Semantics for Timed CSP. Information and Control 116(2), pp.

193–213, doi:10.1006/ inco. 1995. 1014 .

[35] F.W. Vaandrager (1993): Expressiveness Results for Process Algebras. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: Proceedings REX Workshop on Semantics: Foundations and Applications, Beekbergen, The Netherlands, 1992, LNCS 666, Springer, pp. 609–638, doi:10.1007/ 3-540-56596-5_49.

A Proofs of congruence properties

This appendix contains the proofs of the explicit characterisations of the operators ∥_{S}, τ_{I} and R on (rooted) partial failure trace sets: Properties (4), (8), (9), (14), (15) and (16). These are the central parts of the proofs showing that ≡_{F T}^{∗} and ≡_{F T}^{r∗} are congruences for these operators.

Proposition 1 F T^{∗}(P ∥_{S} Q) = col(F T^{∗}(P) ∥_{S} F T^{∗}(Q)).

Proof: “⊇”: Let σ ∈ F T^{∗}(P) ∥_{S} F T^{∗}(Q), and fix a valid decomposition of σ such that σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q). With Observation 1 it suffices to show that σ ∈ F T^{∗}(P ∥_{S} Q). I proceed with structural induction on the derivations of σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q) from the rules in Table 3, making a case distinction on the first symbol of σ. The case σ = ⊤ is trivial.

• Let σ = aρ with a ∈ S. Then σ_{L} = aρ_{L} and σ_{R} = aρ_{R}.

Assume σ_{L} ∈ F T^{∗}(P) is obtained from the third rule of Table 3. Then P ⟶^{τ} P′ and σ_{L} ∈ F T^{∗}(P′). So P ∥_{S} Q ⟶^{τ} P′ ∥_{S} Q by Table 1, and σ ∈ F T^{∗}(P′ ∥_{S} Q) by induction. It follows that σ ∈ F T^{∗}(P ∥_{S} Q). The case that σ_{R} ∈ F T^{∗}(Q) is obtained from the third rule of Table 3 proceeds likewise. So assume σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q) are both obtained from the second rule of Table 3.

Then P ⟶^{a} P′, Q ⟶^{a} Q′, ρ_{L} ∈ F T^{∗}(P′) and ρ_{R} ∈ F T^{∗}(Q′). So P ∥_{S} Q ⟶^{a} P′ ∥_{S} Q′ by

Table 1, and ρ ∈ F T^{∗}(P′ ∥_{S} Q′) by induction. It follows that σ ∈ F T^{∗}(P ∥_{S} Q).

• Let σ = aρ with a ∉ S. Assume that σ_{L} = aρ_{L} and σ_{R} = ρ_{R}—the other case, that σ_{L} = ρ_{L} and σ_{R} = aρ_{R}, will follow by symmetry. Assume σ_{L} ∈ F T^{∗}(P) is obtained from the third rule of Table 3. Then P ⟶^{τ} P′ and σ_{L} ∈ F T^{∗}(P′). So P ∥_{S} Q ⟶^{τ} P′ ∥_{S} Q by Table 1, and σ ∈ F T^{∗}(P′ ∥_{S} Q) by induction. It follows that σ ∈ F T^{∗}(P ∥_{S} Q). Now assume σ_{L} ∈ F T^{∗}(P) is obtained from the second rule of Table 3. Then P ⟶^{a} P′ and ρ_{L} ∈ F T^{∗}(P′). So P ∥_{S} Q ⟶^{a} P′ ∥_{S} Q by Table 1, and ρ ∈ F T^{∗}(P′ ∥_{S} Q) by induction. It follows that σ ∈ F T^{∗}(P ∥_{S} Q).

• Let σ = Xρ. Then σ_{L} = X_{L}ρ_{L} and σ_{R} = X_{R}ρ_{R}. Both these statements must be derived from the fourth to sixth rule of Table 3. Hence P −↛^{α} for all α ∈ X_{L} ∪{τ}, and Q−↛^{α} for all α ∈ X_{R} ∪{τ}. Note that (5)–(7) hold with X, X_{L} and X_{R} in the rôles of σ_{i}, σ_{i}^{L} and σ_{i}^{R}. From (7) it follows that

P ∥_{S} Q−↛^{α} for all α ∈ X ∪ {τ}.

Assume σ_{L} ∈ F T^{∗}(P) is obtained from the fifth rule of Table 3. Then P ⟶^{t} P′ and σ_{L} ∈ F T^{∗}(P′). So P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q by Table 1, and σ ∈ F T^{∗}(P′ ∥_{S} Q) by induction. It follows that σ ∈ F T^{∗}(P ∥_{S} Q). The case that σ_{R} ∈ F T^{∗}(Q) is obtained from the fifth rule of Table 3 proceeds likewise. Assume σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q) are both obtained from the fourth rule of Table 3. Then ρ_{L} ∈ F T^{∗}(P) and ρ_{R} ∈ F T^{∗}(Q). So ρ ∈ F T^{∗}(P ∥_{S} Q) by induction. Hence σ ∈ F T^{∗}(P ∥_{S} Q). Assume σ_{L} ∈F T^{∗}(P) is obtained from the sixth rule of Table 3 and σ_{R} ∈F T^{∗}(Q) from the fourth. Then P ⟶^{t} P′, ρ_{L} ∈ F T^{∗}(P′) and ρ_{L} has the form aη_{L} with a ∈ X_{L} ⊆ X—the latter using (7). Moreover, ρ_{R} ∈ F T^{∗}(Q). Now P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q by Table 1, and ρ ∈ F T^{∗}(P′ ∥_{S} Q) by induction. Since X_{L} is system-ended in σ_{L}, by (5) X must be system-ended in σ. Hence ρ has the form bη with b ∈ X. Using the sixth rule of Table 3 it follows that σ ∈ F T^{∗}(P ∥_{S} Q). The case that σ_{L} ∈ F T^{∗}(P) is obtained from the fourth rule of Table 3 and σ_{R} ∈ F T^{∗}(Q) from the sixth proceeds likewise.

In case σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q) are both obtained from the sixth rule of Table 3, X_{L} is system-ended in σ_{L} and X_{R} is system-ended in σ_{R}. So this case is excluded by condition (6).

“⊆”: Let F T^{e}(x) be defined exactly as F T^{∗}(x)—see Table 3—except that the conclusion of the fifth rule reads “XXρ ∈ F T^{e}(x)”. Now F T^{∗}(P ∥_{S} Q) ⊆ col(F T^{e}(P ∥_{S} Q)), so, using that col is monotonous, it suffices to show that F T^{e}(P ∥_{S} Q) ⊆ F T^{∗}(P) ∥_{S} F T^{∗}(Q).

So let σ ∈ F T^{e}(P ∥_{S} Q). With structural induction on the derivation of σ ∈ F T^{e}(P ∥_{S} Q) from the (amended) rules of Tables 1 and 3 I show that σ ∈ F T^{∗}(P) ∥_{S} F T^{∗}(Q). This means I have to give a valid decomposition of σ such that σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q).

• Let σ = ⊤, with σ ∈ F T^{e}(P ∥_{S} Q) derived from the first rule of Table 3. Then σ has only one decomposition, which is valid. Trivially, σ_{L} = ⊤ ∈ F T^{∗}(P) and σ_{R} = ⊤ ∈ F T^{∗}(Q).

• Let σ = aρ, with σ ∈ F T^{e}(P ∥_{S} Q) derived from the second rule. Then P ∥_{S} Q ⟶^{a} P′ ∥_{S} Q′ and ρ ∈ F T^{e}(P′ ∥_{S} Q′). By induction there is a valid decomposition of ρ such that ρ_{L} ∈ F T^{∗}(P′) and ρ_{R} ∈F T^{∗}(Q′). Depending on which rule of Table 1 was employed to derive P ∥_{S} Q ⟶^{a} P′ ∥_{S} Q′,

(i) either a ∉ S, P ⟶^{a} P′ and Q′ = Q,

(ii) or a ∈ S, P ⟶^{a} P′ and Q ⟶^{a} Q′,

(iii) or a ∉ S, P′ = P and Q ⟶^{a} Q′. In case (i) take σ_{L} := aρ_{L} and σ_{R} := ρ_{R} ∈ F T^{∗}(Q). As the given decomposition of ρ is valid, so is the newly constructed one of σ. The second rule of Table 3 yields σ_{L} ∈ F T^{∗}(P). In case (ii) σ_{L} := aρ_{L} ∈ F T^{∗}(P) and σ_{R} := aρ_{R} ∈ F T^{∗}(Q). Again this decomposition is valid. In case (iii) σ_{L} := ρ_{L} ∈ F T^{∗}(P) and σ_{R} := aρ_{R} ∈ F T^{∗}(Q). Again this decomposition is valid.

• Suppose σ ∈ F T^{e}(P ∥_{S} Q) is derived from the third rule of Table 3. Then P ∥_{S} Q ⟶^{τ} P′∥_{S} Q′ and σ ∈ F T^{e}(P′∥_{S} Q′). By induction there is a valid decomposition of σ such that σ_{L} ∈ F T^{∗}(P′) and σ_{R} ∈F T^{∗}(Q′). Depending on which rule of Table 1 was employed to derive P ∥_{S} Q ⟶^{τ} P′ ∥_{S} Q′,

(i) either P ⟶^{τ} P′ and Q′ = Q,

(ii) or P′ = P and Q ⟶^{τ} Q′.

In either case the third rule of Table 3 yields σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q).

• Let σ = Xρ, with σ ∈ F T^{e}(P ∥_{S} Q) derived from the fourth rule of Table 3. Then P ∥_{S} Q−↛^{α} for all α ∈ X ∪ {τ}, and ρ ∈ F T^{e}(P ∥_{S} Q). By induction there is a valid decomposition of ρ

such that ρ_{L} ∈ F T^{∗}(P) and ρ_{R} ∈ F T^{∗}(Q). Let X_{L} := (X \ S) ∪ {a ∈ X ∩ S | P −↛^{a}} and

X_{R} := (X\S)∪{a ∈ X∩S | Q−↛^{a}}. Considering that, for a∈X∩S, P ∥_{S}Q−↛^{a} iff P −↛^{a}∨Q−↛^{a},

Condition (7), with X, X_{L} and X_{R} in the rôles of σ_{i}, σ_{i}^{L} and σ_{i}^{R}, is satisfied. Moreover, P −↛^{α} for all α ∈ X_{L} ∪ {τ}, and Q−↛^{α} for all α ∈ X_{R} ∪ {τ}. Take σ_{L} = X_{L}ρ_{L} and σ_{R} = X_{R}ρ_{R}. The fourth rule of Table 3 yields σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q). It remains to show that this decomposition satisfies Conditions (5) and (6). Suppose ρ_{L} has the form aη_{L}. Then, by Corollary 1, a ∉ X_{L}. It follows that X_{L} is not systemended in σ_{L}. In the same manner it follows that X_{R} is not system-ended in σ_{R}, and that X is not system-ended in σ.

• Let σ = XXρ, with σ ∈ F T^{e}(P ∥_{S} Q) derived from the amended fifth rule of Table 3. Then

P ∥_{S} Q−↛^{α} for all α ∈ X ∪{τ}, P ∥_{S} Q ⟶^{t} P′∥_{S} Q′ and Xρ ∈ F T^{e}(P′∥_{S} Q′). By induction there

is a valid decomposition (X_{L}ρ_{L}, X_{R}ρ_{R}) of Xρ such that X_{L}ρ_{L} ∈ F T^{∗}(P′) and X_{R}ρ_{R}∈F T^{∗}(Q′). Note that P′−↛^{a} for all a ∈ X_{L} ∪{τ}. Depending on which rule of Table 1 was employed to derive

P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q′,

(i) either P ⟶^{t} P′ and Q′ = Q, (ii) or P′ = P and Q ⟶^{t} Q′. For reasons of symmetry, I may assume the former.

Let X′_{L} := {a ∈ X_{L} | P −↛^{a}} and X′_{R} := (X \ S) ∪ {a ∈ X ∩ S | Q−↛^{a}}. Using the fourth

rule of Table 3, σ_{L} := X′_{L}X_{L}ρ_{L} ∈ F T^{∗}(P′), and by the fifth rule σ_{L} ∈ F T^{∗}(P), also using that P −↛^{τ}. Moreover, by the fourth rule of Table 3, σ_{R} := X′_{R}X_{R}ρ_{R} ∈ F T^{∗}(Q), using that Q−↛^{α} for all α ∈ (X\S) ∪ {τ}. It remains to show the validity of the decomposition of σ that yields σ_{L} and σ_{R}. Conditions (5) and (6) hold trivially. So it remains to check Condition (7).

Let a ∈ X \ S. Then a ∈ X_{L} \ S and P ∥_{S} Q−↛^{a}, so P −↛^{a}, and a ∈ X′_{L} \ S.

Conversely, X′_{L} \ S ⊆ X_{L} \ S = X \ S, and by definition X′_{R} \ S = X \ S. Let a ∈ X ∩ S. Then P ∥_{S} Q−↛^{a}, so P −↛^{a} or Q−↛^{a}. In case Q−↛^{a}, by definition a ∈ X′_{R} ∩ S. In case Q⟶^{a}, it is not possible that a ∈ X_{R}. Hence a ∈ X_{L}, by Property (7) of the given valid decomposition of Xρ. Moreover, P −↛^{a}, so a ∈ X′_{L} ∩ S. Conversely, by definition X′_{R} ∩ S ⊆ X ∩ S and X′_{L} ∩ S ⊆ X_{L} ∩ S ⊆ X ∩ S.

• Let σ = Xaρ, with σ ∈ F T^{e}(P ∥_{S} Q) derived from the sixth rule of Table 3. Then P ∥_{S} Q−↛^{α}

for all α ∈ X ∪ {τ}, a ∈ X, P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q′ and aρ ∈ F T^{e}(P′ ∥_{S} Q′). By induction

there is a valid decomposition of ζ := aρ such that ζ_{L} ∈ F T^{∗}(P′) and ζ_{R} ∈ F T^{∗}(Q′). Let

X_{L} := (X \ S) ∪ {b ∈ X ∩ S | P −↛^{b}} and X_{R} := (X \ S) ∪ {b ∈ X ∩ S | Q−↛^{b}}. Then P −↛^{α}

for all α ∈ X_{L} ∪ {τ}, and Q−↛^{α} for all α ∈ X_{R} ∪ {τ}. Take σ_{L} = X_{L}ζ_{L} and σ_{R} = X_{R}ζ_{R}. I have to show that this is a valid decomposition of σ, and that σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q). Considering that, for all b ∈ X ∩ S, P ∥_{S} Q−↛^{b} iff P −↛^{b} ∨ Q−↛^{b}, Condition (7) is satisfied. Depending on which rule of Table 1 was employed to derive P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q′,

(i) either P ⟶^{t} P′ and Q′ = Q, (ii) or P′ = P and Q ⟶^{t} Q′. For reasons of symmetry, I may assume the former. By the fourth rule of Table 3, σ_{R} ∈ F T^{∗}(Q). I now show that X_{R} is not system-ended in σ_{R}. Namely, if ζ_{R} is of the form bη_{R}, then b ∉ X_{R} by Corollary 1. Thus Condition (6) holds.

– As a further case distinction, assume a ∉ S. Since a ∈ X and thus a ∈ X_{L} and a ∈ X_{R}, by the above it follows that ζ_{R} is not of the form aη_{R}. Hence, ζ_{L} has the form aη_{L}. The sixth rule of Table 3 yields σ_{L} ∈ F T^{∗}(P). Since X_{L} is system-ended in σ_{L} and X is system-ended in σ, Condition (5) holds as well.

– Finally assume a ∈ S. Then ζ_{L} has the form aη_{L} and ζ_{R} has the form aη_{R}. Since X_{R} is not system-ended in σ_{R}, one has a ∉ X_{R}, that is, Q⟶^{a}. As P ∥_{S} Q−↛^{a}, it follows that P −↛^{a}, and thus a ∈ X_{L}. The sixth rule of Table 3 yields σ_{L} ∈ F T^{∗}(P). Since X_{L} is system-ended in σ_{L} and X is system-ended in σ, Condition (5) holds as well. □

Proposition 2 σ ∈ F T^{∗}(τ_{I}(P)) ⇔ ∃ρ ∈ F T^{∗}(P). τ_{I}(ρ) = σ ∪ I.

Proof: Since each state R reachable from τ_{I}(P) satisfies R−↛^{α} for all α ∈ I, a trivial induction shows that σ ∈ F T^{∗}(τ_{I}(P)) ⇔ σ ∪ I ∈ F T^{∗}(τ_{I}(P)). (*)

“⇐”: Let ρ ∈ F T^{∗}(P) and ρ survives abstraction from I. By Condition (i) in the definition of abstraction survival, τ_{I}(ρ) is of the form σ ∪I. In view of (*), it suffices to show that τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)). I do so with structural induction on the derivation of ρ ∈ F T^{∗}(P). The case ρ = ⊤ is trivial.

Assume ρ ∈ F T^{∗}(P) is obtained from the third rule of Table 3. Then P ⟶^{τ} P′ and ρ ∈ F T^{∗}(P′). By induction τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P′)). By Table 1 τ_{I}(P) ⟶^{τ} τ_{I}(P′). Hence τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)) by the third rule of Table 3.

Assume ρ = aη ∈ F T^{∗}(P) is obtained from the second rule of Table 3. Then P ⟶^{a} P′ and η ∈ F T^{∗}(P′). By induction τ_{I}(η) ∈ F T^{∗}(τ_{I}(P′)). By Table 1 τ_{I}(P) ⟶^{α} τ_{I}(P′), with α = τ if a ∈ I and α = a otherwise. In the first case τ_{I}(ρ) = τ_{I}(η) ∈ F T^{∗}(τ_{I}(P)) by the third rule of Table 3. In the second case τ_{I}(ρ) = aτ_{I}(η) ∈ F T^{∗}(τ_{I}(P)) by the second rule of Table 3.

Assume ρ=Xη∈F T^{∗}(P) is obtained from the fourth rule of Table 3. Then P −↛^{α} for all α∈X ∪{τ} and η ∈ F T^{∗}(P). If η has the form aζ, then a ∉ X by Corollary 1. In particular, a ∉ I, using Condition (i) in the definition of abstraction survival. Consequently, τ_{I}(ρ) = Xτ_{I}(η), for any possibly form of η. Furthermore, τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}. Here I use that I ⊆ X. By induction τ_{I}(η) ∈ F T^{∗}(τ_{I}(P)). Hence τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)) by the fourth rule of Table 3.

Assume ρ=Xη ∈F T^{∗}(P) is obtained from the fifth rule of Table 3. Then P −↛^{α} for all α∈X ∪{τ}, P ⟶^{t} P′ and ρ ∈ F T^{∗}(P′). So τ_{I}(P) ⟶^{t} τ_{I}(P′) and τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}, using that I ⊆ X. By induction τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P′)). Note that τ_{I}(ρ) has the form Xζ, although not necessarily with ζ = τ_{I}(η). The fifth rule of Table 3 yields τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)).

Assume ρ=Xη ∈F T^{∗}(P) is obtained from the sixth rule of Table 3. Then P −↛^{α} for all α∈X ∪{τ}, P ⟶^{t} P′ and η ∈ F T^{∗}(P′). So τ_{I}(P) ⟶^{t} τ_{I}(P′) and τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}. By induction τ_{I}(η) ∈ F T^{∗}(τ_{I}(P′)). Using that ρ survives abstraction, I consider three alternatives for η.

• Let η = c_{0} ⋯ c_{n}⊤ with the c_{i} ∈ I. Then τ_{I}(ρ) = X⊤. The first and fourth rules of Table 3 yield τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)).

• Let η = c_{0} ⋯ c_{n}Xζ with the c_{i} ∈ I. Then τ_{I}(ρ) = τ_{I}(η) = τ_{I}(Xζ), and τ_{I}(η) has the form Xζ′. The fifth rule of Table 3 yields τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)).

• Let η = c_{1} ⋯ c_{n}aζ with the c_{i} ∈ I and a ∉ I. Then a ∈ X (using Condition (iii) of abstraction survival if n > 0, and the side condition of the sixth rule of Table 3 if n = 0) and τ_{I}(ρ) = Xτ_{I}(η) with τ_{I}(η) = aτ_{I}(ζ). The sixth rule of Table 3 yields τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)).

“⇒”: Let σ ∈ F T^{∗}(τ_{I}(P)); by (*) I may assume that σ = σ ∪ I. I have to find a ρ ∈ F T^{∗}(P) such that τ_{I}(ρ) = σ. I do so with structural induction on the derivation of σ ∈ F T^{∗}(τ_{I}(P)).

Assume σ ∈ F T^{∗}(τ_{I}(P)) is obtained from the first rule of Table 3. Take ρ = ⊤, so that τ_{I}(ρ) = ⊤ = σ. The first rule of Table 3 yields ρ ∈ F T^{∗}(P).

Assume σ∈F T^{∗}(τ_{I}(P)) is obtained from the second rule of Table 3. Then σ=aζ, τ_{I}(P) ⟶^{a} τ_{I}(P′) and ζ ∈ F T^{∗}(τ_{I}(P′)). So P ⟶^{a} P′ and a ∉ I. By induction, there is a ρ ∈ F T^{∗}(P′) such that τ_{I}(ρ) = ζ. The second rule of Table 3 yields aρ ∈ F T^{∗}(P). Moreover, τ_{I}(aρ) = aζ = σ.

Assume σ ∈ F T^{∗}(τ_{I}(P)) is obtained from the third rule of Table 3. Then τ_{I}(P) ⟶^{τ} τ_{I}(P′) and σ ∈ F T^{∗}(τ_{I}(P′)). So P ⟶^{α} P′ with α ∈ I ∪ {τ}. By induction, there is a ρ ∈ F T^{∗}(P′) such that τ_{I}(ρ) = σ. In case α = τ, the third rule of Table 3 yields ρ ∈ F T^{∗}(P). In case α ≠ τ, the second rule of Table 3 yields αρ ∈ F T^{∗}(P); moreover, τ_{I}(αρ) = τ_{I}(ρ) = σ.

Assume σ ∈ F T^{∗}(τ_{I}(P)) is obtained from the fourth rule of Table 3. Then σ = Xζ, ζ ∈ F T^{∗}(τ_{I}(P)) and τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}. So P −↛^{α} for all α ∈ X ∪ {τ}. By induction, there is a ρ ∈ F T^{∗}(P) such that τ_{I}(ρ) = ζ. Hence Xρ ∈ F T^{∗}(P) by the fourth rule of Table 3. In case ρ has the form ⊤ or Y η, one has τ_{I}(Xρ) = Xτ_{I}(ρ) = Xζ = σ, which needed to be shown. So suppose ρ has the form aη. Then a ∉ X by Corollary 1. In particular, a ∉ I, using Condition (i) in the definition of abstraction survival. Consequently, τ_{I}(Xρ) = Xτ_{I}(ρ) = Xζ = σ.

Assume σ ∈ F T^{∗}(τ_{I}(P)) is obtained from the fifth rule of Table 3. Then σ = Xζ, τ_{I}(P) ⟶^{t} τ_{I}(P′),

σ ∈ F T^{∗}(τ_{I}(P′)) and τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}. So P ⟶^{t} P′ and P −↛^{α} for all α ∈ X ∪ {τ}.

By induction, there is a ρ ∈ F T^{∗}(P′) such that τ_{I}(ρ) = σ. This ρ must have the form Xη. Hence ρ ∈ F T^{∗}(P) by the fifth rule of Table 3.

Finally, assume σ ∈ F T^{∗}(τ_{I}(P)) is obtained from the sixth rule of Table 3. Then σ = Xaζ, a ∈ X,

τ_{I}(P) ⟶^{t} τ_{I}(P′), aζ ∈ F T^{∗}(τ_{I}(P)) and τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}. So P ⟶^{t} P′ and P −↛^{α} for

all α ∈ X ∪ {τ}. By induction, there is a ρ ∈ F T^{∗}(P′) such that τ_{I}(ρ) = aζ. So a ∉ I and ρ has the form c_{1} … c_{n}aη with c_{i} ∈ I ⊆ X for i = 1, …, n and τ_{I}(η) = ζ. The sixth rule of Table 3 yields Xρ ∈ F T^{∗}(P). Moreover, τ_{I}(Xρ) = Xaτ_{I}(η) = Xaζ = σ. □

Proposition 3 σ ∈ F T^{∗}(R(P)) ⇔ ∃ρ ∈ F T^{∗}(P). ρ ∈ R^{−1}(σ).

Proof: “⇐”: Let ρ ∈ F T^{∗}(P). With structural induction on the derivation of ρ ∈ F T^{∗}(P) I show that, for any σ with ρ ∈ R^{−1}(σ), one has σ ∈ F T^{∗}(R(P)).

If ρ ∈ F T^{∗}(P) is obtained from the first rule of Table 3, then σ = ρ = ⊤ and σ ∈ F T^{∗}(R(P)). Assume ρ = aη ∈ F T^{∗}(P) is obtained from the second rule. Then P ⟶^{a} P′ and η ∈ F T^{∗}(P′).

Moreover, σ =bζ with (a, b)∈R and η ∈R^{−1}(ζ). So R(P) ⟶^{b} R(P′) by Table 1, and ζ ∈F T^{∗}(R(P′)) by induction. It follows that σ ∈ F T^{∗}(R(P)).

Assume ρ ∈ F T^{∗}(P) is obtained from the third rule of Table 3. Then P ⟶^{τ} P′ and ρ ∈ F T^{∗}(P′). So R(P) ⟶^{τ} R(P′) by Table 1, and σ ∈ F T^{∗}(R(P′)) by induction. It follows that σ ∈ F T^{∗}(R(P)).

Assume ρ = Y η ∈ F T^{∗}(P) is obtained from the fourth rule. Then P −↛^{α} for all α ∈ Y ∪ {τ} and η ∈ F T^{∗}(P). Moreover, σ = Xζ with Y = R^{−1}(X) and η ∈ R^{−1}(ζ). So R(P)−↛^{α} for all α ∈ X ∪ {τ}, and ζ ∈ F T^{∗}(R(P)) by induction. It follows that σ ∈ F T^{∗}(R(P)).

Assume ρ=Y η∈F T^{∗}(P) is obtained from the fifth rule. Then P −↛^{α} for all α∈Y ∪{τ}, P ⟶^{t} P′ and ρ ∈ F T^{∗}(P′). Moreover, σ=Xζ with Y = R^{−1}(X). So R(P)−↛^{α} for all α∈X∪{τ}, R(P) ⟶^{t} R(P′) and σ ∈ F T^{∗}(R(P′)) by induction. It follows that σ ∈ F T^{∗}(R(P)).

Assume ρ=Y aη∈F T^{∗}(P) is obtained from the sixth rule. Then P −↛^{α} for all α∈Y ∪{τ}, P ⟶^{t} P′, a ∈ Y and aη ∈ F T^{∗}(P). Moreover, σ = Xbζ with Y = R^{−1}(X), (a, b) ∈ R, b ∈ X and aη ∈ R^{−1}(bζ). So R(P)−↛^{α} for all α ∈ X ∪ {τ}, R(P) ⟶^{t} R(P′) and bζ ∈ F T^{∗}(R(P′)) by induction. It follows that σ ∈ F T^{∗}(R(P)).

“⇒”: Let σ ∈ F T^{∗}(R(P)). With structural induction on the derivation of σ ∈ F T^{∗}(R(P)) I show that there exists a ρ ∈ F T^{∗}(P) with ρ ∈ R^{−1}(σ).

If σ = ⊤ ∈ F T^{∗}(R(P)) is obtained from the first rule of Table 3, take ρ = ⊤. Now ρ ∈ F T^{∗}(P). Assume σ = bζ ∈ F T^{∗}(R(P)) is obtained from the second rule of Table 3. Then R(P) ⟶^{b} R(P′)

and ζ ∈ F T^{∗}(R(P′)). So P ⟶^{a} P′ for some a with (a, b)∈R, and by induction there is an η∈F T^{∗}(P′) with η ∈ R^{−1}(ζ). Take ρ = aη. Then ρ ∈ F T^{∗}(P) and ρ ∈ R^{−1}(σ).

Assume σ ∈ F T^{∗}(R(P)) is obtained from the third rule of Table 3. Then R(P) ⟶^{τ} R(P′) and σ ∈ F T^{∗}(R(P′)). So P ⟶^{τ} P′, and by induction there is a ρ ∈ F T^{∗}(P′) with ρ ∈ R^{−1}(σ). Hence ρ ∈ F T^{∗}(P).

Assume σ = Xζ ∈ F T^{∗}(R(P)) is obtained from the fourth rule of Table 3. Then R(P)−↛^{α} for all α ∈ X ∪ {τ} and ζ ∈ F T^{∗}(R(P)). So P −↛^{α} for all α ∈ R^{−1}(X) ∪ {τ}. By induction there is an η ∈ F T^{∗}(P) with η ∈ R^{−1}(ζ). Take ρ = R^{−1}(X)η. Then ρ ∈ F T^{∗}(P) by the fourth rule of Table 3. In case ζ has the form bζ′, then η has the form aη′ with (a, b) ∈ R; moreover, Corollary 1 yields b ∉ X as well as a ∉ R^{−1}(X). Consequently, ρ ∈ R^{−1}(σ).

Assume σ = Xζ ∈ F T^{∗}(R(P)) is obtained from the fifth rule of Table 3. Then R(P)−↛^{α} for all

α ∈ X ∪ {τ}, R(P) ⟶^{t} R(P′) and σ ∈ F T^{∗}(R(P′)). So P −↛^{α} for all α ∈ R^{−1}(X) ∪ {τ}, P ⟶^{t} P′,

and by induction there is a ρ ∈ F T^{∗}(P′) with ρ ∈ R^{−1}(σ). Of course ρ must have the form R^{−1}(X)η. So ρ ∈ F T^{∗}(P) by the fifth rule of Table 3.

Finally assume σ = Xbζ ∈ F T^{∗}(R(P)) is obtained from the sixth rule of Table 3. Then R(P)−↛^{α}

for all α∈X∪{τ}, b ∈ X, R(P) ⟶^{t} R(P′) and bζ ∈ F T^{∗}(R(P′)). So P −↛^{α} for all α∈R^{−1}(X)∪{τ},

P ⟶^{t} P′, and by induction there is an aη ∈F T^{∗}(P′) with (a, b) ∈ R and η ∈ R^{−1}(ζ). So a∈R^{−1}(X). Take ρ = R^{−1}(X)aη. Then ρ ∈ F T^{∗}(P) by the sixth rule of Table 3. Moreover, ρ ∈ R^{−1}(σ). □

Proposition 4 F T^{r∗}(P ∥_{S} Q) = col(F T^{r∗}(P) ∥_{S} F T^{r∗}(Q)).

Proof: “⊇”: Let σ ∈ F T^{r∗}(P) ∥_{S} F T^{r∗}(Q), and fix a valid decomposition of σ as a witness. With the clearly valid generalisation of Observation 1 to F T^{r∗}(P) it suffices to show that σ ∈ F T^{r∗}(P ∥_{S} Q).

• Let σ = stab . Then stab ∈ F T^{r∗}(P) and stab ∈ F T^{r∗}(Q). So stable(P) and stable(Q). Indeed, this implies stable(P ∥_{S} Q), and thus σ ∈ F T^{r∗}(P ∥_{S} Q).

• Let σ = ⊤, σ = aρ or σ = Xρ. Then σ_{L} ∈ F T^{∗}(P) and σ_{R} ∈ F T^{∗}(Q), so from (the proof of) Proposition 1 one obtains σ ∈ F T^{∗}(P ∥_{S} Q) ⊆ F T^{r∗}(P ∥_{S} Q).

• Let σ = tXρ. Assume that σ_{L} = tX_{L}ρ_{L} ∈ F T^{r∗}(P) and σ_{R} = X_{R}ρ_{R} ∈ F T^{r∗}(Q); the other case follows by symmetry. Then σ_{R} ∈ F T^{∗}(Q). Moreover, stab ∈ F T^{r∗}(Q), so Q is stable. By

Definition 9, P ⟶^{t} P′, X_{L}ρ_{L} ∈ F T^{∗}(P′) and P −↛^{α} for α ∈ X_{L} ∪{τ}. Thus P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q

by Table 1, and Xρ ∈ F T^{∗}(P′ ∥_{S} Q) by (the proof of) Proposition 1. Furthermore, X_{R}ρ_{R} ∈ F T^{∗}(Q) must be derived by the fourth to sixth rule of Table 3, so Q−↛^{α} for all α ∈ X_{R} ∪ {τ}. Hence P ∥_{S} Q−↛^{α} for all α ∈ X ∪ {τ}, using (7). Therefore, σ ∈ F T^{r∗}(P ∥_{S} Q).

• Let σ = poststab . Then either poststab ∈ F T^{r∗}(P) ∧ poststab ∈ F T^{r∗}(Q), or poststab ∈ F T^{r∗}(P) ∧ stab ∈ F T^{r∗}(Q), or stab ∈ F T^{r∗}(P) ∧ poststab ∈ F T^{r∗}(Q). Either way, P and Q both have paths of τ-transitions to a stable state, and at least one of them is nonempty. It follows that P ∥_{S} Q has a nonempty path of τ-transitions to a stable state, so σ ∈ F T^{r∗}(P ∥_{S} Q).

“⊆”: Let F T^{re}(P) be defined exactly as F T^{r∗}(P)—see Definition 9—but writing tXXσ instead of tXσ, and employing F T^{e}(P) and F T^{e}(P′), as defined in the proof of Proposition 1, instead of F T^{∗}(P) and F T^{∗}(P′). Obviously, F T^{r∗}(P ∥_{S} Q) ⊆ col(F T^{re}(P ∥_{S} Q)), so, using that col is monotonous, it suffices to show that F T^{re}(P ∥_{S} Q) ⊆ F T^{r∗}(P) ∥_{S} F T^{r∗}(Q).

So let σ ∈ F T^{re}(P ∥_{S} Q). With structural induction on the derivation of σ ∈ F T^{re}(P ∥_{S} Q) from the (amended) rules of Tables 1 and 3 I show that σ ∈ F T^{r∗}(P) ∥_{S} F T^{r∗}(Q). This means that in case σ≠stab , poststab I have to give a valid decomposition of σ such that σ_{L} ∈ F T^{r∗}(P) and σ_{R} ∈ F T^{r∗}(Q); moreover, I have to show that stab ∈ F T^{r∗}(P) and stab ∈ F T^{r∗}(Q) in case σ has the form tXρ.

• Let σ = ⊤, σ = aρ or σ = Xρ. Then σ ∈ F T^{e}(P ∥_{S} Q). So by the proof of Proposition 1 there is a valid decomposition of σ such that σ_{L} ∈ F T^{∗}(P) ⊆ F T^{r∗}(P) and σ_{R} ∈ F T^{∗}(Q) ⊆ F T^{r∗}(Q).

• Let σ = stab . Then P ∥_{S} Q−↛^{τ}, so P −↛^{τ} and Q−↛^{τ}. So stab ∈ F T^{r∗}(P) and stab ∈ F T^{r∗}(Q).

• Let σ = tXXρ. By Definition 9, P ∥_{S} Q−↛^{α} for all α ∈ X ∪ {τ}, P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q′ and

Xρ ∈ F T^{e}(P′ ∥_{S} Q′). It follows that P −↛^{τ} and Q−↛^{τ}, so stab ∈ F T^{r∗}(P) and stab ∈ F T^{r∗}(P). By the proof of Proposition 1 there is a valid decomposition of Xρ such that X_{L}ρ_{L} ∈ F T^{∗}(P′) and X_{R}ρ_{R} ∈ F T^{∗}(Q′). Depending on which rule of Table 1 derived P ∥_{S} Q ⟶^{t} P′ ∥_{S} Q′,

(i) either P ⟶^{t} P′ and Q′ = Q, (ii) or P′ = P and Q ⟶^{t} Q′. For reasons of symmetry, I may assume the former. Let X′_{L} := {a ∈ X_{L} | P −↛^{a}} and X′_{R} := (X \ S) ∪ {a ∈ X ∩ S | Q−↛^{a}}. Using the fourth rule of Table 3, X′_{L}X_{L}ρ_{L} ∈ F T^{∗}(P′), so by Definition 9 σ_{L} := tX′_{L}X_{L}ρ_{L} ∈ F T^{r∗}(P). Moreover, by the fourth rule of Table 3, σ_{R} := X′_{R}X_{R}ρ_{R} ∈ F T^{∗}(Q) ⊆ F T^{r∗}(Q), using that Q−↛^{α} for all α ∈ (X\S) ∪ {τ}. It remains to show the validity of the decomposition of σ into σ_{L} and σ_{R}. This proceeds exactly as in the corresponding case in the proof of Proposition 1 (the case σ = XXρ in direction “⊆”).

• Let σ = poststab . Then P ∥_{S} Q has a nonempty path of τ-transitions to a stable state. This path projects to paths of τ-transitions from P and from Q to stable states, and at least one of them must be nonempty. It follows that either poststab ∈ F T^{r∗}(P) ∧ poststab ∈ F T^{r∗}(Q), or poststab ∈ F T^{r∗}(P) ∧ stab ∈ F T^{r∗}(Q), or stab ∈ F T^{r∗}(P) ∧ poststab ∈ F T^{r∗}(Q). □

Proposition 5 Let stab ≠ σ ≠ poststab . Then σ ∈ F T^{r∗}(τ_{I}(P)) ⇔ ∃ρ ∈ F T^{r∗}(P). τ_{I}(ρ) = σ ∪ I. Moreover, stab ∈ F T^{r∗}(τ_{I}(P)) ⇔ stab ∈ F T^{r∗}(P) ∧ I(P) ∩ I = ∅, and poststab ∈ F T^{r∗}(τ_{I}(P)) ⇔ (∃c_{0}c_{1} … c_{n}I⊤ ∈ F T^{r∗}(P) where n ≥ 0 and all c_{i} ∈ I) ∨ (poststab ∈ F T^{r∗}(P) ∧ I⊤ ∈ F T^{r∗}(P)).

Proof: Let stab ≠ σ ≠ poststab . Since each state R reachable from τ_{I}(P) satisfies R−↛^{α} for all α ∈ I, a trivial induction shows that σ ∈ F T^{r∗}(τ_{I}(P)) ⇔ σ ∪ I ∈ F T^{r∗}(τ_{I}(P)). (*)

“⇐”: Let ρ∈F T^{r∗}(P) and ρ survives abstraction from I. By Condition (i) in the definition of abstraction survival, τ_{I}(ρ) is of the form σ ∪ I. In view of (*), it suffices to show that τ_{I}(ρ) ∈ F T^{r∗}(τ_{I}(P)).

Suppose ρ = ⊤, ρ = aη or ρ = Xη. Then ρ ∈ F T^{∗}(P). So τ_{I}(ρ) ∈ F T^{∗}(τ_{I}(P)) ⊆ F T^{r∗}(τ_{I}(P)) by the proof of Proposition 2.

Suppose ρ = tXη. Then P −↛^{α} for all α ∈ X ∪ {τ}, P ⟶^{t} P′ and Xη ∈ F T^{∗}(P′), by Definition 9. So τ_{I}(Xη) ∈ F T^{∗}(τ_{I}(P′)) by the proof of Proposition 2. Moreover, τ_{I}(P) ⟶^{t} τ_{I}(P′) and τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}, using that I ⊆ X. Note that τ_{I}(Xη) has the form Xζ, although not necessarily with ζ = τ_{I}(η). Definition 9 yields τ_{I}(ρ) = tτ_{I}(Xη) ∈ F T^{r∗}(τ_{I}(P)).

“⇒”: Let σ ∈ F T^{r∗}(τ_{I}(P)); by (*) I may assume that σ = σ ∪ I. I have to find a ρ ∈ F T^{r∗}(P) such that τ_{I}(ρ) = σ.

Suppose σ = ⊤, σ = aη or σ = Xη. Then σ ∈ F T^{∗}(τ_{I}(P)). So by the proof of Proposition 2 there is a ρ ∈ F T^{∗}(P) ⊆ F T^{r∗}(P) such that τ_{I}(ρ) = σ.

Suppose σ = tXζ. Then τ_{I}(P)−↛^{α} for all α ∈ X ∪ {τ}, τ_{I}(P) ⟶^{t} τ_{I}(P′) and Xζ ∈ F T^{∗}(τ_{I}(P′)), by Definition 9. Hence P −↛^{α} for all α ∈ X ∪ {τ}, and P ⟶^{t} P′. By the proof of Proposition 2 there is a Xη ∈ F T^{∗}(P′) such that τ_{I}(Xη) = Xζ. So ρ := tXη ∈ F T^{r∗}(P) by Definition 9, and τ_{I}(ρ) = σ.

The second statement of Proposition 5 is trivial. Now consider the third.

“⇐”: Suppose ∃c_{0}c_{1} … c_{n}I⊤ ∈ F T^{r∗}(P) where n ≥ 0 and all c_{i} ∈ I. Then P has a nonempty path, all of which transitions are labelled τ or c_{i} ∈ I, ending in a state P′ satisfying P′−↛^{α} for all α ∈ I ∪ {τ}. Consequently, τ_{I}(P) has a nonempty part, all of which transitions are labelled τ, ending in a state τ(P′) satisfying τ_{I}(P′)−↛^{τ}. Consequently, τ_{I}(P)⟶^{τ} and ∅⊤ ∈ F T^{∗}(τ_{I}(P)). Thus poststab ∈ F T^{r∗}(τ_{I}(P)).

Now suppose poststab ∈ F T^{r∗}(P) ∧ I⊤ ∈ F T^{r∗}(P). Then P ⟶^{τ} and P has a path, all of which transitions are labelled τ, ending in a state P′ satisfying P′−↛^{α} for all α ∈ I ∪ {τ}. This path must be nonempty. Again it follows that poststab ∈ F T^{r∗}(τ_{I}(P)).

“⇐”: Suppose poststab ∈ F T^{r∗}(τ_{I}(P)). Then τ_{I}(P) has a nonempty part, all of which transitions are labelled τ, ending in a state τ(P′) satisfying τ_{I}(P′)−↛^{τ}. Consequently, P has a nonempty path, all of which transitions are labelled τ or c ∈ I, ending in a state P′ satisfying P′−↛^{α} for all α ∈ I ∪ {τ}. In case on this path some transitions are labelled c∈I, one obtains ∃c_{0}c_{1} … c_{n}I⊤ ∈ F T^{r∗}(P) where n≥0 and all c_{i} ∈ I. In case there are no such transitions, poststab ∈ F T^{r∗}(P) and I⊤ ∈ F T^{r∗}(P). □

Proposition 6 σ ∈ F T^{r∗}(R(P)) ⇔ ∃ρ ∈ F T^{r∗}(P). ρ ∈ R^{−1}(σ).

Proof: “⇐”: Let ρ ∈ F T^{r∗}(P), and let σ satisfy ρ ∈ R^{−1}(σ). I have to show that σ ∈ F T^{r∗}(R(P)). Let ρ=⊤, ρ=aη or ρ=Xη. Then ρ∈F T^{∗}(P), so by Proposition 3 σ∈F T^{∗}(R(P)) ⊆ F T^{r∗}(R(P)). Let ρ = tY η. Then P −↛^{α} for all α ∈ Y ∪ {τ}, P ⟶^{t} P′ and Y η ∈ F T^{∗}(P′). Moreover, σ = tXζ

with Y = R^{−1}(X) and Y η ∈ R^{−1}(Xζ). So R(P)−↛^{α} for all α ∈ X ∪ {τ}, R(P) ⟶^{t} R(P′) and Xζ ∈ F T^{∗}(R(P′)) by Proposition 3. It follows that σ ∈ F T^{r∗}(R(P)).

Let ρ = stab . Then stable(P), so stable(R(P)) and σ = stab ∈ F T^{r∗}(R(P)).

Let ρ = poststab . Then P ⟶^{τ} and ∅⊤ ∈ F T^{∗}(P). So R(P)⟶^{τ} and ∅⊤ ∈ F T^{∗}(R(P)). Therefore σ = poststab ∈ F T^{r∗}(R(P)).

“⇒”: Let σ ∈ F T^{r∗}(R(P)). I have to find a ρ ∈ F T^{r∗}(P) with ρ ∈ R^{−1}(σ).

Let σ = ⊤, σ = aη or σ = Xη. Then σ ∈ F T^{∗}(R(P)), so by Proposition 3 there is a ρ ∈ F T^{∗}(P) ⊆ F T^{r∗}(P) with ρ ∈ R^{−1}(σ).

Let σ = tXζ. Then R(P)−↛^{α} for all α ∈ X ∪ {τ}, R(P) ⟶^{t} R(P′) and Xζ ∈ F T^{∗}(R(P′)). By Proposition 3 there is a Y η ∈ F T^{∗}(P′) with Y η ∈ R^{−1}(Xζ). In particular Y = R^{−1}(X). Therefore, P −↛^{α} for all α ∈ Y ∪ {τ}. Moreover, P ⟶^{t} P′. Take ρ := tY η. Then ρ ∈ F T^{r∗}(P) and ρ ∈ R^{−1}(σ).

Let σ = stab . Then stable(R(P)), so stable(P) and ρ = stab ∈ F T^{r∗}(P).

Let σ = poststab . Then R(P)⟶^{τ} and ∅⊤ ∈ F T^{∗}(R(P)). So P ⟶^{τ} and ∅⊤ ∈ F T^{∗}(P). Therefore ρ = poststab ∈ F T^{r∗}(P). □