zbMATH — the first resource for mathematics

The temporal logic of reactive and concurrent systems. Specification. (English) Zbl 0753.68003
Berlin etc.: Springer-Verlag. XIV, 427 p. (1991).
This volume, the first of two, is a comprehensive and self-contained introduction to concurrent communicating systems (reactive programs), especially to their computational models and to temporal logic as a formal specification language for the description and analysis of behavioral and time-dependent properties of these systems. No detailed knowledge of any particular programming language is necessary and no prior knowledge of temporal logic is required, as these topics are introduced here.
In Chapter 1 a generic model of basic transition systems is introduced and it is shown how it can be mapped onto different concrete languages with specific communication and synchronization constructs as well as onto other formalisms commonly used to represent concurrency (Petri nets here). The programming language allows processes to communicate not only by message-passing but by shared variables as well. Some concurrent programming paradigms (e.g. mutual exclusion, producer — consumer) are presented both in terms of shared variables and in those of different versions of message passing mechanisms.
A fair transition system as a model for real reactive systems is the main topic of Chapter 2. It is examined how faithfully the computational model (in which concurrency is represented by interleaving) corresponds to real (overlapped) concurrent execution of programs. Some syntactical restrictions on programs are defined and the computational model is completed by introducing various notions of (weak/strong) fairness. The correspondence between interleaving-based and real concurrent execution is ensured. This chapter completes the Part I of this volume.
In Chapter 3 the language of temporal logic as a tool for the formal specification of reactive systems is introduced. The language contains two (dual) sets of temporal operators (future/past). Properties of these operators are examined in details. Formal means for the derivation of temporal properties are provided by a deductive proof system. The chapter is concluded with the presentation of the models that correspond to computation of (fair) transition systems.
The last chapter illustrates the use of temporal logic for specifying properties of programs. A hierarchy of the classes of properties expressible by temporal logic is defined. Each class within this hierarchy is examined and for each class of comprehensive set of examples of concrete, class typical properties is presented. The rest of the chapter is devoted to the problems of modular specifications of reactive systems.
The book is of great value for those who are interested in the design, construction and analysis of parallel distributed systems and who want to learn and apply the language of temporal logic to the specification, verification and development of these systems. Each chapter is complemented with a set of problems of various difficulty, from those which are intended to test the understanding of the material included in the chapter of those of research level. This volume is perfectly suitable for a one-semester course either at senior undergraduate level for graduate level.

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing