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

Дерево достижимости представляет собой множество достижимости сети Петри. Рассмотрим следующую сеть Петри.

μ={2;0;0}

При этой маркировке разрешёнными являются переходы t₁ и t₂.

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

Построим дерево достижимости.

(2,0,0)

t₁ t₂

(2,1,0) (1,1,1)

t₁ t₂ t₃

(1,2,1) (0,2,2) (1,0,1)

t₁ t₂

(1,1,1) (0,1,2)

t₃

(0,0,2)

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

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

Для сведения дерева достижимости к конечному можно использовать ещё одно средство.

Рассмотрим последовательность запусков переходов σ, начинающуюся в некоторой маркировке μ. Пусть конечной маркировкой при этом будет μ’, для которой μ’> μ (сравнение идёт покомпонентно), т.е. в некоторых позициях для маркировки μ’ количество фишек будет больше, чем в маркировке μ (в остальных позициях количества фишек будут совпадать).

Условно мы можем записать μ’= μ+(μ’- μ), (μ’- μ)>0. Поскольку лишние фишки не мешают запуску переходов, то мы можем последовательность переходов σ запустить, начиная с маркировки μ’ и получить маркировку μ”= μ’+(μ’- μ)= μ+2(μ’- μ).

Таким образом, мы можем бесконечно увеличивать количество фишек в некоторых позициях.

Представим значение “ ” в маркировке символом ω. Будем считать, что для любого постоянного значения а ω+а=ω и ω-а=ω.

Алгоритм формирования дерева достижимости: каждая вершина i дерева достижимости связана с расширенной маркировкой μ[i]. В этой маркировке число фишек может быть либо неотрицательным целым, либо бесконечным, обозначаемым ω. Каждая вершина дерева может быть одного из четырёх типов:

1) граничная

2) терминальная

3) дублирующая

4) внутренняя

Граничными являются вершины, которые ещё не обработаны алгоритмом. Алгоритм превратит их в терминальные или дублирующие, или внутренние (породив, возможно, при этом некоторый набор граничных вершин).

Пусть х – граничная вершина, которую необходимо обработать.

1) Если в дереве достижимости имеется другая вершина y, не являющаяся граничной, такая, что μ[у]= μ[х], то вершина х становится дублирующей.

2) Если для маркировки μ[х] ни один из переходов не разрешён, то вершина х становится терминальной.

3) Для всякого перехода , разрешённого в маркировке μ[х], необходимо создать новую вершину z дерева достижимости. Маркировка μ[z], связанная с этой вершиной, для каждой позиции определяется следующим образом:

а) Если μ[х]_i=ω, то μ[z]_i=ω.

б) Если на пути от корневой вершины к вершине х существует вершина у такая, что маркировка μ[у]<δ(μ[х], t_j) и, кроме того, в μ[у]_i<δ(μ[х], t_j)_i, то μ[z]_i=ω.

в) В противном случае μ[z]_i= δ(μ[х], t_j)_i. Дуга помечается запущенным переходом t_j, которая направляется от вершины х к вершине z дерева достижимости. Вершина z помечается как граничная. После просмотра всех переходов, которые можно запустить при маркировке μ[х], вершина х помечается как внутренняя.

Прекращение работы алгоритма осуществляется тогда, когда в дереве достижимости не останется граничных вершин.

Основным свойством алгоритма построения дерева достижимости является то, что он заканчивает свою работу.

Для доказательства этого необходимо показать, что алгоритм не может создавать новых граничных вершин бесконечно. Доказательство основано на трёх леммах.

Лемма 1.

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

Лемма 2.

Всякая бесконечная последовательность неотрицательных целых чисел содержит бесконечную неубывающую подпоследовательность.

Лемма 3.

Всякая бесконечная последовательность n-мерных векторов, содержащих элементы как неотрицательные целые числа , содержит бесконечную неубывающую подпоследовательность.

Теорема: дерево достижимости сети Петри конечно.

Доказательство:

Предположим противное, т.е. существует бесконечное дерево достижимости. Тогда, согласно Лемме 1, в нём имеется бесконечный путь х₀,х₁,х₂,…, исходящий из корня х_0. Тогда мы имеем μ[х₀], μ[х₁], μ[х₂],…, бесконечную последовательность n-мерных векторов со значениями, которые определены в Лемме 3. Согласно ей должна существовать бесконечная неубывающая подпоследовательность . Но, согласно алгоритму, мы не можем иметь ситуации, что , поскольку одна из этих вершин была бы дублирующей и не имела бы продолжений. Таким образом, мы имеем последовательность строго возрастающих маркировок . Но по построению дерева достижимости, если , то нам следует заменить хотя бы одну компоненту маркировки на символ ω.

Таким образом, для имеющейся последовательности мы имеем, что содержит, по крайней мере, один символ ω. - по крайней мере, два символа ω и т.д. Т.е. не далее, чем маркировка содержит все n символов ω, а это означает, что следующая маркировка подпоследовательности уже не может быть строго больше, чем . Полученное противоречие доказывает конечность дерева достижимости.

Использование дерева достижимости позволяет решать поставленные ранее задачи анализа сетей Петри. Для этого необходимо будет просмотреть узлы дерева достижимости.