Divide and Congruence: From Decomposition of Modal Formulas

to Preservation of Branching and η-Bisimilarity

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

1 VU University Amsterdam, Department of Computer Science, Amsterdam 2 National ICT Australia, Sydney

3 University of New South Wales, School of Computer Sc. and Engineering, Sydney

       w.j.fokkink@vu.nl, rvg@cs.stanford.edu, p.dewind@tiscali.nl

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 two weak and rooted weak semantics: branching and η-bisimilarity.

1 Introduction

Structural operational semantics [30] 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 [17] classified so-called weak semantics, which take into account the internal action τ. Here we focus on two such equivalences which, to different degrees, abstract away from internal actions: branching bisimilarity [20] and η-bisimilarity [2]. Also we consider the rooted counterparts of these equivalences, which were introduced because unlike the unrooted versions they are congruences for basic process algebras, notably for the alternative composition operator.

In general a behavioural equivalence induced by a transition system specification is not guaranteed to be a congruence, i.e. the equivalence class of a term f(p_{1}, …, p_{n}) need not be determined by f and 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 bisimilarity, such as the De Simone format [31], the GSOS format [7], the tyft/tyxt format [22], and the ntyft/ntyxt format [21]. Bloom [5] introduced congruence formats for branching bisimilarity and for rooted branching bisimilarity. 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 on processes consists of a class C of modal formulas such that two processes are equivalent if and only if they satisfy the same formulas in C. For instance, Hennessy-Milner logic [23] is a modal characterisation of (strong) bisimilarity.

Larsen & Liu [26] introduced a method for decomposing formulas from Hennessy-Milner logic for τ-free processes, with respect to terms from a process algebra with a structural operational semantics in the 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 [6] to the ntyft/ntyxt format without lookahead, and by Fokkink, van Glabbeek & de Wind [12] to the tyft/tyxt format. In [6], 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 [6] to processes with τ-transitions. We present a method for decomposing modal formulas for processes with τ-transitions, and use this decomposition method to obtain congruence formats for two weak and rooted weak semantics: branching and η-bisimilarity. 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. The congruence formats that we obtain are more liberal and more elegant than existing congruence formats for these semantics. In Sect. 8 we will present an in-depth comparison with congruence formats from the literature.

Our formats use two predicates ℵ and Λ on arguments of function symbols: ℵ marks processes that can execute immediately, and Λ marks processes that have started executing (but may currently be unable to execute). The predicate ℵ is new, whereas Λ originates from [10]. The two formats for weak semantics (branching and η-bisimilarity) can be expressed as a subset of the formats for the corresponding rooted weak semantics, by imposing one extra restriction: Λ must be universal, meaning that it holds for all arguments of function symbols.

Preliminary versions of this paper, focusing on branching and η-bisimilarity, respectively, were published as [13,14].

2 Preliminaries

This section recalls the basic notions of labelled transition systems and weak semantics (Sect. 2.1), and presents modal characterisations of the semantic equivalences that are studied in this paper (Sect. 2.2). Then follows a brief introduction to structural operational semantics and the notion of a well-supported proof (Sect. 2.3). Next we recall some syntactic restrictions on transition rules (Sect. 2.4). Finally, we recall a basic result from [6], Prop. 1, regarding so-called ruloids (Sect. 2.5), and introduce two predicates Λ and ℵ on arguments of function symbols (Sect. 2.6).

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 p, q to denote processes, α, β, γ 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

⟶^{τ}.

The following two versions of bisimilarity abstract away, to different degrees, from the internal action τ.

Definition 1. Let B ⊆ ℙ × ℙ be 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 p \underline{↔}_{b} q, if there exists a branching bisimulation B with pBq.

– B is an η-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 η-bisimilar, denoted p\underline{↔}_{η} q, if there exists an η-bisimulation B with pBq.

Clearly, branching bisimilarity is included in η-bisimilarity. A typical example of two processes that are η- but not branching bisimilar is: Let p ⟶^{a} r be the only transition of p, q ⟶^{a} r and q ⟶^{a} s the only two transitions of q, and r ⟶^{τ} s. Then, independent of the transitions of r and s, always p \underline{↔}_{η} q, because q ⟶^{a} s can be mimicked by p ⟶^{a} r ⟶^{τ} s. But in general p\underline{↮}_{b} q.

It is well-known that branching and η-bisimilarity constitute equivalence relations [3,2]. However, these two weak semantics are not congruences with respect to most process algebras from the literature, meaning that the equivalence class of a process f(p_{1}, …, p_{n}), with f an n-ary function symbol, is not always determined by the equivalence classes of its arguments, i.e. the processes p_{1}, …, p_{n}. A rootedness condition generally remedies this imperfection.

Definition 2. Let R ⊆ ℙ × ℙ be 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 p\underline{↔}_{rb} q, if there exists a rooted branching bisimulation R with pRq.

– R is a rooted η-bisimulation if pRq and p ⟶^{α} p′ implies that q ⟶^{α}⟹^{ϵ} q′ for some q′ with p′ \underline{↔}_{η} q′. Processes p, q are rooted η-bisimilar, denoted p\underline{↔}_{rη} q, if there exists a rooted η-bisimulation R with pRq.

Our main aim is to develop congruence formats for both the rooted and the unrooted versions of the two weak semantics defined in this section. These congruence formats will impose syntactic restrictions on the transition rules (see Sect. 2.3) that are used to generate the underlying LTS. The congruence formats will be determined using the characterising modal logics for these two weak semantics, which are presented in the next section.

2.2 Modal logic

Modal logic aims to formulate properties of processes in an LTS. Following [17], we extend Hennessy-Milner logic [23] with the modal connectives ⟨ϵ⟩φ and ⟨τ̂⟩φ, expressing that a process can perform zero or more, respectively zero or one, τ-transitions to a state where φ holds.

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′ for some

p′ with p′ ⊧ φ, p ⊧ ⟨ϵ⟩φ if p ⟹^{ϵ} p′ for some p′ with p′ ⊧ φ, and p ⊧ ⟨τ̂⟩φ if

either p ⊧ φ or p ⟶^{τ} p′ for some 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 𝕆_{e} and 𝕆_{re} of 𝕆, for e ∈ {b, η}, are defined as follows:

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

In these definitions, a ranges over A and α over A_{τ}. The classes 𝕆_{e}^{≡} and 𝕆_{re}^{≡} denote the closures of 𝕆_{e}, respectively 𝕆_{re}, under ≡.

The last clause in the definition of 𝕆_{re} guarantees that 𝕆_{e} ⊆ 𝕆_{re}, which will be needed in the proof of Prop. 4. If this clause were omitted, it would still follow that 𝕆_{e}^{≡} ⊆ 𝕆_{re}^{≡}, using structural induction together with ⟨ϵ⟩⟨ϵ⟩φ ≡ ⟨ϵ⟩φ, ⟨τ⟩⟨ϵ⟩φ ≡ ⟨ϵ⟩⟨τ⟩φ, ⟨ϵ⟩φ ≡ φ ∨ ⟨τ⟩⟨ϵ⟩φ and (for e = b) ⟨τ̂⟩φ ≡ φ ∨ ⟨τ⟩φ. 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 ∼_{𝕆_{e}} q ⇔ p ∼_{𝕆_{e}^{≡}} q and p ∼_{𝕆_{re}} q ⇔ p ∼_{𝕆_{re}^{≡}} q.

Theorem 1. p \underline{↔}_{e} q ⇔ p ∼_{𝕆_{e}} q and p \underline{↔}_{re} q ⇔ p ∼_{𝕆_{re}} q, for all p, q ∈ ℙ, and e ∈ {b, η}.

A proof of this theorem for the case e = b is presented in the appendix. The proof for the case e = η is similar.

2.3 Structural operational semantics

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

Structural operational semantics [30] generates a labelled transition system, in which the processes are the closed terms, and transitions between processes are supplied with labels. The transitions between processes are obtained from a transition system specification, which consists of a set of proof rules called transition rules.

Definition 5. A (positive or negative) literal is an expression t ⟶^{α} u or t −̸→^{α}. A (transition) rule is of the form \frac{H}{λ} with H a set of literals called the premises, and λ a literal called the conclusion; the terms at the left- and right-hand side of λ are called the source and target of the rule, respectively. With rhs(H) we denote the set of right-hand sides of the positive premises in H. A rule \frac{∅}{λ} is also written λ. A rule is standard if it has a positive conclusion. A transition system specification (TSS), written (Σ, R), consists of a signature Σ and a collection R of transition rules over Σ. A TSS is standard if all its rules are.

The concept of a standard TSS with only positive premises was introduced in [22]; negative premises were added in [21]. The resulting notion constitutes the first formalisation of structural operational semantics [30] that is sufficiently general to cover many of its applications. TSSs with negative conclusions were introduced in [6] because they are needed as intermediate steps in our proofs for standard TSSs.

The following definition tells when a literal is provable from a TSS. It generalises the standard definition (see e.g. [22]) by allowing the derivation of transition rules. The derivation of a literal λ corresponds to the derivation of the transition rule \frac{H}{λ} with H = ∅. The case H ≠ ∅ corresponds to the derivation of λ under the assumptions H.

Definition 6. Let P = (Σ, R) be a TSS. An irredundant proof from P of a rule \frac{H}{λ} is a well-founded tree with the nodes labelled by literals and some of the leaves marked “hypothesis”, such that the root has label λ, 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 \frac{K}{μ} is a substitution instance of a rule in R.

The proof of \frac{H}{λ} is called irredundant [6] because H must equal (instead of include) the set of labels of the hypotheses. Irredundancy will be crucial for the preservation under provability of our congruence formats; see Sect. 4.2. Namely, in a ‘redundant’ proof one can freely add premises to the derived rule, so also a premise that violates a syntactic restriction of the congruence format under consideration.

A TSS is meant to specify an LTS in which the transitions are closed positive literals. A standard 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 [18] we adopt the notion of a well-supported proof of a closed literal. Literals t ⟶^{α} u and t −̸→^{α} are said to deny each other.

Definition 7. Let P = (Σ, R) be standard 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. A standard TSS P is complete if for each p and α, either P ⊢_{ws} p −̸→^{α} or P ⊢_{ws} p ⟶^{α} p′ for some p′.

In [18] it was shown that ⊢_{ws} is consistent, in the sense that no standard TSS admits well-supported proofs of two literals that deny each other. A complete TSS specifies an LTS, consisting of the ws-provable closed positive literals.

Example 1. Let A = {a} and P = (Σ, R), where Σ = {a} and R consists of the rule \frac{a−̸→^{a}}{a⟶^{a}a}. The standard TSS P is not complete, because neither P ⊢_{ws} a −̸→^{a} nor P ⊢_{ws} a ⟶^{a} a. For this reason P can be considered not to specify an LTS.

2.4 Syntactic restrictions on transition rules

In this section we present terminology for syntactic restrictions on rules, originating from [6,21,22], where congruence formats are presented for a range of concrete semantics (which do not take into account the internal action τ).

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.

The idea behind the names of the rules is that the ‘n’ in front refers to the presence of negative premises, and the following four letters refer to the allowed forms of left- and right-hand sides of premises and of the conclusion, respectively. For example, ntyft means a rule with negative premises (n), where left-hand sides of premises are general terms (t), right-hand sides of positive premises are variables (y), the source contains exactly one function symbol (f), and the target, if present at all, is a general term (t).

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.

Each combination of syntactic restrictions on transition rules induces a corresponding syntactic format for TSSs of the same name. For instance, a TSS is in decent ntyft format if it contains decent ntyft rules only.

The following lemma, on the preservation of decency under irredundant provability, is proved in [6].

Lemma 1. Let P be a TSS in decent ntytt format. Then any ntytt rule irredundantly provable from P is decent.

We proceed to define further syntactic formats for TSSs. The ntyft/ntyxt and ready simulation formats [21,6] were originally introduced to guarantee congruence for (strong) bisimilarity 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 have no lookahead.

2.5 Ruloids

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

First P is converted to a standard TSS in decent ntyft format. In this conversion from [22], free variables in a rule are replaced by arbitrary closed terms, and if the source is of the form x, then this variable is replaced by a term f(x_{1}, …, x_{ar(f)}) for each n-ary function symbol f in the signature of P, where the variables x_{1}, …, x_{ar(f)} are fresh.

Next, using a construction from [11], left-hand sides of positive premises in rules of P are reduced to variables. Roughly the idea is, given a premise f(t_{1}, …, t_{n}) ⟶^{α} y in a rule r, and another 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 term as left-hand side have disappeared. This yields an intermediate standard TSS, all of whose rules are irredundantly provable from P.

In the final transformation step, non-standard rules with a negative conclusion t −̸→^{α} are introduced. The motivation is that instead of the notion of wellfounded provability of 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 non-standard rule \frac{H}{f(x_{1},...,x_{n})−̸→^{α}} is obtained by picking one premise from each standard rule with a conclusion of the form f(x_{1}, …, x_{n}) ⟶^{α} t, and including the denial of each of the selected premises as a premise in H. For this last transformation it is essential that rules have no lookahead.

The resulting TSS, which is in decent ntyft format, is denoted by P^{+}. In [6] it is established, for all closed literals μ, that P ⊢_{ws} μ if and only if μ is irredundantly provable from P^{+}. The P -ruloids are those decent nxytt rules that are irredundantly provable from P^{+}.

The following correspondence result from [6] 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 ρ(t) ⟶^{a} q, with ρ a closed substitution, if and only if there is a proof of this transition that uses at the root a P -ruloid with source t.

Proposition 1. Let P = (Σ, R) be a standard TSS in ready simulation format, t ∈ 𝕋(Σ) and ρ : V → 𝕋(Σ) a closed substitution. Then P ⊢_{ws} ρ(t) ⟶^{α} q if and only if there are a P -ruloid \frac{H}{t⟶^{α}u} and a closed substitution ρ′ such that P ⊢_{ws} ρ′(μ) for all μ ∈ H, ρ′(t) = ρ(t) and ρ′(u) = q.

2.6 The predicates Λ and ℵ

In Sect. 4, we will assume two predicates on arguments of function symbols. The predicate Λ marks arguments that contain processes that have started executing (but may currently be unable to execute). It stems from [10] and fine-tunes the predicate “tame” from Bloom [5], which is a predicate on function symbols rather than arguments of function symbols. The predicate ℵ is new and marks arguments that contain processes that can execute immediately.

For example, in process algebra, Λ and ℵ hold for the arguments of the merge t_{1}∥t_{2}, and for the first argument of sequential composition t_{1}·t_{2}; they can contain processes that started to execute in the past, and these processes can continue their execution immediately. On the other hand, Λ and ℵ typically do not hold for the second argument of sequential composition; it contains a process that did not yet start to execute, and cannot execute immediately (in absence of the empty process). Finally, Λ does not hold and ℵ holds for the arguments of alternative composition t_{1} + t_{2} (see Ex. 2 in Sect. 3); they contain processes that did not yet start to execute, but that can start executing immediately. In Sections 6.6 and 6.7 we will see examples of arguments for which Λ holds and ℵ does not.

We proceed to introduce some terminology from [5,6] for predicates on arguments of function symbols.

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 Γ -liquid if either t = x, or t = f(t_{1}, …, t_{ar(f)}) and the occurrence is Γ -liquid in t_{i} for a liquid argument i of f; otherwise the occurrence is Γ -frozen.

Note that an occurrence of a variable x in a term t ∈ 𝕋(Σ) is Γ -frozen if and only if t contains a subterm f(t_{1}, …, t_{ar(f)}) such that the occurrence of x is in t_{i} for a Γ -frozen argument i of f.

In Sect. 3 we will present a method for decomposing modal formulas that gives a special treatment to arguments of function symbols that are deemed patient; we will use a predicate Γ to mark the arguments that get this special treatment. In Sect. 4 we will instantiate Γ with ℵ∩Λ.

Definition 12. A standard ntyft rule is a patience rule for argument i of f if it is of the form

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

Given a predicate Γ, the rule above is called a Γ -patience rule, if Γ (f, i). A TSS is Γ -patient if it contains all Γ -patience rules. A standard ntytt rule is Γ - patient if it is irredundantly provable from the Γ -patience rules; else it is called Γ -impatient.

