This book was written to support a short course in the second or third year of an undergraduate computer science, software engineering, or software design program. The prerequisites are fairly modest: some programming experience (ideally in C or C++ or a related language such as JAVA) and some exposure to the most basic concepts of discrete mathematics (sets, functions, binary relations, sequences) and to the language of elementary logic (connectives and quantifiers). It is intended to be only an introduction to software specifications, not a systematic survey of requirements engineering, formal methods, compilers, or computation theory suitable for a senior or graduate-level course. A course based on this book would provide a good foundation for such courses but should not replace them.

The contents may be summarized briefly as follows:

• specification, verification, and development of simple algorithms using pre- and post-conditions and loop invariants;

• specification, verification, and development of simple data representations using abstract models and representation invariants; and

• specification and systematic development of recognizers for formal languages using regular expressions, grammars, and automata.

These techniques have been well studied and are sound and useful. They may be presented to and immediately used by undergraduate students on simple but nontrivial examples. They may be taught without requiring upper-level prerequisites or major investments of time to teach complex notations or computer-based tools. But such material is not often presented at this level, nor in this combination.

We now consider specification and construction techniques tailored to a particular application domain: code that is intended to test whether arbitrary input strings may be matched by a specific “pattern.” The pattern itself is essentially the specification for such a program, and a variety of specialized notations and implementation techniques have been developed to allow convenient expression and realization of such specifications. Although the methods are specialized to the application, the key principles of formal methods—distinguishing between specification and realization, adopting appropriate formalized notation for specifications, and using systematic or verifiable methods of program construction—are still relevant. Chapter 7 introduces the basic concepts, and Chapters 8 to 11 discuss various styles of pattern specification and how they may be systematically transformed and realized.

Additional Reading

Many books cover this material, usually from either a primarily theoretical perspective [HU79, MAK88, LP98] or a compiler-oriented one [ASU86]; [Gou88, AU92, HMU01] are closest to the approach adopted here.

It may not be possible to implement a specification. The requirements may be inconsistent, the specification may be meaningless or ill-defined, or, surprisingly, the function specified may not be computable. The concept of an incomputable function comes from computability theory, a branch of mathematical logic with particular relevance to computer science.

Chapter 12 introduces some of the key ideas of computability theory, both as motivation for subsequent study and to provide the background necessary to appreciate the significance of an incomputability claim. In particular, we will prove that some functions are not computable by any C program, explain why such problems are deemed to be algorithmically unsolvable, and list a number of unsolvable problems of practical importance involving context-free grammars.

Additional Reading

Good presentations of elementary computability theory may be found in [RS86, Sip97, Jon97, GH98, LP98, HMU01].

Case Study: Searching an Array

Professor Higgins wants his programmer, Eliza Doolittle, to write a code fragment that is to test for the presence or absence of a value x in an array A. Here is the intended application: A is to contain the student numbers of all the students currently enrolled in his course on computational metaphysics, and x might be the student number of a student who is trying to verify that he or she is properly registered.

Exercise 1.1 Before reading on, pretend that you are Eliza Doolittle and try to write the desired code. Also, try to write an application program that uses the code.

As you will quickly discover if you try to write the desired code, or to write a program to use it, the preceding paragraph is an inadequate specification. Here are some of the questions that must be answered before (or during) the development of the desired code or any associated applications.

1. What is the range of allowed subscript values for A, and what segment of the array should be searched?

2. What is the type of variable x (also, presumably, the component type of the array), and how should values of this type be compared?

3. How should the result be recorded?

4. Is the array segment sorted in, say, ascending order, to allow use of a more efficient search method?

5. […]

In Section 1.3 we defined what it means for a formula to be satisfied at a state in a model — but as yet we know virtually nothing about this fundamental semantic notion. What exactly can we say about models when we use modal languages to describe them? Which properties of models can modal languages express, and which lie beyond their reach?

