BRICS RS-98-40 Andersen et al.: A Compositional Proof System for the Modal μ-Calculus BRICS

Basic Research in Computer Science

A Compositional Proof System for the Modal μ-Calculus

Henrik Reif Andersen Colin Stirling Glynn Winskel BRICS Report Series RS-98-40 ISSN 0909-0878 December 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/40/

A Compositional Proof System for the Modal μ-Calculus^{∗}

Henrik Reif Andersen^{†} Colin Stirling  Glynn Winskel
Department of Computer Science Laboratory for Foundations of  BRICS^{‡}
Technical University of Denmark  Computer Science  Department of Computer Science
DK-2800 Lyngby  University of Edinburgh  Aarhus University
Denmark  Edinburgh EH9 3JZ  DK-8000 Aarhus C
Scotland, UK  Denmark
hra@id.dtu.dk  cps@dcs.edinburgh.ac.uk  gwinskel@brics.dk

Abstract

We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal μ-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal μ-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes.

1 Introduction

The propositional μ-calculus of Kozen [Kozen, 1983] which was introduced as a powerful extension of propositional dynamic logic has received growing interest as a logic for concurrent systems. This is mainly due to the expressiveness of the logic, which is known to subsume many modal and temporal logics, and the fact that very few operators are needed in achieving this: The logic is an extension of relativized, minimal modal logic K – also known as Hennessy-Milner logic in the process algebra community – with minimum and maximum fixed points. It is due to this connection (explained in more detail in [Stirling, 1992]) that we use the name the modal μ-calculus.

∗Extended abstract appears in: Proceedings of LICS’94, IEEE Computer Society Press.

†Supported by the Danish Technical Research Council.

‡Basic Research in Computer Science, Centre of the Danish National Research Foundation.

It is customary to consider Kripke models or, equivalently, labelled transition systems as models for interpretation of the logic. Since labelled transition systems are used in giving operational semantics of process languages, it is straightforward to view the modal μ-calculus as a language for expressing properties of processes. Despite the expressiveness, it turns out that validity is decidable for the modal μ-calculus, and for finite-state processes the problem of deciding satisfaction between a process and an assertion is decidable too. A range of algorithms and proof systems for this problem has been given in the literature, e.g. [Emerson and Lei, 1986, Arnold and Crubille, 1988, Larsen, 1988, Stirling and Walker, 1991, Cleaveland, 1990, Winskel, 1989, Cleaveland and Steffen, 1992, Andersen, 1994, Vergauwen and Lewi, 1992, Larsen, 1992, Cleaveland et al., 1992, Andersen, 1993]. They mostly rely on globally or locally computing the underlying transition system. However, what we seek here is a method that is compositional in the structure of processes, and which does not rely on computing the underlying transition system.

Compositionality is important for at least the following reasons. Firstly, it makes the verification modular, so that when changing part of a system only the verification concerning that particular part must be redone. Secondly, when designing a system or synthesising a process the compositionality makes it possible to have undefined parts of a process and still be able to reason about it. For instance, it might be possible to reveal inconsistencies in the specification or prove that with the choices already taken in the design no component supplied for the missing parts will ever be able to make the overall system satisfy the original specification. Thirdly, it makes it possible to decompose the verification task into potentially simpler tasks. Finally, it can make possible the reuse of verified components; their previous verification can be used to show that they meet the requirements on the components of a larger system.

Our method will be a compositional proof system, sound for arbitrary processes and complete for a class of finite-state processes. The proof system is compositional in the sense of the rules being guided by the structure of processes and not looking into the structure of subprocesses. Earlier work on compositional proof systems related to the modal μ-calculus includes work by Stirling [Stirling, 1985b, Stirling, 1985a, Stirling, 1987], Winskel [Winskel, 1985, Winskel, 1986, Winskel, 1990a, Winskel, 1990b], Larsen and Xinxin [Larsen and Xinxin, 1990], Andersen and Winskel [Andersen and Winskel, 1992]. The proof system presented here is along the lines of the work by Stirling and Winskel, but it extends their early work for Hennessy-Milner logic to a proper treatment of recursive processes and the full modal μcalculus. It also gives new rules for parallel composition and the other static operators. Actually, to a certain extent, the system can be seen as a result of turning the operational reductions of Larsen and Xinxin and the syntactic reductions of Andersen and Winskel into proof rules. But the match is not exact; apart from the new static rules the treatment of fixed points is closer to the work on local model checking [Larsen, 1988, Stirling and Walker, 1991, Cleaveland, 1990, Winskel, 1989].

2 Languages

p →^{∗} p a.p →^{a} p

\frac{p →^{α} p′}{p + q →^{α} p′} α ≠ ∗ \frac{q →^{α} q′}{p + q →^{α} q′} α ≠ ∗ \frac{t[rec x.t/x] →^{α} t′}{rec x.t →^{α} t′} α ≠ ∗

\frac{p →^{α} p′ q →^{β} q′}{p × q →^{α×β} p′ × q′}  \frac{p →^{α} p′}{p\{Ξ\} →^{β} p′\{Ξ\}} Ξ(α) = β  \frac{p →^{α} p′}{p ↾Λ →^{α} p′ ↾Λ} α ∈ Λ

Table 1: Operational rules.

The process language has a general parallel composition operator called a product, t_{0} × t_{1}, that allows the components to proceed both synchronously and asynchronously. Synchronization can then be enforced – or disallowed – through a restriction operator and synchronized actions can be given proper names through a relabelling operator. We refrain from giving details of how this allows a wide range of parallel operators to be encoded (see for example [Winskel, 1984] or [Andersen, 1993]), and we stick to introducing the language.

Let Act be a set of basic actions not containing the idling action ∗. The set of composite actions Act_{∗} is the free ∗, ×-algebra over Act ∪{∗} such that ∗ × ∗ = ∗. We let a, b, … range over basic actions, α, β, … over composite actions, and κ over sets of composite actions. The set of process terms are generated from the grammar:

t ::= 0 | a.t | t_{0} + t_{1} | t_{0} × t_{1} | t{Ξ} | t ↾Λ | x | rec x.t

The term constructors are called: nil, prefix, sum, product, relabelling, restriction, process variable, and recursion. The restricting set Λ is any subset of Act_{∗} containing {∗}; the relabelling function Ξ : Act_{∗} → Act_{∗} must be strict and injective on idling actions, i.e. Ξ(∗) = ∗ and Ξ^{−1}(∗) = {∗}. The operational semantics of this process language is given as a labelled transition system T = (P, Act_{∗}, →), where P is the set of closed process terms (the notions of open and closed terms are as usual) and →⊆ P × Act_{∗} × P is given as the least relation satisfying the rules of table 1. We shall refer to elements of P simply as processes.

The assertions of the modal μ-calculus will be given in a negation-free version and we use the construction of Winskel [Winskel, 1989] of tagging fixed points with sets of processes. Thus the assertions are constructed from the following grammar:

A ::= \begin{matrix}A_{0} ∨ A_{1} | A_{0} ∧ A_{1} | ⟨κ⟩A | [κ]A | \\ X | μX\{U\}A | νX\{U\}A \end{matrix}

where U ⊆ P is a set of tags and X ranges over a set of assertion variables. The usual tag-free fixed points μX.A and νX.A are special cases corresponding to empty tag sets. We have chosen to let the modalities diamond ⟨κ⟩A and box [κ]A range over sets of composite actions κ ⊆ Act_{∗} instead of just the more commonly single actions.

The semantics of assertions [[A]]ρ ⊆ P is given by induction on the structure of A; the map ρ is an environment taking all free variables of A to subsets of P. For the fixed points we observe that the bodies, when considered as functions of X, are monotonic on the complete lattice (Pow(P), ⊆) and then appeal to the Knaster-Tarski fixed-point theorem [Tarski, 1955] for supplying a minimum fixed point, denoted by μ, and a maximum fixed point, denoted by ν:

[[A_{0} ∨ A_{1}]]ρ = [[A_{0}]]ρ ∪ [[A_{1}]]ρ
[[A_{0} ∧ A_{1}]]ρ = [[A_{0}]]ρ ∩ [[A_{1}]]ρ
[[⟨κ⟩A]]ρ = {p ∈ P | ∃α ∈ κ ∃p′. p →^{α} p′ & p′ ∈ [[A]]ρ}
[[[κ]A]]ρ = {p ∈ P | ∀α ∈ κ ∀p′. p →^{α} p′ ⇒ p′ ∈ [[A]]ρ}
[[X]]ρ = ρ(X)
[[μX{U}A]]ρ = μV.([[A]]ρ[V/X] \ U)
[[νX{U}A]]ρ = νV.([[A]]ρ[V/X] ∪ U)