A patience rule for an argument i of a function symbol f expresses that terms f(p_{1}, …, p_{n}) can mimic the τ-transitions of argument p_{i} (cf. [5,10]). Typically, in process algebra, there are patience rules for the arguments of the merge and for the first argument of sequential composition, but not for the arguments of the alternative composition + or for the second argument of sequential composition.

Remark 1. A standard ntytt rule is Γ -patient if and only if it has the form \frac{x⟶^{τ}y}{C[x]⟶^{τ}C[y]} for some Γ -liquid context C[ ].

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 for closed substitutions ρ, ρ(t) ⊧ φ if ρ(x) ⊧ ψ(x) for all x ∈ var(t). Vice versa, whenever ρ(t) ⊧ φ, there is a decomposition mapping ψ ∈ t^{−1}(φ) with ρ(x) ⊧ ψ(x) for all x ∈ var(t). This is formalised in Thm. 2.

Definition 13. Let P = (Σ, R) be a Γ -patient standard TSS in ready simulation format. We define ·^{−1} : 𝕋(Σ) × 𝕆 → 𝒫(V → 𝕆) as the function that for each t ∈ 𝕋(Σ) and φ ∈ 𝕆 returns the set t^{−1}(φ) ∈ 𝒫(V → 𝕆) of decomposition mappings ψ : V → 𝕆 generated by following six conditions. Let t denote a univariate term, i.e. without multiple occurrences of the same variable.

1. ψ ∈ t^{−1}(⋀_{i∈I} φ_{i}) iff there are ψ_{i} ∈ t^{−1}(φ_{i}) for each i ∈ I such that

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

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

ψ(x) = \{ \begin{matrix}⋀_{χ∈h^{−1}(x)}¬χ(x) & if x ∈ var(t) \\ ⊤ & if x ∉ var(t) \end{matrix}

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

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

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

(a) either there is a χ ∈ t^{−1}(φ) such that

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

(b) or there is a non-Γ -patient P -ruloid \frac{H}{t⟶^{τ}u} and a χ ∈ u^{−1}(⟨ϵ⟩φ) such that

ψ(x) = \begin{cases}⊤ & if x ∉ var(t) \\ ⟨ϵ⟩ (χ(x) ∧ ⋀_{x⟶^{β}y∈H} ⟨β⟩χ(y) ∧ ⋀_{x−̸→^{γ}∈H} ¬⟨γ⟩⊤) & if x occurs ; Γ -liquid in t \\ χ(x) ∧ ⋀_{x⟶^{β}y∈H} ⟨β⟩χ(y) ∧ ⋀_{x−̸→^{γ}∈H} ¬⟨γ⟩⊤ & otherwise \end{cases}

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

(a) either ψ ∈ t^{−1}(φ);

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

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

(c) or there is a Γ -impatient P -ruloid \frac{H}{t⟶^{τ}u} and a χ ∈ u^{−1}(φ) such that

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

6. ψ ∈ σ(t)^{−1}(φ) for a non-injective substitution σ : var(t) → V iff there is a χ ∈ t^{−1}(φ) such that

ψ(x) = ⋀_{z∈σ^{−1}(x)} χ(z) for all x ∈ V

To explain the idea behind Def. 13, we expand on two of its cases. Consider t^{−1}(¬φ), and let ρ be a 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 a closed substitution. The question is under which conditions ψ(x) ∈ 𝕆 on ρ(x), for each 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 each 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 three lemmas state basic properties of formulas ψ(x).

Lemma 2. Let ψ ∈ t^{−1}(φ), for some term t and formula φ. If x ∉ var(t), then ψ(x) ≡ ⊤.

Proof. This can be derived in a straightforward fashion from Def. 13, by induction on the construction of ψ. ⊓ ⊔

The following lemma states that ·^{−1} is invariant under α-conversion up to ≡.

Lemma 3. Let ψ ∈ σ(t)^{−1}(φ) for σ : V → V a bijective renaming of variables. Then there is a ψ′ ∈ t^{−1}(φ) satisfying ψ′(x) ≡ ψ(σ(x)) for all x ∈ V.

Proof. Again by induction on the construction of ψ. ⊓ ⊔

Lemma 4. Let ψ ∈ t^{−1}(⟨ϵ⟩φ), for some term t and formula φ. If x occurs only Γ -liquid in t, then ψ(x) = ⟨ϵ⟩φ′ for some formula φ′.

Proof. Immediate from Def. 13.4. ⊓ ⊔

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

Theorem 2. Let P = (Σ, R) be a Γ -patient complete standard TSS in ready simulation format. For any term t ∈ 𝕋(Σ), closed substitution ρ, and φ ∈ 𝕆:

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

Proof. By simultaneous induction on the structure of φ and the construction of ψ. 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 closed substitution ρ′ with P ⊢_{ws} ρ′(μ) for μ ∈ H, ρ′(t) = ρ(t), i.e. ρ′(x) = ρ(x) for all x ∈ var(t), and ρ′(u) = p. Since ρ′(u) ⊧ φ′, by induction on formula size there is a χ ∈ u^{−1}(φ′) with ρ′(z) ⊧ χ(z) for each z ∈ var(u). Moreover, by Lem. 2, ρ′(z) ⊧ χ(z) ≡ ⊤ for each z ∉ var(u). Define ψ ∈ t^{−1}(⟨α⟩φ′) as in Def. 13.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} yields P ⊬_{ws} ρ′(x) ⟶^{γ} q for all q, and thus ρ′(x) ⊧ ¬⟨γ⟩⊤. Hence ρ(x) = ρ′(x) ⊧ ψ(x).

(⇐) Let ψ ∈ t^{−1}(⟨α⟩φ′) with ρ(x) ⊧ ψ(x) for all x ∈ var(t). According to Def. 13.3, 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 all x ∈ var(t). For each x ∈ var(t), ρ(x) ⊧ ψ(x) yields, for each i ∈ I_{x}, P ⊢_{ws} ρ(x) ⟶^{β_{i}} p_{i} ⊧ χ(y_{i}) for some p_{i}; moreover, for each j ∈ J_{x} we have P ⊬_{ws} ρ(x) ⟶^{γ_{j}} q for all q, so by the completeness of P, P ⊢_{ws} ρ(x) −̸→^{γ_{j}}. Define ρ′(x) = ρ(x) and ρ′(y_{i}) = p_{i} for all 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 all z ∈ var(u), because var(u) ⊆ {x, y_{i} | x ∈ var(t), i ∈ I_{x}}. So by induction on formula size, ρ′(u) ⊧ φ′. Moreover, for each x ∈ var(t),

P ⊢_{ws} ρ′(x) ⟶^{β_{i}} ρ′(y_{i}) for each i ∈ I_{x}, and P ⊢_{ws} ρ′(x) −̸→^{γ_{j}} for each 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 all i∈{0, …, n−1}, with ρ(t) = p_{0} and p_{n} ⊧ φ′, then there is a ψ ∈ t^{−1}(⟨ϵ⟩φ′) with ρ(x) ⊧ ψ(x) for all x ∈ var(t). n = 0 Since ρ(t) = p_{0} ⊧ φ′, by induction on formula size, there is a χ ∈

t^{−1}(φ′) with ρ(x) ⊧ χ(x) for all x ∈ var(t). Define ψ ∈ t^{−1}(⟨ϵ⟩φ′) as in Def. 13.4a, using χ. Then clearly ρ(x) ⊧ ψ(x) for all 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 closed substitution ρ′ with P ⊢_{ws} ρ′(μ) for all μ ∈ H, ρ′(t) = ρ(t), i.e. ρ′(x) = ρ(x) for all x ∈ var(t), and ρ′(u) = p_{1}. Since P ⊢_{ws} ρ′(u) = p_{1} ⟶^{τ} ⋯ ⟶^{τ} p_{n} ⊧ φ′, by induction on n there is a χ ∈ u^{−1}(⟨ϵ⟩φ′) with ρ′(z) ⊧ χ(z) for each z ∈ var(u). Moreover, by Lem. 2, ρ′(z) ⊧ χ(z) ≡ ⊤ for each z ∉ var(u). We distinguish two cases.

Case 1: \frac{H}{t⟶^{τ}u} is Γ -patient. By Remark 1, using that t is univariate, H must be of the form {x_{0} ⟶^{τ} y_{0}}, with u = t[y_{0}/x_{0}], and the unique occurrence of y_{0} in u being Γ -liquid. Let σ : V → V be the bijection that swaps x_{0} and y_{0}, so that u = σ(t). According to Lem. 3, there is a χ′ ∈ t^{−1}(⟨ϵ⟩φ′) satisfying χ′(x) ≡ χ(σ(x)) for all x ∈ V. For each x ∈ var(t)\{x_{0}}, ρ(x) = ρ′(x) ⊧ χ(x) ≡ χ′(x), so ρ(x) ⊧ χ′(x). Furthermore, P ⊢_{ws} ρ′(x_{0}) ⟶^{τ} ρ′(y_{0}) ⊧ χ(y_{0}). By Lem. 4, χ(y_{0})≡⟨ϵ⟩φ′′ for some φ′′. Hence ρ(x_{0}) = ρ′(x_{0}) ⊧ χ(y_{0}) ≡ χ′(x_{0}), so ρ(x_{0}) ⊧ χ′(x_{0}).

Case 2: \frac{H}{t⟶^{τ}u} is Γ -impatient. Define ψ ∈ t^{−1}(⟨ϵ⟩φ′) as in Def. 13.4b, using \frac{H}{t⟶^{τ}u} and χ. Let x ∈ var(t). For each x ⟶^{β} y ∈ H, P ⊢_{ws} ρ′(x) ⟶^{β} ρ′(y) and ρ′(y) ⊧ χ(y), so ρ′(x) ⊧ ⟨β⟩χ(y). Moreover, for each x −̸→^{γ} ∈ H, P ⊢_{ws} ρ′(x) −̸→^{γ}, so the consistency of ⊢_{ws} yields P ⊬_{ws} ρ′(x) ⟶^{γ} q for all q, and thus ρ′(x) ⊧ ¬⟨γ⟩⊤. Hence ρ(x) = ρ′(x) ⊧ ψ(x). (In case the occurrence of x in t is Γ -liquid, note that if p ⊧ ξ then certainly p ⊧ ⟨ϵ⟩ξ.)

(⇐) Let ψ ∈ t^{−1}(⟨ϵ⟩φ′) with ρ(x) ⊧ ψ(x) for all x ∈ var(t). According to Def. 13.4 we can distinguish two cases. Case 1: There is a χ ∈ t^{−1}(φ′) with ψ(x) = ⟨ϵ⟩χ(x) if x occurs Γ -liquid

in t, and ψ(x) = χ(x) otherwise. Then ρ(x) ⊧ χ(x) for each x that occurs Γ -frozen in t. Furthermore, for each x that occurs Γ -liquid in t, ρ(x) ⊧ ⟨ϵ⟩χ(x), i.e. P ⊢_{ws} ρ(x) ⟹^{ϵ} p_{x} ⊧ χ(x) for some p_{x}. Define ρ′(x) = p_{x} if x occurs Γ -liquid in t, and ρ′(x) = ρ(x) otherwise. Since P is Γ -patient, P ⊢_{ws} ρ(t) ⟹^{ϵ} ρ′(t). We have ρ′(x) ⊧ χ(x) for all x ∈ var(t), so by induction on formula size, ρ′(t) ⊧ φ′. Hence ρ(t) ⊧ ⟨ϵ⟩φ′.

Case 2: There is a Γ -impatient P -ruloid \frac{H}{t⟶^{τ}u}, and a χ ∈ u^{−1}(⟨ϵ⟩φ′) with ψ(x) = ⟨ϵ⟩ψ′(x) if x occurs Γ -liquid in t, and ψ(x) = ψ′(x) otherwise, where

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

For each x that occurs Γ -liquid in t, P ⊢_{ws} ρ(x) ⟹^{ϵ} p_{x} ⊧ ψ′(x) for some p_{x}. Let ρ′(x) = p_{x} if x occurs Γ -liquid in t, and ρ′(x) = ρ(x) otherwise. Since P is Γ -patient, P ⊢_{ws} ρ(t) ⟹^{ϵ} ρ′(t). Furthermore ρ′(x) ⊧ ψ′(x) for all x ∈ var(t). Utilising the case φ = ⟨τ⟩φ′ of this proof, which we obtained above, it follows that ρ′(t) ⊧ ⟨τ⟩φ′. Hence ρ(t) ⊧ ⟨ϵ⟩φ′.

– φ = ⟨τ̂⟩φ′ (⇒) Suppose ρ(t) ⊧ ⟨τ̂⟩φ′. Then either ρ(t) ⊧ φ′, or P ⊢_{ws} ρ(t) ⟶^{τ} p ⊧ φ′ for some p. In the first case, by induction on formula size, there is a ψ∈t^{−1}(φ′) such that ρ(x) ⊧ ψ(x) for all x ∈ var(t); by Def. 13.5a, ψ ∈ 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 all μ ∈ H, ρ′(t) = ρ(t), i.e. ρ′(x) = ρ(x) for all x ∈ var(t), and ρ′(u) = p. Since ρ′(u) ⊧ φ′, by induction on formula size, there is a χ ∈ u^{−1}(φ′) such that ρ′(z) ⊧ χ(z) for each z ∈ var(u). Furthermore, by Lem. 2, ρ′(z) ⊧ χ(z) ≡ ⊤ for each z ∉ var(u). We distinguish two cases. Case 1: \frac{H}{t⟶^{τ}u} is Γ -patient. By Remark 1, using that t is univariate, H must

be of the form {x_{0} ⟶^{τ} y_{0}}, with u = t[y_{0}/x_{0}], and the unique occurrence of y_{0} in u being Γ -liquid. Let σ : V → V be the bijection that swaps x_{0} and y_{0}, so that u = σ(t). Let ψ(y_{0}) = ⟨τ̂⟩χ(y_{0}) and ψ(x) = χ(x) for x ≠ y_{0}. By Def. 13.5b, ψ ∈ u^{−1}(⟨τ̂⟩φ). According to Lem. 3, there is a ψ′ ∈ t^{−1}(⟨ϵ⟩φ′) satisfying ψ′(x) ≡ ψ(σ(x)) for all x ∈ V. For each x ∈ var(t)\{x_{0}}, ρ(x) = ρ′(x) ⊧ χ(x) = ψ(x) ≡ ψ′(x), so ρ(x) ⊧ ψ′(x). Furthermore, P ⊢_{ws} ρ′(x_{0}) ⟶^{τ} ρ′(y_{0}) ⊧ χ(y_{0}), hence ρ(x_{0}) = ρ′(x_{0}) ⊧ ⟨τ̂⟩χ(y_{0}) = ψ(y_{0}) ≡ ψ′(x_{0}), so ρ(x_{0}) ⊧ ψ′(x_{0}).

Case 2: \frac{H}{t⟶^{τ}u} is Γ -impatient. Define ψ ∈ t^{−1}(⟨τ̂⟩φ′) as in Def. 13.5c, using \frac{H}{t⟶^{τ}u} and χ. Let x ∈ var(t). For each x ⟶^{β} y ∈ H, P ⊢_{ws} ρ′(x) ⟶^{β} ρ′(y) and ρ′(y) ⊧ χ(y), so ρ′(x) ⊧ ⟨β⟩χ(y). Moreover, for each x −̸→^{γ} ∈ H, P ⊢_{ws} ρ′(x) −̸→^{γ}, so the consistency of ⊢_{ws} yields P ⊬_{ws} ρ′(x) ⟶^{γ} q for all q, and thus ρ′(x) ⊧ ¬⟨γ⟩⊤. Hence ρ(x) = ρ′(x) ⊧ ψ(x).

(⇐) Suppose ψ ∈ t^{−1}(⟨τ̂⟩φ′) with ρ(x) ⊧ ψ(x) for all x ∈ var(t). According to Def. 13.5 we can distinguish three cases.

Case 1: ψ ∈t^{−1}(φ′). By induction on formula size, ρ(t)⊧φ′, so ρ(t)⊧⟨τ̂⟩φ′. Case 2: Some x_{0} occurs Γ -liquid in t, and there is a χ ∈ t^{−1}(φ′) with

