Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation

Wan Fokkink^{1,2}, Rob van Glabbeek^{3,4}, and Paulien de Wind^{1}

1 Vrije Universiteit Amsterdam, Section Theoretical Computer Science, Amsterdam

2 CWI, Department of Software Engineering, Amsterdam 3 National ICT Australia, Sydney

4 University of New South Wales, School of Computer Science and Engineering,

Sydney

               {wanf,pdwind}@cs.vu.nl, rvg@cs.stanford.edu

Abstract. We present a method for decomposing modal formulas for processes with the internal action τ. 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. We use this decomposition method to derive congruence formats for branching and rooted branching bisimulation equivalence.

1 Introduction

Structural operational semantics [20] 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.

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

In general a behavioural 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 behavioural 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 [21], the GSOS format [4], the tyft/tyxt format [16], and the ntyft/ntyxt format [15]. 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.

Behavioural equivalences can be characterised 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 [17] is a modal characterisation of bisimulation.

Larsen and Liu [19] 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 [9] to tyft/tyxt format. In [3], the decomposition method was applied to obtain congruence formats for a range of behavioural equivalences. 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.

Here we extend the work of [3] to processes with τ-transitions. We present a method for decomposing formulas from modal logic for processes with τtransitions. In order to minimise the complexity inherent in the combination of modal decomposition and the internal action τ, we apply the decomposition method to so-called abstraction-free TSSs, where only the patience rules contain the label τ in the conclusion. Furthermore, we use this decomposition method to obtain congruence formats for branching and rooted branching bisimulation. These formats include TSSs that are not abstraction-free, owing to the compositionality of the abstraction operator, which renames certain actions into τ. Our formats use two predicates on arguments of function symbols, to mark both running processes and processes that may have started running. Our congruence formats are more liberal than the simply BB and RBB cool formats from [2] and the RBB safe format from [7]. In Sect. 7 we will present a more in-depth comparison with congruence formats from [2, 7, 13].

In a companion paper [10], we derive congruence formats for η- and rooted η-bisimulation, with a reference to the current paper for the decomposition method. 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 behavioural equivalences.

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. Furthermore, ⟹^{ϵ} denotes the transitive-reflexive closure of ⟶^{τ}.

Definition 1 ([14]). A symmetric relation B ⊆ ℙ×ℙ is a branching bisimulation if pBq and p ⟶^{α} p′ implies that either α = τ and p′ B q, or q ⟹^{ϵ} q′ ⟶^{α} q′′ for some q′ and q′′ with pBq′ and p′Bq′′.

Processes p, q are branching bisimilar, denoted by p \underline{↔}_{b} q, if there exists a branching bisimulation B with pBq.

Branching 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 ([14]). A symmetric relation R ⊆ ℙ × ℙ is a rooted branching bisimulation if pRq and p ⟶^{α} p′ implies that q ⟶^{α} q′ for some q′ with p′ \underline{↔}_{b} q′.

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

2.2 Modal logic

Modal logic aims to formulate properties of processes in an LTS. Following [11], we extend Hennessy-Milner logic [17] with the modal connectives ⟨ϵ⟩φ and ⟨τ̂⟩φ.

Definition 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′ ⊧ φ,

p ⊧ ⟨ϵ⟩φ if p ⟹^{ϵ} p′ with p′ ⊧ φ, and p ⊧ ⟨τ̂⟩φ if either p ⊧ φ or p ⟶^{τ} p′

with p′ ⊧ φ. We use abbreviations ⊤ for the empty conjunction, φ_{1} ∧ φ_{2} for ⋀_{i∈{1,2}} φ_{i}, φ⟨α⟩φ′ for φ ∧ ⟨α⟩φ′, and φ⟨τ̂⟩φ′ for φ ∧ ⟨τ̂⟩φ′. We write φ ≡ φ′ if p ⊧ φ ⇔ p ⊧ φ′ for any process p in any LTS.

Definition 4. The subclasses 𝕆_{b} and 𝕆_{rb} of 𝕆 are defined as follows:

𝕆_{b}  φ ::= ⋀_{i∈I}φ_{i} | ¬φ | ⟨ϵ⟩(φ⟨τ̂⟩φ′) | ⟨ϵ⟩(φ⟨a⟩φ′)
𝕆_{rb}  φ ::= ⋀_{i∈I}φ_{i} | ¬φ | ⟨α⟩φ̂ | φ̂ (φ̂ ∈ 𝕆_{b})

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

The last clause in the definition of 𝕆_{rb} guarantees that 𝕆_{b} ⊆ 𝕆_{rb}, which will be needed in the proof of Prop. 4. If this clause were omitted, it would still follow that 𝕆_{b}^{≡} ⊆ 𝕆_{rb}^{≡}, using structural induction together with ⟨ϵ⟩φ ≡ φ ∨ ⟨τ⟩⟨ϵ⟩φ and ⟨τ̂⟩φ ≡ φ ∨ ⟨τ⟩φ. Note that if φ ∈ 𝕆_{b}^{≡}, then ⟨ϵ⟩φ ≡ ⟨ϵ⟩(φ⟨τ̂⟩φ) ∈ 𝕆_{b}^{≡}.

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

Theorem 1. p \underline{↔}_{b} q ⇔ p ∼_{𝕆_{b}} q and p \underline{↔}_{rb} q ⇔ p ∼_{𝕆_{rb}} 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 5. 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), written (Σ, R), consists of a signature Σ and a collection R of transition rules over Σ.

Definition 6. 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. 4.1 (see Prop. 2).

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 [12] 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 7. 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:

1. either ν is positive and \frac{K}{ν} is a closed substitution instance of a rule in R;

2. 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, 15, 16].

Definition 8. 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 9. 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 [15, 3] were originally introduced to guarantee congruence for bisimulation and ready simulation.

Definition 10. 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 11. 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 (or ℵ-liquid for short), 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; otherwise the occurrence is at an ℵ-frozen position.

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, 7]). We will require the presence of patience rules for ℵ-liquid arguments.

Definition 12. An ntyft rule is a patience rule for 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 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 13. A TSS is abstraction-free with respect to ℵ if only ℵ-patience rules have a conclusion of the form t ⟶^{τ} u.

In Section 4.2 we will obtain preservation results of modal formulas in 𝕆_{b} and 𝕆_{rb} on abstraction-free TSSs. We will lift these to congruence results for \underline{↔}_{b} and \underline{↔}_{rb} on general TSSs, using two facts: abstraction operators preserve \underline{↔}_{b} and \underline{↔}_{rb}, and each TSS can be embedded in an abstraction-free TSS augmented with an abstraction operator.

2.5 Ruloids

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 [16], 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 [8], 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. 7, we want a more constructive notion like Def. 6, 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^{+}. The notion of irredundant provability is adapted in a straightforward fashion to accommodate rules with a negative conclusion. In [3] it is established that P ⊢_{ws} μ if and only if μ is irredundantly provable from P^{+}, for all closed literals μ. P - ruloids are those 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 1 ([3]). 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.

It is not hard to see that the notion of abstraction-freeness is preserved by the transformation to P -ruloids.

