离散实时线性动态逻辑的符号化模型检测

• 作者: 曾昊晟 杨帆 许杭娜 陈祖希 骆翔宇
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 符号化模型检测 时态测试器 实时线性动态逻辑 离散实时系统
• 年，卷（期）: 2020,（9）
• 所属期刊栏目: 人工智能
• 页码范围: 204-212
• 页数: 9页
• 分类号: TP311
• 语种: 中文
• DOI: 10.11896/jsjkx.190900167

摘要

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的.针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较.实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MC-MAS-LDLK.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	骆翔宇		12	73	4.0	8.0
2	杨帆		10	19	3.0	4.0
3	许杭娜		1	0	0.0	0.0
4	曾昊晟		1	0	0.0	0.0
5	陈祖希		1	0	0.0	0.0