BRICS RS-95-18 A. Cheng: Complexity Results for Model Checking

BRICS

Basic Research in Computer Science

Complexity Results for Model Checking

Allan Cheng

BRICS Report Series RS-95-18 ISSN 0909-0878 February 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)

Complexity Results for Model Checking^{⋆}

Allan Cheng^{⋆⋆}

Computer Science Department Cornell University Ithaca, New York 14853, USA

                 e-mail:acheng@cs.cornell.edu

Abstract. The complexity of model checking branching and linear time temporal logics over Kripke structures has been addressed in e.g. [SC85, CES86]. In terms of the size of the Kripke model and the length of the formula, they show that the model checking problem is solvable in polynomial time for CTL and NP-complete for L(F). The model checking problem can be generalised by allowing more succinct descriptions of systems than Kripke structures. We investigate the complexity of the model checking problem when the instances of the problem consist of a formula and a description of a system whose state space is at most exponentially larger than the description. Based on Turing machines, we define compact systems as a general formalisation of such system descriptions. Examples of such compact systems are K-bounded Petri nets and synchronised automata, and in these cases the well-known algorithms presented in [SC85, CES86] would require exponential space in term of the sizes of the system descriptions and the formulas; we present polynomial space upper bounds for the model checking problem over compact systems and the logics CTL and L(X, U, S). As an example of an application of our general results we show that the model checking problems of both the branching time temporal logic CTL and the linear time temporal logics L(F) and L(X, U, S) over K-bounded Petri nets are PSPACE-complete.

1 Introduction

Formal verification techniques of distributed systems have received much attention, see for example [Lam80, SC85, CES86, Lar88, Mil89, SW89, Val90, WG93].

A predominant technique is known as model checking. The approach is as follows. The systems one considers either explicitly or implicitly specify a state space which can be regarded as a (labelled) graph. Viewing these graphs as models (Kripke structures) for temporal logics, one can use logical formulas to express properties of the graphs. The problem of verifying if a system satisfies

⋆ This work has been supported by The Danish Research Councils and the Danish

Research Academy. ⋆⋆ Visiting from Aarhus, BRICS, Basic Research in Computer Science, Centre of the

Danish National Research Foundation. e-mail:acheng@daimi.aau.dk

a property encoded in a formula then reduces to the problem of checking if the formula is satisfied in the systems state space.

The complexity of the model checking problem for both linear and branching time propositional temporal logics has been investigated, among others, by Sistla and Clarke in [SC85] and by Clarke, Emerson, and Sistla in [CES86]. Both papers consider Kripke structures (or just structures) as models for the logics and the complexity results are stated in terms for the sizes of the structures and the length of the formulas. The paper [CES86] shows that the model checking problem for the computational tree logic CTL can be solved in polynomial time while [SC85] shows that the model checking problem for the linear time temporal logic L(F) is NP-complete.

There exists other well known classes of systems over which we can interpret such logics. K-bounded Petri nets and synchronised automata are examples of such systems. Common to these systems is that they can be viewed as compact representations of structures. More precisely, they can specify structures whose sizes are exponentially larger than the description of the systems. For example, the state space of a K-bounded Petri net can be (no more than) exponentially larger than the net. We will call such systems compact systems.

K-bounded Petri nets [JLL77] and synchronised automata [WG93] are examples of models which are widely use to specify and implement concurrent systems. Verification techniques for these and related systems have been presented in [Lar88, SW89, Val90, WG93, ES92, Esp93, BCM^{+}92]. Whereas the work in [Lar88, SW89] focuses on algorithms (tableau systems) for solving the model checking problem, the work in [Val90, WG93, ES92, Esp93, BCM^{+}92] is mainly motivated by the state space explosion problem and how to overcome this problem taking time, and especially, space consumption into account. Structures such as “stubborn sets”, “persistent sets”, “net unfoldings”, and “Binary Decision Diagrams” are proposed.

It is therefore important to evaluate these verification techniques with respect to their space requirements. A primary measure for this evaluation is space complexity. For more specific problems connected to 1-safe Petri nets, for example for the reachability, liveness, and deadlock problem, such a study has been presented in [CEP93].

In this paper we choose a rather general setting both in terms of the systems considered and the problems to be solved. Namely, we formalise the notion of compact systems and investigate what happens to the complexity of the model checking problem in terms of the size of a compact system and the length of the formula. We show that for the well-known temporal logics CTL, L(F), and L(X, U, S) and any class of compact systems, the model checking problem is in PSPACE. Since for most nontrivial classes of compact systems the model checking problem for temporal logics containing the F (future) operator is usually PSPACE-hard, our results provide matching upper bounds. In contrast, the algorithms in [SC85, CES86] for CTL and L(F) would both require exponential space. As an example of how our results may be applied, we consider K-bounded Petri nets. From [CEP93] we easily conclude that the problems for CTL, L(F), and L(X, U, S) are PSPACE-hard. Our results then allow us to conclude that they that PSPACE-complete. In terms of the size of the state spaces of the K-bounded Petri nets (and the length of the formulas) the complexities are P [CES86], NP-complete and PSPACE-complete [SC85], respectively.

The paper is organised as follows. In Sect. 2 we give the necessary definitions. This includes compact systems, the logics and their interpretations, and the model checking problems. Then, in Sect. 3 we give the upper bounds on the model checking problems. In Sect. 4 we apply our results to K-bounded Petri nets and in Sect. 5 we conclude and give suggestions for future work.

2 Definitions

Intuitively, the systems we will consider all have the property that we can associate to them Kripke structures which corresponds to their state space. Moreover, the size of this Kripke structure is atmost exponential in the size of the description of the system. For example K-bounded Petri nets (Petri nets where each place can have atmost K tokens) have this property; a net with n places has atmost (K + 1)^{n} reachable states. We shall refer to these systems as compact systems. We continue by formalising compact systems, defining the logics B(X, U) (CTL) and L(X, U, S) and their interpretations, and finally the model checking problems.

2.1 The Compact Systems

A class of compact systems will be described using strings to encode the systems and a polynomial space bounded nondeterministic Turing machine which given an encoding of a system will “simulate” it. The state space of the Turing machine will then be used to define the state space of the input string (the compact system). In Sect. 4 we will present K-bounded Petri nets as a class of compact systems. For the ease of the presentation we assume that the reader is familiar with Turing machines and basic complexity theory, see [HU79] for an introduction.

