Bounded model checking of Time Petri Nets using SAT solver

To carry out performance evaluation of an asynchronous system, the system is modeled as Time Petri Net (TPN) and an iteration of Petri net simulations produces its performance index. The TPN model needs to satisfy required properties such as deadlock freeness. We proposed a symbolic representation of TPN for SAT-based bounded model checking. In the proposed encoding scheme, firing of transitions and elapsing of place delays are expressed as boolean formulas discretely. Our representation can work with relaxed there exists-step semantics which enables to perform each step by two or more transitions. We applied the encoding to example TPN models and checked the deadlock freeness using SAT solver. The results of experiments demonstrated the effectiveness of the proposed representation.