Toggle Main Menu Toggle Search

ePrints

Canonical Prefixes of Petri Net Unfoldings

Lookup NU author(s): Dr Victor Khomenko, Professor Maciej Koutny

Downloads


Abstract

In this paper, we develop a general technique for truncating Petri net unfoldings, parameterized 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, which with the standard parameters is strictly stronger than that given in [5,6], and is more appropriate for the existing model checking algorithms. A key aspect of our approach is an algorithm-independent notion of cut-off events, used to truncate a Petri net unfolding in the existing model checking systems. Such a notion is based on a cutting context and results in the unique canonical prefix of the unfolding. We show that the canonical prefix is complete in the new, stronger sense, and provide necessary and sufficient conditions for its finiteness, as well as upper bounds on its size in certain cases. We then consider the unfolding algorithm presented in [5,6], and the parallel unfolding algorithm proposed in [10]. We prove that both algorithms, 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.


Publication metadata

Author(s): Khomenko VV, Koutny MS, Vogler W

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: 14th International Conference on Computer Aided Verification (CAV 2002)

Year of Conference: 2002

Pages: 158-173

ISSN: 0302-9743

Publisher: Springer-Verlag

URL: http://dx.doi.org/10.1007/3-540-45657-0_49

DOI: 10.1007/3-540-45657-0_49

Library holdings: Search Newcastle University Library for this item

Series Title: Lecture Notes in Computer Science

ISBN: 9783540439974


Actions

Link to this publication


Share