BRICS RS-97-13 Andersen & Larsen: Compositional Safety Logics BRICS

Basic Research in Computer Science

Compositional Safety Logics

Jørgen H. Andersen Kim G. Larsen BRICS Report Series RS-97-13 ISSN 0909-0878 June 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, 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/97/13/

COMPOSITIONAL SAFETY LOGICS

J.H. Andersen and K.G. Larsen BRICS, Aalborg University, Denmark

June 17, 1997

In this paper we present a generalisation of a promising compositional model–checking technique introduced for finite–state systems by Andersen in [And95] and extended to networks of timed automata by Larsen et al in [LPY95a, LL95, LPY95b, KLL^{+}97a]. In our generalized setting, programs are modelled as arbitrary (possibly infinite–state) transition systems and verified with respect to properties of a basic safety logic. As the fundamental prerequisite of the compositional technique, it is shown how logical properties of a parallel program may be transformed into necessary and sufficient properties of components of the program. Finally, a set of axiomatic laws are provided useful for simplifying formulae and complete with respect to validity and unsatisfiability.

1 Introduction

It is well–known that the major problem in applying automatic verification techniques to analyze concurrent systems is the potential combinatorial explosion of the state space arising from parallel composition. During the last decade, various techniques have been developed to avoid this explosion problem, either by symbolic representation of the state space using BDD [BCM^{+}90, GW91], by application of partial order methods [GW91, Val90] which suppresses unnecessary interleavings of transitions, or by application of abstractions and symmetries [BCM^{+}90, CFJ93, CGL92]. A recently introduced [And95] and very promising technique is a compositional technique, which avoids global state–space construction and – exploration by gradually moving components of a concurrent system from the system description into the specification. Consider the following verification problem

(P_{1} | … | P_{n}) ⊧ φ  (1.1)

where (P_{1} | … | P_{n}) is the concurrent system to be verified and φ is a formula specifying a desired property. The compositional technique allows a component (P_{n} say) to be removed from the network and instead added to the specification φ. This results in a quotient formula φ/P_{n} expressing the sufficient and necessary property of (P_{1} | … | P_{n−1}) in order that (1.1) holds. That is, the original verification problem reduces to

(P_{1} | … | P_{n−1}) ⊧ φ/P_{n}  (1.2)

Now repeating this process of quotienting iteratively yields equivalent verification problems with decreasing numbers of components and hence decreasing state–space sizes. However, this idea alone is clearly not enough to solve the explosion–problem as the explosion may now show up as an exponential growth in the sizes of the quotient formulas instead. The crucial observation in [And95] is that each quotienting should be followed by a minimization of the formula based on a small collection of efficiently implementable strategies. The three parameters to the compositional method are the following: 1) the components P_{i} and their semantic modelling; 2) the notion of parallel composition, and 3) the logic for specifying properties. In order for the compositional method to be applicable the combination of the three parameters must obviously satisfy the following two criteria:

1. The logic must be expressive enough that the quotient formulas can be expressed.

2. There must be heuristics for simplifying formulas of the logic.

In [And95] the compositional method is developed for a setting of finite–state systems with parallel composition being that of CCS [Mil89]. As specification formalism is used the modal μ-calculus [Koz82]. Using a prototype implementation experimental evidence is given that the technique may improve results obtained using BDDs. In [LPY95a, LL95, LPY95b] the compositional method has been extended to deal with real–time systems modelled as networks of timed automata [AD90, AD92], with a real–time version of the modal μ–calculus [LLW95] used as specification formalism. In [KLL^{+}97b] the real–time extension of the technique is applied to the verification of a mutual exclusion protocol; experimental results obtained using a tool implementation of the method gives further evidence of the potential of technique. In this paper we show how to satisfy the basic requirements of the compositional method in a generalized setting, where the components are modelled as arbitrary (possibly infinite–state) transition systems The notion of parallel composition is that of interleaving, and as specification formalism is considered a minimal safety logic. To meet the two criteria of the compositional method, the safety logic is extended in a minimal way to be closed with respect to quotienting. Possible strategies for simplifying formulas are suggested by a set of axiomatic laws for formula equivalence. The laws are shown complete with respect to validity and unsatisfiability of formulas. The paper is organized as follows: In the next section we describe our general setting for modelling parallel programs. For this setting we introduce in Section 3 a minimal modal for expressing safety properties. A necessary extension of this logic allowing for quotienting is then provided in Section 4. In Section 5 we present an axiomatization allowing formulae to be simplified and being complete with respect to validity and unsatisfiability. Finally, we apply the quotient construction and the provided axiomatization to the verification of a (simple) shared variable program in Section 6.

