A Symbolic Model Checker for Petri Nets: pnmc

摘要

Symbolic model checking with decision diagrams is a very efficient technique for handling large models. However, even when using advanced algorithms, model checking tools still need to be carefully written. Indeed, they are both CPU and memory bounded: in addition to the algorithms complexity, the limiting factors are the available memory and how fast computations are performed. Thus, each saved CPU cycle or byte can make the difference between a successful model checker and a failing one. We present pnmc, a symbolic model checker for Petri Nets, and libsdd, its associated library which implements Hierarchical Set Decision Diagrams and automatic saturation. Reliability aside, choices were always made to favour performance. The combination of advanced algorithms for symbolic model checking and advanced coding techniques offer very good results as shown in the Model Checking Contest 2015, which is used as a background to present pnmc and libsdd.