                         SOS 2005 Preliminary Version

Divide and Congruence Applied to η-Bisimulation

Wan Fokkink^{1}

Vrije Universiteit Amsterdam, Department of Computer Science, Amsterdam CWI, Department of Software Engineering, Amsterdam

Rob van Glabbeek^{2}

National ICT Australia, Sydney

Univ. of New South Wales, School of Computer Science and Engineering, Sydney

Paulien de Wind^{3}

Vrije Universiteit Amsterdam, Department of Computer Science, Amsterdam

Abstract

We present congruence formats for η- and rooted η-bisimulation equivalence. These formats are derived using a method for decomposing modal formulas in process algebra. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra.

Key words: Structural operational semantics; modal logic; decomposition; congruence; η-bisimulation

1 Introduction

Structural operational semantics [16] provides process algebras and specification languages with an interpretation. It generates a labelled transition system, in which states are the closed terms over a (single-sorted, first-order) signature, and transitions between states may be supplied with labels. The transitions between states are obtained from a transition system specification, which consists of a set of proof rules called transition rules.

1 Email: wanf@cs.vu.nl
2 Email: rvg@cs.stanford.edu
3 Email: pdwind@cs.vu.nl

This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Fokkink, van Glabbeek and de Wind

Labelled transition systems can be distinguished from each other by a wide range of semantic equivalences, based on e.g. branching structure or decorated versions of execution sequences. Van Glabbeek [8] classified equivalences for processes that take into account the internal action τ. Here we focus on one such equivalence, called η-bisimulation [1].

In general a semantic equivalence induced by a transition system specification is not a congruence, i.e. the equivalence class of a term f(p_{1}, …, p_{n}) need not be determined by the equivalence classes of its arguments p_{1}, …, p_{n}. Being a congruence is an important property, for instance in order to fit the equivalence into an axiomatic framework. Syntactic formats for transition rules have been developed with respect to several semantic equivalences, to ensure that such an equivalence is a congruence. These formats help to avoid repetitive congruence proofs. Several congruence formats were introduced for bisimulation, such as the De Simone format [17], the GSOS format [4], the tyft/tyxt format [13], and the ntyft/ntyxt format [12]. Bloom [2] introduced congruence formats for weak and branching bisimulation and for rooted weak and branching bisimulation. These formats include so-called patience rules for arguments i of function symbols f, which imply that a term f(p_{1}, …, p_{n}) inherits the τ-transitions of its argument p_{i}. Furthermore, arguments of function symbols that contain running processes are marked, and this marking is used to restrict occurrences of variables in transition rules. Recently, van Glabbeek [11] significantly simplified the formats from [2], and presented similar formats for delay and η-bisimulation and for rooted delay and η-bisimulation.

Van Glabbeek [9,8] gave characterisations of equivalences in terms of the observations that an experimenter could make during a session with a process. Modal logic captures such observations. A modal characterisation of an equivalence consists of a class C of modal formulas such that two processes are equivalent if and only if they make true the same formulas in C. For instance, Hennessy-Milner logic [14] is the modal characterisation of bisimulation.

Larsen and Xinxin [15] introduced a method for decomposing formulas from Hennessy-Milner logic for concrete processes, with respect to terms from a process algebra with a structural operational semantics in De Simone format. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy certain other formulas, obtained by decomposing the original formula. This method was extended by Bloom, Fokkink & van Glabbeek [3] to ntyft/ntyxt format without lookahead, and by Fokkink, van Glabbeek & de Wind to tyft/tyxt format in the full version of [7]. In [3], the decomposition method was applied to obtain congruence formats for behavioural equivalences from [9]. The idea is that given an equivalence and its modal characterisation C, the congruence format for this equivalence must ensure that decomposing a formula in C always produces formulas in C.

In an unpublished manuscript, we extend the work of [3] to processes with τ-transitions. We present a method for decomposing formulas from modal logic for processes with τ-transitions, and use this decomposition method to obtain congruence formats for branching and rooted branching bisimulation.

In the current paper, we use this decomposition method to obtain congruence formats for η- and rooted η-bisimulation. Thus we drive home the point that, in contrast to the ad hoc construction of congruence formats from the past, we can now systematically derive expressive congruence formats from the modal characterisations of semantic equivalences. Our formats use two predicates on arguments of function symbols, to mark both running processes and processes that may have started running.

2 Preliminaries

2.1 Equivalences on labelled transition systems

A labelled transition system (LTS) is a pair (ℙ, →) with ℙ a set of processes and → ⊆ ℙ×(A∪{τ})×ℙ where τ is an internal action and A a set of actions not containing τ. We use α, β, γ for elements of A ∪ {τ} and a, b for elements of A. We write p ⟶^{α} q for (p, α, q) ∈ → and p −̸→^{α} for ¬∃q ∈ ℙ : p ⟶^{α} q, and ⟹^{ϵ} for the transitive-reflexive closure of ⟶^{τ}.

Definition 2.1 [1] A symmetric relation B ⊆ ℙ × ℙ is an η-bisimulation if pBq and p ⟶^{α} p′ implies that either α = τ and p′ B q, or q ⟹^{ϵ} q′ ⟶^{α} q′′ ⟹^{ϵ} q′′′ for some q′, q′′, q′′′ with pBq′ and p′Bq′′′. Processes p, q are η-bisimilar, denoted by p\underline{↔}_{η} q, if there exists an η-bisimulation B with pBq.

η-bisimulation is not a congruence with respect to most process algebras from the literature, meaning that the equivalence class of a term f(p_{1}, …, p_{n}) is not always determined by the equivalence classes of its arguments p_{1}, …, p_{n}. A rootedness condition remedies this imperfection.

Definition 2.2 [1] A symmetric relation R ⊆ ℙ×ℙ is a rooted η-bisimulation

if pRq and p ⟶^{α} p′ implies that q ⟶^{α} q′ ⟹^{ϵ} q′′ for some q′, q′′ with p′ \underline{↔}_{η} q′′.

Processes p, q are rooted η-bisimilar, denoted by p\underline{↔}_{rη} q, if there exists a rooted η-bisimulation R with pRq.

2.2 Modal logic

