Decompositional Petri Net Reductions

Abstract

As a means to tackle the state explosion problem of model checking 1-safe Petri nets for linear time logic without next-time (LTL$_{\textrm{-\tiny{X}}}$), an approach that combines compositional verification and Petri net reductions is presented. We decompose a Petri net into (i) a so-called kernel net Σ _k containing all places mentioned by the LTL$_{\textrm{-\tiny{X}}}$ property φ and (ii) environment subnets . These environment nets do not interact with each other and have limited influence on the kernel only. Six distinct and very simple summary nets suffice to describe the influence of any environment net. To determine the appropriate summary net we modularly verify up to three fixed LTL$_{\textrm{-\tiny{X}}}$ formulas on . We reduce Σ by replacing every environment subnet in Σ by its summary net. Instead of checking φ on Σ, we check φ on the reduced net. Verification of several case-studies shows that our reduction approach can significantly speed-up model checking.

This work is supported by the German Research Foundation (DFG), grant GRK 1076/1.