Modeling and verification of interlocking logic based on temporal Petri nets

Temporal Petri nets,which combine the advantages of Petri nets and temporal logic,can describe clearly and compactly causal and temporal relationships between the events of a system,including eventuality and fairness.In this paper,we firstly use temporal Petri nets to describe the railway signal interlocking logic system,a safety-critical system,and use temporal logic to describe temporal relationships of system states.Then,we analyze and verify the properties of model and conclude that the system is effective.