Compositionality of Hennessy-Milner Logic by Structural Operational Semantics

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

1 CWI, Department of Software Engineering PO Box 94079, 1090 GB Amsterdam, The Netherlands 2 National ICT Australia

Locked Bag 6016, University of New South Wales, Sydney 1466, Australia 3 University of New South Wales, School of Computer Science and Engineering

Sydney 2052, Australia

4 Vrije Universiteit Amsterdam, Department of Theoretical Computer Science De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands

      wanf@cs.vu.nl, rvg@cs.stanford.edu, pdwind@cs.vu.nl
                  http://www.cs.vu.nl/~wanf/
               http://theory.stanford.edu/~rvg/
                 http://www.cs.vu.nl/~pdwind/

Abstract. This paper presents a method for the decomposition of HML formulas. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulas, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is the extension of an earlier decomposition method for the De Simone format from the PhD thesis of Kim G. Larsen in 1986, to more general formats.

1 Introduction

In the past two decades, compositional methods have been developed for checking the validity of assertions in modal logics, used to describe the behaviour of processes. This means that the truth of an assertion for a composition of processes can be deduced from the truth of certain assertions for its components. Most research papers in this area focus on a particular process algebra.

Barringer, Kuiper & Pnueli presented in [4] (a preliminary version of) a compositional proof system for concurrent programs, which is based on a rich temporal logic, including operators from process logic [15] and LTL [26]. For modelling concurrent programs they defined a language including assignment, conditional and while statements. Parallel components interact via shared variables.

In [29], Stirling developed modal proof systems for subsets of CCS [22] (with and without silent actions) including only sequential and alternative composition, to decide the validity of formulas from Hennessy-Milner Logic (HML)

[16]. In [31, 30], Stirling extended the results from [29], creating proof systems for subsets of CCS and SCCS [24] including asynchronous and synchronous parallelism and infinite behaviour, using ideas from [4]. In [32], Stirling generalised the proposals from [31, 30] in order to cope with the restriction operator.

Winskel gave in [33] a method to decompose formulas with respect to each operation in SCCS. The language of assertions is HML with infinite conjunction and disjunction. This decomposition provides the foundations of Winskel’s proof system for SCCS with modal assertions. In [34], [3] and [2] processes are described by specification languages inspired by CCS and CSP [8]. The articles describe compositional methods for deciding whether processes satisfy assertions from a modal μ-calculus [18].

Larsen developed in [20] a more general compositional method for deciding whether a process satisfies a certain property. Unlike the aforementioned methods, this method is not oriented towards a particular process algebra, but it is based on structural operational semantics [25], which provides process algebras and specification languages with an interpretation. A transition system specification, consisting of an algebraic signature and a set of transition rules of the form \frac{premises}{conclusion}, generates a transition relation between the closed terms over the signature. An example of a transition rule, for alternative composition, is

\frac{x_{1} ⟶^{a} y}{x_{1} + x_{2} ⟶^{a} y}

meaning for states t_{1}, t_{2} and u that if state t_{1} can evolve into state u by the execution of action a, then so can state t_{1} + t_{2}. Larsen showed how to decompose HML formulas with respect to a transition system specification in the De Simone format [27]. This format was originally put forward to guarantee that the bisimulation equivalence associated with a transition system specification is a congruence, meaning that bisimulation equivalence is preserved by all functions in the signature. In [21], Larsen and Xinxin extended this decomposition method to HML with recursion (which is equivalent to the modal μ-calculus).

Since modal proof systems for specific process algebras are tailor-made, they may be more concise than the ones generated by the general decomposition method of Larsen (e.g., [31, 30, 32]). However, in some cases the general decomposition method does produce modal proof systems that are similar in spirit to those in the literature (e.g., [29, 33]).

For systems consisting of parallel compositions of interacting components and specification logics based on the modal μ-calculus, the efficacy of Larsen’s compositional approach was demonstrated by Andersen in [1]. Laroussinie & Larsen applied this approach in [19] to real-time systems modelled as networks of timed automata.

Bloom, Fokkink & van Glabbeek presented in [5] a method for decomposing formulas from a fragment of HML with infinite conjunction, with respect to terms from any process algebra that has a structural operational semantics in ready simulation format, which is the ntyft/ntyxt format [13] without lookahead. A rule in ntyft/ntyxt format may contain negative premises, the left-hand side of the conclusion contains at most one function symbol and no multiple occurrences of variables, and the right-hand sides of positive premises are variables that are all distinct and do not occur in the left-hand side of the conclusion. Such a rule has no lookahead if variables in the right-hand sides of premises do not occur in the left-hand sides of premises. This format is a generalisation of the De Simone format, and still guarantees that bisimulation equivalence is a congruence. The decomposition method is not presented in its own right, but is used in the derivation of congruence formats for a range of behavioural equivalences from van Glabbeek [11].

In the current paper, the decomposition method from [5] is extended to full HML with infinite conjunction, for process algebras with a structural operational semantics in ntyft/ntyxt format without lookahead or in tyft/tyxt format [14]. The latter format is the same as the ntyft/ntyxt format, but disallows negative premises. The rules in this format may contain lookahead, i.e. there may be a chain of premises such that the right-hand side of each premise occurs in the left-hand side of the next premise; if this chain is finite, we speak of bounded lookahead. We show that if a rule has unbounded lookahead, it can be replaced by a rule with bounded lookahead. This is needed because no HML formula can capture unbounded lookahead.

In [28], Simpson presented a proof system for establishing the validity of HML formulas for processes in arbitrary languages with a structural operational semantics in GSOS format [6], using a mixture of compositional and structural styles of proof. His method differs from ours, and from the work referenced above, in that the validity of an assertion for a process term may be inferred from statements about the dynamic behaviour of that process, whereas we only allow modal assertions for subterms.

An earlier version of this paper, which featured only a compositionality result for ntyft/ntyxt format without lookahead, appeared as [10].

The structure of the paper is as follows. Section 2 contains the preliminaries on modal logic and structural operational semantics. In Section 3 we present the decomposition method for HML formulas. Finally, in Section 4 we show as an application of this method that the congruence theorem for the tyft/tyxt format from [14, 9] is an immediate corollary of our decomposition result.

2 Preliminaries

In this section we give the basic notions of Hennessy-Milner Logic and structural operational semantics that are needed to define our decomposition method.

Definition 1 (LTS, transition relation). A labelled transition system (LTS) is a pair (ℙ, →) with ℙ a set of processes and → ⊆ ℙ × A × ℙ for A a set of actions. The relation → is called the transition relation and its elements are called transitions. We write p ⟶^{a} q for (p, a, q) ∈ → and p −̸→^{a} for ¬∃q ∈ ℙ :

p ⟶^{a} q.

The elements of ℙ represent the processes we are interested in, and p ⟶^{a} q means that process p can evolve into process q while performing the action a.

2.1 Hennessy-Milner Logic

Modal logic aims at formulating properties of processes, and to identify processes that satisfy the same properties. In [16], Hennessy & Milner defined a modal language, often called Hennessy-Milner Logic (HML), which characterises the bisimulation equivalence relation on processes, assuming that the transition relation is image finite, i.e. each process has finitely many outgoing a-transitions for each a ∈ A. This assumption can be discarded if infinite conjunctions are allowed; see [23, 17].

Definition 2 (Hennessy-Milner Logic). Assume an action set A. The set 𝕆 of potential observations or modal formulas is recursively defined by

φ ::= ⋀_{i∈I} φ_{i} | ⟨a⟩φ | ¬φ

with a ∈ A and I some index set.

Definition 3 (satisfaction relation). Let (ℙ, →) be an LTS. The satisfaction relation ⊧ ⊆ ℙ × 𝕆 is defined as follows, with p ∈ ℙ:

p ⊧ ⋀_{i∈I} φ_{i} iff p ⊧ φ_{i} for all i ∈ I
p ⊧ ⟨a⟩φ iff there is a q ∈ ℙ such that p ⟶^{a} q and q ⊧ φ
p ⊧ ¬φ  iff p |̸= φ

We will use the binary conjunction φ_{1} ∧ φ_{2} as an abbreviation of ⋀_{i∈{1,2}} φ_{i}, whereas ⊤ is an abbreviation for the empty conjunction. We identify formulas that are logically equivalent using the laws ⊤ ∧ φ ≅ φ, ⋀_{i∈I}(⋀_{j∈J_{i}} φ_{j}) ≅ ⋀_{i∈I, j∈J_{i}} φ_{j} and ¬¬φ ≅ φ. This is justified because φ ≅ ψ implies p ⊧ φ ⇔ p ⊧ ψ.

Definition 4 (bisimulation). Let (ℙ, →) be an LTS. A binary relation B ⊆ ℙ×ℙ is a bisimulation if it is symmetric and pBq implies: if p ⟶^{a} p′ then there is a q′ such that q ⟶^{a} q′ and p′Bq′. For p, q ∈ ℙ we write p \underline{↔} q if there is a bisimulation B such that pBq.

Proposition 1 ([23, 17]). Let (ℙ, →) be an LTS. Then p \underline{↔} q if and only iff p ⊧ φ ⇔ q ⊧ φ for all φ ∈ 𝕆.

2.2 Structural Operational Semantics

Structural operational semantics [25] provides a framework to give an operational semantics to programming and specification languages. In particular, because of its intuitive appeal and flexibility, structural operational semantics has found considerable application in the study of the semantics of concurrent processes.

Let V be a set of variables. If S is any syntactic object, var(S) denotes the set of variables that occur in S. A syntactic object S is called closed if it does not contain any variables from V, i.e. if var(S) = ∅.

Definition 5 (signature). A signature is a collection Σ of function symbols f ∉ V, equipped with a function ar : Σ → ℕ. The set 𝕋(Σ) of terms over a signature Σ is defined recursively by:

– V ⊆ 𝕋(Σ),

