Конспект установочных лекций по комплексному курсу Информатика, Теория информации
Сети Петри - часть 8
t[ x::t/x ]
Теперь через определенное выше отношение каждому агенту можно предписать множество процессов. Процесс р называется (несовершенным) ходом работы агента t0, если существует агент t1.
t0
Множество ходов работ является замкнутым относительно образования префиксов.
Лемма (закон разложения). Если для агентов t0, t2 и конечного процесса р справедливо высказывание
t0
то для каждого префикса р1
t0
Доказательство - индукцией по числу событий в p1.
Закон разложения означает, что осуществляемые с помощью процессов переходы также могут быть разложены в следующие друг за другом переходы, причем эти последние осуществляются подпроцессами исходного процесса. Справедливо также и обратное утверждение.
Предложение (связывание процессов). Если для агентов t1, t2, t3
и процессов р0, p1 справедливо высказывание
t1
то существует процесс р2 такой, что t1
Доказательство, индукцией по структурам агентов.
Агент t0 называется терминальным, если для любого агента t1
высказывание
t0
справедливо только с пустым процессом р. Таким образом, терминальный агент может осуществлять переходы только с пустым процессом, т. е. не выполняя каких-либо действий.
Процесс р называется совершенным ходом работы агента t0, если для терминального агента t1 справедливо:
t0
или же процесс р является бесконечным и каждый его префикс р1
Два агента называются эквивалентными,
если они обладают одинаковыми множествами совершенных ходов работы.
К анализу агентов можно поставить такие же вопросы, какие ставятся и для сетей Петри. Концепция сети Петри с конкретизациями заменяется концепцией агентов. Тем самым агенту соответствует при сетях пара (N, b), причем N представляет сеть, a b - ее конкретизацию. В случае сетей только рассматривается отношение переходов на конкретизациях, так как сеть оставляет переходы неизменными.
Для агента t0 агент t1 называется достижимым, если существует процесс р такой, что t0