Computing Reviews

Boundedness undecidability for synchronized nets
Devillers R., Van Begin L. Information Processing Letters99(5):208-214,2006.Type:Article
Date Reviewed: 01/10/07

Petri nets provide a graphical representation of concurrent, discrete-event, dynamic systems. This paper answers questions about synchronized Petri nets (SPNs): “Are the nets bounded?” “Which places are unbounded?” “What is the bound for a bounded place?” Section 2 explains SPNs, and introduces a variation: simplified synchronized Petri nets (SSPNs). Section 3 outlines the two-counter machine (2CM), and relates 2CM to SSPNs. Section 4 concludes with the main theorem, proving that the boundedness problem for SSPNs is undecidable. In section 5, the authors successfully argue that the theorem is extensible and general. The theorem is derived elegantly via proof by contradiction: first, the authors establish that SSPNs are bounded if and only if 2CMs are bounded. Then, the boundedness problem for 2CMs is shown to be undecidable, from which follows the undecidability for SSPN bounds, and ultimately for synchronized nets.

The paper would have benefited from serious copyediting to render it more readable and clear. Moreover, a graph for SPNs would have been helpful. A picture could have explained how transitions fire only if all conditions are met and if associated external events occur, provided they pose no conflict with other transitions. The paper will be of interest to theoreticians interested in Petri net variants, such as signal nets, timed nets, prioritized nets, and temporized nets, but it is also relevant to practitioners working with modeling logic controllers.

Reviewer:  Herbert G. Mayer Review #: CR133783 (0712-1302)

Reproduction in whole or in part without permission is prohibited.   Copyright 2024 ComputingReviews.com™
Terms of Use
| Privacy Policy