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

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