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




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


События с действием а в t1'  или t2'  в ходах работы, описанных с помощью агента

(t1' || t2' ) || (p; v)    с :: р; v; с, полностью линейно упорядочены. При таком способе действий для обеспечения взаимных исключений возникают агенты, которые обнаруживают дополнительные возможные тупики - в случае, когда в агенте t1 или t2 в параллельных композициях действие а должно выполняться синхронно.

Лемма (взаимное исключение). Для любого агента t, в котором действие а всегда встречается в виде р; а; v и иначе действия р и v не встречаются, справедливо, что каждый из процессов, порождаемых агентом не содержит никакой пары параллельных событий, помеченных действием а.

Доказательство. Пусть р' - процесс, порождаемый агентом t'. События, которые помечены действиями р или v, образуют последовательный подпроцесс, в котором р и v чередуются. Каждому событию е, помеченному через а, может быть однозначным образом предписано натуральное число событий, которые являются причиной для е и которые помечены через v, соответственно через р. Каждому событию е, помеченное через а, можно однозначно предписать помеченное через р событие еrp(е), которое является причиной для е, а также помеченное через v событие еry(е), для которого е является причиной.




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