ψ(x_{0}) = ⟨τ̂⟩χ(x_{0}), and ψ(x) = χ(x) otherwise. Then ρ(x) ⊧ χ(x) for each x ∈ var(t)\{x_{0}}. Furthermore, ρ(x_{0}) ⊧ ⟨τ̂⟩χ(x_{0}), so either ρ(x_{0}) ⊧ χ(x_{0}) or P ⊢_{ws} ρ(x_{0}) ⟶^{τ} p ⊧ χ(x_{0}) for some p. In the first case, by induction on formula size, ρ(t) ⊧ φ′, so ρ(t) ⊧ ⟨τ̂⟩φ′, and we are done. In the second case, by the presence of all Γ -patience rules, P ⊢_{ws} ρ(t) ⟶^{τ} ρ(t[p/x_{0}]). Furthermore, by induction on formula size, ρ(t[p/x_{0}]) ⊧ φ′. Hence ρ(t) ⊧ ⟨τ̂⟩φ′.

Case 3: There is a Γ -impatient P -ruloid \frac{H}{t⟶^{τ}u}, and a χ ∈ u^{−1}(⟨ϵ⟩φ′) with ψ(x) as given in Def. 13.5c. Utilising the case φ = ⟨τ⟩φ′ of this proof, obtained above, it follows that ρ(t) ⊧ ⟨τ⟩φ′. Hence ρ(t) ⊧ ⟨τ̂⟩φ′.

Finally, suppose t is not univariate. Let t = σ(u) for some univariate u and noninjective substitution σ : var(u) → V. Then ρ(σ(u)) ⊧ φ ⇔ ∃χ ∈ u^{−1}(φ) ∀z ∈ var(u) : ρ(σ(z)) ⊧ χ(z) ⇔ ∃χ ∈ u^{−1}(φ) ∀x ∈ var(t) : ρ(x) ⊧ ⋀_{z∈σ^{−1}(x)} χ(z) ⇔ ∃ψ ∈ t^{−1}(φ) ∀x ∈ var(t) : ρ(x) ⊧ ψ(x). ⊓ ⊔ The part of Thm. 2 that deals with the modalities ⋀_{i∈I}, ¬ and ⟨α⟩ only, has already been established in [12]. There, a few examples are given showing how Def. 13 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 2. Consider basic CCS, consisting of the inaction constant 0, the prefix operator αt where α ranges over some set of actions containing the internal action τ, alternative composition t_{1} + t_{2}, and the merge t_{1}∥t_{2}. The transition rules are:

\overline{αx ⟶^{α} x}  \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_{2} ⟶^{α} y}{x_{1}∥x_{2} ⟶^{α} x_{1}∥y}

This standard TSS is complete and in ready simulation format.

Let Γ be defined to hold only for the two arguments of the merge. The rules \frac{x_{1}⟶^{τ}y}{x_{1}∥x_{2}⟶^{τ}y∥x_{2}} and \frac{x_{2}⟶^{τ}y}{x_{1}∥x_{2}⟶^{τ}x_{1}∥y} are Γ -patience rules. They make the TSS Γ -patient.

We compute (x_{1}∥x_{2})^{−1}(⟨ϵ⟩⟨a⟩⊤). As there is no Γ -impatient ruloid \frac{H}{x_{1}∥x_{2}⟶^{τ}u},

Def. 13.4b is vacuous. By Def. 13.4a, for each ψ ∈ (x_{1}∥x_{2})^{−1}(⟨ϵ⟩⟨a⟩⊤) we have ψ(x_{1}) = ⟨ϵ⟩χ(x_{1}) and ψ(x_{2}) = ⟨ϵ⟩χ(x_{2}) for some χ ∈ (x_{1}∥x_{2})^{−1}(⟨a⟩⊤). According to Def. 13.3, we have (x_{1}∥x_{2})^{−1}(⟨a⟩⊤) = {χ_{1}, χ_{2}}, where χ_{1} and χ_{2} are constructed from the only P -ruloids with a conclusion x_{1}∥x_{2} ⟶^{a} , namely the two rules in the TSS themselves, together with ξ_{1} ∈ (y∥x_{2})^{−1}(⊤) resp. ξ_{2} ∈ (x_{1}∥y)^{−1}(⊤):

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

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

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

4 Branching Bisimilarity as a Congruence

A behavioural equivalence ∼ is a congruence for a function symbol f defined on an LTS if p_{i} ∼ q_{i} for all i ∈ {1, …, ar(f)} implies that f(p_{1}, …, p_{ar(f)}) ∼ f(q_{1}, …, q_{ar(f)}). We call ∼ a congruence for a TSS (Σ, R), if it is a congruence for all function symbols from the signature Σ with respect to the LTS generated by (Σ, R). This is the case if for any open term t ∈ 𝕋(Σ) and any closed substitutions ρ, ρ′ : V → 𝕋 we have that

∀x ∈ var(t). ρ(x) ∼ ρ′(x) ⇒ ρ(t) ∼ ρ′(t) .

A congruence format for ∼ is a list of syntactic restrictions on TSSs, such that ∼ is guaranteed to be a congruence for any TSS satisfying these restrictions.

We proceed to apply the decomposition method from the previous section to derive congruence formats for weak and rooted weak semantics. We start, in this section, by considering branching and rooted branching bisimilarity. The idea behind the construction of these congruence formats is that the format must guarantee that a formula from the characterising logic of the equivalence under consideration is always decomposed into formulas from this same logic. We prove that the branching bisimulation format guarantees that a formula from 𝕆_{b} is always decomposed into formulas from 𝕆_{b}^{≡} (see Prop. 3). Likewise, the rooted branching bisimulation format guarantees 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, respectively).

4.1 Congruence format

We formulate a syntactic format for standard TSSs, called the rooted branching bisimulation format. The branching bisimulation format is defined by means of one simple restriction (namely, Λ is universal) on top of the rooted branching bisimulation format. Our aim for the rest of this section will be to prove that the (rooted) branching bisimulation format guarantees that (rooted) branching bisimilarity is a congruence.

We give some intuition for the conditions below, using process algebraic notations. Recall that Λ marks running processes; to maintain this marking, Λ-liquid arguments of the source and right-hand sides of premises are only allowed to occur Λ-liquid in a rule (conditions 1,2). Furthermore, since ℵ marks the processes that can execute immediately, only ℵ-liquid arguments of the source are allowed to be tested, i.e. to occur ℵ-liquid in left-hand sides of premises (condition 3). In arguments containing running processes, the rootedness property of \underline{↔}_{rb} has been lost; so in view of branching bisimilar processes like a0 and τa0 (cf. Ex. 2), ℵ∩Λ-liquid arguments of the source are not allowed to be tested in negative premises (condition 4b). Likewise, consider for example processes p and q with no other outgoing transitions then p ⟶^{τ} q, q ⟶^{τ} p, p ⟶^{a} 0 and q ⟶^{b} 0. We have p \underline{↔}_{b} a0 + b0, which implies that ℵ∩Λ-liquid arguments of the source cannot be tested multiple times in positive premises (condition 4a). Finally, in view of branching bisimilar processes like a0 and τa0, testing for τ-transitions from ℵ∩Λ-liquid arguments is only allowed when applying patience rules (condition 4c).

Definition 14. A standard ntytt rule r = \frac{H}{t⟶^{α}u} is rooted branching bisimulation safe w.r.t. ℵ and Λ if it satisfies the following conditions. Let x ∈ var(t).^{4}

1. Right-hand sides of positive premises occur only Λ-liquid in u.

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

2. If x occurs only Λ-liquid in t, then x occurs only Λ-liquid in r.

3. If x occurs only ℵ-frozen in t, then x occurs only ℵ-frozen in H.

4. If x has exactly one ℵ-liquid occurrence in t, which is also Λ-liquid, then x has at most one ℵ-liquid occurrence in H, which must be in a positive premise. If moreover this premise is labelled τ, then r must be ℵ∩Λ-patient.

Lookahead must be forbidden in view of rooted branching bisimilar processes like ab0 and aτb0. Therefore the rooted branching bisimulation format is subsumed by the ready simulation format.

Definition 15. A standard TSS is in rooted branching bisimulation format if it is in ready simulation format and, for some ℵ and Λ, it is ℵ∩Λ-patient and only contains rules that are rooted branching bisimulation safe w.r.t. ℵ and Λ.

This TSS is in branching bisimulation format if moreover Λ is universal.

Remark 2. If a standard TSS P is in rooted branching bisimulation format, then there are smallest predicates ℵ_{0} and Λ_{0} such that P is in rooted branching bisimulation format w.r.t. ℵ_{0} and Λ_{0}. Namely the Λ_{0}-liquid arguments are generated by conditions 1 and 2 of Def. 14; they are the smallest collection of arguments such that these two requirements are satisfied. Likewise the ℵ_{0}-liquid arguments are generated by condition 3, which can be read as “If x occurs ℵ-liquid in H, then the unique occurrence of x in t is ℵ-liquid.” For any standard TSS P in ready simulation format, ℵ_{0} and Λ_{0} are determined in this way, and whether P is in rooted branching bisimulation format then depends solely on whether it is ℵ_{0}∩Λ_{0}-patient, and condition 4 of Def. 14 is satisfied by all rules in P.

4.2 Preservation of syntactic restrictions

In the definition of modal decomposition, we did not use the rules from the original standard TSS P, but the P -ruloids. Therefore we must verify that if P is in rooted branching bisimulation format, then the P -ruloids are rooted branching bisimulation safe (Prop. 2). The key part of the proof is to show that the syntactic restriction of decent rooted branching bisimulation safety is preserved under irredundant provability (Lem. 5). The adjective irredundant is essential here; this preservation result would clearly fail if “junk” could be added to the premises of derived rules.

In the proofs of the preservation lemma below, rules with a negative conclusion will play an important role. For this reason, the notion of rooted branching bisimulation safety first needs to be extended to non-standard rules. In Sect. 2.5 it was explained that in the construction of P -ruloids, a non-standard rule \frac{H}{f(x_{1},...,x_{n})−̸→^{α}} is obtained by picking one premise from each standard rule with a conclusion of the form f(x_{1}, …, x_{n}) ⟶^{α} t, and including the denial of each of the selected premises as a premise in H. The following definition is tailored in such a way that applying this procedure to standard ntytt rules that are rooted branching bisimulation safe gives rise to non-standard ntytt rules that are again rooted branching bisimulation safe.

Definition 16. An ntytt rule r = \frac{H}{t−̸→^{α}} is rooted branching bisimulation safe

w.r.t. ℵ and Λ if it satisfies conditions 2 and 3 of Def. 14.^{5}

Lemma 5. Let P be a TSS in decent ntyft format, in which each transition rule is rooted branching bisimulation safe w.r.t. ℵ and Λ. Then any ntytt rule irredundantly provable from P is rooted branching bisimulation safe w.r.t. ℵ and Λ.

Proof. Let an ntytt rule \frac{H}{t⟶^{α}u} or \frac{H}{t−̸→^{α}} be irredundantly provable from P, by means of a proof π. We prove, using structural induction with respect to π, that this rule is rooted branching bisimulation safe w.r.t. ℵ and Λ.

Induction basis: Suppose π has only one node. Then \frac{H}{t⟶^{α}u} equals \frac{t⟶^{α}u}{t⟶^{α}u} (so u is a variable), or \frac{H}{t−̸→^{α}} equals \frac{t−̸→^{α}}{t−̸→^{α}}. Both rules are rooted branching bisimulation safe w.r.t. ℵ and Λ.

Induction step: Let r ∈ R be the rule and σ the substitution used at the bottom of π. By assumption, r is decent, ntyft, and rooted branching bisimulation safe w.r.t. ℵ and Λ. Let

{v_{k} ⟶^{β_{k}} y_{k} | k ∈ K} ∪ {w_{ℓ} −̸→^{γ_{ℓ}}| ℓ ∈ L}

be the set of premises of r, and

f(x_{1}, …, x_{ar(f)}) ⟶^{α} v or f(x_{1}, …, x_{ar(f)}) −̸→^{α}

the conclusion of r. Then σ(f(x_{1}, …, x_{ar(f)})) = t and, in the first case, σ(v) = u.

Moreover, rules r_{k} = _{\frac{H_{k}}{σ(v_{k})⟶^{β_{k}}σ(y_{k})}} for each k ∈ K and r_{ℓ} = _{\frac{H_{ℓ}}{σ(w_{ℓ})−̸→^{γ_{ℓ}}}} for each

ℓ ∈ L are irredundantly provable from P by means of strict subproofs of π, where H = ⋃_{k∈K} H_{k} ∪ ⋃_{ℓ∈L} H_{ℓ}.

As r is decent, var(v_{k}) ⊆ {x_{1}, …, x_{ar(f)}}, so var(σ(v_{k})) ⊆ var(t) for each k ∈ K. Likewise, var(σ(w_{ℓ})) ⊆ var(t) for each ℓ ∈ L. From rhs(H)∩var(t) = ∅ it follows that rhs(H_{k})∩var(σ(v_{k})) = ∅ for each k ∈ K, and rhs(H_{ℓ})∩var(σ(w_{ℓ})) = ∅ for each ℓ ∈ L. So for each k ∈ K and ℓ ∈ L, the rules r_{k} and r_{ℓ} are ntytt rules. By Lem. 1, they are decent. And by induction, they are rooted branching bisimulation safe w.r.t. ℵ and Λ.

We prove that \frac{H}{t⟶^{α}u} satisfies conditions 1–4 of Def. 14, and that \frac{H}{t−̸→^{α}} satisfies conditions 2 and 3 of Def. 16.

1. Consider \frac{H}{t⟶^{α}u}. Let z ∈ rhs(H). Then z ∉ var(t), so z ∉ var(σ(x_{i})) for each i ∈ {1, …, ar(f)}. As r is decent, var(v_{k}) ⊆ {x_{1}, …, x_{ar(f)}}, so z ∉ var(σ(v_{k})) for each k ∈ K. Hence, if z ∈ var(σ(y_{k_{0}})) for some k_{0} ∈ K,

5 The syntactic restrictions on non-standard rules are usually not simply a subset of the ones on standard rules; typically, requirements on positive premises become requirements on negative premises, and vice versa. See for example the failure trace format in [6].

then by the decency of r_{k_{0}}, z ∈ rhs(H_{k_{0}}). Since r_{k_{0}} is rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 1 of Def. 14, z occurs only Λliquid in σ(y_{k_{0}}). Furthermore, since r is rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 1 of Def. 14, y_{k_{0}} occurs only Λ-liquid in v. By the decency of r, var(v) ⊆ {x_{1}, …, x_{ar(f)}} ∪ {y_{k} | k ∈ K}. Concluding, z occurs only Λ-liquid in σ(v) = u.

2. Let x ∈ var(t) occur only Λ-liquid in t. Let I denote {i ∈ {1, …, ar(f)} | x ∈ var(σ(x_{i}))}. Since t = σ(f(x_{1}, …, x_{ar(f)})), for each i ∈ I, Λ(f, i) and x occurs only Λ-liquid in σ(x_{i}). Since r is rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 2 of Def. 14 or Def. 16, the x_{i} for all i ∈ I occur only Λ-liquid in r. Hence x occurs only Λ-liquid in σ(v_{k}) for all k ∈ K and in σ(w_{ℓ}) for all ℓ ∈ L. Since the r_{k} for all k ∈ K and r_{ℓ} for all ℓ ∈ L are rooted branching bisimulation safe w.r.t. ℵ and Λ, and decent, it follows using condition 2 that x occurs only Λ-liquid in these rules. (The reference to the decency of r_{k} and r_{ℓ} is needed in case x does not occur in their source.) So x occurs only Λ-liquid in H. Moreover, x occurs only Λ-liquid in σ(y_{k}) for all k ∈ K. Since r is rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 1 of Def. 14, the y_{k} for all k ∈ K occur only Λ-liquid in v. And for each i ∈ I, Λ(f, i) implies that x_{i} occurs only Λ-liquid in v. We already noted that x occurs only Λ-liquid in σ(x_{i}) for each i ∈ {1, …, ar(f)}. By the decency of r, var(v) ⊆ {x_{1}, …, x_{ar(f)}} ∪ {y_{k} | k ∈ K}. Hence x occurs only Λ-liquid in σ(v) = u. Concluding, x occurs only Λ-liquid in \frac{H}{t⟶^{α}u} or

\frac{H}{t−̸→^{α}}.

