• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Глава

Compositionality of Some Behavioral Properties for Free-Choice Nested Petri Nets

P. 27-34.
Dworzanski L. W., Lomazova I. A.

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.

В книге

Compositionality of Some Behavioral Properties for Free-Choice Nested Petri Nets
Под науч. редакцией: V. Nepomniaschy, V. Sokolov. Yaroslavl: Yaroslavl State University, 2011.