**D Harel, D. Kozen and J. Tiuryn,
***Dynamic Logic, * MIT Press, 2000.
**Table of Contents**
**Part I: Fundamental Concepts **
**1. Mathematical Preliminaries ** 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. Computability and Complexity**
2.1 Machine Models
2.2 Complexity Classes
2.3 Reducibility and Completeness
2.4 Bibliographical Notes
2.5 Exercises
**3. Logic**
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. Reasoning About Programs**
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. 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. Basic Properties**
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. 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. Relationships with Static Logics**
13.1 The Uninterpreted Level
13.2 The Interpreted Level
13.3 Bibliographical Notes
13.4 Exercises
**14. Complexity**
14.1 The Validity Problem
14.2 Spectral Complexity
14.3 Bibliographical Notes
14.4 Exercises
**15. Axiomatization**
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. Variants of DL**
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 |