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