– if f ∈ Σ and t_{1}, …, t_{ar(f)} ∈ 𝕋(Σ), then f(t_{1}, …, t_{ar(f)}) ∈ 𝕋(Σ).

A term c() is abbreviated as c. T (Σ) is the set of closed terms over Σ. A Σsubstitution σ is a partial function from V to 𝕋(Σ). The domain of σ is denoted by dom(σ). If σ is a Σ-substitution and S is any syntactic object, then σ(S) denotes the object obtained from S by replacing, for x in the domain of σ, every occurrence of x in S by σ(x). In that case σ(S) is called a substitution instance of S. A Σ-substitution σ is closed if σ(x) ∈ T (Σ) for all x ∈ V.

In the remainder, let Σ denote a signature and A a set of actions.

Definition 6 (literal). A positive Σ-literal is an expression t ⟶^{a} t′ and a negative Σ-literal an expression t −̸→^{a} with t, t′ ∈ 𝕋(Σ) and a ∈ A. For t, t′ ∈ 𝕋(Σ) and a ∈ A, the literals t ⟶^{a} t′ and t −̸→^{a} are said to deny each other.

Definition 7 (transition rule). A transition rule over Σ is an expression of the form \frac{H}{α} with H a set of Σ-literals (the premises of the the rule) and α a positive Σ-literal (the conclusion). With lhs(H) and rhs(H) we denote the sets of left- and right-hand sides of the premises in H, respectively. The left- and right-hand side of α are called the source and the target of the rule, respectively. A rule \frac{H}{α} with H = ∅ is also written α.

Definition 8 (transition system specification). A transition system specification (TSS) is a pair (Σ, R) with R a collection of transition rules over Σ.

The purpose of a TSS (Σ, R) is to specify an LTS of the form (T (Σ), →) with as processes the closed terms over Σ and as transition relation a set of closed positive literals → ⊆ T (Σ)×A×T (Σ). Hence we refer to a closed positive literal as a transition.

Definition 9 (proof). Let P = (Σ, R) be a TSS. An irredundant proof from P of a transition rule \frac{H}{α} is a well-founded, upwardly branching tree whose nodes are labelled by Σ-literals, and some of the leaves are marked “hypothesis”, such that:

– the root is labelled by α,

– H is the set of labels of the hypotheses, and

– if β is the label of a node q which is not a hypothesis and K is the set of labels of the nodes directly above q, then \frac{K}{β} is a substitution instance of a transition rule in R.

A proof from P of \frac{K}{α} is an irredundant proof from P of \frac{H}{α} with H ⊆ K. If an (irredundant) proof from P of \frac{K}{α} exists, then \frac{K}{α} is (irredundantly) provable from P, notation P ⊢ \frac{K}{α} (resp. P ⊢_{irr} \frac{K}{α}).

The proof of \frac{H}{α} is called irredundant because H must equal (instead of include) the set of labels of the hypotheses. The main advantage of irredundant proofs is that derived rules may inherit certain syntactic structure from the transition rules in the TSS from which they are derived; in standard proofs this syntactic structure is usually lost, because arbitrary literals can be added as premises of derived rules. In the current paper, irredundancy of proofs is not of immediate importance, but it can be essential in applications of our decomposition method for modal formulas. For instance, in [5], irredundancy is essential to guarantee that the syntactic restrictions of congruence formats for TSSs are also satisfied by the rules derived from those TSSs.

A TSS with only positive premises specifies a transition relation in a straightforward way as the set of all provable transitions. But it is much less trivial to associate a transition relation to a TSS with negative premises. Several solutions are proposed by Groote in [13], Bol & Groote in [7], and van Glabbeek in [12]. From the last we adopt the notion of a well-supported proof and a complete TSS.

Definition 10 (well-supported proof). Let P = (Σ, R) be a TSS. A wellsupported proof from P of a closed literal α is a well-founded, upwardly branching tree whose nodes are labelled by closed Σ-literals, such that:

– the root is labelled by α, and

– if β is the label of a node q and K is the set of labels of the nodes directly above q, then

1. either \frac{K}{β} is a closed substitution instance of a transition rule in R

2. or β is negative and for every set N of closed negative literals such that P ⊢ \frac{N}{γ} for γ a closed literal denying β, a literal in K denies one in N.

We say α is ws-provable from P, notation P ⊢_{ws} α, if a well-supported proof from P of α exists.

In [12] it was noted that ⊢_{ws} is consistent, in the sense that no TSS admits well-supported proofs of two literals that deny each other.

Definition 11 (completeness). A TSS P is complete if for any closed literal p −̸→^{a} either P ⊢_{ws} p ⟶^{a} p′ for some closed term p′ or P ⊢_{ws} p −̸→^{a}.

Now a TSS specifies a transition relation if and only if it is complete. The specified transition relation is then the set of all ws-provable transitions. For positive TSSs, the set of ⊢_{ws}-provable closed positive literals and the set of ⊢- provable closed literals are the same.

Example 1. Let A = {a, b} and P = (Σ, R), where Σ consists of the constant c and the unary function symbol f, and R is:

\frac{x −̸→^{a}}{f(x) ⟶^{b} c}  \frac{c −̸→^{a}}{c ⟶^{a} c}

There are well-supported proofs for the closed negative literals f^{n+1}(c) −̸→^{a} for n ≥ 0 and c −̸→^{b}. In each case, the proof consists of a single node, labelled by the literal itself. Furthermore, there are well-supported proofs for the closed positive literals f^{n+2}(c) ⟶^{b} c for n ≥ 0, where the proof consists of a tree of two nodes: the root has as label the literal itself, and the node above it has label f^{n+1}(c) −̸→^{a}. The TSS P is not complete, since there is no well-supported proof for c −̸→^{a} or c ⟶^{a} p for p ∈ T (Σ); moreover, there is no well-supported proof for

f(c) −̸→^{b} or f(c) ⟶^{b} p for p ∈ T (Σ).

2.3 Formats

We recall the tyft/tyxt format [14] and the ready simulation format [5]. Both formats are restrictions of the ntyft/ntyxt format [13], which was introduced as the most liberal format known to guarantee congruence properties for bisimulation equivalence.

Definition 12 (ntytt). An ntytt rule is a transition rule in which the righthand 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, and an ntyft rule if its source contains exactly one function symbol and no multiple occurrences of variables. An ntytt rule is an nxytt rule if the left-hand sides of its premises are variables. A tytt, tyxt, tyft or xytt rule is an ntytt, ntyxt, ntyft or nxytt rule, respectively, without negative premises. A xyft rule is a tyft rule that is also an xytt rule.

Given a premise t ⟶^{a} y of an ntytt rule, there is a dependency between each variable in t and y. This is captured in the dependency graph of the rule. We will strive for rules in which there is neither infinite forward dependency between variables (bounded lookahead), nor infinite backward dependency between variables (well-foundedness).

Definition 13 (lookahead, well-foundedness). Assume a set of positive Σliterals {t_{i} ⟶^{a_{i}} t′_{i} | i ∈ I}. Its dependency graph is a directed graph, with the collection of variables V as vertices, and with as edges

{⟨x, y⟩ | x and y occur in t_{i} and t′_{i} respectively, for some i ∈ I}.

The dependency graph of a transition rule is the dependency graph of its positive premises. A transition rule is well-founded if any backward chain of edges in its dependency graph is finite. A transition rule has lookahead if there is a variable in the right-hand side of a premise that also occurs in the left-hand side of a premise; the lookahead is bounded if any forward chain of edges in the dependency graph is finite.

Definition 14 (pure). A variable in a transition rule is free if it occurs neither in the source nor in right-hand sides of positive premises of this rule. A rule is pure if it is well-founded and does not contain free variables.

Definition 15 (depth). If r is a pure tytt rule of the form \frac{\{v_{k}⟶^{c_{k}}y_{k}|k∈K\}}{t⟶^{a}u}, then the depth of terms v with var(v) ⊆ var(r) is defined by:

depth_{r}(x) = 0  for x ∈ var(t)
depth_{r}(y_{k}) = depth_{r}(v_{k}) + 1  for k ∈ K
depth_{r}(v) = max{depth_{r}(z) | z ∈ var(v)} if var(v) ⊆ var(r)

This is well-defined since the set of premises is well-founded. When clear from the context, the subscript r will be omitted. For d ≥ 0 we write K_{d} for {k ∈ K | depth(v_{k}) = d}.

Each combination of syntactic restrictions on transition rules induces a corresponding syntactic format of the same name for TSSs. For example, a TSS is in tyft/tyxt format if and only if it contains only tyft and tyxt rules.

Definition 16 (ready simulation format). A TSS is in ready simulation format if it contains only ntyft and ntyxt rules without lookahead.

3 Decomposing HML Formulas

In this section it is shown how one can decompose HML formulas with respect to process terms. Section 3.1 explains what this means. The TSS defining the transition relation on these terms should be in ready simulation format or in tyft/tyxt format, i.e. in ntyft/ntyxt format and either without lookahead or without negative premises.

The decomposition method uses a collection of rules extracted from this TSS, called ruloids. These rules have the property that there is a well-supported proof of a transition p ⟶^{a} q, with p a closed substitution instance of a term t, if and only if there exists a proof that uses at the root a ruloid with source t (Theorems 1 and 2). We require our ruloids to be pure nxytt rules with bounded lookahead. Moreover, when dealing with a TSS without lookahead, the ruloids are required to be without lookahead as well, and when dealing with a TSS without negative premises, the ruloids likewise have to be xytt rules.

The construction of the ruloids for a TSS in ready simulation format stems from Bloom, Fokkink & van Glabbeek [5] and is briefly recalled in Section 3.2. In Section 3.3 we construct ruloids for TSSs in tyft/tyxt format, applying the transformation from tyft/tyxt to pure xyft format from Fokkink & van Glabbeek [9]. An essential new step in the construction is the replacement of any pure nxytt rule by an equivalent rule with bounded lookahead.

