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

摘要：

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

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

分类号：TP391.9(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目60674100

在线出版日期：2015-04-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：162-166