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

Статья

On Compositionality of Boundedness and Liveness for Nested Petri Nets

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

Вложенные сети Петри (NP-сети) – суть сети Петри с сетевыми фишками. Проблемы живости и ограниченности неразрешимы для двухуровневых NP-сетей. Для обыкновенных сетей Петри проблема ограниченности относится к классу сложности EXPSPACE, а проблема живости не меньше чем EXPSPACE-сложная. Однако для некоторых ограниченных классов, таких как сети Петри со свободным выбором, эти проблемы являются не такими трудными. Проверка ограниченности и живости сетей Петри со свободным выбором разрешима за полиномиальное время.

В этой статье мы доказываем, что для NP-сетей ограниченность может проверяться композиционально, и формулируем условия композициональности живости. Эти результаты могут использоваться для сведения проверки ограниченности и живости NP-сетей к проверке этих свойств для отдельных одноуровневых компонентов. Компоненты NP-сети могут принадлежать легко анализируемым подклассам сетей Петри, или иметь небольшой размер, что позволяет использовать для их анализа методы проверки моделей.