Department of Computing Science
University of Newcastle upon Tyne
12pm Thursday 11th January 2002
Room 2511, JCMB, King's Buildings
In this talk, I introduce a general technique for truncating Petri net unfoldings, parameterized according to the level of information about the original unfolding one wants to preserve. Moreover, I propose a new notion of completeness of a truncated unfolding. A key aspect of this approach is an algorithm-independent notion of cut-off events, used to truncate a Petri net unfolding. Such a notion is based on a cutting context and results in the unique canonical prefix of the unfolding. Canonical prefixes are complete in the new, stronger sense, and we provide necessary and sufficient conditions for its finiteness, as well as upper bounds on its size in certain cases. A surprising result is that after suitable generalization, the standard unfolding algorithm presented of Esparza, Roemer, and Vogler, and the parallel unfolding algorithm proposed by Heljanko, Khomenko, and Koutny, despite being non-deterministic, generate the canonical prefix. This gives an alternative correctness proof for the former algorithm, and a new (much simpler) proof for the latter one.
This is joint work with Maciej Koutny and Walter Vogler.