The Temporal Logic of Reactive Systems

本项目继续致力于将时间逻辑形式主义转化为实用工具的研究。目标是为反应性系统的规范、验证、开发和合成建立统一的时间逻辑方法，并构建一个实验系统，为这些活动提供自动化支持。所考虑的响应系统类别包括并发、实时和混合程序、过程控制和嵌入式程序、硬件设备和其他系统，其作用是保持与其环境的持续交互。为了实现这些目标，研究了以下主题：(1)从时间规范合成反应模块的演绎技术；(2)混合系统的时间规范和验证；(3)时间证明的自动化支持系统。

This project continues research aimed at turning the temporal-logic formalism into a practical tool. The goals are to establish a uniform temporal-logic methodology for the specification, verification, development, and synthesis of reactive systems, and to construct an experimental system that will provide automated support for these activities. The class of reactive systems considered includes concurrent, real-time, and hybrid programs, process-control and embedded programs, hardware devices, and other systems whose role is to maintain a continuous interaction with their environment. To attain these goals, the following topics are investigated; (1) deductive techniques for the synthesis of reactive modules from temporal specifications, (2) temporal specification and verification of hybrid systems, and (3) an automated support system for temporal proofs.