3. Suppose that x occurs only ℵ-frozen in t. Then, for each i ∈ {1, …, ar(f)}, either ¬ℵ(f, i), or x occurs only ℵ-frozen in σ(x_{i}). In the first case, since r is rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 3 of Def. 14 or Def. 16, x_{i} occurs only ℵ-frozen in v_{k} for all k ∈ K and w_{ℓ} for all ℓ ∈ L. So x occurs only ℵ-frozen in σ(v_{k}) for all k ∈ K and σ(w_{ℓ}) for all ℓ ∈ L. Since r_{k} for all k ∈ K and r_{ℓ} for all ℓ ∈ L are rooted branching bisimulation safe w.r.t. ℵ and Λ, and decent, it follows using conditions 3 of Def. 14 and Def. 16 that x occurs only ℵ-frozen in H.

4. Consider \frac{H}{t⟶^{α}u}. Suppose that x has exactly one ℵ-liquid occurrence in t, which is also Λ-liquid. Then there is an i_{0} ∈ {1, …, ar(f)} with ℵ(f, i_{0}) and Λ(f, i_{0}) such that x has exactly one ℵ-liquid occurrence in σ(x_{i_{0}}), which is also Λ-liquid. Furthermore, for each i ∈ {1, …, ar(f)}\{i_{0}}, either ¬ℵ(f, i), or x occurs only ℵ-frozen in σ(x_{i}). Since r is rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 3 of Def. 14, if ¬ℵ(f, i), then x_{i} occurs only ℵ-frozen in v_{k} for all k ∈ K, as well as in w_{ℓ} for all ℓ ∈ L. And by condition 4 of Def. 14, there is a K′ ⊆ K containing at most one element such that x_{i_{0}} has exactly one ℵ-liquid occurrence in v_{k} if k ∈ K′, and occurs only ℵ-frozen in v_{k} for all k ∈ K\K′, as well as in w_{ℓ} for all ℓ ∈ L. Moreover, by condition 2 of Def. 14, the unique ℵ-liquid occurrence of x_{i_{0}} in v_{k} must be Λ-liquid. Hence x has exactly one ℵ-liquid occurrence in σ(v_{k}) if k ∈ K′, which is also Λ-liquid, and occurs only ℵ-frozen in σ(v_{k}) for all k ∈ K\K′, as well as in w_{ℓ} for all ℓ ∈ L. Since the r_{k} for all k ∈ K and r_{ℓ} for all ℓ ∈ L are rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 4 of Def. 14, x has at most one ℵ-liquid occurrence in (the left-hand side of) one premise in H_{k}, which must be positive, if k ∈ K′. And by conditions 3 of Def. 14 and Def. 16, x occurs only ℵ-frozen in the premises in H_{k} for all k ∈ K\K′, and in those in H_{ℓ} for all ℓ ∈ L. Concluding, since H = ⋃_{k∈K} H_{k} ∪⋃_{ℓ∈L} H_{ℓ}, and K′ contains at most one element, x has at most one ℵ-liquid occurrence in (the left-hand side of) one premise in H, which must be positive. Suppose that x has an ℵ-liquid occurrence in a positive premise in H with label τ. Then clearly K′ = {k_{0}}, where x has exactly one ℵ-liquid occurrence in σ(v_{k_{0}}), which is also Λ-liquid, and in a positive premise in H_{k_{0}} with label τ. Since r_{k_{0}} = _{\frac{H_{k_{0}}}{σ(v_{k_{0}} )⟶^{β_{k_{0}}}σ(y_{k_{0}} )}} is rooted branching bisimulation safe w.r.t. ℵ and

Λ, by condition 4 of Def. 14, r_{k_{0}} must be ℵ∩Λ-patient. In particular, β_{k_{0}} = τ. Since moreover ℵ∩Λ(f, i_{0}), x_{i_{0}} has an ℵ∩Λ-liquid occurrence in v_{k_{0}}, and r is rooted branching bisimulation safe w.r.t. ℵ and Λ, by condition 4 of Def. 14, r must be an ℵ∩Λ-patience rule. This implies that K = {k_{0}} and L = ∅; so H = H_{k_{0}}. It follows that \frac{H}{t⟶^{α}u} is ℵ∩Λ-patient.

Hence \frac{H}{t⟶^{α}u} or \frac{H}{t−̸→^{α}} is rooted branching bisimulation safe w.r.t. ℵ and Λ. ⊓ ⊔

Proposition 2. Let P be a TSS in ready simulation format, in which each transition rule is rooted branching bisimulation safe w.r.t. ℵ and Λ. Then each P -ruloid is rooted branching bisimulation safe w.r.t. ℵ and Λ.

Proof. We recall from Sect. 2.5, that the standard TSS P can be transformed into a TSS P^{+} in decent ntyft format; the P -ruloids are those decent nxytt rules that are irredundantly provable from P^{+}.

As the rules of P are rooted branching bisimulation safe w.r.t. ℵ and Λ, then so are the rules in P^{+}. Namely, as described in Sect. 2.5, the rules in P^{+} are constructed in three steps. The first step (the conversion of P to decent ntyft format) clearly preserves the rooted branching bisimulation format. The second step (the construction to reduce left-hand sides of positive premises to variables) yields an intermediate TSS, all of whose rules are irredundantly provable from P, and thus is covered by Lem. 5. Regarding the final step (constructing nonstandard rules with negative conclusions), as said before Def. 16, this definition is tailored in such a way that applying this procedure to standard ntytt rules that are rooted branching bisimulation safe gives rise to non-standard ntytt rules that are again rooted branching bisimulation safe.

Since the rules in P^{+} are rooted branching bisimulation safe w.r.t. ℵ and Λ, by Lem. 5, each P -ruloid is rooted branching bisimulation safe w.r.t. ℵ and Λ. ⊓ ⊔

4.3 Preservation of modal characterisations

Consider a standard TSS in rooted branching bisimulation format, w.r.t. some ℵ and Λ. Def. 13 yields decomposition mappings ψ ∈ t^{−1}(φ), with Γ := ℵ∩Λ.

In this section we will first prove that if φ ∈ 𝕆_{b}, then ψ(x) ∈ 𝕆_{b}^{≡} if x occurs only Λ-liquid in t. (That is why in the branching bisimulation format, Λ must be universal.) Next we will prove that if φ ∈ 𝕆_{rb}, then ψ(x) ∈ 𝕆_{rb}^{≡} for all variables x. From these preservation results we will, in Sect. 4.4, deduce the promised congruence results for branching bisimilarity and rooted branching bisimilarity, respectively.

Proposition 3. Let P be an ℵ∩Λ-patient standard TSS in ready simulation format, in which each transition rule is rooted branching bisimulation safe w.r.t. ℵ and Λ. For any term t and variable x that occurs only Λ-liquid in t:

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

Proof. We apply simultaneous induction on the structure of φ ∈ 𝕆_{b} and the construction of ψ. Let ψ ∈ t^{−1}(φ), and let x occur only Λ-liquid in t. First we treat the case where t is univariate. If x∉var(t), then by Lem. 2, ψ(x)≡⊤∈𝕆_{b}^{≡}. So suppose x has exactly one, Λ-liquid occurrence in t.

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

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

– φ = ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b}. According to Def. 13.4, we can distinguish two cases. Case 1: ψ(x) is defined on the basis of Def. 13.4a. Then ψ(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. 13.1, χ(x) = χ_{1}(x)∧χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨τ̂⟩φ_{2}). By induction on formula size, χ_{1}(x) ∈ 𝕆_{b}^{≡}. For χ_{2}(x), according to Def. 13.5, we can distinguish three cases.

Case 1.1: χ_{2}(x) is defined on the basis of Def. 13.5a. Then χ_{2} ∈ t^{−1}(φ_{2}). By induction on formula size, χ_{2}(x) ∈ 𝕆_{b}^{≡}. Since ψ(x) is of the form ⟨ϵ⟩(χ_{1}(x) ∧ χ_{2}(x)) or χ_{1}(x) ∧ χ_{2}(x), it follows that ψ(x) ∈ 𝕆_{b}^{≡}.

Case 1.2: χ_{2}(x) is defined on the basis of Def. 13.5b. Then x_{0} occurs ℵ∩Λliquid in t, and either χ_{2}(x)=⟨τ̂⟩ξ(x) and x occurs ℵ-liquid in t (if x=x_{0}) or χ_{2}(x) = ξ(x), for some ξ ∈ t^{−1}(φ_{2}). By induction on formula size, ξ(x) ∈ 𝕆_{b}^{≡}. Since ψ(x) is of the form ⟨ϵ⟩(χ_{1}(x)⟨τ̂⟩ξ(x)), ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x)) or χ_{1}(x) ∧ ξ(x), it follows that ψ(x) ∈ 𝕆_{b}^{≡}.

Case 1.3: χ_{2}(x) is defined on the basis of Def. 13.5c, employing an ℵ∩Λimpatient P -ruloid \frac{H}{t⟶^{τ}u} and a ξ ∈ u^{−1}(φ_{2}). So

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

By Prop. 2, \frac{H}{t⟶^{τ}u} is rooted branching bisimulation safe. Since the occurrence of x in t is Λ-liquid, by condition 2 of Def. 14, x occurs only Λ-liquid in u. Therefore, by induction on formula size, ξ(x) ∈ 𝕆_{b}^{≡}.

Case 1.3.1: The occurrence of x in t is ℵ-frozen. By condition 3 of Def. 14,

x does not occur in H. Hence χ_{2}(x) = ξ(x) ∈ 𝕆_{b}^{≡} and thus ψ(x) ∈ 𝕆_{b}^{≡}. Case 1.3.2: The occurrence of x in t is ℵ-liquid. By condition 4 of Def. 14,

H has at most one premise of the form x ⟶^{β} y, for which β ≠ τ, and none of the form x −̸→^{γ}. Thus either χ_{2}(x) = ξ(x)—and we are done— or χ_{2}(x) = ξ(x)⟨b⟩ξ(y) with b ∈ A and x ⟶^{b} y ∈ H. In the latter case ψ(x) ≡ ⟨ϵ⟩((χ_{1}(x) ∧ ξ(x))⟨b⟩ξ(y)). By condition 1 of Def. 14, y occurs only Λ-liquid in u, so by induction ξ(y) ∈ 𝕆_{b}^{≡}. It follows that ψ(x) ∈ 𝕆_{b}^{≡}.

Case 2: ψ(x) is defined on the basis of Def. 13.4b, employing an ℵ∩Λimpatient P -ruloid \frac{H}{t⟶^{τ}u} and a χ ∈ u^{−1}(⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2})). By Prop. 2, \frac{H}{t⟶^{τ}u} is rooted branching bisimulation safe. Since the occurrence of x in t is Λliquid, by condition 2 of Def. 14, x occurs only Λ-liquid in u. Therefore, by induction on the construction of ψ, χ(x) ∈ 𝕆_{b}^{≡}.

Case 2.1: The occurrence of x in t is ℵ-frozen. Then

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

By condition 3 of Def. 14, x does not occur in H. So ψ(x) = χ(x) ∈ 𝕆_{b}^{≡}. Case 2.2: The occurrence of x in t is ℵ-liquid. Then

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

By condition 4 of Def. 14, H has at most one premise of the form x ⟶^{β} y, for which β ≠ τ, and none of the form x −̸→^{γ}. Thus either ψ(x) = ⟨ϵ⟩χ(x)—and we are done—or ψ(x) = ⟨ϵ⟩χ(x)⟨b⟩χ(y) with b ∈ A and x ⟶^{b} y ∈ H. By condition 1 of Def. 14, y occurs only Λ-liquid in u, so by induction χ(y) ∈ 𝕆_{b}^{≡}. It follows that ψ(x) ∈ 𝕆_{b}^{≡}.

– φ = ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b}. According to Def. 13.4, we can distinguish two cases. Case 1: ψ(x) is defined on the basis of Def. 13.4a. Then ψ(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. 13.1, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨a⟩φ_{2}). By induction on formula size, χ_{1}(x) ∈ 𝕆_{b}^{≡}. And by Def. 13.3,

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

for some P -ruloid \frac{H}{t⟶^{a}u} and ξ ∈ u^{−1}(φ_{2}). By Prop. 2, \frac{H}{t⟶^{a}u} is rooted branching bisimulation safe w.r.t. ℵ and Λ. Since the occurrence of x in t is Λ-liquid, by condition 2 of Def. 14, x occurs only Λ-liquid in u. Moreover, by condition 1 of Def. 14, variables in rhs(H) occur only Λliquid in u. So by induction on formula size, ξ(x) ∈ 𝕆_{b}^{≡}, and ξ(y) ∈ 𝕆_{b}^{≡} for x ⟶^{β} y ∈ H. We distinguish two cases.

Case 1.1: The occurrence of x in t is ℵ-liquid. Then ψ(x) = ⟨ϵ⟩(χ_{1}(x) ∧ χ_{2}(x)). The rule \frac{H}{t⟶^{a}u} is rooted branching bisimulation safe w.r.t. ℵ and Λ, and an nxytt rule. By condition 4 of Def. 14, x is the left-hand side of at most one premise in H, which must be positive. Hence either χ_{2}(x) = ξ(x), or χ_{2}(x) = ξ(x)⟨β⟩ξ(y) with x ⟶^{β} y ∈ H. Since a ≠ τ, by condition 4 of Def. 14, β ≠ τ. Since ψ(x) is of the form ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x)) or ⟨ϵ⟩((χ_{1}(x) ∧ ξ(x))⟨β⟩ξ(y)), it follows that ψ(x) ∈ 𝕆_{b}^{≡}.

Case 1.2: The occurrence of x in t is ℵ-frozen. Then ψ(x) = χ_{1}(x) ∧ χ_{2}(x). The rule \frac{H}{t⟶^{a}u} is rooted branching bisimulation safe w.r.t. ℵ and Λ, and an nxytt rule. By condition 3 of Def. 14, x does not occur in H. So χ_{2}(x) = ξ(x), and thus ψ(x) = χ_{1}(x) ∧ ξ(x) ∈ 𝕆_{b}^{≡}.

Case 2: ψ(x) is defined on the basis of Def. 13.4b. This case proceeds in the same way as case 2 of φ = ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}).

Finally, suppose t is not univariate. Then t = σ(u) for some univariate term u and σ : var(u) → V not injective. By Def. 13.6, ψ(x) = ⋀_{z∈σ^{−1}(x)} χ(z) for some χ ∈ u^{−1}(φ). Since u is univariate, and for each z ∈ σ^{−1}(x) the occurrence in u is Λ-liquid, χ(z) ∈ 𝕆_{b}^{≡} for all z ∈ σ^{−1}(x). Hence ψ(x) ∈ 𝕆_{b}^{≡}. ⊓ ⊔

Proposition 4. Let P be an ℵ∩Λ-patient standard TSS in ready simulation format, in which each transition rule is rooted branching bisimulation safe w.r.t. ℵ and Λ. For any term t and variable x:

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

Proof. We apply simultaneous induction on the structure of φ ∈ 𝕆_{rb} and the construction of ψ. Let ψ ∈ 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 by Lem. 2, ψ(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. 13.3,

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

for some P -ruloid \frac{H}{t⟶^{α}u} and χ ∈ u^{−1}(φ′). By induction on formula size, χ(x) ∈ 𝕆_{rb}^{≡}. (Induction may be applied because φ′ ∈ 𝕆_{b} ⊆ 𝕆_{rb}.) By Prop. 2, \frac{H}{t⟶^{α}u} is rooted branching bisimulation safe w.r.t. ℵ and Λ, so by condition 1 of Def. 14, variables in rhs(H) occur only Λ-liquid in u. Hence by Prop. 3, χ(y) ∈ 𝕆_{b}^{≡}, and thus ⟨β⟩χ(y) ∈ 𝕆_{rb}^{≡}, for all x ⟶^{β} y ∈ H. Moreover, ¬⟨γ⟩⊤ ∈

𝕆_{rb}^{≡} for all x −̸→^{γ}∈ H. Hence ψ(x) ∈ 𝕆_{rb}^{≡}.

– φ ∈ 𝕆_{b}. The cases φ = ⋀_{i∈I} φ_{i} and φ = ¬φ′ proceed as in the proof of Prop. 3. We therefore focus on the other two cases. 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.

∗ φ = ⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b}. According to Def. 13.4, we can distinguish two cases. Case 1: ψ(x) is defined on the basis of Def. 13.4a. Then, since x occurs Λ-