\{ \begin{matrix}P_{1} =^{Δ} \\ loop_{1} : & if x ≥ MAX \\ then goto exit & 1 \\ & else x := x + 1; \\ goto loop & 1 \\ exit_{1} : \end{matrix} \} | \{ \begin{matrix}P_{2} =^{Δ} \\ loop_{2} : & if x = 0 \\ then goto exit & 2 \\ & else x := x − 1; \\ goto loop & 2 \\ exit_{2} : \end{matrix} \}

Figure 1: A parallel counter.

2 Programs and Transition Systems

Component programs as well as their composition are modelled as arbitrary transition systems.

Definition 1 (Transition system)A transition system is a tuple ⟨S, s_{0}, Σ⟩ where: S is a set of states, s_{0} ∈ S is a start state and Σ ⊂ S×S is a transition relation. ◇

Parallel composition is equally general: given two transition systems T_{1} = ⟨S, s_{0}, Σ_{1}⟩ and T_{2} = ⟨S, s_{0}, Σ_{2}⟩ over the same set of states and with the same start state we define the composition of T_{1} and T_{2} as the transition system T = T_{1} | T_{2} = ⟨S, s_{0}, Σ_{1} ∪ Σ_{2}⟩. That is we model parallel composition as pure interleaving. In typical applications, the state–space S of a composition of programs P = P_{1} | ⋯ | P_{n} over a shared data–domain D will be described as the product of the local state-spaces S_{i} of the individual programs and D, that is S = S_{1} × ⋯×S_{n} ×D. To ensure that S_{i} acts as a local state–space for the component P_{i}, one may impose the following constraint on the transition relation Σ_{i} modelling the behaviour of P_{i}: whenever (⟨s_{1}, …, s_{n}, d⟩, ⟨s′_{1}, …, s′_{n}, d′⟩) ∈ Σ_{i} then s_{j} = s′_{j} for all j ≠ i. Thus, transitions of P_{i} may depend on the global state but can only effect the local state of P_{i} and the shared data.

Example 1 [Parallel counter] Consider the program of Figure 1. Both component programs P_{1} and P_{2} have two local control–states. In the loop state P_{1} repeatedly increments the value of the shared variable x until it reaches the value MAX, at which point P_{1} goes to the terminating exit control state. Dually, in the loop control state, P_{2} repeatedly decrements x unless it has reached the value 0, at which point P_{2} goes to the terminating exit control state. In the interleaved parallel composition of P_{1} and P_{2}, the value of x will in most states be incremented or decremented non–deterministically. Thus, the termination properties of the combined program is less obvious than those of the component programs. Formally, we describe P_{1} and P_{2} in terms of transition systems:

T_{i} = ⟨S_{1} × S_{2} × ℕ, ⟨loop_{1}, loop_{2}, 0⟩, Σ_{i}⟩, i ∈ {1, 2}

where S_{i} = {loop_{i}, exit_{i}} and:

Σ_{1} = {(⟨loop_{1}, l_{2}, n⟩, ⟨loop_{1}, l_{2}, n + 1⟩) | n < MAX and l_{2} ∈ S_{2}} ∪
{(⟨loop_{1}, l_{2}, n⟩, ⟨exit_{1}, l_{2}, n⟩) | n ≥ MAX and l_{2} ∈ S_{2}}
Σ_{2} = {(⟨l_{1}, loop_{2}, n⟩, ⟨l_{1}, loop_{2}, n − 1⟩) | n > 0 and l_{1} ∈ S_{1}} ∪
{(⟨l_{1}, loop_{2}, n⟩, ⟨l_{1}, exit_{2}, n⟩) | n ≤ 0 and l_{1} ∈ S_{1}}

The composition of P_{1} and P_{2} is then described by the transition system:

T = ⟨S_{1} × S_{2} × ℕ, ⟨loop_{1}, loop_{2}, 0⟩, Σ_{1} ∪ Σ_{2}⟩
◇

3 Safety Logic

We first introduce a minimal modal logic, L_{S}^{safe}, for expressing safety properties of programs over a given set of states S. Formulae in L_{S}^{safe} are given by the following BNF:

φ ::= B | φ ∧ φ | □φ | X

