zbMATH — the first resource for mathematics

Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. (English) Zbl 0607.68022
Current trends in concurrency, overviews and tutorials, Lect. Notes Comput. Sci. 224, 510-584 (1986).
[For the entire collection see Zbl 0587.00018.]
This is one of the most complete and certainly documented surveys of the subject. It is divided in four parts: 1. An abstract computational model for reactive systems, namely ”fair transition system”, 2. Basic notions and results for temporal logic (TL); 3. A formal global proof system for the fair transition model using TL; 4. Preliminary approaches to modular specification and verification of reactive systems. The connection with existing real systems is emphasized. References, examples and possible developments are also provided.
Reviewer: C.Masalagiu

68Q65 Abstract data types; algebraic specification
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)