×

Verifying temporal properties of systems. (English) Zbl 0753.68065

Progress in Theoretical Computer Science. Boston, MA etc.: Birkhäuser. viii, 113 p. (1992).
This monograph is concerned with the verification of infinite systems. The approach is based on the idea of model-checking, a recent alternative to proving properties of systems by means of logical reasoning. The idea of model-checking is to consider some system as a model for some logic, and check whether the model satisfies a given formula of the logic expressing some property. Model-checking, at least in my opinion, is a very promising and effective approach to verify systems. The monograph is the first one introducing the topic in a very concise, sufficiently formal, and readable manner. Even more, the author brings together the ideas of finite, algorithmic, model-checking and the ability to perform proofs. This mixture of automatic checking and proof requiring intelligence seems to be essential for general infinite systems and makes the method suitable for computer assisted verification.
The technique used for model-checking is a tableau method, based on the logic of the propositional modal mu-calculus. In chapter 2, the author introduces the modal mu-calculus, particularly focusing on the fixed point operators. Chapter 3 is the main body of the book, in which a tableau system for infinite state model-checking is developed. Soundness and completeness are proven and various variants of the system are considered. In chapter 4, application to concurrent systems in the form of Petri nets is considered. Chapter 5 then discusses the complexity of mu-formulae on nets.
The book will be of particular interest to those concerned with formal verification of systems. The book is accessible to advanced graduate students as well as researchers.
Reviewer: L.S.Brim (Brno)

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
PDFBibTeX XMLCite