Temporal logic of programs. (English) Zbl 0609.03007

Kröger, Fred

EATCS Monographs on Theoretical Computer Science, Vol. 8. Berlin etc.: Springer-Verlag. VIII, 148 p.; DM 68.00 (1987).

Temporal logic has become an indispensable tool in reasoning about the behavior of programs since the pioneering work of A. Pnueli [Proc. 18th Ann. Symp. Foundations of Computer Science, Providence, RI. New York (1977)]. This interesting monograph is intended for an introduction to this vital area, assuming only modest familiarity with the fundamental concepts of mathematical logic. The monograph consists of seven chapters, the first three of which deal with the pure (linear time) temporal logic. Chapter 4 is devoted to representing programs and their properties within this formalism. Chapter 5 treats the invariance and precedence properties of programs, while the succeeding chapter is devoted to the eventuality properties of programs. The final chapter discusses two special methods of sequential programs from a standpoint of temporal logic.

Reviewer: H.Nishimura

MSC:

03B70	Logic in computer science
68Q65	Abstract data types; algebraic specification
68Q60	Specification and verification (program logics, model checking, etc.)
03-02	Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
68-02	Research exposition (monographs, survey articles) pertaining to computer science
03-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
68-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science

Keywords:

invariance property; precedence property; reasoning about the behavior of programs; eventuality properties of programs; sequential programs