BRICS RS-95-53 Klarlund et al.: Automated Logical Veri�cation based on Trace Abstractions

BRICS

Basic Research in Computer Science

Automated Logical Veri�cation based on Trace Abstractions

Nils Klarlund Mogens Nielsen Kim Sunesen

BRICS Report Series RS-95-53 ISSN 0909-0878 November 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, 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 publications in the BRICS Report Series. 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@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Automated logical verification based on trace abstractions

Nils Klarlund Mogens Nielsen Kim Sunesen BRICS^{∗} Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C. {klarlund,mnielsen,ksunesen}@daimi.aau.dk

Abstract

We propose a new and practical framework for integrating the behavioral reasoning about distributed systems with model-checking methods.

Our proof methods are based on trace abstractions, which relate the behaviors of the program and the specification. We show that for finitestate systems such symbolic abstractions can be specified conveniently in Monadic Second-Order Logic (M2L). Model-checking is then made possible by the reduction of non-determinism implied by the trace abstraction.

Our method has been applied to a recent verification problem by Broy and Lamport. We have transcribed their behavioral description of a distributed program into temporal logic and verified it against another distributed system without constructing the global program state space. The reasoning is expressed entirely within M2L and is carried out by a decision procedure. Thus M2L is a practical vehicle for handling complex temporal logic specifications, where formulas decided by a push of a button are as long as 10-15 pages.

1 Introduction

This paper is concerned with the specification and verification of distributed systems. Often, the relationship between a program and a specification is expressed in terms of a state-based refinement mapping, see [18] for a survey. Thus, when systems are specified by behavioral or temporal constraints, it is necessary first to find state-representations. In this process, important information may be lost or misconstrued.

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

In this paper, we exhibit a logic of traces (i.e. finite computation sequences) that allows compositional reasoning directly about behaviors. We formulate trace abstractions and their proof rules as an alternative to the use of refinement mappings for the verification of distributed systems.

Our main goal is to show that our method is useful in practice for complicated examples. Thus, use of our logic and proof rules must be supported by a decision procedure that will give answers to logical questions about the systems, such as “Does trace abstraction R show that program P implements S?”

To this end, we formulate a sound and complete verification method based on trace abstractions. We show that our method for finite-state systems can be formulated in a very succinct formalism: the Monadic Second-order Logic (M2L).

We address the important problem of relating a distributed program to a non-deterministic specification that also is a distributed system. Non-determinism arises when systems have alphabets that are partioned into observable and internal actions. Abstracting away internal actions generally introduces nondeterminism.

Our contribution is to show an alternative to usual techniques, which tend to involve rather involved concepts such as prophecy variables or mappings to sets of sets of states. These can be replaced by behavioral predicates that need only to partially link the program and the specification. The remaining information is then calculated automata-theoretically by means of the subset construction.

We formulate a compositional rule to avoid the explicit construction of the global program space.

Using the Mona implementation of M2L, we have verified a recent verification problem by Broy and Lamport by transcribing several pages of informally stated temporal properties. The formulas resulting are decided in minutes despite their size (10^{5} characters). A detailed treatement of this problem can be found in [11].

1.1 Relations to previous work

The systems we define are closely related to those described by Hoare in [9], where an alphabet Σ and a set of traces over Σ is associated with every process. We use a composition operator, similar to Hoare’s parallel operator (∥ [9]) forcing systems to synchronize on events or actions shared by both alphabets.

We do not know of any earlier work using relations directly on traces. In fact, the use of state mappings—one of the most advocated methods for proving refinement, see e.g. [17, 15, 16, 10] and for a survey [18]—were introduced as a way to avoid behavioral reasoning, often regarded as being too complex. The theory of state mappings is by now well-understood, but not simple, with the completeness results in [1, 12, 20]. In the finite state case, an important difference between the state mapping approach and ours is that in the traditional approaches, the mapping is to be exactly specified state by state whereas in our approach the relation between behaviors may be specified partially leaving the rest to our verification tool. In [2], Lamport and Abadi gave a proof rule for proving correctness of implementation of compound systems based on an assumption/guarantee method. A closed compound system is split into a number of open systems by factoring out dependencies as assumptions. Our rule is very different in that dependencies are reflected in a requirement about the relationship between trace abstractions for components.

The TLA formalism by Lamport [16] and the temporal logic of Manna and Pnueli [10] offer unified frameworks for specifying systems and state mappings, and for proving the correctness of implementation. Both logics are undecidable, but work has been done on establishing mechanical support, see [6, 7].

Clarke, Browne, and Kurshan [4] have applied model checking techniques to the language containement problem (L(M_{1}) ⊆ L(M_{2})), where M_{1} and M_{2} are ωautomata. They reduce the containment problem to a model-checking problem by forming a product of the automata and checking whether the product is a model for a certain CT L^{∗} formula. The method is applicable to any common kind of ω-automata. Thus it deals with liveness properties unlike our method, which only deals with logic over finite prefixes. However, the method in [4] suffers from the restriction that M_{2} be deterministic.

Kurshan, see [13], has devised an automata-theoretic framework for modeling and verifying synchronous transition systems. His use of homomorphisms allow complex properties to be reduced to ones that can be verified by means of model-checking.

Kurshan’s methods were extended in [14] to the asynchronous input/output automata of [17]. There, Kurshan et al. give an account of interleaving composition in terms of conventional, synchronous automata. Our treatment of concurrency is similar in its use of stuttering for modeling asynchrony except that we do not consider fairness (which is a property of infinite sequences). A principal difference is that our proposal is based on comparing sequences of events, whereas the method of [14] is essentially state-based or event-based.

Binary Decision Diagrams (BDDs) are usually used in verification to compactify representations of state-spaces, see e.g. [5]. The Mona implementation [8] of a decision procedure for M2L uses BDDs to handle large alphabets.

1.2 Overview

In Section 2, we discuss our formal framework, which is based on an interleaving semantics of processes that work in a global space of events. M2L is explained in Section 3. We show in Section 4 that with some additional concepts, it is possible to formulate the verification method of Section 2 in M2L. In Section 5, we explain the role of trace abstractions in our solution of the Broy and Lamport verification problem.

2 Traces and abstractions

We regard systems in a fairly standard way: they are devices that produce sequences of events that are either observable or internal. Systems exist in a universe. They can be composed and compared. Trace abstractions relate a program to a specification. These abstractions form a sound and complete verification method, and a simple decomposition rule is easy to formulate.