Satisfaction between a process p and a closed assertion A is now defined by, p ⊧ A, iff, p ∈ [[A]]ρ for all ρ. For future reference we define:

Definition 1 Let S_{p} be the set of sub-term reachable states of the process p. I.e. the least set of states closed under

(i) p ∈ S_{p},
(ii) if q ∈ S_{p} and q →^{α} q′ then q′ ∈ S_{p},
(iii) if q ∈ S_{p} and q′ is a closed subterm of q then q′ ∈ S_{p}.

Let R_{p}, the reachable states of p, be the least subset of S_{p} closed under (i) and (ii). □

It is not hard to prove that if all recursive terms in a process p are regular (i.e. the body is built entirely from 0, +, a., x, and rec) then S_{p} is finite. A recursion rec x.t is said to be guarded if any occurrence of x in t is inside a prefix.

3 The proof system

The proof system will be presented as “goal-oriented” proof rules defining inductively the relation ⊢⊆ P × ClAssn between processes and closed assertions. The rules naturally fall into three classes: Rules that do not involve the process operators, rules for the dynamic process operators (0, a., +, rec), and finally rules for the static process operators ({Ξ},↾Λ, ×).

3.1 Rules for the fixed points, boolean connectives and idling modalities

The first class of rules, given in table 2, only depend on the structure of assertions. They encompass rules for the boolean connectives, modalities with the idling action and fixed points. These are straightforward rules that need little comment, except for the fixed-point rules. They are based on the following observation, originally due to Kozen, and later used as the key step in a local model checker by Winskel:

Lemma 1 (Reduction lemma) ([Kozen, 1983], [Winskel, 1989]) For ψ a monotonic function on a powerset Pow(D) with p ∈ D, we have

p ∈ μV.ψ(V) ⇔ p ∈ ψ(μV.(ψ(V) \ {p})),
p ∈ νV.ψ(V) ⇔ p ∈ ψ(νV.(ψ(V) ∪ {p})).

The last bi-implication holds for an arbitrary set P and inclusion instead of just for a singleton; the first not. Kozen [Kozen, 1983, Prop.5.7(vi)] proved the direction from right to left. Cleaveland [Cleaveland, 1990] used a quite similar lemma in showing completeness of his tableau method.

The right-hand sides of the bi-implications involve a slightly modified unfolding of the fixed points. For the minimum fixed point a single element, p, is removed in the unfolding; for the maximum it is added. The tagged fixedpoint assertions were introduced to make this unfolding expressible directly in the logic. Thus under the assumption that p ∉ U the first bi-implication shows that p ⊧ μX{U}A if and only if p ⊧ A[μX{U, p}A/X], which shows soundness of the rule (μ). Similarly, the soundness of the maximum fixed point rule (ν1) follows from the second bi-implication.^{1}

Remark We shall refer to the rules in the sequel by names constructed from the operators of the term and assertion that is involved in the rule. When this does not give a unique name we add numbers starting from 0. The names will be shown next to the rules in the tables. □

1An alternative to the tags is to change the proof system into a tableau system where a similar effect is achieved by giving global success/failure criteria on the proof tree. See for example [Stirling and Walker, 1991] for an explanation of the relationship between the two approaches.

\begin{matrix}(∧) \frac{t ⊢ A_{0} ∧ A_{1}}{t ⊢ A_{0} t ⊢ A_{1}} \\ (∨0) & \frac{t ⊢ A_{0} ∨ A_{1}}{t ⊢ A_{0}} & (∨1) & \frac{t ⊢ A_{0} ∨ A_{1}}{t ⊢ A_{1}} \\ ([∗]) & \frac{t ⊢ [∗, κ]A}{t ⊢ A t ⊢ [κ]A} \\ (⟨∗⟩0) & \frac{t ⊢ ⟨∗, κ⟩A}{t ⊢ A} & (⟨∗⟩1) & \frac{t ⊢ ⟨∗, κ⟩A}{t ⊢ ⟨κ⟩A} \\ (μ) \frac{t ⊢ μX\{U\}A}{t ⊢ A[μX\{U, t\}A/X]} t ∉ U \\ (ν0) \underline{t ⊢ νX\{U, t\}A} (ν1) \frac{t ⊢ νX\{U\}A}{t ⊢ A[νX\{U, t\}A/X]} t ∉ U \end{matrix}

Table 2: Rules for the boolean connectives, idling modalities and fixed points.

3.2 Rules for the dynamic operators

What is missing now are rules for assertions where the top-level operator is a modality which do not involve an idling action. These remaining rules will depend on the structure of the process term, in different ways for the dynamic and the static operators. For the dynamic process operators they are rather direct consequences of the operational semantics, see table 3, once the following is observed for the recursion operator:

Proposition 1 Assume rec x.t is a closed process term, A a closed assertion, and κ a set of composite actions not containing ∗. Then

rec x.t ⊧ [κ]A ⇔ t[rec x.t/x] ⊧ [κ]A,
rec x.t ⊧ ⟨κ⟩A ⇔ t[rec x.t/x] ⊧ ⟨κ⟩A.

Proof: Since there is only one operational rule for the recursion operator – the unfolding rule – rec x.t and t[rec x.t/x] have syntactically the same αsuccessors for any α ≠ ∗. The proposition now follows from the observation

(0[]) \underline{0 ⊢ [κ]A}

(.[]0) \frac{a.t ⊢ [a, κ]A}{t ⊢ A} (.[]1) \underline{a.t ⊢ [κ]A} a ∉ κ

(.⟨⟩) \frac{a.t ⊢ ⟨a, κ⟩A}{t ⊢ A}
(+[]) \frac{t_{0} + t_{1} ⊢ [κ]A}{t_{0} ⊢ [κ]A t_{1} ⊢ [κ]A}

(+⟨⟩0) \frac{t_{0} + t_{1} ⊢ ⟨κ⟩A}{t_{0} ⊢ ⟨κ⟩A}  (+⟨⟩1) \frac{t_{0} + t_{1} ⊢ ⟨κ⟩A}{t_{1} ⊢ ⟨κ⟩A}

(rec[]) \frac{rec x.t ⊢ [κ]A}{t[rec x.t/x] ⊢ [κ]A}  (rec⟨⟩) \frac{rec x.t ⊢ ⟨κ⟩A}{t[rec x.t/x] ⊢ ⟨κ⟩A}

Table 3: Dynamic process operators. All rules assume ∗ ∉ κ.

that for any closed process p, the judgements p ⊧ ⟨κ⟩A and p ⊧ [κ]A are fully determined by the κ-successors of p. □

It is important that the top-level assertion is a modality: The successor states of rec x.t and its unfolded version are syntactically identical (since unfolding is the only operational rule for recursion), and thus satisfies the same set of assertions. But rec x.t satisfies νX{rec x.t}A whereas this is not necessarily the case for t[rec x.t/x].

3.3 Rules for the static operators

In order to give rules for the static operators we shall extend the assertions with operators expressing the “pre-images” of the corresponding process operators. For relabelling, this mean that we allow assertions like A{Ξ} with the semantic interpretation

[[A{Ξ}]]ρ = {p | p{Ξ} ∈ [[A]]ρ}.

Thus t ⊧ A{Ξ} if and only if t{Ξ} ⊧ A. Hence, we include in the syntax these extended assertions:

A ::= … | A{Ξ} | A ↾Λ | A/t

(\{\}[]) \frac{t\{Ξ\} ⊢ [κ]A}{t ⊢ [Ξ^{−1}(κ)](A\{Ξ\})} (\{\}⟨⟩) \frac{t\{Ξ\} ⊢ ⟨κ⟩A}{t ⊢ ⟨Ξ^{−1}(κ)⟩(A\{Ξ\})}

(↾[]) \frac{t ↾Λ ⊢ [κ]A}{t ⊢ [Λ ∩ κ](A ↾Λ)} (↾⟨⟩) \frac{t ↾Λ ⊢ ⟨κ⟩A}{t ⊢ ⟨Λ ∩ κ⟩(A ↾Λ)}

