反应系统的连续时序逻辑表示和验证

引进一个称为LTLC的连续时间时序逻辑，用来对反应系统进行规范与验证．LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质，这样就可将系统与性质问的满足关系转化为逻辑公式间的蕴涵关系．同时，采用非负实数集作为时间域还使我们可以利用标准的存在量词来表示变量隐藏，并可用逻辑蕴涵来表示反应系统间的求精关系．该文首先给出了LTLC的一个简单介绍，然后讨论了如何使用LTLC对反应系统进行表示与推理，最后证明了一个关于LTLC的可判定性结果．此结果可用于有穷状态反应系统的自动验证．

Representing and Verifying Reactive Systems with Continuous-Time Temporal Logic

A continuous-time temporal logic, called LTLC, is introduced in this paper for the specification and verification of reactive systems. A distinguished feature of LTLC is that it can represent both reactive systems and their properties in one unified logic framework, so the satisfaction relation between systems and their properties can be expressed by logical implication. In addition, the use of non-negative real numbers as time domain enables us to express hiding of variables as standard existential quantification and express the relation of refinement between reactive systems as implications between logic formulas. This paper begins with a brief introduction to LTLC and then describes how it is used to represent and reason about reactive systems. Finally, a decidability result about LTLC is given. The result can be used for the automatic verification of finite-state reactive systems.