Инвариантность модели Петри протокола TCP

Анотація

Доказана инвариантность модели Петри для фаз установления соединения и разъединения протокола TCP. Выполнена декомпозиция модели Петри на функциональные подсети. Вычисление инвариантов осуществлено в процессе последовательной композиции, что обеспечило существенное ускорение вычислений.