Compositionality of Hennessy-Milner Logic through Structural Operational Semantics^{⋆}

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

1 CWI, Department of Software Engineering PO Box 94079, 1090 GB Amsterdam, The Netherlands 2 Vrije Universiteit Amsterdam, Department of Theoretical Computer Science De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands

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

Abstract. This paper presents a method for the decomposition of HML formulae. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulae, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is that an earlier decomposition method from Larsen [14] for the De Simone format is extended to the more general ntyft/ntyxt format without lookahead.

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 the components of the composition. Most research papers in this area focus on a particular process algebra.

Barringer, Kuiper & Pnueli [3] present (a preliminary version of) a compositional proof system for concurrent programs, which is based on a rich temporal logic, including operators from process logic [10] and LTL [20]. For modelling concurrent programs they define a language including assignment, conditional and while statements. Interaction between parallel components is done via shared variables.

In Stirling [22] modal proof systems are developed for subsets of CCS [16] (with and without silent actions) including only sequential and alternative composition, to decide the validity of formulae from Hennessy-Milner Logic (HML) [11]. In Stirling [23, 24] the results from [22] are extended, creating proof sys-

⋆ To appear in: Proc. 14th International Symposium on Fundamentals of Computation Theory, Malmö, Sweden, LNCS, Springer, August 2003. \begin{matrix}c \\ ◯ \end{matrix} Springer-Verlag

tems for subsets of CCS and SCCS [18] including asynchronous and synchronous parallelism and infinite behaviour, using ideas from [3]. In Stirling [25] the proposals in [23, 24] are generalised to be able to cope with the restriction operator.

In Winskel [26] a method is given to decompose formulae 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 [27], [2] and [1] processes are described by specification languages inspired by CCS and CSP [6]. The articles describe compositional methods for deciding whether processes satisfy assertions from a modal μ-calculus [13].

Larsen [14] developed 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 [19], 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 formulae with respect to a transition system specification in the De Simone format [21]. 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. Larsen and Xinxin [15] 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., [23–25]). 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., [22, 26]).

In Bloom, Fokkink & van Glabbeek [4] a method is given for decomposing formulae from a fragment of HML with infinite conjunctions, with respect to terms from any process algebra that has a structural operational semantics in ntyft/ntyxt format [9] without lookahead. 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 [8].

In this paper the decomposition method from [4] is extended to full HML with infinite conjunction, again with respect to terms from any process algebra that has a structural operational semantics in ntyft/ntyxt format without lookahead.

2 Preliminaries

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

2.1 Structural Operational Semantics

Structural operational semantics [19] 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 an infinite set of variables. A syntactic object is called closed if it does not contain any variables from V.

