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

摘要：

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

关键词：线性时态逻辑、Petri网、Büchi自动机、模型检测

所属期刊栏目：25

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

资助基金：基金申请人:周清雷;项目名称:基于时间自动机的模型验证理论及应用研究;基金颁发部门:河南省教育厅2006520015;基金申请人:周清雷项目名称:模型验证技术研究;基金颁发部门:河南省自然科学基金0411012169

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

页数：共3页

页码：100-101,106