Volume 43, Number 5, 307-330, DOI: 10.1007/s00236-006-0023-y

Merged processes: a new condensed representation of Petri net behaviour

Victor Khomenko, Alex Kondratyev, Maciej Koutny and Walter Vogler

View Related Documents

Abstract

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

Fulltext Preview

Image of the first page of the fulltext document