There is a growing need for effective formal methods of constructing correct and reliable computer programs. This need becomes especially crucial in the case of concurrent,distributed, real-time, or, more generally, reactive systems. Such systems typically involve a number of delicate and subtle aspects such as parallel operation of distinct, often geographically dispersed components, and ongoing, ideally nonterminating computation where each component repeatedly interacts with neighboring components in order to achieve a global goal or maintain a global invariant. Many safety critical real-world applications programs can be counted among the reactive systems. Examples include: computer operating systems, computer network communication protocols, air traffic control systems, on-board avionics control systems, as well as automated banking networks. The approach taken in this research to reasoning about such reactive systems centers around the use of Temporal Logic, a formalism that can be used for specification, verification, design, and synthesis of reactive systems. This research investigates to what extent efficient automation of temporal reasoning about reactive systems is possible. Considerable attention is devoted to the following particular aspects: attacking the state explosion problem, reasoning about many homogenous processes, real-time reasoning, and synthesis of reactive systems.