2.1 Systems, universes and normalization

A system A determines an alphabet Σ_{A} of events, which is partioned into observable events Σ_{A}^{Obs} and internal events Σ_{A}^{Int}. A behavior of A is a finite sequence over Σ_{A}. The system A also determines a prefix-closed language L_{A} of behaviors called traces of A. We write A = (L_{A}, Σ_{A}^{Obs}, Σ_{A}^{Int}). The projection π from a set Σ^{∗} to a set Σ′^{∗} (Σ′ ⊆ Σ) is the unique string homomorphism from Σ^{∗} to Σ′^{∗} given by π(a) = a, if a is in Σ′, and π(a) = ϵ otherwise, where ϵ is the empty string. The observable behaviors of a system A, Obs(A), are the projections on Σ_{A}^{Obs} of the traces of A, that is Obs(A) = {π(α) | α ∈ L_{A}}, where π is the projection from Σ_{A}^{∗} onto (Σ_{A}^{Obs})^{∗}.

A system A is thought of as existing in a universe which contains the systems with which it is composed and compared. The events possible in this universe constitute a global alphabet U, which contains Σ_{A} and all other alphabets of interest. Moreover, U is assumed to contain the distinguished event τ, which is not in the alphabet of any system. The set N_{Σ}(A) of normalized traces over an alphabet Σ ⊇ Σ_{A} is the set h^{−1}(L_{A}), where h is the projection from Σ^{∗} onto Σ_{A}^{∗}. Normalization plays an essential rôle when composing systems and when proving correctness of implementation of systems with internal events.

2.2 Composition

We say that systems A and B are composable if they do not disagree on the partition of events, that is, if no internal event of A is an observable event of B and vice versa, or symbolically, if Σ_{A}^{Int} ∩ Σ_{B}^{Obs} = ∅ and Σ_{B}^{Int} ∩ Σ_{A}^{Obs} = ∅. Given composable systems A and B, we define their composition A ∥ B = (L_{A∥B}, Σ_{A∥B}^{Obs}, Σ_{A∥B}^{Int}), where

• the set of observable events is the union of the sets of observable events of the components, that is, Σ_{A∥B}^{Obs} = Σ_{A}^{Obs} ∪ Σ_{B}^{Obs},

• the set of internal events is the union of the sets of internal events of the components, that is, Σ_{A∥B}^{Int} = Σ_{A}^{Int} ∪ Σ_{B}^{Int}, and

• the set of traces is the intersection of the sets of normalized traces with respect to the alphabet Σ_{A∥B}, i.e. L_{A∥B} = N_{Σ_{A∥B}} (A) ∩ N_{Σ_{A∥B}} (B).

(Note that the restriction above for composability ensures that A ∥ B has also disjoint observable and internal events.)

A trace of A ∥ B is the interleaving of a trace of A with a trace of B in which common events are synchronized. The projection of a trace of A ∥ B onto the alphabet of any of the components is a trace of the component. Composition is commutative, idempotent, and associative, and extends straightforwardly to any number n of composable systems A_{i}. We write A_{1} ∥ … ∥ A_{n} or just ∥A_{i}.

Example 2.1 To make the concepts clearer, we show how to present the wellknown scheduler [19] of Milner in terms of our systems. The distributed scheduler is based on passing a token consecutively between a number of computing agents. We consider a three-agent version of the scheduler. The ith agent S_{i} performs observable events a_{i} and b_{i} to indicate the begining and the end of computing, respectively, and it synchronizes with its neighbor agents by interacting on the internal events c_{i} and c_{i⊖1}, where i is 0, 1, or 2, and ⊖ is subtraction modulo 3.

For a regular expression r, we denote by L^{P re}(r) the regular language obtained by taking the prefix-closure of the language associated with r. Thus the agents may be described by:

S_{0} = (L^{P re}((a_{0}c_{0}(b_{0}c_{2} + c_{2}b_{0}))^{∗}), {a_{0}, b_{0}}, {c_{0}, c_{2}}),
S_{1} = (L^{P re}(c_{0}(a_{1}c_{1}(b_{1}c_{0} + c_{0}b_{1}))^{∗}), {a_{1}, b_{1}}, {c_{0}, c_{1}}),
S_{2} = (L^{P re}(c_{1}(a_{2}c_{2}(b_{2}c_{1} + c_{1}b_{2}))^{∗}), {a_{2}, b_{2}}, {c_{1}, c_{2}})

The scheduler is defined in terms of the compound system:

S = S_{0} ∥ S_{1} ∥ S_{2}

where the set of observable events then consists of the a_{i}’s and b_{i}’s.

2.3 Implementation

We say that systems A and B are comparable if they have the same set of observable events Σ^{Obs}, that is, Σ^{Obs} = Σ_{A}^{Obs} = Σ_{B}^{Obs}. In the following, A and B denote comparable systems and π denotes the projection from U^{∗} onto (Σ^{Obs})^{∗}.

Definition 2.1 A implements B if and only if Obs(A) ⊆ Obs(B)

Example 2.2 Another way of defining a scheduler is to use a central agent C. The ith agent still performs observable events a_{i} and b_{i} but now synchronizes with the agent C by interacting on the internal event d_{i}. The agents are given by the systems

\begin{aligned}C & = & (L^{P re}((d_{0}d_{0}d_{1}d_{1}d_{2}d_{2})^{∗}), ∅, \{d_{0}, d_{1}, d_{2}\}), \\ P_{i} & = & (L^{P re}((d_{i}a_{i}d_{i}b_{i})^{∗}), \{a_{i}, b_{i}\}, \{d_{i}\}), i = 0, 1, 2 \end{aligned}

and the scheduler is defined by the compound system:

P = P_{0} ∥ P_{1} ∥ P_{2} ∥ C

where the observable events are the a_{i}’s and b_{i}’s and internal events are the d_{i}’s.

The systems S and P may be seen as existing in the universe U = {a_{i}, b_{i}, c_{i}, d_{i}, τ | i = 0, 1, 2} and are clearly comparable. The reader may convince himself that P implements S, but in general this not an easy task.

2.4 Relational trace abstractions

A trace abstraction is a relation on traces preserving observable behaviors.

Definition 2.2 A trace abstraction R from A to B is a relation on U^{∗} × U^{∗} such that

1. If αRβ then π(α) = π(β)

2. N_{U}(A) ⊆ dom R

