BRICS RS-96-43 A. Ing� olfsd� ottir: Weak Semantics Based on Lighted Button Pressing Experiments

BRICS

Basic Research in Computer Science

Weak Semantics Based on Lighted Button Pressing Experiments

An Alternative Characterization of the Readiness Semantics

Anna Ing� olfsd� ottir

BRICS Report Series RS-96-43 ISSN 0909-0878 November 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through World Wide Web and anonymous FTP:

http://www.brics.dk/
ftp://ftp.brics.dk/pub/BRICS

This document in subdirectory RS/96/43/

Weak Semantics Based on Lighted Button Pressing Experiments

An Alternative Characterizations of the Readiness Semantics

Anna Ingólfsdóttir BRICS ^{∗}

Department of Computer Science, Aalborg University, Denmark^{†}

Abstract

Imposing certain restrictions on the transition system that defines the behaviour of a process allows us to characterize the readiness semantics of

[OH86] by means of black–box testing experiments, or more precisely by lighted button testing experiments [BM92]. As divergence is considered we give the semantics as a preorder, the readiness preorder, which kernel coincides with the readiness equivalence of [OH86]. This leads to a bisimulation like characterization and a modal characterization of the semantics. A concrete language, recursive free CCS without τ, is introduced, a proof system defined and it is shown to be sound and complete with respect to the readiness preorder. In the completeness proof the modal characterization plays an important role as it allows us to prove algebraicity of the preorder purely operationally.

1 Introduction

The behaviour of concurrent processes or complex systems is often given by operational semantics [Mil80]. Usually the operational semantics is based on a two level approach. The first level consists of assigning to the process a state transition graph which gives the different states the process can enter and the transitions between these together with informations about which action the process has to perform in a given state to enter another state. This level is usually modelled by a labelled transition system. As the labelled transition systems only describe the stepwise computation the process may perform, it is in general too concrete to abstract away from unimportant differences in the behaviour of two processes. To overcome this problem equivalences have been introduced on top of the labelled transition systems to identify processes with the same or similar behaviour. These relations are usually based on the idea that two processes should be identified behaviourally unless an external observer can tell them apart. The precise definition of the relation then depends on how powerful the external observer is both what concerns what she can observe and how she can interact with the process being observed.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

†email: annai@iesd.auc.dk

One way of identifying processes is by performing a so-called button-pressing experiment on them. In [BM92] this set up is described as follows.

A process is thought of as a black box with an interface which is equipped with one button for each possible action it can make and possibly some other control devices. The observer presses the buttons. Either the button is locked and the experiment fails or it goes down and the process changes to another state. The observer then either has completed the experiment with success, or she may continue the experiment in the new state.

In this study we use the convention that the observer performs an experiment by applying a test on the process, by which we mean a description of how the button pressing is going to take place depending on how the process reacts. If the experiment fails the process is said to fail the test and if it is successful we say that the process passes the test. Because of the possibility of nondeterminism in the behaviour of the process, a process may sometimes pass a given test and sometimes not. Two processes are considered behaviourally equivalent if and only if the may pass exactly the same tests.

The outcome of a black box experiment strongly depends on what behavioural aspects of the process are immediately observable and what kinds of tests the observer has in her power. For instance the buttons of the black box interface might have lights inside them so the observer can immediately see which actions are available in a given state without pressing the buttons and thereby the process changing state. This testing scenario is referred to as lighted button pressing experiments in [BM92]. Alternatively there might be no lights inside the buttons in which case the observer has to press the button and possibly change the state of the process to observe the ability of performing that action (blind button pressing experiments). Also the tests which are allowed in the experiments can be specified in different ways.

It has become a standard practice to distinguish between external and internal actions that occur in a computation of a process. (An internal action occurs for instance when a system of two parallel processes changes state as a consequence of a private communication.) In the literature researchers distinguish between strong semantics, which allows the observer to record the internal actions, and the weak semantics where the internal actions ar not observable. The button pressing experiments in [BM92] only concerns the strong semantic approach. In [Gla90] and [Gla93] van Glabbeek gives a very thorough study of most known behavioural preorders and equivalences both based on the strong and the weak semantic approach. However his main focus is on comparing the different relations, i. e. ordering them with respect to inclusion. In this paper we will study a version of the lighted button pressing scenario based on the idea of readiness semantics introduced by Olderog and Hoare in [OH86]. Unlike in [Gla93] our main purpose is to use the button pressing characterization to derive hopefully a rather simple theory to reason about process behaviour. The readiness semantics of [OH86] may be described as follows:

The meaning of a process is given by a set of observations. The observation space is the set of all elements which either are of the form s or sA where s is a sequence of actions and A is a finite set of actions. We say that a process is stable if it can not perform an internal action and divergent if it can perform an infinite sequence of internal actions. The set of observations of a process, p, obs(p) is defined as the least set that satisfies:

• If p can perform the sequence s (possibly interspersed with internal actions) then s ∈ obs(p),

• if p can perform the sequence s and thereby reach a stable state p′ where A is exactly the set of actions p′ can perform then sA ∈ obs(p),

• if p diverges on s (i.e. p may perform a prefix of the string s and thereby reach a divergent state) then obs(p) contains s and sA for all A.

Two processes are behaviourally equivalent if their sets of observations coincide. In particular this means that the set of observations for any divergent process is equal to the whole observation space Obs. Therefore all divergent processes are identified with the inactive divergent process which in the reference mentioned above is called div.

As this semantics adopts the weak approach we have to decide how to extend the button pressing scenario described above accordingly. Here there are a few questions which have to be addressed and some assumption are to be made. Introducing internal actions into the semantics implies the possibility of divergence. How is this to be observed by an external observer? There are several possible choices but in this first approach we make the following assumption: a divergent process does not react on any experiment. We do not assume that the divergent process fails the experiment but rather take an intuitionistic point of view by saying that we do not know if it does or not. The experiment is simply aborted if the process enters a divergent state, i.e. no test terminates when applied to a divergent state. Only when the process is convergent we may say something about the outcome of an experiment. This means in particular that failing and passing an experiment are not complementary in the sense that we may have a process where we can not decide whether it may fail or pass a given experiment. However, although divergent processes can not be tested we assume that divergence is in some sense observable. For instance we may assume a “time out” for the process to reach a stable state after a fixed period of time.

When divergence sensitive behavioural semantics is given for processes it has become standard to compare processes by a preorder rather than an equivalence. Intuitively “a process p is smaller than q” if they “have the same behaviour but p may diverge more often than q”. Following this approach we say that “p is smaller than q” iff “whenever t must terminate when applied to p and p may pass t, then t must terminate on q and also q may pass t” and “whenever t must terminate when applied to p and p must fail t, then the same must hold for q”.

The next assumption we want to make is that we only need to test a convergent process when it has reached a stable state. In particular this means that we assume that the process does not lose any of its communication abilities, i. e. abilities to output and input, by performing an internal action. In terms of process description languages like CCS this means that, if p ⟶^{a} p′ and p ⟶^{τ} p′′, then p′′ ⟶^{a} p′, which is in general not true for this calculus. However this condition holds for the language we considered, which is the regular sub-language of the language considered in [Hen88], basically the standard CCS where the internal action τ is replaced by the internal choice operator ⊕. A drawback with this approach is that this condition does not hold if the parallel operator | is allowed with the standard definition of the operational semantics for it. Whether the definition of the behaviour of | can be modified in such a way that it fits into this set–up is an open question.

For the readiness semantics described above the restriction we impose on the labelled transition system implies that we do not have to consider separately the observations of the form s as whenever p may perform a sequence s it can perform s and thereby go to a stable state and will therefore have an observation of the form sA.

Based on the considerations above we make the following assumptions about the transition system that describes the behaviour of the process:

• Internal actions preserve the ability of performing external actions (in the sense described above).

• The process can only perform a finite number of different actions in its convergent states during its whole lifetime (weak sort finiteness).

• Each convergent state can only perform a finite number of actions, external or internal, leading to different states (weak finite branching).

Now we describe the black–box interface as follows.

• The control panel of the black-box machine has one button for each potential action of the process. The buttons are labelled with the actions and have lights inside them. It also has a red and a green control lamp. These are the only control devices.

• For all processes either the red or the green lamp will eventually light after a limited amount of time.

• If the process enters a divergent state the red lamp lights and all buttons are blocked.

• If the process converges the green lamp lights and some button lights come on as well; the experiment may start (or continue if it has already started in a previous state).

Our next task is to describe the class of tests needed in the experiments in order to characterize the readiness semantics and how the observer applies them on the process.

The tests have the form a_{1}.a_{2}. · · · a_{n}.A, n ≥ 0 where a_{1}.a_{2}…. a_{n} is a sequence of visible or external actions and A is a finite sets of such actions. They are applied as follows: The observer waits for the control light. If it is red the experiment is aborted. If it is green, we have the following cases:

• If n = 0 she checks if A coincides with the set of labels of the lighted buttons.

• If n > 0 and a_{1} is not in A she records failure, otherwise she presses the a_{1}-button. Then she continues by applying the remainder of the test, a_{2}. · · · a_{n}.A in the new state.

This testing scenario induces a preorder which we refer to as the readiness preorder. Not so surprisingly it turns out that the equivalence induced by this preorder is exactly the readiness equivalence given our constraints on the transition system. However this is only true if the set of all possible actions is infinite. The following example shows this.

Let a be the only possible action. Then

Obs = {a^{n}A, a^{n}|n ≥ 0 and A = {a}, ∅}.

Assume furthermore that the set of states is given by {s_{1}, s_{2}, s_{3}, s_{4}}, the internal actions by ≻→ and the external ones by ⟶^{a} where

s_{1} ≻→ s_{2} ⟶^{a} s_{1}, s_{1} ≻→ s_{3} and s_{4} ≻→ s_{4}.

It is easy to see that obs(s_{1}) = obs(s_{4}) = Obs. However s_{1} ^{⋢}_{R} s_{4} as s_{1} ↓ and may be accepted by the test a.∅ but s_{4} ↑ and does not react on any test. Thus the readiness semantics in [OH86] does not detect divergence if the set of labels is finite.

The aim of this study is to show that this characterization of the readiness semantics leads to a rather simple bisimulation like characterization; the preorder is obtained as a least fixed point to a monotonic function on a complete lattice. We also define a modal logic to reason about process behaviour and show that it characterizes exactly the readiness preorder. Then we introduce a concrete language, CCS_{⊕}, regular CCS with τ replaced by the internal choice operator ⊕, and give it an axiomatic semantics by means of an equationally based proof system. We prove that it is sound and complete with respect to the readiness preorder. The proof system is a slight modification of the system introduced in [BKO88]. However in that reference only a sub-language consisting of recursion free terms of ACP is considered.

