论文部分内容阅读
Petri网由于有强大的建模能力和成熟的理论支持,被广泛应用于各种系统的建模.本文通过把Petri网转换成转移系统,利用转移系统和Kripke结构给出了时序逻辑语义的解释,从而建立一种在Petri网上进行时序分析的方法.这种方法是根据不动点理论,用模型检查验证公式正确性.通过对Ada程序会合性质进行模型检查,验证了这种方法的有效性.