Modal logic aims to formulate properties of processes in an LTS. Following [8], we extend Hennessy-Milner logic [14] with the modal connective ⟨ϵ⟩.

Definition 2.3 The class 𝕆 of modal formulas is defined as follows, where I ranges over all index sets:

𝕆 φ ::= ⋀_{i∈I}φ_{i} | ¬φ | ⟨α⟩φ | ⟨ϵ⟩φ

p ⊧ φ denotes that p satisfies φ. By definition, p ⊧ ⟨α⟩φ if p ⟶^{α} p′ with p′ ⊧ φ, and p ⊧ ⟨ϵ⟩φ if p ⟹^{ϵ} p′ with p′ ⊧ φ. We use abbreviations ⊤ for the empty conjunction, φ_{1} ∧ φ_{2} for ⋀_{i∈{1,2}} φ_{i}, and φ⟨α⟩φ′ for φ ∧ ⟨α⟩φ′. We write φ ≡ φ′ if p ⊧ φ ⇔ p ⊧ φ′ for any process p in any LTS.

Definition 2.4 The subclasses 𝕆_{η} and 𝕆_{rη} of 𝕆 are defined as follows:

𝕆_{η} φ ::= ⋀_{i∈I}φ_{i} | ¬φ | ⟨ϵ⟩φ | ⟨ϵ⟩(φ⟨a⟩⟨ϵ⟩φ)  (a ∈ A)
𝕆_{rη} φ ::= ⋀_{i∈I}φ_{i} | ¬φ | ⟨α⟩⟨ϵ⟩φ̂ | φ̂  (φ̂ ∈ 𝕆_{η}, α ∈ A ∪ {τ})

The classes 𝕆_{η}^{≡} and 𝕆_{rη}^{≡} are the closures of 𝕆_{η}, respectively 𝕆_{rη}, under ≡.

The last clause in the definition of 𝕆_{rη} guarantees that 𝕆_{η} ⊆ 𝕆_{rη}, which we need in the proof of Prop. 3.7. Also without this clause it would follow that 𝕆_{η}^{≡} ⊆ 𝕆_{rη}^{≡}, using structural induction and ⟨ϵ⟩φ ≡ φ ∧ ⟨τ⟩⟨ϵ⟩φ.

For L ⊆ 𝕆, we write p ∼_{L} q if p and q satisfy the same formulas in L. Note that, trivially, p ∼_{𝕆_{η}} q ⇔ p ∼_{𝕆_{η}^{≡}} q and p ∼_{𝕆_{rη}} q ⇔ p ∼_{𝕆_{rη}^{≡}} q.

Theorem 2.5 p\underline{↔}_{η} q ⇔ p ∼_{𝕆_{η}} q and p\underline{↔}_{rη} q ⇔ p ∼_{𝕆_{rη}} q, for all p, q ∈ ℙ.

A proof of this theorem is presented in the appendix.

2.3 Structural operational semantics

Let V be an infinite set of variables, with typical elements x, y, z. A syntactic object is closed if it does not contain any variables. A signature is a set Σ of function symbols f with arity ar(f). We always take |Σ|, |A| ≤ |V |. The set 𝕋(Σ) of terms over Σ and V is defined as usual. t, u denote terms and p, q closed terms. var(t) is the set of variables that occur in t. A substitution is a partial function from V to 𝕋(Σ). A closed substitution σ is a total function from V to closed terms.

Definition 2.6 A (positive or negative) literal is an expression t ⟶^{α} t′ or t −̸→^{α}. A (transition) rule is of the form \frac{H}{t⟶^{α}t′} with H a set of literals called the premises. t ⟶^{α} t′ is the conclusion and t the source of the rule. A rule \frac{∅}{t⟶^{α}t′} is also written t ⟶^{α} t′. A transition system specification (TSS) is a set of transition rules.

Definition 2.7 Let P = (Σ, R) be a TSS. An irredundant proof from P of a rule \frac{H}{t⟶^{α}t′} is a well-founded tree with the nodes labelled by literals and some of the leaves marked “hypothesis”, such that the root has label t ⟶^{α} t′, H is the set of labels of the hypotheses, and if μ is the label of a node that is not a hypothesis and K is the set of labels of the children of this node, then μ is positive and \frac{K}{μ} is a substitution instance of a rule in R.

The proof of \frac{H}{t⟶^{α}t′} is called irredundant because H must equal (instead of include) the set of labels of the hypotheses. This irredundancy will be crucial for the preservation of our congruence formats in Sect. 3.1 (see Prop. 3.4).

A TSS is meant to specify an LTS in which the transitions are closed positive literals. A TSS with only positive premises specifies an LTS in a straightforward way, but it is not so easy to associate an LTS to a TSS with negative premises. From [10] we adopt the notion of a well-supported proof of a closed literal. Literals t ⟶^{α} t′ and t −̸→^{α} are said to deny each other.

Definition 2.8 Let P = (Σ, R) be a TSS. A well-supported proof from P of a closed literal μ is a well-founded tree with the nodes labelled by closed literals, such that the root is labelled by μ, and if ν is the label of a node and K is the set of labels of the children of this node, then:

(i) either ν is positive and \frac{K}{ν} is a closed substitution instance of a rule in R; (ii) or ν is negative and for each set N of closed negative literals with \frac{N}{κ}

irredundantly provable from P and κ a closed positive literal denying ν, a literal in K denies one in N.

P ⊢_{ws} μ denotes that a well-supported proof from P of μ exists. P is complete if for each p and α, either P ⊢_{ws} p −̸→^{α} or P ⊢_{ws} p ⟶^{α} p′ for some p′.

A complete TSS specifies an LTS, consisting of the ws-provable closed positive literals.

2.4 Notions regarding transition rules

In this section we present terminology for syntactic restrictions on rules, originating from [3,12,13].

Definition 2.9 An ntytt rule is a rule in which the right-hand sides of positive premises are variables that are all distinct, and that do not occur in the source. An ntytt rule is an ntyxt rule if its source is a variable, an ntyft rule if its source contains exactly one function symbol and no multiple occurrences of variables, and an nxytt rule if the left-hand sides of its premises are variables.