Definition 1. A class of compact systems, (C, M_{C}), is a set C = {s_{1}, s_{2}, …} of strings referred to as systems, over some alphabet Σ, together with a polynomial space bounded nondeterministic Turing machine M_{C} with a distinguished “signal” state q^{⋆} such that

– for any s ∈ C, M_{C} has a unique configuration^{3} c_{s}, such that any computation on s reaches c_{s} and c_{s} is the first configuration along the computation whose machine state is q^{⋆}. Intuitively, c_{s} is the initial state of the system s.

– for any string s ∉ C, M_{C} will never enter the state q^{⋆} for any computation on input s.

3 A configuration of M_{C} consists of the contents of the tape, a machine state, and a postition on the tape.

In the following we assume a fixed class of compact systems (C, M_{C}). Since M_{C} is polynomial space bounded on inputs of length n, say by the polynomial q′(n), M_{C} has on any input s atmost exponentially many reachable configurations whose machine state is q^{⋆}; there exists a B > 0 and a polynomial q(n), independent of s, such that given s there are atmost B^{q(|s|)} possible configurations. Call the configurations whose machine state is q^{⋆} signal configurations, and let Sig_{M_{C}}(s) = {c | c is a signal configuration of M_{C} on input s}. We can now define the state space associated to s ∈ C.

Definition 2. For s ∈ C, let (V_{s}, E_{s}, i_{s}) be the rooted graph whose nodes V_{s} are Sig_{M_{C}}(s), the signal configurations of M_{C} on input s, whose edges are pairs of nodes (c, c′) such that (c, c′) ∈ E_{s} if and only if M_{C} can reach c′ from c without entering any other signal configurations, and whose initial/root node is the unique configuration c_{s}.

Remark. We shall refer to (V_{s}, E_{s}, i_{s}) as the state space of the system s, whenever s ∈ C. Also, the nodes will be refered to as states of s and will be ranged over by v, w, . . .. Notice that any system s has atmost B^{q(|s|)} states. Whenever (V_{s}, E_{s}, i_{s}) is understood from the context, we will use the notation v_{0} → v_{1} → ⋯ → v_{n} instead of (v_{0}, v_{1}), (v_{1}, v_{2}), …, (v_{n−1}, v_{n}) ∈ E_{s}. For a state v of s, we use the notation v ↛ to indicate that there exists no state v′ ∈ V_{s} such that v → v′.

A run of the system s is any sequence v_{0} → v_{1} → ⋯ that is either infinite or ends in a state v_{n} such that v_{n} ↛. The length of a finite run v_{0} → ⋯ → v_{n} is n. We will use Greek letters σ, γ, … to denote runs of the system s.

Henceforth, we assume a fixed class of compact systems (C, M_{C}) and continue by giving the syntax of the temporal logics we will be considering.

2.2 The Logics

Let A be a set of atomic propositions. We assume it to be fixed in the following. We will consider the temporal logics L(X, U, S) and B(X, U), both described in detail in [Eme90].

The formulas of the logic L(X, U, S) over A are defined inductively:

– t, f, or any p ∈ A.

– ¬ϕ_{1}, ϕ_{1} ∧ ϕ_{2}, X(ϕ_{1}), ϕ_{1}Uϕ_{2}, and ϕ_{1}Sϕ_{2} are formulas, where ϕ_{1} and ϕ_{2} are formulas.

L(X, U, S) is a linear time temporal logic, whose formulas are interpreted over runs of a systems s.

In order to interpret the formulas of L(X, U, S) over the runs of a system s we need a valuation η_{s} : A × Sig_{M_{C}}(s) ⟶ 2 which tells us if an atomic proposition holds at a state. Furthermore, we require that the valuation eta_{s} is computable by a polynomial space bounded deterministic Turing machine which we denote T_{η_{s}}. We assume the atomic propositions to be encoded as strings.

Given s, σ = v_{0} → v_{1} → ⋯ a run of s, a natural number 0 ≤ i ≤ |σ|, and η_{s}. Relative to η_{s} we interpret the formulas of L(X, U, S) at (σ, i) as follows:

– (σ, i) ⊧ t and (σ, i) |̸= f.

– (σ, i) ⊧ p iff η_{s}(p, v_{i}) = 1.

– (σ, i) ⊧ ¬ϕ iff (σ, i) |̸= ϕ.

– (σ, i) ⊧ ϕ_{1} ∧ ϕ_{2} iff (σ, i) ⊧ ϕ_{1} and (σ, i) ⊧ ϕ_{2}.

– (σ, i) ⊧ X(ϕ) iff i < |sigma| and (σ, i + 1) ⊧ ϕ.

– (σ, i) ⊧ ϕ_{1}Uϕ_{2} iff there exists a natural number i ≤ j ≤ |σ| such that (σ, j) ⊧ ϕ_{2} and for all i ≤ k < j, (σ, k) ⊧ ϕ_{1}.

– (σ, i) ⊧ ϕ_{1}Sϕ_{2} iff there exists a 0 ≤ j ≤ i such that (σ, j) ⊧ ϕ_{2} and for all j < k ≤ i, (σ, k) ⊧ ϕ_{1}.

The interpretation of the logic should be clear except perhaps for ϕ_{1}Uϕ_{2} and ϕ_{1}Sϕ_{2}. Intuitively the former expresses that ϕ_{2} holds somewhere in the future and that ϕ_{1} holds “until” then; the latter expresses that somewhere in the past ϕ_{2} holds and “since” then, ϕ_{1} holds. Remember that the “past” and “future” is relative to σ.

Next, we consider a well-known branching time temporal logic. The formulas of the logic B(X, U) over A (also known as CTL [CES86]) are also defined inductively:

– t, f, or any p ∈ A.

– ¬ϕ_{1}, ϕ_{1} ∧ ϕ_{2}, EX(ϕ_{1}), AX(ϕ_{1}), E(ϕ_{1}Uϕ_{2}), or A(ϕ_{1}Sϕ_{2}) are formulas, where ϕ_{1} and ϕ_{2} are formulas.

B(X, U) is a branching time logic whose formulas are interpreted at state of a system s.

Given a system s, v a state of s, and a valuation η_{s}. Then, the formulas of B(X, U) are interpreted relative to η_{a} as follows:

– v ⊧ t and v |̸= f.

– v ⊧ p iff η_{s}(p, v) = 1.

– v ⊧ ¬ϕ iff v |̸= ϕ.

– v ⊧ ϕ_{1} ∧ ϕ_{2} iff v ⊧ ϕ_{1} and v ⊧ ϕ_{2}.