Definition 1 (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. For t ∈ 𝕋(Σ), var(t) denotes the set of variables that occur in t. T (Σ) is the set of closed terms over Σ, i.e. the terms t ∈ 𝕋(Σ) with var(t) = ∅. A Σ-substitution σ is a partial function from V to 𝕋(Σ). 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 it is a total function from V to T (Σ).

In the remainder, let Σ denote a signature and A a set of actions, satisfying |Σ| ≤ |V | and |A| ≤ |V |.

Definition 2 (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 3 (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). 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 4 (transition system specification). A transition system specification (TSS) is a pair (Σ, R) with R a collection of transition rules over Σ.

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

– the root is labelled by α,

– H contains the labels of the hypotheses, and

– if β is the label of a node q which is not an 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.

If a proof of \frac{K}{α} from P exists, then \frac{K}{α} is provable from P, notation P ⊢ \frac{K}{α}.

Definition 6 (transition relation). A transition relation over Σ is a relation

→ ⊆ T (Σ) × A × T (Σ). We write p ⟶^{a} q for (p, a, q) ∈ → and p −̸→^{a} for

¬∃q ∈ T (Σ) : p ⟶^{a} q.

Thus a transition relation over Σ can be regarded as a set of closed positive Σ-literals (transitions). 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 in Groote [9], Bol & Groote [5] and van Glabbeek [7]. From the latter we adopt the notion of a well-supported proof and a complete TSS.

Definition 7 (well-supported proof). Let P = (Σ, R) be a TSS. A wellsupported proof of a closed literal α from P is a well-founded, upwardly branching tree of which the 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 negative closed 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 of α from P exists.

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

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

2.2 Hennessy-Milner Logic

A variety of modal logics have been developed to express properties of transition relations. Modal logic aims to formulate properties of process terms, and to identify terms that satisfy the same properties. Hennessy & Milner [11] have defined a modal language, often called Hennessy-Milner Logic (HML), which characterises the bisimulation equivalence relation on process terms, assuming that each term has only finitely many outgoing transitions. This assumption can be discarded if infinite conjunctions are allowed [17, 12].

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

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

with a ∈ A and I some index set.

Definition 10 (satisfaction relation). Let P = (Σ, R) be a TSS. The satisfaction relation ⊧_{P} ⊆ T (Σ) × 𝕆 is defined as follows, with p ∈ T (Σ):

p ⊧_{P} ⋀_{i∈I} φ_{i} iff p ⊧_{P} φ_{i} for all i ∈ I
p ⊧_{P} ⟨a⟩φ iff there is a q ∈ T (Σ) such that P ⊢_{ws} p ⟶^{a} q and q ⊧_{P} φ
p ⊧_{P} ¬φ iff p |̸=_{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 formulae 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} φ ⇔ p ⊧_{P} ψ.

3 Decomposing HML Formulae

In this section we will see how one can decompose HML formulae with respect to process terms. The TSS defining the transition relation on these terms should be in ready simulation format [4], allowing only ntyft/ntyxt rules [9] without lookahead.

Definition 11 (ntyxt,ntyft,nxytt). An ntytt rule is a transition 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, 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.

Definition 12 (lookahead). A transition rule has no lookahead if the variables occurring in the right-hand sides of its positive premises do not occur in the lefthand sides of its premises.

Definition 13 (ready simulation format). A TSS is in ready simulation format if its transition rules are ntyft or ntyxt rules that have no lookahead.

Definition 14 (free). A variable occurring in a transition rule is free if it does not occur in the source nor in the right-hand sides of the positive premises of this rule.

Definition 15 (decent). A transition rule is decent if it has no lookahead and does not contain free variables.

In Bloom, Fokkink & van Glabbeek [4] for any TSS P in ready simulation format the collection of P -ruloids is defined. These are decent nxytt rules for which the following holds:

Theorem 1. [4] Let P be a TSS in ready simulation format. Then P ⊢_{ws} σ(t) ⟶^{a} p for t a term, p a closed term and σ a closed substitution, iff there are a P -ruloid \frac{H}{t⟶^{a}u} and a closed substitution σ′ with P ⊢_{ws} σ′(α) for α ∈ H, σ′(t) = σ(t) and σ′(u) = p.

Given a TSS P = (Σ, R) 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 decomposition mapping ψ ∈ t_{P}^{−1}(φ) with σ(x) satisfying ψ(x) for all x ∈ var(t). This is formalised in Theorem 2 and proven thereafter.

Definition 16. Let P = (Σ, R) be a TSS in ready simulation format. Then ·_{P}^{−1} : 𝕋(Σ) → (𝕆 → P(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) ∧ ⋀_{(x⟶^{b}y)∈H} ⟨b⟩χ(y) ∧ ⋀_{(x−̸→^{c})∈H} ¬⟨c⟩⊤ if & x ∈ var(t) \\ ⊤ if & x ∉ var(t) \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)

When clear from the context, the subscript P will be omitted.

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

Theorem 2. Let P = (Σ, R) be a complete TSS in ready simulation format. Let φ ∈ 𝕆. For any term t ∈ 𝕋(Σ) and closed substitution σ : V → T (Σ) one has

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

Proof. With induction on the structure of φ.

– φ = ⟨a⟩φ′ ⇒ Suppose σ(t) ⊧ ⟨a⟩φ′. Then by Definition 10 there is a p ∈ T (Σ) with P ⊢_{ws} σ(t) ⟶^{a} p and p ⊧ φ′. Thus, by 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). Furthermore σ′(z) ⊧ χ(z) = ⊤ for all z ∉ var(u). Now define ψ as indicated in Definition 16. By definition, ψ ∈ t^{−1}(⟨a⟩φ′). Let x ∈ var(t). For (x ⟶^{b} y) ∈ H one has P ⊢_{ws} σ′(x) ⟶^{b} σ′(y) and σ′(y) ⊧ χ(y), so σ′(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⟩⊤. It follows that σ(x) = σ′(x) ⊧ ψ(x). ⇐ Now suppose that there is a ψ ∈ t^{−1}(⟨a⟩φ′) such that σ(x) ⊧ ψ(x) for all x ∈ var(t). This means that there is a P -ruloid

\frac{\{x ⟶^{a_{i}} y_{i} | i ∈ I_{x}, x ∈ var(t)\} ∪ \{x −̸→^{b_{j}}| j ∈ J_{x}, x ∈ var(t)\}}{t ⟶^{a} u}

and a decomposition mapping χ ∈ u^{−1}(φ′) such that, for all x ∈ var(t),

σ(x) ⊧ χ(x) ∧ ⋀_{i∈I_{x}}⟨a_{i}⟩χ(y_{i}) ∧ ⋀_{j∈J_{x}} ¬⟨b_{j}⟩⊤

By Definition 10 it follows that, for x ∈ var(t) and i ∈ I_{x}, P ⊢_{ws} σ(x) ⟶^{a_{i}} p_{i} for some p_{i} ∈ T (Σ) with p_{i} ⊧ χ(y_{i}). Moreover, for x ∈ var(t) and j ∈ J_{x},

P ⊬_{ws} σ(x) ⟶^{b_{j}} q for all q ∈ T (Σ), so by the completeness of P, P ⊢_{ws}

σ(x) −̸→^{b_{j}}. Let σ′ be a closed substitution with σ′(x) = σ(x) for x ∈ var(t) and σ′(y_{i}) = p_{i} for i ∈ I_{x} and x ∈ var(t). Here we use that the variables x and y_{i} are all different. Now σ′(z) ⊧ χ(z) for z ∈ var(u), using that u contains only variables that occur in t or in the premises of the ruloid. Thus the induction hypothesis can be applied, and σ′(u) ⊧ φ′. Moreover,

P ⊢_{ws} σ′(x) ⟶^{a_{i}} σ′(y_{i}) for x ∈ var(t) and i ∈ I_{x}, and P ⊢_{ws} σ′(x) −̸→^{b_{j}} for

x ∈ var(t) and j ∈ J_{x}. So, by Theorem 1, P ⊢_{ws} σ′(t) ⟶^{a} σ′(u), which implies σ(t) = σ′(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).

– φ = ¬φ′ ⇒ Suppose σ(t) ⊧ ¬φ′. Then by Definition 10 we have σ(t) |̸= φ′. Using the induction hypothesis, there is no χ ∈ t^{−1}(φ′) such that σ(x) ⊧ χ(x) for all x ∈ var(t). So for all χ ∈ t^{−1}(φ′) there is an x ∈ var(t) such that σ(x) ⊧ ¬χ(x). Let us denote this x as h(χ), so that we obtain a function h : t^{−1}(φ′) → var(t) such that σ(h(χ)) ⊧ ¬χ(h(χ)) for all χ ∈ t^{−1}(φ′). Define ψ ∈ t^{−1}(¬φ′) as indicated in Definition 16, using h. Let x ∈ var(t). If x = h(χ) for some χ ∈ t^{−1}(φ′) then σ(x) ⊧ ¬χ(x). Hence, σ(x) ⊧ ⋀_{χ∈h^{−1}(x)} ¬χ(x) = ψ(x). ⇐ Suppose that there is a ψ ∈ t^{−1}(¬φ′) such that σ(x) ⊧ ψ(x) for all x ∈ var(t). By Definition 16 there is a function h : t^{−1}(φ′) → var(t) such that ψ(x) = ⋀_{χ∈h^{−1}(x)} ¬χ(x) for all x ∈ var(t). So for all x ∈ var(t) and for all χ ∈ h^{−1}(x) we have that σ(x) ⊧ ¬χ(x). In other words, for all χ ∈ t^{−1}(φ′),we have σ(h(χ)) ⊧ ¬χ(h(χ)). So ¬∃χ ∈ t^{−1}(φ′)∀x ∈ var(t)(σ(x) ⊧ χ(x)). Then using the induction hypothesis, we have σ(t) |̸= φ′, so σ(t) ⊧ ¬φ′.

We give a few examples of the application of Definition 16.

Example 1. Let A = {a, b} and let P = (Σ, R) with Σ consisting 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⟩⊤). There are two P -ruloids with a conclusion of the form

f(x_{1}, x_{2}) ⟶^{b} , namely \frac{x_{1}⟶^{a}y}{f(x_{1},x_{2})⟶^{b}y} and \frac{x_{2}⟶^{a}y x_{1}−̸→^{b}}{f(x_{1},x_{2})⟶^{b}y}. According to Definition

16, we have f(x_{1}, x_{2})^{−1}(⟨b⟩⊤) = {ψ_{1}, ψ_{2}} with ψ_{1} and ψ_{2} as defined below, using χ ∈ y^{−1}(⊤) (so χ(x) = ⊤ for all variables x ∈ V):

ψ_{1}(x_{1}) = χ(x_{1}) ∧ ⟨a⟩χ(y) = ⊤ ∧ ⟨a⟩⊤ = ⟨a⟩⊤ ψ_{1}(x_{2}) = χ(x_{2}) = ⊤ ψ_{1}(x) = ⊤ for x ∉ var(f(x_{1}, x_{2}))

ψ_{2}(x_{1}) = χ(x_{1}) ∧ ¬⟨b⟩⊤ = ⊤ ∧ ¬⟨b⟩⊤ = ¬⟨b⟩⊤ ψ_{2}(x_{2}) = χ(x_{2}) ∧ ⟨a⟩χ(y) = ⊤ ∧ ⟨a⟩⊤ = ⟨a⟩⊤ ψ_{2}(x) = ⊤ for x ∉ var(f(x_{1}, x_{2}))

By Theorem 2 a closed term f(u_{1}, u_{2}) can execute a b if and only if the closed term u_{1} can execute an a, or the closed term u_{1} can not execute a b and the closed term u_{2} can execute an a. Looking at the premises, this is what we would expect.

Example 2. Using the TSS and the mappings ψ_{1}, ψ_{2} ∈ f(x_{1}, x_{2})^{−1}(⟨b⟩⊤) from Example 1, we can 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⟩⊤).

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 2 a closed term f(u_{1}, u_{2}) can not execute a b if and only if (1) the closed term u_{1} can execute a b but not an a, or (3) the closed term u_{1} can not execute an a and the closed term u_{2} can not execute an a. Looking at the premises, this is again what we would expect. The other two possibilities (2) and (4) do not qualify, since no term can ever satisfy ¬⊤.

