Affiliations: National Research University Higher School of Economics, Moscow, 101000, Russia, [email protected] | National Research University Higher School of Economics, Moscow, 101000, Russia | Program Systems Institute of the Russian Academy of Science, Pereslavl-Zalessky, 152020, Russia, [email protected]
Note: [] Address for correspondence: National Research University Higher School of Economics, Moscow, 101000, Russia The research is partially supported by the Russian Fund for Basic Research (projects 11-01-00737, 11-07-00549)
Note: [] Address for correspondence: National Research University Higher School of Economics, Moscow, 101000, Russia The research is partially supported by the Russian Fund for Basic Research (projects 11-01-00737, 11-07-00549). This study was carried out within the National Research University Higher School of Economics' Academic Fund Program in 2012-2013, research grant No. 11-01-0032.
Abstract: 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.
