In: H. Garavel, J. Hatcliff (Eds.): Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), 9th International Conference, Part of ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Volume 2619 of Lecture Notes in Computer Science, pages 458-472. Springer Verlag, 2003, February 2003.
Abstract: In this paper, we define branching processes and unfoldings of high-level Petri nets and propose an algorithm which builds finite and complete prefixes of such unfoldings. The advantage of our method is that it avoids a potentially expensive translation of a high-level Petri net into a low-level one. The approach is conservative as all the verification tools employing the traditional unfoldings can be reused with prefixes derived directly from high-level nets. We show that this is often better than the usual explicit construction of the intermediate low-level net.
Keywords: verification; model checking; high-level Petri nets; unfolding.