frozen in t, ψ(x) = χ(x) for some χ ∈ t^{−1}(φ_{1}⟨τ̂⟩φ_{2}). By Def. 13.1, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨τ̂⟩φ_{2}). By induction on formula size, χ_{1}(x) ∈ 𝕆_{rb}^{≡}. So to prove ψ(x) ∈ 𝕆_{rb}^{≡}, it suffices to prove χ_{2}(x) ∈ 𝕆_{rb}^{≡}. According to Def. 13.5, we can distinguish three cases.

Case 1.1: χ_{2}(x) is defined on the basis of Def. 13.5a. Then χ_{2} ∈ t^{−1}(φ_{2}).

By induction on formula size, χ_{2}(x) ∈ 𝕆_{rb}^{≡}. Case 1.2: χ_{2}(x) is defined on the basis of Def. 13.5b. Then, since x occurs

Λ-frozen in t, χ_{2}(x) = ξ(x) for some ξ ∈ t^{−1}(φ_{2}). By induction on formula size, χ_{2}(x) = ξ(x) ∈ 𝕆_{rb}^{≡}.

Case 1.3: χ_{2}(x) is defined on the basis of Def. 13.5c. Then χ_{2}(x) ∈ 𝕆_{rb}^{≡} follows in exactly the same way as ψ(x) ∈ 𝕆_{rb}^{≡} in the case φ = ⟨α⟩φ′ of this proof.

Case 2: ψ(x) is defined on the basis of Def. 13.4b, using a P -ruloid \frac{H}{t⟶^{τ}u} and a χ ∈ u^{−1}(⟨ϵ⟩(φ_{1}⟨τ̂⟩φ_{1})). As the occurrence of x in t is Λ-frozen,

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

By induction on the construction of ψ, χ(x) ∈ 𝕆_{b}^{≡}. The rest of the argument proceeds as in the case φ = ⟨α⟩φ′ above.

∗ φ = ⟨ϵ⟩(φ_{1}⟨a⟩φ_{2}) with φ_{1}, φ_{2} ∈ 𝕆_{b}. According to Def. 13.4, we can distinguish two cases. Case 1: ψ(x) is defined on the basis of Def. 13.4a. Then, since x occurs Λ-

frozen in t, ψ(x) = χ(x) for some χ ∈ t^{−1}(φ_{1}⟨a⟩φ_{2}). By Def. 13.1, χ(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) ∈ 𝕆_{rb}^{≡}. So ψ(x) ∈ 𝕆_{rb}^{≡}.

Case 2: ψ(x) is defined on the basis of Def. 13.4b. This case proceeds in the same way as case 2 of φ = ⟨ϵ⟩φ_{1}⟨τ̂⟩φ_{2}. ⊓ ⊔

4.4 Congruence results

Now we are in a position to prove the promised congruence results for \underline{↔}_{b} and \underline{↔}_{rb}.

Theorem 3. Let P be a complete standard TSS in branching bisimulation format. Then \underline{↔}_{b} is a congruence for P.

Proof. Let ρ, ρ′ be closed substitutions and t a term. Suppose that ρ(x)\underline{↔}_{b} ρ′(x) for all x ∈ var(t); we need to prove that then ρ(t)\underline{↔}_{b} ρ′(t).

By Def. 15 each transition rule in P is rooted branching bisimulation safe w.r.t some ℵ and the universal predicate Λ, and P is ℵ∩Λ-patient and in ready simulation format. Let ρ(t) ⊧ φ ∈ 𝕆_{b}. By Thm. 2, taking Γ := ℵ∩Λ, there is a ψ ∈ t^{−1}(φ) with ρ(x) ⊧ ψ(x) for all x ∈ var(t). Since x occurs Λ-liquid in t (because Λ is universal), by Prop. 3, ψ(x) ∈ 𝕆_{b}^{≡} for all x ∈ var(t). By Thm. 1, ρ(x) \underline{↔}_{b} ρ′(x) implies ρ(x) ∼_{𝕆_{b}^{≡}} ρ′(x) for all x ∈ var(t). So ρ′(x) ⊧ ψ(x) for all x ∈ var(t). Therefore, by Thm. 2, ρ′(t) ⊧ φ. Likewise, ρ′(t) ⊧ φ ∈ 𝕆_{b} implies ρ(t) ⊧ φ. So ρ(t) ∼_{𝕆_{b}} ρ′(t). Hence, by Thm. 1, ρ(t)\underline{↔}_{b} ρ′(t). ⊓ ⊔

We can follow the same approach to prove that the rooted branching bisimulation format guarantees that \underline{↔}_{rb} is a congruence.

Theorem 4. Let P be a complete standard TSS in rooted branching bisimulation format. Then \underline{↔}_{rb} is a congruence for P.

The proof is similar to the one of Thm. 3, except that Prop. 4 is applied instead of Prop. 3; therefore x needs not occur Λ-liquid in t, which is why universality of Λ can be dropped.

5 η-Bisimilarity as a Congruence

We now proceed to derive a congruence format for rooted η-bisimilarity. This format can be formulated by adding one extra syntactic restriction to the rooted branching bisimulation format. The proofs that the resulting format is preserved under the transformation to ruloids, and that it guarantees that rooted η-bisimilarity is a congruence, are for a large part similar to these proofs for the rooted branching bisimulation format. We will therefore only explain how these proofs deviate from the proofs for the rooted branching bisimulation format.

The notion of rooted η-bisimulation safeness is obtained by strengthening condition 1 in the definition of rooted branching bisimulation safeness. The action refinement operator exemplifies that this strengthening is essential; see Sect. 6.6.

Definition 17. A standard ntytt rule r = \frac{H}{t⟶^{α}u} is rooted η-bisimulation safe w.r.t. ℵ and Λ if it satisfies conditions 2–4 of Def. 14, together with:

1′. Right-hand sides of positive premises occur only \underline{ℵ∩Λ}-liquid in u.

Definition 18. A standard TSS is in rooted η-bisimulation format if it is in ready simulation format and, for some ℵ and Λ, it is ℵ∩Λ-patient and contains only rules that are rooted η-bisimulation safe w.r.t. ℵ and Λ.

This TSS is in η-bisimulation format if moreover Λ is universal.

For non-standard ntytt rules, the notion of rooted η-bisimulation safeness coincides with the notion of rooted branching bisimulation safeness (see Def. 16).

Lemma 6. Let P be a TSS in decent ntyft format, in which each transition rule is rooted η-bisimulation safe w.r.t. ℵ and Λ. Then any ntytt rule irredundantly provable from P is rooted η-bisimulation safe w.r.t. ℵ and Λ.

Proof. Since rooted η-bisimulation safeness is stricter than rooted branching bisimulation safeness, preservation of conditions 2–4 of rooted η-bisimulation safeness follows directly from Lem. 5.

We only need to prove that condition 1′ of Def. 17 is preserved. For this, the part within the proof of Lem. 5 that is devoted to the preservation of condition 1 in Def. 14 can be copied almost literally. The only difference is that to obtain a preservation proof for condition 1′, the three occurrences of “Λ-liquid” in the preservation proof for condition 1 have to be replaced by “ℵ∩Λ-liquid”. ⊓ ⊔

Now the following proposition can be proved in the same way as the corresponding Prop. 2 for the rooted branching bisimulation format.

Proposition 5. Let P be a TSS in ready simulation format, in which each transition rule is rooted η-bisimulation safe w.r.t. ℵ and Λ. Then each P -ruloid is rooted η-bisimulation safe w.r.t. ℵ and Λ.

Proposition 6. Let P be an ℵ∩Λ-patient standard TSS in ready simulation format, in which each transition rule is rooted η-bisimulation safe w.r.t. ℵ and Λ. For any term t and variable x that occurs only Λ-liquid in t:

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

Proof. Again, the proof is very similar to the proof of the corresponding Prop. 3 for the rooted branching bisimulation format. We spell out (part of) the only two cases where the proofs really differ. The differences are underlined. It is here that the stronger condition 1′ will be needed. We recall that it is assumed that t is univariate, and that x has exactly one, Λ-liquid occurrence in t.

– φ = ⟨ϵ⟩\underline{φ′} with φ′ ∈𝕆_{η}. According to Def. 13.4, we can distinguish two cases.

Case 1: ψ(x) is defined on the basis of Def. 13.4a.

Then either ψ(x) = ⟨ϵ⟩χ(x) or ψ(x) = χ(x) for some χ ∈ t^{−1}(φ′).

By induction on formula size, χ(x) ∈ 𝕆_{η}^{≡}. So ψ(x) ∈ 𝕆_{η}^{≡}.

Case 2 proceeds as in the proof of Prop. 3 (in that proof the two occurrences of “Case 2” proceed in the same way). However, Case 2.2 now ends by: By condition \underline{1′ of Def. 17}, y occurs only \underline{ℵ∩Λ}-liquid in u, so by induction χ(y) ∈ 𝕆_{η}^{≡}, \underline{and according to Lem. 4, χ(y) ≡ ⟨ϵ⟩χ(y).} It follows that ψ(x) ∈ 𝕆_{η}^{≡}.

– φ = ⟨ϵ⟩φ_{1}⟨a⟩\underline{⟨ϵ⟩}φ_{2} with φ_{1}, φ_{2} ∈ 𝕆_{η}. According to Def. 13.4, we can distinguish two cases. Case 1: ψ(x) is defined on the basis of Def. 13.4a. Then ψ(x) = ⟨ϵ⟩χ(x) if x occurs ℵ-liquid in t, or ψ(x) = χ(x) if x occurs ℵ-frozen in t, for some χ ∈ t^{−1}(φ_{1}⟨a⟩\underline{⟨ϵ⟩}φ_{2}). By Def. 13.1, χ(x) = χ_{1}(x) ∧ χ_{2}(x) with χ_{1} ∈ t^{−1}(φ_{1}) and χ_{2} ∈ t^{−1}(⟨a⟩\underline{⟨ϵ⟩}φ_{2}). By induction on formula size, χ_{1}(x) ∈ 𝕆_{η}^{≡}. And by Def. 13.3,

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

for some P -ruloid \frac{H}{t⟶^{a}u} and ξ ∈ u^{−1}(\underline{⟨ϵ⟩}φ_{2}). By Prop. 5, \frac{H}{t⟶^{a}u} is rooted η-bisimulation safe w.r.t. ℵ and Λ. Since the occurrence of x in t is Λliquid, by condition 2 of Def. 14, x occurs only Λ-liquid in u. Moreover, \underline{by condition 1′ of Def. 17}, variables in rhs(H) occur only \underline{ℵ∩Λ}-liquid in u. So by induction on formula size, ξ(x) ∈ 𝕆_{η}^{≡}, and ξ(y) ∈ 𝕆_{η}^{≡} for each x ⟶^{β} y ∈ H. \underline{According to Lem. 4, ξ(y) ≡ ⟨ϵ⟩ξ(y).} We distinguish two cases.

Case 1.1: The occurrence of x in t is ℵ-liquid. Then ψ(x) = ⟨ϵ⟩(χ_{1}(x) ∧ χ_{2}(x)). The rule \frac{H}{t⟶^{a}u} is rooted η-bisimulation safe w.r.t. ℵ and Λ, and an nxytt rule. By condition 4 of Def. 14, x is the left-hand side of at most one premise in H, which must be positive. Hence either χ_{2}(x) = ξ(x), or χ_{2}(x) = ξ(x)⟨β⟩ξ(y) with x ⟶^{β} y ∈ H. Since a ≠ τ, by condition 4 of Def. 14, β ≠ τ. Since ψ(x) is of the form ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x)) or ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x))⟨β⟩ξ(y) \underline{≡ ⟨ϵ⟩(χ_{1}(x) ∧ ξ(x))⟨β⟩⟨ϵ⟩ξ(y)}, it follows that ψ(x) ∈ 𝕆_{η}^{≡}.

Case 1.2 and case 2 proceed as in the proof of Prop. 3. ⊓ ⊔

Proposition 7. Let P be an ℵ∩Λ-patient standard TSS in ready simulation format, in which each transition rule is rooted η-bisimulation safe w.r.t. ℵ and Λ. For any term t and variable x:

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

Proof. Again, the proof is very similar to the proof of the corresponding Prop. 4 for the rooted branching bisimulation format. As in the previous proof, the only real difference is that we have to exploit the stronger condition 1′ of Def. 17: for each P -ruloid \frac{H}{t⟶^{α}u}, each y ∈ rhs(H) can occur only ℵ∩Λ-liquid in u; so by Lem. 4, if χ ∈ u^{−1}(⟨ϵ⟩φ), then χ(y) ≡ ⟨ϵ⟩χ(y). Moreover, we need to observe that ¬⟨γ⟩⊤ ≡ ¬⟨γ⟩⟨ϵ⟩⊤ ∈ 𝕆_{rη}. ⊓ ⊔

The proofs of the following congruence theorems for (rooted) η-bisimulation are omitted, as they are almost identical to the proofs of the corresponding congruence theorems for (rooted) branching bisimilarity.

Theorem 5. Let P be a complete standard TSS in η-bisimulation format. Then \underline{↔}_{η} is a congruence for P.

Theorem 6. Let P be a complete standard TSS in rooted η-bisimulation format. Then \underline{↔}_{rη} is a congruence for P.

6 Examples

In this section we present some applications of our congruence formats, as well as some counterexamples to show the need for the requirements in our congruence formats.

6.1 Basic process algebra

Basic process algebra BPA [4] 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}. In addition to τ, we assume two special constants outside Act: ε represents successful termination, while the deadlock δ does not display any behaviour. These intuitions are made precise by means of the transition rules for BPA_{εδτ} presented below. In these rules, ℓ ranges over Act ∪ {τ}, and α over Act ∪ {τ, √}.

\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_{1} x_{2} ⟶^{α} y_{2}}{x_{1}·x_{2} ⟶^{α} y_{2}} \end{matrix}

The TSS above is in ready simulation format: it consists of ntyft rules that do not contain lookahead. In view of condition 1 of Def. 14, we make the first argument of sequential composition Λ-liquid, and the two arguments of alternative composition and the second argument of sequential composition Λ-frozen. This is in line with the intuition that Λ-liquid arguments can contain running processes. The two rules for sequential composition clearly satisfy condition 2 of Def. 14: the variable x_{1} only occurs Λ-liquid in both rules. We make the two arguments of both alternative and sequential composition ℵ-liquid, because these four arguments can all start executing immediately (in the case of the second argument of sequential composition this is due to the presence of ε). Since all arguments of function symbols are ℵ-liquid, condition 3 of Def. 14 is satisfied trivially. Finally, condition 4 of Def. 14 needs to be checked for the two rules for sequential composition, as the first argument of this operator is ℵ∩Λ-liquid. In both rules, x_{1} has only one ℵ-liquid occurrence in the premises, and this occurrence is in a positive premise. In the second rule for sequential composition, the label of this premise is √ ≠ τ. In the first rule, if ℓ = τ, then this is the patience rule for the first argument of sequential composition. Concluding, the TSS for BPA_{εδτ} is in rooted branching bisimulation format.

The rules also satisfy the strengthened condition 1′ of Def. 17. So the TSS for BPA_{εδτ} is in rooted η-bisimulation format.

Corollary 1. \underline{↔}_{rb} and \underline{↔}_{rη} are congruences for BPA_{εδτ}.

6.2 Recursion

Given a signature Σ, a recursive specification E is a finite set of equations {X_{i} = t_{i} | i = 1, …, n}, where the X_{i} are recursion variables, and the t_{i} are open terms over Σ, with possible occurrences of recursion variables. Intuitively, the syntactic construct ⟨X|E⟩ denotes a solution of X with respect to E. The precise meaning of this construct is given by the transition rules for recursion below, which originate from [16]. The expression E in these rules represents a recursive specification, which contains an equation X = t. Furthermore, ⟨t|E⟩ denotes the term t with occurrences of recursion variables Y replaced by ⟨Y |E⟩. We consider the expressions ⟨X|E⟩ as constants.

\frac{⟨t|E⟩ ⟶^{α} y}{⟨X|E⟩ ⟶^{α} y}

The resulting TSS is in rooted η-bisimulation format.

