Compositionality of Some Behavioral Properties for Free-Choice Nested Petri Nets
Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level Nested Petri nets (NP-nets). Boundedness and liveness are still very hard to check even for plain Petri nets (EXPSPACE or worse). For the restricted class of free-choice Petri nets some problems become more amenable to analysis. There is the polynomial time algorithm to check if a free-choice Petri net is live and bounded. We prove that for some restricted class of NP-nets with free-choice components boundedness can be checked in a compositional way and define restrictions, under which liveness is also compositional. The motivating example of such restricted NP-nets is provided.