Верификация вычислительных решеток с особыми краевыми условиями бесконечными сетями Петри

Представлена методика верификации вычислительных решеток с помощью нахождения инвариантов бесконечных сетей Петри. Построены модели структур квадратных решеток в форме параметрических сетей Петри для таких краевых условий, как соединение краев и усеченные устройства. По параметрическим сетям Петри построены бесконечные системы линейных алгебраических уравнений для вычисления p-инвариантов и получены их параметрические решения. P-инвариантные сети Петри являются структурно консервативными и ограниченными, что, вместе с живостью, является свойствами моделей идеальных систем. Исследование живости модели на основе анализа сифонов и ловушек может быть выполнено с помощью p-инвариантов модифицированных сетей.