Definition 2.10 A variable in a rule is free if it occurs neither in the source nor in right-hand sides of premises. A rule has lookahead if some variable occurs in the right-hand side of a premise and in the left-hand side of a premise. A rule is decent if it has no lookahead and does not contain free variables.

The ntyft/ntyxt and ready simulation formats [12,3] were originally introduced to guarantee congruence for bisimulation and ready simulation.

Definition 2.11 A TSS is in ntyft/ntyxt format if it consists of ntyft and ntyxt rules, and in ready simulation format if moreover its rules do not have lookahead.

A predicate ℵ marks arguments of function symbols that contain running processes (cf. [3]). Typically, in process algebra, ℵ holds for the arguments of the merge ∥, but not for the arguments of alternative composition +.

Definition 2.12 Let ℵ be a unary predicate on {(f, i) | 1 ≤ i ≤ ar(f), f ∈ Σ}. If ℵ(f, i), then argument i of f is liquid; otherwise it is frozen. An occurrence of x in t is at an ℵ-liquid position if either t = x, or t = f(t_{1}, …, t_{ar(f)}) and the occurrence is at an ℵ-liquid position in t_{i} for a liquid argument i of f.

A patience rule for an argument i of a function symbol f expresses that term f(p_{1}, …, p_{n}) inherits the τ-transitions of argument p_{i} (cf. [2,5]). We will require the presence of patience rules for liquid arguments.

Definition 2.13 An ntyft rule is a patience rule for (f, i), with 1 ≤ i ≤ ar(f), if it is of the form

\frac{x_{i} ⟶^{τ} y}{f(x_{1}, …, x_{i}, …, x_{ar(f)}) ⟶^{τ} f(x_{1}, …, x_{i−1}, y, x_{i+1} …, x_{ar(f)})}

It is an ℵ-patience rule if ℵ(f, i).

An ntytt rule is patient with respect to ℵ if it is irredundantly provable from the ℵ-patience rules. Such rules have the form \frac{t⟶^{τ}y}{C[t]⟶^{τ}C[y]} with C[] an ℵ-liquid context, meaning that the context symbol [] occurs at an ℵ-liquid position.

Definition 2.14 A TSS is ℵ-patient if it contains all ℵ-patience rules. It is abstraction-free if only patience rules have a conclusion of the form t ⟶^{τ} u.

2.5 Decomposition of modal formulas

To decompose modal formulas, we use a result from [3], where for any TSS P in ready simulation format a collection of decent nxytt rules, called P -ruloids, is constructed. We explain this construction on a rather superficial level; the precise transformation can be found in [3].

First P is converted to a TSS in decent ntyft format. In this conversion from [13], free variables in a rule are replaced by closed terms, and if the source is of the form x then this variable is replaced by a term f(x_{1}, …, x_{n}) for each f ∈ Σ. Next, using a construction from [6], left-hand sides of positive premises are reduced to variables. Roughly the idea is, given a premise f(t_{1}, …, t_{n}) ⟶^{α} y in a rule r, and a rule \frac{H}{f(x_{1},...,x_{n})⟶^{α}t}, to transform r by replacing the aforementioned premise by H, y by t, and the x_{i} by the t_{i}; this is repeated (transfinitely) until all positive premises with a non-variable left-hand side have disappeared. In the final transformation step, rules with a negative conclusion t −̸→^{α} are introduced. The motivation is that instead of the notion of well-founded provability in Def. 2.8, we want a more constructive notion like Def. 2.7, by making it possible that a negative premise is matched with a negative conclusion. A rule r with a conclusion f(x_{1}, …, x_{n}) −̸→^{α} is obtained by picking one premise from each rule with a conclusion f(x_{1}, …, x_{n}) ⟶^{α} t, and including the denial of each of the selected premises as a premise of r. For this last transformation it is essential that rules do not have lookahead.

The resulting TSS, which is in decent ntyft format, is denoted by P^{+}. In [3] it is established that P^{+} ⊢ μ ⇔ P ⊢_{ws} μ for all closed literals μ. The notion of irredundant provability is adapted in a straightforward fashion to accommodate rules with a negative conclusion. P -ruloids are the decent nxytt rules that are irredundantly provable from P^{+}. The following correspondence result from [3] between a TSS and its ruloids plays a crucial role in the decomposition method employed here. It says that there is a well-supported proof from P of a transition p ⟶^{a} q, with p a closed substitution instance of a term t, if and only if there is a proof of this transition that uses at the root a P -ruloid with source t.

Proposition 2.15 Let P be a TSS in ready simulation format. Then P ⊢_{ws} σ(t) ⟶^{α} p if and only if there are a P -ruloid \frac{H}{t⟶^{α}u} and a σ′ with P ⊢_{ws} σ′(μ) for μ ∈ H, σ′(t) = σ(t) and σ′(u) = p.

We now show how one can decompose formulas from 𝕆. To each term t and formula φ we assign a set t^{−1}(φ) of decomposition mappings ψ : V → 𝕆. Each of these mappings ψ ∈ t^{−1}(φ) guarantees that σ(t) ⊧ φ if σ(x) ⊧ ψ(x) for x ∈ var(t). Vice versa, whenever σ(t) ⊧ φ, there is a decomposition mapping ψ ∈ t^{−1}(φ) with σ(x) ⊧ ψ(x) for x ∈ var(t). This is formalised in Thm. 2.17.

Definition 2.16 Let P be an ℵ-patient, abstraction-free TSS in ready simulation format. We define ·^{−1} : 𝕋(Σ)×𝕆 → 𝒫(V → 𝕆) as follows. Let t denote a univariate term, i.e. without multiple occurrences of the same variable.

(i) ψ ∈ t^{−1}(⋀_{i∈I} φ_{i}) iff for x ∈ V

ψ(x) = ⋀_{i∈I} ψ_{i}(x)

where ψ_{i} ∈ t^{−1}(φ_{i}) for i ∈ I.

(ii) ψ ∈ t^{−1}(⟨α⟩φ) iff there is a P -ruloid \frac{H}{t⟶^{α}u} and a χ ∈ u^{−1}(φ) with

