The Temporal Logic of Reactive Programs

反应式程序的时间逻辑

• 批准号: 8911512
• 负责人: Zohar Manna
• 金额: $ 29.53万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-05-01 至 1993-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8911512&HistoricalAwards=false
• 关键词: Temporal; Logic; 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.

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