3. rng R ⊆ N_{U}(B)

The first condition states that any pair of related traces must agree on observable events. The second and third condition require that any normalized trace of A should be related to some normalized trace of B, and only to normalized traces of B. The use of trace abstractions forms a sound and complete method in the sense that there exists a trace abstraction from A to B if and only if A implements B.

Theorem 2.1 There exists a trace abstraction from A to B if and only if A implements B.

We would like to prove that a compound system ∥A_{i} implements another compound system ∥B_{i} by exhibiting trace abstractions R_{i} from A_{i} to B_{i}. A simple extra condition is neeeded for this to work:

Theorem 2.2 Let A_{i} and B_{i} be pairwise comparable systems forming the compound systems ∥A_{i} and ∥B_{i}. If

R_{i} is a trace abstraction from A_{i} to B_{i}  (1)
⋂_{i} dom R_{i} ⊆ dom ⋂_{i} R_{i}  (2)

then

∥A_{i} implements ∥B_{i}

Intuitively, the extra condition 2., which we call the compatibility requirement, ensures that the choices defined by the trace abstractions can be made to agree on internal events.

Due to the possibility of non-trivial interference on internal events among the component systems, the first premise alone of the composition rule is not sufficient to ensure the conclusion. Consider e.g. the following systems

\begin{matrix}A_{1} = (\{a\}^{∗}, \{a\}, ∅), & B_{1} = (\{ac\}^{∗}\{ϵ, a\}, \{a\}, \{c\}) \\ A_{2} = (\{b\}^{∗}, \{b\}, ∅), & B_{2} = (\{bc\}^{∗}\{ϵ, b\}, \{b\}, \{c\}) \end{matrix}

where ϵ is the empty string. Obs(A_{i}) ⊆ Obs(B_{i}), but Obs(A_{1} ∥ A_{2}) ⊈ Obs(B_{1} ∥ B_{2}), since aa ∈ Obs(A_{1} ∥ A_{2}), but aa ∉ Obs(B_{1} ∥ B_{2}).

The next example illustrates that even when significant internal interaction exists among the components, the decomposition theorem may be applied.

Example 2.3 Consider the schedulers from before. For each i = 0, 1, 2 let χ_{i} be the string homomorphism from U^{∗} to U^{∗} inductively defined by χ_{i}(ϵ) = ϵ, and for α ∈ U^{∗} and u ∈ U,

χ_{i}(αu) = \{ \begin{matrix}χ_{i}(α)c_{i} & if u = d_{i} & \\ & the number of d_{i}s in α is odd \\ χ_{i}(α) & if u = c_{i} \\ χ_{i}(α)u & otherwise \end{matrix}

where ϵ is the empty string. χ_{i} maps every string α into a string identical to α except for every occurrence of c_{i} being erased and every even occurrence of d_{i} being replaced by c_{i}. Let χ = χ_{0} ∘ χ_{1} ∘ χ_{2}. We use χ to relate the internal behaviors of P and S. It is not hard to check that the relations R_{i} = {(α, χ(α)) | χ(α) ∈ N_{U}(S_{i})} are trace abstractions from P_{i} ∥ C to S_{i}, respectively. (Requirements 1. and 3. are satisfied by definition. To see that 2. holds, we consider some α ∈ N_{U}(P_{i} ∥ C) and argue that χ(α) ∈ N_{U}(S_{i}).) Also, it is not hard to see that ⋂_{i} dom R_{i} ⊆ dom ⋂_{i} R_{i}. (For each α there is exactly one χ(α).) Hence by Theorem 2.2, it follows that (P_{0} ∥ C) ∥ (P_{1} ∥ C) ∥ (P_{2} ∥ C) implements S and therefore that P implements S.

An almost trivial observation is:

Corollary 2.1 If additionally the components of the specification are noninterfering on internal events, that is, Σ_{B_{i}}^{Int} ∩ Σ_{B_{j}}^{Int} = ∅, for every i ≠ j, then A_{i} implements B_{i} implies ∥A_{i} implements ∥B_{i}.

3 Monadic second-order logic on strings

The logical language we use is the monadic second-order logic (M2L) on strings, where a closed formula is interpreted relative to a natural number n (the length). First-order variables p, q, … range over the set {0, …, n − 1} (the set of positions), and second-order variables P, Q, …, P_{1}, P_{2}, … range over subsets of {0, …, n − 1}. Atomic formulas are of the form p = q, p = q + 1, p < q and q ∈ P. Formulas are constructed in the standard way from atomic formulas by means of the Boolean connectives ¬, ∧, ∨, ⇒ and ⇔, and first and second-order quantifiers ∀ and ∃. We adopt the standard notation of writing ϕ(P_{1}, …, P_{k}, p_{1}, …, p_{l}) to denote an open formula ϕ whose free variables are among P_{1}, …, P_{k}, p_{1}, …, p_{l}. Let 0 and $ be the M2L definable constants denoting the positions 0 and n − 1, respectively. The expressive power of M2L is illustrated by the formula

∃P.0 ∈ P ∧ (∀p.p < $ ⇒ (p ∈ P ⇔ p + 1 ∉ P))

which defines the set of even numbers. A second-order variable P can be seen as denoting a string of bits b_{0} … b_{n−1} such that b_{i} = 1 if and only if i ∈ P. This leads to a natural way of associating a language L(ϕ) over Σ = IB^{m} of satisfying interpretations to an open formula ϕ(P_{1}, …, P_{m}) having only second-order variables occurring free (IB denotes the set {0, 1}). As an example, consider the formula ϕ ≡ ∀p.p ∈ P_{1} ⇔ p ∉ P_{2}. Then L(ϕ) is a language over the alphabet Σ = IB^{2}, where each (b_{1}, b_{2}) ∈ IB^{2} denotes the membership status of the current position relative to P_{1} and P_{2}. For example, writing the tuples as columns, we have

_{P_{2}: 00101}^{P_{1}: 11010} ∈ L(ϕ) and _{P_{2}: 01000}^{P_{1}: 11010} ∉ L(ϕ)

Any language defined by a M2L formula is regular and conversely any regular language can be defined by a M2L formula. Given a formula ϕ, a minimal finite automaton accepting L(ϕ) can effectively be constructed using the standard operations of complementation, product, subset construction, and projection. In particular, the existential quantifier becomes associated with a subset construction—and a potential exponential blow-up in the number of states. The construction of automata constitutes a decision procedure for M2L, since ϕ is a tautology if and only if L(ϕ) is the set of all strings. In case ϕ is not a tautology, a witness in terms of a minimal interpretation falsifying ϕ can be derived from the minimum deterministic automaton recognizing L(ϕ). We use the tool Mona [8], which implements the decision procedure and the counter-example facility.

4 The finite state case

We now restrict attention to systems with regular trace languages. We show for a large class of finite-state systems that trace abstractions definable by regular languages constitute a complete method for proving the implementation property.

Given strings α = α_{0} … α_{n} ∈ Σ_{1}^{∗} and β = β_{0} … β_{n} ∈ Σ_{2}^{∗}, we write α^{∧}β for the string (α_{0}, β_{0}) … (α_{n}, β_{n}) ∈ (Σ_{1} × Σ_{2})^{∗}. Every language L_{R} over a product alphabet Σ_{1} × Σ_{2} has a canonical embedding as a relation R_{L} ⊆ Σ_{1}^{∗} × Σ_{2}^{∗} on strings of equal length given by α^{∧}β ∈ L_{R} ⇔^{def}αR_{L}β. Hence in the following we shall use the two representations interchangeably. Accordingly, we say that a trace abstraction is regular if it is the embedding of a regular language over U × U.

Not all trace abstractions between finite-state systems are regular, since there may be an unbounded number of internal events between pairs of corresponding observable events. The next definition is an essential step towards the identification of regular trace abstractions.

Definition 4.1 Given a subset Σ′ of Σ we say that strings α, β ∈ Σ^{∗} are Σ′– synchronized if they are of equal length and if whenever the ith position in α contains a letter in Σ′ then the ith position in β contains the same letter, and vice versa.

Definition 4.2 Let R̂ be the language over U × U given by α^{∧}β ∈ R̂ if and only if

β ∈ N_{U}(B) and α, β are Σ^{Obs}-synchronized

Since N_{U}(B) is a regular language (by assumption of this Section), so is R̂. The next proposition gives a sufficient condition for R̂ and any regular subset of R̂ to be a trace abstraction. We return to the significance of the last part when dealing with automated proofs.

Proposition 4.1 If N_{U}(A) ⊆ dom R̂ then R̂ is a regular trace abstraction from A to B. Moreover, in general for any regular language C ⊆ (U × U)^{∗}, if N_{U}(A) ⊆ dom R̂ ∩ C, then R̂ ∩ C is a regular trace abstraction from A to B.

It is not hard to see that if R̂ is a regular trace abstraction, then it is the largest such relating Σ^{Obs}-synchronized traces. In this case we denote R̂ the canonical trace abstraction.

Non-regularity of trace abstractions occurs if for example there are arbitrarily many non-observable events between any two observable events. However, it may also happen that a behavior of the program may have too few internal events between two observable events in the sense that any behavior of the specification with the same observable behavior may require more internal events. We next give a precise definition of this phenomenon. Let π_{A} and π_{B} be the projections from Σ_{A}^{∗} and Σ_{B}^{∗}, respectively, onto (Σ^{Obs})^{∗}.

Definition 4.3 A trace α ∈ L_{A} is internally finer than a trace β ∈ L_{B} if π_{A}(α) = π_{B}(β), and for all e, e′ ∈ Σ^{Obs}, u ∈ (Σ_{A}^{Int})^{∗}, v ∈ (Σ_{B}^{Int})^{∗}, α_{1}, α_{2} ∈ Σ_{A}^{∗} and β_{1}, β_{2} ∈ Σ_{B}^{∗}, such that π_{A}(α_{1}) = π_{B}(β_{1})

\begin{matrix}& α = α_{1}eue′α_{2} & ∧ & β = β_{1}eve′β_{2} \\ ∨ \\ & α = ue′α_{2} & ∧ & β = ve′β_{2} \end{matrix} \} ⇒ |u| ≥ |v|