The decomposition method is given in Section 3.4, together with the proof that a term t under closed substitution σ satisfies a formula if and only if the variables in t under substitution σ satisfy the formulas given by the decomposition method.

Section 3.6 contains two toy examples to illustrate the method. Section 3.7 features two counterexamples; one to underline the importance that TSSs are complete, and one to show why our two decomposition results for ready simulation and tyft/tyxt format cannot be combined in a straightforward fashion.

3.1 Some Intuition

To explain our decomposition method, we start with an example.

Example 2. Consider the TSS with rules

a.x ⟶^{a} x \frac{x ⟶^{a} x′}{x∥y ⟶^{a} x′∥y} \frac{y ⟶^{a} y′}{x∥y ⟶^{a} x∥y′}

for a ∈ A. The following rules describe all circumstances under which a process x∥y satisfies the modal formula ⟨a⟩⟨b⟩⊤:

\frac{x ⊧ ⟨a⟩⟨b⟩⊤}{x∥y ⊧ ⟨a⟩⟨b⟩⊤} \frac{x ⊧ ⟨a⟩⊤ y ⊧ ⟨b⟩⊤}{x∥y ⊧ ⟨a⟩⟨b⟩⊤} \frac{x ⊧ ⟨b⟩⊤ y ⊧ ⟨a⟩⊤}{x∥y ⊧ ⟨a⟩⟨b⟩⊤} \frac{y ⊧ ⟨a⟩⟨b⟩⊤}{x∥y ⊧ ⟨a⟩⟨b⟩⊤}

In this paper we show how to produce, for any modal formula φ, a complete set of rules for deriving x∥y ⊧ φ, whose premises have the form x ⊧ ψ or y ⊧ ψ. As the number of rules we need grows dramatically in the size of φ, we cannot simply list these rules exhaustively. Instead we generate them with induction on the structure of φ. Let us start with proposing some notation. The set of rules above, all of which share the conclusion x∥y ⊧ ⟨a⟩⟨b⟩⊤, is completely determined by their sets of premises. Each set of premises can be given as a partial function ψ that associates modal formulas ψ(x) to variables x. The second rule, for instance, is given by the partial function ψ_{2}, defined by ψ_{2}(x) = ⟨a⟩⊤ and ψ_{2}(y) = ⟨b⟩⊤. For convenience, we extend these partial functions to total ones—in the first rule above by defining ψ_{1}(y) = ⊤. This is justified because the premise y ⊧ ⊤ is vacuously true for any process y. The set of the four mappings ψ_{1}–ψ_{4} characterising the four rules displayed above is called the modal decomposition of the formula ⟨a⟩⟨b⟩⊤ with respect to the term x∥y in the TSS above. This model decomposition is denoted (x∥y)^{−1}(⟨a⟩⟨b⟩⊤).

In general, for a given term t and a modal formula φ, the modal decomposition t^{−1}(φ) of φ w.r.t. t is a set of requirements ψ_{i}, one of which must be satisfied in order for t to satisfy φ. Each requirement ψ_{i} is given as a mapping from variables to modal formulas; it holds when for all x ∈ var(t) the process represented by x satisfies ψ_{i}(x).

The main contribution of this paper is the definition of t^{−1}(φ) for any HML formula φ and any term t, relative to a complete TSS in ready simulation format or in tyft/tyxt format (Definition 19), together with the theorem that states that this definition is correct (Theorem 3):

For any closed substitution σ, the process σ(t) satisfies φ exactly when there is a mapping ψ in the modal decomposition t^{−1}(φ) such that σ(x) satisfies ψ(x) for all variables x in t.

This model decomposition result can be used to infer the validity of a statement t ⊧ φ by structural induction on t. However, the result is obtained by structural induction on φ.

3.2 Ruloids for the Ready Simulation Format

In the decomposition of modal formulas, we need an important result from [5], where for any TSS P in ready simulation format a collection of pure nxytt rules, called P -ruloids, is constructed. We explain this construction on a rather superficial level; the precise transformation can be found in [5].

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

The resulting TSS, which is in pure ntyft format without lookahead, is denoted by P^{+}. In [5] it is established that P^{+} ⊢ α ⇔ P ⊢_{ws} α for all closed literals α. The notion of irredundant provability is adapted in a straightforward fashion to accommodate rules with a negative conclusion. P -ruloids are the pure nxytt rules without lookahead that are irredundantly provable from P^{+}. The following correspondence result from [5] between a TSS and its ruloids will play a crucial rôle in our decomposition method. It says that, provided we have enough variables to build ruloids, there is a well-supported proof from P of a transition p ⟶^{a} q, with p a closed substitution instance of a term t, if and only if there is a proof of this transition that uses at the root a P -ruloid with source t.

Theorem 1 (Lemma 8.2 from [5], which is Lemma 13 in the report version of [5]). Let the set V of variables be infinite and satisfying |V | ≥ |A|. Let P = (Σ, R) be a TSS in ready simulation format with |Σ| ≤ |V |. Then P ⊢_{ws} σ(t) ⟶^{a} p for t ∈ 𝕋(Σ), p ∈ T (Σ) and σ a closed substitution, if and only if there are a P -ruloid \frac{H}{t⟶^{a}u} and a closed substitution σ′ with P ⊢_{ws} σ′(α) for α ∈ H, σ′(t) = σ(t) and σ′(u) = p.

3.3 Ruloids for the Tyft/Tyxt Format

In this section we construct ruloids for TSSs in tyft/tyxt format (see Theorem 2). We proceed in three steps. First any TSS in tyft/tyxt format is converted into a TSS in pure xyft format, applying a result from [9] (Proposition 2). Then we show that the pure xytt rules irredundantly provable from the resulting TSS satisfy all properties of ruloids, except for having bounded lookahead (Proposition 3). Finally we get rid of unbounded lookahead (Proposition 4).

Proposition 2 ([9], Section 4). Let the set V of variables be infinite. For each TSS P in tyft/tyxt format there is a TSS Q in pure xyft format, such that P ⊢ α ⇔ Q ⊢ α for all closed positive literals α.

Proposition 3. Let the set V of variables be infinite and satisfying |V | ≥ |A|. Let P = (Σ, R) be a TSS in pure tyft format with |Σ| ≤ |V |. Then P ⊢ σ(t) ⟶^{a} p for t ∈ 𝕋(Σ), p ∈ T (Σ) and σ a closed substitution, if and only if there are a pure xytt rule \frac{H}{t⟶^{a}u} and a closed substitution σ′ with P ⊢_{irr} \frac{H}{t⟶^{a}u}, P ⊢ σ′(α) for α ∈ H, σ′(t) = σ(t) and σ′(u) = p.

Before giving the proof of this proposition, we simultaneously illustrate Theorem 1 and Proposition 3 through a TSS in pure tyft format without lookahead. It is based on an example in [9].

Example 3. (A fragment of CCS with replication). Let A be a set of names. The set Ā of co-names is given by Ā = {ā | a ∈ A}, and L = A ∪ Ā is the set of visible actions. The function ¯· is extended to L by declaring ¯ ā = a. Furthermore A = L ∪ {τ} is the set of actions. Note that τ̄ is undefined.

The process algebra CCS has a constant 0, a unary operator a for a ∈ A, binary operators + and |, and a few constructs that are omitted here. In addition we consider the unary replication operator !. The TSS CCS! is given by the pure tyft rules without lookahead below; note that the rule for replication is not xyft. These rules are actually schemata, where a ranges over A.

\begin{matrix}ax ⟶^{a} x & \frac{x ⟶^{a} x′}{x + y ⟶^{a} x′} & \frac{y ⟶^{a} y′}{x + y ⟶^{a} y′} \\ \frac{x ⟶^{a} x′}{x | y ⟶^{a} x′ | y} & \frac{x ⟶^{a} x′ y ⟶^{ā} y′}{x | y ⟶^{τ} x′ | y′} & \frac{y ⟶^{a} y′}{x | y ⟶^{a} x | y′} & \frac{!x | x ⟶^{a} x′}{!x ⟶^{a} x′} \end{matrix}

We give an example application of Proposition 3, with t =!(a0 + x), σ(x) = ā0 and p = (a0 + ā0) | 0 | 0. Note that σ(t) ⟶^{τ} p is part of the transition relation.

Below we depict the construction of an irredundant proof of the pure xytt

rule \frac{x ⟶^{ā} x′}{!(a0 + x) ⟶^{τ} !(a0 + x) | 0 | x′}. Labels of the proof tree are obtained by

applying ρ to the conclusions of the rules in the structure below. Definition 9 of a proof tree does not specify the identity of the nodes that occur in the tree; it merely poses requirements on their labels. Following a convention from [9], we do not depict the hypothesis explicitly, and any other node we take to be an α-conversion of the proof rule applied in that node to obtain its label from the labels of the nodes above it. By choosing the variables in all these rules to be disjoint, we can unite the substitutions applied in each of these nodes into one global substitution ρ.

