On Compositionality of Boundedness and Liveness for Nested Petri Nets
Titel:
On Compositionality of Boundedness and Liveness for Nested Petri Nets
Auteur:
Dworzański, Leonid W. Lomazova, Irina A.
Verschenen in:
Fundamenta informaticae
Paginering:
Jaargang 120 (2012) nr. 3-4 pagina's 275-293
Jaar:
2012-12-03
Inhoud:
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.
Tijdschrift beschrijving