联锁逻辑形式化模型检验的研究

• 作者: XU Zhong-wei 宋波 杜军威
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 有色Petri网 线性时态逻辑 带标签的广义Büchi自动机 联锁逻辑
• 年，卷（期）: 2007,（15）
• 所属期刊栏目: 博士论文
• 页码范围: 33-35
• 页数: 3页
• 分类号: TP311
• 字数: 3722字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2007.15.012

摘要

利用自动机理论模型检验算法,检验车站联锁逻辑的有色Petri网模型是否满足预期的性能.通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑,有效地解决了模型检验中的状态空间爆炸问题.该方法的研究增强了有色Petri网的分析和验证能力,利用该方法对车站联锁逻辑的实际问题进行了性能验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杜军威	同济大学电子与信息工程学院	50	341	9.0	17.0
5	XU Zhong-wei	上海大学计算机学院	2	1	1.0	1.0
6	宋波	同济大学电子与信息工程学院	4	5	2.0	2.0