[figure: \frac{!z | z ⟶^{τ} z′}{!z ⟶^{τ} z′}; \frac{y_{1} ⟶^{a} y′_{1} y_{2} ⟶^{ā} y′_{2}}{y_{1} | y_{2} ⟶^{τ} y′_{1} | y′_{2}}; \frac{x_{2} ⟶^{ā} x′_{2}}{x_{1} + x_{2} ⟶^{ā} x′_{2}}; \frac{!w | w ⟶^{a} w′}{!w ⟶^{a} w′}; \frac{v_{2} ⟶^{a} v′_{2}}{v_{1} | v_{2} ⟶^{a} v_{1} | v′_{2}}; \frac{u_{1} ⟶^{a} u′_{1}}{u_{1} + u_{2} ⟶^{a} u′_{1}}; as ⟶^{a} s]  \begin{aligned}ρ(s) & = & 0 \\ ρ(u_{1}) & = & a0 \\ ρ(u′_{1}) & = & 0 \\ ρ(u_{2}) & = & x \\ ρ(v_{1}) & = & !(a0 + x) \\ ρ(v_{2}) & = & a0 + x \\ ρ(v′_{2}) & = & 0 \\ ρ(w) & = & a0 + x \\ ρ(w′) & = & !(a0 + x) | 0 \\ ρ(x_{1}) & = & a0 \\ ρ(x_{2}) & = & x \\ ρ(x′_{2}) & = & x′ \\ ρ(y_{1}) & = & !(a0 + x) \\ ρ(y′_{1}) & = & !(a0 + x) | 0 \\ ρ(y_{2}) & = & a0 + x \\ ρ(y′_{2}) & = & x′ \\ ρ(z) & = & a0 + x \\ ρ(z′) & = & !(a0 + x) | 0 | x′ \end{aligned}

Moreover, σ′(x) = ā0 and σ′(x′) = 0. Note that σ′(x ⟶^{ā} x′) = ā0 ⟶^{ā} 0 is part of the transition relation.

Proof of Proposition 3: ⇐ Suppose there are a pure xytt rule \frac{H}{t⟶^{a}u} and a closed substitution σ′, with P ⊢_{irr} \frac{H}{t⟶^{a}u}, P ⊢ σ′(α) for α ∈ H, σ′(t) = σ(t) and σ′(u) = p. Let π be an irredundant proof from P of \frac{H}{t⟶^{a}u}. Then a proof of

σ(t) ⟶^{a} p is obtained by taking σ′(π) and replacing each σ′(α) for α ∈ H by a proof of σ′(α).

⇒ Let P ⊢ σ(t) ⟶^{a} p. First, suppose t is a variable. Let y be a different

variable. By definition, the pure xytt rule \frac{t⟶^{a}y}{t⟶^{a}y} is irredundantly provable from P. Let σ′ be a closed substitution with σ′(t) = σ(t) and σ′(y) = p. Clearly,

P ⊢ σ′(t ⟶^{a} y).

Next, suppose t = f(t_{1}, …, t_{ar(f)}). We apply structural induction on a closed proof π from P of σ(t) ⟶^{a} p. Let r ∈ R be the pure tyft rule and ρ with dom(ρ) = var(r) be the closed substitution used at the bottom of π, where r is

of the form \frac{\{v_{k}⟶^{c_{k}}y_{k}|k∈K\}}{f(x_{1},...,x_{ar(f)})⟶^{a}v}. Then ρ(x_{i}) = σ(t_{i}) for i ∈ \{1, …, ar(f)\}, ρ(v) = p,

and ρ(v_{k}) ⟶^{c_{k}} ρ(y_{k}) for k ∈ K are provable from P by means of strict subproofs of π.

We now show how to define two substitutions ρ_{∞} and σ_{∞}, and a pure xytt rule \frac{H}{t⟶^{a}ρ_{∞}(v)} that is irredundantly provable from P, such that P ⊢ σ_{∞}(α) for

α ∈ H and σ_{∞}(t ⟶^{a} ρ_{∞}(v)) = σ(t) ⟶^{a} p. The substitutions ρ_{∞} and σ_{∞} will be given as the “limits” of sequences of substitutions ρ_{d} and σ_{d}, and the set H will be defined in the process. We begin by inductively defining substitutions ρ_{d} and σ_{d} for d ∈ ℕ, such that

dom(ρ_{d}) = {z ∈ var(r) | depth(z) ≤ d}, (1)

var(ρ_{d}(z)) ⊆ dom(σ_{d}) for z ∈ dom(ρ_{d}), and (2)

σ_{d}ρ_{d}(z) = ρ(z) for z ∈ dom(ρ_{d}). (3)

Let ρ_{0} and σ_{0} be substitutions such that

dom(ρ_{0}) = {x_{1}, …, x_{ar(f)}}, (4)

dom(σ_{0}) = var(t), (5)

ρ_{0}(x_{i}) = t_{i} for i ∈ {1, …, ar(f)}, and (6)

σ_{0}(z) = σ(z) for z ∈ var(t). (7)

Note that σ_{0}(z) ∈ T (Σ) for z ∈ dom(σ_{0}).

Properties (1)–(3) hold for d = 0: dom(ρ_{0}) =^{(4)} {z ∈ var(r) | depth(z) ≤ 0},

var(ρ_{0}(x_{i})) =^{(6)}var(t_{i}) ⊆ var(t) =^{(5)}dom(σ_{0}) for i ∈ {1, …, ar(f)}, and σ_{0}ρ_{0}(x_{i}) =^{(6)}

σ_{0}(t_{i}) =^{(7)} σ(t_{i}) = ρ(x_{i}) for i ∈ {1, …, ar(f)}.

Suppose ρ_{d} and σ_{d} have been defined for some d ≥ 0. According to Defini-

tion 15, for k ∈ K_{d} we have depth(v_{k}) = d, so P ⊢ σ_{d}ρ_{d}(v_{k}) =^{(1),(3)} ρ(v_{k}) ⟶^{c_{k}} ρ(y_{k}) by means of a strict subproof of π. By induction on the structure of π there are a pure xytt rule _{\frac{H_{k}}{ρ_{d}(v_{k})⟶^{c_{k}}u_{k}}} and a closed substitution σ′_{k} with

P ⊢_{irr} \frac{H_{k}}{ρ_{d}(v_{k}) ⟶^{c_{k}} u_{k}} , (8)

P ⊢ σ′_{k}(α) for α ∈ H_{k}, (9)

σ′_{k}ρ_{d}(v_{k}) = σ_{d}ρ_{d}(v_{k}), and (10)

σ′_{k}(u_{k}) = ρ(y_{k}). (11)

We define the substitution ρ_{d+1} by:

dom(ρ_{d+1}) = dom(ρ_{d}) ∪ {y_{k} ∈ var(r) | k ∈ K_{d}}, (12)

ρ_{d+1}(z) = ρ_{d}(z) if z ∈ dom(ρ_{d}), and (13)

ρ_{d+1}(y_{k}) = u_{k} for k ∈ K_{d}. (14)

Owing to the assumption that |Σ| ≤ |V | and |A| ≤ |V |, we can choose the sets rhs(H_{k}) for k ∈ K_{d} pairwise disjoint, and disjoint from dom(σ_{d}) (cf. Lemma 6.4 in [5], which is Lemma 6 in the report version of [5]). We define the substitution σ_{d+1} by:

dom(σ_{d+1}) = dom(σ_{d}) ∪ ⋃_{k∈K_{d}}rhs(H_{k}), (15)

σ_{d+1}(z) = σ_{d}(z) if z ∈ dom(σ_{d}), and (16)

σ_{d+1}(z) = σ′_{k}(z) if z ∈ rhs(H_{k}) for some k ∈ K_{d}. (17)

Note that σ_{d+1}(z) ∈ T (Σ) for z ∈ dom(σ_{d+1}).

We proceed to prove (1)–(3) for d + 1, assuming by induction that they hold

for d. First, dom(ρ_{d+1}) =^{(12),(1)} {z ∈ var(r) | depth(z) ≤ d + 1}. Next, we prove that var(ρ_{d+1}(z)) ⊆ dom(σ_{d+1}) for z ∈ dom(ρ_{d+1}).

– Let z ∈ dom(ρ_{d}). Then var(ρ_{d+1}(z)) =^{(13)}var(ρ_{d}(z)) ⊆^{(2)}dom(σ_{d}) ⊆^{(15)}dom(σ_{d+1}).

– Let z = y_{k} for some k ∈ K_{d}. Then var(ρ_{d+1}(z)) =^{(14)} var(u_{k}) ⊆ var(ρ_{d}(v_{k}))∪

rhs(H_{k}) by the pureness of _{\frac{H_{k}}{ρ_{d}(v_{k})⟶^{c_{k}}u_{k}}}. We have var(v_{k}) ⊆^{(1)} dom(ρ_{d}), so

var(ρ_{d}(v_{k})) ⊆^{(2)} dom(σ_{d}) ⊆^{(15)} dom(σ_{d+1}). Further, rhs(H_{k}) ⊆^{(15)} dom(σ_{d+1}).

Finally, we prove that σ_{d+1}ρ_{d+1}(z) = ρ(z) for z ∈ dom(ρ_{d+1}).

– Let z ∈ dom(ρ_{d}). Then σ_{d+1}ρ_{d+1}(z) =^{(13)} σ_{d+1}ρ_{d}(z) =^{(2),(16)} σ_{d}ρ_{d}(z) =^{(3)} ρ(z).

– Let z = y_{k} for some k ∈ K_{d}. Let w ∈ var(ρ_{d}(v_{k})). Then w ∈^{(2)} dom(σ_{d}),

and hence σ_{d+1}(w) =^{(16)} σ_{d}(w). Since σ′_{k}ρ_{d}(v_{k}) =^{(10)} σ_{d}ρ_{d}(v_{k}), it follows that σ_{d}(w) = σ′_{k}(w). Hence

σ_{d+1}(w) = σ′_{k}(w), if w ∈ var(ρ_{d}(v_{k})) for some k ∈ K_{d}. (18)

By the pureness of _{\frac{H_{k}}{ρ_{d}(v_{k})⟶^{c_{k}}u_{k}}}, we have var(u_{k}) ⊆ var(ρ_{d}(v_{k})) ∪ rhs(H_{k}), so

σ_{d+1}ρ_{d+1}(z) =^{(14)} σ_{d+1}(u_{k}) =^{(17),(18)} σ′_{k}(u_{k}) =^{(11)} ρ(z).

Hence, (1)-(3) hold for d + 1.

Now we define a substitution ρ_{∞} with dom(ρ_{∞}) = var(r) as the limit of the ρ_{d}, so

