Множество достижимости

Состояние сети Петри определяется ее маркировкой. Запуск перехода изменяет состояние сети Петри посредством изменения маркировки сети. Пространство состояний сети Петри, обладающей п позициями, есть множество всех маркировок, т. е. Nⁿ.Изменение в состоянии, вызванное запуском перехода, определяется функцией изменения δ, которую мы назовем функцией следующего состояния. Когда эта функция применяется к маркировке μ (состоянию) и переходу t_j она образует новую маркировку μ ' (состояние), которая получается при запуске перехода t_j в маркировке μ. Так как t_j может быть запущен только в том случае, когда он разрешен, то функция δ(μ, t_j) не определена, если t_j не разрешен в маркировке μ.

Если же t_j разрешен, то δ(μ, t_j) = μ', где μ ' есть маркировка полученная в результате удаления фишек из входов t_j и добавления фишек в выходы t_j.

Определение 8. Функция следующего состояния δ для сети Петри С = (Р, Т, I, О) с маркировкой µ и переходом t_j Є Т определена тогда и только тогда, когда µ(р_i) = > #(р_i) для всех р_i Є Р. Если δ(µ, t_j) определена, то δ(µ, t_j) = µ '= µ(p_i) - #(p_i,I (t_j)) + #(p_i,O(t_j)) для всех р_i Є Р.

Пусть дана сеть Петри С = (Р, Т, I, О) с начальной маркировкой µ₀. Эта сеть может быть выполнена последовательным запуcком переходов. Запуск разрешенного перехода t_j в начальной маркировке образует новую маркировку µ¹ = δ(µ, t_j). В этой новой маркировке можно запустить любой другой разрешенный переход, например t_k, образующий новую маркировку µ ² = δ(µ¹, t_k). Этот процесс будет продолжаться до тех пор, пока в маркировке будет существовать хотя бы один разрешенный переход. Если же получена маркировка, в которой ни один переход не разрешен, то никакой переход не может быть запущен, функция следующего состояния не определена для всех переходов, и выполнение сети должно быть закончено.

При выполнении сети Петри получаются две последовательности: последовательность маркировок (µ⁰, µ¹, µ²,...) и последовательность переходов, которые были запущены (t_j0, t_j1, t_j2,...). Эти две последовательности связаны следующим соотношением: δ(µ^k, t_jk) = µ ^k+1 для k = 0, 1, 2,.... Имея последовательность переходов и µ⁰, легко получить последовательность маркировок сети Петри, а имея последовательность маркировок, легко получить последовательность переходов. Таким образом, обе эти последовательности представляют описание выполнения сети Петри.

Пусть некоторый переход в маркировке µ разрешен и, следовательно, может быть запущен. Результат запуска перехода в маркировке µ есть новая маркировка µ'. Говорят, что µ ' является непосредственно достижимой из маркировки µ, иными словами, состояние µ' непосредственно получается из состояния µ.

Определение 9. Для сети Петри С = (Р, Т, I, О) с маркировкой µ маркировка µ' называется непосредственно достижимой из µ, если существует переход t_j Є Т такой, что µ' = δ(µ, t_j).

Можно распространить это понятие на определение множества достижимых маркировок данной маркированной сети Петри. Если µ' непосредственно достижима из µ, а µ" — из µ', говорят, что µ " достижима из µ. Определим множество достижимости R(C,µ) сети Петри С с маркировкой µ' как множество всех маркировок, достижимых из µ. Маркировка µ' принадлежит R(C,µ), если существует какая-либо последовательность запусков переходов, изменяющих µ на µ'. Отношение «достижимости» является рефлексивным, транзитивным замыканием отношения «непосредственной достижимости».

Определение 10. Множество достижимости R(C, µ) для сети Петри С = (Р, Т, I, О) с маркировкой µ есть наименьшее множество маркировок, определенных следующим образом:

Рис. 2.20. Маркированная сеть Петри.

Удобно распространить функцию следующего состояния на отображение маркировки и последовательности переходов в новую маркировку. Для последовательности переходов (t_j1, t_j2 ,...., t_jk) и маркировки µ' маркировка µ' = σ(t_j1, t_j2 ,...., t_jk) есть результат запусков: сначала - t_j1 затем - t_j2 и т.д. до t_jk. (Такая операция, конечно, возможна только в том случае, если каждый переход к моменту его запуска разрешен.)

Определение 11. Расширенная функция следующего состояния σ(t_j1, t_j2 ,...., t_jk) определяется для маркировки µ⁰ и последовательности переходов t_j0, t_j1 ,...., t_jk следующими соотношениями: δ(µⁱ, t_ji) = µ ⁱ⁺¹ для i = 0, 1, 2,....

Обычно мы применяем эту расширенную функцию.