Lemma 1. If a TSS P is abstraction-free with respect to some ℵ, then all P - ruloids with a conclusion of the form t ⟶^{τ} u are ℵ-patient.

3 Decomposition of Modal Formulas

In this section we 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.

In order to minimise the complexity inherent in the combination of modal decomposition and the internal action τ, we apply the decomposition method to abstraction-free TSSs. In Sect. 4, where we will develop congruence formats on the basis of this decomposition method, we will be able to circumvent the restriction to abstraction-free TSSs, owing to the compositionality of the abstraction operator.

Definition 14. Let P be a TSS in ready simulation format, which contains the ℵ-patience rules and is abstraction-free with respect to ℵ. We define ·^{−1} : 𝕋(Σ) × 𝕆 → 𝒫(V → 𝕆) as follows. Let t denote a univariate term, i.e. without multiple occurrences of the same variable.

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

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

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

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

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

3. ψ ∈ 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}

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

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

5. ψ ∈ t^{−1}(⟨τ̂⟩φ) iff one of the following holds:

(a) ψ ∈ t^{−1}(φ), or

(b) there is an x_{0} ∈ V that occurs ℵ-liquid in t and a χ ∈ t^{−1}(φ) such that

ψ(x) = \{ \begin{matrix}⟨τ̂⟩χ(x) & if x = x_{0} \\ χ(x) & if x ≠ x_{0} \end{matrix}

6. ψ ∈ ρ(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. 14, we expand on two of its cases. 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).

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. 1, 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.

The following theorem will be the key to the forthcoming congruence results.

Theorem 2. Given a complete TSS P in ready simulation format, which contains the ℵ-patience rules and is abstraction-free with respect to ℵ. For any term t, closed substitution σ and φ ∈ 𝕆:

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

Proof. By structural induction on φ. First we treat the case where t is univariate.

– φ = ⋀_{i∈I} φ_{i} σ(t) ⊧ ⋀_{i∈I} φ_{i} ⇔ ∀i ∈ I : σ(t) ⊧ φ_{i} ⇔ ∀i ∈ I ∃ψ_{i} ∈ t^{−1}(φ_{i}) ∀x ∈ var(t) : σ(x) ⊧ ψ_{i}(x) ⇔ ∃ψ ∈ t^{−1}(⋀_{i∈I} φ_{i}) ∀x ∈ var(t) : σ(x) ⊧ ψ(x).

– φ = ¬φ′ σ(t) ⊧ ¬φ′ ⇔ σ(t) |̸= φ′ ⇔ ∃h : t^{−1}(φ′) → var(t) ∀χ ∈ t^{−1}(φ′) : σ(h(χ)) |̸= χ(h(χ)) ⇔ ∃h : t^{−1}(φ′) → var(t) ∀x ∈ var(t) : σ(x) ⊧ ⋀_{χ∈h^{−1}(x)} ¬χ(x) ⇔ ∃ψ ∈ t^{−1}(¬φ′) ∀x ∈ var(t) : σ(x) ⊧ ψ(x).

– φ = ⟨α⟩φ′ (⇒) Let σ(t) ⊧ ⟨α⟩φ′. Then P ⊢_{ws} σ(t) ⟶^{α} p with p ⊧ φ′. By Prop. 1 there is a P -ruloid \frac{H}{t⟶^{α}u} and a σ′ with P ⊢_{ws} σ′(μ) for μ ∈ H, σ′(t) = σ(t), i.e. σ′(x) = σ(x) for x ∈ var(t), and σ′(u) = p. Since σ′(u) ⊧ φ′, by induction there is a χ ∈ u^{−1}(φ′) with σ′(z) ⊧ χ(z) for z ∈ var(u). Furthermore, σ′(z) ⊧ χ(z) ≡ ⊤ for z ∉ var(u). Define ψ ∈ t^{−1}(⟨α⟩φ′) as in Def. 14.3, using

\frac{H}{t⟶^{α}u} and χ. Let x ∈ var(t). For x ⟶^{β} y ∈ H, P ⊢_{ws} σ′(x) ⟶^{β} σ′(y) ⊧ χ(y),

so σ′(x) ⊧ ⟨β⟩χ(y). Moreover, for x −̸→^{γ} ∈ H, P ⊢_{ws} σ′(x) −̸→^{γ}, so the consistency of ⊢_{ws} (see [12]) yields P ⊬_{ws} σ′(x) ⟶^{γ} q for all closed terms q, and thus σ′(x) ⊧ ¬⟨γ⟩⊤. Hence σ(x) = σ′(x) ⊧ ψ(x).

(⇐) Let ψ ∈ t^{−1}(⟨α⟩φ′) with σ(x) ⊧ ψ(x) for x ∈ var(t). There is a P -ruloid

\frac{\{x ⟶^{β_{i}} y_{i} | i ∈ I_{x}, x ∈ var(t)\} ∪ \{x −̸→^{γ_{j}}| j ∈ J_{x}, x ∈ var(t)\}}{t ⟶^{α} u}

and a χ ∈ u^{−1}(φ′) with ψ(x) = χ(x)∧⋀_{i∈I_{x}}⟨β_{i}⟩χ(y_{i})∧⋀_{j∈J_{x}} ¬⟨γ_{j}⟩⊤ for x ∈ var(t). For x ∈ var(t), σ(x) ⊧ ψ(x) yields, for i ∈ I_{x}, P ⊢_{ws} σ(x) ⟶^{β_{i}} p_{i} with p_{i} ⊧ χ(y_{i}) for some closed term p_{i}; moreover, for j ∈ J_{x}, P ⊬_{ws} σ(x) ⟶^{γ_{j}} q for all closed terms q, so by the completeness of P, P ⊢_{ws} σ(x) −̸→^{γ_{j}}. Define σ′(x) = σ(x) and σ′(y_{i}) = p_{i} for x ∈ var(t) and i ∈ I_{x}. Here we use that the y_{i} are all different and do not occur in t. Then σ′(z) ⊧ χ(z) for z ∈ var(u), since var(u) ⊆ {x, y_{i} | x ∈ var(t), i ∈ I_{x}}. So by induction, σ′(u) ⊧ φ′. Moreover, for x ∈ var(t), P ⊢_{ws} σ′(x) ⟶^{β_{i}} σ′(y_{i}) for i ∈ I_{x}, and P ⊢_{ws} σ′(x) −̸→^{γ_{j}} for j ∈ J_{x}, so by Prop. 1, P ⊢_{ws} σ′(t) ⟶^{α} σ′(u). Hence σ(t) = σ′(t) ⊧ ⟨α⟩φ′.

– φ = ⟨ϵ⟩φ′ (⇒) We prove by induction on n: if P ⊢_{ws} p_{i} ⟶^{τ} p_{i+1} for i ∈ {0, …, n − 1} with σ(t) = p_{0} and p_{n} ⊧ φ′, then there is a ψ ∈ t^{−1}(⟨ϵ⟩φ′) with σ(x) ⊧ ψ(x) for x ∈ var(t). n = 0 Since σ(t) = p_{0} ⊧ φ′, by induction on formula size, there is a χ ∈

t^{−1}(φ′) with σ(x) ⊧ χ(x) for x ∈ var(t). Define ψ ∈ t^{−1}(⟨ϵ⟩φ′) as in Def. 14.4, using χ. Then σ(x) ⊧ ψ(x) for x ∈ var(t).

n > 0 Since P ⊢_{ws} σ(t) ⟶^{τ} p_{1}, by Prop. 1 there is a P -ruloid \frac{H}{t⟶^{τ}u} and a σ′ with P ⊢_{ws} σ′(μ) for μ ∈ H, σ′(t) = σ(t), i.e. σ′(x) = σ(x) for

x ∈ var(t), and σ′(u) = p_{1}. Since σ′(u) = p_{1} ⟶^{τ} ⋯ ⟶^{τ} p_{n} ⊧ ⟨ϵ⟩φ′,

by induction on n, there is a χ ∈ u^{−1}(⟨ϵ⟩φ′) with σ′(y) ⊧ χ(y) for y ∈ var(u). Furthermore, σ′(y) ⊧ χ(y) ≡ ⊤ for y ∉ var(u). Since P is abstraction-free, by Lem. 1, the P -ruloid \frac{H}{t⟶^{τ}u} must be ℵ-patient. Thus H = {x_{0} ⟶^{τ} y_{0}}, where x_{0} occurs ℵ-liquid in t and, since t is univariate, u = t[y_{0}/x_{0}]. Moreover, y_{0} ∉ var(t), so u is also univariate. The occurrence of y_{0} in u is ℵ-liquid, so according to Def. 14.4, χ(y_{0}) is of the form ⟨ϵ⟩φ′′. Let ψ(x_{0}) = χ(y_{0}), ψ(y_{0}) = χ(x_{0}) ≡ ⊤, and ψ(z) = χ(z) otherwise. By alpha-conversion, χ ∈ u^{−1}(⟨ϵ⟩φ′) implies ψ ∈ t^{−1}(⟨ϵ⟩φ′). For x ∈ var(t)\{x_{0}}, σ(x) = σ′(x) ⊧ χ(x) = ψ(x). Furthermore, P ⊢_{ws} σ′(x_{0}) ⟶^{τ} σ′(y_{0}) and σ′(y_{0}) ⊧ χ(y_{0}) = ψ(x_{0}); so since ψ(x_{0}) is of the form ⟨ϵ⟩φ′′, σ(x_{0}) = σ′(x_{0}) ⊧ ψ(x_{0}).

(⇐) Let ψ ∈ t^{−1}(⟨ϵ⟩φ′) with σ(x) ⊧ ψ(x) for x ∈ var(t). Then there is a χ ∈ t^{−1}(φ′) with ψ(x) = ⟨ϵ⟩χ(x) if x occurs ℵ-liquid in t and ψ(x) = χ(x) otherwise. For each x that occurs ℵ-liquid in t, σ(x) ⊧ ψ(x) = ⟨ϵ⟩χ(x), i.e. σ(x) ⟹^{ϵ} p_{x} with p_{x} ⊧ χ(x). Define σ′(x) = p_{x} if x occurs ℵ-liquid in t and σ′(x) = σ(x) otherwise. Due to the presence of the ℵ-patience rules and the fact that t is univariate, σ(t) ⟹^{ϵ} σ′(t). Furthermore, σ′(x) ⊧ χ(x) for x ∈ var(t), so by induction on formula size, σ′(t) ⊧ φ′. Hence σ(t) ⊧ ⟨ϵ⟩φ′.

– φ = ⟨τ̂⟩φ′ (⇒) Suppose σ(t) ⊧ ⟨τ̂⟩φ′. Then either σ(t) ⊧ φ′ or P ⊢_{ws} σ(t) ⟶^{τ} p ⊧ φ′ for some closed term p. In the first case, by induction there is a ψ ∈ t^{−1}(φ′) such that σ(x) ⊧ ψ(x) for x ∈ var(t); by Def. 14.5(a), ψ ∈ t^{−1}(⟨τ̂⟩φ′), and we are done. In the second case, by Prop. 1 there is a P -ruloid \frac{H}{t⟶^{τ}u} and a closed substitution σ′ with P ⊢_{ws} σ′(μ) for μ ∈ H, σ′(t) = σ(t), i.e. σ′(x) = σ(x) for x ∈ var(t), and σ′(u) = p. Since σ′(u) ⊧ φ′, by induction there is a χ ∈ u^{−1}(φ′) such that σ′(y) ⊧ χ(y) for y ∈ var(u). Furthermore, σ′(y) ⊧ χ(y) ≡ ⊤ for y ∉ var(u). Since P is abstraction-free, by Lem. 1, the P -ruloid \frac{H}{t⟶^{τ}u} must be ℵ-patient. Thus H = \{x_{0} ⟶^{τ} y_{0}\}, where x_{0} occurs ℵ-liquid in t and, since t is univariate, u = t[y_{0}/x_{0}]. Moreover, y_{0} ∉ var(t), so u is also univariate. Let ψ(x_{0}) = ⟨τ̂⟩χ(y_{0}), ψ(y_{0}) = χ(x_{0}) ≡ ⊤, and ψ(x) = χ(x) otherwise. By Def. 14.5(b) together with alpha-conversion, ψ ∈ t^{−1}(⟨τ̂⟩φ′). For x ∈ var(t)\{x_{0}}, σ(x) = σ′(x) ⊧ χ(x) = ψ(x). Moreover, since P ⊢_{ws} σ′(x_{0}) ⟶^{τ} σ′(y_{0}) and σ′(y_{0}) ⊧ χ(y_{0}), it follows that σ(x_{0}) = σ′(x_{0}) ⊧ ⟨τ̂⟩χ(y_{0}) = ψ(x_{0}).

(⇐) Suppose ψ ∈ t^{−1}(⟨τ̂⟩φ′) with σ(x) ⊧ ψ(x) for all x ∈ var(t). If ψ ∈ t^{−1}(φ′), then by induction σ(t) ⊧ φ′, so σ(t) ⊧ ⟨τ̂⟩φ′, and we are done. Suppose that for some χ ∈ t^{−1}(φ′) and some x_{0} that occurs ℵ-liquid in t, ψ(x) = χ(x) for x ≠ x_{0} and ψ(x_{0}) = ⟨τ̂⟩χ(x_{0}). Then σ(x) ⊧ χ(x) for x ∈ var(t)\{x_{0}}. Furthermore, σ(x_{0}) ⊧ ψ(x_{0}) = ⟨τ̂⟩χ(x_{0}), so either σ(x_{0}) ⊧ χ(x_{0}) or σ(x_{0}) ⟶^{τ} p ⊧ χ(x_{0}) for some closed term p. In the first case, by induction σ(t) ⊧ φ′, so σ(t) ⊧ ⟨τ̂⟩φ′, and we are done. In the second case, define σ′(x) = σ(x) for x ∈ var(t) and σ′(y_{0}) = p. Since P ⊢_{ws} σ′(x_{0}) ⟶^{τ} σ′(y_{0}), and \frac{x_{0}⟶^{τ}y_{0}}{t⟶^{τ}t[y_{0}/x_{0}]} is an ℵ-patient P -ruloid, by Prop. 1,

P ⊢_{ws} σ′(t) ⟶^{τ} σ′(t[y_{0}/x_{0}]). Furthermore, by induction σ′(t[y_{0}/x_{0}]) ⊧ φ′. Hence σ(t) = σ′(t) ⊧ ⟨τ̂⟩φ′.

Finally, suppose t is not univariate. Let t = ρ(u) for some univariate u and ρ : var(u) → V not injective. σ(ρ(u)) ⊧ φ ⇔ ∃χ ∈ u^{−1}(φ) ∀y ∈ var(u) : σ(ρ(y)) ⊧ χ(y) ⇔ ∃χ ∈ u^{−1}(φ) ∀x ∈ var(t) : σ(x) ⊧ ⋀_{y∈ρ^{−1}(x)} χ(y) ⇔ ∃ψ ∈ t^{−1}(φ) ∀x ∈ var(t) : σ(x) ⊧ ψ(x). ⊓ ⊔

The part of Thm. 2 that deals with the modalities ⋀_{i∈I}, ¬ and ⟨α⟩ only has been established in [9]. There, a few examples are given showing how Def. 14 can be used to decompose a modal formula, as well as a counterexample showing that the completeness requirement in Thm. 2 cannot simply be skipped. The inclusion of the modalities ⟨ϵ⟩ and ⟨τ̂⟩ is new. The following example illustrates the use of the decomposition method on a formula with the modality ⟨ϵ⟩.

Example 1. Let A = {a} and P = (Σ, R), where Σ consists of a binary function symbol ∥ with liquid arguments, and R contains the rules \frac{x⟶^{α}x′}{x∥y⟶^{α}x′∥y} and

\frac{y⟶^{α}y′}{x∥y⟶^{α}x∥y′} for α ∈ \{a, τ\}. The TSS P is complete and in ready simulation format. Furthermore, it contains the two patience rules and is abstraction-free.

We compute (x∥y)^{−1}(⟨ϵ⟩⟨a⟩⊤). By Def. 14.4, for each ψ ∈ (x∥y)^{−1}(⟨ϵ⟩⟨a⟩⊤) we have ψ(x) = ⟨ϵ⟩χ(x) and ψ(y) = ⟨ϵ⟩χ(y) for some χ ∈ (x∥y)^{−1}(⟨a⟩⊤). According to Def. 14.3, (x∥y)^{−1}(⟨a⟩⊤) = {χ_{1}, χ_{2}}, where χ_{1} and χ_{2} are constructed from the only P -ruloids with a conclusion x∥y ⟶^{a} , namely \frac{x⟶^{a}x′}{x∥y⟶^{a}x′∥y} and

\frac{y⟶^{a}y′}{x∥y⟶^{a}x∥y′}, together with ξ_{1} ∈ (x′∥y)^{−1}(⊤) resp. ξ_{2} ∈ (x∥y′)^{−1}(⊤):

\begin{matrix}χ_{1}(x) = ξ_{1}(x) ∧ ⟨a⟩ξ_{1}(x′) ≡ ⟨a⟩⊤ & χ_{2}(x) = ⊤ \\ χ_{1}(y) = ⊤ & χ_{2}(y) = ξ_{2}(y) ∧ ⟨a⟩ξ_{2}(y′) ≡ ⟨a⟩⊤ \end{matrix}

Hence (x∥y)^{−1}(⟨ϵ⟩⟨a⟩⊤) = {ψ_{1}, ψ_{2}} with ψ_{1} and ψ_{2} defined as follows:

\begin{matrix}ψ_{1}(x) = ⟨ϵ⟩χ_{1}(x) ≡ ⟨ϵ⟩⟨a⟩⊤ & ψ_{2}(x) = ⟨ϵ⟩χ_{2}(x) = ⟨ϵ⟩⊤ ≡ ⊤ \\ ψ_{1}(y) = ⟨ϵ⟩χ_{1}(y) = ⟨ϵ⟩⊤ ≡ ⊤ & ψ_{2}(y) = ⟨ϵ⟩χ_{2}(y) ≡ ⟨ϵ⟩⟨a⟩⊤ \end{matrix}

4 Branching Bisimulation as a Congruence

We proceed to apply the decomposition method from the previous section to derive congruence formats for branching and rooted branching bisimulation equivalence. The idea is that the branching bisimulation format must guarantee that a formula from 𝕆_{b} is always decomposed into formulas from 𝕆_{b}^{≡} (see Prop. 3). Likewise, the rooted branching bisimulation format must guarantee that a formula from 𝕆_{rb} is always decomposed into formulas from 𝕆_{rb}^{≡} (see Prop. 4). This implies the desired congruence results (see Thm. 3 and Thm. 4). In the derivation of the congruence formats, we will circumvent the restriction in the decomposition method to abstraction-free TSSs, using compositionality of the abstraction operator.

4.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 might currently be resting, in which case no patience rules are needed for these arguments. Always ℵ ⊆ Λ.

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

1. it has no lookahead,

2. right-hand sides of premises occur only Λ-liquid in u, and

3. if x occurs exactly once^{5} in t, at a Λ-liquid position, then: (a) all occurrences of x in the rule are Λ-liquid,

(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 ℵ-frozen in t, then x does not occur ℵ-liquid in left-hand sides of premises.

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

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

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

If a TSS P is in rooted branching bisimulation format then there are smallest predicates ℵ_{0} and Λ_{0} such that P consists of the ℵ_{0}-patience rules and rules that are rooted branching bisimulation safe with respect to ℵ_{0} and Λ_{0}. Namely the Λ_{0}-liquid arguments are generated by requirements 2 and 3(a) of Def. 15; they are the smallest collection of arguments such that these two requirements are satisfied. Given Λ_{0}, ℵ_{0} is the unique collection of arguments within Λ_{0} for which patience rules exists. For any TSS P, ℵ_{0} and Λ_{0} can be calculated in this way, and whether P is in rooted branching bisimulation format then depends solely on whether requirements 1 and 3(b–d) of Def. 15 are satisfied.

When restricting to TSSs consisting of nxytt rules only, it becomes easier to reformulate the definition of the rooted branching bisimulation format without mentioning ℵ. Namely, requirements 3(b–d) of Def. 15, together with the existence of the patience rules required in Def. 16 then amount to

3. (b) x does not occur as the left-hand side of a negative premise,

5 For the rooted branching bisimulation format in Def. 16, only the requirements for rules in which t is univariate matter. The formulation of Def. 15 for general terms t paves the way for Prop. 2.

(c) x occurs at most once as the left-hand side of a positive premise, and this premise has a label from A, and

(d) if within t, x occurs in an argument of an operator f for which there is no patience rule, then x does not occur in the left-hand side of premises.

A TSS is now in rooted branching bisimulation format if it consists of patience rules and rules that are rooted branching bisimulation safe with respect to Λ and that collection of patience rules.

Using this, it is not hard to see that the rooted branching bisimulation format strengthens the RBB safe format from [7].

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) branching bisimulation format, then so are the P -ruloids.

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

The proof of Prop. 2 is omitted here. The key part of the proof is to show that the decent (rooted) branching bisimulation format is preserved under irredundant provability. The adjective irredundant is essential here; this preservation result would fail if “junk” could be added to the premises of derived transition rules.

4.2 Preservation of modal characterisations

In this section we prove that given a TSS in rooted branching bisimulation format, if ψ ∈ t^{−1}(φ) with φ ∈ 𝕆_{b}, then ψ(x) ∈ 𝕆_{b}^{≡} if x occurs only Λ-liquid in t. (That is why in the branching bisimulation format, Λ must be universal.) If φ ∈ 𝕆_{rb}, then ψ(x) ∈ 𝕆_{rb}^{≡} for all variables x.

Proposition 3. Let P be an abstraction-free TSS in rooted branching bisimulation format, with respect to some ℵ and Λ. For any term t and variable x that occurs only Λ-liquid in t:

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

Proof. We apply structural induction on φ ∈ 𝕆_{b}. 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) ≡ ⊤ ∈ 𝕆_{b}^{≡}. Suppose x occurs once in t.

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

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

