D Harel, D. Kozen and J. Tiuryn, Dynamic Logic, MIT Press, 2000.

Table of Contents Preface ~ Order Info. from Amazon ~ Order Info. from Barnes and Noble

Table of Contents

Part I: Fundamental Concepts

1.1 Notational Conventions
1.2 Sets
1.3 Relations
1.4 Graphs and Dags
1.5 Lattices
1.6 Transfinite Ordinals
1.7 Set Operators
1.8 Bibliographical Notes
1.9 Exercises

2.1 Machine Models
2.2 Complexity Classes
2.3 Reducibility and Completeness
2.4 Bibliographical Notes
2.5 Exercises

3.1 What is Logic?
3.2 Propositional Logic
3.3 Equational Logic
3.4 Predicate Logic
3.5 Ehrenfeucht-Fraisse Games
3.6 Infinitary Logic
3.7 Modal Logic
3.8 Bibliographical Notes
3.9 Exercises

4.1 States and Executions
4.2 Programs
4.3 Program Verification
4.4 Exogenous and Endogenous Logics
4.5 Bibliographical Notes
4.6 Exercises

Part II: Propositional Dynamic Logic

5.1 Syntax
5.2 Semantics
5.3 Computation Sequences
5.4 Satisfiability and Validity
5.5 A Deductive System
5.6 Bibliographical Notes
5.7 Exercises