where B ⊆ S is a condition over a set of states and X is a formula identifier of a finite set of identifiers Id. X is declared by some declaration D ∈ Id → L_{S}^{safe}. Note that L_{S}^{safe} is parameterized with the set of states over which conditions are expressed. A formula φ of L_{S}^{safe} is interpreted with respect to a declaration and a transition relation in the following obvious sense:

Definition 2 Let S be a set of states and Σ ⊆ S × S a transition relation over S. Let D ∈ Id → L_{S}^{safe} be a declaration. The satisfaction relation ⊧_{D,Σ} is the maximal relation satisfying the following set of implications:

s ⊧_{D,Σ} φ ∧ ψ ⇒ s ⊧_{D,Σ} φ and s ⊧_{D,Σ} ψ
s ⊧_{D,Σ} □φ ⇒ whenever (s, s′) ∈ Σ then s′ ⊧_{D,Σ} φ
s ⊧_{D,Σ} B  ⇒ s ∈ B
s ⊧_{D,Σ} X  ⇒ s ⊧_{D,Σ} D(X)
◇

Any relation satisfying the above implications is a satisfiability relation. It follows from standard fixpoint theory [Tar55] that ⊧_{D,Σ} is the union of all satisfiability relations and that the above implications are biimplications for ⊧_{D,Σ}.

Example 2 Continuing Example 1, we may wonder whether there are executions of P_{1} | P_{2} in which P_{2} will terminate. Let ¬exit_{2} denote the set of all states ⟨l_{1}, l_{2}, n⟩ where l_{2} ≠ exit_{2}. Then the property that no execution will bring P_{2} to termination may be expressed as follows ^{1}

X =^{Δ} ¬exit_{2} ∧ □X

◇

4 Quotienting and L_{S}

Now let P_{1} and P_{2} be component programs modelled as transition relations Σ_{1} and Σ_{2} over some common global state space S. Verification problems for P_{1} | P_{2} then becomes assertions of the form s ⊧_{D,Σ_{1}∪Σ_{2}} φ. To meet the requirements of the compositional method, we are required to describe a technique for moving parts of Σ_{1} ∪ Σ_{2} (say Σ_{2} which corresponds to the component P_{2}) into φ. More precisely, we offer a construction for quotienting a formula φ with respect to a transition relation Σ_{2} such that:

s ⊧_{D,Σ_{1}∪Σ_{2}} φ iff s ⊧_{D,Σ_{1}} φ/_{Σ_{2}}

1Clearly P_{1} | P_{2} does not satisfy this property and later (in Section 6) we shall provide a proof of this fact using the compositional proof technique.

In order to express quotient formulae we extend L_{S}^{safe} with a new construction Δ ↠ φ, where Δ ⊆ S × S (the so–called step–operator). Formulae of the resulting extended logic, simply called L_{S}, is given by the following BNF:

φ ::= B | φ ∧ φ | □φ | X | Δ ↠ φ

where Δ ⊆ S × S. The interpretation of L_{S} extends that of L_{S}^{safe} (Definition 2) with the following implication:

s ⊧_{D,Σ} Δ ↠φ ⇒ whenever (s, s′) ∈ Δ then s′ ⊧_{D,Σ} φ

To see how Δ ↠ φ is used in quotienting consider a simple assertion of the form

s ⊧_{D,Σ_{1}∪Σ_{2}} □B  (4.1)

Now clearly (4.1) holds if s′ ∈ B whenever (s, s′) ∈ Σ_{1} and s′′ ∈ B whenever (s, s′′) ∈ Σ_{2}. More concisely, this becomes s ⊧_{D,Σ_{1}} □B and s ⊧_{D,Σ_{1}} Σ_{2} ↠ B. Thus the quotient formula □B/_{Σ_{2}} is precisely □B ∧ Σ_{2} ↠ B. Generally, the quotient–construction is given by the following definition:

Definition 3 (Quotienting) Let ϕ be an L_{S}-formula and let Σ ⊆ S ×S be a transition relation. Then the quotient formula (ϕ/_{Σ}) is defined inductively over ϕ as follows

φ ∧ ψ/_{Σ} = φ/_{Σ} ∧ ψ/_{Σ}
□φ/_{Σ} = □ φ/_{Σ} ∧ Σ↠φ/_{Σ}
Δ↠φ/_{Σ} = Δ↠φ/_{Σ}
B/_{Σ} = B
X/_{Σ} = X^{Σ}

