The book contains the author’s lectures given at Stanford University in 1986 on modal logic with emphasis on temporal and dynamic logics. It is divided into three parts. Part 1 deals with normal modal and temporal propositional logics; it covers the canonical model construction used for completeness and the filtration method for decidability. Part 2 applies the theory to logics of discrete, dense, and continuous time with emphasis on concurrent and regular programs. The last part deals with first-order dynamic logic and focuses on the relationship between the processes of assignment of a variable (dynamic) and substitution for a variable (static). A completeness result is obtained.

The exercises form an integral part of the text. The material is presented in an attractive and original manner. The book could readily serve as a text for a course on modal logic in theoretical computer science.