The Temporal Logic of Reactive Programs

时间逻辑是一种有用的、强大的形式，用于规范、分析和开发大型系统（称为反应系统）。这类系统包括并发和实时程序、过程控制和嵌入式程序、硬件设备和其他系统，其作用是保持与其环境的持续交互。本项目旨在将时间形式主义转化为实用工具进行研究。主要目标是为反应系统的规范、验证、开发和自动合成建立统一的时间逻辑方法，并构建一个实验系统，为这些活动提供计算机支持。要研究的具体主题包括：时间逻辑规范的表达能力和便利性，以及通过扩展（如过去运算符和状态变量的量化）对其可能的改进；时间逻辑与转换系统（如自动机）的结合；时间规范的组合性是通过分解和细化进行系统开发的基础。

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.