(\{\}) \frac{t ⊢ A\{Ξ\}}{t\{Ξ\} ⊢ A} (↾) \frac{t ⊢ A ↾Λ}{t ↾Λ ⊢ A} (×) \frac{t_{0} ⊢ A/t_{1}}{t_{0} × t_{1} ⊢ A}

Table 4: Rules for eliminating relabelling and restriction from the process, and the three shift rules. The rules assume ∗ ∉ κ.

The semantic interpretations of the last two operators, restriction and quotienting, are:

\begin{aligned}[[A ↾Λ]]ρ & = & \{p | p ↾Λ ∈ [[A]]ρ\} \\ [[A/t]]ρ & = & \{p | p × t ∈ [[A]]ρ\} \end{aligned}

The new assertion operators will be used in giving rules for the modalities. For instance, one of the rules for relabelling will be

\frac{t\{Ξ\} ⊢ [κ]A}{t ⊢ [Ξ^{−1}(κ)](A\{Ξ\})}

Notice, that the operator {Ξ} is applied to an assertion “guarded” by a boxmodality. This box-modality can be removed by further application of the rules. At some point we might end up with {Ξ} being applied at the toplevel, and the rule we choose to give for such an assertion is a shift rule that shifts the operator back to the process, see table 4.

Various versions of parallel composition has traditionally posed the greatest difficulties in giving compositional rules. To get an idea of the difficulties, suppose we are confronted with the satisfaction problem t_{0} × t_{1} ⊢ A and we want to decompose this to satisfaction problems for t_{0} and t_{1} without inspecting the structure of t_{0} and t_{1}. If we think of t_{0} × t_{1} as an element of the two-dimensional “plane”, P×P, the assertion A will be some two-dimensional “shape” in this plane. A decomposition of A could now be constructed by taking fragments A_{0} and A_{1} of the two axes, such that t_{0} should satisfy A_{0} and t_{1} should satisfy A_{1}. However, for this to be a complete decomposition, valid for all t_{0} and t_{1}, we would need to have A equal to the product of A_{0} and A_{1}. This product would always be a “rectangle” – something which is certainly not true for arbitrary A. One way to get around this problem is to approximate A from the inside by a set of pairs of assertions (A_{0}^{i}, A_{1}^{i}) forming rectangles, the union of which forms exactly A. However, as Winskel argues in [Winskel, 1990b] the presence of fixed points can force this to be an infinite set; resulting in a poor decomposition.^{2}

Fortunately, if we are slightly less ambitious and allow ourselves to inspect the structure of one of the two components, we can do better. In the suggested picture, this corresponds to the fact that if we fix a point on one of the axes, we can project to the other and get a subset of P. The task of decomposition is now to find the assertion expressing this projection. As we shall see in section 6, if the component is finite-state, it is possible to directly compute the projected assertion. But in the rules we will be more general and impose no restrictions on finiteness; in fact, the rules will be local and for the dynamic operators follow very closely the rules of table 3. The main difference is that we are now considering a process t′ in a ‘context’ t× which, however, play no active role in the rules; all the rules are guided solely by the structure of t′.

As before with the idling modalities, we shall need some rules that allow actions idling in the right component to be taken outside of the modalities. In order to state these rules we use the auxiliary operation κ/α of quotienting a set of actions with respect to a particular action. This operation is defined by κ/α = {β | β × α ∈ κ}. We also use κ \ × ∗ for the set of actions α × β ∈ κ for which β is not ∗. These rules are given as the first three rules of table 5. They are easily seen to be sound. The last eight rules of table 5 are the rules for the dynamic operators.

When the right component t′ is headed by a static operator, we simplify the right component at the expense of the left. Let the operation l_{×}(A) reassociate every modality and every tag of the form × ( × ) in A to the left. Then, we change the product t×(t_{0} ×t_{1}) to (t×t_{0})×t_{1} and perform the corresponding rearrangement on A by replacing it by l_{×}(A). Analogously, when t′ is a relabelling we will exploit that t × (t′{Ξ}) is equivalent to (t × t′){Id×Ξ}, where Id is the identity relabelling and the product of relabellings

2An example of a difficult assertion is the assertion B from [Andersen, 1993] expressing bisimilarity: p × q ⊧ B, iff, p and q are strongly bisimilar. Hence, B forms a diagonal in the “plane”. A decomposition would include a rectangle for each equivalence class.

(×[∗]) \frac{t × t′ ⊢ [κ]A}{t ⊢ [κ/∗](A/t′) t × t′ ⊢ [κ \ × ∗]A}
(×⟨∗⟩0) \frac{t × t′ ⊢ ⟨κ⟩A}{t ⊢ ⟨κ/∗⟩(A/t′)} (×⟨∗⟩1) \frac{t × t′ ⊢ ⟨κ⟩A}{t × t′ ⊢ ⟨κ \ × ∗⟩A}

The rules below all assume κ/∗ = ∅ (×0[]) \underline{t × 0 ⊢ [κ]A}

(×.[]) \frac{t × a.p ⊢ [κ]A}{t ⊢ [κ/a](A/p)} (×.⟨⟩) \frac{t × a.p ⊢ ⟨κ⟩A}{t ⊢ ⟨κ/a⟩(A/p)}

(×+[]) \frac{t × (t_{0} + t_{1}) ⊢ [κ]A}{t × t_{0} ⊢ [κ]A t × t_{1} ⊢ [κ]A}

(×+⟨⟩0) \frac{t × (t_{0} + t_{1}) ⊢ ⟨κ⟩A}{t × t_{0} ⊢ ⟨κ⟩A} (×+⟨⟩1) \frac{t × (t_{0} + t_{1}) ⊢ ⟨κ⟩A}{t × t_{1} ⊢ ⟨κ⟩A}

(×rec[]) \frac{t × rec x.t′ ⊢ [κ]A}{t × t′[rec x.t′/x] ⊢ [κ]A}

(×rec⟨⟩) \frac{t × rec x.t′ ⊢ ⟨κ⟩A}{t × t′[rec x.t′/x] ⊢ ⟨κ⟩A}

Table 5: Product rules for idling and dynamic operators. We use the abbreviations κ/α = {β | β × α ∈ κ} and κ \ × ∗ = {α × β ∈ κ | β ≠ ∗}.

(××) \frac{t × (t_{0} × t_{1}) ⊢ A}{(t × t_{0}) × t_{1} ⊢ l_{×}(A)}

(×\{\}) \frac{t × (t′\{Ξ\}) ⊢ A}{(t × t′)\{Id × Ξ\} ⊢ l_{\{Ξ\}}(A)}

(× ↾) \frac{t × (t′ ↾Λ) ⊢ A}{(t × t′) ↾(Act_{∗} × Λ) ⊢ l_{↾Λ}(A)}

Table 6: Product rules for static operators.

Ξ_{0} × Ξ_{1} is defined by

Ξ_{0} × Ξ_{1}(α) = \{ \begin{matrix}Ξ_{0}(α_{0}) × Ξ_{1}(α_{1}) & if α = α_{0} × α_{1} \\ α & otherwise. \end{matrix}

The corresponding change on an assertion A is to replace every tag of the form × ( {Ξ}) by a tag ( × ){Id × Ξ} and removing the others. Let l_{{Ξ}}(A) be the result of performing this operation on A.

Finally, for restriction we exploit the equivalence between t_{0} ×(t_{1} ↾Λ) and (t_{0} × t_{1}) ↾(Act_{∗} × Λ) using the operation l_{↾Λ}(A) to change the tags of A from × ( ↾ Λ) to ( × ) ↾ (Act_{∗} × Λ) and removing the others. This gives rise to the three rules of table 6 for the static operators.

4 Soundness

The rules are sound for arbitrary processes and complete for a set of finitestate processes, i.e. processes with only guarded regular recursions.

Many of the rules are both upwards and downwards sound as captured by the following proposition:

Proposition 2 For all processes t, t_{0}, t_{1} and t_{2}, closed extended assertions A and sets of composite actions κ not containing the idling action, we have

i) t{Ξ} ⊧ [κ]A ⇔ t ⊧ [Ξ^{−1}(κ)](A{Ξ})
i′) t{Ξ} ⊧ ⟨κ⟩A ⇔ t ⊧ ⟨Ξ^{−1}(κ)⟩(A{Ξ})
ii) t ↾Λ ⊧ [κ]A ⇔ t ⊧ [Λ ∩ κ](A ↾Λ)
ii′) t ↾Λ ⊧ ⟨κ⟩A ⇔ t ⊧ ⟨Λ ∩ κ⟩(A ↾Λ)
iii)  t ⊧ A{Ξ} ⇔ t{Ξ} ⊧ A
iv)  t ⊧ A ↾Λ ⇔ t ↾Λ ⊧ A
v)  t_{0} ⊧ A/t_{1} ⇔ t_{0} × t_{1} ⊧ A.

