Дерево достижимости

Дерево достижимости представляется множеством состояний сети.

В начальной маркировке (1, 0, 0) разрешены два перехода t1 и t2. Первый шаг построения дерева достижимости показан на рис (б). Из маркировки (1, 1, 0) можно снова запустить t1 (получая (1, 2, 0)) и t2 (получая (0, 2, 1)); из (0, 1, 1) можно запустить t3 (получая (0, 0, 1)). Второй шаг построения дерева достижимости показан на рис (в).

Продолжая три маркировки (рис (в)) на третьем шаге маркировки (рис (г)). Маркировка (0, 0, 1) пассивная: никакой переход в ней не разрешен. Маркировка (0, 1, 1), порождаемая запуском t3 в (0, 2, 1) была уже порождена непосредственно из начальной маркировки запуском t2.

Если эту процедуру повторять снова и снова, каждая достижимая маркировка окажется порожденной, а полученное дерево может оказаться бесконечным.

Всякий путь в дереве, начинающийся в корне соответствует допустимой последовательности переходов.

Для превращения дерева в полезный инструмент анализа необходимо найти средства ограничения его до конечного размера. Приведение к конечному представлению осуществляется двумя операциями.

Первая из них – это использование пассивных маркировок, именуемых терминальными вершинами, и маркировок, ранее встречавшихся в дереве, именуемых дублирующими вершинами. В нашем примере маркировка (0, 0, 1) – терминальная, а (0, 1, 1) – дублирующая.

Вторая операция. Рассмотрим последовательность запусков переходов s, начинающуюся в начальной маркировке М0 и концом . Маркировка M’ совпадает с маркировкой М0, за исключением того, что имеет некоторые “дополнительные” метки в некоторых позициях, то есть . Поскольку на запуски переходов дополнительные метки не влияют, последовательность s можно запустить снова, начиная в M’, приходя к маркировке . Так как действие последовательности переходов s добавило  меток к маркировке M0, она добавит также  меток к маркировке M’, поэтому M”=M’+(M’-M0) или . В общем случае последовательность s можно запустить n раз, получив в результате маркировку .

В нашем примере можно запустить переход t1 столько раз сколько необходимо для того, чтобы получить произвольное число меток в P2. Это бесконечное число маркировок обозначим символом w. Для любого a определим

Эти операции с символом w достаточны для построения дерева.