基于有色Petri网的电梯门系统建模与仿真

来源：计算机技术与发展杂志2015年第03期北京时间：

作者：刘文良;刘久富;周建勇

摘要：文中分析了电梯门系统的组成结构，描述了电梯门系统的运行过程。文中利用有色Petri网中不同颜色的token可以表示系统的不同类型的状态的原理建立了基于有色Petri网的电梯门系统模型，避免了传统Petri网建模模型时引起的状态空间爆炸问题。然后利用CPN Tools对模型进行动态分析并生成状态空间报告以分析模型的回归性、有界性、活性及公平性。活性分析存在死标识时，提出基于ASK-CTL模型检验理论的死标识合理性算法验证模型中不存在自循环终端和死锁标识，进而验证了死标识存在的合理性，证实了电梯门系统CPN模型的正确性。

关键词：电梯门系统;有色Petri网 ;ASK-CTL;死标识;活性