| 基于线性时态逻辑的Petri网模型检测 |
| |
| 引用本文： | 蒋屹新,林闯,邢栩嘉.基于线性时态逻辑的Petri网模型检测[J].系统仿真学报,2003,15(Z1):6-10. |
| |
| 作者姓名： | 蒋屹新 林闯 邢栩嘉 |
| |
| 作者单位： | 清华大学计算机科学与技术系,北京,100084 |
| |
| 基金项目： | 国家重点基础研究发展规划973计划项目(G1999032707)、国家高技术研究发展计划863计划课题(2001AA112080)、国家自然科学基金(90104002)和香港研究资助局(60218003)的资助. |
| |
| 摘 要： | Petri网是一种重要的数学工具,它能有效地对并发系统进行描述和建模.线性时态逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能方便准确地描述并发系统的重要性质,如安全性和活性.文章深入描述了线性时态逻辑、Bu chi自动机、Petri网和同步积之间的内在联系,并探讨了基于线性时态逻辑的Petri网模型检测策略.与其它方法比较,这种模型检测的策略结合了线性时态逻辑和Petri网模型的不同优点,增强了Petri网的模型分析和验证能力.最后,通过对一个并发系统形式化的模型检测分析,验证了相应的结论.
|
| 关 键 词： | 线性时序逻辑 Petri网 B u chi自动机 同步积 模型检测 |
| 文章编号： | 1004-731X(2003)S1-0006-05 |
| 修稿时间： | 2003年5月14日 |
Model Checking of Petri Nets Based on Linear Temporal Logic |
| |
| JIANG Yi-xin,LIN Chuang,Xing xu-jia.Model Checking of Petri Nets Based on Linear Temporal Logic[J].Journal of System Simulation,2003,15(Z1):6-10. |
| |
| Authors: | JIANG Yi-xin LIN Chuang Xing xu-jia |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