A system A is internally finer than a system B if for any trace α of A such that π_{A}(α) ∈ Obs(B), there exists a trace β of B such that α is internally finer than β.

Consider the scheduler example. System P is internally finer than S, whereas the converse is not true. We restate the soundness and completeness result from the general case for a constrained class of systems and regular trace abstractions.

Theorem 4.1 Assume that A is internally finer than B. There exists a canonical trace abstraction from A to B if and only if A implements B.

The restriction on programs to be internally finer than their specifications can be overcomed simply by adding more internal behavior to the program. More precisely, given systems A and B there always exists a system A′ such that A and A′ have the same observable behaviors, that is, Obs(A) = Obs(A′), and such that A′ is internally finer than B. E.g. using S′_{0} = (L^{P re}((d_{0}a_{0}d_{0}c_{0}(b_{0}c_{2} + c_{2}b_{0}))^{∗}), {a_{0}, b_{0}}, {c_{0}, c_{2}, d_{0}}) instead of S_{0} and with similar changes using S′_{1} and S′_{2} for S_{1} and S_{2}, respectively, we have that S′ = S′_{0} ∥ S′_{1} ∥ S′_{2} is internally finer than P and that Obs(S) = Obs(S′).

4.1 A uniform logical framework

In the finite setting, reasoning about systems can conveniently be expressed in M2L. Let U = IB^{m} be the universe, where m is a natural number. Any behavior α over U can be viewed as an interpretation of a sequence of secondorder variables U_{1}^{α}, …, U_{m}^{α}. So behaviors over, say, 1024 different events may be coded using just 10 variables.

We use for each event σ = (b_{1}, …, b_{m}) ∈ U and α the notation α(t) = σ for the M2L predicate

( ⋀_{b_{i}=1} t ∈ U_{i}^{α}) ∧ ( ⋀_{b_{i}=0} t ∉ U_{i}^{α}),

which states that the behavior denoted by α has a σ event in the position denoted by t. A system A = (L_{A}, Σ_{A}^{Obs}, Σ_{A}^{Int}) is represented by a triple

A = (ϕ_{A}, ϕ_{A}^{Obs}, ϕ_{A}^{Int})

of formulas defining the normalized traces of the system, ϕ_{A}(α), the observable events, ϕ_{A}^{Obs}(α, t), and the internal events, ϕ_{A}^{Int}(α, t). That is, N_{U}(A) = L(ϕ_{A}) and ϕ_{A}^{Obs}(α, t)) and ϕ_{A}^{Int}(α, t) are predicates that are true if and only if the position denoted by t in the behavior denoted by α is an element of Σ_{A}^{Obs} and Σ_{A}^{Int}, respectively. Given composable systems A and B, composition is represented by