Where X^{Σ} is a new identifier. For D a declaration over Id and Σ a transition relation, D^{Σ} is the declaration over Id^{Σ} = {X^{Σ} | X ∈ Id} given by D^{Σ} =

{X^{Σ} =^{Δ} φ/_{Σ} | X =^{Δ} φ ∈ D}. ◇

Theorem 1 (Correctness of Quotienting) Let Σ_{1} and Σ_{2} be transition relations, and let D be a declaration. Then

s ⊧_{D,Σ_{1}∪Σ_{2}} φ ⇔ s ⊧_{D^{Σ_{2}},Σ_{1}} φ/_{Σ_{2}}

Proof: See Appendix. ◇

5 Axiomatization

Having introduced the logic L_{S} the question of axiomatizing equivalence between and validity of formulae naturally arises. Besides providing fundamental theoretical insight these axiomatizations are crucial in simplifying quotient formulae and hence making the compositional approach to model checking feasible. By ⊧_{D,Σ} φ ≃ ψ we denote that φ and ψ are equivalent with respect to the declaration D and the transition relation Σ in the obvious sense, that is:

⊧_{D,Σ} φ ≃ ψ iff ∀s ∈ S.s ⊧_{D,Σ} φ ⇔ s ⊧_{D,Σ} ψ

By ⊧ φ ≃ ψ we denote that ⊧_{D,Σ} φ ≃ ψ holds for all D and Σ, and by we denote that ⊧_{Σ} φ ≃ ψ holds for all D. A formula φ is valid whenever ⊧ φ ≃ S and we denote this by ⊧ φ. A formula is unsatisfiable if ⊧ φ ≃ ∅ which we denote^{2} ⊧ ¬φ. Now — due to the single universal modality □ of L_{S} — it is not hard to see that validity (unsatisfiability) of formulae reduces to validity (unsatisfiability) with respect to the total (empty) transition relation, that is:

Lemma 1 Let φ be a formula of L_{S}. Then ⊧ φ if and only if ⊧_{S×S} φ ≃ S. Moreover ⊧ ¬φ if and only if ⊧_{∅} φ ≃ ∅. ◇

Note that for □-free formulae φ and ψ equivalence is independent of the interpreting transition relation. That is for any Σ:

⊧_{Σ} φ ≃ ψ if and only if ⊧ φ ≃ ψ

Let φ be a recursion-free formula. Then by replacing all occurrences of subformulae of the form □η with Σ ↠ η we obtain a Σ-equivalent formula φ^{Σ}, i.e. ⊧_{Σ} φ ≃ φ^{Σ}. It follows that:

⊧_{Σ} φ ≃ ψ if and only if ⊧ φ^{Σ} ≃ ψ^{Σ}

Applied to the special case of validity and unsatisfiability this yields:

Lemma 2 Let φ be a recursion-free formula of L_{S}. Then ⊧ φ if and only if ⊧ φ^{S×S} ≃ S. Moreover ⊧ ¬φ if and only if ⊧ φ^{∅} ≃ ∅ ◇

2The notation ¬φ does not imply that ¬φ is added to the logic as a construct

⊢ B_{1} ∧ B_{2} ≃ B_{1} ∩ B_{2}  (5.1)
⊢ ∅ ↠ φ ≃ S  (5.2)
⊢ ∅ ∧ φ ≃ ∅  (5.3)
⊢ S ∧ φ ≃ φ  (5.4)
⊢ □ φ ∧ □ ψ ≃ □ (φ ∧ ψ)  (5.5)
⊢ Δ ↠ φ ∧ ∇ ↠ φ ≃ (Δ ∪ ∇) ↠ φ  (5.6)
⊢ Δ ↠ ∇ ↠ φ ≃ Δ ∘ ∇ ↠ φ  (5.7)
⊢ Δ ↠ φ ∧ Δ ↠ ψ ≃ Δ ↠ (φ ∧ ψ)  (5.8)
⊢ Δ ↠ B ≃ Δ^{−1}(B)  (5.9)
⊢ B ∧ Δ ↠ φ ≃ B ∧ Δ ↠ (Δ(B) ∧ φ)  (5.10)
⊢ B ∧ Δ ↠ φ ≃ B ∧ Δ↓_{B}↠ φ  (5.11)
⊢ Δ ↠ φ ∧ ∇ ↠ ψ ≃ Δ\∇ ↠ φ ∧ ∇\Δ ↠ ψ ∧  (5.12)
Δ ∩ ∇ ↠ (φ ∧ ψ)

