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

摘要：

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

关键词：反应系统、公平转换系统、时序逻辑、性质验证、可判定性

所属期刊栏目：26

分类号：TP311(计算技术、计算机技术)

资助基金：国家高技术研究发展计划863计划2001AA113200;国家自然科学基金60073020,60273025;国家重点基础研究发展计划973计划2002cb312200

在线出版日期：2004-01-02（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：1424-1434