– v ⊧ EX(ϕ) iff there exists v → v′ such that v′ ⊧ ϕ.

– v ⊧ AX(ϕ) iff for all v → v′, v′ ⊧ ϕ.

– v ⊧ E(ϕ_{1}Uϕ_{2}) iff there exists v → v_{1} → ⋯ → v_{n} such that v_{n} ⊧ ϕ_{2} and for all 0 ≤ j < n, v_{j} ⊧ ϕ_{1}, where v_{0} = v.

– v ⊧ A(ϕ_{1}Uϕ_{2}) iff for all v → v_{1} → ⋯ there exists an n such that v_{n} ⊧ ϕ_{2} and for all 0 ≤ j < n, v_{j} ⊧ ϕ_{1}, where v_{0} = v.

The interpretation of the temporal formulas shows the branching nature of B(X, U). At a state several possible successor states or paths have to be taken into account. The intuition behind the interpretation of the “until” formulas corresponds well to that of L(X, U, S) except that we quantify existentially or universally over paths from the state v.

2.3 The Model Checking Problems

Definition 3. An instance of the model checking problem for L(X, U, S) is a tuple (s, T_{η_{s}}, ϕ), where s ∈ C, η_{s} is a valuation, and ϕ is a L(X, U, S) formula. The model checking problem for (s, T_{η_{s}}, ϕ) is to decide whether or not there exists a run σ of the system s such that (σ, 0) ⊧ ϕ.

Definition 4. An instance of the model checking problem for B(X, U) is a tuple (s, T_{η_{s}}, ϕ), where s ∈ C, η_{s} is a function, and ϕ is a B(X, U) formula. The model checking problem for (s, T_{η_{s}}, ϕ) is to decide whether or not i_{s} ⊧ ϕ.

Remark. Notice that the valuation is usually implicitely assumed part of the problem instances to the model checking problem [SC85] or assume to be easily computable [CES86]. We could also have defined a valuation to be relative to (C, M_{C}) and A. This wouldn’t leed to any significant changes of the results.

Having given the necessary definitions, we summarize in the table below our results and related known results [SC85, CES86] about the model checking problem.

Logic  Problem Instance  Complexity
CTL  R-structure (Kripke)  P

and a formula

L(F) R-structure NP-complete

and a formula

L(X, U, S) R-structure PSPACE-complete

and a formula

CTL  Compact system
L(F) and a formula PSPACE
L(X, U, S)

Fig. 1. Complexity in terms of Kripke structures and compact systems.

3 The Upper Bounds

In this section we provide PSPACE upper bounds for the model checking problems defined in Def. 3 and Def. 4. We start by L(X, U, S).

3.1 Linear Time

The results of this section is based on the idea behind the decision procedure for the logic L(X, U, S) given in [SC85]. There, Sistla and Clarke also reduce the problem of determining truth in an R-structure (model checking problem over Kripke structures) to the satisfiability problem by encoding an R-structure into a formula. Since a compact system may have exponentially many states, encoding the state space (Kripke structure) of a system in a formula would yield an exponentially long formula.

Instead one could try to encode the system itself in the logic. This is easily done for systems like 1-safe Petri nets. However, when considering other models like K-bounded Petri nets, this encoding quickly becomes more troublesome. One of the reasons why we have chosen the setting of (C, M_{C}) is because describing a class of systems as a class of compact sytems is often more straightforward and credible.

Our solution is based on proving the existence of a run which ends in a dead state v′, v′ ↛, or in a loop. Moreover, one has to bound the lengths of these paths. This seems to be the only (obvious) technique applicable to solve the problem.

Definition 5. Given a system s, σ = v_{0} → v_{1} → ⋯ a run of s, ϕ a formula of L(X, U, S), and η_{s} a valuation. Then, Sub(σ, i, ϕ) is the set of subformulas ϕ′ of ϕ such that (σ, i) ⊧ ϕ′.

Lemma 6. Given a system s, σ = v_{0} → v_{1} → ⋯ a run of s, ϕ a formula of L(X, U, S), and η_{s}. If Sub(σ, i, ϕ) = Sub(σ, j, ϕ), i < j ≤ |σ|, and v_{i} = v_{j}, then

∀0 ≤ l ≤ i. Sub(σ, l, ϕ) = Sub(σ′, l, ϕ)
∀j ≤ l ≤ |σ|. Sub(σ, l, ϕ) = Sub(σ′, l − (j − i), ϕ)

where all indices range over natural numbers and σ′ = v′_{0} → v′_{1} → ⋯ = v_{0} → ⋯ → v_{i} → v_{j+1} → v_{j+2} → · · ·.

Proof. Induction in ϕ. ⊓ ⊔

Given a run σ = v_{0} → v_{1} → ⋯ of a system s, two indices i and j, and a formula ϕ of L(X, U, S). ϕ is said to be fulfilled between i and j if and only if i < j and there exists a k, i ≤ k < j, such that (σ, k) ⊧ ϕ.

Lemma 7. Given a systems s, σ = v_{0} → v_{1} → ⋯ an infinite run of s, ϕ a formula of L(X, U, S), an index i, and a natural number p > 0 (the period) such that v_{i} = v_{i+p}, Sub(σ, i, ϕ) = Sub(σ, i + p, ϕ), and for every formula ϕ_{1}Uϕ_{2} in Sub(σ, i, ϕ), ϕ_{2} is fulfilled between i and i + p. Let σ′ = v′_{0} → v′_{1} → ⋯ be the run v_{0} → … → v_{i} → ⋯ → v_{i+p−1} → v_{i} → ⋯ → v_{i+p−1} → v_{i} → ⋯, i.e. the period v_{i} → ⋯ → v_{i+p} is repeated infinitely often. Then

∀0 ≤ l ≤ i + p. Sub(σ, l, ϕ) = Sub(σ′, l, ϕ)
∀i ≤ l. Sub(σ′, l, ϕ) = Sub(σ′, (l + p), ϕ)

Proof. Induction in ϕ, case based analysis. ⊓ ⊔

Lemma 7 states that from a run where two identical states satisfy the same subformulas of ϕ, one can obtain a new run which consists of a finite “prefix” and a period which is repeated.

Now we continue to the theorem which our upper bound result is based upon. It is a variant of “Ultimately Periodic Model Theorem” [SC85].

Theorem 8. Given a system s, η_{s} a valuation, σ a run of s, and ϕ a formula of L(X, U, S) such that (σ, 0) ⊧ ϕ, then

