On Compositionality of Boundedness and Liveness for Nested Petri Nets
Title:
On Compositionality of Boundedness and Liveness for Nested Petri Nets
Author:
DworzaĆski, Leonid W. Lomazova, Irina A.
Appeared in:
Fundamenta informaticae
Paging:
Volume 120 (2012) nr. 3-4 pages 275-293
Year:
2012-12-03
Contents:
Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level NP-nets [14]. Boundedness is in EXPSPACE and liveness is in EXPSPACE or worse for plain Petri nets [6]. However, for some restricted classes, e.g. for plain free-choice Petri nets, problems become more amenable to analysis. There is a polynomial time algorithm to check if a free-choice Petri net is live and bounded [4]. In this paper we prove, that for NP-nets boundedness can be checked in a compositional way, and define restrictions, under which liveness is also compositional. These results give a base to establish boundedness and liveness for NP-nets by checking these properties for separate plain components, which can belong to tractable Petri net subclasses, or be small enough for model checking.