论文研究有色Petri网模型中死标志合理性分析与验证.pdf

针对使用CPNTools对系统进行建模仿真得到的状态空间报告中出现的死标志是否会影响系统的安全性和模型的正确性进行了研究，提出了一种基于ASK-CTL及模型检验理论的死标志合理性验证算法。该算法采用模型检验技术通过ML语言编辑相关功能函数使用非标准状态空间查询法，进一步分析与研究CPNTools仿真状态空间报告中出现的死标志，通过验证死标志存在的合理性来确保所建立CPN模型的准确性与系统的安全性。最后，以电梯门系统为例，使用CPNTools建立电梯门系统的CPN模型，证明了算法的有效性。