ρ_{∞}(z) = ρ_{d}(z) for z ∈ dom(ρ_{d}) and d ∈ ℕ. (19)

Let H = ⋃_{k∈K} H_{k}. We define a closed substitution σ_{∞} that behaves as the limit of the σ_{d} on variables from var(t) ∪ rhs(H) and maps all other variables to arbitrary closed terms.

σ_{∞}(z) = σ_{d}(z) for z ∈ dom(σ_{d}) and d ∈ ℕ. (20)

The substitutions ρ_{∞} and σ_{∞} are well-defined, owing to (13) and (16). We verify that the rule \frac{H}{t⟶^{a}ρ_{∞}(v)} together with the closed substitution σ_{∞} satisfies the desired properties.

– \frac{H}{t⟶^{a}ρ_{∞}(v)} is pure xytt:

The right-hand sides of the positive premises in any H_{k} are distinct variables. By construction, these sets of variables (one for every k ∈ K) are pairwise disjoint, and disjoint from var(t). Furthermore, the left-hand sides of the premises in any H_{k} are variables. This makes \frac{H}{t⟶^{a}ρ_{∞}(v)} an xytt rule. We prove that this rule does not contain free variables. We consider two cases:

• z is the left-hand side of a premise in H_{k} for some k ∈ K and z ∉ rhs(H). Since _{\frac{H_{k}}{ρ_{∞}(v_{k})⟶^{c_{k}}u_{k}}} is pure, z ∈ var(ρ_{∞}(v_{k})).

• z ∈ var(ρ_{∞}(v)).

Since var(ρ_{∞}(w)) ⊆^{(2)} dom(σ_{∞}) =^{(5),(15)} var(t) ∪ rhs(H) for w ∈ var(r), in either case z ∈ var(t) ∪ rhs(H). We prove that \frac{H}{t⟶^{a}ρ_{∞}(v)} is well-founded. Let y ∈ lhs(H_{k}) ∩ rhs(H_{ℓ}) with

k ∈ K_{d}, ℓ ∈ K_{e} and k ≠ ℓ. We prove that e < d. Since \frac{H}{t⟶^{a}ρ_{∞}(v)} is xytt and

y ∈ rhs(H_{ℓ}), it follows that y ∉ rhs(H_{k}) and y ∉ var(t). Since _{\frac{H_{k}}{ρ_{∞}(v_{k})⟶^{c_{k}}u_{k}}}

is pure and y ∈ lhs(H_{k})\rhs(H_{k}), we have y ∈ var(ρ_{∞}(v_{k})). This implies

that y ∈ var(ρ_{d}(v_{k})) ⊆^{(2)} dom(σ_{d}) ⊆^{(5),(15)} var(t) ∪ ⋃_{k′∈K_{d−1}∪...∪K_{0}} rhs(H_{k′}). Since

y ∉ var(t) and y ∈ rhs(H_{ℓ}) with ℓ ∈ K_{e} we have e ∈ {0, …, d − 1} and thus e < d. Thus, if ⟨x, y⟩ and ⟨y, z⟩ are edges in the dependency graphs of respectively H_{ℓ} with ℓ ∈ K_{e} and H_{k} with k ∈ K_{d} and k ≠ ℓ, then e < d. Moreover, well-foundedness of the rules _{\frac{H_{k}}{ρ_{∞}(v_{k})⟶^{c_{k}}u_{k}}} for k ∈ K implies that

their dependency graphs do not contain infinite backward chains. Hence, the dependency graph of H does not contain an infinite backwards chain of edges either. Therefore, \frac{H}{t⟶^{a}ρ_{∞}(v)} is well-founded.

– P ⊢_{irr} \frac{H}{t⟶^{a}ρ_{∞}(v)}:

Since r ∈ R, we have P ⊢_{irr} ρ_{∞}(r) =^{(6),(14)} \frac{\{ρ_{∞}(v_{k})⟶^{c_{k}}u_{k}|k∈K\}}{t⟶^{a}ρ_{∞}(v)}. Furthermore,

P ⊢_{irr}^{(8)} _{\frac{H_{k}}{ρ_{∞}(v_{k})⟶^{c_{k}}u_{k}}} for k ∈ K. As H = ⋃_{k∈K} H_{k}, it follows that P ⊢_{irr}

\frac{H}{t⟶^{a}ρ_{∞}(v)}.

– P ⊢ σ_{∞}(α) for α ∈ H:

Let α ∈ H. Then there is a k ∈ K such that α ∈ H_{k}, so k ∈ K_{d} for some d ≥ 0. By the pureness of _{\frac{H_{k}}{ρ_{d}(v_{k})⟶^{c_{k}}u_{k}}}, it follows that var(α) ⊆ var(ρ_{d}(v_{k})) ∪

var(rhs(H_{k})), so P ⊢^{(9)} σ′_{k}(α) =^{(17),(18)} σ_{d+1}(α)) =^{(20)} σ_{∞}(α).

– σ_{∞}(t) =^{(7)} σ(t).

– σ_{∞}ρ_{∞}(v) =^{(3)} ρ(v) = p. □

We have now obtained the required ruloids, except that we still have to get rid of unbounded lookahead. We will do this by replacing any ruloid by one with bounded lookahead.

Definition 17 (replacement). We say that a transition rule r can be replaced by a transition rule s if r is a substitution instance of s and for any closed substitution instance \frac{K}{α} of s there is a closed substitution instance \frac{H}{α} of r such that H ⊆ K.

Note that if a transition rule r can be replaced by a transition rule s, the TSSs (Σ, R ∪ {r}) and (Σ, R ∪ {s}) specify the same transition relation.

The following proposition requires an abundance of variables. Whereas for Theorem 1 and Propositions 2 and 3 we merely needed infinitely many variables and |V | ≥ |A| + |Σ|, here we need uncountably many variables and |V | > |Σ|, so that we have |V | > |T (Σ)|.

Proposition 4. Suppose V is uncountable and |Σ| < |V |. Any pure xytt rule r can be replaced by a pure xytt rule s with bounded lookahead with the same conclusion.

Proof: Let r = \frac{H}{α}. Let κ be an infinite cardinal, such that |T (Σ)| < κ ≤ |V |, and let O_{κ} denote the set of sequences of strictly decreasing ordinals that have a cardinality smaller than κ. Let V (r) denote the finite set of variables y_{0} such that r has premises y_{0} ⟶^{a_{1}} y_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} y_{n} for n ≥ 0 with y_{n} occurring in α, and let U(r) be the set of all other variables occurring in r. For every variable x ∈ U(r) and η ∈ O_{κ}, pick a distinct variable x_{η} ∈ V not occurring in r. This is possible because |O_{κ}| = κ. Let s = \frac{K}{α} with

K = {x ⟶^{a} y | (x ⟶^{a} y) ∈ H, y ∈ V (r)} ∪

{x ⟶^{a} y_{λ} | (x ⟶^{a} y) ∈ H, x ∈ V (r), y ∈ U(r), λ < κ} ∪

{x_{η} ⟶^{a} y_{ηλ} | (x ⟶^{a} y) ∈ H, x ∈ U(r), η, ηλ ∈ O_{κ}}.

By definition s is an xytt rule, and if r is pure then so is s. As there are only finitely many variables occurring in α, and there is no infinite chain of strictly decreasing ordinals, the rule s has bounded lookahead. It remains to be shown that r can be replaced by s.

First of all the substitution ξ given by ξ(x_{η}) = x for all x ∈ U(r) and η ∈ O_{κ} shows that r is a substitution instance of s.

Now consider a closed substitution σ. We need to define a closed substitution ρ, such that ρ(H) ⊆ σ(K) and ρ(α) = σ(α). For x ∈ V (r) let ρ(x) = σ(x). Since x ∈ V (r) for x ∈ var(α), ρ(α) = σ(α). Define the relative depth rd(x) of variables x ∈ var(r) by

rd(x) = 0  for x ∈ V (r)
rd(y) = rd(x) + 1 for y ∈ U(r) and (x ⟶^{a} y) ∈ H.

As in Definition 15 this is well-defined because r is well-founded. With induction on the relative depth of x ∈ U(r) we are going to define ρ(x) and S_{x} ⊆ {η ∈ O_{κ} | σ(x_{η}) = ρ(x)} such that |{λ < κ | ∃η ∈ O_{κ} : ηλ ∈ S_{x}}| = κ. Base case: Let x ∈ V (r), y ∈ U(r) and (x ⟶^{a} y) ∈ H. As |T (Σ)| < κ, there must be a set S ⊆ {λ | λ < κ} with |S| = κ and σ(y_{λ}) = σ(y_{λ′}) for λ, λ′ ∈ S.

Let ρ(y) = σ(y_{λ}) for some λ ∈ S. We define S_{y} = S. Then we have ρ(x ⟶^{a} y) =

σ(x ⟶^{a} y_{λ}) ∈ σ(K) for λ ∈ S_{y} and |{λ < κ | ∃η ∈ O_{κ} : ηλ ∈ S_{y}}| = |S_{y}| = κ.

Induction step: Let x ∈ U(r), ρ(x) is already defined, and (x ⟶^{a} y) ∈ H. As |{λ < κ | ∃η ∈ O_{κ} : ηλ ∈ S_{x}}| = κ and hence |{ν | ∃ηλ ∈ S_{x} : ν < λ}| = κ, whereas |T (Σ)| < κ, there must be a set S′ ⊆ {ην ∈ O_{κ} | η ∈ S_{x}} with |{ν < κ | ∃η ∈ O_{κ} : ην ∈ S′}| = κ and σ(y_{η}) = σ(y_{η′}) for η, η′ ∈ S′. Let ρ(y) = σ(y_{ην}) for some ην ∈ S′. We define S_{y} = S′. Then we have ρ(x ⟶^{a} y) = σ(x_{η} ⟶^{a} y_{ην}) ∈ σ(K) for ην ∈ S_{y}. Hence, ρ(H) ⊆ σ(K). So r can be replaced by s. □