– φ = ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b}. By Def. 14.4, either ψ(x) = ⟨ϵ⟩χ(x) if x occurs ℵ-liquid in t, or ψ(x) = χ(x) if x occurs ℵ-frozen in t, for some χ ∈ t^{−1}(φ_{1}⟨τ̂⟩φ_{2}). By Def. 14.1, χ(x) = χ_{1}(x)∧χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨τ̂⟩φ_{2}). By Def. 14.5, either χ_{2}(x) = ⟨τ̂⟩ξ(x) and x occurs ℵ-liquid in t, or χ_{2}(x) = ξ(x), for some ξ ∈ t^{−1}(φ_{2}). So ψ(x) is of the form ⟨ϵ⟩(χ_{1}(x)⟨τ̂⟩ξ(x)), ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x)) or χ_{1}(x) ∧ ξ(x). By induction, χ_{1}(x), ξ(x) ∈ 𝕆_{b}^{≡}. Hence ψ(x) ∈ 𝕆_{b}^{≡}.

– φ = ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b}. By Def. 14.4, either ψ(x) = ⟨ϵ⟩χ(x) if x occurs ℵ-liquid in t, or ψ(x) = χ(x) if x occurs ℵ-frozen in t, for some χ ∈ t^{−1}(φ_{1}⟨a⟩φ_{2}). By Def. 14.1, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨a⟩φ_{2}). By induction, χ_{1}(x) ∈ 𝕆_{b}^{≡}. By Def. 14.3,

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