A ∥ B = (ϕ_{A} ∧ ϕ_{B}, ϕ_{A}^{Obs} ∨ ϕ_{B}^{Obs}, ϕ_{A}^{Int} ∨ ϕ_{B}^{Int})

We have that L(ϕ_{A} ∧ ϕ_{B}) = L(ϕ_{A}) ∩ L(ϕ_{B}) = N_{U}(A ∥ B) and that ϕ_{A}^{Obs} ∨ ϕ_{B}^{Obs} and ϕ_{A}^{Int} ∨ ϕ_{B}^{Int} defines the union of the observable and the internal events, respectively. Let now behavior β be represented by U_{1}^{β}, …, U_{m}^{β}. The property that behaviors α and β in U^{∗} are Σ^{Obs}-synchronized is expressed by predicate ϕ_{A,B}^{Obs}(α, β) defined by

∀t : (ϕ_{A}^{Obs}(α, t) ∨ ϕ_{B}^{Obs}(α, t)) ⇒ α(t) = β(t)

The canonical trace abstraction R̂ of Definition 4.2 is defined by

R̂_{A,B}(α, β) ≡^{def} ϕ_{B}(β) ∧ ϕ_{A,B}^{Obs}(α, β)

By Proposition 4.1 and Theorem 4.1, the implementation property is implied by N_{U}(A) ⊆ dom R̂ and hence by the validity of

ϕ_{A}(α) ⇒ ∃β : R̂_{A,B}(α, β)  (3)

where ∃β is defined as ∃U_{1}^{β}. · · · ∃U_{m}^{β}. Let R_{i}(α, β) ≡^{def} R̂_{A_{i},B_{i}}(α, β) ∧ ϕ_{i}(α, β).

The premises of the decomposition rule 2.2 are expressed by

⋀_{i}(ϕ_{A_{i}}(α) ⇒ ∃β : R_{i}(α, β))  (4)
⋀_{i} ∃β_{i} : R_{i}(α, β_{i}) ⇒ ∃β : ⋀_{i} R_{i}(α, β)  (5)

To express the premise of Corollary 2.1 simply replace equation (5) above by

⋀_{i≠j} ∀t : ϕ_{B_{i}}^{Int}(α, t) ⇒ ¬ϕ_{B_{j}}^{Obs}(α, t)

Also, properties like composability and comparability can be expressed. The former by

∀t :  (ϕ_{A}^{Int}(α, t) ⇒ ¬ϕ_{B}^{Obs}(α, t)) ∧
(ϕ_{B}^{Int}(α, t) ⇒ ¬ϕ_{A}^{Obs}(α, t))

and the latter by

∀t : ϕ_{A}^{Obs}(α, t) ⇔ ϕ_{B}^{Obs}(α, t)

In general M2L is a very flexible logical language making it easy to write tense time and interval temporal logic operators in a straightforward manner. As examples, consider the past operator ϕ_{σ,μ}^{Before}(α) defined by

∀t_{1}. α(t_{1}) = μ ⇒ ∃t_{0}. t_{0} < t_{1} ∧ α(t_{0}) = σ,

and the interval operator ϕ_{σ}^{Between}(α, t_{1}, t_{2})

∃t. t_{1} < t < t_{2} ∧ α(t) = σ

4.2 Automated proofs

Formulas (3), (4), and (5) are potentially very difficult, since they involve quantification over behaviors, that is, over m second-order variables. Each quantification can lead to an exponential blow-up. But if A has much internal behavior, then it seems reasonable to use a more clever trace abstraction guided by A’s internal events. In fact, it must be suspected that it is inappropriate that the definition of R̂ does not involve A at all.

The canonical trace abstraction can be constrained by adding more precise information about the connection between the internal behavior of system A and B. This may reduce the blow-up—or even avoid it in the case a functional regular trace abstraction is formulated.

We next turn to a substantial verification problem to illustrate our technique.

5 A specification problem

In this section, we consider the problem proposed by Broy and Lamport [3]. The first part of [3] calls for a specification of a reactive system consisting of a number of sequential processes issuing blocking read and write calls to a memory server. The memory server maintains its memory by performing special atomic reads and writes whenever requested to do so by read and write calls. Depending on the success of atomic reads and writes, return events contain the answers to read and write calls. The memory must be able to handle several calls (from different processes) concurrently.

The second part of [3] calls for an implementation based on a remote procedure call protocol. The protocol involves a local and a remote party. Calls received locally are forwarded to the remote site, where they are executed. The resulting return events are propagated back to the local site. Altogether, we deal here with four levels of calls and returns.

The goal of [3] is now to verify that every observable trace of the implementation (where atomic read and writes and the remote events are abstracted away) is an observable trace of the specification.

The full informal description [3] includes many technical complications concerning the parameters passed and different kinds of erroneous behaviors. A detailed presentation of our solution can be found in [11].

In performing the verifications, we have limited ourselves to finite domains. We have chosen to have two locations, two kinds of values, two kinds of flags, and two process identities (in addition to the memory process). The resulting program has approximately a hundred thousand states and the specification approximately a thousand states. The systems allow thousands of different events. The systems are modelled as deterministic automata. The full specification amounts to more than 13 pages of M2L formulas (written in a macro language).

The aspect that we are interested in here is the use of trace abstractions. Without going into any further details, we assume that the M2L formulas ϕ_{P_{1}} ∧ ϕ_{P_{2}} and ϕ_{S_{1}} ∧ ϕ_{S_{2}} define the implementation and the specification, respectively, of our solution. The universe U consists of τ and a number of parameterized events: rd, wrt, rtn, atmrd, atmwrt, rpcCall, rpcRtn denoting reads, writes, returns, atomic reads, atomic writes, rpc calls and rpc returns respectivly. For example, rd : [?, obs, 1] is a read event, where the first parameter is unspecified, the second is obs, which stands for an observable event, and the last parameter 1 denotes the process id. A similar notation is used for other events.

The Mona tool is currently not able to handle automata of the size corresponding to the distributed program just discussed. Hence we prove the correctness of the implementation by using our composition rule. The obvious idea is to try whether

ϕ_{P_{i}}(α) ⇒ ϕ_{S_{i}}(α)