The logical characterization gives us an interesting and strong proof technique for proving properties of the behavioural preorder. Like in [AH92] we use it to prove that the preorder is finitary in the sense of [Abr91]. However here we go a step further and prove the algebraicity, in the sense of [Hen88], of the preorder by using its modal characterization. This allows us to reduce the proof of the completeness of the proof system to only proving the completeness over finite or recursion free terms. This proof technique is interesting in itself as the algebraicity usually follows only as a corollary to a full abstractness result with respect to a denotational model defined in terms of an algebraic domain. See for instance [Hen88, AH92, HI93, Ing95] for this.

The structure of what remains of the paper is as follows: In the next section we define the readiness preorder as an abstraction on the stepwise semantics given by labelled transition systems. We also give a bisimulation like characterization of the preorder. Section 3 is devoted to a modal characterization of the preorder. In Section 4 we introduce the language CCS_{⊕} and apply the theory to it, introduce a proof system and prove its soundness and completeness with respect to the readiness preorder. We complete the paper by pointing out some directions for further work in Section 5.

2 Operational Semantics

We describe the behaviour of processes by means of a slight modification of the standard labelled transition system, extended labelled transition system [Hen88], where the internal actions are given by the transition relation ≻→ instead of the more standard notation ⟶^{τ}.

Definition 2.1 We define an extended labelled transition system (LT S) as ⟨States, Lab, ⟶, ≻→⟩ where

• States is a set of states, ranged over by s,

• Lab is a set of labels, ranged over by l,

• ⟶ ⊆ States × Lab × States is an external transition relation,

• ≻→ ⊆ States × States is an internal transition relation.

We let Λ range over all LT S’s. □

As usual, we write (s, s′) ∈≻→ as s ≻→ s′ (read “s may evolve spontaneously to s′”) and (s, l, s′) ∈ ⟶ as s ⟶^{l} s′ (read “s may perform l and thereby become s′”). We define ⟹^{ε} as ≻→^{∗}, ⟹^{l} (the weak l-action) as ≻→^{∗} · ⟶^{l} · ≻→^{∗} and ⟹^{σ} where σ ∈ Lab^{∗} similarly. We write s ≻→ if s ≻→ s′ for some s′ and s ⊁→ if no such s′ exists. In this case we say that s is a stable state. We say that s ↑ (read “s diverges” or “is divergent”) if there is an infinite sequence of states s_{1}, s_{2}, … such that s ≻→ s_{1} ≻→ s_{2} . . .. That s ↓ (read s “converges” or “is convergent”) is defined as ¬(s ↑). We also define s ↑ l (read “s diverges on l”) as

(s ↑ ∨∃s′.s ⟹^{l} s′ ∧ s′ ↑) and s ↓ l as ¬(s ↑ l). We define

• I(s) = {l ∈ Lab|s ⟶^{l}}, the initial set of s

• I(S) = {I(s)|s ∈ S}, the ready set of S,

• I(S) = ⋃ I(S), the initial set of S,

• Int(s) = {s′|s ≻→ s′},

• Ext(s) = {s′|∃l ∈ Lab.s ⟶^{l} s′},

• Sort_{w}(s) = {l ∈ Lab | ∃σ ∈ Act^{∗}, s′ ∈ States. s′ ↓ ∧s ⟹^{σ} s′ ⟹^{l}}.

We say that s is finitely branching if Int(s)∪Ext(s) is finite and that Λ is weakly finitely branching if all its convergent states are finitely branching. A state, s, is said to be weakly sort finite if Sort_{w}(s) is finite. This definition extends to LT S’s in the obvious way. If for all s ∈ States the following holds:

s ⟶^{a} s′ and s ≻→ s′′ implies s′′ ⟶^{a} s′

we say that communication capabilities are preserved by ≻→. If this is the case then it is easy to see that if s ↓ and s ⟶^{a} s′ then there is a state s′′ ⊁→ such that s ≻→^{∗} s′′ ⟶^{a} s′. As explained in the Introduction we make the following assumption.

Assumption 2.2 Throughout the paper we assume that all LT S’s are weakly sort-finite and weakly finitely branching and that communication capabilities are preserved by ≻→.

In the Introduction we made the assumption that we are not able to test divergent processes, i.e. no tests terminate when applied to them, and that we only perform experiments on processes when they have reached a stable state. Therefore we model a convergent process as the set of stable states it can reach internally and a divergent process as the singleton set {⊥}. Furthermore, as we want to model when two processes s and t may pass the same tests, we have to compare the set of all possible stable states s may reach when performing a weak l-action to the set of all possible stable states t may reach when performing the same action. To model this we define the l-derative, Der(l, S) of a set of stable states, S, where l ∈ I(S), as the set of stable states which can be reached from the states in S by performing a weak l-action if all its states converge on l and {⊥} otherwise. In this way any labelled transition system, Λ, induces a deterministic labelled transition system where the new states are either finite sets of stable states of the original one or the singleton set {⊥}. To ensure that this approach makes sense we prove the following property.

Lemma 2.3 For all s ∈ States the following holds.

1. If s ↓ then {s′|s ≻→^{∗} s′} is finite.

2. If s ↓ l then {s′|s ⟹^{l} s′} is finite.

Proof Follows by a simple application of Köning’s Lemma [Knu73]. □

Next we define some notation we use throughout the paper.

• Stb(s) = {s′|s ≻→^{∗} s′ ⊁→}: the set of stable states of s,

