论文部分内容阅读
time Petri net（TPN）在实时控制系统的建模中得到广泛应用，而冲撞是Petri网及其扩展模型的重要行为，解决冲撞是正确分析模型动态行为的关键．由于引入时间约束，使得TPN模型的使能和触发语义比Petri网模型的语义复杂，冲撞的检测及消解变得更加困难．首先根据时间约束，给出了变迁持续使能时延迟区间的计算方法，并证明了该方法的正确性；然后在此基础上定义并证明了TPN模型中冲撞的检测方法；给出了冲撞时间区间及修改时间约束的冲撞消解方法；最后通过实例验证说明了该方法的有效性和正确性．