ψ(x) = \{ \begin{matrix}χ(x) ∧ ⋀_{x⟶^{β}y∈H} ⟨β⟩χ(y) ∧ ⋀_{x−̸→^{γ}∈H} ¬⟨γ⟩⊤ & if x ∈ var(t) \\ ⊤ & if x ∉ var(t) \end{matrix}

(iii) ψ ∈ t^{−1}(¬φ) iff there is a function h : t^{−1}(φ) → var(t) with

ψ(x) = ⋀_{χ∈h^{−1}(x)}¬χ(x) for x ∈ V

(iv) ψ ∈ t^{−1}(⟨ϵ⟩φ) iff there is a χ ∈ t^{−1}(φ) with

ψ(x) = \{ \begin{matrix}⟨ϵ⟩χ(x) & if x occurs ℵ-liquid in t \\ χ(x) & otherwise \end{matrix}

(v) ψ ∈ ρ(t)^{−1}(φ) for ρ : var(t) → V not injective iff there is a χ ∈ t^{−1}(φ)

with

ψ(x) = ⋀_{y∈ρ^{−1}(x)} χ(y) for x ∈ V

It is not hard to see that if ψ ∈ t^{−1}(φ), then ψ(x) ≡ ⊤ for x ∉ var(t).

To explain the idea behind Def. 2.16, we expand on two of its cases. Consider t^{−1}(⟨α⟩φ), and let σ be any closed substitution. The question is under which conditions ψ(x) ∈ 𝕆 on σ(x), for x ∈ var(t), there is a transition σ(t) ⟶^{α} q with q ⊧ φ. According to Prop. 2.15, there is such a transition if and only if there is a closed substitution σ′ with σ′(t) = σ(t) and a P -ruloid \frac{H}{t⟶^{α}u} such that (1) the premises in σ′(H) are satisfied and (2) σ′(u) ⊧ φ. The first condition is covered if for x ∈ var(t), ψ(x) contains conjuncts ⟨β⟩⊤ for x ⟶^{β} y ∈ H and conjuncts ¬⟨γ⟩⊤ for x −̸→^{γ} ∈ H. By adding a conjunct χ(x), and replacing each conjunct ⟨β⟩⊤ by ⟨β⟩χ(y), for some χ ∈ u^{−1}(φ), the second condition is covered as well.

Consider t^{−1}(¬φ), and let σ be any closed substitution. We have σ(t) |̸= φ if and only if there is no χ ∈ t^{−1}(φ) such that σ(x) ⊧ χ(x) for all x ∈ var(t). In other words, for each χ ∈ t^{−1}(φ), ψ(x) must contain a conjunct ¬χ(x), for some x ∈ var(t).

The following theorem, whose proof is omitted here, will be the key to the forthcoming congruence results.

Theorem 2.17 Given a complete TSS in ready simulation format that contains the ℵ-patience rules for some ℵ. For any term t, closed substitution σ and φ ∈ 𝕆:

σ(t) ⊧ φ ⇔ ∃ψ ∈ t^{−1}(φ) ∀x ∈ var(t) : σ(x) ⊧ ψ(x)

3 η-Bisimulation as a Congruence

We proceed to apply the decomposition method from the previous section to derive congruence formats for η- and rooted η-bisimulation equivalence. The idea is that the η-bisimulation format must guarantee that a formula from 𝕆_{η} is always decomposed into formulas from 𝕆_{η}^{≡} (see Prop. 3.6). Likewise, the rooted η-bisimulation format must guarantee that a formula from 𝕆_{rη} is always decomposed into formulas from 𝕆_{rη}^{≡} (see Prop. 3.7). This implies the desired congruence results (see Thm. 3.9 and Thm. 3.11).

In order minimise the complexity inherent in the combination of modal decomposition and abstraction, we apply the decomposition method to abstraction-free TSSs, and extend our results to the general case using the well-known compositionality of the abstraction operator.

3.1 Congruence formats

We assume a second predicate Λ on arguments of function symbols, to denote that the processes they contain may have started running (but may currently be resting). Always ℵ ⊆ Λ. Typically, in process algebra, ℵ holds for the first argument of sequential composition while only Λ holds for the second argument, and Λ does not hold for the arguments of alternative composition.

Definition 3.1 Let ℵ ⊆ Λ. An ntytt rule \frac{H}{t⟶^{α}u} is rooted η-bisimulation safe with respect to ℵ and Λ if:

(i) it has no lookahead, (ii) right-hand sides of premises occur only at ℵ-liquid positions in u, and (iii) if x occurs exactly once^{4} in t, at a Λ-liquid position, then:

(a) all occurrences of x in the rule are at Λ-liquid positions,

(b) x has no ℵ-liquid occurrences in left-hand sides of negative premises,

(c) x has at most one ℵ-liquid occurrence in the left-hand side of one positive premise, and this premise has a label from A, and

(d) if x occurs at an ℵ-frozen position in t, then x does not occur at ℵ-liquid positions in left-hand sides of premises.

In case Λ is the universal predicate, we say that the rule is η-bisimulation safe with respect to ℵ.

Definition 3.2 A TSS in ready simulation format is in rooted η-bisimulation format if, for some ℵ ⊆ Λ, it consists of the ℵ-patience rules and rules that are rooted η-bisimulation safe with respect to ℵ and Λ.

A TSS in ready simulation format is in η-bisimulation format if, for some ℵ, it consists of the ℵ-patience rules and rules that are η-bisimulation safe with respect to ℵ.

The operators initial priority (with frozen argument), binary Kleene star (with both arguments frozen) and action refinement (with only the second argument frozen) of [3] fit the rooted η-bisimulation format. In these applications, as well as for capturing the operators of CCS and similar languages, it suffices to take Λ = ℵ. In the following example this is not possible.

Example 3.3 Let f be a binary operator that interleaves actions α ∈ A∪{τ} from its arguments, until its first arguments produces an action crash. Then f performs the actions alert and prevent meltdown, without any τ-steps in between, and subsequently continues as its second argument.

\frac{x ⟶^{α} x′}{f(x, y) ⟶^{α} f(x′, y)} \frac{y ⟶^{α} y′}{f(x, y) ⟶^{α} f(x, y′)} \frac{x ⟶^{crash} x′}{f(x, y) ⟶^{alert} pm.y} pm.y ⟶^{meltdown}^{prevent} y

pm is a CCS action-prefixing operator. For this TSS to be in (rooted) ηbisimulation format it is essential that the argument of pm is marked as ℵfrozen (and hence not accompanied by a patience rule) but Λ-liquid, for it harbours a process that has already started but is not currently running.

In the definition of modal decomposition, we did not use the rules from the original TSS P, but the P -ruloids. Therefore we must verify that if P is in (rooted) η-bisimulation format, then so are the P -ruloids.

Proposition 3.4 If a TSS P is in (rooted) η-bisimulation format with respect to some ℵ, then each P -ruloid is either patient or (rooted) η-bisimulation safe with respect to ℵ.

4 Only the requirements for rules in which t is univariate matter. The current formulation of Def. 3.1 for general terms t paves the way for Prop. 3.4.

The proof of Prop. 3.4 is omitted here. The key part of the proof is to show that the decent (rooted) η-bisimulation format is preserved under irredundant provability. (The adjective irredundant is essential here.)

3.2 Preservation of modal characterisations

From now on we will mention patient and (rooted) branching safe rules without reference to the accompanying predicates ℵ and Λ.

Lemma 3.5 Given a TSS in ready simulation format. For any term t, φ ∈ 𝕆 and variable x that occurs only ℵ-liquid in t, ψ ∈ t^{−1}(⟨ϵ⟩φ) ⇒ ψ(x) ≡ ⟨ϵ⟩ψ(x).

Proof. Let ψ ∈ t^{−1}(⟨ϵ⟩φ) and x occur only ℵ-liquid in t. Then by Def. 2.16.iv and 2.16.v, ψ(x) is of the form ⋀_{i∈I}⟨ϵ⟩φ_{i}. So ψ(x) ≡ ⟨ϵ⟩ψ(x). □

Proposition 3.6 Let P be an abstraction-free TSS in rooted η-bisimulation format. For any term t and variable x that occurs only Λ-liquid in t:

φ ∈ 𝕆_{η} ⇒ ∀ψ ∈ t^{−1}(φ) : ψ(x) ∈ 𝕆_{η}^{≡}

Proof. We apply structural induction on φ. Let φ ∈ 𝕆_{η}. Let t ∈ 𝕋(Σ) and ψ ∈ t^{−1}(φ), and let x occur only Λ-liquid in t. First we treat the case where t is univariate. If x ∉ var(t), then ψ(x) = ⊤ ∈ 𝕆_{η}^{≡}. Suppose x occurs once in t.

• φ = ⋀_{i∈I} φ_{i} with φ_{i} ∈ 𝕆_{η} for i ∈ I. By Def. 2.16.i, ψ(x) = ⋀_{i∈I} ψ_{i}(x) with ψ_{i} ∈ t^{−1}(φ_{i}) for i ∈ I. By induction, ψ_{i}(x) ∈ 𝕆_{η}^{≡} for i ∈ I, so ψ(x) ∈ 𝕆_{η}^{≡}.

• φ = ¬φ′ with φ′ ∈ 𝕆_{η}. By Def. 2.16.iii, there is a function h : t^{−1}(φ′) → var(t) such that ψ(x) = ⋀_{χ∈h^{−1}(x)} ¬χ(x). By induction, χ(x) ∈ 𝕆_{η}^{≡} for χ ∈ h^{−1}(x), so ψ(x) ∈ 𝕆_{η}^{≡}.

• φ = ⟨ϵ⟩φ′ with φ′ ∈ 𝕆_{η}. By Def. 2.16.iv, either ψ(x) = ⟨ϵ⟩χ(x) or ψ(x) = χ(x) for some χ ∈ t^{−1}(φ′). By induction on formula size, χ(x) ∈ 𝕆_{η}^{≡}. So ψ(x) ∈ 𝕆_{η}^{≡}.

• φ = ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{η}. By Def. 2.16.iv, either ψ(x) = ⟨ϵ⟩χ(x) or ψ(x) = χ(x) for some χ ∈ t^{−1}(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}). By Def. 2.16.i, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨a⟩⟨ϵ⟩φ_{2}). By induction on formula size, χ_{1}(x) ∈ 𝕆_{η}^{≡}. By Def. 2.16.ii,