Corollary 2. \underline{↔}_{rb} and \underline{↔}_{rη} are congruences for BPA_{εδτ} extended with recursion constants ⟨X|E⟩.

6.3 Replication

Let γ : Act ×Act ⇀ Act be a partial communication function, normally required to be commutative and associative. Then the ACP parallel composition [4] is given by the following rules, where ℓ ranges over Act ∪ {τ}, and a, b over Act.

\frac{x_{1} ⟶^{ℓ} y}{x_{1}∥x_{2} ⟶^{ℓ} y∥x_{2}}  \frac{x_{2} ⟶^{ℓ} y}{x_{1}∥x_{2} ⟶^{ℓ} x_{1}∥y}

\frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{b} y_{2}}{x_{1}∥x_{2} ⟶^{γ(a,b)} y_{1}∥y_{2}} (γ(a, b) defined)  \frac{x_{1} ⟶^{√} y_{1} x_{2} ⟶^{√} y_{2}}{x_{1}∥x_{2} ⟶^{√} y_{1}∥y_{2}}

Here γ(a, b) is defined if the actions a and b can communicate, say because one of them is a send action and the other a corresponding receive action. In that case γ(a, b) ∈ Act is the action that results from the synchronisation of a and b.

The arguments of ∥ need to be chosen Λ-liquid as well as ℵ-liquid. The TSS for BPA_{εδτ} augmented with parallel composition is in rooted η-bisimulation format, so \underline{↔}_{rb} and \underline{↔}_{rη} are congruences for this TSS. If we leave out the operators for alternative and sequential composition, the resulting TSS is even in η-bisimulation format, and also \underline{↔}_{b} and \underline{↔}_{η} become congruences.

The following unary replication operator ! stems from the π-calculus [29]. Intuitively it can be regarded as a parallel composition of infinitely many copies of its argument process.

\frac{x∥!x ⟶^{ℓ} y}{!x ⟶^{ℓ} y}

The argument of ! is Λ-frozen and ℵ-liquid, and the rule is in rooted η-bisimulation format.

Corollary 3. \underline{↔}_{rb} and \underline{↔}_{rη} are congruences for BPA_{εδτ} with parallel composition and replication.

We have included this example because it requires a non-variable term in the premise of its rule. It is tempting to rewrite the rule above as

\frac{x ⟶^{ℓ} y}{!x ⟶^{ℓ} y∥!x}

but this would not capture initial communications between two copies of the replicated process.

6.4 Binary Kleene star

The binary Kleene star t_{1}^{∗}t_{2} [25] 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_{εδτ}.

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

We take the arguments of the binary Kleene star to be Λ-frozen (they do not contain running processes) and ℵ-liquid (they can start executing immediately). The resulting TSS is in rooted η-bisimulation format.

Corollary 4. \underline{↔}_{rb} and \underline{↔}_{rη} are congruences for BPA_{εδτ} with the binary Kleene star.

6.5 Initial priority

Initial priority is a unary function that assumes an ordering on 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 first rule for the initial priority operator below, which is added to the rules for BPA_{εδτ}.

\frac{x ⟶^{ℓ} y  x −̸→^{ℓ′} for all ℓ′ > ℓ}{θ(x) ⟶^{ℓ} y}  \frac{x ⟶^{√} y}{θ(x) ⟶^{√} y}

We take the argument of initial priority to be Λ-frozen (it does not contain running processes) and ℵ-liquid (it can start executing immediately). The resulting TSS is in rooted η-bisimulation format.

Corollary 5. \underline{↔}_{rb} and \underline{↔}_{rη} are congruences for BPA_{εδτ} with initial priority.

Initial priority is derived from the priority operator Θ [1]: in Θ(t) all transitions of t (so not only the initial ones) are blocked by simultaneous transitions of t with a greater label.

\frac{x ⟶^{ℓ} y  x −̸→^{ℓ′} for all ℓ′ > ℓ}{Θ(x) ⟶^{ℓ} Θ(y)}  \frac{x ⟶^{√} y}{Θ(x) ⟶^{√} y}

Consider the first rule above. In view of the target Θ(y), by condition 1 of Def. 14, the argument of Θ must be chosen Λ-liquid. And in view of condition 3 of Def. 14, the argument of Θ must be chosen ℵ-liquid. The ℵ∩Λ-liquid argument x occurs ℵ-liquid in the negative premise, which violates condition 4 of Def. 14. In general, the priority operator Θ does not preserve rooted branching bisimilarity (cf. [32, pp. 130–132]).

6.6 Action refinement

The binary action refinement operator t_{1}[b ⇝ t_{2}], for some b∈Act, replaces each b-transition in t_{1} by the behaviour of t_{2}.

\frac{x_{1} ⟶^{α} y}{x_{1}[b ⇝ x_{2}] ⟶^{α} y[b ⇝ x_{2}]} (α ≠ b) \frac{x_{1} ⟶^{b} y_{1} x_{2} ⟶^{ℓ} y_{2}}{x_{1}[b ⇝ x_{2}] ⟶^{ℓ} y_{2}·(y_{1}[b ⇝ x_{2}])}

Note that an initial successful termination of t_{2} is ignored, as else we would get a transition rule with lookahead, which would violate the rooted branching bisimulation format.

For the second rule of action refinement to be rooted branching bisimulation safe, it is essential that the second argument of sequential composition is Λliquid, for else it would violate condition 1 of Def. 14. But then, since in BPA_{εδτ}

this argument is also ℵ-liquid, the rule \frac{x_{1}⟶^{√}y_{1} x_{2}⟶^{τ}y_{2}}{x_{1}·x_{2}⟶^{τ}y_{2}} violates condition 4 of Def. 14. Namely, the occurrence of x_{2} in the source is at an ℵ∩Λ-position, and x_{2} occurs at an ℵ-liquid position in a positive premise with the label τ, but this is not an ℵ∩Λ-patience rule. Thus the TSS for BPA_{εδτ} with the rules for action refinement above is not in rooted branching bisimulation format. And it should not be, as \underline{↔}_{rb} is not a congruence for this process algebra, due to the presence of the empty process. For example, b·(τ·c) \underline{↔}_{rb} b·c, but the terms b·(τ·c)[b ⇝ b·(d·δ + ε)] \underline{↔}_{rb} b·(d·δ + τ·c) and b·c[b ⇝ b·(d·δ + ε)] \underline{↔}_{rb} b·(d·δ + c) are not rooted branching bisimilar.

Let us now consider the action refinement operator in the context of BPA_{δτ}, so without the empty process. Since ε is no longer present, we adapt the TSS for this basic process algebra as follows, where a ranges over Act. Whereas in BPA_{εδτ} a transition p ⟶^{√} q can be thought of as statement that immediate termination is possible in state p, here it indicates an internal action resulting in successful termination.

\begin{matrix}a ⟶^{a} τ  τ ⟶^{√} δ  \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 TSS for BPA_{δτ} with action refinement is in rooted branching bisimulation format, if we mark the arguments of the BPA operators as before, except that the second argument of sequential composition is Λ-liquid, in view of the second rule for action refinement. Moreover, the first argument of action refinement is made Λ-liquid and ℵ-liquid, while the second argument of action refinement is made Λ-frozen and ℵ-liquid.

Corollary 6. \underline{↔}_{rb} is a congruence for BPA_{δτ} with the action refinement operator.

In the congruence format for rooted η-bisimilarity, condition 1 of Def. 14 is strengthened: right-hand sides of premises can only occur ℵ∩Λ-liquid in the target. That this strengthening is essential is illustrated by the fact that BPA_{δτ} with action refinement fails to be compositional for rooted η-bisimilarity. For example, the law a·(τ·x + y) = a·(τ·x + y) + a·x is sound modulo rooted ηbisimilarity, while after refining a to b·c, the resulting law (b·c)·(τ·x + y) = (b·c)(τ·x+y)+(b·c)·x is not sound modulo rooted η-bisimilarity; see [20, Sect. 7]. Note that the second rule for action refinement above violates condition 1′ of Def. 17, because the occurrence of y in the target is at an ℵ-frozen position. And if we try to resolve this by making the second argument of sequential composition ℵ-liquid, then the TSS is not ℵ∩Λ-patient (and thus not in rooted branching bisimulation format), due to the absence of a patience rule for the ℵ∩Λ-liquid second argument of sequential composition.

6.7 Λ-liquid but ℵ-frozen

In most of the above applications, it suffices to take Λ ⊆ ℵ. The only exception so far is action refinement, but this operator does not fall in the rooted η-bisimulation format. The TSS of the following example does fall in the ηbisimulation format (Λ is universal); yet it is not possible to take Λ ⊆ ℵ.

Example 3. Let f be a binary operator that interleaves actions ℓ ∈ A ∪ {τ} from its arguments, until its first argument 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 ⟶^{ℓ} y}{f(x_{1}, x_{2}) ⟶^{ℓ} f(y, x_{2})} \frac{x_{2} ⟶^{ℓ} y}{f(x_{1}, x_{2}) ⟶^{ℓ} f(x_{1}, y)} \frac{x ⟶^{crash} x′}{f(x, y) ⟶^{alert} pm.y} pm.y ⟶^{meltdown}^{prevent} y

Here pm is a CCS action-prefixing operator (cf, Example 2). 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.

6.8 Counterexamples

We now present 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 [22] a series of counterexamples can be found showing that the syntactic restrictions of the ntyft/ntyxt format are essential as well. Furthermore, in [8] a counterexample is given to show that completeness (there called positive after reduction) is essential.

It is well-known that branching and η-bisimilarity are not a congruence for BPA_{εδτ}. For instance, a \underline{↔}_{b} τ·a, but a + b \underline{↮}_{η} τ·a + b. The TSS for BPA_{εδτ} (see Sect. 6.1) is in rooted η-bisimulation format, whereby it is essential that the arguments of alternative composition and the second argument of sequential composition are made Λ-frozen. This shows that universality of the predicate Λ cannot be omitted from the branching and η-bisimulation format.

The following counterexamples will focus on the rooted branching bisimulation format. They feature terms t_{1}, t_{2} and a unary function symbol f with t_{1} \underline{↔}_{rb} t_{2} and f(t_{1})\underline{↮}_{η} f(t_{2}). This shows that none of the four semantics of this paper is a congruence, since \underline{↔}_{rb} and \underline{↔}_{η} are the strictest and most relaxed semantics, respectively, in this paper. The need for the strengthened restriction 1′ of Def. 17 (compared to condition 1 of Def. 14) was already shown at the end of Sect. 6.6.

The examples in this section assume the TSS for BPA_{εδτ} with Act = {a, b, c}. The arguments of alternative composition and the second argument of sequential composition are Λ-frozen and ℵ-liquid, while the first argument of sequential composition is Λ- and ℵ-liquid.

Example 4. We extend BPA_{εδτ} with the following rule:

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

Clearly, a·a \underline{↔}_{rb} a·(τ·a). However, f(a·a) \underline{↮}_{η} f(a·(τ·a)), since f(a·a) ⟶^{c} δ, while f(a·(τ·a)) cannot perform any transition.

We make the argument of f Λ-frozen and ℵ-liquid. The rule above is not in rooted branching bisimulation format because it contains lookahead.

Example 5. We extend BPA_{εδτ} with the following rule:

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

f(a·a) \underline{↮}_{η} f(a·(τ·a)), since f(a·a) ⟶^{a} f(ε·a) ⟶^{a} f(ε), while f(a·(τ·a)) can do an a-transition only to f(ε·(τ·a)), which cannot perform any transition.

If the argument of f is Λ-frozen, then y occurs as the right-hand side of a premise and Λ-frozen in the target, violating condition 1 of Def. 14. And if the argument of f is ℵ-frozen, then x occurs ℵ-frozen in the source and ℵ-liquid in the premise, violating condition 3 of Def. 14. Finally, if the argument of f is ℵ∩Λ-liquid, then it violates the restriction in Def. 15 that there should be an ℵ∩Λ-patience rule for this argument.

Example 6. We extend BPA_{εδτ} 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} δ}

f(a·a)\underline{↮}_{η} f(a·(τ·a)), since f(a·(τ·a)) ⟶^{a} f(ε·(τ·a)) ⟶^{c} δ, while f(a·a) can do

an a-transition only to f(ε·a), and f(ε·a) −̸→^{α} for α ∈ {c, τ}.

As in the previous example, it can be argued that the argument of f must be ℵ∩Λ-liquid. Note that this time there is an ℵ∩Λ-patience rule for the argument of f. However, the third rule is not rooted branching bisimulation safe, because the occurrence of x in the source is ℵ∩Λ-liquid, and x occurs ℵ-liquid in the negative premise, violating condition 4 of Def. 14.

Example 7. We extend BPA_{εδτ} 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} δ}

f(a·a)\underline{↮}_{η} f(a·(τ·a)), since f(a·(τ·a)) ⟶^{a} f(ε·(τ·a)) ⟶^{c} δ, while f(a·a) can do

an a-transition only to f(ε·a), and f(ε·a) −̸→^{α} for α ∈ {c, τ}.

As in the previous examples, the argument of f must be ℵ∩Λ-liquid. However, then the third rule is not rooted branching bisimulation safe, because the occurrence of x in the source is ℵ∩Λ-liquid, and x occurs ℵ-liquid in the positive premise with the label τ, while this rule is not ℵ∩Λ-patient, violating condition 4 of Def. 14.

Example 8. We extend BPA_{εδτ} with the following rules:

κ ⟶^{τ} ζ  ζ ⟶^{τ} κ  κ ⟶^{a} δ  ζ ⟶^{b} δ  ν ⟶^{a} δ  ν ⟶^{b} δ

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

Clearly, τ·ν \underline{↔}_{rb} τ·κ. However, f(τ·ν) \underline{↮}_{η} f(τ·κ), since f(τ·ν) ⟶^{τ} f(ε·ν) ⟶^{τ}

g(ε·ν) ⟶^{c} δ, while f(τ·κ) only exhibits an infinite sequence of τ-transitions: f(τ·κ) ⟶^{τ} f(ε·κ) ⟶^{τ} f(ζ) ⟶^{τ} f(κ) ⟶^{τ} ⋯, with side transitions f(τ·κ) ⟶^{τ} g(τ·κ), f(ζ) ⟶^{τ} g(ζ), etc., to states from which no further actions are possible.

Again, the argument of f must be ℵ∩Λ-liquid. Considering the last rule, the argument of g must be ℵ-liquid, in view of condition 3 of Def. 14. If the argument of g is Λ-liquid, then in the last rule the occurrence of x in the source is ℵ∩Λliquid, and x has two ℵ-liquid occurrences in the premises, violating condition 4 of Def. 14. And if the argument of g is Λ-frozen, then in the last but one rule, x occurs Λ-liquid in the source and Λ-frozen in the target, violating condition 2 of Def. 14.

Example 9. In the TSS from Ex. 8, we replace the last two rules with the following rules:

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

f(τ·ν)\underline{↮}_{η} f(τ·κ), since f(τ·ν) ⟶^{τ} f(ε·ν) ⟶^{c} δ, while f(τ·κ) can only perform τ-transitions.

Again, the argument of f must be ℵ∩Λ-liquid. Considering the first rule, the argument of g must be ℵ-liquid, in view of condition 3 of Def. 14, and Λ-frozen, in view of condition 4 of Def. 14. However, then the second rule is not rooted branching bisimulation safe, because x occurs Λ-liquid in the source and Λ-frozen in the left-hand side of the premise, violating condition 2 of Def. 14.

7 Abbreviation Expansion

Inspired by the congruence formats of [5], in [19] a two-tiered approach to structural operational semantics was introduced. It divides function symbols into two classes: principal operators and abbreviations. An abbreviation can be obtained by grouping together (and permuting) the arguments of a principal operator. For example, f(x, y) could be an abbreviation of g(x, y, x), for a ternary principal operator g. In the two-tiered approach the abbreviations do not have to obey the syntactic restrictions of a congruence format, as long as they abbreviate principal operators that do. Here we generalise this two-tiered approach from TSSs in GSOS format [7] to standard TSSs in decent ntyft format (using a different presentation than in [19]). This generalisation will help us to give a fair comparison between the congruence formats in [5,19] and the ones in the current paper; see Sect. 8.

The following copying operator occurs in [7, page 257]; there it plays an essential role in analysing the expressive power of the ready simulation format for processes without internal actions.