Proof: For the bi-implications i–ii′ observe that there is only one rule that applies to a relabelled term and to a restricted term. Combining this with the semantics of extended assertions immediately results in the four bi-implications.

The bi-implications iii–v follow directly from the definition of the semantics of extended assertions. □

Before arguing for soundness of the product static rules, table 6, we need a simple lemma on the semantics of assertions and another lemma relating fixed points in different lattices.

Lemma 2 (Locality Lemma, [Andersen and Winskel, 1992]) Assume that U is a set of processes closed under →. Let T_{U} be the restriction of T to U. By [[A]]_{U}ρ we denote the semantics of A with respect to this restricted transition system: Tag-sets are restricted to U and fixed points are found in the complete lattice Pow(U). Then for all A and ρ,

[[A]]ρ ∩ U = [[A]]_{U}ρ_{U}

where ρ_{U}(X) = ρ(X) ∩ U.

To see how we shall employ this lemma, take L = {t_{0} × (t_{1}{Ξ}) | t_{0}, t_{1} ∈ P, Ξ a relabelling} and R = {(t_{0} × t_{1}){Id × Ξ} | t_{0}, t_{1} ∈ P, Ξ a relabelling}. Since no operational rules can remove the static operators, L and R are closed under →. Now, by the locality lemma

t_{0} × (t_{1}{Ξ}) ⊧ A ⇔ t_{0} × (t_{1}{Ξ}) ∈ [[A]]_{L}ρ_{L}

for all ρ. Hence, we lose no information by taking the local view of the semantics. Similarly for processes in R we have

(t_{0} × t_{1}){Id × Ξ} ⊧ A ⇔ (t_{0} × t_{1}){Id × Ξ} ∈ [[A]]_{R}ρ_{R}.

Our proof of soundness of (×{}) will relate these two local views of the semantics. In doing this we will need to relate fixed points in the two complete lattices Pow(L) and Pow(R). The following lemma gives the means to relate minimum fixed points – a dual version of it for relating maximum fixed points:

Lemma 3 Let D and E be complete sub-lattices of Pow(P). Let in : D → E be an ω-continuous function such that in(⊥_{D}) = ⊥_{E}. Suppose ϕ : E → E and θ : D → D are monotonic functions such that

in ∘ θ = ϕ ∘ in.

Then

in(μθ) = μϕ.

See [Andersen and Winskel, 1992] or [Andersen, 1993] for a proof.

In proving (×{}) sound we shall use the lemma in the case where D is Pow(L), E is Pow(R) and in is the ω-continuous function l_{{Ξ}} mapping t_{0} × (t_{1}{Ξ}) to (t_{0} × t_{1}){Id × Ξ}. Similar setups work for the rules (××) and (× ↾):

Lemma 4 For all processes t_{0}, t_{1}, t_{2} and closed extended assertions A we have:

vi) t_{0} × (t_{1} × t_{2}) ⊧ A ⇔ (t_{0} × t_{1}) × t_{2} ⊧ l_{×}(A)
vii) t_{0} × (t_{1}{Ξ}) ⊧ A ⇔ (t_{0} × t_{1}){Id × Ξ} ⊧ l_{{Ξ}}(A)
viii) t_{0} × (t_{1} ↾Λ) ⊧ A ⇔ (t_{0} × t_{1}) ↾(Act_{∗} × Λ) ⊧ l_{↾Λ}(A).

Proof: We shall prove vii the remaining two bi-implications are similar. By structural induction on A we prove for all A, P (A) where P (A) is defined by, P (A) holds if and only if

l_{{Ξ}}([[A]]_{L}ρ) = [[l_{{Ξ}}(A)]]_{R}l_{{Ξ}} ∘ ρ

for all environments ρ assigning variables to subsets of L. Having proven P (A) it follows immediately by the locality lemma that for any closed A, if t_{0} × (t_{1}{Ξ}) ⊧ A then l_{{Ξ}}(t_{0} × (t_{1}{Ξ})) = (t_{0} × t_{1}){Id × Ξ} satisfies l_{{Ξ}}(A).

To prove P (A) we consider the possible forms of A.

Case A ≡ X. This case follows directly from the semantic clause for X: l_{{Ξ}}([[X]]_{L}ρ) = l_{{Ξ}}(ρ(X)).

Case A ≡ μX{U}A. Let θ(V) = [[A]]_{L}ρ[V/X] ∪ U and ϕ(V) = [[A]]_{R}(l_{{Ξ}} ∘ ρ)[V/X] ∪ l_{{Ξ}}(U). By the induction hypothesis it follows that

l_{{Ξ}}(θ(V)) = ϕ(l_{{Ξ}}(V))

and hence, since both θ and ϕ are clearly monotonic, l_{{Ξ}}(∅) = ∅ and l_{{Ξ}} is ω-continuous it follows from lemma 3 that

l_{{Ξ}}(μθ) = μϕ.

By expanding θ and ϕ and using the semantic clause for the minimum fixed points we get

l_{{Ξ}}([[μX{U}A]]_{L}ρ) = [[μX{U}A]]_{R}l_{{Ξ}} ∘ ρ

completing the case for the minimum fixed point.

The case for the maximum fixed point is completely dual. The remaining cases for A are simple provided the following is observed for the modalities: A transition

t_{0} × (t_{1}{Ξ}) →^{α×β} t′_{0} × (t′_{1}{Ξ})

is possible, if and only if, t_{0} →^{α} t′_{0} and there exists a γ such that t_{1} →^{γ} t′_{1} and Ξ(γ) = β. This will be the case, if and only if,

(t_{0} × t_{1}){Id × Ξ} →^{α×β} (t′_{0} × t′_{1}){Id × Ξ}.

Hence, the two terms will always be capable of performing the same initial transitions. (In fact, they are strongly bisimilar cf. [Milner, 1989]). □

We can now prove soundness for the full set of rules:

Theorem 1 (Soundness) Assume a process t and a closed assertion A. If t ⊢ A can be proven using the rules of table 2, 3, 4, 5, and 6 then t ⊧ A.

Proof: As usual this is shown by proving that each rule is sound. We shall argue that they are sound even for extended assertions. Rules (∧), (∨0) and (∨1) are straightforward. The idling rules ([]∗), (⟨⟩∗0) and (⟨⟩∗1) are straightforward since all processes t – due to the restrictions on Ξ and Λ – have the unique idling transition t →^{∗} t.

Soundness of the fixed point rules (μ), (ν1) follows from the reduction lemma and they are both upwards and downwards sound. Soundness of (ν0) is immediate from the semantics.

Soundness of (0[]), (.[]0), (.[]1), (.⟨⟩), (+[]), (+⟨⟩0) and (+⟨⟩1) can be proven directly from the operational semantics. The recursive process rules are both upwards and downwards sound as shown in proposition 1.

Soundness of the rules ({Ξ}[]), ({Ξ}⟨⟩), (↾ Λ[]), (↾ Λ⟨⟩), ({Ξ}), (↾ Λ), and (×) of table 4 follows from proposition 2. The idling rules (×[]∗), (×⟨⟩∗0) and (×⟨⟩∗1) follows directly from the operational semantics as for the×-free versions. Similarly, the dynamic rules (×0), (×.[]), (×.⟨⟩) etc. are proven like their ×-free counterparts (0), (.[]0)/(.[]1), (.⟨⟩) etc.

Soundness of the product static rules (××), (×{Ξ}) and (× ↾Λ) follows also from proposition 2. □

