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

• 作者: 唐稚松 李广元
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 反应系统 公平转换系统 时序逻辑 性质验证 可判定性
• 年，卷（期）: 2003,（11）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1424-1434
• 页数: 11页
• 分类号: TP311
• 字数: 13489字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2003.11.002

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐稚松	中国科学院软件研究所计算机科学重点实验室	8	175	4.0	8.0
2	李广元	中国科学院软件研究所计算机科学重点实验室	3	8	2.0	2.0