• Stb_{w}(s) = \{ \begin{matrix}Stb(s) & if s ↓ \\ \{⊥\} & if s ↑ \end{matrix} : the set of weakly stable states of s and

• Stb = {s|s ⊁→}: the set of stable states.

By Lemma 2.3, Stb_{w}(s) is finite for all s ∈ States. We let S= P_{fin}^{+}(Stb) ∪ {{⊥}}, where P_{fin}^{+}(Stb) denotes the family of finite non-empty subsets of Stb. For S ∈ S we define

• S ↑ iff S = {⊥},

• S ↓ iff ¬(S ↑),

• S ↑ l iff S ↑ or ∃s ∈ S.s ↑ l, • S ↓ l iff ¬(S ↑ l),

• for l ∈ I(S) we let

Der(l, S) = \{ \begin{matrix}\{s′ | ∃s ∈ S. s ⟹^{l} s′ \\ ands′ ⊁→\} & if S ↓ l \\ \{⊥\} & if S ↑ l \end{matrix} : the l-derivative of S.

Again Lemma 2.3 ensures that Der : Lab × S ↪ S is well-defined this way as a partial function. In what follows we will define the readiness preorder, ^{⊑}_{R}. For this purpose we give a formal definition of the class of tests we apply in the experiments. We also define predicates which tell when a process may or may not pass a given test. Because of our intuitionistic approach, i.e. that the divergent states are not testable, we need two predicates, one to record when a process may pass the test and another one to tell when it must fail.

Definition 2.4 (Readiness Tests) The set T of readiness tests is defined as the least set which satisfies:

1. A ⊆_{fin} Lab implies A ∈ T ,

2. γ ∈ T , l ∈ Lab implies l.γ ∈ T .

The success functions MayP ass, MustF ail : T × S ⟶ Bool are defined as follows:

For all S ∈ S
1. MayP ass(A, S) = S ↓ ∧ A ∈ I(S),
2. MayP ass(l.γ, S) = S ↓ ∧ l ∈ I(S) ∧ MayP ass(γ, Der(l, S)).
1. MustF ail(A, S) = S ↓ ∧ A ∉ I(S),
2. MustF ail(l.γ, S) = S ↓ ∧ (l ∈ I(S) ⇒ MustF ail(γ, Der(l, S))).

□

We define the readiness preorder by

Definition 2.5 (Readiness Preorder)

S ^{⊑}_{R} T iff ∀γ ∈ T . \begin{matrix}MayP ass(γ, S) ⇒ MayP ass(γ, T)∧ \\ MustF ail(γ, S) ⇒ MustF ail(γ, T). \end{matrix}

and for s, t ∈ State

s ^{⊑}_{R} t iff Stb_{w}(s) ^{⊑}_{R} Stb_{w}(t).

The derived equivalence is denoted by =_{R}. □

Example 2.6 Let γ_{1} = {l}, γ_{2} = l.∅ and S = {l.Ω}, where Ω ↑. It is easy to see that MayP ass(γ_{1}, S) is true and MustF ail(γ_{1}, S) is not. On the other hand neither MayP ass(γ_{2}, S) nor MustF ail(γ_{2}, S) is true.

We have the following result which is proved in Appendix A.

Theorem 2.7 If the set of labels, Lab, is infinite then the equivalence =_{R} coincides with the readiness equivalence of [OH86].

Next we give a bisimulation like characterization of the relation ^{⊑}_{R}, i.e. we obtain the preorder as the greatest fixed point to a monotonic endofunction over the complete lattice (S × S, ⊆).

Definition 2.8 (Alternative Readiness Preorder) Let F : S × S ⟶ S × S be defined by:

F(R) = \{(S, T)| S ↓ implies \begin{matrix}1. T ↓, \\ 2. I(S) = I(T) and \\ 4. ∀l ∈ I(S).(Der(l, S), Der(l, T)) ∈ R\}. \end{matrix}

The alternative readiness preorder ⪯ is defined as the greatest fixed-point to F. We define

s_{1} ⪯ s_{2} iff Stb_{w}(s_{1}) ⪯ Stb_{w}(s_{2}).
□

R is said to be an alternative readiness relation if R ⊆ F(R). By the standard fixed point theory [Tar55],

⪯ = ⋃{R ⊆ S × S | R ⊆ F(R)},

or equivalently

S_{1} ⪯ S_{2} iff (S_{1}, S_{2}) ∈ R for some alternative readiness relation R.

The ω-alternative readiness preorder ⪯_{ω} is defined as follows.

1. ⪯_{0}= S × S,

2. ⪯_{n+1}= F(⪯_{n}),

3. ⪯_{ω}= ⋂_{n∈ω} ⪯_{n}

and as before

s_{1} ⪯_{ω} s_{2} iff Stb_{w}(s_{1}) ⪯_{ω} Stb_{w}(s_{2}).

In what follows we state that the two preorders ⪯ and ⪯_{ω} coincide and that they actually are preorders.

Lemma 2.9

I. ⪯=⪯_{ω}.

II. ⪯ is a preorder. We refer to its kernel as ≃.

Proof Obviously it is sufficient to prove the statements for ⪯ in S × S instead of States × States. We prove each of the statements separately.

I. It is easy to see that ⪯⊆⪯_{n} for all n and therefore that ⪯⊆⪯_{ω}. To prove that ⪯_{ω}⊆⪯ it is sufficient to prove that ⪯_{ω} is a readiness preorder. This in turn follows easily from the fact that the transition relation is deterministic on S.

II. To prove the reflexivity we note that ⪯_{n} is reflexive for all n. To prove the transitivity it is sufficient to prove that ⪯_{n} is transitive for all n. We proceed by induction on n. The base case n = 0 is trivial. For the inductive step we assume that S_{1} ⪯_{n+1} S_{2} and S_{2} ⪯_{n+1} S_{3}, we will prove that S_{1} ⪯_{n+1} S_{3}, i.e. that S_{1}F(⪯_{n})S_{3}. We proceed as follows.

Assume S_{1} ↓.

1. This implies that S_{2} ↓ and therefore that S_{3} ↓.

2. Assume S_{1} ↓, S_{2} ↓ and S_{3} ↓. As S_{1} ⪯_{n+1} S_{2}, I(S_{1}) = I(S_{2}). As S_{2} ⪯_{n+1} S_{3}, I(S_{2}) = I(S_{3}), i.e. I(S_{1}) = I(S_{3}).

3. Again assume S_{1} ↓, S_{2} ↓ and S_{3} ↓, I(S_{1}) = I(S_{2}) and that l ∈ I(S_{1}). Then l ∈ I(S_{2}). Furthermore, by assumption, Der(l, S_{1}) ⪯_{n} Der(l, S_{2}) and Der(l, S_{2}) ⪯_{n} Der(l, S_{3}). By induction Der(l, S_{1}) ⪯_{n} Der(l, S_{3}).

□

The following theorem states the equivalence between the two relations defined above.

Theorem 2.10 (Alternative characterization) For all s, t ∈ States

s ⪯ t iff s ^{⊑}_{R} t.

Proof It is sufficient to prove the theorem for S, T ∈ S.

“only if”: Assume that S ⪯ T, we will prove that

∀γ ∈ T . \begin{matrix}1.MayP ass(γ, S) ⇒ MayP ass(γ, T) and \\ 2.MustF ail(γ, S) ⇒ MustF ail(γ, T). \end{matrix}

We proceed by induction on the definition of γ and consider each statement,

1. and 2., separately. First we note that S ⪯ T and S ↓ implies I(T) = I(T). Now we proceed as follows.

1. For the base case assume A ⊆_{fin} Lab. Then we have

MayP ass(A, S) ⇒ S ↓ ∧A ∈ I(S) (by def. of MayP ass)
⇒ T ↓ ∧A ∈ I(T)  (as S ⪯ T)
⇒ MayP ass(A, T) .

For the inductive step assume l ∈ Lab and γ ∈ T .

MayP ass(l.γ, S) ⇒ S ↓ ∧l ∈ I(S) ∧ MayP ass(γ, Der(l, S))
(by def. of MayP ass)
⇒ T ↓ ∧l ∈ I(T) ∧ MayP ass(γ, Der(l, T))
(by ind. as S ⪯ T)
⇒ MayP ass(l.γ, T).

2. For the base case, as before, assume A ⊆_{fin} Lab. We have

MustF ail(A, S) ⇒ S ↓ ∧A ∉ I(S) (by def. of MustF ail)
⇒ T ↓ ∧A ∉ I(S)  (as S ⪯ T)
⇒ MustF ail(A, T).

For the inductive step we have:

MustF ail(l.γ, S) ⇒ S ↓ ∧(l ∈ I(S) ⇒ MustF ail(γ, Der(l, S))
(by def. of MustF ail)

⇒ T ↓ ∧(l ∈ I(T) ⇒ MustF ail(γ, Der(l, T))

(by ind. as S ⪯ T
⇒ MustF ail(l.γ, T).

“if”: It is sufficient to prove the following statement:

(∀n.S ⪯̸_{n} T) implies ∃γ ∈ T . \begin{matrix}(MayP ass(γ, S) ∧ ¬MayP ass(γ, T))∨ \\ (MustF ail(γ, S) ∧ ¬MustF ail(γ, T)). \end{matrix}

We prove this statement by induction on n where the base case n = 0 is trivial. For the inductive step we proceed by considering the following cases according to why S ⪯_{n+1} T fails.

S ↓ but T ↑: Let A ∈ I(S). Then MayP ass(A, S) but ¬MayP ass(A, T).

S ↓ and T ↓ but I(S) \ I(T) ≠ ∅ : Let A ∈ I(S) \ I(T). As before MayP ass(A, S) but ¬MayP ass(A, T).

S ↓ and T ↓ but I(T) \ I(S) ≠ ∅ : Let A ∈ I(T) \ I(S). Then MustF ail(A, S) but ¬MustF ail(A, T).

S ↓, T ↓, I(S) = I(T) and l ∈ I(S) = I(T) but Der(l, S) ⪯̸_{n} Der(l, T): By induction there is a γ ∈ T such that either of the following holds:

MayP ass(γ, Der(l, S)) but ¬MayP ass(γ, Der(l, T)):

In this case MayP ass(l.γ, S) but ¬MayP ass(l.γ, T). MustF ail(γ, Der(l, S)) but ¬MustF ail(γ, Der(l, T)):

Then MustF ail(l.γ, S) but ¬MustF ail(l.γ, T). □

As the preorders ⪯ and ^{⊑}_{R} coincide from now on we refer to both of them as the readiness preorder.

3 Modal Characterization

In this section we give a modal characterization of the readiness preorder. This characterization will be an important tool in proving properties of the preorder. The modal logic L is generated by the following syntax

ϕ ::= A [l]ϕ ϕ ∧ ϕ.

where A ⊆ P_{fin}(Lab)^{1}. The satisfaction relation ⊧⊆ S ×L, is defined inductively by:

1. S ⊧ A iff S ↓ and I(S) = A,

2. S ⊧ [l]ϕ iff S ↓ ∧(l ∈ I(S) ⇒ Der(l, S) ⊧ ϕ),

3. S ⊧ ϕ_{1} ∧ ϕ_{2} iff S ⊧ ϕ_{1} and S ⊧ ϕ_{2}.

As ∧ is commutative and associative we often write ϕ_{1} ∧ ϕ_{2} ∧ … ∧ ϕ_{n} without giving the bracketing. Furthermore we let

s ⊧ ϕ iff Stb_{w}(s) ⊧ ϕ.

In this case we say that s satisfies ϕ. Note that a state or a set of states satisfies a formula in L only if it is convergent. This implies that S ⊧ [l]ϕ and l ∈ I(S) only if S ↓ l. The modal depth, md(ϕ), of a formula, ϕ is defined by • md(A) = 1,

1the family of finite subsets of Lab

• md([l]ϕ) = 1 + md(ϕ) for l ∈ Lab,

• md(ϕ_{1} ∧ ϕ_{2}) = max{md(ϕ_{1}), md(ϕ_{2})}.

Also we define L_{n} = {ϕ ∈ L|md(ϕ) ≤ n} for n ≥ 0. We let L(S) = {ϕ ∈ L|S ⊧ ϕ} and L_{n}(S) = L_{n} ∩ L(S). We define L(s) and L_{n}(s) in the same way. The modal characterization of the readiness preorder is the content of the following theorem.

Theorem 3.1

1. For all S, T, ∀n. S ⪯_{n} T iff L_{n}(S) ⊆ L_{n}(T).

2. For all s, t, s ⪯ t iff L(s) ⊆ L(t)

Proof To prove 1. we proceed as follows:

“only if”: We prove the statement by induction on n. The base case n = 0 is obvious. For the inductive step assume S ⪯_{n+1} T and S ⊧ ϕ, where md(ϕ) = n + 1. We will prove that T ⊧ ϕ. We proceed by structural induction on ϕ.

ϕ ≡ A:

S ⊧ A ⇒ S ↓ ∧I(S) = A  (Pr. def. of ⊧)
⇒ T ↓ ∧I(T) = A ( as S ⪯_{n+1} T)
⇒ T ⊧ A (Pr. def. of ⊧)

ϕ ≡ [l]ψ: We recall that S ⊧ [l]ψ is equivalent to

S ↓ ∧(l ∈ I(S) ⇒ Der(l, S) ⊧ ψ).  (1)

We will prove that (1) holds for S replaced by T. As S ⪯_{n+1} T, T ↓. So assume l ∈ I(T). Then l ∈ I(S) and by (1), Der(l, S) ⊧ ψ. As Der(l, S) ⪯_{n} Der(l, T) and md(ψ) = n, by the outer induction Der(l, T) ⊧ ψ. This implies T ⊧ [l]ψ.

ϕ ≡ ϕ_{1} ∧ ϕ_{2}: S ⊧ ϕ_{1} ∧ ϕ_{2} implies S ⊧ ϕ_{1} and S ⊧ ϕ_{2}. By the structural induction T ⊧ ϕ_{1} and T ⊧ ϕ_{2}, i.e. T ⊧ ϕ_{1} ∧ ϕ_{2}.

“if”: It is sufficient to prove that for all n.

S ⪯̸_{n} T ⇒ ∃ϕ ∈ L_{n}. S ⊧ ϕ ∧ T |̸= ϕ.

We prove this statement by induction on n. The base case for the induction is vacuously true. For the inductive step it is sufficient to consider following cases according to why S ⪯̸_{n+1} T.

S ↓ but T ↑: Then S ⊧ I(S) but T |̸= I(S)
S ↓ and T ↓ and I(S) ≠ I(T): Again S ⊧ I(S) but T |̸= I(S).

S ↓, T ↓, I(S) = I(T) and l ∈ I(T) = I(S) but Der(l, S) ⪯̸_{n} Der(l, T): By induction there is a ψ ∈ L_{n} such that Der(l, S) ⊧ ψ but Der(l, T) |̸=

ψ. This implies that S ⊧ [l]ψ but T |̸= [l]ψ.

Statement 2. follows directly from statement 1., Lemma 2.9 and the definitions of s ⪯ t and L(s). □

Theorem 3.1 says that the preorder is fully characterized by the logic L interpreted over ⊧. Furthermore from the proof we see that the operator ∧ is not needed in the characterization. However in what follows we show that each S ∈ S that corresponds to a finite convergent process may be characterized up to ⪯ by one single formula in L, i. e. every such S has a characteristic formula in the sense of [SI94]. To obtain this result we need the ∧ operator. We start by defining dpth(S) = sup{|s| |S ⟹^{σ}}. We say that S is of finite depth if dpth(S) < ∞.

Definition 3.2 (Characteristic formula) Let D ∈ S be convergent and of finite depth. We define the characteristic formula, ϕ_{D}, for D by induction on dpth(D) by:

dpth(D) = 0: ϕ_{D} ≡ {∅}.

dpth(D) = n + 1: ϕ_{D} ≡ I(D) ∧ ⋀{[l]ϕ_{Der(l,D)}|l ∈ I(D) ∧ D ↓ l}.

□

We have the following characterization theorem

Theorem 3.3 For every convergent D ∈ S of finite depth following holds:

1. D ⊧ ϕ_{D} and

2. ∀S. S ⊧ ϕ_{D} ⇒ D ⪯ S.

Proof

1. We prove the statement by induction on dpth(D).

dpth(D) = 0: Obviously D ⊧ {∅}.

dpth(D) = n + 1: Again it is obvious that D ⊧ I(D). Furthermore, if l ∈ I(D) and D ↓ l, then Der(l, D) ↓. By induction Der(l, D) ⊧ ϕ_{Der(l,D)} which in turn implies that D ⊧ [l]ϕ_{Der(l,S)}. We have therefore that D ⊧ ⋀{[l]ϕ_{Der(l,D)}|l ∈ I(D) ∧ D ↓ l}. This completes the proof

of D ⊧ ϕ_{D}.

2. Next assume that S ⊧ ϕ_{D}. We will prove that D ⪯ S by showing that the defining clauses for ⪯ are satisfied. Again we prove the statement by induction on dpth(D).

dpth(D) = 0: It is easy to check that S ⊧ {∅} implies D ⪯ S.

dpth(D) = n + 1: Now we proceed as follows: We know that D ↓.

(a) As S ⊧ ϕ_{D}, S ↓.

(b) As S ⊧ I(D), I(S) = I(D)

(c) Let l ∈ I(S) = I(T). We have the following possibilities: • Der(l, D) ↑: Then Der(l, D) ⪯ Der(l, S).

• Der(l, D) ↓: As S ⊧ ⋀{[l]ϕ_{Der(l,D)}|l ∈ I(D) ∧ D ↓ l} this implies Der(l, S) ⊧ ϕ_{Der(l,D)}. By induction we get that Der(l, D) ⪯ Der(l, S).

□

4 Application to Regular CCS

In this section we give the syntax for a sublanguage of a slight modification of the standard CCS and an operational semantics based on the ideas described in the previous section.

4.1 Syntax

The language we investigate in this study is the set of regular processes of the language CCS_{⊕}, i. e. CCS where τ is replaced by the internal choice operator ⊕. This language is studied in more detail for testing based semantics in [Hen88].

In the definition of the syntax we assume a predefined countably infinite set of process variables P V ar ranged over by x,y, etc. and a set of of actions, Act, ranged over by a,b, etc. The set of allowed operators is Θ, Ω of arity 0, a. , a ∈ Act of arity 1 and ⊕ and + of arity 2. We use Σ to denote this collection of operators and Σ_{k} those of arity k. The set of (process) terms is then defined by the BNF-definition

t ::= Θ Ω t + t t ⊕ t a.t x recx.t.

The construction recx. binds occurrences of process names which gives rise in the usual way to free and bound names and to closed and open terms. We use t[u/x] to denote the term which results from substituting the term u for every free occurrence of x in t. We will sometimes use a more general form of substitution. If ρ is a mapping from P V ar to the set of terms then tρ is the term which results

1. a.p ⟶^{a} p
2. p ⟶^{a} p′ implies  p + q ⟶^{a} p′

q + p ⟶^{a} p′

3. p ⊕ q ≻→ p

p ⊕ q ≻→ q

4. Ω ≻→ Ω
5. recx.t ≻→ t[recx.t/x]
6. p ≻→ p′ implies p + q ≻→ p′ + q

q + p′ ≻→ q + p′

Figure 1: Rules for ≻→ and ⟶^{a}

from simultaneously substituting ρ(x) for each free occurrence of x in t. The set of processes, i.e. closed terms, is denoted by P roc ranged over by p and that of recursion free processes by F inP roc, ranged over by d.

4.2 The Operational Semantics

The concrete operational semantics for P roc is given by Figure 1. It is easy to check that the labelled transition system defined this way, ⟨P roc, Act, ⟶, ≻→ ⟩, satisfies the conditions described in Assumption 2.2. It turns out that the readiness preorder is a precongruence with respect to the operators in Σ.

Lemma 4.1 ⪯ is a precongruence with respect to the operators in Σ.

Proof To prove that ⪯ is a precongruence it is sufficient to prove that for all n, ⪯_{n} is preserved by the operators. We proceed by induction on n where the base case, n = 0, is trivial. For the inductive step we consider each of the operators separately:

a. : First we note that for any p, Stb_{w}(a.p) = {a.p}. Now it is straight forward to show that Stb_{w}(p) ⪯_{n+1} Stb_{w}(q) implies {a.p} ⪯_{n+1} {a.q}.

⊕: Here we note that for any p_{1} and p_{2}, p_{1} ⊕ p_{2} ↓ iff p_{1} ↓ and p_{2} ↓. Furthermore, if p_{1} ⊕ p_{2} ↓, then Stb_{w}(p_{1} ⊕ p_{2}) = Stb_{w}(p_{1}) ∪ Stb_{w}(p_{2}). Then we note that

∀S, T, U ≠ {⊥}. S ⪯ T ⇒ S ∪ U ⪯ T ∪ U.  (2)

Now the result follows easily by induction using these observations.

+: As before, for any p_{1} and p_{2}, p_{1} + p_{2} ↓ iff p_{1} ↓ and p_{2} ↓. Now we proceed as follows:

Assume Stb_{w}(p_{1}) ⪯_{n+1} Stb_{w}(q_{1}) and Stb_{w}(p_{2}) ⪯_{n+1} Stb_{w}(q_{2}). We will prove that Stb_{w}(p_{1} + p_{2}) ⪯_{n+1} Stb_{w}(q_{1} + q_{2}). So assume Stb_{w}(p_{1} + p_{2}) ↓.

1. Then Stb_{w}(p_{1}) ↓ and Stb_{w}(p_{2}) ↓. This implies that Stb_{w}(q_{1}) ↓ and Stb_{w}(q_{2}) ↓ which in turn implies that Stb_{w}(q_{1} + q_{2}) ↓.

2. Next assume that Stb_{w}(p_{1} + p_{2}) ↓ and Stb_{w}(q_{1} + q_{2}) ↓.

(a) First let p ∈ Stb(p_{1} + p_{2}). This implies that p = p′_{1} + p′_{2} where p′_{1} ∈ Stb(p_{1}) and p′_{2} ∈ Stb(p_{2}). Then there is a q′_{1} ∈ Stb(q_{1}) such that I(p′_{1}) = I(q′_{1}) and q′_{2} ∈ Stb(q_{2}) such that I(p′_{2}) = I(q′_{2}). This implies that I(p) = I(p′_{1} + p′_{2}) = I(q′_{1} + q′_{2}) = I(q) where q′_{1} + q′_{2} ∈ Stb(q_{1} + q_{2}).

(b) Now let Stb_{w}(p_{1} + p_{2}) ↓, Stb_{w}(q_{1} + q_{2}) ↓ and q ∈ Stb_{w}(q). As before we may conclude that I(p) = I(q) for some p ∈ Stb_{w}(p_{1} + p_{2}).

(a) and (b) imply that I(Stb(p_{1} + p_{2})) = I(Stb(q_{1} + q_{2})).

3. Finally assume that Stb_{w}(p_{1} + p_{2}) ↓, Stb_{w}(q_{1} + q_{2}) ↓ and a ∈ I(Stb(p_{1} + p_{2})) = I(Stb(q_{1} + q_{2})).

(a) First assume that p_{1} + p_{2} ↑ a. Then

Der(a, Stb_{w}(p_{1} + p_{2})) = {⊥}

and therefore

Der(a, Stb_{w}(p_{1} + p_{2})) ⪯ Der(a, Stb_{w}(q_{1} + q_{2})).

(b) Next assume that p_{1} +p_{2} ↓ a. If a ∉ I(p_{i}) for either i = 1 or i = 2, say i = 1 then a ∉ I(q_{1}) and

\begin{matrix}Der(a, Stb(p)) = Der(a, Stb(p_{2})) ⪯ \\ Der(a, Stb(q_{2})) = Der(a, Stb(q)). \end{matrix}

So assume a ∈ I(p_{1}) ∩ I(p_{2}). Then

Der(a, Stb(p_{1} +p_{2})) = Der(a, Stb(p_{1}))∪Der(a, Stb(p_{2})).

As Stb_{w}(p_{1}) ⪯_{n+1} Stb_{w}(q_{1}) and Stb_{w}(p_{2}) ⪯_{n+1} Stb_{w}(q_{2}), by (2)

Der(a, Stb_{w}(p_{1} + p_{2})) =
Der(a, Stb_{w}(p_{1})) ∪ Der(a, Stb_{w}(p_{2})) ⪯_{n}
Der(a, Stb_{w}(q_{1})) ∪ Der(a, Stb_{w}(q_{2})) =
Der(a, Stb_{w}(q_{1} + q_{2})).
□

4.3 The Proof System

In this section we introduce a proof system to reason about process behaviour. The proof system consists of a set of equations, Figure 2, and an inference system, Figure 3. The equations are a slight modification of those introduced in [BKO88] due to a different language as in that reference a subset of recursive free processes of ACP is considered. Furthermore the proof system is almost the same as for the must testing preorder [Hen88] with the following differences.

• The (in)equations

(X + Y) ⊕ Z = (X ⊕ Z) + (Y ⊕ Z)

and

X ⊕ Y ^{⊑} X

are omitted as they are not sound with respect to the readiness preorder.

• The equation

(a.X + Y) ⊕ (a.Z + W) = (a.X + Y) ⊕ (a.X + W) ⊕ (a.Z + W)

has been added here but is derivable in the proof system that characterizes the must testing.

For the motivation of these equations and the inference rules see the references above.

The syntactical approximations p^{n} that occur in the (ω)-rule are taken directly from [Hen88] and are defined as follows:

• p^{0} = Ω

• p^{n+1} is defined inductively by:

– (op(\underline{p}))^{n+1} = op(\underline{p}^{n+1}) for op ∈ Σ,

– (recx.u)^{n+1} = u^{n+1}[(recx.u)^{n}/x].

We refer to the set of equations as E and let ^{⊑}_{E} denote the preorder derived from E and the finitary inference rules (least)–(axiom) in Figure 3, while ^{⊑}_{E_{rec}^{−ω}} is obtained by adding the rule (fix) and ^{⊑}_{E_{rec}} is obtained by further adding the rule (ω), i.e. the full system. The discussion above shows that these preorders are strictly stronger than the corresponding ones for the must testing.

The following partial soundness result follows as an easy consequence of the definition of ⪯.

Lemma 4.2 (Partial soundness) The proof system consisting of the equations and the inference rules (least)–(fix) is sound with respect to the stable state preorder, i.e.

∀p, q. p ^{⊑}_{E_{rec}^{−ω}} q implies p ⪯ q.

Proof The inference rules (least)–(congr) only state that the relation is as precongruence with Ω as a least element and are therefore sound for ⪯. Also the rule (fix) is obviously sound for ⪯. Therefore it only remains to proof the soundness of the rule (axiom), i.e. to check whether the equations are sound with respect to ⪯. This in turn is straight forward and is left to the reader. □

Here we would like to point out that, at this point, we have not stated the soundness of the ω-rule as the proof for this is non trivial and will be dealt with later. In what remains of the paper we use the equations (⊕1)–(⊕3) and (+1)–(+4) to rewrite process terms without further explanation. Now we will state a standard result that holds for all proof systems of this kind. For justification see for instance [Hen88].

Lemma 4.3 For all d, p,

1. ∀n.p^{n} ^{⊑}_{E_{rec}^{−ω}} p,

2. d ^{⊑}_{E_{rec}} p implies d ^{⊑}_{E_{rec}^{−ω}} p,

3. d ^{⊑}_{E_{rec}} p implies ∃n.d ^{⊑}_{E} p^{n}.

Proof All the statements are standard and a justification for them may be found in for instance in [Hen88]. □

Lemma 4.4 The following equation is derivable from E.

(a.X + Y) ⊕ (a.Z + W) = (a.(X ⊕ Z) + Y) ⊕ (a.(X ⊕ Z) + W) (Der).

\begin{matrix}⊕1 & X ⊕ (Y ⊕ Z) = (X ⊕ Y) ⊕ Z \\ ⊕2 & X ⊕ Y = Y ⊕ X \\ ⊕3 & X ⊕ X = X \\ ⊕Ω & X ⊕ Ω = Ω \\ +1 & X + (Y + Z) = (X + Y) + Z \\ +2 & X + Y = Y + X \\ +3 & X + X = X \\ +4 & X + Θ = X \\ +Ω & X + Ω = Ω \\ pre + ⊕1 & a.X + a.Y = a.(X ⊕ Y) \\ pre + ⊕2 & a.X ⊕ a.Y = a.(X ⊕ Y) \\ + ⊕ 1 & X + (Y ⊕ Z) = (X + Y) ⊕ (X + Z) \\ + ⊕ 2 & (a.X + Y) ⊕ (a.Z + W) = (a.X + Y) ⊕ (a.X + W) ⊕ (a.Z + W) \end{matrix}

Figure 2: Equations

Proof The equation may be derived as follows:

(a.X + Y) ⊕ (a.Z + W) =
(a.X + Y) ⊕ (a.X + W) ⊕ (a.Z + Y) ⊕ (a.Z + W) = (+ ⊕ 2)
(a.X + (Y ⊕ W)) ⊕ (a.Z + (Y ⊕ W)) = (+ ⊕ 1)
(a.X ⊕ a.Z) + (Y ⊕ W) = (+ ⊕ 1)
a.(X ⊕ Z) + (Y ⊕ W) = (pre + ⊕2)
(a.(X ⊕ Z) + Y) ⊕ (a.(X ⊕ Z) + W). (+ ⊕ 1)
□

4.4 Finitariness and Algebraicity

In this subsection we will show that the preorder ⪯ is finitary in the sense of Abramsky [Abr91]. The proof is very similar to a proof of the same property for a bisimulation based preorder in [AH92] and like in that reference we use the logical characterization. However we go a step further and show that the preorder is algebraic in the sense of [Hen88] (basically that the (ω)-rule is sound) using similar techniques and by using the characteristic formula. This proof is of

(least) Ω ^{⊑} X

(preord) t ^{⊑} t  \frac{t ^{⊑} u, u ^{⊑} v}{t ^{⊑} v}

(congr) \frac{t_{i} ^{⊑} u_{i}}{op(\underline{t}) ^{⊑} op(\underline{u})}  for every op ∈ ∑

(axiom) \overline{tρ ^{⊑} uρ}  for every equation t ^{⊑} u and closed substitution ρ

(fixp)  \overline{recx.t = t[recx.t/x]}

(ω)  \frac{∀n. t^{n} ^{⊑} u}{t ^{⊑} u}

Figure 3: Proof System

some theoretical interest in itself as the algebraicity of the behavioural preorder, and the soundness of the ω-rule are proved by using properties of the modal logics, the operational semantics and of the proof system where the rule (ω) is omitted. Normally this result follows as a consequence of a full abstractness of the behavioural preorder with respect to a denotational model in terms of an algebraic cpo [Hen88, AH92, HI93, Ing95]. Proving the algebraicity directly allows us to reduce the proof of completeness of the proof system over the full language to a completeness proof only over recursion free processes. We start by giving Abramsky’s definition of when a preorder is finitary.

Definition 4.5 (Finitariness) The finitary part, ≤^{F}, of a preorder, ≤, is defined by

p ≤^{F} q iff (∀d.d ≤ p ⇒ d ≤ q).

A preorder ≤ is finitary if ≤^{F} =≤. □

We need the following lemma:

1. For all p ∈ P roc, p ⊁→ implies

p =_{E_{rec}^{−ω}} ∑{a.p′|p ⟶^{a} p′}.

2. For all p ∈ P roc, p ↓ implies

p =_{E_{rec}^{−ω}} ∑ ∘ Stb(p).

3. For all p ∈ P roc, p ⊁→ and p ↓ a implies

p =_{E_{rec}^{−ω}} ∑{a. ∑ ∘ Der(a, {p})|a ∈ I(p)}.

Proof

1. We will prove the statement by structural induction on p. The cases p ≡ Ω, p_{1} ⊕ p_{2}, recx.u are trivial as p is not stable. Also the cases p ≡ Θ, a.p_{1} follow immediately. For the only remaining case, p ≡ p_{1} + p_{2}, we proceed as follows.

First we note that p ⟶^{a} p′_{1} iff p_{1} ⟶^{a} p′_{1} or p_{2} ⟶^{a} p′_{1}. By induction we have

p ≡ p_{1} + p_{2} =_{E_{rec}^{−ω}}

∑{a.p′_{1}|p_{1} ⟶^{a} p′} + ∑{a.p′_{2}|p_{2} ⟶^{a} p′} =_{E_{rec}^{−ω}}

∑{a.p′|p ⟶^{a} p′}.

2. First we note that the statement is true if p ⊁→. Then we prove by structural induction that

p ↓ ∧p ≻→ implies p =_{E_{rec}^{−ω}} ∑ ∘ {p′|p ≻→ p′}.

For the only nontrivial case, p ≡ p_{1} + p_{2}, we proceed as follows.

Assume p_{1} + p_{2} ≻→ p′. Then either p′ ≡ p′_{1} + p_{2} where p_{1} ≻→ p′_{1} or p′ ≡ p_{1} +p′_{2} where p_{2} ≻→ p′_{2}. By the equation (⊕3), structural induction and the equation (+ ⊕ 1), we have

p_{1} + p_{2} =_{E_{rec}^{−ω}} (p_{1} + p_{2}) ⊕ (p_{1} + p_{2})
=_{E_{rec}^{−ω}} (∑ ∘ {p′_{1}|p_{1} ≻→ p′_{1}} + p_{2}) ⊕ (p_{1} + ∑ ∘ {p′_{2}|p_{2} ≻→ p′_{2}})
=_{E_{rec}^{−ω}} ∑ ∘ {p′_{1} + p_{2}|p_{1} ≻→ p′_{1}} ⊕ ∑ ∘ {p_{1} + p′_{2}|p_{2} ≻→ p′_{2}}
=_{E_{rec}^{−ω}} ∑ ∘ {p′|p_{1} + p_{2} ≻→ p′}.

Now the result follows easily by induction on the internal depth of p, i.e. max{n|∃p′.p ≻→^{n} p′}.

3. Let der(a, p) = {p′|p ⟶^{a} p′}. By 1. and equation (pre + ⊕1),

p =_{E_{rec}^{−ω}} ∑{a. ∑ ∘ der(a, p)|a ∈ I(p)}.

Furthermore

Der(a, {p}) = Stab(∑ ∘ der(a, p)).

By assumption, ∑ ∘ der(a, p) ↓ and thus, by 2.

∑ ∘ der(a, p) = ∑ ∘ Der(a, {p})

and the result follows.

□

The key to the proof of the finitariness of ⪯ is the following proposition which also is proved in [AH92] where, as mentioned before, a CCS-like language and prebisimulation are considered.

Proposition 4.7 For all p and ϕ, if p ⊧ ϕ then there is a finite d such that d ^{⊑}_{E_{rec}^{−ω}} p and d ⊧ ϕ.

Proof We prove the statement by structural induction on ϕ and we proceed as follows:

ϕ ≡ A: p ⊧ A means that p ↓ and I(Stb(p)) = A. Let

d ≡ ∑ ∘ {∑{a.Ω|a ∈ I(p′)}|p′ ∈ Stb(p)}.

Obviously d ⊧ A. Furthermore

d ≡ ∑ ∘ {∑{a.Ω|a ∈ I(p′)}|p′ ∈ Stb(p)}

⊑_{E_{rec}^{−ω}} ∑ ∘ {∑{a.p′′|p′ ⟶^{a} p′′}|p′ ∈ Stb(p)}

⊑_{E_{rec}^{−ω}} p ( by L.4.6.1,2)

ϕ ≡ [a]ψ: First we note that p ⊧ [a]ψ implies p ↓. If a ∉ I(Stb(p)) then d defined as in the previous case satisfies the conditions. So assume a ∈ I(Stb(p)). Then Der(a, Stb(p)) ⊧ ψ and thus p′ ≡ ∑ ∘ Der(a, Stb(p)) ⊧ ψ. By induction there is a d′ such that d′ ⊧ ψ and d′ ^{⊑}_{E_{rec}^{−ω}} p′. Now let

d ≡ ∑ ∘ {∑{b.d_{b}|b ∈ I(p′)}|p′ ∈ Stb(p)},

where d_{a} ≡ d′ and d_{b} ≡ Ω if b ≠ a. It is easy to see that d ⊧ [a]ψ. Furthermore

Der(a, Stb(p)) = ⋃{Der(a, {p′})|p′ ∈ Stb(p)}.

Now we have

d ≡ ∑ ∘ {∑{b.d_{b}|b ∈ I(p′)}|p′ ∈ Stb(p)}

⊑_{E_{rec}^{−ω}} ∑ ∘ {∑ b.{∑ ∘ Der(b, Stb(p))|b ∈ I(p′)}|p′ ∈ Stb(p)} ( by (least))

=_{E_{rec}^{−ω}} ∑ ∘ {∑{b. ∑ ∘ Der(b, {p′})|b ∈ I(p′)}|p′ ∈ Stb(p)} ( by (Der))

=_{E_{rec}^{−ω}} ∑ ∘ p′|p′ ∈ Stb(p)} ( by Lem. 4.6.3)

=_{E_{rec}^{−ω}} p ( by Lem. 4.6.1).

ϕ ≡ ϕ_{1} ∧ϕ_{2}: We recall that p ⊧ ϕ_{1} ∧ϕ_{2} iff p ⊧ ϕ_{1} and p ⊧ ϕ_{2}. By the structural induction there are d_{1} and d_{2} such that d_{i} ⊧ ϕ_{i} and d_{i} ^{⊑}_{E_{rec}^{−ω}} p for i = 1, 2. By Lemma 4.3, for i = 1, 2 there is an n_{i} such that d_{i} ^{⊑}_{E} p^{n_{i}}. Now let n = max{n_{1}, n_{2}} and d ≡ p^{n}. Then d_{i} ^{⊑}_{E_{rec}^{−ω}} d ^{⊑}_{E_{rec}^{−ω}} p. As d_{i} ⊧ ϕ_{i}, this and

Theorem 3.1 imply that d ⊧ ϕ_{1} ∧ ϕ_{2}.

□

Now we get that ⪯ is finitary and algebraic as a corollary to Proposition 4.7. The finitariness is proved basically in the same way as a similar result in [AH92].

Corollary 4.8 (Finitariness) ⪯^{F} =⪯=⪯_{ω}.

Proof It is sufficient to prove that ⪯^{F} =⪯ as the second equality is the content of Lemma 2.9. Obviously ⪯⊆⪯^{F}. To prove the opposite inclusion, by Theorem 3.1 it is sufficient to prove that

p ⪯^{F} q ⇒ L(p) ⊆ L(q).

To prove this we proceed as follows.

Assume that (∀d ↓ .d ⪯ p ⇒ d ⪯ q) and that p ⊧ ϕ. We will prove that q ⊧ ϕ. By Proposition 4.7 there is a d such that d ^{⊑}_{E_{rec}^{−ω}} p and d ⊧ ϕ. By the partial soundness d ⪯ p, by our assumption d ⪯ q and by Theorem 3.1, q ⊧ ϕ.

□

In the proof of the algebraicity we take advantage of the characteristic formulae for processes of finite depth, that was defined for sets of states. We extend this definition to recursion free processes by

∀d ↓ . ϕ_{d} ≡ ϕ_{Stb(d)}.

It is easy to see that ϕ_{d} is a characteristic formula for d in the sense of Theorem 3.3. The algebraicity of ⪯ is the content of the following corollary.

Corollary 4.9 (Algebraicity)

∀p, d. d ⪯ p ⇒ ∃n.d ⪯ p^{n}.

Proof If d ↑ we are done. So assume that d ↓ and d ⪯ p. Let ϕ_{d} be the characteristic formula for d. Then d ⊧ ϕ_{d} and therefore p ⊧ ϕ_{d}, by Theorem 3.1. By Proposition 4.7, there is a recursion free d′ such that d′ ^{⊑}_{E_{rec}^{−ω}} p and d′ ⊧ ϕ_{d}. Therefore d ⪯ d′ ^{⊑}_{E_{rec}^{−ω}} p. Now, by Lemma 4.3, there exists an n such that d′ ^{⊑}_{E} p^{n}. This implies d ⪯ p^{n}. □

From these corollaries we may derive the soundness of the (ω)-rule.

Corollary 4.10 (Soundness of the ω-rule) (∀n.p^{n} ⪯ q) implies p ⪯ q.

Proof By Corollary 4.8 it is sufficient to prove that

(∀n.p^{n} ⪯ q) implies (∀d.d ⪯ p ⇒ d ⪯ q).

So assume (∀n.p^{n} ⪯ q) and d ⪯ p. By Corollary 4.9, d ⪯ p^{n} for some n and by our assumption we get d ⪯ q. □

4.5 Completeness of the Proof System

In this final subsection we will prove the completeness of the proof system with respect to the readiness preorder, ⪯. By the algebraicity of the preorder, stated in Corollary 4.9, the proof of the completeness for the proof system with respect to it may be reduced to proving the completeness for finite processes and then applying the inference rule (ω). The proof of the completeness for the finite processes is, as usual, based on the notion of normal forms.

Definition 4.11 (Normal forms) An n ∈ F inP roc is in a normal form if either n ≡ Ω, n ≡ Θ or it is of the form n ≡ ∑ ∘ _{j≤N} ∑_{i≤N_{j}} a_{i}^{j}.n_{i}^{j} where the following holds for all i, i_{1}, i_{2}, j, k, l, :

1. n_{i}^{j} is a normal form,

2. if i_{1} ≠ i_{2} then a_{i_{1}}^{j} ≠ a_{i_{2}}^{j},

3. if a_{i}^{j} = a_{l}^{k} then n_{i}^{j} ≡ n_{l}^{k}.

□

Next we show that any finite process is provably equal to a normal form.

Lemma 4.12 (Normalization) For all d ∈ F inP roc there is a normal form nf(d) such that d =_{E} nf(d).

Proof Let dpth(d) = max{|σ| |d ⟹^{σ}}. We prove the statement by induction on dpth(d). The base case follows from an easy structural induction on d. To prove the inductive step we also proceed by structural induction on d.

d ≡ Θ, Ω: Obvious.

d ≡ a.d_{1}: By induction there is a normal form, nf(d_{1}), such that nf(d_{1}) =_{E} d_{1}. Then a.nf(d_{1}) =_{E} a.d_{1}, where a.nf(d_{1}) is a normal form.

d ≡ d_{1} ⊕ d_{2}: By structural induction d_{1} =_{E} n_{1} and d_{2} =_{E} n_{2} where n_{1} and n_{2} are normal forms. If either n_{1} ≡ Ω or n_{2} ≡ Ω, then d_{1} ⊕ d_{2} =_{E} Ω where Ω is a normal form. Also the case where n_{i} ≡ Θ for i = 1 or i = 2 is trivial. So assume

n_{1} ≡ ∑ ∘ _{j≤N} ∑_{i≤N_{j}} a_{i}^{j}.n_{i}^{j} and n_{2} ≡ ∑ ∘ _{l≤M} ∑_{k≤M_{l}} b_{k}^{l}.m_{k}^{l}.

Then

d_{1} ⊕ d_{2} =_{E} n_{1} ⊕ n_{2} =_{E}
∑ ∘ _{j≤N} ∑_{i≤N_{j}} a_{i}^{j}.n_{i}^{j} ⊕ ∑ ∘ _{l≤M} ∑_{k≤M_{l}} b_{k}^{l}.m_{k}^{l} =_{E}
∑ ∘ _{s≤N+M}d_{s},

where d_{s} ≡ ∑_{i≤N_{s}} a_{i}^{s}.n_{i}^{s} for s ≤ N and d_{N+s} ≡ ∑_{k≤M_{s}} b_{k}^{s}.m_{k}^{s} for s ≤ M. Obviously condition 1. and 2. for normal forms hold. To ensure 3. we apply the equation (Der) of Lemma 4.4 repeatedly. Now condition 2. and 3. hold but 1. may not hold any more. However now we may apply the outer induction hypothesis to rewrite the term to normal form.

d ≡ d_{1} + d_{2}: By structural induction, for i = 1, 2, there is a normal form n_{i} such that d_{i} =_{E} n_{i}. This implies d =_{E} n_{1} + n_{2}. To rewrite n_{1} + n_{2} into a normal form, using E, we proceed as follows: First we distribute + over ⊕, i.e. apply (+ ⊕ 1), sufficiently often so we end up with a double sum of the form ∑ ∘ _{s} ∑_{r} α_{r}^{s}.η_{r}^{s}. Then we apply equation (pre + ⊕1) to obtain 2. Now we may proceed as in the previous case.

□

The next step of the completeness proof is to prove the completeness for normal forms.

Lemma 4.13 (Partial Completeness) For all normal forms n, m

n ⪯ m iff n ^{⊑}_{E} m.

Proof The “if” part of the statement follows from the soundness of the proof system. Therefore we only have to prove the “only if” part. We proceed by structural induction on n. If n ≡ Ω we are done. Also the case n ≡ Θ follows easily. So assume n ≡ ∑ ∘ _{j≤N} ∑_{i≤N_{j}} a_{i}^{j}.n_{i}^{j}. As n ↓ we have that m ↓ and has the same form, m ≡ ∑ ∘ _{l≤M} ∑_{k≤M_{l}} b_{k}^{l}.m_{k}^{l}. Let j ≤ N. As n ⪯ m there is an l_{j} ≤ M such that {a_{1}^{j}, …, a_{N_{j}}^{j}} = {b_{1}^{l_{j}}, …, b_{M_{l_{j}}}^{l_{j}} }. This means that we may assume that

Nj = M_{l_{j}} and a_{i}^{j} = b_{i}^{l_{j}} for j ≤ N. Because of the structure of the normal forms Der(a_{i}^{j}, Stb(n)) = Stb_{w}(n_{i}^{j}) and Der(b_{i}^{l_{j}}, Stb(m)) = Stb_{w}(m_{i}^{l_{j}}), i ≤ N_{j}. This implies

Stb_{w}(n_{i}^{j}) ⪯ Stb_{w}(m_{i}^{l_{j}}),

or equivalently that n_{i}^{j} ⪯ m_{i}^{l_{j}}. By induction n_{i}^{j} ^{⊑}_{E} m_{i}^{l_{j}}. This implies

∑_{i≤N_{j}} a_{i}^{j}.n_{i}^{j} ^{⊑}_{E} ∑_{k≤M_{l_{j}}} b_{k}^{l_{j}}.m_{k}^{l_{j}}.  (3)

In a similar way we may show that for all l ≤ M there is a j_{l} ≤ N such that

∑_{i≤N_{j_{l}}} a_{i}^{j_{l}}.n_{i}^{j_{l}} ^{⊑}_{E} ∑_{k≤M_{l}} b_{k}^{l}.m_{k}^{l}.  (4)

From (3) and (4) we get

n ≡ ∑ ∘ _{j≤N} ∑_{i≤N_{j}} a_{i}^{j}.n_{i}^{j} =_{E}
∑ ∘ _{j≤N} ∑_{i≤N_{j}} a_{i}^{j}.n_{i}^{j} ⊕ ∑ ∘ _{l≤M} ∑_{i≤N_{j_{l}}} a_{i}^{j_{l}}.n_{i}^{j_{l}} ^{⊑}_{E}
∑ ∘ _{j≤N} ∑_{k≤M_{l}} b_{k}^{l_{j}}.m_{k}^{l_{j}} ⊕ ∑ ∘ _{l≤M} ∑_{k≤M_{l}} b_{k}^{l}.m_{k}^{l} =_{E} m.

This completes the proof of the theorem. □

Finally we show the completeness for the full language P roc.

Theorem 4.14 (Completeness) For all p, q ∈ P roc

p ⪯ q iff p ^{⊑}_{E_{rec}} q

Proof The “if” implication follows from the soundness of the proof system. For the “only if” part we proceed as follows:

p ⪯ q ⇒ ∀n.p^{n} ⪯ q  (by Lem. 4.3 and 4.2)
⇒ ∀n∃m.p^{n} ⪯ q^{m} ( by Cor. 4.9)
⇒ ∀n∃m.nf(p^{n}) ⪯ nf(q^{m}) ( by Lem. 4.12)
⇒ ∀n∃m.nf(p^{n}) ^{⊑}_{E} nf(q^{m})( by Lem. 4.13)
⇒ ∀n∃m.p^{n} ^{⊑}_{E} q^{m} ( by Lem. 4.12)
⇒ ∀n.p^{n} ^{⊑}_{E_{rec}} q ( by Lem. 4.3)
⇒ p ^{⊑}_{E_{rec}} q ( by the rule (ω)).

Here nf(p^{n}) has the same meaning as in the normalization Theorem 4.12, i. e. nf(p^{n}) is a normal form where nf(p^{n}) =_{E} p^{n}. □

5 Conclusion

In this study we have given three characterizations of the readiness semantics, one by means of lighted button pressing experiments, a bisimulation like one and a modal characterization given some restrictions on the underlying LT S. The most important of these restrictions is the assumption that the communication capabilities are preserved by internal transitions which is not true for standard process description languages like CCS. We have applied the theory on a concrete language that has this property, the regular sublanguage of CCS_{⊕}, CCS without τs. For this language we also characterized the readiness semantics by means of a sound and complete proof system. We used the modal characterization to prove the algebraicity of the behavioural preorder and thus reduced the completeness proof to a completeness proof over recursion free terms.

To complete this study we would like to be able to reason about the full language CCS_{⊕}. As pointed out in the introduction, if we add the parallel operator with the standard operational semantics to the language, the internal actions do not preserve communication capabilities. A future task is therefore to investigate whether the parallel operator may be modelled suitably so it fits into this set–up. Another obvious extension of this work is to use similar methods to obtain the same kind of characterization of the failures semantics [OH86] and the must testing [DNH84]. Most of the work is already done by the author and will be recorded elsewhere.

References

[Abr91] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

[AH92] L. Aceto and M. Hennessy. Termination, deadlock and divergence. Journal of the ACM, 39(1):147–187, January 1992.

[BKO88] J.A. Bergstra, J.W. Klop, and E.-R. Olderog. Readies and failures in the algebra of communicating processes. SIAM Journal on Computing, 17(6):1134–1177, 1988.

[BM92] B. Bloom and A.R. Meyer. Experimenting with process equivalence. Theoretical Computer Science, 101(2):223-237, 1992.

[DNH84] DeNicola, R. and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83-133, 1984.

[Gla90] R.J. van Glabbeek. The linear time – branching time spectrum. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, volume 458 of Lecture Notes in Computer Science, pages 278– 297. Springer-Verlag, 1990.

[Gla93] Robert Jan van Glabbeek. The linear time – branching time spectrum II: the semantics of sequential processes with silent moves. In E. Best, editor, Proceedings CONCUR 93, Hildesheim, Germany, volume 715 of Lecture Notes in Computer Science, pages 66–81. Springer-Verlag, 1993.

[Hen88] M. Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts, 1988.

[HI93] M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes with value-passing. Information and Computation, 107(2):202– 236, 1993.

[Ing95] A. Ingólfsdóttir. A semantic theory for value-passing processes late approach — Part II: A behavioural semantics and full abstractness. Report RS–95–22, BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Institute for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University Centre, April 1995.

[Knu73] D.E. Knuth. Fundamental Algorithms, volume 1 of The Art of Computer Programming. Addison-Wesley, Reading, Massachusetts, 1973. Second edition.

[Mil80] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

[OH86] E.-R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23:9–66, 1986.

[SI94] Bernhard Steffen and Anna Ingólfsdóttir. Characteristic formulae for processes with divergence. Information and Computation, 110(1):149– 163, April 1994.

[Tar55] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.

A Proof of Theorem 2.6

First we state the following results.

Lemma A.1 Let s, t ∈ State, σ ∈ Lab^{∗} and l ∈ Lab. If s ↓ l and s ⟹^{lσ} t ⊁→

then s ⟹^{ε} s′ ⟹^{l} t′ ⟹^{σ} t for some s′, t′ ⊁→.

Proof Follows easily from Assumption 2.2. □

In what follows we assume that the set Lab is infinite. To prove Theorem 2.7 first we review the definition of the readiness semantics as it is given in [OH86]. The set of observations Obs is given by

Obs = {σ, σA|σ ∈ Lab^{∗}, A ⊆_{fin} Lab}.

Then the set of observations of a state s, obs(s) is defined as the least set satisfying

1. s ⟹^{σ} implies σ ∈ obs(s),

2. s ⟹^{σ} s′ ⊁→ and I(s′) = A implies σA ∈ obs(s),

3. s ↑ σ implies σ, σA ∈ obs(s) for all A ⊆_{fin} Lab. Then s and t are readiness equivalent iff obs(s) = obs(t). Now let

Obs^{∗} = {σA|s ∈ Lab^{∗}, A ⊆_{fin} Lab}.

and obs^{∗}(s) be defined as the least set satisfying 2. and 3. in the definition of obs. Then we have Lemma A.2 For all s, t ∈ S and σ ∈ Lab^{∗},

1. obs^{∗}(s) = obs^{∗}(t) implies (∀σ.s ↓ σ ⇔ t ↓ σ),

2. obs(s) = obs(t) iff obs^{∗}(s) = obs^{∗}(t).

Proof

1. This may be proved as follows:

Assume obs^{∗}(s) = obs^{∗}(t) and s ↓ σ. We have the following cases: s ≠⇒^{σ}: Then σA ∉ obs^{∗}(s) = obs^{∗}(t) for all A. This in turn

implies t ↓ σ.

s ⟹^{σ}: Let A = {I(s′)|s ⟹^{σ} s′ ⊁→}. By Lemma 2.3, A is finite and as Lab is infinite we may choose a A ⊆_{fin} Lab such that A ∉ A. Now it is easy to see that σA ∉ obs^{∗}(s) and therefore, by our assumption, σA ∉ obs^{∗}(t). This in turn implies that t ↓ σ.

The statement now follows by symmetry.

2. Now we proceed as follows:

“only if”: Follows immediately.

“if”: Assume obs^{∗}(s) = obs^{∗}(t). By symmetry it is sufficient to prove that whenever o ∈ obs(s) then o ∈ obs(t). The only non-trivial case is when o = σ. So assume σ ∈ obs(s). If s ↑ σ then, by part 1 of this lemma, t ↑ σ and therefore σ ∈ obs(t). Next assume s ↓ σ. Then s ⟹^{σ} s′ where s′ ⊁→. This implies

σI(s′) ∈ obs^{∗}(s) = obs^{∗}(t) ⊆ obs(t),

which in turn implies σ ∈ obs(t).

□

To prove Theorem 2.7 it is now sufficient to prove that

s =_{R} t iff obs^{∗}(s) = obs^{∗}(t).

To obtain this first we extend the transition function Der : Lab × S ↪ S in the standard way to a transition function of the functionality Der : Lab^{∗} × S ↪ S by

• Der(ε, S) = S,

• Der(lσ, S) = S′ iff Der(l, S) = S′′ for some S′′ where Der(σ, S′′) = S′.

Sometimes we write S ⟹^{σ} S′ if Der(σ, S) = S′ and S ⟹^{σ} if S ⟹^{σ} S′ for some S′. Also the convergence predicate ↓ is extended by

• S ↓ ε iff S ↓,

• S ↓ lσ iff S ↓ and (l ∈ I(S) ⇒ Der(l, S) ↓ σ).

We need the following intermediate results.

Lemma A.3 ∀s ∈ State, σ ∈ Lab^{∗}, A ⊆_{fin} Lab, S ∈ S.

1. s ↓ σ iff Stb_{w}(s) ↓ σ, 2. S ↓ σ implies

(a) S ⟹^{σ} implies Der(σ, S) = {s′|∃s ∈ S.s ⟹^{σ} s′ ∧ s′ ⊁→}

(b) {s′|∃s ∈ S.s ⟹^{σ} s′ ∧ s′ ⊁→} ≠ ∅ implies S ⟹^{σ}.

3.

(a) MayP ass(σA, Stb(s)) iff σA ∈ obs^{∗}(s) ∧ s ↓ σ

(b) MustF ail(σA, Stb(s)) iff σA ∉ obs^{∗}(s).

Proof

1. This statement follows from the following two statements:

s ↓ σ iff (∀s′ ∈ Stb_{w}(s). s′ ↓ σ)  (5)

and

S ↓ σ iff (∀s ∈ S. s ↓ σ).  (6)

(where we use the convention ⊥ ↑). We prove each of these statements separately.

Statement (5):

“only if”:We proceed by structural induction on σ. The base case σ = ε follows immediately. For the inductive step assume s ↓ lρ and s′ ∈ Stb_{w}(s) and we will prove that s′ ↓ lρ. Obviously s′ ↓. Next assume s′ ⟹^{l} s′′. Then s ⟹^{l} s′′ and by assumption s′′ ↓ ρ. This implies s′ ↓ lρ.

“if”: Again we proceed by induction on σ and again the base case follows immediately. For the inductive step assume that for all s′ ∈ Stb_{w}(s), s′ ↓ lρ. In particular s′ ↓ for all s′ ∈ Stb_{w}(s) and by the base case, s ↓. So assume s ⟹^{l} s′′. Then, by Lemma A.1, there is an s^{∗} ∈ Stb_{w}(s) such that s^{∗} ⟹^{l} s′′. By assumption s′′ ↓ ρ which implies that s ↓ lρ.

Statement (6):

“only if”: We proceed by induction in σ where the base cases σ = ε, l follow immediately. For the inductive step, assume S ↓ lρ. Then S ↓ l and therefore s ↓ l for all s ∈ S by the base case. In particular s ↓ for all s ∈ S. Next assume s ∈ S and s ⟹^{l} r′, we will prove that r′ ↓ ρ. First we note that l ∈ I(S) and Der(l, S) ↓. Furthermore r′ ↓ and Stb_{w}(r′) ⊆ Der(l, S). By definition of ↓ ρ on S, Der(l, S) ↓ ρ and by induction for all r′′ ∈ Der(l, S), r′′ ↓ ρ. In particular this is true for all r′′ ∈ Stb_{w}(r′). By the “if” part of statement (5), r′ ↓ ρ as we wanted to prove.

“if”: Again we proceed by induction on σ and the base case follows immediately. So assume s ↓ lρ for all s ∈ S. In particular this means that s ↓ for all s ∈ S and therefore, by the base case S ↓. Next assume l ∈ I(S), we will prove that Der(l, S) ↓ ρ. To prove this assume r ∈ Der(l, S). Then s ⟹^{l} r for some s ∈ S. By assumption r ↓ ρ. As this is true for any r ∈ Der(l, S), by induction Der(l, S) ↓ ρ, as wanted.

2. (a) Assume S ↓ σ and S ⟹^{σ}, i.e. Der(σ, S) exists and is different from {⊥} and ∅. Let

D(σ, S) = {s′|∃s ∈ S.s ⟹^{σ} s′ ∧ s′ ⊁→}.

We will prove that D(σ, S) = Der(σ, S) by induction on σ. The base cases σ = ε and σ = l follow immediately. For the inductive step, by definition of Der, by the case σ = l and by induction we get

Der(lσ′, S) = Der(σ′, Der(l, S)) = Der(σ′, D(l, S)) = D(σ′, D(l, S)).

Therefore it only remains to prove that

D(σ′, D(l, S)) = D(lσ′, S).

To prove this first assume s′ ∈ D(lσ′, S). This implies s ⟹^{lσ′} s′ ⊁→ for some s ∈ S. By Lemma A.1, s ⟹^{l} s′′′ ⟹^{σ′} s′ for some s′′′ ⊁→, i.e. for some s′′′ ∈ D(l, S). This implies that s′ ∈ D(σ′, D(l, S)). Next assume s′ ∈ D(σ′, D(l, S)). This means that there is an s′′ ∈

D(l, S) such that s′′ ⟹^{σ′} s′. As s′′ ∈ D(l, S), s ⟹^{l} s′′ for some s ∈ S,

i.e. s ⟹^{lσ′} s′ and therefore s′ ∈ D(lσ′, S).

(b) We prove the statement by induction on σ. The base cases σ = ε and σ = l are obvious. For the inductive step assume that there are s ∈ S

and s′ ⊁→ such that s ⟹^{lσ} s′. Then s ⟹^{l} s′′ ⟹^{σ} s′ for some s′′ ⊁→,

i.e. for some s′′ ∈ Der(l, S). Furthermore Der(l, S) ↓ σ. By induction

Der(l, S) ⟹^{σ}. As S ⟹^{l} Der(l, S) this implies S ⟹^{lσ}.

3. (a) The result follows from the following two statements:

MayP ass(σA, S) iff S ↓ σ, S ⟹^{σ} and A ∈ I(Der(σ, S)) (7)
\begin{matrix}Stb_{w}(s) ↓ σ, Stb_{w}(s) ⟹^{σ} and A ∈ I(Der(σ, Stb_{w}(s))) \\ iff σA ∈ obs^{∗}(s) ∧ s ↓ σ \end{matrix}  (8)

Statement (7):

“only if”: We proceed by induction on σ where the base case is obvious. For the inductive step we proceed as follows. Assume MayP ass(lσA, S), i.e. S ↓, l ∈ I(S) and MayP ass(σ, Der(l, S)). By induction

Der(l, S) ↓ σ, Der(l, S) ⟹^{σ}

and

A ∈ I(Der(σ, Der(l, S))) = I(Der(lσ, S)).

This implies that S ↓ lσ, S ⟹^{lσ} and A ∈ I(Der(lσ, S)). “if”: Again we proceed by induction on σ where the base case is

obvious. For the inductive step we proceed as follows: Assume

S ↓ lσ, S ⟹^{lσ} and A ∈ I(Der(lσ, S)). Then

S ⟹^{l} Der(l, S) ⟹^{σ} Der(σ, Der(l, S)) = Der(lσ, S)

and Der(l, S) ↓ σ. By induction MayP ass(σA, Der(l, S)). As l ∈ I(S) and S ↓ this implies MayP ass(lσA, S).

Statement (8): “only if”: Assume that

Stb(s) ↓ σ, Stb(s) ⟹^{σ} and A ∈ I(Der(σ, Stb(s)).

By 1. of this lemma, s ↓ σ. Furthermore A ∈ I(Der(σ, Stb(s)) implies that I(s′) = A for some s′ ∈ Der(σ, Stb(s)). By 2.(a) of this lemma there is an s′′ ∈ Stb(s) such that s′′ ⟹^{σ} s′, which implies s ⟹^{σ} s′. This shows that σA ∈ obs^{∗}(s).

“if”: Assume

σA ∈ obs^{∗}(s) and s ↓ σ.

Again by 1. of this lemma, s ↓ σ implies Stb(s) ↓ σ. As σA ∈ obs^{∗}(s) and s ↓ σ then s ⟹^{σ} s′ ⊁→ for some s′ where I(s′) = A. By Lemma A.1, there is an s′′ ∈ Stb(s) such that s′′ ⟹^{σ} s′. By 2.(b) and (a) of this lemma, Stb(s) ⟹^{σ} and s′ ∈ Der(σ, S). This implies that A ∈ I(Der(σ, S)).

(b) May be proved in a similar way by first proving the following two statements

MustF ail(σA, S) iff S ↓ σ, S ⟹^{σ} and A ∉ I(Der(σ, S)) (9)
S ↓ σ, S ⟹^{σ} and A ∉ I(Der(σ, S)) iff σA ∉ obs^{∗}(s). (10)

Here we note that σA ∉ obs^{∗}(s) implies s ↓ σ.

□

Proof of Theorem 2.7

As pointed out before it is sufficient to prove that

obs^{∗}(s) = obs^{∗}(t) iff s =_{R} t.

We prove each implication separately.

“only if”: Let obs^{∗}(s) = obs^{∗}(t). First assume MayP ass(σA, Stb_{w}(s)), we will prove that MayP ass(σA, Stb_{w}(t)). By Lemma A.3.3 we have that σA ∈ obs^{∗}(s) = obs^{∗}(t) and s ↓ σ. Lemma A.2.1 implies t ↓ σ. Again by Lemma A.3.3. we may conclude that MayP ass(σA, Stb(t)). Similarly we prove that MustF ail(σ, Stb_{w}(s)) implies MustF ail(σ, Stb_{w}(s)) and the result follows by symmetry.

“if”: Assume that obs^{∗}(s) ≠ obs^{∗}(t) witnessed by σA ∈ obs^{∗}(s) but σA ∉ obs^{∗}(t). By Lemma A.3.3, MustF ail(σA, Stb(t)) and ¬MustF ail(σA, Stb(s)).

Recent Publications in the BRICS Report Series

RS-96-43 Anna Ing� olfsd� ottir. Weak Semantics Based on Lighted Button Pressing Experiments: An Alternative Characterization of the Readiness Semantics. November 1996. 36 pp. An extended abstract to appear in the proceedings of the 10th Annual International Conference of the European Association for Computer Science Logic, CSL ’96.

RS-96-42 Gerth St�lting Brodal and Sven Skyum. The Complexity of Computing the k-ary Composition of a Binary Associative Operator. November 1996. 15 pp.

RS-96-41 Stefan Dziembowski. The Fixpoint Bounded-Variable Queries are PSPACE-Complete. November 1996. 16 pp. Presented at the 10th Annual International Conference of the European Association for Computer Science Logic, CSL ’96.

RS-96-40 Gerth St�lting Brodal, Shiva Chaudhuri, and Jaikumar Radhakrishnan. The Randomized Complexity of Maintaining the Minimum. November 1996. 20 pp. To appear in a special issue of Nordic Journal of Computing devoted to the proceedings of SWAT ’96. Appears in Karlson and Lingas, editors, Algorithm Theory: 5th Scandinavian Workshop, SWAT ’96 Proceedings, LNCS 1097, 1996, pages 4�15.

RS-96-39 Hans H� uttel and Sandeep Shukla. On the Complexity of Deciding Behavioural Equivalences and Preorders � A Survey. October 1996. 36 pp.

RS-96-38 Hans H� uttel and Josva Kleist. Objects as Mobile Processes. October 1996. 23 pp.

RS-96-37 Gerth St�lting Brodal and Chris Okasaki. Optimal Purely Functional Priority Queues. October 1996. 27 pp. To appear in Journal of Functional Programming, 6(6), December 1996.

RS-96-36 Luca Aceto, Willem Jan Fokkink, and Anna Ing� olfsd� ottir. On a Question of A. Salomaa: The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based. October 1996. 16 pp.