Table 1: Equivalence laws of L_{S}.

In Table 1 we state a number of laws for equivalence between formulae. To ease notation we introduce a couple of operators on sets of transitions.

Δ(B) = {s′ ∈ S | (s, s′) ∈ Δ ∧ s ∈ B}

Δ^{−1}(B) = {s ∈ S | (s, s′) ∈ Δ ⇒ s′ ∈ B}

Δ ∘ ∇ = {(s, s′′) ∈ S × S | ∃s′ ∈ S. (s, s′) ∈ Δ ∧ (s′, s′′) ∈ ∇}

Δ ↓_{B}= {(s, s′′) ∈ Δ | s ∈ B}

The laws are sound in the following sense:

Theorem 2 (Soundness) Whenever ⊢ φ ≃ ψ then ⊧ φ ≃ ψ ◇

The laws enable all recursion-free formulae to be transformed into the following strong normal-form:

Definition 4 A formula φ is in strong normal-form if φ is of the form:

φ ≡ B ∧ □φ′ ∧ ⋀_{i∈I} Δ_{i} ↠ φ_{i}

where φ′ and φ_{i} (i ∈ I) are themselves in strong normal-form and:

i) i ≠ j → Δ_{i} ∩ Δ_{j} = ∅  ii) Δ_{i} = Δ_{i} ↓_{B}
iii) B_{φ_{i}} = Δ_{i}(B)  iv) B = ⋂_{i∈I} Δ_{i}^{−1}(B_{φ_{i}})

where for a formula φ in strong normal-form B_{φ} refers to the conjunct B of φ. ◇

Theorem 3 For any recursion-free formula φ of L_{S} there exists a strong normal-form formula φ′ such that ⊢ φ ≃ φ′.

Proof: By using the laws (5.1) through (5.8) iteratively we can bring any formula φ into a formula φ′ of the required (syntactic) form. To meet the requirements i) through iv) we can apply the remaining laws (5.9) through (5.13). ◇ For recursion-free formulae the laws of Table 1 are complete with respect to validity and unsatisfiability as stated below:

Theorem 4 (Completeness) Let φ be a recursion-free formula. Then:

Whenever ⊧ φ then ⊢ φ^{S×S} ≃ S and whenever ⊧ ¬φ then ⊢ φ^{∅} ≃ ∅

◇

It still is an open question as to whether the laws of Table 1 are complete w.r.t. to general formula equivalence — though we conjecture this to be the case.

6 Example

Let us now apply the compositional quotient technique to the program described in Example 1 and the property given in Example 2. For simplicity we consider the following simplified version of the program of Example 1:

\{ \begin{matrix}P_{1} =^{Δ} \\ while true do \\ if x ≥ MAX then x := x + 1 \end{matrix} \} | \{ \begin{matrix}P_{2} =^{Δ} \\ while true do \\ if x > 0 then x := x − 1 \end{matrix} \}

In this simplified version both P_{1} and P_{2} have a single control location. The state-space therefore degenerates to ℕ (i.e. the value of the shared variable x). The transition relation given by the components P_{1} and P_{2} are now:

\begin{matrix}Σ_{1} = \{(n, n + 1) | n ∈ ℕ\} \\ Σ_{2} = \{(n + 1, n) | n ∈ ℕ\} \end{matrix}

The property of divergence of P_{2} can be expressed simply as: the value of x is invariantly different from 0, i.e:

X =^{Δ} {0}^{∁} ∧ □X

Now, we claim that for no state (i.e. no k ∈ ℕ) the above program P_{1} | P_{2} will have this property. That is:

Claim 1 For any k ∈ ℕ:  k |̸=_{Σ_{1}∪Σ_{2}} X  ◇

In fact – which should be intuitively clear – component P_{2} is entirely to blame for this; no matter what component P_{1} does the composite program P_{1} | P_{2} will always fail having the property X for all states. That is:

Claim 2 For any Σ ⊆ ℕ × ℕ and any k ∈ ℕ:  k |̸=_{Σ} X/Σ_{2}  ◇

Note that Claim 1 follows from Claim 2 by taking Σ = Σ_{1} and applying the quotient theorem (Theorem 1). To justify Claim 2 for a particular k ∈ ℕ we actually only need a certain initial part of Σ_{2} (Σ_{2}^{≤k}). For k ∈ ℕ define:

