基于线性时态逻辑的Petri网模型检测研究

• 作者: 周清雷 赵东明 赵晓凡
• 来源期刊: 科技与创新
• 关键词: 线性时态逻辑 Petri网 Büchi自动机 模型检测
• 年，卷（期）: 2009,（3）
• 所属期刊栏目: 网络与通信
• 页码范围: 100-101,106
• 页数: 3页
• 分类号: TP311
• 语种: 中文
• DOI: 10.3969/j.issn.1008-0570.2009.03.041

摘要

线性时态逻辑Petri网结合了Petri网和时序逻辑的优点,清晰简洁的描述并发系统事件间的时序和因果关系,包括系统的活性和安全性.其中自动机的体积是模型检验的一个关键性问题,为了得到尽可能小体积的自动机,在LTL公式转换为Büchi自动机之前,对LTL公式进行预处理来减少冗余,然后通过布尔技术优化自动机.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周清雷	郑州大学信息工程学院	109	475	10.0	16.0
2	赵东明	郑州大学信息工程学院	18	49	4.0	6.0
3	赵晓凡	郑州大学信息工程学院	1	4	1.0	1.0