1) if |σ| < ∞, then there exists a run γ of s such that |γ| ≤ B^{q(|s|)}2^{|ϕ|} and (γ, 0) ⊧ ϕ.

2) if |σ| = ∞, then there exists a run γ = w_{0} → w_{1} → ⋯ and indices 0 ≤ i ≤ B^{q(|s|)}2^{|ϕ|}, 0 < p ≤ |ϕ|B^{q(|s|)}2^{|ϕ|} such that w_{l} = w_{l+p} for l ≥ i and (γ, 0) ⊧ ϕ.

where B and q(n) were described in Sect. 2.1.

Proof. We only consider the case where σ is infinite. The other case can be handled similarly. So assume (σ, 0) ⊧ ϕ. Since s has at most B^{q(|s|)} states and ϕ has at most 2^{|ϕ|} subformulas there must exist indices i < j such that

i) v_{i} = v_{j}, Sub(σ, i, ϕ) = Sub(σ, j, ϕ), and for all ϕ_{1}Uϕ_{2} ∈ Sub(σ, i, ϕ), ϕ_{2} is fulfilled between i and j.

Now applying Lemma 6 repeatedly to the initial part of σ we obtain a new run σ′ and indices i′ < j′ such that

ii) (σ′, 0) ⊧ ϕ, v′_{i′} = v′_{j′}, Sub(σ, i, ϕ) = Sub(σ′, i′, ϕ) = Sub(σ′, j′, ϕ), i′ ≤ B^{q(|s|)}2^{|ϕ|}, and for all ϕ_{1}Uϕ_{2} ∈ Sub(σ′, i′, ϕ), ϕ_{2} is fulfilled between i′ and j′.

Also, repeatedly applying Lemma 6 between v′_{i′} and v′_{j′} we can assume that (j′ − i′) ≤ |ϕ|B^{q(|s|)}2^{|ϕ|}; if at any time during the application of Lemma 6 the current value of (j′ − i′) is larger than |ϕ|B^{q(|s|)}2^{|ϕ|}, there must exist more than |ϕ| identical states v′_{l} among v′_{i′+1}, …, v′_{j′} satisfying the same set Sub(σ′, l, ϕ) of formulas. Since ϕ has less then |ϕ| subformulas of the form ϕ_{1}Uϕ_{2}, we can remove a loop between two of these states and still have all such ϕ_{2}’s fulfilled between i′ and (the new value of) j′ (in the resulting new run). We therefore conclude that there exists a run σ′′ of s and indices i′′ < j′′ such that

iii) (σ′′, 0) ⊧ ϕ, v′′_{i′′} = v′′_{j′′}, Sub(σ′′, i′′, ϕ) = Sub(σ′′, j′′, ϕ), i′′ ≤ B^{q(|s|)}2^{|ϕ|}, (j′′ − i′′) ≤ |ϕ|B^{q(|s|)}2^{|ϕ|}, and for all ϕ_{1}Uϕ_{2} ∈ Sub(σ′′, i′′, ϕ), ϕ_{2} is fulfilled between i′′ and j′′.

Using Lemma 7 we conclude that the run γ = v′′_{0} → ⋯ → v′′_{i′′} → ⋯ → v′′_{j′′} → v′′_{i′′+1} → ⋯ → v′′_{j′′} → ⋯ of s has the property (γ, 0) ⊧ ϕ. ⊓ ⊔

Theorem 9. Fix any class of compact systems (C, M_{C}) and set of atomic propositions A. Then, the model checking problem for L(X, U, S) is in PSPACE.

Proof. We shall describe an algorithm in a Pascal like programming language which given any instance (s, T_{η_{s}}, ϕ) of the model checking problem for L(X,U,S) solves it using only an amount of space polynomial in the sum |s| + |T_{η_{s}}| + |ϕ|. Let n denote this sum. Henceforth, whenever we write polynomial, we implicitly mean polynomial in n. The algorithm can be encoded as a nondeterministic polynomial space bounded Turing machine.

Notice that given possible configurations v and v′ of M_{C} run on input s, there are polynomial space bounded nondeterministic Turing machines which decide properties such as whether or not v ∈ V_{s}, v → v′ given v ∈ V_{s}, or v ↛. Moreover, we can also compute i_{s} given s using only a polynomial amount of space. For example, let us consider the case where we given v ∈ V_{s} and a possible configuration v′ have to decide if v → v′. Our nondeterministic Turing machine will simulate M_{C} from v. It guesses a number k_{1} ≤ B^{q(|s|)}. v′ is reachable from v if and only if it can be reached from v in at most B^{q(|s|)} computation steps of M_{C} (simulated on input s). Then, storing at most two new configurations of M_{C}, it guesses, one step at the time, a computation of M_{C} of length k_{1}. For each step it decrements k_{1} and checks if M_{C} can go from the old configuration to the new (guessed) configuration. Also, it checks that none of these intermediate configurations of M_{C} are signal configurations. Finally, if it reaches k_{1} = 0 it check that the guessed configuration equal v′ and is a signal configuration. It should be clear that this machine uses at most a polynomial amount of space. Now applying the technique from [HU79] Theorem 12.10, we obtain a deterministic polynomial space bounded Turing machine, since we can compute an exponential bound for the maximal number of configurations of the nondeterministic machine. Also, since η_{s}(p, v) can be computed in polynomial space by T_{η_{s}} this can also be done by simulating T_{η_{s}}.

Hence, in the algorithm we shall refer freely to the states of s and use the notation v → v′. Whenever a property is checked and is found not to hold, the algorithms fails. Let Sub(ϕ) be the set of subformulas of ϕ, let S range over subsets of Sub(ϕ), and let Un(ϕ) be the set {ϕ_{2} | ϕ_{1}Uϕ_{2} ∈ Sub(ϕ)}.

First we consider the case where the answer to (s, T_{η_{s}}, ϕ) is Yes because of an infinite run.

Algorithm 1a