holds (for i = 1 or i = 2; the formulas are symmetric). The Mona tool, however, quickly determines that this formula is not valid. There is a counter-example of length 12:

rd:[obs], rpcCall, rd, atmrd, rtn, rpcRtn, rpcCall, rd, atmrd, rtn, rpcRtn, rtn:[obs]

where we have left out most of the parameters. The counter-example arises because the specification system requires exactly one atomic read in every successful read call, whereas the implementation is allowed to retry on failure.

Fortunately, we can let Mona establish

ϕ_{P_{i}}(α) ⇒ ∃β. R̂_{i}(α, β),  (6)

where R̂_{i}(α, β) ≡^{def} ϕ_{P_{i},S_{i}}^{Obs}(α, β) ∧ ϕ_{S_{i}}(α, β) is the canonical trace abstraction. Thus, ϕ_{P_{i}} implements ϕ_{S_{i}}.

To avoid explicitly modeling the whole system at the implementation level, we use the proof rule for compound systems. The compatibility premise of Theorem 2.2 becomes:

⋀_{i} ∃β_{i} : R̂_{i}(α, β_{i}) ⇒ ∃β : ⋀_{i} R̂_{i}(α, β)  (7)

However, the existential quantification on the right hand side of the implication leads to a state explosion that cannot be handled by the Mona tool.

Instead, we can exploit the information that the counter-example provided to formulate a more precise trace abstraction. So we have defined predicates that in more detail describe how internal events at one level relate to internal events at the other level. For example, we may add our intuition that between any successful read and its corresponding return at the implementation level only the last atomic read is mapped to an atomic read on the specification level. This formula, which we denote by ψ_{i}, looks like:

∀t_{1}, t_{2}. (t_{1} < t_{2} ∧
α(t_{1}) = rd : [?, obs, i] ∧
α(t_{2}) = rtn : [?,?, normal, obs, i] ∧
¬ϕ_{rd:[?,obs,i]}^{Between}(α, t_{1}, t_{2}) ∧
¬ϕ_{wrt:[?,?,obs,i]}^{Between}(α, t_{1}, t_{2}))
⇒
(∃t. t_{1} < t < t_{2} ∧
α(t) = β(t) = atmrd : [?,?,?, i] ∧
¬ϕ_{atmrd:[?,?,?,i]}^{Between}(α, t, t_{2}) ∧
¬ϕ_{atmrd:[?,?,?,i]}^{Between}(β, t_{1}, t) ∧
¬ϕ_{atmrd:[?,?,?,i]}^{Between}(β, t, t_{2}))

We define the new trace abstractions R_{i}(α, β) to be equal to R̂_{i} conjoined with the ψ_{i} and two other similar predicates (one stating that any event on the program level—but an atomic read—is matched by the same event on the specification level; the other stating that an atomic read event on the program level is matched by either an atomic read event or a τ event on the specification level). With R_{i}, the Mona tool proves formulas (6) and (7) within minutes.

The compatibility property (7) is stated in a single M2L formula of size 10^{5} with approximately 32 visible variables at the level of deepest nesting (corresponding to an alphabet size of 2^{32}). During its processing automata with millions of BDD nodes are created. The proof required user intervention in the form of an explicit (but natural) ordering of BDD variables. Also, we have supplied a little information about evaluation order in the form of parentheses.

6 Conclusion

We have offered a practical alternative to the use of refinement mappings. We have indicated how the user contribution of information about behavioral similarities directly can be used to reduce the computational work involved in guessing internal events when two distributed systems are compared.

Our method is entirely formulated within M2L: state machines, temporal properties, finite domains, and verification rules all take on the syntax of the Mona system.

Our experiments show that very complex temporal logic formulas on finite segments of time can be decided in practice—quite in contrast to the situation for temporal logic on the natural numbers.

References

[1] M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.

[2] M. Abadi and L. Lamport. Conjoining specifications. Technical Report Report 118, Digital Equipment Corporation, Systems Research Center, 1993.

[3] M. Broy and L. Lamport. Specification problem, 1994. A case study for the Dagstuhl Seminar 9439.

[4] E. M. Clark, I.A. Browne, and R.P Kurshan. A unified approach for showing language containment and equivalence between various types of ω-automata. In A. Arnold, editor, CAAP, LNCS 431, pages 103–116, 1990.

[5] E. M. Clarke, O. Grumberg, and D. E. Long. Verification tools for finitestate concurrent systems. In A Decade of Concurrency, pages 124–175. Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 803, Proceedings of the REX School/Symposium, Noordwijkerhout, The Netherlands, June 1993.

[6] U. Engberg, Grønning P., and Lamport L. Mechanical verification of concurrent systems with tla. In Computer Aided Verification, CAV ’92. Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 663.

[7] Manna Z. et al. Step: The stanford temporal prover. In Theory and Practice of Software Development (TAPSOFT). Springer-Verlag, 1995. Lecture Notes in Computer Science, Vol. 915.

[8] J.G. Henriksen, O.J.L. Jensen, M.E. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A.B. Sandholm. Mona: Monadic second-order logic in practice. In U.H. Engberg, K.G. Larsen, and A. Skou, editors, Procedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 58–73, 1995. BRICS Notes Series NS-95-2.

[9] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

[10] Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification and simulation and refinement. In A Decade of Concurrency, pages 273–346. ACM, Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 803, Proceedings of the REX School/Symposium, Noordwijkerhout, The Netherlands, June 1993.

[11] N. Klarlund, M. Nielsen, and K. Sunesen. Using monadic second-order logic with finite domains for automated verification. Technical Report RS-95-54, BRICS, Aarhus University, 1995.

[12] N. Klarlund and F.B. Schneider. Proving nondeterministically specified safety properties using progress measures. Information and Computation, 107(1):151–170, 1993.

[13] R. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.

[14] R. P. Kurshan, M. Merritt, A. Orda, and S. R. Sachs. Modelling asynchrony with a synchronous model. In Computer Aided Verification, CAV ’95, LNCS, 1995. Lecture Notes in Computer Science.

[15] L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, 1983.

[16] L. Lamport. The temporal logic of actions. Technical Report Report 70, Digital Equipment Corporation, Systems Research Center, 1994. To appear in Transactions on Programming Language and Systems.

[17] N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. Sixth Symp. on the Principles of Distributed Computing, pages 137–151. ACM, 1987.

