Верификация вложенных сетей Петри с помощью метода развёртки

Вложенные сети Петри (NP-сети) являются одним из наиболее подходящих формализмов для анализа распределенных систем и моделирования. Они естественным образом представляют собой структуру мультиагентных систем, так как фишки в системной сети сами являются классическими сетями Петри (P/T-сетями) и могут иметь свое собственное поведение. Для проверки свойств вложенных сетей Петри используется один из наиболее популярных методов верификации – проверка моделей. Тем не менее, существует серьезная проблема при верификации высоко параллельных систем при использовании подхода проверки моделей – большое количество интерливингов параллельных процессов. Это ведет к так называемой проблеме взрывообразного роста состояний. Для решения этой проблемы был представлен подход развёртки. В статье Д. Фрумина и И. Ломазовой была изучена применимость разверток для NP-сетей и был предложен метод построения разверток для безопасных консервативных NP-сетей. Однако, поскольку безопасные консервативные вложенные сети Петри ограничены, для такой сети можно построить классическую сеть Петри с эквивалентным поведением, на которой могут быть применены стандартные методы развертки. Возникает вопрос, действительно ли прямая развёртка намного лучше, чем построение разверток с помощью трансляции NP-сетей в безопасные P/T сети с точки зрения сложности и времени. Здесь мы изучаем этот вопрос. Для этого мы разработали алгоритм для трансляции безопасной консервативной NP-сети в поведенчески эквивалентную P/T сеть. Мы доказали, что графы достижимости исходной NP-сети и полученной P/T сети изоморфны, и, следовательно, оба метода дают одинаковый (с точностью до изоморфизма) результат. Из общих соображений трансляция NP-сети в P/T сеть, а затем построение развертки займет больше времени, чем построение развертки непосредственно. Чтобы проверить, существует ли этот разрыв во времени на практике, мы реализовали все упомянутые алгоритмы и сравнили оба метода экспериментально.