A little less obvious example is the following:

Example 3. Let A = {a, b} and let P = (Σ, R) with Σ consisting 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}{f(x) ⟶^{a} f(y)}

This TSS is complete and in ready simulation format. We proceed to compute f(f(x))^{−1}(⟨b⟩⟨a⟩⊤). The only P -ruloid that has a conclusion f(f(x)) ⟶^{b}

is \frac{x⟶^{b}y}{f(f(x))⟶^{b}f(y)}. So for each ψ ∈ f(f(x))^{−1}(⟨b⟩⟨a⟩⊤), ψ(x) = χ(x) ∧ ⟨b⟩χ(y)

with χ ∈ f(y)^{−1}(⟨a⟩⊤). The only P -ruloid that has a conclusion f(y) ⟶^{a}

is \frac{y⟶^{b}z}{f(y)⟶^{a}f(z)}. So χ(y) = χ′(y) ∧ ⟨b⟩χ′(z) with χ′ ∈ f(z)^{−1}(⊤). Since χ′(y) =

χ′(z) = ⊤ we have χ(y) = ⟨b⟩⊤. Moreover x ∉ var(f(y)) implies χ(x) = ⊤. Hence ψ(x) = ⟨b⟩⟨b⟩⊤.

By Theorem 2 a closed term f(f(u)) can execute a b followed by an a if and only if the closed term u can execute two consecutive b’s.

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