for some ξ ∈ u^{−1}(φ_{2}) and P -ruloid \frac{H}{t⟶^{a}u}. Since a ≠ τ, by Prop. 2, \frac{H}{t⟶^{a}u} is rooted branching bisimulation safe with respect to ℵ and Λ. 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 in u. So by induction, ξ(x) ∈ 𝕆_{b}^{≡} and ξ(y) ∈ 𝕆_{b}^{≡} 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 branching bisimulation safe with respect to ℵ and Λ and an nxytt rule, x does not occur in left-hand sides of negative premises in H, and at most once in the left-hand side of one positive premise in H, which is of the form x ⟶^{b} y with b ∈ A. Hence either χ_{2}(x) = ξ(x) or χ_{2}(x) = ξ(x)⟨b⟩ξ(y). Since ψ(x) = ⟨ϵ⟩(χ_{1}(x) ∧ χ_{2}(x)), either ψ(x) = ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x)) ∈ 𝕆_{b}^{≡} or ψ(x) ≡ ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x)⟨b⟩ξ(y)) ∈ 𝕆_{b}^{≡}.

Case 2: The occurrence of x in t is ℵ-frozen. Then ψ(x) = χ(x). Since \frac{H}{t⟶^{a}u} is rooted branching bisimulation safe with respect to ℵ and Λ 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) ∈ 𝕆_{b}^{≡}.