χ_{2}(x) = ξ(x) ∧ ⋀_{x⟶^{β}y∈H}⟨β⟩ξ(y) ∧ ⋀_{x−̸→^{γ}∈H} ¬⟨γ⟩⊤

for some ξ ∈ u^{−1}(⟨ϵ⟩φ_{2}) and some P -ruloid \frac{H}{t⟶^{a}u}. Since a ≠ τ, by Prop. 3.4, \frac{H}{t⟶^{a}u} is rooted η-bisimulation safe. Since the occurrence of x in t is Λliquid, x occurs only Λ-liquid in u. Moreover, variables in right-hand sides of premises in H occur only ℵ-liquid (hence Λ-liquid) in u. So in the previous case we proved that ξ(x) ∈ 𝕆_{η}^{≡} and ξ(y) ∈ 𝕆_{η}^{≡} for x ⟶^{β} y ∈ H. We distinguish two cases.

Case 1: The occurrence of x in t is ℵ-liquid. Then ψ(x) = ⟨ϵ⟩χ(x). Since \frac{H}{t⟶^{a}u} is rooted η-bisimulation safe and an nxytt rule, x does not occur in left-hand sides of negative premises in H, and at most once in the lefthand side of one positive premise in H, which is of the form x ⟶^{b} y with b ∈ A. The right-hand side, y, of such a premise, occurs only ℵ-liquid in u, so by Lem. 3.5, ξ(y) ≡ ⟨ϵ⟩ξ(y). Hence, either χ_{2}(x) = ξ(x) or χ_{2}(x) = ξ(x)⟨b⟩ξ(y) ≡ ξ(x)⟨b⟩⟨ϵ⟩ξ(y). Since ψ(x) = ⟨ϵ⟩(χ_{1}(x) ∧ χ_{2}(x)), either ψ(x) = ⟨ϵ⟩(χ_{1}(x)∧ξ(x)) ∈ 𝕆_{η}^{≡} or ψ(x) ≡ ⟨ϵ⟩(χ_{1}(x)∧ξ(x)⟨b⟩⟨ϵ⟩ξ(y)) ∈ 𝕆_{η}^{≡}.