In the following definition of a ruloid and the forthcoming Theorems 2 and 3 we assume the existence of sufficiently many variables (satisfying the conditions of Propositions 3 and 4). However, this assumption will be discharged in Section 3.5, showing that our mail result (Theorem 3) will hold regardless.

Definition 18 (ruloid). Let P be a TSS in tyft/tyxt format. According to Proposition 2 there is a TSS Q in pure xyft format, such that P ⊢ α ⇔ Q ⊢ α for all closed positive literals α. The set of P -ruloids is obtained by first taking the set of pure xytt rules, irredundantly provable from Q, and next replacing each of these pure xytt rules by one with bounded lookahead, using Proposition 4.

Theorem 2. Suppose V is uncountable and |A| ≤ |V |. Let P = (Σ, R) be a TSS in tyft/tyxt format with |Σ| < |V |. Then P ⊢ σ(t) ⟶^{a} p for t ∈ 𝕋(Σ), p ∈ T (Σ) and σ a closed substitution, if and only if there are a P -ruloid \frac{H}{t⟶^{a}u} and a closed substitution σ′ with P ⊢ σ′(α) for α ∈ H, σ′(t) = σ(t) and σ′(u) = p.

Proof: According to Proposition 2 there is a TSS Q in pure xyft format, such that P ⊢ α ⇔ Q ⊢ α for all closed positive literals α.

⇒ Suppose P ⊢ σ(t) ⟶^{a} p. Then Q ⊢ σ(t) ⟶^{a} p. According to Proposition 3 (⇒), there are a pure xytt rule \frac{G}{t⟶^{a}u} and a closed substitution σ′ with

Q ⊢_{irr} \frac{G}{t⟶^{a}u}, Q ⊢ σ′(α) for α ∈ G, σ′(t) = σ(t) and σ′(u) = p. Replace \frac{G}{t⟶^{a}u}

by the P -ruloid \frac{H}{t⟶^{a}u}, using Proposition 4. According to Definition 17, there is a substitution σ′′ such that σ′′(\frac{H}{t⟶^{a}u}) = \frac{G}{t⟶^{a}u}. Hence Q ⊢ σ′σ′′(α) for α ∈ H, σ′′(t) = t and σ′′(u) = u. Thus for the P -ruloid \frac{H}{t⟶^{a}u} and the closed substitution σ′σ′′ we have P ⊢ σ′σ′′(α) for α ∈ H, σ′σ′′(t) = σ′(t) = σ(t) and σ′σ′′(u) = σ′(u) = p.

⇐ Suppose there are a P -ruloid \frac{H}{t⟶^{a}u} and a closed substitution σ′ with P ⊢ σ′(α) for α ∈ H, σ′(t) = σ(t) and σ′(u) = p. Then Q ⊢ σ′(α) for α ∈ H. \frac{H}{t⟶^{a}u} is a replacement of a pure xytt rule \frac{G}{t⟶^{a}u} irredundantly provable from Q. According to Definition 17, for σ′(\frac{H}{t⟶^{a}u}) there is a closed substitution σ′′ such that σ′′(G) ⊆ σ′(H), σ′′(t) = σ′(t) and σ′′(u) = σ′(u). Since Q ⊢ σ′(α) for α ∈ H, we have Q ⊢ σ′′(α) for α ∈ G. Thus according to Proposition 3 (⇐) we

have Q ⊢ σ(t) ⟶^{a} p, so P ⊢ σ(t) ⟶^{a} p. □

3.4 Decomposition of HML Formulas

Given a TSS P = (Σ, R) in tyft/tyxt format or in ready simulation format, the following definition assigns to each term t ∈ 𝕋(Σ) and each observation φ ∈ 𝕆 a collection t_{P}^{−1}(φ) of decomposition mappings ψ : V → 𝕆. Each of these mappings ψ ∈ t_{P}^{−1}(φ) guarantees, given a closed substitution σ, that σ(t) satisfies φ if σ(x) satisfies the formula ψ(x) for all x ∈ var(t). Moreover, whenever for some closed substitution σ the term σ(t) satisfies φ, there must be a ψ ∈ t_{P}^{−1}(φ) with σ(x) satisfying ψ(x) for all x ∈ var(t). This is formalised in Theorem 3.

Definition 19. Let P = (Σ, R) be a TSS in tyft/tyxt format (resp. ready simulation format) and assume that the set V of variables is infinite, with |V | ≥ |A| and |V | > |Σ|. Then ·_{P}^{−1} : 𝕋(Σ) → (𝕆 → 𝒫(V → 𝕆)) is defined by:

– ψ ∈ t_{P}^{−1}(⟨a⟩φ) iff there is a P -ruloid \frac{H}{t⟶^{a}u} and a χ ∈ u_{P}^{−1}(φ) and ψ : V → 𝕆 is given by

ψ(x) = \begin{cases}⋀_{(x⟶^{b}y)∈H} ⟨b⟩ψ(y) ∧ ⋀_{(x−̸→^{c})∈H} ¬⟨c⟩⊤ ∧ χ(x) & if x ∈ var(u) \\ ⋀_{(x⟶^{b}y)∈H} ⟨b⟩ψ(y) ∧ ⋀_{(x−̸→^{c})∈H} ¬⟨c⟩⊤ & if x ∉ var(u) \end{cases}

– ψ ∈ t_{P}^{−1}(⋀_{i∈I} φ_{i}) iff

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

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

– ψ ∈ t_{P}^{−1}(¬φ) iff there is a function h : t_{P}^{−1}(φ) → var(t) and ψ : V → 𝕆 is given by

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

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

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

Each ψ(x) in Definition 19 is a HML formula, owing to the fact that the rule \frac{H}{t⟶^{a}u} in the definition of t_{P}^{−1}(⟨a⟩φ) has bounded lookahead. When clear from the context, subscripts P will be omitted.

Theorem 3. Let P = (Σ, R) be a complete TSS in tyft/tyxt format (resp. ready simulation format). For any t ∈ 𝕋(Σ), σ : V → T (Σ) and φ ∈ 𝕆:

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

Proof: With induction on the structure of φ. Here we assume that V is infinite, |V | ≥ |A| and |V | > |Σ|. This assumption will be discharged in Section 3.5.

– φ = ⟨a⟩φ′ ⇒ Suppose σ(t) ⊧ ⟨a⟩φ′. Then by Definition 3 there is a p ∈ T (Σ) with P ⊢_{ws} σ(t) ⟶^{a} p and p ⊧ φ′. Thus, by Theorem 2 (resp. Theorem 1) there must be a P -ruloid \frac{H}{t⟶^{a}u} and a closed substitution σ′ with P ⊢_{ws} σ′(α) for α ∈ H, σ′(t) = σ(t), i.e. σ′(x) = σ(x) for x ∈ var(t), and σ′(u) = p. Since σ′(u) ⊧ φ′, the induction hypothesis can be applied, and there must be a χ ∈ u^{−1}(φ′) such that σ′(z) ⊧ χ(z) for all z ∈ var(u). Now define ψ ∈ t^{−1}(⟨a⟩φ′) as indicated in Definition 19, using \frac{H}{t⟶^{a}u} and χ. For (x ⟶^{b} y) ∈ H one has

P ⊢_{ws} σ′(x) ⟶^{b} σ′(y). Moreover, for (x −̸→^{c}) ∈ H one has P ⊢_{ws} σ′(x) −̸→^{c}, so the consistency of ⊢_{ws} yields P ⊬_{ws} σ′(x) ⟶^{c} q for all q ∈ T (Σ), and thus σ′(x) ⊧ ¬⟨c⟩⊤. We proceed to prove that σ′(x) ⊧ ψ(x) for x ∈ V. We apply ordinal induction on the lookahead of x in H, which is defined by

sup{1 + lookahead of y in H | x ⟶^{b} y ∈ H for some b ∈ A}

Since \frac{H}{t⟶^{a}u} has bounded lookahead, the lookahead of x in H is a well-defined ordinal number. We distinguish two cases.

x ∈ var(u). Then ψ(x) = ⋀_{(x⟶^{b}y)∈H}⟨b⟩ψ(y) ∧ ⋀_{(x−̸→^{c})∈H} ¬⟨c⟩⊤ ∧ χ(x). By

induction on lookahead σ′(y) ⊧ ψ(y), so σ′(x) ⊧ ⟨b⟩ψ(y) for (x ⟶^{b} y) ∈ H. Since moreover σ′(x) ⊧ ¬⟨c⟩⊤ for (x −̸→^{c}) ∈ H and σ′(x) ⊧ χ(x), it follows that σ′(x) ⊧ ψ(x).

x ∉ var(u). Then ψ(x) = ⋀_{(x⟶^{b}y)∈H}⟨b⟩ψ(y) ∧ ⋀_{(x−̸→^{c})∈H} ¬⟨c⟩⊤. By induc-

tion on lookahead σ′(y) ⊧ ψ(y), so σ′(x) ⊧ ⟨b⟩ψ(y) for (x ⟶^{b} y) ∈ H. Since moreover σ′(x) ⊧ ¬⟨c⟩⊤ for (x −̸→^{c}) ∈ H, it follows that σ′(x) ⊧ ψ(x).

Finally, σ(x) = σ′(x) ⊧ ψ(x) for x ∈ var(t). ⇐ Suppose that there is a ψ ∈ t^{−1}(⟨a⟩φ′) such that σ(x) ⊧ ψ(x) for all x ∈ var(t). Let ψ be defined in terms of the P -ruloid \frac{H}{t⟶^{a}u} and χ ∈ u^{−1}(φ′). We define a closed substitution σ′ with as domain the variables in this P - ruloid such that:

σ′(t) = σ(t), (21)

