Branching processes of high-level petri nets

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 in the sense that all the verification tools employing the traditional unfoldings can be reused with prefixes derived directly from high-level nets. Our experiments demonstrate that this method is often superior to the usual one, involving the explicit construction of the intermediate low-level net