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



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


t[ x::t/x ] 

 t0 => x::t
 t0.

Теперь через определенное выше отношение каждому агенту можно предписать множество процессов. Процесс р называется (несовершенным) ходом работы агента t0, если существует агент t1.

t0

 t1.

Множество ходов работ является замкнутым относительно образования префиксов.

Лемма (закон разложения). Если для агентов t0, t2 и конечного процесса р справедливо высказывание

t0

t2,

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

 р существует агент t1 такой, что

t0

t1, t1
 t2,

Доказательство - индукцией по числу событий в p1.

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

Предложение (связывание процессов). Если для агентов t1, t2, t3

и процессов р0, p1  справедливо высказывание

t1

 t2 ^ t2 
 t3,

то существует процесс р2 такой, что t1

 t3.

Доказательство, индукцией по структурам агентов.

Агент t0 называется терминальным, если для любого агента t1

высказывание

t0

 t1

справедливо только с пустым процессом р. Таким образом, терминальный агент может осуществлять переходы только с пустым процессом, т. е. не выполняя каких-либо действий.

Процесс р называется совершенным ходом работы агента t0, если для терминального агента t1 справедливо:

t0

 t1

или же процесс р является бесконечным и каждый его префикс р1

 р является ходом работы.

Два агента называются эквивалентными,

если они обладают одинаковыми множествами совершенных ходов работы.

К анализу агентов можно поставить такие же вопросы, какие ставятся и для сетей Петри. Концепция сети Петри с конкретизациями заменяется концепцией агентов. Тем самым агенту соответствует при сетях пара (N, b), причем N представляет сеть, a b - ее конкретизацию. В случае сетей только рассматривается отношение переходов на конкретизациях, так как сеть оставляет переходы неизменными.

Для агента t0 агент t1 называется достижимым, если существует процесс р такой, что t0

 t1




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