[18] N. Lynch and F. W. Vaandrager. Forward and backward simulations – part i: untimed systems. Technical Report CS-R9313, Centrum voor Wiskunde en Informatica, CWI, Computer Science/Department of Software Technology, 1993.

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

[20] A.P. Sistla. On verifying that a concurrent program satisfies a nondeterministic specification. Information Processing Letters, 32(1):17–24, July 1989.

A Proof of Theorem 2.1

Proof: Only if: Assume that R is a trace abstraction from A to B. Let η ∈ Obs(A). Then there exists a trace α ∈ L_{A} ⊆ N_{U}(A) such that η = π(α). By 2.) and 3.) of Definition 2.2 there exists a β ∈ N_{U}(B) such that αRβ and hence by 1.) of Definition 2.2 such that π(α) = π(β). Hence η = π(α) = π(β) ∈ Obs(B). If: Assume Obs(A) ⊆ Obs(B). Define R = {(α, β) | β ∈ N_{U}(B) ∧ π(α) = π(β)} ⊆ U^{∗} × U^{∗}. We prove that R is a trace abstraction from A to B. Clearly, 1) and 3) of Definition 2.2 are satisfied. To see that 2) is satisfied let α ∈ N_{U}(A). Then π(α) ∈ Obs(A) ⊆ Obs(B) by assumption. Hence there exists a β ∈ L_{B} ⊆ N_{U}(B) such that π(α) = π(β). Thus αRβ and therefore α ∈ dom R. □

B Proof of Theorem 2.2

Proof: The key is that the R_{i}’s are trace abstractions on U^{∗} × U^{∗}. Assume (1) and (2). By Theorem 2.1, it is enough to prove that ⋂_{i} R_{i} is a trace abstraction from ∥A_{i} to ∥B_{i} on U^{∗} × U^{∗}.

We show that ⋂_{i} R_{i} satisfies 1.)-3.) of Definition 2.2.

1.) Obvious.

2.) N_{U}(∥A_{i}) = ⋂_{i} N_{U}(A_{i}) ⊆ ⋂_{i} dom R_{i} ⊆ dom ⋂_{i} R_{i}. The first inclusion follows from assumption (1) and Definition 2.2(2). The second inclusion from assumption (2).

3.) rng ⋂_{i} R_{i} ⊆ ⋂_{i} rng R_{i} ⊆ ⋂_{i} N_{U}(B_{i}) = N_{U}(∥B_{i}). The second inclusion follows from assumption (1) and Definition 2.2(3).

□

C Proof of Corollary 2.1

Proof: Assume that Σ_{B_{i}}^{Int} ∩ Σ_{B_{j}}^{Int} = ∅ for every i ≠ j and that A_{i} implements B_{i}. Let Σ_{i}^{Obs} = Σ_{A_{i}}^{Obs} = Σ_{B_{i}}^{Obs}, Σ^{Obs} = Σ_{∥A_{i}}^{Obs} = Σ_{∥B_{i}}^{Obs}, and let π, π_{i} and h_{i} be the projections from U^{∗} to (Σ^{Obs})^{∗}, (Σ_{i}^{Obs})^{∗} and (Σ_{B_{i}})^{∗}, respectively. By Theorem 2.1, there exist trace abstractions from A_{i} to B_{i}. Let R_{i} be the largest such, that is R_{i} = {(α, β) | β ∈ N_{U}(B_{i}) ∧ π_{i}(α) = π_{i}(β)}.

We first prove that if R_{i} is a trace abstraction then also R′_{i} given by R_{i} ∩ {(α, β) | π(α) = π(β)} is a trace abstraction. Clearly, it is sufficient to show that for all α ∈ U^{∗} if there exists a β ∈ N_{U}(B_{i}) such that π_{i}(α) = π_{i}(β) then there exists a β′ ∈ N_{U}(B_{i}) such that π(α) = π(β′). To show this assume that α ∈ U^{∗} and β ∈ N_{U}(B_{i}) such that π_{i}(α) = π_{i}(β). Then h_{i}(β) ∈ L_{B_{i}} ⊆ N_{U}(B_{i}) and π_{i}(h_{i}(β)) = π_{i}(α) = o_{1} … o_{m}, where o_{j} ∈ Σ_{i}^{Obs}. Let α_{1}, …, α_{m+1} ∈ (U−Σ_{i}^{Obs})^{∗} and β_{1}, …, β_{m+1} ∈ (Σ_{B_{i}}^{Int})^{∗} be such that

α = α_{1}o_{1}α_{2} … α_{m}o_{m}α_{m+1},
h_{i}(β) = β_{1}o_{1}β_{2} … β_{m}o_{m}β_{m+1}

then

β′ = π(α_{1})β_{1}o_{1} … π(α_{m})β_{m}o_{m}π(α_{m+1})β_{m+1}

is in N_{U}(B_{i}), since h_{i}(β′) = h_{i}(β) as π(α_{i}) ∈ (Σ^{Obs} − Σ_{i}^{Obs})^{∗} and clearly π(α) = π(β′).

We next prove that ⋂_{i} dom R′_{i} ⊆ dom ⋂_{i} R′_{i} and hence the result follows from Theorem 2.2. Given α ∈ ⋂_{i} dom R′_{i}. Let

α = α_{1}o_{1}α_{2} … α_{m}o_{m}α_{m+1}

where o_{j} ∈ Σ^{Obs} and α_{j} ∈ (U − Σ^{Obs})^{∗}. Then there exists

β^{1} = β_{1}^{1}o_{1} … β_{m}^{1}o_{m}β_{m+1}^{1} ∈ N_{U}(B_{1})
⋮
β^{n} = β_{1}^{n}o_{1} … β_{m}^{n}o_{m}β_{m+1}^{n} ∈ N_{U}(B_{n})

where β_{1}^{i}, …, β_{m+1}^{i} ∈ (Σ_{B_{i}}^{Int})^{∗} such that αR′_{i}β^{i}. Hence

η = β_{1}^{1} … β_{1}^{n}o_{1} … β_{m}^{1} … β_{m}^{n}o_{m}β_{m+1}^{1} … β_{m+1}^{n}

is in N_{U}(∥B_{i}), since h_{i}(η) = β^{i} as Σ_{B_{i}}^{Int} ∩Σ_{B_{j}}^{Int} = ∅ for i ≠ j, and thus α(⋂_{i} R_{i})η. □

D Proof of Proposition 4.1

Proof: Assume that N_{U}(A) ⊆ dom R̂ then by Definition 4.2, R̂ is a trace abstraction, c.f. Definition 2.2.

