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

被引：7

作者：

蒋屹新

林闯

邢栩嘉

机构：

[1] 清华大学计算机科学与技术系

[2] 清华大学计算机科学与技术系北京

[3] 北京

来源：

系统仿真学报 | 2003年 / S1期

关键词：

线性时序逻辑; Petri网; Büchi自动机; 同步积; 模型检测;

D O I：

10.16182/j.cnki.joss.2003.s1.002

中图分类号：

TP301.6 [算法理论];

学科分类号：

081202 ;

摘要：

Petri网是一种重要的数学工具,它能有效地对并发系统进行描述和建模。线性时态逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能方便准确地描述并发系统的重要性质,如安全性和活性。文章深入描述了线性时态逻辑、Büchi自动机、Petri网和同步积之间的内在联系,并探讨了基于线性时态逻辑的Petri网模型检测策略。与其它方法比较,这种模型检测的策略结合了线性时态逻辑和Petri网模型的不同优点,增强了Petri网的模型分析和验证能力。最后,通过对一个并发系统形式化的模型检测分析,验证了相应的结论。

引用

页码：6 / 10

页数：5