In this chapter we examine such questions in detail. We introduce disjoint unions, generated submodels, bounded morphisms, and ultrafilter extensions, the ‘big four’ operations on models that leave modal satisfaction unaffected. We discuss two ways to obtain finite models and show that modal languages have the finite model property. Moreover, we define the standard translation of modal logic into first-order logic, thus opening the door to correspondence theory, the systematic study of the relationship between modal and classical logic. All this material plays a fundamental role in later work; indeed, the basic track sections in this chapter are among the most important in the book.

But the central concept of the chapter is that of a bisimulation between two models. Bisimulations reflect, in a particularly simple and direct way, the locality of the modal satisfaction definition. We introduce them early on, and they gradually come to dominate our discussion. By the end of the chapter we will have a good understanding of modal expressivity over models, and the most interesting results all hinge on bisimulations.

As we saw in Section 1.3, the concept of validity, which abstracts away from the effects of particular valuations, allows modal languages to get to grips with frame structure. As we will now see, this makes it possible for modal languages to define classes of frames, and most of the chapter is devoted to exploring this idea.

The following picture will emerge. Viewed as tools for defining frames, every modal formula corresponds to a second-order formula. Although this second-order formula sometimes has a first-order equivalent, even quite simple modal formulas can define classes of frames that no first-order formula can. In spite of this, there are extremely simple first-order definable frame classes which no modal formula can define. In short, viewed as frame description languages, modal languages exhibit an unusual blend of first- and second-order expressive powers.

The chapter has three main parts. The first, consisting of the first four sections, introduces frame definability, explains why it is intrinsically second-order, presents the four fundamental frame constructions and states the Goldblatt-Thomason Theorem, and discusses finite frames. The second part, consisting of the next three sections, is essentially a detailed exposition of the Sahlqvist Correspondence Theorem, which identifies a large class of modal formulas which correspond to first-order formulas. The final part, consisting of the last section, studies further frame constructions and gives a model-theoretic proof of the Goldblatt-Thomason Theorem. With the exception of the last two sections, all the material in this chapter lies on the basic track.

In this appendix we review some basic (universal) algebraic notions used in Chapter 5. The first part deals with algebras and operations on (classes of) algebras, the second part is about algebraic model theory, and in the third part we discuss equational logic. Birkhoff's fundamental theorems are stated without proof.

For an introduction to universal algebra, see Burris and Sankappanavar [81] or Grätzer [198]; McKenzie, McNulty and Taylor [321] provide more comprehensive reading. Basic track readers may like the algebraic accounts of propositional logic given in Chapter 3 of Bell and Machover [32] and Chapters 1 and 2 of Bell and Slomson [33]. Many readers will find Davey and Priestly [105] useful supplementary reading.

Universal Algebra

An algebra is a set together with a collection of functions over the set; these functions are usually called operations. Algebras come in various similarity types, determined by the number and arity of the operations.

Definition B.1 (Similarity Type) An algebraic similarity type is an ordered pair ƒ = (F, ρ) where F is a non-empty set and ρ is a function F → ℕ. Elements of F are called function symbols; the function ρ assigns to each operator f ∈ F a finite arity or rank, indicating the number of arguments that f can be applied to.

Ask three modal logicians what modal logic is, and you are likely to get at least three different answers. The authors of this book are no exception, so we will not try to start off with a neat definition. Nonetheless, a number of general ideas guide our thinking about the subject, and we will present the most important right away as a series of three slogans. These are meant to be read now, and, perhaps more importantly, referred back to occasionally; doing so will help you obtain a firm grasp of the ideas and intuitions that have shaped this book. Following the slogans we will discuss the aims and content of the book in more detail.

Our first slogan is the simplest and most fundamental. It sets the basic theme on which the others elaborate:

Slogan 1: Modal languages are simple yet expressive languages for talking about relational structures.