\begin{matrix}Σ_{2}^{≤k} = \{(n + 1, n) | n < k\} \\ Σ_{2}^{>k} = Σ_{2}\Σ^{≤k} \end{matrix}

Now Claim 2 follows from the following theorem by instantiating it to Σ ∪ Σ_{2}^{>k} and using the fact that φ/Σ_{1}/Σ_{2} ≃ φ/(Σ_{1} ∪ Σ_{2}).

Theorem 5 For any Σ ⊆ ℕ × ℕ and for any k ∈ ℕ: k |̸=_{Σ} X/Σ_{2}^{≤k}

Proof: Let Y^{≤k} be defined by the following equation:

Y^{≤k} =^{Δ} {0 … k}^{∁} ∧ □Y^{≤k}

We prove by induction on k that X/Σ_{2}^{≤k} ≃ Y^{≤k}.

Basis k = 0: Trivial, as Σ_{2}^{≤0} = ∅. It is then easy to see that X/∅ ≃ X and as the equation for Y^{≤0} is exactly that of X, it follows that X/Σ_{2}^{≤0} ≃_{Σ} Y^{≤0}.

Step: By definition Σ_{2}^{≤k+1} = Σ_{2}^{≤k} ∪ {(k + 1, k)}. Again, by using the fact that φ/Σ_{1}/Σ_{2} ≃ φ/(Σ_{1} ∪ Σ_{2}) and by induction hypothesis we have:

X/Σ_{2}^{≤k+1} ≃ (X/Σ_{2}^{≤k})/{(k + 1, k)} ≃^{IH} Y^{≤k}/{(k + 1, k)}

Now expanding the definition of Y^{≤k} yields:

Y^{≤k}/{(k + 1, k)} =^{Δ} {0 … k}^{∁} ∧ □(Y^{≤k}/{(k + 1, k)})∧
{(k + 1, k)} ↠ (Y^{≤k}/{(k + 1, k)})
≃ {0 … k}^{∁} ∧ □(Y^{≤k}/{(k + 1, k)})∧

{(k + 1, k)} ↠ ({0 … k}^{∁} ∧ (Y^{≤k}/{(k + 1, k)}))

Now, by using the laws of Table 1 we can simplify Y^{≤k}/{(k + 1, k)} in the following manner^{3}:

{0 … k}^{∁} ∧ □Z ∧ {(k + 1, k)} ↠ ({0 … k}^{∁} ∧ Z)
≃  by (5.8)

{0 … k}^{∁} ∧ □Z ∧ {(k + 1, k)} ↠ {0 … k}^{∁} ∧ {(k + 1, k)} ↠ Z

≃  by (5.9)
{0 … k}^{∁} ∧ □Z ∧ {0 … k + 1}^{∁} ∧ {(k + 1, k)} ↠ Z
≃  by (5.11)
{0 … k + 1}^{∁} ∧ □Z ∧ {} ↠ Z
≃  by (5.2)
{0 … k + 1}^{∁} ∧ □Z

That is, Y^{≤k}/{(k + 1, k)} – and hence X/Σ_{2}^{≤k+1} – satisfies precisely the defining equation for Y^{≤k+1}. ◇

3For better readability we substitute Z for Y^{≤k}/{(k + 1, k)}

7 Concluding Remarks

We have presented a generalisation of the promising compositional model– checking technique presented in [And95] and extended in [LPY95a, LL95, LPY95b] to programs modelled as arbitrary (possibly infinite–state) transition systems. Both our quotient construction and laws of equivalence between formulae may be applied to the more specialized settings of [And95, LPY95a, LL95, LPY95b] but also to other settings such as shared variable models as demonstrated in the Example of the paper and studied in [ASM96]. In fact, we believe that the framework offered by our paper may serve as a guideline when instantiating the compositional model–checking technique to a variety of settings. In a practical implementation care must of course be taken in choosing a suitable and compact representation of the sets of states and the relation on states occurring in formulae. In addition the representation should lead to efficiency in manipulation using the laws of Table 1. For finite state programs BDD’s are obvious candidates [ASM96] and for networks of timed automata a variety of techniques for representing subsets of the Euclidean space exists.

Appendix

Theorem 6 (Correctness of Quotienting) Let Σ_{1} and Σ_{2} be transition relations, and let D be a declaration. Then

s ⊧_{D,Σ_{1}∪Σ_{2}} φ ⇔ s ⊧_{D^{Σ_{2}},Σ_{1}} φ/_{Σ_{2}}
◇