01: Guess 0 ≤ n_{1} ≤ B^{q(|s|)}2^{|ϕ|} 02: Guess S_{current} ⊆ Sub(ϕ) 03: Let v_{current} = i_{s} 04: Check boolean consistency of S_{current} and v_{current}, i.e. that 05: (∀p ∈ Sub(ϕ). s ∈ S_{current} ⇔ η_{s}(p, v_{current})) 06: (∀ϕ_{1} ∧ ϕ_{2} ∈ Sub(ϕ). ϕ_{1} ∧ ϕ_{2} ∈ S_{current} ⇔ ϕ_{1} ∈ S_{current} and ϕ_{2} ∈ S_{current}) 07: (∀¬ϕ′ ∈ Sub(ϕ). ¬ϕ′ ∈ S_{current} ⇔ ϕ′ ∉ S_{current}) 08: Check that ϕ ∈ S_{current} 09: Check that (∀ϕ_{1}Sϕ_{2} ∈ Sub(ϕ). ϕ_{2} ∈ S_{current}) 10: Let count := 0 11: While count < n_{1} do 12: Guess a configuration v_{next} and check that v_{current} → v_{next} 13: Guess S_{next} ⊆ Sub(ϕ) 14: Check boolean consistency of S_{next} and v_{next} 15: Check that 16: (∀Xϕ′ ∈ Sub(ϕ). Xϕ′ ∈ S_{current} ⇔ ϕ′ ∈ S_{next}) 17: (∀ϕ_{1}Sϕ_{2} ∈ Sub(ϕ). ϕ_{1}Sϕ_{2} ∈ S_{next} ⇔

(ϕ_{2} ∈ S_{next} ∨ (ϕ_{1} ∈ S_{next} ∧ ϕ_{1}Sϕ_{2} ∈ S_{current})))

18: (∀ϕ_{1}Uϕ_{2} ∈ Sub(ϕ). ϕ_{1}Uϕ_{2} ∈ S_{current} ⇔

(ϕ_{2} ∈ S_{current} ∨ (ϕ_{1} ∈ S_{current} ∧ ϕ_{1}Uϕ_{2} ∈ S_{next})))

19: Let count := count + 1 20: Let v_{current} = v_{next} 21: Let S_{current} := S_{next} 22: Endwhile 23: Let v_{loop} := v_{current} 24: Let S_{loop} := S_{current} 25: Guess 0 ≤ n_{1} ≤ |ϕ|B^{q(|s|)}2^{|ϕ|} 26: Let count := 0 27: Let S_{U} := ∅ 28: While count < n_{1} do 29: (∗ Lines 29 to 38 are a copy of lines 12 to 21 ∗) 39: Let S_{U} := S_{U} ∪ (S_{current} ∩ Un(ϕ)) 40: Endwhile 41: Check that v_{current} = v_{loop} 42: Check that S_{current} = S_{loop} 43: Check that (∀ϕ_{1}Uϕ_{2} ∈ S_{loop}. ϕ_{2} ∈ S_{U}) 44: Answer Yes

For the case where the run is finite the following algorithm is derived:

Algorithm 1b

01: (∗ Lines 02 to 23 are a copy of lines 01 to 22 of Algorithm 1a ∗) 24: Check that v_{current} ↛ 25: Check that (∀ϕ_{1}Uϕ_{2} ∈ S_{current}. ϕ_{2} ∈ S_{current}) 26: Answer Yes

Our final algorithm chooses nondeterministically between Algorithm 1a and Algorithm 1b. The correctness of the algorithm is straightforward to establish; if the algorithm answers Yes, examine the guessed run of s, the values of S_{current} and S_{U}, and conclude that this run indeed shows that the answer to (s, T_{η_{s}}, ϕ) is Yes. Let σ′ denote the guessed run. Then, by induction in ϕ′ ∈ Sub(ϕ) show that for any of the values v_{current}(= v′_{j}) and S_{current}, (σ′, j) ⊧ ϕ′ ⇔ ϕ′ ∈ S_{current}; conversely, if the answer to (s, T_{η_{s}}, ϕ) is Yes then by Theorem 8 there exists a run of the algorithm which answers Yes.

I should be clear, from the assumptions about M_{C}, T_{η_{s}}, and the above comments about how to decide properties about the nodes and edges of (V_{s}, E_{s}) using only a polynomial amount of space, that this algorithm can be implemented by a nondeterministic polynomial space bounded Turing machine. By Savitch’s Theorem (NPSPACE = PSPACE) we conclude that the model checking problem for L(X, U, S) is in PSPACE. ⊓ ⊔

3.2 Branching Time

In this section we describe an algorithm which will solve the model checking problem for B(X, U) using only a polynomial amount of space.

We start by sketching the intuition behind our solution. We will describe our solution stepwise using Turing machines and results about the complexity of constructing and transforming such machines.

The idea behind our construction will be to construct a C-tape Turing machine M, where C is some constant. Denote these tapes by T_{1}, …, T_{C}. Given a problem instance as input M will, in polynomial time, construct a (description of a) deterministic polynomial space bounded machine M_{ϕ′} for each occurrence of a subformula^{4} ϕ′ of ϕ. Let us call these machines subformula machines.

The subformula machines have the extra ability that they may call certain subformula machines as subroutines. A machine M_{ϕ′} will call as subroutines the subformula machines corresponding to the immediate subformulas of ϕ′; e.g. M_{ϕ_{1}Uϕ_{2}} will call M_{ϕ_{1}} and M_{ϕ_{2}} as subroutines. These calls may be considered as single computation steps from the calling machines point of view much in the same way as Turing machines use oracles. M will simulate all of the subformula machines and their subroutine calls. Notice that M will need a stack of depth at most |ϕ| to simulate the subroutine call sequence. Figure 2 illustrates this.

[figure: (p ∧ q)U(¬q); p ∧ q; ¬q; p; q; q; M_{(p∧q)U(¬q)}; M_{p∧q}; M_{¬q}; M_{p}; M_{q}; M_{q}]

Fig. 2. Formula (p ∧ q)U(¬q) and the corresponding subformula machines. The arrows indicate which machines may be used as subroutines.

The subformula machines will be constructed in an bottom up fashion, i.e. when constructing M_{ϕ′}, all subformula machines corresponding to the proper

4 For convenience we shall use the same notation for both subformulas of and occurrences of subformulas of ϕ.

subformulas of ϕ′ have been constructed. The subformula machines will be stored on one of M’s tape using only a polynomial amount of tape. Each of these machines will compute the function f_{ϕ′} : V_{s} ⟶ 2, defined by f_{ϕ′}(v) =1 if and only if v ⊧ ϕ′. Since there are at most |ϕ| subformula occurrences in ϕ, say m, one of M’s C tapes, say T_{l}, will be used to simulate tapes for each of the machines M_{ϕ′}; assuming we have the m machines enumerated, the j’th machines tape will consist of all of T_{l}’s cells whose index i equals j modulo m. Figure 3 illustrates this for the case where there are three subformula occurrences. The j’th cell on a simulated tape is indicated by superscript j.