Notice, that the fixed-point rules, the dynamic process operator rules, and all the static operator rules – including the product rules – are both upwards and downwards sound. In fact, only the disjunction rules and the 8 diamond rules (⟨∗⟩0), (⟨∗⟩1), (+⟨⟩0), (+⟨⟩1), (×⟨∗⟩0), (×⟨∗⟩1), (×+⟨⟩0), (×+⟨⟩1) fail to be downwards sound.

5 Completeness

Central in our proof of completeness will be a well-founded relation on assertions:

Lemma 5 The relation ≺ defined on closed assertions with tags from a finite set S by

A ≺ A′ iff A is a proper subassertion of A′, or A′ ≡ σX{U}B and

A ≡ B[σX{U, t}B/X] for some t ∉ U,

where σ is one of μ and ν, is well-founded.

The relation ≺ embodies the fact that the small modifications to the tags when unfolding the fixed points is enough to ensure that the fixed-point rules can only be applied a finite number of times before t ∈ U. It captures in a very precise manner the reason for termination of model checking algorithms based on the fixed-point rules (μ), (ν0) and (ν1) as in the works of Stirling and Walker [Stirling and Walker, 1991], Cleaveland [Cleaveland, 1990] and Winskel [Winskel, 1989].

The proof strategy in proving completeness is as follows. Assume a process p with a finite set of sub-term reachable states S_{p}. By well-founded induction using ≺ we show that for all t ∈ S_{p}, if t ⊧ A then t ⊢ A. When A is of the form [κ]B or ⟨κ⟩B this will involve inspecting the structure of the term t. Thus we shall show by another induction, this time on t, how to construct from proofs of some t_{1} ⊢ B, …, t_{n} ⊢ B where t_{i} is less than t and for all i t_{i} ⊧ B, a proof of t ⊢ A. The “less than” ordering we use on terms is based on a measure w(t) that is roughly “the maximal depth to a prefix, nil or variable in t,” which, however, gives more weight to the second component of a product than to the first. Hence, simplifying the second component at the expense of the first, as it is done in the static rules, is still considered a way of making progress.

Theorem 2 (Completeness for finite-state processes) If p is a process with guarded regular recursions then, for all closed assertions A with tags in S_{p}, if p ⊧ A then p ⊢ A.

Proofs of this theorem and lemma 5 can be found in the appendix.

To show an example of the usage of the rules, we will consider the CCS parallel composition | as an abbreviation for ( × ) ↾ Λ{Ξ} where Λ and Ξ are as follows. First, the actions Act are supposed to include a distinguished internal action τ and the remaining actions are called names. Associated with each name a is a co-name ā; such that ¯ forms a bijection on Act \ τ. Then, take Λ = {a × ā, a′ × ∗, ∗ × a′ | a ∈ Act \ τ, a′ ∈ Act}, and let Ξ(a × ā) = τ, Ξ(a′ × ∗) = Ξ(∗ × a′) = a′ and on other actions α, Ξ(α) = α. It is not hard to see that (p × q) ↾Λ{Ξ} will behave exactly as p|q.

Example This example illustrates how the compositionality facilitates proving a property about a process that contains infinite-state components – when the infinite-state behaviour is irrelevant for the property: Assume p and q ≡ rec x.τ.x + t are infinite-state processes (x might be free in t). We shall consider the process p|q and prove that it has an infinite τ-loop as expressed by the assertion νX{}⟨τ⟩X.

p|q ⊢ νX{}⟨τ⟩X \begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (ν1) \\ p|q ⊢ ⟨τ⟩νX\{p|q\}⟨τ⟩X \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (\{\}⟨⟩) \\ (p × q) ↾Λ ⊢ ⟨Ξ^{−1}(τ)⟩(νX\{p|q\}⟨τ⟩X)\{Ξ\} \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (↾⟨⟩) \\ p × q ⊢ ⟨κ⟩(νX\{p|q\}⟨τ⟩X)\{Ξ\} ↾Λ \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (×rec⟨⟩) \\ p × (τ.q + t[q/x]) ⊢ ⟨κ⟩(νX\{p|q\}⟨τ⟩X)\{Ξ\} ↾Λ \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (×+⟨⟩0) \\ p × τ.q ⊢ ⟨κ⟩(νX\{p|q\}⟨τ⟩X)\{Ξ\} ↾Λ \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (×⟨∗⟩1) \\ p × τ.q ⊢ ⟨κ \ × ∗⟩(νX\{p|q\}⟨τ⟩X)\{Ξ\} ↾Λ \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (×.⟨⟩) \\ p ⊢ ⟨∗⟩(νX\{p|q\}⟨τ⟩X)\{Ξ\} ↾Λ/q \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (⟨∗⟩0) \\ p ⊢ (νX\{p|q\}⟨τ⟩X)\{Ξ\} ↾Λ/q \end{matrix}

\begin{matrix}- & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & - & (×), (↾), (\{\}) \\ p|q ⊢ νX\{p|q\}⟨τ⟩X \end{matrix}

------------------------------------------------------------------------------------ (ν0)

Figure 1: A proof tree for the example.

Let κ = Λ ∩ Ξ^{−1}(τ) = {a × ā | a ∈ Act \ τ} ∪ {τ × ∗, ∗ × τ}. The proof tree is given in figure 1. Note that in the application of rule (×.⟨⟩), we are using (κ \ × ∗)/τ = {∗}.

6 Reductions

There is an alternative approach to compositionality, followed in [Andersen and Winskel, 1992] and to some extent in [Larsen and Xinxin, 1990], based on the idea of reductions. A reduction transforms a satisfaction problem for a composite process op(t_{1}, …, t_{n}) ⊢ A into a boolean expression over satisfaction problems t_{1} ⊢ A_{1}, …, t_{n} ⊢ A_{n} for the subterms of the process – independent of the structure of these. Simple examples of reductions can be derived from:

\begin{aligned}t_{0} + t_{1} ⊧ [κ]A & ⇔ & (t_{0} ⊧ [κ]A) and (t_{1} ⊧ [κ]A), \\ t_{0} + t_{1} ⊧ ⟨κ⟩A & ⇔ & (t_{0} ⊧ ⟨κ⟩A) or (t_{1} ⊧ ⟨κ⟩A). \end{aligned}

In general, the reductions will be more involved. However, for the relabelling and restriction it is possible to give quite concise reductions. They simply change the modalities (and the tags) of the assertion and leave everything else unchanged. In the context of our proof rules such a reduction can be seen as a means for eliminating the extended assertions. I.e. for any assertion A, equivalent assertions e(A{Ξ}) and e(A ↾Λ) with {Ξ} and ↾Λ removed, can be found. Table 7 shows these reductions. An alternative to the rules ({Ξ}[]) and ({Ξ}⟨⟩) could now be

\frac{t\{Ξ\} ⊢ A}{t ⊢ e(A\{Ξ\})}

Thus, no extended assertion will be introduced by this new rule.

e(X{Ξ}) = X
e(A_{0} ∧ A_{1}{Ξ}) = e(A_{0}{Ξ}) ∧ e(A_{1}{Ξ})
e(A_{0} ∨ A_{1}{Ξ}) = e(A_{0}{Ξ}) ∨ e(A_{1}{Ξ})
e([κ]A{Ξ}) = [Ξ^{−1}(κ)]e(A{Ξ})
e(⟨κ⟩A{Ξ}) = ⟨Ξ^{−1}(κ)⟩e(A{Ξ})
e(νX{U}A{Ξ}) = νX{U{Ξ}}e(A{Ξ})
e(μX{U}A{Ξ}) = μX{U{Ξ}}e(A{Ξ})
e(X ↾Λ) = X
e(A_{0} ∧ A_{1} ↾Λ) = e(A_{0} ↾Λ) ∧ e(A_{1} ↾Λ)
e(A_{0} ∨ A_{1} ↾Λ) = e(A_{0} ↾Λ) ∨ e(A_{1} ↾Λ)
e([κ]A ↾Λ) = [Λ ∩ κ]e(A ↾Λ)
e(⟨κ⟩A ↾Λ) = ⟨Λ ∩ κ⟩e(A ↾Λ)
e(νX{U}A ↾Λ) = νX{U ↾Λ}e(A ↾Λ)
e(μX{U}A ↾Λ) = μX{U ↾Λ}e(A ↾Λ)

Table 7: Reductions for relabelling and restriction. Recall, U{Ξ} = {p | p{Ξ} ∈ U} and U ↾Λ = {p | p ↾Λ ∈ U}.

