Model Checking of Timed Petri Nets to Semantically Equivalent Timed Automata Based on Uppaal
基于Uppaal的时延Petri网到时间自动机等价模型验证

Both timed Petri nets and timed automata can carry on behavior simulation and performance analysis to the real-time system effectively.Utilizes a translation algorithm (referred to as TPN-to-TA translation) which can map a timed Petri nets model of real-time system into a collect of semantically equivalent timed automata, use a mature model checker Uppaal for timed automata to verify the performance of this timed Petri nets model.