T_{l}: T_{ϕ_{1}}^{1}  T_{ϕ_{2}}^{1}  T_{ϕ_{3}}^{1}  T_{ϕ_{1}}^{2}  T_{ϕ_{2}}^{2}  T_{ϕ_{3}}^{2}  T_{ϕ_{1}}^{3}  T_{ϕ_{2}}^{3}
Fig. 3. T_{l} simulates 3 tapes: T_{ϕ_{1}}, T_{ϕ_{2}}, and T_{ϕ_{3}}.

Having constructed all the machines M_{ϕ′}, M then proceeds by giving M_{ϕ} the input i_{s} and starts simulating M_{ϕ}.

Theorem 10. Fix any class of compact systems (C, M_{C}) and set of atomic propositions A. Then, the model checking problem for B(X, U) is in PSPACE.

Proof. Given (s, T_{η_{s}}, ϕ). Let n denote the size of this problem instance. M is defined as follows:

– M stores its input (s, η_{s}, ϕ) on tape T_{1}.

– It enumerates all subformulas occurrences of ϕ and remembers how many there are. This is done on T_{2}.

Remark. Having found the number of subformula occurrences M will use T_{3} to simulate one tape T_{ϕ′} for each subformula occurrence ϕ′ as indicated in Fig.3.

– It now proceeds to construct the deterministic subformula machines as follows, starting with the smallest subformula occurrences. For a subformula occurrence ϕ′:

• If ϕ′ is an atomic proposition p, then M_{ϕ′} is the machine which given v computes uses T_{η_{s}} to compute η_{s}(p, v).

• If ϕ′ is of the form ¬ϕ′′, then M_{ϕ′} is the machine which given v calls M_{ϕ′′} as subroutine with v as parameter and returns the negated value obtained from M_{ϕ′′}.

• If ϕ′ is of the form ϕ_{1} ∧ ϕ_{2}, then M_{ϕ′} is the machine which given v first calls M_{ϕ_{1}} and then M_{ϕ_{2}}, remembering the values returned. It then returns 1 if and only if both values were 1.

• If ϕ′ is of the form EX(ϕ′′), then M first constructs a nondeterministic machine which does the following:

Given v it guesses v′, a possible configuration of s. Then it check that v → v′. Finally it calls M_{ϕ′′} with parameter v′. If the returned value is 1 it returns 1, else it returns 0.

Then, M constructs a deterministic version of this machine using e.g. a construction similar to the one sketched in [HU79] Theorem 12.10. This can be done since a (fully space constructible) polynomial bound on the space consumption of the nondeterministic machine can be computed. This machine will systematically examine all successor states of v and check if ϕ′′ holds at one of these states; if yes, then 1 is returned; if no, 0 is returned. This is the machine M_{ϕ′}.

• If ϕ′ is of the form AX(ϕ′′), then M first constructs a nondeterministic machine which does the following:

Given v it guesses v′, a possible configuration of s. Then it check that v → v′. Finally it calls M_{ϕ′′} with parameter v′. If the returned value is 0 it returns 0, else it returns 1.

Then, M constructs a deterministic version of this machine. This is the machine M_{ϕ′}.

• If ϕ′ is of the form E(ϕ_{1}Uϕ_{2}), then M first constructs a nondeterministic machine which does the following, given v:

Guess a number 0 ≤ k ≤ B^{q(|s|)} Let v_{current} := v While k > 0 do

Call M_{ϕ_{1}} to check that v_{current} ⊧ ϕ_{1} Guess v′, a possible state of s Check that v_{current} → v′ Let v_{current} := v′ Decrement k by 1

Endwhile Call M_{ϕ_{2}} to check that v_{current} ⊧ ϕ_{2}

If the machine reaches the last test and it is successful, the machine returns 1, else it returns 0.

Then, M constructs a deterministic version of this machine. This is the machine M_{ϕ′}.

• If ϕ′ is of the form A(ϕ_{1}Uϕ_{2}), then M first constructs a nondeterministic machine which does the following, given v:

It nondeterministically chooses to execute one of the following (nondeterministic) programs: a) Guess a number 0 ≤ k ≤ B^{q(|s|)}

Let v_{current} := v While k > 0 do

Call M_{ϕ_{1}} to check that v_{current} ⊧ ϕ_{1} Call M_{ϕ_{2}} to check that v_{current} |̸= ϕ_{2} Guess v′, a possible state of s Check that v_{current} → v′ Let v_{current} := v′ Decrement k by 1

Endwhile Check that either

v_{current} ↛ and v_{current} ⊧ ϕ_{1} (by calling M_{ϕ_{1}})and v_{current} |̸= ϕ_{2} (by calling M_{ϕ_{2}})

or v_{current} |̸= ϕ_{1} and v_{current} |̸= ϕ_{2}

If the machine reaches the last test and it was successful, the machine returns 0, else it returns 1.

b) Guess a number 0 ≤ k ≤ 2B^{q(|s|)} Guess a possible configuration v_{loop} Let b := 0 Let v_{current} := v While k > 0 do

If v_{current} = v_{loop} then let b := 1 Call M_{ϕ_{1}} to check that v_{current} ⊧ ϕ_{1} Call M_{ϕ_{2}} to check that v_{current} |̸= ϕ_{2} Guess v′, a possible state of s Check that v_{current} → v′ Let v_{current} := v′ Decrement k by 1

Endwhile Check that v_{current} = v_{loop} and that b = 1

If the machine reaches the last test and it was successful, the machine returns 0, else it returns 1.

Then, M constructs a deterministic version of this machine. This is the machine M_{ϕ′}.

Remark. Notice that all nondeterministic machines above always answer either 1 or 0, as do their deterministic versions. The algorithm for constructing the subformula machines is based on the observation that 1) if v ⊧ E(ϕ_{1}Uϕ_{2}), then there exists a path v_{0} → v_{1} → ⋯ → v_{k} starting at v such that (∀0 ≤ i < k. v_{i} ⊧ ϕ_{1}), v_{k} ⊧ ϕ_{2}, and 0 ≤ k ≤ B^{q(|s|)}; and 2) if v |̸= A(ϕ_{1}Aϕ_{2}), then 2a) there exists a path v_{0} → v_{1} → ⋯ → v_{k} starting at v such that (∀0 ≤ i < k. v_{i} ⊧ ϕ_{1} ∧ ¬ϕ_{2}), 0 ≤ k ≤ B^{q(|s|)}, and either (v_{k} ⊧ ¬ϕ_{1} ∧¬ϕ_{2}) or (v_{k} ↛ ∧ v_{k} ⊧ ϕ_{1} ∧¬ϕ_{2}); or 2b) there exists paths of the form v_{0} → ⋯ → v_{k_{1}} and v′_{0} → ⋯ → v′_{k_{2}} such that v_{0} = v, v_{k_{1}} = v′_{0} = v′_{k_{2}}, 0 ≤ k_{1}, k_{2} ≤ B^{q(|s|)}, and (∀0 ≤ j ≤ k_{1}. v_{j} ⊧ ϕ_{1} ∧ ¬ϕ_{2}) ∧ (∀0 ≤ j ≤ k_{2}. v′_{j} ⊧ ϕ_{1} ∧ ¬ϕ_{2}). By an induction argument one can show that the machine M_{ϕ′} indeed computes f_{ϕ′}.

