TAPAAL and Reachability Analysis of P/T Nets

摘要

We discuss selected model checking techniques used in the tool TAPAAL for the teachability analysis of weighted Petri nets with inhibitor arcs. We focus on rechniques that had the most significant effect at the 2015 Model Checking Contest (MCC). While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.