If t is a finite-state process, also the quotienting A/t can be removed by a reduction. To give this reduction we need to introduce tagged simultaneous fixed points. Let σ be any one of μ and ν. Then the syntax is:

σX_{1}{U_{1}} … X_{n}{U_{n}}(A_{1}, …, A_{n}) ↓ X_{i},

abbreviated as σX⃗{U⃗}A⃗ ↓ X_{i}. The semantics should be clear. The reduction is given in table 8. An alternative rule for product could now be

\frac{t_{0} × t_{1} ⊢ A}{t_{0} ⊢ e(A/t_{1})} ,

\begin{aligned}e(X/p) & = & X_{p} \\ e(A_{0} ∨ A_{1}/p) & = & e(A_{0}/p) ∨ e(A_{1}/p) \\ e(A_{0} ∧ A_{1}/p) & = & e(A_{0}/p) ∧ e(A_{1}/p) \\ e(⟨κ⟩A/p) & = & ⋁\{⟨α⟩e(A/p′) | ∃α × β ∈ κ. p →^{β} p′\} \\ e([κ]A/p) & = & ⋀\{[α]e(A/p′) | ∃α × β ∈ κ. p →^{β} p′\} \\ e(σX\{U\}A/p) & = & σX_{p_{1}}\{U/p_{1}\} ⋯ X_{p_{n}}\{U/p_{n}\}.(e(A/p_{1}), …, e(A/p_{n})) ↓ X_{p} \\ & & where \{p_{1}, …, p_{n}\} = R_{p} \end{aligned}

Table 8: Reduction for quotienting. Recall, U/p = {t | t × p ∈ U}.

which, again, does not introduce any extended assertion. The price is, that the new rule is only applicable for finite-state processes, and we must now consider simultaneous fixed points. The simultaneous fixed points can be converted into simple fixed points using the Scott-Bekič principle [Bekič, 1984], thereby potentially increasing the size of the assertion considerably. A more appealing approach would be to extend the fixed-point rules to simultaneous fixed points. Then, for example, (μ) should be replaced by

\frac{t ⊢ μX⃗\{U⃗\}A⃗ ↓ X_{i}}{t ⊢ A_{i}[μX⃗\{U⃗′\}A⃗/X⃗]} ,

where U⃗′ = (U_{1}, …, U_{i−1}, U ∪ {t}, U_{i+1}, …, U_{n}) and the substitution [μX⃗{U⃗′}A⃗/X⃗] is an abbreviation for [μX⃗{U⃗′}A⃗ ↓ X_{1}/X_{1}, …, μX⃗{U⃗′}A⃗ ↓ X_{n}/X_{n}].

(Proving the above reductions correct is an easy generalisation to tagged fixed points of the proofs in [Andersen and Winskel, 1992] and [Andersen, 1993].)

7 Conclusion

The idea of compositionality being “not looking into the structure of subprocesses” could be formalised using a set of “meta-variables” x̂, ŷ, … distinct from the recursion variables. We should think of a variable x̂ as being a yet undefined process – a “hole” in the term. Any proof carried out with such variables appearing in the terms, would then be valid for all instantiations of the variable – capturing the reusability of proofs. However, in defining the substitution on terms with meta-variables, a little care must be taken. In, for example, rec x.a.ŷ we have the undefined process ŷ, which we might at some point decide to instantiate to the term x. Thus we would require (rec x.a.ŷ)[x/ŷ] = rec x.a.x. (Also, a substitution like ŷ[rec x.a.ŷ/x] cannot be reduced.)

It is interesting that the rules for recursion in combination with the tagging could actually help us in finding appropriate instantiations of metavariables. Consider as an example the term rec x.a.ŷ and the assertion νX{}⟨a⟩X expressing the existence of an infinite a-path. Using, in sequence, the rules (ν1),(rec⟨⟩),(.⟨⟩) we will end up with

ŷ[rec x.a.ŷ/x] ⊢ νX{rec x.a.ŷ}⟨a⟩X.

Suppose we would try to apply rule (ν0) in proving this valid. Then we would have to solve the equation ŷ[rec x.a.ŷ/x] = rec x.a.ŷ. A solution is to substitute x for ŷ, arriving at rec x.a.x ⊢ νX{rec x.a.x}⟨a⟩X, which by rule (ν0) is valid.^{3}

Returning to the proof system, we notice that compared to the earlier work of Stirling, Winskel, and Andersen and Winskel, the rules are few and quite simple. In particular, only three simple rules are needed to deal with fixed-point assertions, two to deal with recursive processes.

A useful amendment to the system is the possibility of relaxing the condition in (ν0) that t should be an element of the tags of the maximum fixedpoint to simply be strongly bisimilar to one of the tags. This amendment is straightforward since satisfaction in the modal μ-calculus is invariant under strong bisimulation, provided the tags are interpreted as equivalences classes. Another useful amendment would then be to combine the proof system with a proof system for bisimulation equivalence on processes.

In a recent paper [Andersen, 1995] it is shown how the quotienting combined with heuristics for simplifying simultaneous fixed points gives rise to a technique for handling the state explosion problem.

3The reduction for recursion given in [Andersen and Winskel, 1992] would, using some simplification steps, transform the satisfaction problem rec x.a.ŷ ⊢ νX.⟨a⟩X into the problem ŷ ⊢ νX.(⟨a⟩X ∨ {x}), where {x} is an assertion true at the variable x – called a state identifier there. Thus it can immediately be seen that substituting x for ŷ yields a solution. That reduction, however, is rather more involved and does not seem to give rise easily to a corresponding proof rule.

Appendix. Proofs

This appendix contains proofs of lemma 5 and theorem 2.

Lemma 5 The relation ≺ defined on closed assertions with tags from a finite set S by

A ≺ A′ iff A is a proper subassertion of A′, or A′ ≡ σX{U}B and

A ≡ B[σX{U, t}B/X] for some t ∉ U,

where σ is one of μ and ν, is well-founded.

Proof: Take the predicate Q(A) on closed assertions A with tags in S to be defined by

Q(A) ⇔_{def} all ≺-decreasing sequences from A are finite.

Extend this to open terms by

Q^{+}(A) ⇔_{def} ∀θ : F V (A) → ClAssn.
(∀X ∈ F V (A).Q(θ(X))) ⇒ Q(A[θ]).

Observe that if A is closed Q^{+}(A) is simply Q(A). The proof is by wellfounded induction on a slightly different relation ≺′ defined by

A′ ≺′ A iff A′ is a proper subassertion of A, or A ≡ σX{U}B and

A′ ≡ σX{U, t}B for some t ∉ U.

Since tags belong to the finite set S this relation is easily seen to be wellfounded. Thus assume for all A′ ≺′ A, Q^{+}(A) holds and ∀X ∈ F V (A).Q(θ(X)). We consider the possible first successor A′ in a ≺-decreasing sequence A[θ] ≻ A′ and argue that any continuation of the sequence must be finite. We consider the two possible reasons for A[θ] ≻ A′.

Case 1. A′ is a proper subassertion of A[θ]. Then either there exists a subassertion A′′ of A such that A′′[θ] ≡ A′, or A′ is a subassertion of some θ(X). In the first case the result follows from the induction hypothesis since A′′ ≺′ A; in the second it follows immediately from the assumption Q(θ(X)).

Case 2. In this case, A′ ≡ B[σX{U, t}B/X] and A[θ] ≡ σX{U}B. Either A ≡ Y and θ(Y) = σX{U}B or A ≡ σX{U}(B′[θ]) for some B′. In the first case the result follows from the assumption of Q(θ(Y)); in the second it can be shown from the induction hypothesis as follows. Since B ≡ B′[θ] and X ∉ F V (A), we can write A′ as

B′[θ][σX{U, t}(B′[θ])/X] ≡ B′[σX{U, t}B′/X][θ].

Hence, since σX{U, t}B′ ≺′ σX{U}B′ it follows from the induction hypothesis that Q^{+}(σX{U, t}B′) holds.

Take θ′(Y) = θ(Y) for Y ≠ X and θ′(X) = σX{U, t}(B′[θ]). Thus we have just argued Q(θ′(X)) and surely Q(θ′(Y)) for all Y ≠ X. Since B′ is a subassertion of A and therefore B′ ≺′ A we can again use the induction hypothesis to conclude Q(A[θ]).

