• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

On Compositionality of Boundedness and Liveness for Nested Petri Nets

Fundamenta Informaticae. 2012. Vol. 120. No. 3-4. P. 275-293.

Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level NP-nets. Boundedness is in EXPSPACE and liveness is in EXPSPACE or worse for plain Petri nets. 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.

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.