Finally, suppose t is not univariate. Then t = ρ(u) for some univariate term u and ρ : var(u) → V not injective. By Def. 14.6, ψ(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) ∈ 𝕆_{b}^{≡} for y ∈ ρ^{−1}(x). Hence ψ(x) ∈ 𝕆_{b}^{≡}. ⊓ ⊔

Proposition 4. Let P be an abstraction-free TSS in rooted branching bisimulation format, with respect to some ℵ and Λ. For any term t and variable x:

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

Proof. We apply structural induction on φ ∈ 𝕆_{rb}. Let 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. If x ∉ var(t), then ψ(x) ≡ ⊤ ∈ 𝕆_{rb}^{≡}. So suppose x occurs once in t.

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

– φ = ⟨α⟩φ′ with φ′ ∈ 𝕆_{b}. By Def. 14.3,

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

for some χ ∈ u^{−1}(φ′) and P -ruloid \frac{H}{t⟶^{α}u}. By induction, χ(x) ∈ 𝕆_{rb}^{≡}. (Induction may be applied because φ′ ∈ 𝕆_{b} ⊆ 𝕆_{rb}.) By Prop. 2, \frac{H}{t⟶^{α}u} is either rooted branching bisimulation safe with respect to ℵ and Λ or ℵ-patient. In either case, variables in right-hand sides of premises in H occur only Λliquid in u. By Prop. 3, χ(y) ∈ 𝕆_{b}^{≡} for x ⟶^{β} y ∈ H, so ⟨β⟩χ(y) ∈ 𝕆_{rb}^{≡}. Also ¬⟨γ⟩⊤ ∈ 𝕆_{rb}^{≡}. Hence ψ(x) ∈ 𝕆_{rb}^{≡}.

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

∗ φ = ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b} ⊆ 𝕆_{rb}. Since the occurrence of x in t is ℵ-frozen, by Def. 14.4, ψ(x) = χ(x) for some χ ∈ t^{−1}(φ_{1}⟨τ̂⟩φ_{2}). By Def. 14.1, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨τ̂⟩φ_{2}). Since the occurrence of x in t is ℵ-frozen, by Def. 14.5, χ_{2}(x) = ξ(x) for some ξ ∈ t^{−1}(φ_{2}). By induction, χ_{1}(x), ξ(x) ∈ 𝕆_{rb}^{≡}. Hence ψ(x) ∈ 𝕆_{rb}^{≡}.

∗ φ = ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b} ⊆ 𝕆_{rb}. Since the occurrence of x in t is ℵ-frozen, by Def. 14.4, ψ(x) = χ(x) for some χ ∈ t^{−1}(φ_{1}⟨a⟩φ_{2}). By Def. 14.1, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨a⟩φ_{2}). By induction, χ_{1}(x), χ_{2}(x) ∈ 𝕆_{rb}^{≡}. Hence ψ(x) ∈ 𝕆_{rb}^{≡}. ⊓ ⊔

4.3 Congruence results

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

Lemma 2. Given a complete, abstraction-free TSS in branching bisimulation format, with respect to some ℵ. If σ(x) \underline{↔}_{b} σ′(x) for x∈var(t), then σ(t) \underline{↔}_{b} σ′(t).

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

Theorem 3. Given a complete TSS P = (Σ, R) in branching bisimulation format, with respect to some ℵ. If σ(x) \underline{↔}_{b} σ′(x) for x∈var(t), then σ(t) \underline{↔}_{b} σ′(t).

