Interpolation Based Unbounded Model Checking for Time Petri Nets

Safety critical systems are often modeled using Time Petri Net (TPN) for analyzing its reliability with formal verification methods. This paper proposed a safety verification method for TPN introducing unbounded model checking based on over-approximation of the state space. The proposed method expresses time constraints of TPN by Difference Logic (DL) and uses an SMT solver for verification. DL is a sub-theory of linear arithmetic obtained by restricting each inequality between a difference of two variables and a constant. Its effectiveness was also demonstrated with an experiment.