□

Let the measure w(t) be defined by structural induction on terms t by

w(0) = w(x) = 0
w(a.t) = 0
w(t_{0} + t_{1}) = 1 + max{w(t_{0}), w(t_{1})}
w(rec x.t) = 1 + w(t)
w(t{Ξ}) = w(t ↾Λ) = 1 + w(t)
w(t_{0} × t_{1}) = 1 + w(t_{0}) + 2w(t_{1}).

We can now prove the following lemma:

Lemma 3 Assume a closed assertion B and a closed term t with guarded, regular recursions. If t ⊧ [κ]B (t ⊧ ⟨κ⟩B) then there exists some t_{1}, …, t_{n} with t_{i} ⊧ B and from t_{1} ⊢ B, …, t_{n} ⊢ B there is a proof of t ⊢ [κ]B (t ⊢ ⟨κ⟩B).

Proof: We prove the claim by showing ∀t.P (t) using well-founded induction on t with the ordering induced by w(t) where

P (t) ⇔_{def} for all closed, extended assertions A,

if t ⊧ [κ]A then

∃t_{1}, …, t_{n}. t_{i} ⊧ A, and

t ⊢ [κ]A can be proven from {t_{i} ⊢ A}_{i}.

We shall only consider the case for the box-modality, the case of diamondmodality is similar. Thus assume for all t′ with w(t′) < w(t) that P (t′) holds and assume further that t ⊧ [κ]A. We shall establish P (t) on these assumptions by considering the possible forms of t.

However, consider first the case where ∗ ∈ κ. Then from the semantics we observe that t ⊧ A and t ⊧ [κ \ ∗]A. The first is already on the required form hence take t_{1} ≡ t; for t ⊧ [κ \ ∗]A the steps below assuming ∗ ∉ κ provides the required remaining t_{2}, …, t_{n} to establish P (t) using rule ([]∗). Thus assume in the sequel ∗ ∉ κ.

t ≡ 0. Immediate from rule (0[]).

t ≡ a.t′. If a ∈ κ then t′ ⊧ A and rule (.[]0) gives a proof of a.t′ ⊢ [κ]A from a proof of t′ ⊢ A. This shows P (t) in this case.

If a ∉ κ then rule (.[]1) immediately gives a proof of a.t′ ⊢ [κ]A showing P (t) in this case.

t ≡ t_{0} + t_{1}. It follows from the semantics of assertions that t_{0} ⊧ [κ]A and t_{1} ⊧ [κ]A, hence since w(t_{0}) < w(t) and w(t_{1}) < w(t) if follows by induction that there exists t_{0}^{1}, …, t_{0}^{m} and t_{1}^{1}, …, t_{1}^{n} with t_{0}^{i} ⊧ A and t_{1}^{j} ⊧ A such that proofs of t_{0} ⊢ A and t_{1} ⊢ A can be constructed from proofs of t_{0}^{i} ⊢ A and t_{1}^{j} ⊢ A. Thus using rule (+[]) we can get a proof of t_{0} + t_{1} ⊢ A completing this case.

t ≡ rec x.t′. It follows from proposition 1 that t′[rec x.t′/x] ⊧ [κ]A. Now, since all recursions are guarded and regular w(t′[rec x.t′/x]) < w(rec x.t′) hence by the induction hypothesis there exists t_{1} ⊧ A, …, t_{n} ⊧ A such that a proof of t′[rec x.t′/x] ⊢ [κ]A can be constructed from proofs of t_{i} ⊢ A. Applying rule (rec[]) to such a proof we have shown P (t) in this case.

t ≡ t′{Ξ}. It follows from downwards soundness of rule ({Ξ}[]) that t′ ⊧ [Ξ^{−1}(κ)](A{Ξ}). Since w(t′) < w(t) it follows by induction that there exists t′_{1}, …, t′_{n} such that t′_{i} ⊧ A{Ξ} and that from proofs of t′_{i} ⊢ A{Ξ} we can construct a proof of t′ ⊢ [Ξ^{−1}(κ)](A{Ξ}). Now, to extend this to a proof of t′{Ξ} ⊢ [κ]A first take t_{i} ≡ t′_{i}{Ξ}. Hence from proofs of t_{i} ⊢ A, i.e. t′_{i}{Ξ} ⊢ A, we get proofs of t′_{i} ⊢ A{Ξ} using rule ({Ξ}). Finally, using rule ({Ξ}[]) we get a proof of t′{Ξ} ⊢ [κ]A from a proof of t′ ⊢ [Ξ^{−1}(κ)](A{Ξ}) which as we have just argued can be proven from t_{1} ⊢ A, …, t_{n} ⊢ A.

t ≡ t′ ↾Λ. As above but using rules (↾Λ) and (↾Λ[]). t ≡ t_{0} × t_{1}.

If κ/∗ ≠ ∅ we can remove the set (κ/∗) × {∗} by applying rule (×[]∗) and proceed as below – exactly like in the case of ∗ ∈ κ considered in the beginning of the proof. Hence, in the sequel assume κ/∗ = ∅ and consider the possible forms of t_{1}.

t_{1} ≡ 0, t_{1} ≡ a.t′, t_{1} ≡ t′_{1} + t′′_{1}, t_{1} ≡ rec x.t′. Analogous to the cases above. See the discussion in section 3.3 about the relationship between the product dynamic rules and the dynamic rules.

t_{1} ≡ t′_{1}×t′′_{1}. A little bit of arithmetic shows w((t_{0}×t′_{1})×t′′_{1}) < w(t):

w((t_{0} × t′_{1}) × t′′_{1})
= 1 + w(t_{0} × t′_{1}) + 2w(t′′_{1})
= 1 + (1 + w(t_{0}) + 2w(t′_{1})) + 2w(t′′_{1})
= 1 + w(t_{0}) + 1 + 2w(t′_{1}) + 2w(t′′_{1})
< 1 + w(t_{0}) + 2(1 + w(t′_{1}) + 2w(t′′_{1}))
= w(t_{0} × (t′_{1} × t′′_{1})) = w(t)

Thus P (t) follows from the induction hypothesis and rule (××).

t_{1} ≡ t′_{1}{Ξ}. As above we compute:

w((t_{0} × t_{1}){Ξ})
= 1 + w(t_{0} × t_{1})
= 1 + (1 + w(t_{0}) + 2w(t_{1}))
< 1 + w(t_{0}) + 2(1 + w(t_{1}))
= w(t_{0} × (t_{1}{Ξ}))

Thus P (t) follows from the induction hypothesis and rule (×{Ξ}).

t_{1} ≡ t′_{1} ↾Λ. As above.

□

The proof of completeness now follows by well-founded induction on the relation ≺:

Theorem 2 (Completeness for finite-state processes) If p is a process with guarded regular recursions then for all closed assertions A with tags in S_{p},

p ⊧ A ⇒ p ⊢ A. 25

Proof: Let Q(A) be defined on closed assertions with tags in S_{p} by

Q(A) ⇔_{def} ∀t ∈ S_{p}. t ⊧ A ⇒ t ⊢ A.

We prove Q(A) for all closed assertions with tags in S_{p} by induction on ≺. Hence assume Q(A′) for all A′ ≺ A.

We consider the potential forms of A.

A ≡ X. Impossible since A is assumed to be closed.

A ≡ A_{0} ∧ A_{1}. Since t ⊧ A_{0} ∧ A_{1} implies t ⊧ A_{0} and t ⊧ A_{1}, and, moreover, A_{0} ≺ A, and A_{1} ≺ A the result follows from the induction hypothesis applying rule (∧).

A ≡ A_{0} ∨ A_{1}. Since t ⊧ A_{0} ∨ A_{1} implies t ⊧ A_{0} or t ⊧ A_{1}, and, moreover, A_{0} ≺ A, and A_{1} ≺ A the result follows from the induction hypothesis applying either rule (∨0) or (∨1).

A ≡ μX{U}B. From lemma 1 it follows that if t ⊧ μX{U}B then t ⊧ B[μX{U, t}B/X] and as it can easily be seen from the semantics of tagged minimum fixed points, t ∉ U. Thus rule (μ) can be applied to yield a proof of t ⊢ μX{U}B from a proof of t ⊢ B[μX{U, t}B/X]. Since B[μX{U, t}B/X] ≺ μX{U}B we have by the induction hypothesis a proof of B[μX{U, t}B/X] completing this case.