Proof (⇐):: Let S = {(s, φ) | s ⊧ φ/_{Σ_{2}}}. We prove S^{+} = S ∪ ⊧_{D,Σ_{1}∪Σ_{2}} is a satisfiability relation under D, Σ_{1}∪Σ_{2} according to the extended Definition 2. Case φ = □ψ: Assume (s, □ψ) ∈ S^{+}. We must prove:

(s, s′) ∈ Σ_{1} ∪ Σ_{2} ⇒ (s′, ψ) ∈ S^{+}

If (s, □ψ) ∈⊧_{D,Σ_{1}∪Σ_{2}} this holds trivially. Hence assume (s, □ψ) ∈ S and (s, s′) ∈ Σ_{1} ∪ Σ_{2}:

By definition of S we have s ⊧_{D,Σ_{1}} □(ψ/_{Σ_{2}}) ∧ Σ_{2} ↠ψ/_{Σ_{2}}. We now have two cases: (s, s′) ∈ Σ_{1} and (s, s′) ∈ Σ_{2}.

• If (s, s′) ∈ Σ_{1} then s ⊧_{D,Σ_{1}} □(ψ/_{Σ_{2}}) implies s′ ⊧_{D^{+},Σ_{1}} ψ/_{Σ_{2}}. By definition of S we then have (s′, ψ) ∈ S^{+}.

• If (s, s′) ∈ Σ_{2} then s ⊧_{D,Σ_{1}} Σ_{2} ↠ ψ/_{Σ_{2}} implies s′ ⊧_{D^{+},Σ_{1}} ψ/_{Σ_{2}}. By definition of S we then have (s′, ψ) ∈ S^{+}.

Thus, we have established: (s′, ψ) ∈ S^{+} (⇒):: Let S = {(s, φ/_{Σ_{2}}) | s ⊧_{D,Σ_{1}∪Σ_{2}} φ}. We prove S^{+} = S ∪ ⊧_{D,Σ_{1}} is a satisfiability relation under D^{+}, Σ_{1} according to the extended Definition 2. Case φ = □ψ: Assume (s, □ψ/_{Σ_{2}}) ∈ S^{+}. By definition of φ/_{Σ} we have □φ/_{Σ_{2}} = □(ψ/_{Σ_{2}}) ∧ Σ_{2} ↠φ/_{Σ_{2}}. We must then prove:

• (s, s′) ∈ Σ_{1} ⇒ (s′, ψ/_{Σ_{2}}) ∈ S^{+}

• (s, s′′) ∈ Σ_{2} ⇒ (s′′, ψ/_{Σ_{2}}) ∈ S^{+}

If (s, □(ψ/_{Σ_{2}}) ∧ Σ_{2} ↠ ψ/_{Σ_{2}}) ∈⊧_{D^{+},Σ_{1}} this holds trivially. Hence assume (s, □ψ) ∈ S, (s, s′) ∈ Σ_{1} and (s, s′′) ∈ Σ_{2}:

By definition of S we have s ⊧_{D^{+},Σ_{1}} □(ψ/_{Σ_{2}}) ∧ Σ_{2} ↠ ψ/_{Σ_{2}}. We now have two cases: (s, s′) ∈ Σ_{1} and (s, s′) ∈ Σ_{2}.

• If (s, s′) ∈ Σ_{1} then s ⊧_{D,Σ_{1}} □(ψ/_{Σ_{2}}) implies s′ ⊧_{D^{+},Σ_{1}} ψ/_{Σ_{2}}. By definition of S we then have (s′, ψ) ∈ S^{+}.

• If (s, s′′) ∈ Σ_{2} then s ⊧_{D,Σ_{1}} Σ_{2} ↠ ψ/_{Σ_{2}} implies s′′ ⊧_{D^{+},Σ_{1}} ψ/_{Σ_{2}}. By definition of S we then have (s′′, ψ) ∈ S^{+}.

Thus, we have established both (s′, ψ) ∈ S^{+} and (s′′, ψ) ∈ S^{+}. ◇

References

[AD90] R. Alur and D.L. Dill. Automata for modeling real-time systems. In M. Paterson, editor, Proceedings 17^{th} ICALP, Warwick, volume 443 of Lecture Notes in Computer Science, pages 322–335. Springer-Verlag, July 1990.

[AD92] R. Alur and D.L. Dill. The theory of timed automata. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings REX Workshop on Real-Time: Theory in Practice, Mook, The Netherlands, June 1991, volume 600 of Lecture Notes in Computer Science, pages 45–73. Springer-Verlag, 1992.