6.1 Properties Inherited from Modal Logic
6.2 Properties of U,`,-,?
6.3 The * Operator
6.4 Hoare Logic
6.5 Bibliographical Notes 6.6 Exercises

7. Filtration and Decidability

7.1 The Fischer-Ladner Closure
7.2 Filtration and the Small Model Theorem
7.3 Filtration over Nonstandard Models
7.4 Bibliographical Notes
7.5 Exercises

8. Deductive Completeness

8.1 Deductive Completeness
8.2 Logical Consequences
8.3 Bibliographical Notes
8.4 Exercises

9. Complexity of PDL

9.1 A Deterministic EXPTIME Algorithm
9.2 A Lower Bound
9.3 Logical Consequences
9.4 Bibliographical Notes
9.5 Exercises

10. Nonregular PDL

10.1 Context-Free Programs
10.2 Basic Results
10.3 Undecidable Extensions
10.4 Decidable Extensions
10.5 Finite Model Property for One-Letter Programs
10.6 Bibliographical Notes
10.7 Exercises

11. Other Variants of PDL

11.1 Deterministic PDL and While Programs
11.2 Restricted Tests
11.3 Representations by Automata
11.4 Complementation and Intersection
11.5 Converse
11.6 Well-Foundedness and Total Correctness
11.7 Concurrency and Communication
11.8 Bibliographical Notes

Part III: First-Order Dynamic Logic

12.1 Basic Syntax
12.2 Richer Programs
12.3 Semantics
12.4 Satisfiability and Validity
12.5 Bibliographical Notes
12.6 Exercises

13.1 The Uninterpreted Level
13.2 The Interpreted Level
13.3 Bibliographical Notes
13.4 Exercises

14.1 The Validity Problem
14.2 Spectral Complexity
14.3 Bibliographical Notes
14.4 Exercises

15.1 Uninterpreted Systems
15.2 Interpreted Systems
15.3 Bibliographical Notes
15.4 Exercises

16. Expressive Power

16.1 The Unwind Property
16.2 Spectra and Expressive Power
16.3 Bounded Nondeterminism
16.4 Unbounded Memory
16.5 The Power of Boolean Stack
16.6 Unbounded Nondeterminism
16.7 Bibliographical Notes
16.8 Exercises

17.1 Algorithmic Logic
17.2 Nonstandard Dynamic Logic
17.3 Well-Foundedness
17.4 Dynamic Algebra
17.5 Probabilistic Programs
17.6 Concurrency and Communication
17.7 Intuitionistic Dynamic Logic
17.8 Bibliographical Notes

18. Other Approaches

18.1 Logic of Effective Definitions
18.2 Temporal Logic
18.3 Process Logic
18.4 The mu-Calculus

Bibliography

Index

Back to Top

Preface

Dynamic Logic is a formal system for reasoning about programs. Traditionally, this has meant formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other activities fall into this category as well: determining the equivalence of programs, comparing the expressive power of various programming constructs, synthesizing programs from specifications, etc. Formal systems too numerous to mention have been proposed for these purposes, each with its own peculiarities.

This book presents a comprehensive introduction to one system, or rather family of systems, collectively called Dynamic Logic (DL). Among the myriad approaches to formal reasoning about programs, DL enjoys the singular advantage of strong connections with classical logic. It can be described as a blend of three complementary classical ingredients: propositional and predicate logic, modal logic, and the algebra of regular events. These components merge to form a system of remarkable unity that is theoretically rich as well as practical.

The name Dynamic Logic emphasizes the principal feature distinguishing it from classical predicate logic. In the latter, truth is static: the truth value of a formula is determined by a valuation of its free variables over some structure. The valuation and the truth value of it induces are regarded as immutable; there is no formalism relating them to any other valuations or truth values. In Dynamic Logic, there are explicit syntactic constructs called programs, whose main role is to change the values of variables, thereby changing the truth values of formulas. For example, the program x:=x+1 over the natural numbers changes the truth value of the formula "x is even".

Such changes occur on a metalogical level in classical predicate logic. For example, in the Tarski definition of a formula, if u:{x,y,...} -> N is a valuation of variables over the natural numbers N, then the formula existsx x**2=y is defined to be true under the valuation u iff there exists an a in N such that the formula x**2=y is true under the valuation u[x/a], where u[x/a] agrees with u everywhere except x, on which it takes the value a. This definition involves a metalogical operation which produces u[x/a], from u for all possible values a in N. This operation becomes explicit in Dynamic Logic in the form of the program x:=?, called a nondeterministic or wildcard assignment. This is a rather unconventional program, since it is not effective; however, it is quite useful as a descriptive tool. A more conventional way to obtain a square root of y, if it exists, would be the program

x:=0; while x**2 < y do x:=x+1. (1)

In Dynamic Logic, such programs are first-class objects on a par with formulas, complete with a collection of operators for forming compound programs inductively from a basis of primitive programs. In the simplest version of DL, these program operators are U (nondeterministic choice), ; (sequential composition), * (iteration), and ? (test). These operators are already sufficient to generate all while programs, which over N are sufficient to compute all partial recursive functions. To discuss the effect of the execution of a program on the truth of a formula , DL uses a modal construct that states, "It is possible to execute and halt in a state satisfying .

This book is divided into three parts. Part I reviews the fundamental concepts of logic and computability theory that are needed in the study of Dynamic Logic. Part II discusses Propositional Dynamic Logic and its variants, and Part III discusses First-Order Dynamic Logic and its variants. Examples are provided throughout, and a collection of exercises and a short historical section are included at the end of each chapter.

Part I was included in an effort to achieve a certain level of self-containment, although the level achieved is far from absolute, since DL draws on too many disciplines to cover adequately. The treatment of some topics in Part I is therefore necessarily abbreviated, and a passing familiarity with the basic concepts of mathematical logic, computability, formal languages and automata, and program verification is a desirable prerequisite. This background material can be found in Shoenfield [185] (logic), Rogers [174] (recursion theory), Kozen [118] (formal languages, automata, and computability), Keisler [99] (infinitary logic), Manna [127] (program verification), and Harel [] (computability and complexity).

Apart from the obvious heavy reliance on classical logic, computability theory and programming, the subject has its roots in the work of Thiele [198] and Engeler [42] in the late 1960's, who were the first to advance the idea of formulating and investigating formal systems dealing with properties of programs in an abstract setting. Research in program verification flourished thereafter with the work of many researchers, notably Floyd [50], Hoare [92], Manna [127], and Salwicki [179]. The first precise development of a Dynamic Logic-like system was carried out by Salwicki [179], following Engeler [42]. This system was called Algorithmic Logic. A similar system, called Monadic Programming Logic, was developed by Constable [?]. Dynamic Logic, which emphasizes the modal nature of the program/assertion interaction, was introduced by Pratt in 1976 [162].

There are by now a number of books and survey papers treating logics of programs and Dynamic Logic. We refer the reader to [70,71,150,56,57,106,31,36,117].

The material of this book has been used as the basis for graduate courses at the Weizmann Institute of Science, Bar-Ilan University, Aarhus University, Waraw University, and Cornell University.

We welcome comments and criticism from readers.

Back to Top