In this book we will be examining various propositional modal languages: that is, the familiar language of propositional logic augmented by a collection of modal operators. Like the familiar boolean connectives (¬ ∧, ∨, →, ⊥, and ⊤), modal operators do not bind variables. Thus, as far as syntax is concerned, we will be working with the simplest non-trivial languages imaginable.

But in spite of their simplicity, propositional modal languages turn out to be an excellent way of talking about relational structures, and this book is essentially an attempt to map out some of the ramifications of this.

This chapter is about the completeness — and incompleteness — of normal modal logics. As we saw in Section 1.6, normal modal logics are collections of formulas satisfying certain simple closure conditions. They can be specified either syntactically or semantically, and this gives rise to the questions which dominate the chapter: Given a semantically specified logic, can we give it a syntactic characterization, and if so, how? And: Given a syntactically specified logic, can we give it a semantic characterization (and in particular, a characterization in terms of frames), and if so, how? To answer either type of question we need to know how to prove (soundness and) completeness theorems, and the bulk of the chapter is devoted to developing techniques for doing so.

The chapter has two major parts. The first, comprising the first four sections, is an introduction to basic completeness theory. It introduces canonical models, explains and applies the completeness-via-canonicity proof technique, discusses the Sahlqvist Completeness Theorem, and proves two fundamental limitative results. The material introduced in these sections (which are all on the basic track) is needed to follow the second part and the algebraic investigations of Chapter 5.

In the second part of the chapter we turn to the following question: what are we to do when canonicity fails? (As will become clear, canonicity failure is a fact of life for temporal logic, propositional dynamic logic, and other applied modal languages.)

Here we list and briefly describe a number of textbooks, survey articles, and more specialized books which the reader may find useful. We have not aimed for comprehensive coverage. Rather, we have commented on the sources the reader is most likely to run into, provided pointers to topics not discussed in this book (in particular, modal proof theory and theorem proving, and first-order modal logic) and drawn attention to some interesting emerging themes.

This is a good place to mention the Advances in Modal Logic initiative, which attempts to bring together scholars working in various areas of modal logic and its applications. You can find out more at: http://www.aiml.net. The collection Advances in Modal Logic, Volume 1, edited by Kracht et al. [281], contains a selection of papers from the first conference hosted by the initiative. Selections from later workshops have also been published; see Advances in Modal Logic, Volume 2, edited by Zakharyaschev et al. [469]; Advances in Modal Logic, Volume 3, edited by Wolter et al. [461]; and Advances in Modal Logic, Volume 4, edited by Balbiani et al. [18].

Textbooks on Modal Logic

To start, here is an annotated list of textbooks on modal logic.

ο A Manual of Intensional Logic, van Benthem [44]. What is modal logic? What is not! This inspiring little book takes the reader on a whirlwind tour of the many faces of modal logic.

In this chapter we investigate the computability and complexity of normal modal logics. In particular, we examine the computability of satisfiability problems (given a modal formula ø and a class of models M, is it computable whether ø is M-satisfiable?) and validity problems (given a modal formula ø and a class of models M, is it computable whether ø is valid on M?). When the answer is ‘yes’, we probe further: how complex is the problem — in particular, what resources of time (that is, computation steps) or space (that is, memory) are needed to carry out the required computations? When the answer is ‘no’, we pose a similar question: how uncomputable is the problem? There are vast differences in the complexities of modal satisfiability problems: some are no worse than the satisfiability problem for propositional calculus, while others are highly undecidable.

This chapter has two main parts. The first, consisting of the five sections on the basic track, introduces the basic ideas and discusses modal (un-)decidability. Three techniques for proving decidability are discussed (finite models, interpretations in monadic second-order theories of trees, and quasi-models and mosaics) and undecidability is approached via tiling problems. In the second part, consisting of the last three sections of the chapter, we examine the complexity of some key modal satisfiability problems. These sections are on the advanced track, but the initial part of each of them should be accessible to all readers.