\frac{x ⟶^{a} y}{cp(x) ⟶^{a} cp(y)}  \frac{x ⟶^{l} y_{1} x ⟶^{r} y_{2}}{cp(x) ⟶^{s} cp(y_{1})∥cp(y_{2})}

The underlying alphabet of actions is {b, c, d, l, r, s}, with a ranging over the normal actions b, c, d, and l, r, s being the left and right forking actions and split action. The copying operator passes normal actions through, but when its argument process offers a choice between actions l and r, the copying process chooses both branches, thereby turning into a parallel composition of two copies of itself.

One way of extending this idea with the internal action τ is to add a patience rule for the argument of cp and replace the second rule by something like

\frac{x ⟹⟶^{l} y_{1} x ⟹⟶^{r} y_{2}}{cp(x) ⟹⟶^{s} cp(y_{1})∥cp(y_{2})}

where ⟹ stands for a sequence of internal transitions. This way we have

cp(τ·l·p + τ·r·q) ⟹⟶^{s} cp(p)∥cp(q) .

We also have cp(τ·l·p + τ·r·q) ⟶^{τ} cp(l.p), where the target process deadlocks.

Of course, the suggested TSS does not fit in the ready simulation format, due to the presence of lookahead, but the following TSS in ready simulation format implements the same idea.

\frac{x ⟶^{a} y}{cp(x) ⟶^{a} cp(y)}  \frac{x ⟶^{l} y_{1} x ⟶^{r} y_{2}}{cp(x) ⟶^{s} cp(y_{1})∥cp(y_{2})}

\frac{x ⟶^{τ} y}{cp(x) ⟶^{τ} bn(y, x)}  \frac{x ⟶^{τ} y}{cp(x) ⟶^{τ} bn(x, y)}

\frac{x_{1} ⟶^{τ} y}{bn(x_{1}, x_{2}) ⟶^{τ} bn(y, x_{2})}  \frac{x_{2} ⟶^{τ} y}{bn(x_{1}, x_{2}) ⟶^{τ} bn(x_{1}, y)}

\frac{x_{1} ⟶^{a} y}{bn(x_{1}, x_{2}) ⟶^{a} cp(y)}  \frac{x_{2} ⟶^{a} y}{bn(x_{1}, x_{2}) ⟶^{a} cp(y)}

\frac{x_{1} ⟶^{l} y_{1} x_{2} ⟶^{r} y_{2}}{bn(x_{1}, x_{2}) ⟶^{s} cp(y_{1})∥cp(y_{2})}

Here the auxiliary operator bn is a binary version of the copying operator, that can probe two branches of τ-actions at the same time. If these two branches offer a pair of forking actions, the desired split occurs, whereas a normal action encountered on any of the branches collapses bn back to its unary counterpart.

In view of the first, fifth and sixth rule, the arguments of both cp and bn need to be ℵ∩Λ-liquid. Therefore the second, third and fourth rule violate condition 4 of the rooted branching bisimulation format; moreover, the patience rule for cp(x) is missing. In spite of this, \underline{↔}_{b}, \underline{↔}_{rb}, \underline{↔}_{η} and \underline{↔}_{rη} are congruences for cp. This can be seen by thinking of cp(x) as an abbreviation for bn(x, x). This way, all rules for cp can be construed as special cases of the rules for bn, and the resulting five rules for bn fit the η-bisimulation format.

In general, we will translate one TSS P into another TSS P^{∗}, by finding a principal operator (like bn) for each abbreviation (like cp). From the fact that a weak semantics ∼ is a congruence for P^{∗}, we will then conclude that ∼ is a congruence for P.

Definition 19. A translation from a TSS P = (Σ, R) to a TSS P^{∗} = (Σ^{∗}, R^{∗}) is a function ^{∗} : Σ → Σ^{∗}, together with, for each f ∈ Σ, an argument matching f : {1, …, ar(f^{∗})} → {1, …, ar(f)}.

Here we overload the symbol f; it is always clear from the context whether we mean the function symbol in Σ or its corresponding argument matching. Translations naturally extend to functions ^{∗} : 𝕋(Σ) → 𝕋(Σ^{∗}) by x^{∗} =x for x∈V and f(t_{1}, …, t_{ar(f)})^{∗} = f^{∗}(t_{f(1)}^{∗}, …, t_{f(ar(f^{∗}))}^{∗}). They further extend trivially to (sets of) literals. Moreover, they extend to substitutions σ : V → 𝕋(Σ) by σ^{∗}(x) := σ(x)^{∗}, so that σ(t)^{∗} = σ^{∗}(t^{∗}) for any term t.

A translation from P to P^{∗} is lifted to a conversion of rules of P to rules of P^{∗} in two steps. First the sources are “starred”, producing an intermediate TSS P′. Next the premises are starred, yielding P^{∗}. There is a degree of freedom in converting P to P′; however, both P and P^{∗} are completely determined by P′.

Definition 20. A standard TSS P = (Σ, R) in decent ntyft format is an alternative representation of a standard TSS P^{∗} = (Σ^{∗}, R^{∗}) in decent ntyft format if there exists a translation ^{∗} : Σ → Σ^{∗}, and an intermediate standard TSS P′ = (Σ ∪ Σ^{∗}, R′) in decent ntyft format, whose rules have sources in 𝕋(Σ^{∗}) but premises and targets in 𝕋(Σ), such that

R^{∗} = \{\frac{H^{∗}}{t ⟶^{α} u^{∗}} | \frac{H}{t ⟶^{α} u} ∈ R′ \}

and

R = \{\frac{σ_{f}(H)}{f(x_{1}, …, x_{ar(f)}) ⟶^{α} σ_{f}(u)} | \frac{H}{f^{∗}(z_{1}, …, z_{ar(f^{∗})}) ⟶^{α} u} ∈ R′ \}

where the substitution σ_{f} : {z_{1}, …, z_{ar(f^{⋆})}} → {x_{1}, …, x_{ar(f)}} is given by σ_{f}(z_{i}) = x_{f(i)}. (By α-conversion we can ensure that all sources f(…) in R have arguments x_{1}, …, x_{ar(f)}, and all sources f^{∗}(…) in R^{∗} have arguments z_{1}, …, z_{ar(f^{∗})}.)

In our running example, the translation is given by cp^{∗}=bn with cp(1)=cp(2)=1 and bn^{∗} =bn with bn(1)=1 and bn(2)=2. The intermediate TSS consists of just the five rules for bn in the original TSS. Note that the first rule of P is linked to the third (and fourth) rule of P′, the second rule of P is linked to the fifth rule of P′, and the third and fourth rule of P are linked to the first and second rule of P′. The TSS P^{∗} is obtained by replacing terms cp(z) in targets in P′ by bn(z, z).

\frac{x_{1} ⟶^{τ} y}{bn(x_{1}, x_{2}) ⟶^{τ} bn(y, x_{2})}  \frac{x_{2} ⟶^{τ} y}{bn(x_{1}, x_{2}) ⟶^{τ} bn(x_{1}, y)}

\frac{x_{1} ⟶^{a} y}{bn(x_{1}, x_{2}) ⟶^{a} bn(y, y)}  \frac{x_{2} ⟶^{a} y}{bn(x_{1}, x_{2}) ⟶^{a} bn(y, y)}

\frac{x_{1} ⟶^{l} y_{1} x_{2} ⟶^{r} y_{2}}{bn(x_{1}, x_{2}) ⟶^{s} bn(y_{1}, y_{1})∥bn(y_{2}, y_{2})}

This TSS is in η-bisimulation format, with both arguments of bn ℵ∩Λ-liquid. Thus \underline{↔}_{b}, \underline{↔}_{rb}, \underline{↔}_{η} and \underline{↔}_{rη} are congruences for P^{∗}.

In all applications of this approach we have encountered so far, including the example above, we have (possibly up to renaming of function symbols) Σ^{∗} ⊆ Σ and R′ ⊆ R. In [19] this was even required by definition. It is in this case that we call P a two-tiered TSS, with the operators in Σ^{∗} principal operators and the ones in Σ \ Σ^{∗} abbreviations.

We will now prove that, if P is an alternative representation of P^{∗}, then for any weak semantics ∼ including strong bisimilarity, any congruence result for P^{∗} carries over to P.

Lemma 7. Let P = (Σ, R) be an alternative representation of P^{∗} = (Σ^{∗}, R^{∗})

and p, q′ ∈ 𝕋(Σ) closed. Then P^{∗} ⊢_{ws} p^{∗} ⟶^{α} q′ iff ∃q : P ⊢_{ws} p ⟶^{α} q ∧ q^{∗} = q′.

Proof. “Only if”: The proof of this direction will be delivered in three steps.

Claim 1: Let \frac{K}{μ} be a closed substitution instance of a rule of P. Then \frac{K^{∗}}{μ^{∗}} is a closed substitution instance of a rule of P^{∗}.

Proof: Let \frac{K}{p⟶^{α}q} be obtained by applying the closed substitution σ to the rule in R corresponding to \frac{H}{f^{∗}(z_{1},...,z_{ar(f^{∗})})⟶^{α}u} in R′. Then K = σ(σ_{f}(H)), and thus

K^{∗} = σ^{∗}(σ_{f}^{∗}(H^{∗})) = σ^{∗}(σ_{f}(H^{∗})) (because σ_{f}^{∗} = σ_{f}). Likewise q^{∗} = σ^{∗}(σ_{f}(u^{∗})). Furthermore,

\begin{matrix}p^{∗} = & σ(f(x_{1}, …, x_{ar(f)}))^{∗} \\ = & σ^{∗}(f^{∗}(x_{f(i)}, …, x_{f(ar(f^{∗}))})) \\ = & σ^{∗}(σ_{f}(f^{∗}(z_{1}, …, z_{ar(f^{∗})}))) . \end{matrix}

Thus \frac{K^{∗}}{p^{∗}⟶^{α}q^{∗}} is a substitution instance of the rule \frac{H^{∗}}{f^{∗}(z_{1},...,z_{ar(f^{∗})})⟶^{α}u^{∗}} in R^{∗}, using the closed substitution σ ∘ σ_{f}.

Claim 2: If a closed transition rule \frac{N}{p^{∗}⟶^{α}q′}, where N contains only negative premises and p ∈ 𝕋(Σ), is irredundantly provable from P^{∗}, then N = M^{∗} and q′ = q^{∗}, with \frac{M}{p⟶^{α}q} irredundantly provable from P.

Proof: By induction on the structure of irredundant proofs. Let π be an irredundant proof of \frac{N}{p^{∗}⟶^{α}q′} from P^{∗}, and let r ∈ R^{∗} be the rule and ρ the substitution used in the last step of π. Let r = \frac{H^{∗}}{t⟶^{α}u^{∗}} ∈ R^{∗} with \frac{H}{t⟶^{α}u} ∈ R′. Furthermore, let p = f(p_{1}, …, p_{ar(f)}). Then p^{∗} = f^{∗}(p_{f(1)}^{∗}, …, p_{f(ar(f^{∗}))}) = ρ(t). Hence t = f^{∗}(z_{1}, …, z_{ar(f^{∗})}) and ρ(z_{i}) = p_{f(i)}^{∗} for 1 ≤ i ≤ ar(f^{∗}). Let the closed substitution ω : {z_{1}, …, z_{ar(f^{∗})}} → 𝕋(Σ^{∗}) be given by ω(z_{i}) = p_{f(i)} for 1 ≤ i ≤ ar(f^{∗}). Then ρ(z_{i}) = ω^{∗}(z_{i}) for 1 ≤ i ≤ ar(f^{∗}).

For each positive premise v_{y} ⟶^{α_{y}} y in H, a strict subproof of π irredundantly proves a rule _{\frac{N_{y}}{ρ(v_{y}^{∗})⟶^{αy}ρ(y)}}, with N_{y} ⊆ N. Since r is decent, var(v_{y}^{∗}) ⊆ var(t) =

{z_{1}, …, z_{ar(f^{∗})}}. Hence ρ(v_{y}^{∗}) = ω^{∗}(v_{y}^{∗}) = ω(v_{y})^{∗}. By induction we obtain N_{y} =

M_{y}^{∗} and ρ(y) = q_{y}^{∗} with \frac{M_{y}}{ω(v_{y})⟶^{αy}q_{y}} irredundantly provable from P.

We have r′ = \frac{σ_{f} (H)}{f(x_{1},...,x_{ar(f)})⟶^{α}σ_{f} (u)} ∈ R with σ_{f}(z_{i}) = x_{f(i)} for 1 ≤ i ≤ ar(f^{∗}).

Let σ : var(r′) → 𝕋(Σ) be the closed substitution with σ(x_{i})=p_{i} for 1≤i≤ar(f) and σ(y)=q_{y} for y∈rhs(σ_{f}(H))=rhs(H). Then σ∘σ_{f}(z_{i})=σ(x_{f(i)})=p_{f(i)}=ω(z_{i}) for 1 ≤ i ≤ ar(f^{∗}). Therefore, for each v_{y} ⟶^{α_{y}} y ∈ H we have σ ∘ σ_{f}(v_{y} ⟶^{α_{y}} y) =

ω(v_{y}) ⟶^{α_{y}} q_{y}, and for each v −̸→^{β} ∈ H we have σ ∘ σ_{f}(v −̸→^{β}) = ω(v) −̸→^{β}.

The rules \frac{M_{y}}{ω(v_{y})⟶^{αy}q_{y}} for y ∈ rhs(H) are irredundantly provable from P, and

applying σ to r′ ∈ R yields

\frac{\{ω(v_{y}) ⟶^{α_{y}} q_{y} | y ∈ rhs(H)\} ∪ \{ω(v) −̸→^{β} | v −̸→^{β} ∈ H\}}{f(p_{1}, …, p_{ar(f)}) ⟶^{α} σ(σ_{f}(u))} .

So \frac{M}{p⟶^{α}σ(σ_{f} (u))} with M := ⋃_{y∈rhs(H)} M_{y} ∪ \{ω(v) −̸→^{β} | v −̸→^{β} ∈ H\} is irredun-

dantly provable from P.

\begin{matrix}M^{∗} = & ⋃_{y∈rhs(H)} M_{y}^{∗} ∪ & \{ω^{∗}(v^{∗}) −̸→^{β} | v −̸→^{β} ∈ H\} = \\ = & ⋃_{y∈rhs(H)} N_{y} ∪ & \{ρ(v^{∗}) −̸→^{β} | v −̸→^{β} ∈ H\} = & N . \end{matrix}

As \frac{H}{t⟶^{α}u} is decent, u contains no other variables than z_{i} for 1 ≤ i ≤ ar(f^{∗}) and y for y ∈ rhs(H). We have (σ ∘ σ_{f})^{∗}(z_{i}) = ω^{∗}(z_{i}) = ρ(z_{i}) for 1 ≤ i ≤ ar(f^{∗}) and (σ ∘ σ_{f})^{∗}(y) = σ(σ_{f}(y))^{∗} = σ(y)^{∗} = q_{y}^{∗} = ρ(y) for y ∈ rhs(H). Therefore σ(σ_{f}(u))^{∗} = ρ(u^{∗}) = q′.

The following claim strengthens the direction “only if” of the lemma.

Claim 3: If P ⊢_{ws} λ for a closed literal λ, then P^{∗} ⊢_{ws} λ^{∗}.

Proof: By induction on the structure of well-supported proofs. Let π be a wellsupported proof from P of a closed positive literal λ = p ⟶^{α} q. Then there is a closed substitution instance \frac{K}{λ} of a rule in R, and each literal μ ∈ K is provable by a strict subproof of π. By induction, P^{∗} ⊢_{ws} μ^{∗} for each such μ. By Claim 1 \frac{K^{∗}}{μ^{∗}} is a closed substitution instance of a rule of P^{∗}. It follows that P^{∗} ⊢_{ws} λ^{∗}.

Now let π be a well-supported proof from P of a closed negative literal λ = p −̸→^{α}. In order to show that P^{∗} ⊢_{ws} λ^{∗}, let N be a set of closed negative literals such that, for some closed term q′, the rule \frac{N}{p^{∗}⟶^{α}q′} is irredundantly provable from P^{∗}. It suffices to show that P^{∗} ⊢_{ws} ν, for a literal ν denying a literal in N.

