Temporal logic is a useful, powerful formalism for the specification, analysis, and development of a large class of systems, referred to as reactive systems. This class of systems includes concurrent and real- time programs, process control and embedded programs, hardware devices, and other systems whose role is to maintain a continuous interaction with their environment. This project is to conduct a research aimed at making the temporal formalism into a practical tool. The primary goals are to establish a uniform temporal-logic methodology for the specification, verification, development, and automatic synthesis of reactive systems, and to construct an experimental system that will provide computerized support for these activities. Specific topics to be investigated include: the expressive power and convenience of specification by temporal logic, and its possible improvements by extensions such as past operators and quantification over state-variables; combination of temporal logic with transition systems, such as automata; and compositionality of temporal specifications as a basis for systematic development by decomposition and refinement.