Case 2: The occurrence of x in t is ℵ-frozen. Then ψ(x) = χ(x). Since \frac{H}{t⟶^{a}u} is rooted η-bisimulation safe and an nxytt rule, x does not occur in left-hand sides of premises in H. So χ_{2}(x) = ξ(x), and thus ψ(x) = χ_{1}(x) ∧ χ_{2}(x) = χ_{1}(x) ∧ ξ(x) ∈ 𝕆_{η}^{≡}.

Finally, suppose t is not univariate. Then t = ρ(u) for some univariate term u and ρ : var(u) → V not injective. By Def. 2.16.v, ψ(x) = ⋀_{y∈ρ^{−1}(x)} χ(y) for some χ ∈ u^{−1}(φ). Since u is univariate, and for each y ∈ ρ^{−1}(x) the occurrence in u is Λ-liquid, χ(y) ∈ 𝕆_{η}^{≡} for y ∈ ρ^{−1}(x). Hence, ψ(x) ∈ 𝕆_{η}^{≡}. □

Proposition 3.7 Let P be an abstraction-free TSS in rooted η-bisimulation format. For any term t and variable x:

φ ∈ 𝕆_{rη} ⇒ ∀ψ ∈ t^{−1}(φ) : ψ(x) ∈ 𝕆_{rη}^{≡}

Proof. We apply structural induction on φ. Let φ ∈ 𝕆_{rη}, t ∈ 𝕋(Σ) and ψ ∈ t^{−1}(φ). We restrict attention to the case where t is univariate; the general case then follows just as at the end of the proof of Prop. 3.6. If x ∉ var(t), then ψ(x) = ⊤ ∈ 𝕆_{rη}^{≡}. So suppose x occurs once in t.

• The cases φ = ⋀_{i∈I} φ_{i} and φ = ¬φ′ proceed as in the proof of Prop. 3.6.

• φ = ⟨α⟩⟨ϵ⟩φ′ with φ′ ∈ 𝕆_{η}. By Def. 2.16.ii,

ψ(x) = χ(x) ∧ ⋀_{x⟶^{β}y∈H}⟨β⟩χ(y) ∧ ⋀_{x−̸→^{γ}∈H} ¬⟨γ⟩⊤

for some χ ∈ u^{−1}(⟨ϵ⟩φ′) and some P -ruloid \frac{H}{t⟶^{α}u}. By induction, χ(x) ∈ 𝕆_{rη}. (Induction may be applied because ⟨ϵ⟩φ′ ∈ 𝕆_{η} ⊆ 𝕆_{rη} and ⟨ϵ⟩φ′ is a strict subformula of φ.) By Prop. 3.4, \frac{H}{t⟶^{α}u} is either rooted η-bisimulation safe or patient. Thus variables in right-hand sides of premises in H occur only ℵ-liquid in u. By Prop. 3.6, χ(y) ∈ 𝕆_{η} for x ⟶^{β} y ∈ H. Moreover, by Lemma 3.5, χ(y) ≡ ⟨ϵ⟩χ(y). Hence ⟨β⟩χ(y) ≡ ⟨β⟩⟨ϵ⟩χ(y) ∈ 𝕆_{rη}^{≡}. Also ¬⟨γ⟩⊤ ≡ ¬⟨γ⟩⟨ϵ⟩⊤ ∈ 𝕆_{rη}^{≡}. Hence, ψ(x) ∈ 𝕆_{rη}.

• φ ∈ 𝕆_{η}. If the occurrence of x in t is Λ-liquid, then ψ(x) ∈ 𝕆_{rη}^{≡} follows from Prop. 3.6. So we can assume that this occurrence is Λ-frozen. The cases φ = ⋀_{i∈I} φ_{i} and φ = ¬φ′ proceed as before. We focus on the other two cases.

∗ φ = ⟨ϵ⟩φ′ with φ′ ∈ 𝕆_{η} ⊆ 𝕆_{rη}. Since the occurrence of x in t is Λ-frozen, by Def. 2.16.iv, ψ(x) = χ(x) for some χ ∈ t^{−1}(φ′). By induction on formula size, χ(x) ∈ 𝕆_{rη}. So ψ(x) ∈ 𝕆_{rη}.

∗ φ = ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{η} ⊆ 𝕆_{rη}. Since the occurrence of x in t is Λ-frozen, by Def. 2.16.iv, ψ(x) = χ(x) for some χ ∈ t^{−1}(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}). By Def. 2.16.i, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨a⟩⟨ϵ⟩φ_{2}). By induction on formula size, χ_{1}(x), χ_{2}(x) ∈ 𝕆_{rη}. Hence, ψ(x) ∈ 𝕆_{rη}. □

3.3 Congruence results

Finally we are in a position to prove the promised congruence results.

Lemma 3.8 Given a complete abstraction-free TSS in η-bisimulation format. If σ(x)\underline{↔}_{η} σ′(x) for x ∈ var(t), then σ(t)\underline{↔}_{η} σ′(t).

Proof. By Thm. 2.5, σ(x) \underline{↔}_{η} σ′(x) implies σ(x) ∼_{𝕆_{η}^{≡}} σ′(x) for x ∈ var(t). Let σ(t) ⊧ φ ∈ 𝕆_{η}. By Thm. 2.17 there is a ψ ∈ t^{−1}(φ) with σ(x) ⊧ ψ(x) for x ∈ var(t). Since Λ is universal, by Prop. 3.6, ψ(x) ∈ 𝕆_{η}^{≡} for x ∈ var(t). Since σ(x) ∼_{𝕆_{η}^{≡}} σ′(x), σ′(x) ⊧ ψ(x) for x ∈ var(t). By Thm. 2.17, σ′(t) ⊧ φ. Likewise, σ′(t) ⊧ φ ∈ 𝕆_{η} implies σ(t) ⊧ φ. So σ(t) ∼_{𝕆_{η}} σ′(t). Hence, σ(t)\underline{↔}_{η} σ′(t). □

