Конспект установочных лекций по комплексному курсу Информатика, Теория информации



         

Сети Петри - часть 4


b

b.

(2)        Пусть р = (Е0, ?0, ?) - процесс с тривиальным причинным порядком, в котором различные события являются причинно независимыми.

Для процесса р справедливо следующее:

e, d
 Е0: e ?0 d
e = d.

Тогда  для конкретизации b0 и b1

отношение

b0

b1

справедливо только тогда, когда все события в р помечены по-разному и потому справедлива следующая формула:

e, d
 Е0: e ? d
 ?(e) ? ?(d),

и множество К = { ?(e): e

 Е0 } для конкретизации b0

готово к передаче и ведет к последующей конкретизации b1.

(3)        Для каждого процесса р = (Е0, ?0, ?), который не удовлетворяет условиям (1) или (2), отношение

b0

b2

справедливо только тогда, когда для каждого непустого префикс-процесса

р1 = (Е1, ?1, ?1) со свойством

р1

 р ^ p1 ? p

существует такая конкретизация b1, что для процесса р2 = р | E0\E1

справедливо следующее высказывание:

b0

b1

^ b1

b2

Это определение принимает во внимание в пункте (2) то обстоятельство, что вентили в сети Петри рассматриваются только как последовательные единицы. Параллельные события всегда маркируются различными вентилями.

а

с

b

e

Для каждого конечного процесса р и каждой конкретизации b0 через

b0

b1

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

Лемма. Если для процесса р = (Е0, ?0, ?) и конкретизации b0 и b1 справедливо высказывание

b0

b1,

то для каждого префикса р1

процесса р с множеством событий Е1 справедливо следующее высказывание: для каждого множества событий Е2, которое является минимальным относительно ?0 в Е0\Е1, справедливо, что множество { ?(e): e

 Е2} является готовым к передаче.

Доказательство. Подпроцесс в р, который состоит только из событий из Е2, для конкретизации b1 является ходом работы.

Лемма.

Если процесс р есть ход работы сети N с исходной конкретизацией b0, то каждый префикс-процесс р1

 р есть ход работы сети N с исходной конкретизацией b0.

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


Содержание  Назад  Вперед