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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Khomenko, V., Kondratyev, A., Koutny, M., & Vogler, W. (2005). Merged processes - A new condensed representation of Petri net behaviour. In Lecture Notes in Computer Science (Vol. 3653, pp. 338–352). Springer Verlag. https://doi.org/10.1007/11539452_27
Mendeley helps you to discover research relevant for your work.