Model checking based on Petri net unfoldings is an approach widely applied to cope with the state space explosion problem. In this paper, we propose a new condensed representation of a Petri net’s behaviour called
merged processes, which copes well not only with concurrency, but also with other sources of state space explosion, viz sequences of choices and non-safeness. Moreover, this representation is sufficiently similar to the traditional unfoldings, so that a large body of results developed for the latter can be re-used. Experimental results indicate that the proposed representation of a Petri net’s behaviour alleviates the state space explosion problem to a significant degree and is suitable for model checking.
V. Khomenko is a Royal Academy of Engineering/Epsrc Research Fellow supported by the RAEng/Epsrc grant EP/C53400X/1 (Davac).
M. Koutny is supported by the EC IST grant 511599 (Rodin).
W. Vogler is supported by the DFG-project STG-Dekomposition VO 615/7-1