Proof. Let P′ be obtained from P, by changing in all rules, expect the ℵ-patience rules, conclusions of the form t ⟶^{τ} u into t ⟶^{i} u, for a fresh action i ∉ A ∪ {τ}. By construction, P′ is abstraction-free and in branching bisimulation format with respect to ℵ. So by Lem. 2, \underline{↔}_{b} 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 and trivial to check that \underline{↔}_{b} 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{↔}_{b} is a congruence for τ_{i} ∘ f in P′′, it must be a congruence for f in P. ⊓ ⊔

Lemma 3. Given a complete, abstraction-free TSS in rooted branching bisimulation format, with respect to some ℵ and Λ. If σ(x) \underline{↔}_{rb} σ′(x) for x ∈ var(t), then σ(t) \underline{↔}_{rb} σ′(t).

Theorem 4. Given a complete TSS in rooted branching bisimulation format, with respect to some ℵ and Λ. If σ(x) \underline{↔}_{rb} σ′(x) for x∈var(t), then σ(t) \underline{↔}_{rb} σ′(t).

The proof of Lem. 3 is similar to the one of Lem. 2, except that Prop. 4 is applied instead of Prop. 3. Likewise, the proof of Thm. 4 is similar to the one of Thm. 3.

5 Applications

In this section we present four applications of the rooted branching bisimulation format.

5.1 Basic Process Algebra

Basic process algebra BPA [1] assumes a collection Act of constants, called atomic actions, which upon execution terminate successfully. The signature of BPA moreover includes function symbols + and · of arity two, called alternative composition and sequential composition, respectively. Intuitively, t_{1} +t_{2} executes either t_{1} or t_{2}, while t_{1}·t_{2} first executes t_{1} and upon successful termination executes t_{2}. We assume a special atomic action tick ∈ Act, indicating the activity of successful termination upon executing the internal action τ, and a special constant deadlock δ, outside Act, which does not display any behaviour. These intuitions are made precise by means of the transition rules for BPA_{δ}^{tick} presented below. In these rules, ℓ ranges over Act, and α over A = {ℓ, ℓ^{√} | ℓ ∈ Act}. The label ℓ^{√} denotes that upon execution of ℓ, the process terminates successfully.

\begin{matrix}ℓ ⟶^{ℓ^{√}} δ  \frac{x_{1} ⟶^{α} y}{x_{1} + x_{2} ⟶^{α} y}  \frac{x_{2} ⟶^{α} y}{x_{1} + x_{2} ⟶^{α} y} \\ \frac{x_{1} ⟶^{ℓ} y}{x_{1}·x_{2} ⟶^{ℓ} y·x_{2}} & \frac{x_{1} ⟶^{ℓ^{√}} y}{x_{1}·x_{2} ⟶^{ℓ} x_{2}} \end{matrix}

The label tick counts as internal action, and for this reason the labels tick and tick^{√} can also be written τ and τ^{√}, respectively. The label τ^{√} denotes termination and counts as a normal observable action. When this action occurs in the first component of a sequential composition, it changes into the internal action τ, so that this TSS is not abstraction-free. We do not have a \underline{↔}_{rb} a·tick, as the former process performs one visible action and the latter two. For this reason we call the constant tick tick, rather than τ.

The TSS above is in rooted branching bisimulation format, if we take the arguments of alternative composition to be Λ-frozen, the first argument of sequential composition to be ℵ-liquid, and the second argument of sequential composition to be ℵ-frozen. For the sake of the application to the action refinement operator, in Sect. 5.4, we take the second argument of sequential composition to be Λ-liquid.

Corollary 1. Rooted branching bisimulation is a congruence for BPA_{δ}^{tick}.

5.2 Binary Kleene star

The binary Kleene star t_{1}^{∗}t_{2} [18] repeatedly executes t_{1} until it executes t_{2}. This operational behaviour is captured by the following rules, which are added to the rules for BPA_{δ}^{tick}.

\frac{x_{1} ⟶^{ℓ} y}{x_{1}^{∗}x_{2} ⟶^{ℓ} y·(x_{1}^{∗}x_{2})}  \frac{x_{1} ⟶^{ℓ^{√}} y}{x_{1}^{∗}x_{2} ⟶^{ℓ} x_{1}^{∗}x_{2}}  \frac{x_{2} ⟶^{α} y}{x_{1}^{∗}x_{2} ⟶^{α} y}

The resulting TSS is in rooted branching bisimulation format, if we take the arguments of the binary Kleene star to be Λ-frozen.

Corollary 2. Rooted branching bisimulation is a congruence for BPA_{δ}^{tick} with the binary Kleene star.

5.3 Initial Priority

Initial priority is a unary function symbol that assumes an ordering on labels (which is usually defined on the level of atomic actions). The term θ(t) executes the transitions of t, with the restriction that an initial transition t ⟶^{α} t_{1} only gives rise to an initial transition θ(t) ⟶^{α} t_{1} if there does not exist an initial transition t ⟶^{β} t_{2} with α < β. This intuition is captured by the rule for the initial priority operator below, which is added to the rules for BPA_{δ}^{tick}.

\frac{x ⟶^{α} y x −̸→^{β} for α < β}{θ(x) ⟶^{α} y}

The resulting TSS is in rooted branching bisimulation format, if we take the argument of initial priority to be Λ-frozen.

Corollary 3. Rooted branching bisimulation is a congruence for BPA_{δ}^{tick} with initial priority.

5.4 Action Refinement

In the previous applications, it sufficed to take Λ = ℵ. In the following example, however, this is not possible.

The binary action refinement operator t_{1}[ℓ ⇝ t_{2}], for ℓ ∈ Act\{tick}, replaces each ℓ-transition in t_{1} by t_{2}. Its transition rules, presented below, are added to the rules for BPA_{δ}^{tick}.

\frac{x_{1} ⟶^{α} y}{x_{1}[ℓ ⇝ x_{2}] ⟶^{α} y[ℓ ⇝ x_{2}]} (α ≠ ℓ, ℓ^{√})

\frac{x_{1} ⟶^{ℓ} y_{1} x_{2} ⟶^{ℓ′} y_{2}}{x_{1}[ℓ ⇝ x_{2}] ⟶^{ℓ′} y_{2}·(y_{1}[ℓ ⇝ x_{2}])}  \frac{x_{1} ⟶^{ℓ^{√}} y_{1} x_{2} ⟶^{ℓ′} y_{2}}{x_{1}[ℓ ⇝ x_{2}] ⟶^{ℓ′} y_{2}}

\frac{x_{1} ⟶^{ℓ} y_{1} x_{2} ⟶^{ℓ′^{√}} y_{2}}{x_{1}[ℓ ⇝ x_{2}] ⟶^{ℓ′} y_{1}[ℓ ⇝ x_{2}]}  \frac{x_{1} ⟶^{ℓ^{√}} y_{1} x_{2} ⟶^{ℓ′^{√}} y_{2}}{x_{1}[ℓ ⇝ x_{2}] ⟶^{ℓ′√} y_{2}}