A ≡ νX{U}B. If t ∈ U, rule (ν0) immediately yields a proof of t ⊢ νX{U}B. If t ∉ U but t ⊧ νX{U}B if follows from lemma 1 that t ⊧ B[νX{U, t}B/X] thus rule (ν1) gives a proof of t ⊢ νX{U}B from a proof of t ⊢ B[νX{U, t}B/X]. Since B[νX{U, t}B/X] ≺ νX{U}B we have by the induction hypothesis a proof of B[μX{U, t}B/X] completing this case.

A ≡ [κ]B, A ≡ ⟨κ⟩B. Assuming t ⊧ [κ]B it follows from lemma 3 that there exists t_{1}, …, t_{n} such that t_{i} ⊧ B and t ⊧ [κ]B can be proven from proofs of t_{i} ⊢ B. However, since B ≺ [κ]B it follows from the induction hypothesis that such proofs do indeed exist, completing the case for the box-modality. The case for the diamond-modality is similar.

□

References

[Andersen, 1993] Andersen, H. R. (1993). Verification of Temporal Properties of Concurrent Systems. PhD thesis, Department of Computer Science, Aarhus University, Denmark. PB-445.

[Andersen, 1994] Andersen, H. R. (1994). Model checking and Boolean graphs. Theoretical Computer Science, 126(1):3–30.

[Andersen, 1995] Andersen, H. R. (1995). Partial model checking (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 398–407, La Jolla, San Diego. IEEE Computer Society Press.

[Andersen and Winskel, 1992] Andersen, H. R. and Winskel, G. (1992). Compositional checking of satisfaction. Formal Methods in System Design, 1(4).

[Arnold and Crubille, 1988] Arnold, A. and Crubille, P. (1988). A linear algorithm to solve fixed-point equations on transition systems. Information Processing Letters, 29:57–66.

[Bekič, 1984] Bekič, H. (1984). Definable operations in general algebras, and the theory of automata and flow charts. In C.B.Jones, editor, Hans Bekič: Programming Languages and Their Definition, volume 177, pages 30–55. Springer-Verlag.

[Cleaveland, 1990] Cleaveland, R. (1990). Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27:725–747.

[Cleaveland et al., 1992] Cleaveland, R., Dreimüller, M., and Steffen, B. (1992). Faster model checking for the modal mu-calculus. In [v. Bochmann and Probst, 1992], pages 383–394.

[Cleaveland and Steffen, 1992] Cleaveland, R. and Steffen, B. (1992). A linear-time model-checking algorithm for the alternation-free modal mucalculus. In Larsen, K. G. and Skou, A., editors, Proceedings of the 3rd Workshop on Computer Aided Verification, July 1991, Aalborg, volume 575 of LNCS. Springer-Verlag.

[Emerson and Lei, 1986] Emerson, E. A. and Lei, C.-L. (1986). Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of Symposium on Logic in Computer Science, pages 267–278, Cambridge. IEEE.

[Kozen, 1983] Kozen, D. (1983). Results on the propositional mu-calculus. Theoretical Computer Science, 27.

[Larsen, 1988] Larsen, K. G. (1988). Proof systems for Hennessy-Milner logic with recursion. In Dauchet, M. and Nivat, M., editors, Proceedings of CAAP, Nancy, Franch, volume 299 of Lecture Notes in Computer Science, pages 215–230.

[Larsen, 1992] Larsen, K. G. (1992). Efficient local correctness checking. In [v. Bochmann and Probst, 1992].

[Larsen and Xinxin, 1990] Larsen, K. G. and Xinxin, L. (1990). Compositionality through an operational semantics of contexts. In Paterson, M., editor, Proceedings of ICALP, volume 443 of LNCS, pages 526–539. Springer-Verlag.

[Milner, 1989] Milner, R. (1989). Communication and Concurrency. Prentice Hall.

[Stirling, 1985a] Stirling, C. (1985a). A complete compositional modal proof system for a subset of CCS. volume 194 of Lecture Notes in Computer Science, pages 475–486. Springer-Verlag.

[Stirling, 1985b] Stirling, C. (1985b). A complete modal proof system for a subset of SCCS. volume 185 of Lecture Notes in Computer Science, pages 253–266. Springer-Verlag.

[Stirling, 1987] Stirling, C. (1987). Modal logics for communicating systems. Theoretical Computer Science, 49:311–347.

[Stirling, 1992] Stirling, C. (1992). Modal and Temporal Logics. In Abramsky, S., Gabbay, D., and Maibaum, T., editors, Handbook of Logic in Computer Science, volume 2, pages 477–563. Oxford University Press.

[Stirling and Walker, 1991] Stirling, C. and Walker, D. (1991). Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161–177.

[Tarski, 1955] Tarski, A. (1955). A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309.

[v. Bochmann and Probst, 1992] v. Bochmann, G. and Probst, D. K., editors (1992). Proceedings of the 4th Workshop on Computer Aided Verification, CAV’92, June 29 - July 1, 1992, Montreal, Quebec, Canada, volume 663 of LNCS. Springer-Verlag.

[Vergauwen and Lewi, 1992] Vergauwen, B. and Lewi, J. (1992). A linear algorithm for solving fixed-point equations on transition systems. In Raoult, J.-C., editor, Proceedings of 17’th Colloquium on Trees in Algebra and Programming, CAAP’92, Rennes, France, volume 581 of LNCS, pages 322– 341. Springer-Verlag.

[Winskel, 1984] Winskel, G. (1984). Synchronisation trees. Theoretical Computer Science, 34:33.

[Winskel, 1985] Winskel, G. (1985). On the composition and decomposition of assertions. Technical Report TR-59, Computer Laboratory, University of Cambridge.

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

[Winskel, 1989] Winskel, G. (1989). A note on model checking the modal νcalculus. In Ausiello, G., Dezani-Ciancaglini, M., and Rocca, S. R. D., editors, Proceedings of ICALP, volume 372 of LNCS, pages 761–772. Springer-Verlag.

[Winskel, 1990a] Winskel, G. (1990a). A compositional proof system on a category of labelled transition systems. Information and Computation, 87.

[Winskel, 1990b] Winskel, G. (1990b). On the compositional checking of validity. In Baeten, J. and Klop, J., editors, Proceedings of CONCUR ’90, volume 458 of LNCS, pages 481–501. Springer-Verlag.

Recent BRICS Report Series Publications

RS-98-40 Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal μ-Calculus. December 1998. 29 pp.

RS-98-39 Daniel Fridlender. An Interpretation of the Fan Theorem in Type Theory. December 1998. 15 pp. To appear in International Workshop on Types for Proofs and Programs 1998, TYPES ’98 Selected Papers, LNCS, 1999.

RS-98-38 Daniel Fridlender and Mia Indrika. An n-ary zipWith in Haskell. December 1998. 12 pp.

RS-98-37 Ivan B. Damgård, Joe Kilian, and Louis Salvail. On the (Im)possibility of Basing Oblivious Transfer and Bit Commitment on Weakened Security Assumptions. December 1998. 22 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EUROCRYPT ’99 Proceedings, LNCS, 1999.

RS-98-36 Ronald Cramer, Ivan B. Damgård, Stefan Dziembowski, Martin Hirt, and Tal Rabin. Efficient Multiparty Computations with Dishonest Minority. December 1998. 19 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EURO-CRYPT ’99 Proceedings, LNCS, 1999.

RS-98-35 Olivier Danvy and Zhe Yang. An Operational Investigation of the CPS Hierarchy. December 1998.

RS-98-34 Peter G. Binderup, Gudmund Skovbjerg Frandsen, Peter Bro Miltersen, and Sven Skyum. The Complexity of Identifying Large Equivalence Classes. December 1998. 15 pp.

RS-98-33 Hans Hüttel, Josva Kleist, Uwe Nestmann, and Massimo Merro. Migration = Cloning ; Aliasing (Preliminary Version). December 1998. 40 pp. To appear in 6th International Workshop on the Foundations of Object-Oriented, FOOL6 Informal Proceedings, 1998.

RS-98-32 Jan Camenisch and Ivan B. Damgård. Verifiable Encryption and Applications to Group Signatures and Signature Sharing. December 1998. 18 pp.