bound by a modality. An assertion A is guarded if all predicates in A are guarded with respect to all variables. ✷
Lemma 2.5 Let A be a guarded, closed assertion and assume that T is a transition system with finite basic label-set L. Then there exists an assertion A without action quantifiers or predicates, such that
|=T A↔A
If the predicates appearing in A are decidable, then A is computable from A.
Proof: For assertions guarded with respect to α, lemma 2.3 can easily be strengthened to
a /∈L⇒ ∀ρ, φ. [[A]]T,Vρ φ[a/α] = [[A]]T,Vρ φ[#/α]
for all basic actions a.
As in lemma 2.4 now each subexpression∃α.B can be replaced by
a∈L∪{#}
B[a/α].
If the predicates are computable, all predicates now being applied to variable-free action expressions can be algorithmically replaced by truth-values, mak-ing A computable from A. ✷
Example 2.4 Many apparently unguarded assertions can be transformed to guarded assertions. Consider for instance the unguarded assertion ∃α.(a ∈ Λ)∧ αA abbreviating ΛA for any (possibly infinite) set of actions Λ. It is equivalent to the guarded assertion ∃α.α((α ∈ Λ)∧A). Hence, assum-ing that Λ is a computable set, ΛA always has a quantifier-free version on transition systems with finite basic label-set by lemma 2.5. ✷
2.8 Bibliographic Notes
The generic process algebra WPA introduced here appears in work of Winskel [91]. Discussions about the applicability of process algebras as models of con-current systems and intuitions behind the various operators can be found in
various textbooks like Milner’s book [59] and Hoare’s book [42]. The process algebra OPA which only differs from CCS in the respect that synchronized actions are visible seems to have the benefit of making it possible to verify even closed systems (i.e. without external synchronization being allowed) using the µ-calculus because it is possible to investigate the behaviour of synchronized actions – which is impossible for CCS where any closed system is (weakly) equivalent to nil! Hence OPA offers a solution to the “probe problem” reported by Walker in [87].
In the modal logic community labelled transition systems are often called Kripke models and are defined slightly differently but the differences are inessential. They are also sometimes – especially when only one action is present – called “possible world semantics” indicating the more philosophical approach to modal logics as explained in Hughes and Cresswell [44].
The modal µ-calculus – here called the standard calculus – is due to Kozen [49] based upon earlier work by Park [68], Hitchcock, Scott, de Bakker, de Roever, and Pratt. Kozen, who refers to the logic as thepropositional µ-calculus, has proven a range of results about the logic which we will return to in chapter 9. The term ‘modal µ-calculus’ and the name µK is due to Stirling – who observed that the logic is really the minimal modal logic K extended with fixed-points (see for example [79]).
The idea of extending theµ-calculus with simultaneous fixed-points has been recognized by other authors as being important. This is the case in for instance the work of Larsen and Xinxin [57], Arnold and Crubille [9], and Cleaveland and Steffen [27]. However, even though Larsen and Xinxin introduces a notation for simultaneous fixed-points they do not allow for nested fixed-points to ‘share across products’ (i.e. the ability for several components of a simultaneous fixed-point to refer to variables of another simultaneous fixed-point without duplicating it), which is going to be a key stepin making the reductions for the compositional method and the model-checking algorithms efficient. A similar construction achieving the effect of
‘sharing across products’ is implicitly present in Cleaveland, Dreim¨uller and Steffen [24].
Bekiˇc’s theorem dates back to the late sixties and appears in unpublished manuscripts by Scott and de Bakker, Park, and Bekiˇc. The earliest publically available version the present author has been able to find is in a collection of Hans Bekiˇc’s papers [12] from 1984, where it appears in a paper dated 8.
December 1969. The theorem is there called the ‘bisection lemma.’
2.8 Bibliographic Notes 47 Thanks are due to Dirk Taubner for a useful discussion on the subtleties in generating finite-state systems from CCS terms and for drawing my at-tention to his thesis [83].
Chapter 3
Compositional Checking of Satisfaction
In the modal logic approach to verification the central problem of verifying that systems meet their specifications correspond to determining satisfaction, i.e. deciding whether a given model satisfies a given assertion. In this chapter we present a compositional method for deciding satisfaction, centered around the standard calculus but also with generalizations to the extended calculus.
The method iscompositional in the structure of the processes and works purely on the syntax of processes. It consists of applying a sequence of re-ductions, each of which only take into account the top-level operator of the process (except the reduction for product which inspects one of the compo-nents). Such a reduction transforms a satisfaction problem for a composite process into equivalent satisfaction problems for the immediate subcompo-nents - without inspecting the internal structure of these.
Using process variables, systems with undefined subcomponents can be defined, and given an overall requirement to the system, necessary and su-ficient conditions on these subcomponents can be found. Hence the process variables make it possible to specify and reason about what are often referred to as contexts, environments, and partial implementations.
Compositionality is important for at least the following reasons. Firstly, it makes the verification modular, so that when changing a part of a sys-tem only the verification concerning that particular part must be redone.
Secondly, when designing a system or synthesizing a process the composi-tionality 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 incon-sistencies 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 previ-ous verification can be used to show that they meet the requirements on the components of a larger system.
We first describe the reductions for the standard calculus then look at some examples and finally discuss how to generalize the reductions to the extended calculus.
3.1 Introduction
In the process of deriving the reductions we will temporarily have to internal-ize the correctness assertions (t :A) into the logic which is then an extension of the standard calculus which we will refer to as µK(:). It has the following syntax:
A::= F | ¬A|A0∨A1 | aA|X |µX.A|(t:A)
We still require the correctness assertions (t:A) to be well-formed, i.e. tmust be mono-typed andtype(A)⊆type(t). We will say that an assertionAispure if it does not contain any correctness assertions, hence a pure assertion in µK(:) is really an assertion in the standard calculus. A correctness assertion (t : A) is pure if A is pure, and we shall later show that all correctness assertions can be made pure.
A correctness assertion (t : A) is to denote true or false depending on whether t satisfies A or not. This suggests the following simple extension of the semantics using superscript (:) to indicate that assertions are fromµK(:):
[[(t :A)]](:)T ρ=
ST if t∈[[A]](:)T ρ
∅ otherwise
Instead of using t ∈ [[A]](:)T ρ we could just as well, according to the locality lemma, take t ∈ [[A]](:)T φ. However, there is a small problem with the envi-ronmentρ. On the left-hand side ρ is a mapAssnV ar → P(ST) but on the
3.1 Introduction 51 right-hand side we need an environment ρ : AssnV ar → P(P rocW P A) or ρ:AssnV ar → P(Rt) depending on whether we use the global or local view.
If A is closed we could take any environment ρ of the right kind and get a well-defined semantics. Unfortunately, during the reductions assertions con-taining correctness assertions over various different terms with free variables will appear, and therefore the environment used in the semantics must map these variables to subsets of states of the corresponding transition systems.
Sticking to a global semantics using the universal transition system T and only consider environments mapping all variables to subsets of P rocWPA is not a useful solution because the reductions will require a local view.
The solution we take is to give the semantics of assertions inµK(:) with respect to environmentsρwhich respect the ‘types’ of the free assertion vari-ables. We annotate variables with types (i.e. transition systems) according to the following rules: Let T be a transition system. Then AT is the type-annotated assertion constructed from A by annotating all variables X not within correctness assertions as XT. If X appears inside a correctness asser-tion we annotateXwith the process term of the nearest enclosing correctness assertion. For example (X∨(t :Y ∨(t :Z)))T =XT ∨(t:Yt∨(t :Zt)).
An environment ρ : AssnV ar → P(P rocWPA) respects the types of the assertion AT if for all free variablesXT,
ρ(XT)⊆ST ⊆P rocWPA (3.1) This is trivially fulfilled by a closed assertion and the open assertions appear-ing durappear-ing[-5mm] the construction of the reductions will turn out to satisfy (3.1).
Given an environment ρ satisfying (3.1) for all free variables of AT we now define [[AT]](:)T ρ by structural induction on A.
Notice, that if A is pure then if ρ maps all free variables to P(ST), then ρ respects the types of AT and for any environment AssnV ar → P(ST) we have [[AT]](:)T ρ = [[A]]Tρ, hence for pure assertions we could just use the standard semantics.
The technical difficulties we have just experienced will not be fully re-warded until the reduction for product, which is the only reduction where correctness assertions will have to be nested.
The correctness assertions (t : A) will also be atoms in a propositional logic L which will be used to express the reductions.1 A grammar for the logic L is:
L::=T | ¬L|L0 ∨L1 |(t :A)
where A is an assertion in µK(:). Satisfaction in L of a formula L is de-fined, relative to an environmentρwhich respects the type of the correctness assertions of L, as follows:
|=ρ T always
|=ρ ¬L iff not|=ρL
|=ρ L0∨L1 iff |=ρL0 or L1
|=ρ t:A iff t∈[[At]](:)t ρ Furthermore we define the derived predicate |= as:
|=L iff for all ρ|=ρL.
Taking • to be the trivial transition system with one state (denoted •) and no transitions, we observe that the set of assertions built from correctness assertions, negations, and conjunctions when interpreted over•is essentially a copy of the logicL, i.e. for such an assertionAwe have [[A]]•ρ={•}if and only if|=ρA where A is interpreted as a formula in the propositional logic.
InL we are able to express complex relationships between properties of different processes. For example
(p+q:aA)↔(p:aA)∨(q :aA),
1This propositional logic is of course a sublogic of the above definedµ-calculus, but it will be beneficial to keep the two levels separate. The correctness assertions appearing in the assertions only have a temporary existence and will ultimately be removed whereas the correctness assertions in the propositional logic are crucial for expressing the reductions.
3.1 Introduction 53 expresses a very simple example of a reduction. It states that the process p+q can perform an a-action and get into a state that satisfies A if and only if p or q can do an a-action and get into a state that satisfies A. It is a reduction because the formula is valid for all p’s and q’s, and the validity of (p+q : aA) is reduced to validity of correctness assertions over the subterms p and q. Although this reduction is almost trivial, in general, it might be quite difficult to get reductions. Consider for example the problem of choosing a B such that
(rec P.t:µX.A)↔(t:B)
holds. The aim of this chapter is to describe a method for generating such a B and analogous assertions for all the other operators.
In constructing these reductions we will be involved with therooting of transition systems which is defined as follows.
Definition 3.1 Given a pointed transition system T = (S, i, L,→) the rooting of T is a pointed transition system T = (S ∪ {i}, i, L,→) where i is a new state assumed not to be in S, and the transition relation →⊆ (S∪ {i})×L×(S∪ {i}) is defined by:
→ = → ∪{(i, a, q)|i→a q}.
✷
Figure 3.1: The rooting of a transition system. Notice, that no transitions enter i.
Pictorially the rooting of a pointed transition system is constructed by ad-joining a new initial state with the same out-going transitions as the old initial state (see figure 3.1). The rooting of a transition system T is “just as good as T” with respect to satisfaction in our logic. A claim made precise by the rooting lemma below.
Lemma 3.1 (Rooting lemma.)
Given a pointed transition system,T = (ST, i, L,→T),where ST is countable and with the rooting T. Let r : P(ST) → P(ST ∪ {i}) be the map on prop-erties that take the initial state of T to the two copies of it in T and take all other states to their obvious counterparts. Assume A is a pure assertion.
Let ρ:AssnV ar → P(ST) be an environment of assertions which since A is pure, respects the types of A. Then
r([[A]]T ρ) = [[A]]T(r◦ρ).
Proof: See appendix A.1. ✷
The connection given by the rooting lemma between pointed transition systems T and their rootings T could be summarized as: The set of states satisfying an assertion will be the same in both interpretations up to applica-tion of the mapr. In particular the initial state ofT will satisfyAif and only if the initial state ofT satisfiesA; an observation central to our development of reductions in section 3.2.