P ⊢_{ws} σ′(x) ⟶^{b} σ′(y) for (x ⟶^{b} y) ∈ H, (22)

P ⊢_{ws} σ′(x) −̸→^{c} for (x −̸→^{c}) ∈ H; and (23)

σ′(y) ⊧ ψ(y) for y ∈ dom(σ′). (24)

σ′(y) is defined by induction on the depth of y in the P -ruloid.

• depth(y) = 0. Then y ∈ var(t). We define σ′(y) = σ(y). This yields property (21). Moreover, property (24) for y holds. The formula ψ(y) contains the conjunct ¬⟨c⟩⊤ for (y −̸→^{c}) ∈ H, so by the completeness of P, property (24) for y implies property (23) for y.

• depth(y) > 0. Let x ⟶^{b} y be the positive premise in the P -ruloid with right-hand side y. By induction, σ′(x) is already defined. By property (24), σ′(x) ⊧ ψ(x), so σ′(x) ⊧ ⟨b⟩ψ(y). Hence, P ⊢_{ws} σ′(x) ⟶^{b} p for some p ∈ T (Σ) with p ⊧ ψ(y). We define σ′(y) = p. Then property (22) for the premise x ⟶^{b} y and property (24) for y hold. By the completeness of P, property (24) for y implies that property (23) for y holds as well. Since ψ(z) implies χ(z) for z ∈ var(u), property (24) yields σ′(y) ⊧ χ(y) for y ∈ var(u). Thus the induction hypothesis can be applied, so σ′(u) ⊧ φ′. By properties (21)–(23) together with Theorem 2 (resp. Theorem 1), P ⊢_{ws}

σ(t) ⟶^{a} σ′(u). Hence, σ(t) ⊧ ⟨a⟩φ′.

– φ = ⋀_{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). □

3.5 Counting variables

So far we have developed a modal decomposition method that applies to arbitrary languages with a structural operational semantics in tyft/tyxt format or in ready simulation format, provided that we have an uncountable set of variables whose cardinality exceeds the cardinality of the collection of operators in the language, and at least equals the cardinality of the set of actions. In computer science applications, however, it is customary to work with countable sets of variables. Here we show that our decomposition result applies regardless of the cardinality of the set of variables.

Assume a given set of true variables V_{true}. These are the only ones that are used in a given application. Now, given a set of actions A and a TSS P = (Σ, R), we define an uncountable set V ⊇ V_{true} satisfying |V | ≥ |A| and |V | > |Σ|. The elements of V are called variables and variables in V −V_{true} are virtual variables.

As long as only the true variables appear in TSSs and specifications of processes, nothing stops us from defining any amount of virtual variables to be used in our constructions. Terms, TSSs, ruloids and other syntactic constructions are called true if they only contain true variables, and virtual otherwise.

Theorems 1 and 2 (our intermediate results) apply merely to virtual ruloids; they may fail to hold for true ruloids. Definition 19 on the other hand provides a modal decomposition t^{−1}(φ) for any virtual term t (and any HML formula φ), and thus surely for every true term t. Such a modal decomposition consists of a set of decomposition mappings ψ, each of which allocates an HML formula ψ(x) to every variable x. As only the ψ(x) for x ∈ var(t) play a rôle in Theorem 3, nothing is lost by restricting the domain of ψ(x) to var(t). (This is an a posteriori restriction; virtual variables may have been used in the definition of ψ(x).) Using this restriction of the decomposition mappings, Theorem 3 restricts to a valid statement involving true variables only.

3.6 Examples

We give two examples of the application of Theorem 3.

Example 4. Let A = {a, b} and P = (Σ, R), where Σ consists of the constant c and the binary function symbol f, and R is:

c ⟶^{a} c  \frac{x_{1} ⟶^{a} y}{f(x_{1}, x_{2}) ⟶^{b} y}  \frac{x_{2} ⟶^{a} y x_{1} −̸→^{b}}{f(x_{1}, x_{2}) ⟶^{b} y}

This TSS is complete and in ready simulation format. We proceed to compute f(x_{1}, x_{2})^{−1}(⟨b⟩⊤). The only two P -ruloids (modulo α-conversion) with a conclusion f(x_{1}, x_{2}) ⟶^{b} are

\frac{x_{1} ⟶^{a} y}{f(x_{1}, x_{2}) ⟶^{b} y}  \frac{x_{2} ⟶^{a} y x_{1} −̸→^{b}}{f(x_{1}, x_{2}) ⟶^{b} y}

According to Definition 19, f(x_{1}, x_{2})^{−1}(⟨b⟩⊤) = {ψ_{1}, ψ_{2}} where ψ_{1} and ψ_{2} are defined as follows, using some χ ∈ y^{−1}(⊤) (so χ(x) = ⊤ for all x ∈ V):

ψ_{1}(y) = χ(y) = ⊤  ψ_{2}(y) = χ(y) = ⊤
ψ_{1}(x_{1}) = ⟨a⟩ψ_{1}(y) = ⟨a⟩⊤ ψ_{2}(x_{1}) = ¬⟨b⟩⊤
ψ_{1}(z) = ⊤ if z ∉ {y, x_{1}}  ψ_{2}(x_{2}) = ⟨a⟩ψ_{2}(y) = ⟨a⟩⊤
ψ_{2}(z) = ⊤ if z ∉ {y, x_{1}, x_{2}}

So by Theorem 3 a closed term f(p_{1}, p_{2}) can execute a b if and only if p_{1} can execute an a, or p_{1} cannot execute a b and p_{2} can execute an a.

We proceed to compute f(x_{1}, x_{2})^{−1}(¬⟨b⟩⊤). There are four possible functions h : f(x_{1}, x_{2})^{−1}(⟨b⟩⊤) → var(f(x_{1}, x_{2})), yielding four possible definitions of ψ ∈ f(x_{1}, x_{2})^{−1}(¬⟨b⟩⊤). In all four cases, ψ(z) = ⊤ for z ∉ {x_{1}, x_{2}}.

1. If h(ψ_{1}) = h(ψ_{2}) = x_{1} then

\begin{matrix}ψ(x_{1}) = ¬ψ_{1}(x_{1}) ∧ ¬ψ_{2}(x_{1}) = ¬⟨a⟩⊤ ∧ ¬¬⟨b⟩⊤ = ¬⟨a⟩⊤ ∧ ⟨b⟩⊤ \\ ψ(x_{2}) = ⊤ \end{matrix}

2. If h(ψ_{1}) = h(ψ_{2}) = x_{2} then

\begin{matrix}ψ(x_{1}) = ⊤ \\ ψ(x_{2}) = ¬ψ_{1}(x_{2}) ∧ ¬ψ_{2}(x_{2}) = ¬⊤ ∧ ¬⟨a⟩⊤ \end{matrix}

3. If h(ψ_{1}) = x_{1} and h(ψ_{2}) = x_{2} then

\begin{matrix}ψ(x_{1}) = ¬ψ_{1}(x_{1}) = ¬⟨a⟩⊤ \\ ψ(x_{2}) = ¬ψ_{2}(x_{2}) = ¬⟨a⟩⊤ \end{matrix}

4. If h(ψ_{1}) = x_{2} and h(ψ_{2}) = x_{1} then

\begin{matrix}ψ(x_{1}) = ¬ψ_{2}(x_{1}) = ¬¬⟨b⟩⊤ = ⟨b⟩⊤ \\ ψ(x_{2}) = ¬ψ_{1}(x_{2}) = ¬⊤ \end{matrix}

By Theorem 3 a closed term f(p_{1}, p_{2}) cannot execute a b if and only if either (1) p_{1} can execute a b but not an a, or (3) neither p_{1} nor p_{2} can execute an a. The other two possibilities (2) and (4) do not qualify, since no term can ever satisfy ¬⊤.

Example 5. Let A = {a, b} and P = (Σ, R), where Σ consists of the constant c and the unary function symbol f, and R is:

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

This TSS is complete and in tyft/tyxt format. We compute f(f(x))^{−1}(⟨b⟩⟨a⟩⊤). The only P -ruloid (modulo α-conversion) with a conclusion f(f(x)) ⟶^{b} is

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

So for each ψ ∈ f(f(x))^{−1}(⟨b⟩⟨a⟩⊤) we have ψ(x) = ⟨b⟩ψ(y) = ⟨b⟩(⟨a⟩ψ(z) ∧ χ(y)) = ⟨b⟩(⟨a⟩⊤ ∧ χ(y)) with χ ∈ f(y)^{−1}(⟨a⟩⊤). The only P -ruloid (modulo α-conversion) with a conclusion f(y) ⟶^{a} is

\frac{y ⟶^{b} z z ⟶^{a} w}{f(y) ⟶^{a} f(z)}

So χ(y) = ⟨b⟩χ(z) = ⟨b⟩(⟨a⟩χ(w) ∧ χ′(z)) = ⟨b⟩(⟨a⟩⊤ ∧ χ′(z)) for some χ′ ∈ f(z)^{−1}(⊤). Since χ′(z) = ⊤, ψ(x) = ⟨b⟩(⟨a⟩⊤ ∧ ⟨b⟩⟨a⟩⊤).

By Theorem 3 a closed term f(f(p)) can execute a b followed by an a if and only if p ⟶^{b} p′ where p′ can execute an a and also a b followed by an a.

3.7 Counterexamples

The following example shows that in Theorem 3 it is essential that the TSS is complete. That is, the result would fail if we took the transition relation induced by a TSS to consist of those transitions for which a well-supported proof exists.

Example 6. Let A = {a, b} and P = (Σ, R), where Σ consists of the constant c and the unary function symbol f, and R is:

\frac{x −̸→^{a}}{f(x) ⟶^{b} c}  \frac{c −̸→^{a}}{c ⟶^{a} c}

