time Petri net (TPN)在实时控制系统的建模中得到广泛应用,而冲撞是Petri网及其扩展模型的重要行为,解决冲撞是正确分析模型动态行为的关键.由于引入时间约束,使得TPN模型的使能和触发语义比Petri网模型的语义复杂,冲撞的检测及消解变得更加困难.首先根据时间约束,给出了变迁持续使能时延迟区间的计算方法,并证明了该方法的正确性；然后在此基础上定义并证明了TPN模型中冲撞的检测方法；给出了冲撞时间区间及修改时间约束的冲撞消解方法；最后通过实例验证说明了该方法的有效性和正确性.%Time Petri net is widely used to model real-time control systems. Contacts are important behaviors of Petri net and these expansion models. To solve the contacts is a key of analyzing models dynamic behaviors. Because the time constraints are adhibited, time Petri net enabling and triggering semantics are becoming more complex than Petri net, and contacts checking and resolution are getting more difficult. Time intervals of transitions are defined when these transitions are durably enabled, and this definition correctness is discussed. An approach is proposed to check contacts of time Petri net and a contacts resolution approach based on changing time constraints of transitions is defined and proved. The approach availability is verified by an example analysis. The results show that applying our approach to check the resource contacts of time Petri net is feasible.
展开▼