[And95] H.R. Andersen. Partiel model checking. In Proceedings of Logics in Computer Science, LICS’95, 95.

[ASM96] Henrik Reif Andersen, Jørgen Staunstrup, and Niels Maretti. Partial model checking with robdds. In To appear in Proceedings of TACAS’97, 1996.

[BCM^{+}90] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking 10^{20} states and beyond. In Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA, pages 428–439. IEEE Computer Society Press, 1990.

[CFJ93] E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetry in Temporal Logic Model Checking. 697, 1993. In Proc. of CAV’93.

[CGL92] E. M. Clarke, O. Grümberg, and D. E. Long. Model Checking and Abstraction. Principles of Programming Languages, 1992.

[GW91] P. Godefroid and P. Wolper. A partial approach to model checking. In Proceedings 6^{th} Annual Symposium on Logic in Computer Science, Amsterdam, pages 406–416. IEEE Computer Society Press, 1991.

[KLL^{+}97a] K. Kristoffersen, F. Laroussinie, K.G. Larsen, P. Petterson, and Wang Yi. A compositional proof of a real-time mutual exclusion protocol. In Proceedings of TAPSOFT97, 1997.

[KLL^{+}97b] K. Kristoffersen, F. Laroussinie, K.G. Larsen, P. Petterson, and Wang Yi. A compositional proof of a real-time mutual exclusion protocol. In Proceedings of TAPSOFT97, 1997.

[Koz82] D. Kozen. Results on the propositional mu–calculus. Lecture Notes in Computer Science, 140, 1982. in Proc. of International Colloquium on Algorithms, Languages and Programming 1982.

[LL95] F. Laroussinie and K.G. Larsen. Compositional Model Checking of Real Time Systems. In Proc. of CONCUR ’95, Lecture Notes in Computer Science. Springer–Verlag, 1995.

[LLW95] François Laroussinie, Kim G. Larsen, and Carsten Weise. From timed automata to logic - and back. Lecture Notes in Computer Science, 969:pages 529–539, 1995. In Proceedings of MFCS95.

[LPY95a] Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 76–87, December 1995.

[LPY95b] Kim G. Larsen, Paul Pettersson, and Wang Yi. Model-Checking for Real-Time Systems. In Proc. of Fundamentals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 62–88, 1995.

[Mil89] R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.

[Tar55] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.

[Val90] A. Valmari. A stubborn attack on state explosion. Theoretical Computer Science, 3, 1990.

Recent BRICS Report Series Publications

RS-97-13 Jørgen H. Andersen and Kim G. Larsen. Compositional Safety Logics. June 1997. 16 pp.

RS-97-12 Andrej Brodnik, Peter Bro Miltersen, and J. Ian Munro. Trans-Dichotomous Algorithms without Multiplication — some Upper and Lower Bounds. May 1997. 19 pp. Appears in Dehne, Rau-Chaulin, Sack and Tamassio, editors, Algorithms and Data Structures: 5th International Workshop, WADS ’97 Proceedings, LNCS 1272, 1997, pages 426–439.

RS-97-11 Kārlis Čerāns, Jens Chr. Godskesen, and Kim G. Larsen. Timed Modal Specification — Theory and Tools. April 1997. 32 pp.

RS-97-10 Thomas Troels Hildebrandt and Vladimiro Sassone. Transition Systems with Independence and Multi-Arcs. April 1997. 20 pp. Appears in Peled, Pratt and Holzmann, editors, DIMACS Workshop on Partial Order Methods in Verification, POMIV ’96, pages 273–288.

RS-97-9 Jesper G. Henriksen and P. S. Thiagarajan. A Product Version of Dynamic Linear Time Temporal Logic. April 1997. 18 pp. Appears in Mazurkiewicz and Winkowski, editors, Concurrency Theory: 8th International Conference, CONCUR ’97 Proceedings, LNCS 1243, 1997, pages 45–58.

RS-97-8 Jesper G. Henriksen and P. S. Thiagarajan. Dynamic Linear Time Temporal Logic. April 1997. 33 pp.

RS-97-7 John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus (Extended Version). March 1997. 55 pp. Extended version of article to appear in the Journal of Functional Programming.

RS-97-6 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. March 1997. 53 pp. Extended version of an article to appear in the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’97), Amsterdam, The Netherlands, June 1997.