As shown in Example 1, this TSS, which is in ready simulation format, is incomplete. In particular, neither P ⊢_{ws} c ⟶^{a} p for a closed term p nor P ⊢_{ws} c −̸→^{a}.

Let us assume that the transition relation induced by this TSS consists of those transitions for which a well-supported proof exists. Then there is no atransition for c and no b-transition for f(c), so c ⊧_{P} ¬⟨a⟩⊤ and f(c) ⊧_{P} ¬⟨b⟩⊤.

The only P -ruloid with a conclusion f(x) ⟶^{b} is \frac{x−̸→^{a}}{f(x)⟶^{b}c}. Hence Theorem 3

would yield f(c) ⊧_{P} ⟨b⟩⊤ ⇔ c ⊧_{P} ¬⟨a⟩⊤. Since this is false, Theorem 3 would fail with respect to P.

Finally, we argue that Theorem 1 and Theorem 2 cannot be combined in a straightforward fashion to apply to TSSs that contain both bounded lookahead and negative premises.

Example 7. Let A = {a, b} and P = (Σ, R), where Σ consists of the constant 0, the unary function symbols a , b and f and the binary function symbol + , and R is as follows for all m ∈ A:

\frac{x ⟶^{m} x′}{x + y ⟶^{m} x′}  \frac{y ⟶^{m} y′}{x + y ⟶^{m} y′}  mx ⟶^{m} x

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

This TSS is complete and in nxyft format. Note that for closed substitutions σ,

σ(f(f(x))) ⊧ ⟨b⟩⊤
⇔ σ(f(x)) ⊧ ⟨a⟩(¬⟨b⟩⊤)
⇔ σ(x)  ⊧ ⟨a⟩¬(⟨a⟩¬⟨b⟩⊤)

Suppose that there would exist a notion of P -ruloids, being nxytt rules, such that P ⊢_{ws} σ(f(f(x))) ⟶^{a} 0 for σ a closed substitution if and only if there are a P -ruloid \frac{H}{f(f(x))⟶^{a}u} and a closed substitution σ′ with P ⊢_{ws} σ′(α) for α ∈ H,

σ′(x) = σ(x) and σ′(u) = 0. In that case we would have, as in Theorem 3, that for all closed substitutions σ,

σ(f(f(x))) ⊧ ⟨b⟩⊤ ⇔ ∃ψ ∈ f(f(x))^{−1}(⟨b⟩⊤) : σ(x) ⊧ ψ(x)

However, according to Definition 19, for each ψ ∈ f(f(x))^{−1}(⟨b⟩⊤) and y ∈ V, ψ(y) does not contain nested negations, whereas the formula ⟨a⟩¬(⟨a⟩¬⟨b⟩⊤) above cannot be written as a (possibly infinite) disjunction of HML formulas (as defined in Definition 2) without nested negations. The latter follows because the formula ⟨a⟩¬(⟨a⟩¬⟨b⟩⊤) distinguishes the two process of Figure 1—yet these processes are 2-nested simulation equivalent [14] and 2-nested equivalent processes cannot be distinguished by HML formulas without nested negations [14].

[figure: a; a; a; b; a; a; b; a(a0 + ab0) + aab0; ⊧ ⟨a⟩¬(⟨a⟩¬⟨b⟩⊤); a; a; a; b; a(a0 + ab0); |̸= ⟨a⟩¬(⟨a⟩¬⟨b⟩⊤)]

Fig. 1. Two 2-nested simulation equivalent processes that can be distinguished by the HML formula with nested negations ⟨a⟩¬(⟨a⟩¬⟨b⟩⊤)

4 Bisimulation as a Congruence

In [14], Groote & Vaandrager introduced the tyft/tyxt format, and proved that on any LTS specified by a well-founded TSS in tyft/tyxt format, bisimulation equivalence is a congruence, i.e. is preserved by all functions in the signature. Fokkink & van Glabbeek showed in [9] that the well-foundedness condition can be dropped, by constructing for each TSS in tyft/tyxt format an equivalent TSS that consists of pure xyft rules only. In this section we show that the congruence result for TSSs in tyft/tyxt format is a corollary of Theorem 3.

Corollary 1. Let P = (Σ, R) be a TSS in tyft/tyxt format, t ∈ 𝕋(Σ) and σ, σ′ closed substitutions. If σ(x) \underline{↔} σ′(x) for x ∈ var(t), then σ(t) \underline{↔} σ′(t).

Proof: In light of Proposition 1, it suffices to show that σ(t) and σ(t′) satisfy the same formulas from 𝕆. Let σ(t) ⊧ φ ∈ 𝕆. By Theorem 3 there is a ψ ∈ t^{−1}(φ) such that σ(x) ⊧ ψ(x) for x ∈ var(t). Since ψ(x) ∈ 𝕆 and σ(x) \underline{↔} σ′(x) for x ∈ var(t), it follows by Proposition 1 that σ′(x) ⊧ ψ(x) for x ∈ var(t). So by Theorem 3, σ′(t) ⊧ φ. By symmetry, σ′(t) ⊧ φ ∈ 𝕆 implies σ(t) ⊧ φ. □

Likewise, it follows from Theorem 3 that on any LTS specified by a complete TSS in ready simulation format, bisimulation equivalence is a congruence. This is a special case of the congruence result from [7, 9] for complete TSSs in ntyft/ntyxt format.

Bloom, Fokkink & van Glabbeek [5] showed how the decomposition method of modal formulas can be used to obtain general congruence formats for a wide range of behavioural semantics. The idea is to take as a starting point the modal characterization of the semantics under scrutiny, this being a set O of HML formulas such that two processes are semantically equivalent if and only if they make true the same formulas in O. The congruence format for this semantics should guarantee that the decomposition of a formula in O always produces formulas in O. With the decomposition method in the current paper, we could use this same approach to produce congruence formats that include lookahead. We leave this as future work.

References

1. H. R. Andersen (1995): Partial model checking. In Proceedings Tenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, San Diego, California, pp. 398–407.

2. H.R. Andersen, C. Stirling & G. Winskel (1994): A compositional proof system for the modal μ-calculus. In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 144–153.

3. H.R. Andersen & G. Winskel (1992): Compositional checking of satisfaction. Formal Methods in System Design 1(4), pp. 323–354.

4. H. Barringer, R. Kuiper & A. Pnueli (1984): Now you may compose temporal logic specifications. In ACM Symposium on Theory of Computing (STOC ’84), ACM Press, pp. 51–63.

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

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

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

8. S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599.

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

10. W.J. Fokkink, R.J. van Glabbeek & P. de Wind (2003): Compositionality of Hennessy-Milner logic through structural operational semantics. In A. Lingas & B.J. Nilsson, editors: 14^{th} International Symposium on Fundamentals of Computation Theory (FCT ’03), LNCS 2751, Springer, pp. 412–422.

11. R.J. van Glabbeek (2001): The linear time – branching time spectrum I: The semantics of concrete, sequential processes. In J.A. Bergstra, A. Ponse & S.A. Smolka, editors: Handbook of Process Algebra, chapter 1, Elsevier, pp. 3–99.

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

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

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

15. D. Harel, D. Kozen & R. Parikh (1982): Process logic: Expressiveness, decidability, completeness. Journal of Computer and System Sciences 25(2), pp. 144–170.

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

17. M.C.B. Hennessy & C. Stirling (1985): The power of the future perfect in program logics. Information and Control 67, pp. 23–52.

18. D. Kozen (1983): Results on the propositional μ-calculus. Theoretical Computer Science 27(3), pp. 333–354.

19. F. Laroussinie & K. G. Larsen (1995): Compositional model checking of real time systems. In I. Lee & S. A. Smolka, editors: CONCUR ’95: Concurrency Theory, 6th Conference, LNCS 962, Springer-Verlag, pp. 27–41.

20. K.G. Larsen (1986): Context-Dependent Bisimulation between Processes. PhD thesis, University of Edinburgh, Edinburgh.

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

22. R. Milner (1980): A Calculus of Communicating Systems. Springer. LNCS 92.

23. R. Milner (1981): A modal characterization of observable machine-behaviour. In E. Astesiano & C. Böhm, editors: CAAP ’81: Trees in Algebra and Programming, 6^{th} Colloquium, LNCS 112, Springer, pp. 25–34.

24. R. Milner (1983): Calculi for synchrony and asynchrony. Theoretical Computer Science 25(3), pp. 267–310.

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

26. A. Pnueli (1981): The temporal logic of concurrent programs. Theoretical Computer Science 13, pp. 45–60.

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

28. A. Simpson (2004): Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS. Journal of Logic and Algebraic Programming 60/61, pp. 287–322.

29. C. Stirling (1985): A proof-theoretic characterization of observational equivalence. Theoretical Computer Science 39(1), pp. 27–45.

30. C. Stirling (1985): A complete modal proof system for a subset of SCCS. In H. Ehrig, C. Floyd, M. Nivat & J.W. Thatcher, editors: Mathematical Foundations of Software Development: Proceedings of the Joint Conference on Theory and Practice of Software Development (TAPSOFT), Volume 1: Colloquium on Trees in Algebra and Programming (CAAP ’85), LNCS 185, Springer, pp. 253–266.

31. C. Stirling (1985): A complete compositional modal proof system for a subset of CCS. In W. Brauer, editor: Automata, Languages and Programming, 12th Colloquium (ICALP ’85), LNCS 194, Springer, pp. 475–486.

32. C. Stirling (1987): Modal logics for communicating systems. Theoretical Computer Science 49(2-3), pp. 311–347.

33. G. Winskel (1986): A complete proof system for SCCS with modal assertions. Fundamenta Informaticae IX, pp. 401–420.

34. G. Winskel (1990): On the compositional checking of validity (extended abstract). In J.C.M. Baeten & J.W. Klop, editors: CONCUR ’90: Theories of Concurrency: Unification and Extension, LNCS 458, Springer, pp. 481–501.