Example 4. Let A = {a, b} and let P = (Σ, R) with Σ consisting 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}

This TSS, which is in ready simulation format, is incomplete. For example, neither P ⊢_{ws} c ⟶^{a} t for a closed term t 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 |̸= ⟨a⟩⊤ and f(c) |̸= ⟨b⟩⊤.

The only P -ruloid is \frac{x−̸→^{a}}{f(x)⟶^{b}c}. Hence Theorem 2 would yield f(c) ⊧ ⟨b⟩⊤ ⇔

c ⊧ ¬⟨a⟩⊤ ⇔ c |̸= ⟨a⟩⊤. Since this is false, Theorem 2 would fail with respect to P.

References

1. 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, Paris, France, pp. 144–153.

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

3. 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, Baltimore, USA, pp. 51–63.

4. B. Bloom, W. J. Fokkink & R. J. van Glabbeek (2003): Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic. To appear.

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

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

7. R. J. van Glabbeek (1996): The meaning of negative premises in transition system specifications II. In F. Meyer auf der Heide & B. Monien, editors: Automata, Languages and Programming, 23rd Colloquium (ICALP ’96), Lecture Notes in Computer Science 1099, Springer-Verlag, Paderborn, Germany, pp. 502–513.

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

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

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

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

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

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

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

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

16. R. Milner (1980): A Calculus of Communicating Systems. Springer-Verlag. Volume 92 of Lecture Notes in Computer Science.

17. 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, Lecture Notes in Computer Science 112, Springer-Verlag, Genoa, pp. 25–34.

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

19. G. D. Plotkin (1981): A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark.

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

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

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

23. 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), Lecture Notes in Computer Science 194, Springer-Verlag, pp. 475–486.

24. 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), Lecture Notes in Computer Science 185, Springer-Verlag, pp. 253–266.

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

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

27. 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, Lecture Notes in Computer Science 458, Springer-Verlag, Amsterdam, The Netherlands, pp. 481–501.