基于线性时态逻辑的Petri网模型检测
Petri网是一种重要的数学工具,它能有效地对并发系统进行描述和建模.线性时态逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能方便准确地描述并发系统的重要性质,如安全性和活性.文章深入描述了线性时态逻辑、Büchi自动机、Petri网和同步积之间的内在联系,并探讨了基于线性时态逻辑的Petri网模型检测策略.与其它方法比较,这种模型检测的策略结合了线性时态逻辑和Petri网模型的不同优点,增强了Petri网的模型分析和验证能力.最后,通过对一个并发系统形式化的模型检测分析,验证了相应的结论.
线性时序逻辑 Petri网 同步积 模型检测
蒋屹新 林闯 邢栩嘉
清华大学计算机科学与技术系(北京)
国内会议
杭州
中文
6-10
2003-09-01（万方平台首次上网日期，不代表论文的发表时间）