Liveness Analysis of Parallel Program´s Petri Net Models

The liveness of Petri net models of parallel programs is a very important property. The existing analysis techniques take Petri net models as a whole to study properties, which is subject to the state explosion problem. In this study, we decompose a parallel program´s Petri net model into multiple process subnets to study liveness preservation instead of taking it as a whole, which thus mitigates efficiently the state explosion problem to some extent. In this paper, the liveness preservation relation between a MPINet and its process subnets is analyzed in detail. A necessary condition of keeping liveness of a MPINet composed of n live process subnets is given. And a class of CR-restricted MPINets is proposed. Liveness preservation can be efficiently verified based on only their net structures for CR-restricted MPINets.