Bounded model checking of Time Petri Nets using SAT solver

Tomoyuki Yokogawa
Masafumi Kondo
Hisashi Miyazaki
Sousuke Amasaki
Yoichiro Sato
Kazutami Arimoto

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.

IEICE ELECTRONICS EXPRESS

IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG

12

2

20141112

20141112

10.1587/elex.11.20141112

https://doi.org/10.1587/elex.11.20141112
https://dblp.uni-trier.de/rec/journals/ieiceee/YokogawaKMASA15
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000351017100005&DestApp=WOS_CPL
http://dblp.uni-trier.de/db/journals/ieiceee/ieiceee12.html#journals/ieiceee/YokogawaKMASA15