Bounded model checking of Time Petri Nets using SAT solver

[摘要] References(10)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 �?-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.

[学科分类] 电子、光学、磁材料

[关键词] symbolic model checking;bounded model checking;Time Petri Net;SAT solver