有色Petri网模型中死标志合理性分析与验证

摘要

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