Theorem 3.9 Given a complete TSS P = (Σ, R) in η-bisimulation format. If σ(x)\underline{↔}_{η} σ′(x) for x ∈ var(t), then σ(t)\underline{↔}_{η} σ′(t).

Proof. Let P′ be obtained from P, by changing in all rules expect ℵ-patience rules a conclusion of the form t ⟶^{τ} u into t ⟶^{i} u, for a fresh action i ∉ A ∪ {τ}. By construction, P′ is abstraction-free and in η-bisimulation format. So by Lemma 3.8, \underline{↔}_{η} is a congruence for all operators of P′.

Let P′′ be obtained from P′ by adding a new operator τ_{i} with rules

\frac{x ⟶^{α} y}{τ_{i}(x) ⟶^{α} τ_{i}(y)} (α ≠ i) \frac{x ⟶^{i} y}{τ_{i}(x) ⟶^{τ} τ_{i}(y)}

This operator turns all i-labels into τ-labels. It is well-known [1] and trivial to check that \underline{↔}_{η} is a congruence for τ_{i} as well.

If follows trivially that for any operator f ∈ Σ the behaviour of τ_{i} ∘ f in P′′ is the same as the behaviour of f in P. So as \underline{↔}_{η} is a congruence for τ_{i} ∘ f in P′′, it must be a congruence for f in P. □

Lemma 3.10 Given a complete abstraction-free TSS in rooted η-bisimulation format. If σ(x)\underline{↔}_{rη} σ′(x) for x ∈ var(t), then σ(t)\underline{↔}_{rη} σ′(t).

Theorem 3.11 Given a complete TSS in rooted η-bisimulation format. If σ(x)\underline{↔}_{rη} σ′(x) for x ∈ var(t), then σ(t)\underline{↔}_{rη} σ′(t).

The proof of Lemma 3.10 is similar to the one of Lemma 3.8, except that Prop. 3.7 is applied instead of Prop. 3.6. Likewise, the proof of Thm. 3.11 is similar to the one of Thm. 3.9.

4 Related work

The only other formats for η- and rooted η-bisimulation that we are aware of appeared in [11]. Those formats are contained in the GSOS format [4]. The formats of [11] distinguish so-called “principal” operators and “abbreviations”. The latter can be regarded as syntactic sugar, adding nothing that could not be expressed with principal operators. Our formats are incomparable with the ones of [11]. However, our formats generalise the result of simplifying the formats of [11] by requiring all operators to be principal.

For the η-bisimulation format our generalisation consists in allowing transition rules outside the GSOS format; the simplified format of [11] is exactly the intersection of our η-bisimulation format and the GSOS format. However, the intersection of our rooted η-bisimulation format and the GSOS format is still a proper generalisation of the simplified format for rooted η-bisimulation of [11]. The latter can be described as the intersection of our rooted η-bisimulation format and the GSOS format in which all arguments of all operators that occur in the right-hand sides of conclusions of transition rules, are required to be Λ-liquid.

The format of [11] for rooted η-bisimulation, following [2], distinguishes “tame” and “wild” function symbols. In terms of our approach, wild operators have only Λ-frozen arguments, and tame operators only Λ-liquid arguments. The idea to allow operators with both kinds of arguments stems from [5].

References

[1] J. Baeten and R. van Glabbeek. Another look at abstraction in process algebra. In Proc. ICALP’87, LNCS 267, pp. 84–94. Springer 1987

[2] B. Bloom. Structural operational semantics for weak bisimulations. Theoretical Computer Science, 146(1/2):25–68, 1995.

[3] B. Bloom, W. Fokkink, and R. van Glabbeek. Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic, 5(1):26–78, 2004.

[4] B. Bloom, S. Istrail, and A. Meyer. Bisimulation can’t be traced. Journal of the ACM, 42(1):232–268, 1995.

[5] W. Fokkink. Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences, 60(1):13–37, 2000.

[6] W. Fokkink and R. van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Information and Computation, 126(1):1–10, 1996.

[7] W. Fokkink, R. van Glabbeek, and P. de Wind. Compositionality of Hennessy-Milner logic by structural operational semantics. Extended abstract appeared in: Proc. FCT’03, LNCS 2751, pp. 412–422. Springer, 2003.

[8] R. van Glabbeek. The linear time-branching time spectrum II: The semantics of sequential systems with silent moves. In Proc. CONCUR’93, LNCS 715, pp. 66–81. Springer, 1993.

[9] R. van Glabbeek. 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, pp. 3–99. Elsevier, 2001.

[10] R. van Glabbeek. The meaning of negative premises in transition system specifications II. Journal of Logic and Algebraic Programming, 60/61:229–258, 2004.

[11] R. van Glabbeek. On cool congruence formats for weak bisimulations.

http://theory.stanford.edu/~rvg/abstracts.html#58.

[12] J.F. Groote. Transition system specifications with negative premises. Theoretical Computer Science, 118(2):263–299, 1993.

[13] J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202–260, 1992.

[14] M. Hennessy and R. Milner. Algebraic laws for non-determinism and concurrency. Journal of the ACM, 32(1):137–161, 1985.

[15] K.G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. Journal of Logic and Computation, 1(6):761–795, 1991.

[16] G. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60/61:17–139, 2004. Originally appeared in 1981.

[17] R. de Simone. Higher-level synchronising devices in Meije–SCCS. Theoretical Computer Science, 37(3):245–267, 1985.

A Modal Characterisation of η-Bisimulation

We prove the first part of Thm. 2.5, which states that 𝕆_{η} is a modal characterisation of η-bisimulation equivalence. We need to prove, given an LTS (ℙ, →), that p\underline{↔}_{η} q ⇔ p ∼_{𝕆_{η}} q for all p, q ∈ ℙ.

Proof. (⇒) Suppose p \underline{↔}_{η} q, and p ⊧ φ for some φ ∈ 𝕆_{η}. We prove q ⊧ φ, by structural induction on φ. The reverse implication follows by symmetry.

• φ = ⋀_{i∈I} φ_{i}. Then p ⊧ φ_{i} for i ∈ I. By induction q ⊧ φ_{i} for i ∈ I, so q ⊧ ⋀_{i∈I} φ_{i}.

