9804736 There is a serious need for effective formal methods to construct correct computer programs. This need becomes crucial for reactive systems associated with many safety critical or economically vital applications, such as computer network communication protocols or air traffic control systems. One promising approach centers around the use of Temporal Logic, a logical formalism for describing change over time. Purely manual temporal reasoning seems infeasible for large-scale reactive systems. The goal of this research is to make verification of reactive systems as automated as possible. Automated verification is more reliable than manual verification. It is also more likely to be of industrial utility, as it is possible to offer fully automated push-button verification and debugging tools. The basic idea is that certain problems associated with (propositional) Temporal Logic are decidable, in some cases efficiently. These include the model checking problem (Is a program's global state graph a model of Temporal Logic specification ?). This research investigates, the following key technical issues: (i) Amelioration of the state explosion problem in model checking; (ii) Reasoning about many homogeneous processes; (iii) Development of a modular Research Model Checker; and (vi) Efficient program synthesis.***
