?
On Compositionality of Boundedness and Liveness for Nested Petri Nets
Вложенные сети Петри (NP-сети) – суть сети Петри с сетевыми фишками. Проблемы живости и ограниченности неразрешимы для двухуровневых NP-сетей. Для обыкновенных сетей Петри проблема ограниченности относится к классу сложности EXPSPACE, а проблема живости не меньше чем EXPSPACE-сложная. Однако для некоторых ограниченных классов, таких как сети Петри со свободным выбором, эти проблемы являются не такими трудными. Проверка ограниченности и живости сетей Петри со свободным выбором разрешима за полиномиальное время.
В этой статье мы доказываем, что для NP-сетей ограниченность может проверяться композиционально, и формулируем условия композициональности живости. Эти результаты могут использоваться для сведения проверки ограниченности и живости NP-сетей к проверке этих свойств для отдельных одноуровневых компонентов. Компоненты NP-сети могут принадлежать легко анализируемым подклассам сетей Петри, или иметь небольшой размер, что позволяет использовать для их анализа методы проверки моделей.