• φ = ¬φ′. Then p |̸= φ′. By induction q |̸= φ′, so q ⊧ ¬φ′.

• φ = ⟨ϵ⟩φ. Then for some n there are p_{0}, …, p_{n} ∈ ℙ with p_{n} = p, p_{i+1} ⟶^{τ} p_{i}

for i ∈ {0, …, n − 1}, and p_{0} ⊧ φ. We apply induction on n. n = 0 p ⊧ φ, so by induction on formula size, q ⊧ φ. Hence q ⊧ ⟨ϵ⟩φ. n > 0 Since p_{n} ⟶^{τ} p_{n−1}, according to Def. 2.1 there are two possibilities.

(i) Either p_{n−1} \underline{↔}_{η} q. Since p_{n−1} ⊧ ⟨ϵ⟩φ, by induction on n, q ⊧ ⟨ϵ⟩φ.

(ii) Or q ⟹^{ϵ} q′ ⟶^{τ} q′′ ⟹^{ϵ} q′′′ with p_{n−1} \underline{↔}_{η} q′′′. Since p_{n−1} ⊧ ⟨ϵ⟩φ, by

induction on n, q′′′ ⊧ ⟨ϵ⟩φ. Hence q ⊧ ⟨ϵ⟩φ.

• φ = ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}). Then for some n there are p_{0}, …, p_{n} ∈ ℙ with p_{n} = p,

p_{i+1} ⟶^{τ} p_{i} for i ∈ {0, …, n − 1}, and p_{0} ⊧ φ_{1}⟨a⟩⟨ϵ⟩φ_{2}. We apply induction

on n. n = 0 Then p ⊧ φ_{1}, and there is a p′ ∈ ℙ with p ⟶^{a} p′ and p′ ⊧ ⟨ϵ⟩φ_{2}. By

Def. 2.1, q ⟹^{ϵ} q′ ⟶^{a} q′′ ⟹^{ϵ} q′′′ with p\underline{↔}_{η} q′ and p′ \underline{↔}_{η} q′′′. By induction

on formula size, q′ ⊧ φ_{1} and q′′′ ⊧ ⟨ϵ⟩φ_{2}. Hence q ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}). n > 0 Since p_{n} ⟶^{τ} p_{n−1}, according to Def. 2.1 there are two possibilities.

(i) Either p_{n−1} \underline{↔}_{η} q. Since p_{n−1} ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}), by induction on n, q ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}).

(ii) Or q ⟹^{ϵ} q′ ⟶^{τ} q′′ ⟹^{ϵ} q′′′ with p_{n−1} \underline{↔}_{η} q′′′. By induction on n, p_{n−1} ⊧

⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}), so q′′′ ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}). Hence q ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩⟨ϵ⟩φ_{2}). We conclude that p ∼_{𝕆_{η}} q.

(⇐) We prove that ∼_{𝕆_{η}} is an η-bisimulation relation. The relation is clearly symmetric. Let p ∼_{𝕆_{η}} q. Suppose p ⟶^{α} p′. If α = τ and p′ ∼_{𝕆_{η}} q, then the first condition of Def. 2.1 is fulfilled. So we can assume that either (i) α ≠ τ or (ii) p′ ≁_{𝕆_{η}} q. We define

\begin{aligned}Q′ & = & \{q′ ∈ ℙ | q ⟹^{ϵ} q′ ∧ p ≁_{𝕆_{η}} q′\} \\ Q′′′ & = & \{q′′′ ∈ ℙ | ∃q′, q′′ ∈ ℙ : q ⟹^{ϵ} q′ ⟶^{α} q′′ ⟹^{ϵ} q′′′ ∧ p′ ≁_{𝕆_{η}} q′′′\} \end{aligned}

For each q′ ∈ Q′, let φ_{q′} be a formula in 𝕆_{η} such that p ⊧ φ_{q′} and q′ |̸= φ_{q′}. (Such a formula always exists because 𝕆_{η} is closed under negation ¬.) We define

φ = ⋀_{q′∈Q′} φ_{q′}

Similarly, for each q′′′ ∈ Q′′′, let ψ_{q′′′} be a formula in 𝕆_{η} such that p′ ⊧ ψ_{q′′′} and q′′′ |̸= ψ_{q′′′}. We define

ψ = ⋀_{q′′′∈Q′′′} ψ_{q′′′}

Clearly, φ, ψ ∈ 𝕆_{η}, p ⊧ φ and p′ ⊧ ψ. We distinguish two cases.

(i) α ≠ τ. Since p ⊧ ⟨ϵ⟩(φ⟨α⟩⟨ϵ⟩ψ) ∈𝕆_{η} and p∼_{𝕆_{η}} q, also q ⊧ ⟨ϵ⟩(φ⟨α⟩⟨ϵ⟩ψ). Hence, q ⟹^{ϵ} q′ ⟶^{α} q′′ ⟹^{ϵ} q′′′ with q′ ⊧ φ and q′′′ ⊧ ψ. By the definition of φ and ψ it follows that p ∼_{𝕆_{η}} q′ and p′ ∼_{𝕆_{η}} q′′′.

(ii) α = τ and p′ ≁_{𝕆_{η}} q. Let φ̂ ∈ 𝕆_{η} such that p′ ⊧ φ̂ and q |̸= φ̂. Since p ⊧ ⟨ϵ⟩(φ̂ ∧ ψ) ∈ 𝕆_{η} and p ∼_{𝕆_{η}} q, also q ⊧ ⟨ϵ⟩(φ̂ ∧ ψ). Since q |̸= φ̂, q ⟶^{τ} q′′ ⟹^{ϵ} q′′′ with q′′′ ⊧ φ̂ ∧ ψ. By the definition of ψ it follows that p′ ∼_{𝕆_{η}} q′′′.

Both cases imply that the second condition of Def. 2.1 is fulfilled. We therefore conclude that ∼_{𝕆_{η}} is an η-bisimulation relation. □

Using the first part of Thm. 2.5, which was proved above, it is not hard to derive the second part of Thm. 2.5, i.e. that 𝕆_{rη} is a modal characterisation of rooted η-bisimulation equivalence.