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.
Branching Processes of High-Level Petri Nets
In 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2003), Warsaw, Poland, 7-11 April 2003
Garavel, H. and Hatcliff, J. (eds.)
Lecture Notes in Computer Science, 2619, pp 458-472
Springer-Verlag, 2003ISBN 3-540-00898-5
[Abstract]