– Having constructed all subformula machines, M starts simulating a call of M_{ϕ} given input v. This simulation will use at most polynomial space and the answer returned by M_{ϕ} is 1 if and only if i_{s} ⊧ ϕ. So M solves the model checking problem.

It remains to argue for the complexity of M. Any states of s can be stored in polynomial space. M_{C} and T_{η_{s}} are polynomial bounded space machines. which can be simulated by M in polynomial space. Properties about (V_{s}, E_{s}) can be decided in polynomial space, see the proof of Theorem 9. The subformula machines can be constructed in polynomial time and each of them use at most polynomial space. When simulating the subformula machines, M only needs a stack of depth at most |ϕ|, where for each waiting subroutine call, M only needs a polynomial amount of space. We therefore conclude that M solves the model checking problem for B(X, U) using only polynomial space. ⊓ ⊔

4 Example of an Application

In this section we define K-bounded nets and describe how they can be specified as a class of compact systems.

Definition 11. A K-bounded Place/ Transition net, or just a K-bounded net, is a tuple N = (P, T, F, M_{init})_{K} such that

– P and T are finite disjoint nonempty sets; their elements are called places and transitions, respectively.

– F ⊆ (P × T) ∪ (T × P); F is called the flow relation.

– M_{init}: P → {0, 1, 2 …, K} ⊆ IN; M_{init} is called the initial marking of N; in general, a mapping M: P → {0, 1, 2 …, K} ⊆ IN is called a marking of N. We shall use the notation p ∈ M if M(p) > 0.

Next, we define the behaviour of K-bounded Petri nets.

Definition 12. Given a K-bounded net N = (P, T, F, M_{init})_{K}.

– A transition t ∈ T is enabled at a marking M of N if M(p) > 0 for every place p in ^{•}t = {p | (p, t) ∈ F }, the preset of t, and M(p) < K for every place p in t^{•}\^{•}t, where t^{•} = {p | (t, p) ∈ F }, the postset of t. Henceforth, we shall assume that there are no isolated elements, i.e. (∀p ∈ P.^{•}p^{•} ≠) and (∀t ∈ T.^{•}t^{•} ≠).

– Given a transition t, we define a relation →^{t} between markings as follows: M →^{t} M′ if t is enabled at M and M′(s) = M(s) + F (t, s) − F (s, t), where F (x, y) is 1 if (x, y) ∈ F and 0 otherwise. The transition t is said to occur (or fire) at M. A marking M is a deadlock, denoted M ↛, if it enables no transitions.

– If M_{0} →^{t_{1}} M_{1} →^{t_{2}} ⋯ →^{t_{n}} M_{n} for some markings M_{0}, M_{1}, … M_{n}, then the

sequence σ = t_{1} … t_{n} is called an occurrence sequence from M_{0}. M_{n} is the marking reached by σ, and this is denoted M_{0} →^{σ} M_{n}. In general, we use the notation σ for a finite or infinite sequence of transitions and use the notation M_{0} →^{σ} to indicate that all finite prefixes of σ are occurrence sequences from M_{0}. Sometimes, the notation M_{0} →^{σ} is also used to denote the sequence

M_{0} →^{t_{1}} M_{1} →^{t_{1}} · · ·.

– An occurrence sequence σ from a marking M_{0} is maximal if it is either infinite or it is finite and reaches a deadlock.

