Abstract
In this paper, we develop a general technique for truncating Petri net unfoldings, parameterised according to the level of information about the original unfolding one wants to preserve. Moreover, we propose a new notion of completeness of a truncated unfolding. A key aspect of our 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 pre x of the unfolding. Canonical pre xes are complete in the new, stronger sense, and we provide necessary and sucient conditions for its niteness, as well as upper bounds on its size in certain cases. A surprising result is that after suitable generalisation, the standard unfolding algorithm presented in [5], and the parallel unfolding algorithm proposed in [8], despite being non-deterministic, generate the canonical pre x. This gives an alternative correctness proof for the former algorithm, and a new (much simpler) proof for the latter one.
Canonical Prefixes of Petri Net Unfoldings
In 14th International Conference on Computer Aided Verification (CAV 2002),Copenhagen, Denmark, 27-31 July 2002
Brinksma E. and Larsen K.G. (eds.)
Lecture Notes in Computer Science, 2404, pp 582-595
Springer-Verlag, 2002ISBN 3-540-43997-8
[Abstract]