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

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

P1 t2 P3

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

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

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

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

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

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

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

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

w+а=w, w-а=w, а<w, w£w

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