– A marking M is reachable from M_{0} if it is the marking reached by some occurrence sequence from M_{0}. [M_{0}⟩ will denote the set of markings reachable from M_{0}. [M_{init}⟩ is the set of reachable markings of N.

– The reachability graph of N is the edge-labelled graph, (V_{N}, E_{N}), whose vertices are the reachable markings of N; if M →^{t} M′ for a reachable marking M, then there is an edge from M to M′ labelled t. Notice that N has at most (K + 1)^{|P |} markings.

Encoding a K-bounded net can be done along the lines of e.g. [HU79] Chap. 8.3. We choose the following encoding: The string s_{N} encodes (in binary) the number of places, the number of transitions, the pairs in F, and the initial marking. Without loss of generality, interpreting the atomic propositions A as places of K-bounded gives us a valuation η for all nets. η maps a pair consisting of an atomic proposition a and a place p to 1 if and only if the encoding of a equals the encoding of p. We therefore only need one T_{η} for the class of K-bounded Petri nets. Having one for each N would also be possible.

The machine M_{C} will do the following: First, it checks that the input string encodes a K-bounded net. Assume that the net described by the input has n places. Since N is assumed to have no isolated elements, the length of the input is at least n. Hence, M_{C} may then use n log K tape squares to store a marking (notice K is fixed for the class of K-bounded nets). So, it starts by storing the initial marking of the net. It then enters its signal state to signal that the configuration is a marking of the net. Then, it leaves the signal state, guesses a transition, and checks if it is enabled. If it is, M_{C} “fires” it by updating the stored marking accordingly. Having done that M_{C} enters the signal state, signaling that it has computed a new marking of the net. Then it continues as before; leaving the signal state, guessing a new transition to fire et.c. If the guessed transition is not enabled, M_{C} just halts. Notice that if s_{N} is the encoding of the K-bounded net N, then the state space of s_{N} is isomorphic to the reachability graph of N such that i_{s_{N}} corresponds to the initial marking of N.

Hence K-bounded Petri nets can be specified as a class of compact systems.

Theorem 13. The model checking problems for K-bounded Petri nets and the logics L(F), L(X, U, S) , and B(X, U) are PSPACE-complete.

Proof. Sketch: The PSPACE-hardness of the problem follows from the fact that the logics can express the reachability of a marking M in a 1-safe net [CEP93] (A 1-safe net has the property that it is K-bounded for any K ≥ 1). This can be done using an obvious formula linear in the size of P: ϕ ≡ F ((⋀_{p∈M} p) ∧ (⋀_{p∉M} ¬p)). Actually, along the lines in [CEP93] one can prove that for a given 1-safe net N and a place p of N, the problem of deciding whether or not there exists a reachable marking M such that p ∈ M (M(p) = 1) is PSPACE-complete. Since this is expressed by the formula F (p), model checking any reasonable propositional branching time temporal logic must be PSPACE-hard.

Since L(F) is a fragment of L(X, U, S) (F (ϕ) is short for t Uϕ), Theorem 9 and Theorem 10 give us the matching PSPACE upper bounds. ⊓ ⊔

5 Conclusion

We have provided algorithms which give us an upper bound on the complexity of the model checking problem for a well known class of basic temporal logics interpreted over any class of compact systems, i.e. any class of systems satisfying certain conditions which limits the “succinctness” of their description; their associated state graphs must at most be exponentially larger than the models themselves.

Our results gave an upper bound for both L(X, U, S) and CTL. As an application of our results, we showed in Sect. 4 that the model checking problems for L(F), L(X, U, S) , and B(X, U) over K-bounded nets are PSPACE-complete.

For a net N known to be bounded, that is one only knows that there exists a K such that N is K-bounded, storing any reachable marking would require exponential space in the worst case. We claim similar lower bounds hold for other nontrivial classes of compact systems. In general, we cannot give a PSPACEhardness lower bound for a class of compact systems; R-structures are a trivial class of compact systems which doesn’t have this lower bound for e.g. L(F).

Future research should investigate temporal logics containing and combining other operators than the ones considered here. Also, the same approach is applicable if e.g. compact systems are defined such that M_{C} is exponential space bounded, i.e. the systems s describe a double exponentially large state space. One would then get EXPSPACE upper bounds.

References

[BCM^{+}92] J. R. Bruch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10^{20} states and beyond. Information and Computation, 98:142–170, 1992.

[CEP93] Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1safe nets. In Proc. FST&TCS 13, Thirteenth Conference on the Foundations of Software Technology & Theoretical Computer Science, pages 326–337. Springer-Verlag (LNCS 761), Bombay, India, December 1993. To appear in TCS, volume 148.

[CES86] Edmund M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent system using temporal logic. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.

[Eme90] E. Allen Emerson. Temporal and Modal Logic, chapter 16. Elsevier Science Publishers, 1990. in Handbook Of Theoretical Computer Science, editor J. van Leeuwen.

[ES92] Javier Esparza and Manuel Silva. A polynomial-time algorithm to decide liveness of bounded free choice nets. Theoretical Computer Science, 102:185–205, 1992.

[Esp93] Javier Esparza. Model checking using net unfoldings. In Proc. TAP-SOFT’93, pages 613–628. Springer-Verlag (LNCS 668), 1993. Full version to appear in Science of Computer Programming.

[HU79] John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979.

[JLL77] Neil D. Jones, Lawrence H. Landweber, and Y. Edmund Lien. Complexity of some problems in Petri nets. Theoretical Computer Science, 4:277–299, 1977.

[Lam80] Leslie Lamport. “Not never” – on the Temporal Logic of programs. Proc. 7th Ann. ACM Symp. on Princples of Programming Languages, pages 174– 185, 1980.

[Lar88] Kim G. Larsen. Proof systems for Hennessy-Milner logic with recursion. In Proceedings of CAAP, Nancy France, pages 215–230. Springer-Verlag (LNCS 299), March 1988.

[Mil89] Robin Milner. Communication and Concurrency. Prentice Hall International Series In Computer Science, C. A. R. Hoare series editor, 1989.

[SC85] A. P. Sistla and E. M. Clarke. The complexity of Propositional Linear Temporal Logic. Journal of the ACM, 32(3):733–749, 1985.

[SW89] Colin P. Stirling and David Walker. Local model checking in the modal mu-calculus. Technical Report ECS–LFCS–89–78, Laboratory for Foundations of Computer Science, Department of Computer Science – University of Edinburgh, May 1989.

[Val90] Antti Valmari. Stubborn sets for reduced state space generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1990, pages 491–515. Springer-Verlag (LNCS 483), 1990.

[WG93] Pierre Wolper and Patrice Godefroid. Partial-order methods for temporal verification. Technical report, Université de Liège, Institut Montefiore, August 1993. Wolper-1, Hand-outs at Summerschool in Logical Methods In Concurrency Aarhus’93, To appear in: Concur’93 Proceedings.

This article was processed using the LaTEX macro package with LLNCS style

Recent Publications in the BRICS Report Series

RS-95-18 Allan Cheng. Complexity Results for Model Checking. February 1995. 18pp.

RS-95-17 Jari Koistinen, Nils Klarlund, and Michael I. Schwartzbach. Design Architectures through Category Constraints. February 1995. 19 pp.

RS-95-16 Dany Breslauer and Ramesh Hariharan. Optimal Parallel Construction of Minimal Suf�x and Factor Automata. February 1995. 9 pp.

RS-95-15 Devdatt P. Dubhashi, Grammati E. Pantziou, Paul G. Spirakis, and Christos D. Zaroliagis. The Fourth Moment in Luby’s Distribution. February 1995. 10 pp.

RS-95-14 Devdatt P. Dubhashi. Inclusion�Exclusion(3) Implies Inclusion�Exclusion(n). February 1995. 6 pp.

RS-95-13 Torben Bra� uner. The Girard Translation Extended with Recursion. 1995. Full version of paper to appear in Proceedings of CSL ’94, LNCS.

RS-95-12 Gerth St�lting Brodal. Fast Meldable Priority Queues. February 1995. 12 pp.

RS-95-11 Alberto Apostolico and Dany Breslauer. An Optimal O(log log n) Time Parallel Algorithm for Detecting all Squares in a String. February 1995. 18 pp. To appear in SIAM Journal on Computing.

RS-95-10 Dany Breslauer and Devdatt P. Dubhashi. Transforming Comparison Model Lower Bounds to the Parallel-Random-Access-Machine. February 1995. 11 pp.

RS-95-9 Lars R. Knudsen. Partial and Higher Order Differentials and Applications to the DES. February 1995. 24 pp.

RS-95-8 Ole I. Hougaard, Michael I. Schwartzbach, and Hosein Askari. Type Inference of Turbo Pascal. February 1995. 19 pp.

RS-95-7 David A. Basin and Nils Klarlund. Hardware Veri�cation using Monadic Second-Order Logic. January 1995. 13 pp.