The resulting TSS is in rooted branching bisimulation format, if we take the first argument of action refinement to be ℵ-liquid and the second argument to be Λ-frozen. For the second rule to be rooted branching bisimulation safe, it is essential that the second argument of sequential composition is Λ-liquid, for else it would violate restriction 2 of Def. 15.

Corollary 4. Rooted branching bisimulation is a congruence for BPA_{δ}^{tick} with action refinement.

6 Counterexamples

This section presents a series of counterexamples of complete TSSs in ntyft/ntyxt format, to show that none of the syntactic restrictions of our congruence formats can be omitted. (Of course it remains possible that certain restrictions can be refined.) In [16] a series of counterexamples can be found showing that the syntactic restrictions of the ntyft/ntyxt format are essential as well. Furthermore, in [5] a counterexample is given to show that completeness (there called positive after reduction) is essential.

It is well-known that branching bisimulation is not a congruence for BPA_{δ}^{tick}. For instance, a\underline{↔}_{b} tick·a, but a + c\underline{↮}_{b} (tick·a) + c. Still we saw in Sect. 5.1 that the TSS for this process algebra is in rooted branching bisimulation format. This shows that universality of the predicate Λ cannot be omitted from the branching bisimulation format.

The examples in this section assume an action set A = {a, b, c} and a TSS P = {Σ, R}, where the signature Σ contains the constant 0 and unary function symbols α for α ∈ A ∪ {τ}, and R contains the rules αx ⟶^{α} x for α ∈ A ∪ {τ}. The argument of α is ℵ-frozen. Unlike before, in this section occurrences of a, b, c as labels in rules are explicit action names, instead of parameters ranging over A.

Example 2. We extend P with the following rule:

\frac{x ⟶^{a} y y ⟶^{b} z}{f(x) ⟶^{c} 0}

The rule above is not rooted branching bisimulation safe, because it contains lookahead, violating restriction 1 (of Def. 15). Clearly, ab0 \underline{↔}_{rb} aτb0 (and thus ab0\underline{↔}_{b} aτb0). However, f(ab0)\underline{↮}_{b} f(aτb0) (and thus f(ab0)\underline{↮}_{rb} f(aτb0)), since

f(ab0) ⟶^{c} 0, while f(aτb0) −̸→^{α} for α ∈ {c, τ}.

Example 3. We extend P with the following rule:

\frac{x ⟶^{a} y}{f(x) ⟶^{a} f(y)}

The argument of f must be ℵ-frozen, in view of the restriction in Def. 16 that for each ℵ-liquid argument there is an ℵ-patience rule. The rule above is not rooted branching bisimulation safe. Namely, if the argument of f is Λ-frozen, then y occurs both as the right-hand side of a premise and Λ-frozen in the right-hand side of the conclusion, violating restriction 2. And if the argument of f is Λ-liquid, then x occurs Λ-liquid and ℵ-frozen in the source and ℵ-liquid in the left-hand side of the premise, violating restriction 3(d). We have f(aa0)\underline{↮}_{b} f(aτa0), since f(aa0) ⟶^{a} f(a0) ⟶^{a} f(0), while f(aτa0) can only do an a-transition to f(τa0),

and f(τa0) −̸→^{α} for α ∈ {a, τ}.

Example 4. We extend P with the following rules:

\frac{x ⟶^{τ} y}{f(x) ⟶^{τ} f(y)}  \frac{x ⟶^{a} y}{f(x) ⟶^{a} f(y)}  \frac{x −̸→^{a}}{f(x) ⟶^{c} 0}

The argument of f has to be Λ-liquid, for else the first and second rule would violate restriction 2. It even has to be ℵ-liquid, for otherwise these rules would violate requirement 3(d). However, with the argument of f ℵ-liquid, the third rule is not rooted branching bisimulation safe, because x occurs ℵ-liquid both in the source and in the left-hand side of the negative premise, violating restriction 3(b). We have f(aa0)\underline{↮}_{b} f(aτa0), since f(aτa0) ⟶^{a} f(τa0) ⟶^{c} 0, while f(aa0) can only do an a-transition to f(a0), and f(a0) −̸→^{α} for α ∈ {c, τ}.

Example 5. We extend P with the following rules:

\frac{x ⟶^{τ} y}{f(x) ⟶^{τ} f(y)}  \frac{x ⟶^{a} y}{f(x) ⟶^{a} f(y)}  \frac{x ⟶^{τ} y}{f(x) ⟶^{c} 0}

As in the previous example, the argument of f has to be ℵ-liquid. The third rule is not rooted branching bisimulation safe, because x occurs ℵ-liquid both in the source and in the left-hand side of the positive premise with label τ, violating restriction 3(c). We have f(aa0) \underline{↮}_{b} f(aτa0), since f(aτa0) ⟶^{a} f(τa0) ⟶^{c} 0, while f(aa0) can only do an a-transition to f(a0), and f(a0) −̸→^{α} for α ∈ {c, τ}.

Example 6. We extend P with the following rules:

η ⟶^{a} 0  ζ ⟶^{b} 0  η ⟶^{τ} ζ  ζ ⟶^{τ} η  ν ⟶^{a} 0  ν ⟶^{b} 0

\frac{x ⟶^{τ} y}{f(x) ⟶^{τ} f(y)}  \frac{x ⟶^{a} y x ⟶^{b} z}{f(x) ⟶^{c} 0}

Again, the argument of f is ℵ-liquid. The last rule is not rooted branching bisimulation safe, because x has an ℵ-liquid occurrence in the source, and two ℵliquid occurrences in the left-hand sides of the premises, violating restriction 3(c). Clearly, τν \underline{↔}_{rb} τη. However, f(τν)\underline{↮}_{b} f(τη), since f(τν) ⟶^{τ} f(ν) ⟶^{c} 0, while f(τη) only exhibits an infinite sequence of τ-transitions: f(τη) ⟶^{τ} f(η) ⟶^{τ}

f(ζ) ⟶^{τ} f(η) ⟶^{τ} · · ·.

Example 7. In the TSS from Example 6, we replace the last rule with the following rules:

f(x) ⟶^{τ} g(x) \frac{x ⟶^{a} y x ⟶^{b} z}{g(x) ⟶^{c} 0}

The argument of f is again ℵ-liquid, and the argument of g must be Λ-frozen, as otherwise the second rule would violate restriction 3(c). The first rule above is not rooted branching bisimulation safe, because x occurs ℵ-liquid (hence Λ-liquid) in the source and Λ-frozen in the right-hand side of the conclusion, violating restriction 3(a). We have f(τν)\underline{↮}_{b} f(τη), since f(τν) ⟶^{τ} f(ν) ⟶^{τ} g(ν) ⟶^{c} 0, while f(τη) can only perform τ-transitions.

Example 8. In the TSS from Example 6, we replace the last rule with the following rules:

\frac{x ⟶^{a} y x ⟶^{b} z}{g(x) ⟶^{c} 0}  \frac{g(x) ⟶^{c} y}{f(x) ⟶^{c} 0}

As in the previous example, the argument of f must be ℵ-liquid, and the argument of g Λ-frozen. The last rule above is not rooted branching bisimulation safe, because x occurs ℵ-liquid in the source and Λ-frozen in the left-hand side of the premise, violating restriction 3(a). We have f(τν) \underline{↮}_{b} f(τη), since f(τν) ⟶^{τ} f(ν) ⟶^{c} 0, while f(τη) can only perform τ-transitions.