To see that R̂ is regular consider the following definition.

Definition D.1 Let D_{U} and D_{B} be the deterministic finite automata associated with the sets of normalized traces of the finite system B and the universe U, respectively. Define from these a non-deterministic automaton D_{U} ⊗ D_{B} on the alphabet U × U as follows. The initial state is the pair of initial states. A state is accepting iff it is a pair of accepting states. The transition relation is given

by the set {(s, s′) →^{(a,b)} (t, t′)|s →^{a} t ∧ s′ →^{b} t′ ∧ ((a ∉ Σ^{Obs} ∧ b ∉ Σ^{Obs}) ∨ a = b)}

The product automaton lock steps the two automata forcing observable events to be synchronized and guessing the right pair otherwise.

Let α = α_{1} … α_{n} ∈ U and β = β_{1} … β_{n} ∈ U. Assume α^{∧}β ∈ L(D_{U} ⊗ D_{B}). Then there exists an accepting run

(s_{0}, t_{0}) →^{(α_{1},β_{1})} (s_{1}, t_{1}) →^{(α_{2},β_{2})} … →^{(α_{n},β_{n})} (s_{n}, t_{n})

of D_{U} ⊗ D_{B} and it is now trivial to check that α and β are Σ^{Obs}-synchronized and that β ∈ N_{U}(B). Hence α^{∧}β ∈ R̂. Conversely, assume that 1) α and β are Σ^{Obs}-synchronized, 2) β ∈ N_{U}(B). We prove that α^{∧}β ∈ L(D_{U} ⊗ D_{B}). Since α ∈ U^{∗} there exists an accepting run

s_{0} →^{α_{1}} s_{1} →^{α_{2}} … →^{α_{n}} s_{n}

of D_{U} and likewise, since β ∈ N_{U}(B) there exists an accepting run

t_{0} →^{β_{1}} t_{1} →^{β_{2}} … →^{β_{n}} t_{n}

of D_{B}. Due to 1.) and Definition D.1 it follows that

(s_{0}, t_{0}) →^{(α_{1},β_{1})} (s_{1}, t_{1}) →^{(α_{2},β_{2})} … →^{(α_{n},β_{n})} (s_{n}, t_{n})

is an accepting run of D_{U} ⊗ D_{B} accepting α^{∧}β.

Finally, since C is regular the last result follows trivially. □

E Proof of Theorem 4.1

Proof: The only if direction is as in the proof of Theorem 2.1, c.f. appendix A. We prove the if direction. Let π be the projection from U^{∗} onto (Σ^{Obs})^{∗}. Assume that A implements B. Let R̂ be the language defined in Definition 4.2. According to Proposition 4.1, we only need to prove that N_{U}(A) ⊆ dom R̂. Let α ∈ N_{U}(A). Then, since A implements B, π(α) ∈ Obs(A) ⊆ Obs(B), and hence by assumption there exists a trace β ∈ L_{B} such that α′ = h(α) ∈ L_{A} is internally finer that β, where h is the projection from U^{∗} onto Σ_{A}^{∗}. Let π(α′) = π(α) = π(β) = o_{1} … o_{n} and

α = α_{1}o_{1}α_{2} … α_{n}o_{n}α_{n+1},
α′ = α′_{1}o_{1}α′_{2} … α′_{n}o_{n},
β = β_{1}o_{1}β_{2} … β_{n}o_{n}

where o_{j} ∈ Σ^{Obs}, α_{j} ∈ (U − Σ^{Obs})^{∗}, α′_{j} ∈ (Σ_{A}^{Int})^{∗} and β_{j} ∈ (Σ_{B}^{Int})^{∗}. Note, that since L_{A} and L_{B} are prefix-closed we can with out lose of generality assume that α′ and β end in observable events. Since α′ is internally finer than β, it follows that |α′_{i}| ≥ |β_{i}| for every i = 1, …, n, and since α′ is the projection of α onto Σ_{A}^{∗}, it follows that |α_{i}| ≥ |α′_{i}| for every i = 1, …, n. Define

η = η_{1}o_{1}η_{2} … η_{n}o_{n}η_{n+1}

where η_{i} = β_{i}τ^{|α_{i}|−|β_{i}|} for i = 1, …, n and η_{n+1} = τ^{|α_{n+1}|}. Hence we have the required η such that αRη, since η and α are Σ^{Obs}–synchronized and η ∈ N_{U}(B). □

Recent Publications in the BRICS Report Series

RS-95-53 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Automated Logical Veri�cation based on Trace Abstractions. November 1995. 19 pp.

RS-95-52 Anton��n Ku� cera. Deciding Regularity in Process Algebras. October 1995. 42 pp.

RS-95-51 Rowan Davies. A Temporal-Logic Approach to Binding-Time Analysis. October 1995. 11 pp.

RS-95-50 Dany Breslauer. On Competitive On-Line Paging with Lookahead. September 1995. 12 pp.

RS-95-49 Mayer Goldberg. Solving Equations in the λ-Calculus using Syntactic Encapsulation. September 1995. 13 pp.

RS-95-48 Devdatt P. Dubhashi. Simple Proofs of Occupancy Tail Bounds. September 1995. 7 pp. To appear in Random Structures and Algorithms.

RS-95-47 Dany Breslauer. The Suf�x Tree of a Tree and Minimizing Sequential Transducers. September 1995. 15 pp.

RS-95-46 Dany Breslauer, Livio Colussi, and Laura Toniolo. On the Comparison Complexity of the String Pre�x-Matching Problem. August 1995. 39 pp. Appears in Leeuwen, editor, Algorithms - ESA ’94: Second Annual European Symposium proceedings, LNCS 855, 1994, pages 483�494.

RS-95-45 Gudmund Skovbjerg Frandsen and Sven Skyum. Dynamic Maintenance of Majority Information in Constant Time per Update. August 1995. 9 pp.

RS-95-44 Bruno Courcelle and Igor Walukiewicz. Monadic Second-Order Logic, Graphs and Unfoldings of Transition Systems. August 1995. 39 pp. To be presented at CSL ’95.

RS-95-43 Noam Nisan and Avi Wigderson. Lower Bounds on Arithmetic Circuits via Partial Derivatives (Preliminary Version). August 1995. 17 pp. To appear in 36th Annual Conference on Foundations of Computer Science, FOCS ’95, IEEE, 1995.