By Claim 2, \frac{N}{p^{∗}⟶^{α}q′} = \frac{M^{∗}}{p^{∗}⟶^{α}q^{∗}}, for some rule \frac{M}{p⟶^{α}q} irredundantly provable

from P. Since P ⊢_{ws} p −̸→^{α}, by Def. 7, a strict subproof of π proves a literal μ denying a literal in M. By induction, P^{∗} ⊢_{ws} μ^{∗}. Moreover, μ^{∗} denies a literal in M^{∗} = N.

The last claim strengthens the “if”-direction of the lemma. Its proof proceeds along the same lines as for the claims above.

Claim 4: Let p ∈ 𝕋(Σ). If P^{∗} ⊢_{ws} p^{∗} ⟶^{α} q′, then P ⊢_{ws} p ⟶^{α} q with q^{∗} = q′.

Likewise, if P^{∗} ⊢_{ws} p^{∗} −̸→^{α}, then P ⊢_{ws} p −̸→^{α}.

Proof: By induction on the structure of irredundant proofs. Let π be a wellsupported proof from P^{∗} of p^{∗} ⟶^{α} q′ and let r ∈ R^{∗} be the rule and ρ the substitution used in the last step of π. Let r = \frac{H^{∗}}{t⟶^{α}u^{∗}} ∈ R^{∗} with \frac{H}{t⟶^{α}u} ∈ R′. Furthermore, let p = f(p_{1}, …, p_{ar(f)}). Then p^{∗} = f^{∗}(p_{f(1)}^{∗}, …, p_{f(ar(f^{∗}))}) = ρ(t). Hence t = f^{∗}(z_{1}, …, z_{ar(f^{∗})}) and ρ(z_{i}) = p_{f(i)}^{∗} for 1 ≤ i ≤ ar(f^{∗}). Let the closed substitution ω : {z_{1}, …, z_{ar(f^{∗})}} → 𝕋(Σ^{∗}) be given by ω(z_{i}) = p_{f(i)} for 1 ≤ i ≤ ar(f^{∗}). Then ρ(z_{i}) = ω^{∗}(z_{i}) for 1 ≤ i ≤ ar(f^{∗}).

For each positive premise v_{y} ⟶^{α_{y}} y in H, a strict subproof of π proves ρ(v_{y}^{∗}) ⟶^{α_{y}} ρ(y). Since r is decent, var(v_{y}^{∗}) ⊆ var(t) = {z_{1}, …, z_{ar(f^{∗})}}. Hence ρ(v_{y}^{∗}) = ω^{∗}(v_{y}^{∗}) = ω(v_{y})^{∗}. By induction P ⊢_{ws} ω(v_{y}) ⟶^{α_{y}} q_{y} for some q_{y} with q_{y}^{∗} = ρ(y). Likewise, for each negative premise v −̸→^{β} in H, a strict subproof of π proves ρ(v^{∗}) −̸→^{β}. Again ρ(v^{∗}) = ω^{∗}(v^{∗}) = ω(v)^{∗}. By induction P ⊢_{ws} ω(v) −̸→^{β}.

We have r′ = \frac{σ_{f} (H)}{f(x_{1},...,x_{ar(f)})⟶^{α}σ_{f} (u)} ∈ R with σ_{f}(z_{i}) = x_{f(i)} for 1 ≤ i ≤ ar(f^{∗}).

Let σ : var(r′) → 𝕋(Σ) be the closed substitution with σ(x_{i})=p_{i} for 1≤i≤ar(f) and σ(y)=q_{y} for y∈rhs(σ_{f}(H))=rhs(H). Then σ∘σ_{f}(z_{i})=σ(x_{f(i)})=p_{f(i)}=ω(z_{i}) for 1 ≤ i ≤ ar(f^{∗}). Therefore, for each v_{y} ⟶^{α_{y}} y ∈ H we have σ ∘ σ_{f}(v_{y} ⟶^{α_{y}} y) =

ω(v_{y}) ⟶^{α_{y}} q_{y}, and for each v −̸→^{β} ∈ H we have σ ∘ σ_{f}(v −̸→^{β}) = ω(v) −̸→^{β}.

Applying σ to r′ ∈ R yields

\frac{\{ω(v_{y}) ⟶^{α_{y}} q_{y} | y ∈ rhs(H)\} ∪ \{ω(v) −̸→^{β} | v −̸→^{β} ∈ H\}}{f(p_{1}, …, p_{ar(f)}) ⟶^{α} σ(σ_{f}(u))} .

So P ⊢_{ws} p ⟶^{α} σ(σ_{f}(u)).

As \frac{H}{t⟶^{α}u} is decent, u contains no other variables than z_{i} for 1 ≤ i ≤ ar(f^{∗}) and y for y ∈ rhs(H). We have (σ ∘ σ_{f})^{∗}(z_{i}) = ω^{∗}(z_{i}) = ρ(z_{i}) for 1 ≤ i ≤ ar(f^{∗}) and (σ ∘ σ_{f})^{∗}(y) = σ(σ_{f}(y))^{∗} = σ(y)^{∗} = q_{y}^{∗} = ρ(y) for y ∈ rhs(H). Therefore σ(σ_{f}(u))^{∗} = ρ(u^{∗}) = q′.

Now let π be a well-supported proof from P^{∗} of p^{∗} −̸→^{α}. In order to show that P ⊢_{ws} p −̸→^{α}, let N be a set of closed negative literals such that, for some closed term q, the rule \frac{N}{p⟶^{α}q} is irredundantly provable from P. It suffices to show that P ⊢_{ws} λ, for a literal λ denying a literal ν in N.

By Claim 1, and a trivial induction on the structure of irredundant proofs, the rule \frac{N^{∗}}{p^{∗}⟶^{α}q^{∗}} is irredundantly provable from P^{∗}. Since P^{∗} ⊢_{ws} p^{∗} −̸→^{α}, by Def. 7, a strict subproof of π proves a literal μ denying a literal in N^{∗}. The latter literal must have the form ν^{∗} for some ν ∈ N.

In case ν = (p_{ν} ⟶^{α_{ν}} q_{ν}), we have μ = (p_{ν}^{∗} −̸→^{α_{ν}}). By induction P ⊢_{ws} p_{ν} −̸→^{α_{ν}}, and this literal denies ν ∈ N.

In case ν = (p_{ν} −̸→^{β_{ν}}), we have μ = (p_{ν}^{∗} ⟶^{β_{ν}} q′_{ν}) for some p_{ν} ∈ 𝕋(Σ) and q′ ∈ 𝕋(Σ^{∗}). By induction P ⊢_{ws} p_{ν} ⟶^{β_{ν}} q_{ν} for some q_{ν} ∈ 𝕋(Σ) with q_{ν}^{∗} = q′_{ν}. Again this literal denies ν ∈ N. ⊓ ⊔

A symmetric relation R ⊆ ℙ × ℙ is a strong bisimulation if pRq and p ⟶^{α} p′ implies that q ⟶^{α} q′ for some q′ with p′Rq′. Processes p, q are strongly bisimilar, denoted p \underline{↔} q, if there exists a strong bisimulation R with pRq. Processes in different TSSs can be compared up to strong bisimilarity, namely by considering the disjoint union of the TSSs.

Corollary 7. Let P be an alternative representation of P^{∗}, and ∼ any equivalence relation on processes satisfying p \underline{↔} q ⇒ p ∼ q. Then p^{∗} ∼ q^{∗} iff p ∼ q.

Proof. We have p \underline{↔} p^{∗} for all closed terms p ∈ 𝕋(Σ), because the relation {(p, p^{∗}), (p^{∗}, p) | p ∈ 𝕋(Σ)} is a strong bisimulation by Lemma 7. Hence if p ∼ q then p^{∗} \underline{↔} p ∼ q \underline{↔} q^{∗}, implying p^{∗} ∼ q^{∗}, and if p^{∗} ∼ q^{∗} then p \underline{↔} p^{∗} ∼ q^{∗} \underline{↔} q, implying p ∼ q. ⊓ ⊔

Corollary 8. Let P be an alternative representation of P^{∗} and ∼ be any equivalence relation on processes satisfying p \underline{↔} q ⇒ p ∼ q, such that ∼ is a congruence for P^{∗}. Then ∼ is a congruence for P.

Proof. Suppose p_{i} ∼ q_{i} for i = 1, …, ar(f). By Cor. 7, p_{i}^{∗} ∼ q_{i}^{∗} for i = 1, …, ar(f). By assumption, f(p_{1}, …, p_{ar(f)})^{∗} ∼ f(q_{1}, …, q_{ar(f)})^{∗}. Thus, by Cor. 7, f(p_{1}, …, p_{ar(f)}) ∼ f(q_{1}, …, q_{ar(f)}). ⊓ ⊔

As for our running example, it now follows that \underline{↔}_{b}, \underline{↔}_{rb}, \underline{↔}_{η} and \underline{↔}_{rη} are congruences for cp.

Definition 21. Let F be a congruence format on standard TSSs that lays within the decent ntyft format. A TSS is said to be in the two-tiered F -format [19], iff it is an alternative representation of a TSS in F -format.

Theorem 7. Let ∼ be an equivalence relation on LTSs such that p \underline{↔} q ⇒ p ∼ q, and let F be a format on standard TSSs within the decent ntyft format so that for any TSS in F -format, ∼ is a congruence. Then ∼ is a congruence for any TSS in the two-tiered F -format.

Proof. Apply Cor. 8. ⊓ ⊔

8 Related Work

The first congruence formats for branching and rooted branching bisimilarity were presented in [5], and reformulated in [19]. The latter paper also added the first formats for η- and rooted η-bisimilarity. Those four formats, which are contained in the GSOS format [7] (and thereby also in the intersection of the nxytt and decent ntyft formats), distinguish so-called “principal” function symbols and “abbreviations”. The latter can be regarded as syntactic sugar, adding nothing that could not be expressed with principal function symbols. In [5,19] also simplified variants of these four formats were proposed, obtained by requiring all function symbols to be principal; as shown in [19], the general formats of [5,19] can be obtained as the two-tiered version of the corresponding simplified formats. Our main formats strictly generalise the simplified formats of [5,19]. Consequently, the two-tiered versions of our formats (or more precisely, of the intersection of our formats with the decent ntyft format) generalise the full formats of [5,19].

For the branching bisimulation format our generalisation consists of allowing transition rules outside the GSOS format; the simplified format of [5,19] is exactly the intersection of our branching bisimulation format and the GSOS format. (Our predicate ℵ marks the arguments of function symbols that are called active in [19].) Likewise, the simplified η-bisimulation format of [19] is the intersection of our η-bisimulation format and the GSOS format. However, the intersections of our rooted formats and the GSOS format are still proper generalisations of the simplified rooted formats of [5,19]. The latter can be described as the intersections of our rooted formats and the GSOS format in which all arguments of all function symbols that occur in targets of rules are required to be Λ-liquid.

The applications of our formats presented in Sections 6.1 (sequential composition in basic process algebra), 6.4 (the binary Kleene star) and 6.6 (action refinement) fall inside the GSOS format but outside the formats of [5,19]. The replication operator of Section 6.3 is an example of an application of our formats that falls outside the GSOS format; recursion (Section 6.2) is another example. We have not repeated applications of our approach that fall already within the formats of [5,19]; these include the full process algebras CCS [28] and CSP [24].

The rooted formats of [5,19] distinguish “tame” and “wild” function symbols. In terms of our approach, wild function symbols have only Λ-frozen arguments, and tame function symbols only Λ-liquid arguments. The idea to allow function symbols with both kinds of arguments stems from [10], where a so-called RBB safe format for rooted branching bisimilarity was proposed, which generalises the simplified format of [5,19]. 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 liberal than the format of [10]. Still, all applications of our work discussed in Sect. 6 fall within the format of [10]. The main point of the current framework is not that we have obtained more liberal congruence formats, but that their formulations are simpler and more elegant than existing congruence formats, and, most importantly, that they were obtained in a systematic way from the modal characterisations of (rooted) branching and η-bisimilarity.

9 Conclusions

We have extended the method from [6] for modal decomposition and the derivation of congruence formats to weak semantics. This paper gives a deeper insight into the link between modal logic and congruence formats, and provides a framework for the derivation of congruence formats for the spectrum of weak semantics from [17].

Admittedly, the whole story is quite technical and intricate. Partly this is because we build on a rich body of earlier work in the realm of structural operational semantics: the notions of well-supported proofs and complete TSSs from [18] (or actually [15] in logic programming); the ntyft/ntyxt format from [8]; the transformation to ruloids, which for the main part goes back to [11]; and the work on modal decomposition and congruence formats from [6].

In spite of these technicalities, we have arrived at a relatively simple framework for the derivation of congruence formats for weak semantics. Namely, for this one only needs to: (1) provide a modal characterisation of the weak semantics under consideration; (2) study the class of modal formulas that result from decomposing this modal characterisation, and formulate syntactic restrictions on TSSs to bring this class of modal formulas within the original modal characterisation; and (3) check that these syntactic restrictions are preserved under the transformation to ruloids. As shown in Sect. 5, steps (2) and (3) are very similar in structure for the different weak semantics based on branching and ηbisimulation. And as said, the end results are congruence formats that are more general and at the same time more elegant than existing congruence formats for these weak semantics in the literature.

We have been working on this paper over an extended period of time. Most of all it has taken a lot of effort to arrive at the proper predicates ℵ and Λ, and the corresponding notion of patience rules. When in the end these notions were all in place, it turned out that the whole machinery works like clockwork.

The door is now open to derive congruence formats for a wide range of weak semantics. However, we have found that weak semantics like delay bisimilarity [27] and weak bisimilarity [28], for which the relation pBq′ from Def. 1 is missing, require a non-trivial extension of the framework put forward in this paper. We intend to put forward this extended framework in a follow-up of the current paper. For future research, it would also be interesting to see whether the bridge between modal logic and congruence formats could be employed in the realm of logics and semantics for e.g. probabilities and security.

References

1. J.C.M. Baeten, J.A. Bergstra & J.W. Klop (1986): Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae 9(2), pp. 127–167.

2. J.C.M. Baeten & R.J. van Glabbeek (1987): Another look at abstraction in process algebra. In Proc. ICALP’87, LNCS 267, pp. 84–94. Springer.

3. T. Basten (1996): Branching bisimulation is an equivalence indeed!, Information Processing Letters 58(3), pp. 141-147.

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

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

6. 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.

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

8. 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.

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

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

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

12. 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.

13. W.J. Fokkink, R.J. van Glabbeek & P. de Wind (2006a): Divide and congruence: From decomposition of modalities to preservation of branching bisimulation. In Proc. FMCO’05, LNCS 4111, pp. 195–218. Springer.

14. W.J. Fokkink, R.J. van Glabbeek & P. de Wind (2006b): Divide and congruence applied to η-bisimulation. In Proc. SOS’05, ENTCS 156(1), pp. 97–113. Elsevier.

15. A. van Gelder, K. Ross & J.S. Schlipf (1991): The well-founded semantics for general logic programs. Journal of the ACM 38(3), pp. 620–650.

16. R.J. van Glabbeek (1987): Bounded nondeterminism and the approximation induction principle in process algebra. In Proc. STACS’87, LNCS 247, pp. 336– 347. Springer.

17. 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.

18. 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.

19. R.J. van Glabbeek (2011): On cool congruence formats for weak bisimulations. Theoretical Computer Science, 412(28):3283–3302, 2011.

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

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

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

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

24. C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice Hall.

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

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

27. R. Milner (1981): A modal characterisation of observable machine-behaviour. In Proc. CAAP’81, LNCS 112, pp. 25–34. Springer.

28. R. Milner (1989): Communication and Concurrency. Prentice-Hall.

29. R. Milner (1999): Communicating and Mobile Systems: the π-Calculus. Cambridge University Press.

30. 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.

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

32. F.W. Vaandrager (1990): Algebraic Techniques for Concurrency and their Application. PhD thesis, University of Amsterdam.

A Modal Characterisations

We prove the first part of Thm. 1, which states that 𝕆_{b} is a modal characterisation of branching bisimilarity. The proof is based on [9]. 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}. Furthermore,

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 induc-

tion 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 possi-

bilities.

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 induc-

tion 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. 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. ⊓ ⊔

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 bisimilarity.

The validity of the modal characterisation of η-bisimilarity can be proved in a similar fashion.