7 Related Work

The first congruence formats for branching and rooted branching bisimulation were presented in [2], and reformulated in [13]. Those formats, which are contained in the GSOS format [4], 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 [2, 13]. However, our formats generalise the result of simplifying the formats of [2, 13] by requiring all operators to be principal.

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

The format of [2, 13] for rooted branching bisimulation 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 [7].

In [7] a format for rooted branching bisimulation was proposed that generalises the simplified format of [2, 13]. Given that it applies to TSSs with predicates, it is incomparable with our current rooted branching bisimulation format. However, predicates can easily be encoded in terms of transitions, and when disregarding predicates, our current format is more general than the format of [7]. Still, the format of [7] strictly contains the intersection of our format with the GSOS format, and all applications of our work discussed in Sect. 5 fall within that intersection.

In [10] we apply the techniques of the current paper to derive congruence formats for η- and rooted η-bisimulation. These formats differ from the ones of the current paper only in restriction 2 of Def. 15. There it is required that right-hand sides of premises occur only ℵ-liquid in u, whereas here we merely require Λ-liquidity. That the rooted branching bisimulation format is essentially more general than the rooted η-bisimulation format is illustrated by the action refinement example of Sec. 5.4. BPA_{δ}^{tick} with action refinement falls outside the rooted η-bisimulation format, due to the fact that the second argument of sequential composition needs to be ℵ-liquid in order for the second action refinement rule to be rooted η-bisimulation safe. Indeed, this operator fails to be compositional for rooted η-bisimulation [14].

References

1. J.A. Bergstra & J.W. Klop (1984): Process algebra for synchronous communication. Information and Control 60(1/3), pp. 109–137.

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

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

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

5. R.N. Bol & J.F. Groote (1996): The meaning of negative premises in transition system specifications. Journal of the ACM 43(5), pp. 863–914.

6. R. De Nicola & F.W. Vaandrager (1995): Three logics for branching bisimulation. Journal of the ACM 42(2), pp. 458–487.

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

8. W.J. Fokkink & R.J. van Glabbeek (1996): Ntyft/ntyxt rules reduce to ntree rules. Information and Computation 126(1), pp. 1–10.

9. W.J. Fokkink, R.J. van Glabbeek & P. de Wind (2006): Compositionality of Hennessy-Milner logic by structural operational semantics. Theoretical Computer Science 354(3), pp. 421–440.

10. W.J. Fokkink, R.J. van Glabbeek & P. de Wind (2005): Divide and congruence applied to η-bisimulation. In Proc. SOS’05, To appear, ENTCS. Elsevier.

11. R.J. van Glabbeek (1993): 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.

12. R.J. van Glabbeek (2004): The meaning of negative premises in transition system specifications II. Journal of Logic and Algebraic Programming 60/61, pp. 229–258.

13. R.J. van Glabbeek (2005): On cool congruence formats for weak bisimulations (extended abstract). In Proc. ICTAC’05, LNCS 3722, pp. 331–346. Springer.

14. R.J. van Glabbeek & W.P. Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600.

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

16. J.F. Groote & F.W. Vaandrager (1992): Structured operational semantics and bisimulation as a congruence. Information and Computation 100(2), pp. 202–260.

17. M.C.B. Hennessy & R. Milner (1985): Algebraic laws for non-determinism and concurrency. Journal of the ACM 32(1), pp. 137–161.

18. S.C. Kleene: Representation of events in nerve nets and finite automata. In (C. Shannon and J. McCarthy, eds.) Automata Studies, pp. 3–41. Princeton University Press, 1956.

19. K.G. Larsen & X. Liu (1991): Compositionality through an operational semantics of contexts. Journal of Logic and Computation 1(6), pp. 761–795.

20. G.D. Plotkin (2004): A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60/61, pp. 17–139. Originally appeared in 1981.

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

A Modal Characterisation of Branching Bisimulation

We prove the first part of Thm. 1, which states that 𝕆_{b} is a modal characterisation of branching bisimulation equivalence. The proof is based on [6]. We need to prove, given an LTS (ℙ, →), that p\underline{↔}_{b} q ⇔ p ∼_{𝕆_{b}} q for all p, q ∈ ℙ.

Proof. (⇒) Suppose p \underline{↔}_{b} q, and p ⊧ φ for some φ ∈ 𝕆_{b}. We prove q ⊧ φ, by structural induction on φ. The reverse implication (q ⊧ φ implies p ⊧ φ) 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 ⊧ ¬φ′.

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

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

n. n = 0 Then p ⊧ φ_{1}, so by induction on formula size, q ⊧ φ_{1}. Further-

more, either (1) p ⊧ φ_{2} or (2) there is a p′ ∈ ℙ with p ⟶^{τ} p′ and p′ ⊧ φ_{2}. In case (1), by induction on formula size, q ⊧ φ_{2}, so q ⊧ ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}). In case (2), since p \underline{↔}_{b} q, by Def. 1 either (2.1) p′ \underline{↔}_{b} q or (2.2) q ⟹^{ϵ} q′ ⟶^{τ} q′′ with p \underline{↔}_{b} q′ and p′ \underline{↔}_{b} q′′. In case (2.1), by induction on formula size, q ⊧ φ_{2}. In case (2.2), by induction on formula size, q′ ⊧ φ_{1} and q′′ ⊧ φ_{2}. In both cases, q ⊧ ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}).

n > 0 Since p ⟶^{τ} p_{1}, and p \underline{↔}_{b} q, according to Def. 1 there are two possibilities.

1. Either p_{1} \underline{↔}_{b} q. Since p_{1} ⊧ ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}), by induction on n, q ⊧ ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}).

2. Or q ⟹^{ϵ} q′ ⟶^{τ} q′′ with p_{1} \underline{↔}_{b} q′′. Since p_{1} ⊧ ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}), by in-

duction on n, q′′ ⊧ ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}). Hence q ⊧ ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}).

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

p_{i} ⟶^{τ} p_{i+1} for i ∈ {0, …, n − 1}, and p_{n} ⊧ φ_{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}. Since

p\underline{↔}_{b} q, by Def. 1 q ⟹^{ϵ} q′ ⟶^{a} q′′ with p\underline{↔}_{b} q′ and p′ \underline{↔}_{b} q′′. By induction on formula size, q′ ⊧ φ_{1} and q′′ ⊧ φ_{2}. Hence q ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}).

n > 0 Since p ⟶^{τ} p_{1}, and p \underline{↔}_{b} q, according to Def. 1 there are two possibilities.

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

2. Or q ⟹^{ϵ} q′ ⟶^{τ} q′′ with p_{1} \underline{↔}_{b} q′′. Since p_{1} ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}), by in-

duction on n, q′′ ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}). Hence q ⊧ ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}).

We conclude that p ∼_{𝕆_{b}} q.

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

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

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

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

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

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

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

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

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

Both cases imply that the second condition of Def. 1 is fulfilled. We therefore conclude that ∼_{𝕆_{b}} is a branching bisimulation relation. ⊓ ⊔

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