Анализ сетей Петри на основе матричных уравнений

Матричный подход основывается на представлении сети двумя матрицами Д^- и Д⁺, представляющими входную и выходную функции сети. Каждая матрица имеет m строк (по одной на переход) и n столбцов (по одному на позицию). Определим Д^-(j,i)=K(P_i,I(t_j)), а Д⁺(j,i)=K(P_i,O(t_j)). Д^- определяет входы в переходы, Д⁺ - выходы. K – кратность позиции по входам и выходам.

Введём m - вектор e(j), содержащий нули везде, за исключением j-й компоненты. Переход t_j представляется m - вектором e(j).

Тогда переход t_j в маркировке М разрешён, если М≥e(j)Д^-, а результат запуска перехода t_j в маркировке М записывается как:

δ(M,t_j)=M - e(j) Д^- + e(j) Д⁺ = M+ e(j)(- Д^- + Д⁺) = M + e(j)Д

где Д = Д⁺ - Д^- - составная матрица изменений.

Тогда для последовательности запусков переходов G = t_j1, t_j2,…, t_jk имеем

δ(M,G) =δ(M, t_j1, t_j2,…, t_jk) = M + e(j₁)Д + e(j₂)Д + … + e(j_k)Д =

= M +[ e(j₁) + e(j₂) + … + e(j_k)]Д = M + f(G)Д (1)

Вектор f(G) = e(j₁)+e(j₂) …..+e(j_k) называется вектором запуска последовательности t_j1,t_j2,…,t_jk. i-й элемент вектора f(G), f(G)_i - это число запусков перехода t_j в последовательности t_j1,t_j2,…,t_jk. Вектор запусков, следовательно, является вектором с неотрицательными целыми компонентами.

Рассмотрим задачу сохранения при известном векторе взвешивания меток W. Если M₀ - начальная маркировка, а M’ - произвольная достижимая маркировка, необходимо, чтобы M₀W = M’W. Тогда существует последовательность запусков переходов G, которая переводит сеть из M₀ в M’. Поэтому

M’ = δ(M₀,G) = M₀ + f(G)Д

Следовательно, M₀W = M’W = (M₀ + f(G) Д) W = M₀W + f(G) ДW, поэтому f(G)ДW = 0.

Поскольку это должно быть верно для всех f(G), имеем ДW = 0.

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

Матричная теория является инструментом для решения проблемы достижимости. Пусть маркировка M’ достижима из M₀, тогда существует последовательность (возможно пустая) запусков переходов G, которая приводит из M₀ к M’. Это означает, что f(G) является неотрицательным целым решением следующего матричного уравнения для X:

M’ = M₀ + X Д (*)

Следовательно, если M’ достижима из M₀, тогда уравнение (*) имеет решение в неотрицательных целых; если уравнение не имеет решения, тогда M’ недопустима из M₀.

ПРИМЕР:

Д^- =

Д⁺=

	-1	-1
	+2	+1	-1
		-1	+1

Д = Д⁺ - Д^- =

В начальной маркировке M₀=(1,0,1,0) переход t₃ разрешён и приводит к маркировке M’, где:

	-1	-1
	+2	+1	-1
		-1	+1

M’=(1,0,1,0)+(0,0,1) =(1,0,1,0)+(0,0,-1,+1)=(1,0,0,1)

Последовательность G= t_­­3 t_­­2 t_­­3 t_­­2 t_­­1 представляется вектором запусков f(G)=(1,2,2) и получает маркировку M’:

	-1	-1
	+2	+1	-1
		-1	+1

M’ = (1,0,1,0) + (1,2,2) =(1,0,1,0) +(0,3,-1,0) = (1,3,0,0)

Для определения того, является ли маркировка (1, 8, 0, 1) достижимой из маркировки (1, 0, 1, 0), имеем уравнение

	-1	-1
	+2	+1	-1
		-1	+1

(1, 8, 0, 1) = (1, 0, 1, 0) + X

	-1	-1
	+2	+1	-1
		-1	+1

(0,8,-1,1)= X

которое имеет решение X=(0, 4, 5). Это соответствует последовательности G= t₃ t₂ t₃ t₂ t₃ t₂ t₃ t₂ t₃.

Можно показать, что маркировка (1, 7, 0, 1) недостижима из маркировки (1, 0, 1, 0) поскольку матричное уравнение

	-1	-1
	+2	+1	-1
		-1	+1

(1,7,0,1)=(1,0,1,0) + X

	-1	-1
	+2	+1	-1
		-1	+1

(0,7,-1,1)= X

не имеет решения.