Petri网性质的线性时序逻辑描述与Spin检验

Petri网是描述并发系统的很直观的图形工具Spin是一种著名的分析验证并发系统性质的工具。本文首先论述Petri网性质的线性时序逻辑描述,研究用Promela编程描述Petri网和用Spin对Petri网性质进行检验的方法,最后通过两个具体的示例说明这种方法是成功的。