In: Martín Abadi, Luca de Alfaro (Eds.): Lecture Notes in Computer Science, 3653: CONCUR 2005 - Concurrency Theory: 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005., pages 338-352. Springer-Verlag, November 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1153945227,.
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.
Keywords: Merged processes, Petri net unravelling, Petri net unfolding, state space explosion, model checking, formal verification.