Русская Википедия:Алгебраическая сеть Петри
Шаблон:Не путать Алгебраическая сеть Петри (Шаблон:Lang-en) — расширение обычных сетей Петри, в котором обычные маркеры заменены на элементы алгебраических типов данных[1]. Этот формализм во многом подобен раскрашенным сетям Петри[2], однако в случае алгебраических сетей семантика типов данных задаётся системой аксиом, позволяющей осуществлять с её использованием доказательства и вычисления над типами.
Впервые введены Жаком Вотереном в 1985 году[3], усовершенствованы Вольфгангом Райзигом[4].
Формализм включает две составляющие:
- управляющую часть, задаваемую сетью Петри;
- часть данных, задаваемую одним или несколькими алгебраическими типами данных.
Сами алгебраические типы данных могут быть разделены на две части:
- сигнатура, которая задаёт допустимые константы и операции в Шаблон:Iw.
- аксиоматизация, задающая семантику операций, определённых сигнатурой.
Управляющая часть включает:
- позиции, содержащие мультимножества маркеров; маркеры являются элементами алгебры термов, построенной с использованием сигнатуры, каждая позиция содержит одно и только одно мультимножество термов, позиция типизирована приписанным ей мультимножеством;
- дуги могут быть отмаркированы мультмножествами определённых или свободных термов, также как и для позиций, термы определяются из алгебраических типов сигнатуры;
- переходы — это события, которые активируются каждый раз, когда достаточно маркеров во входных позициях, чтобы переместить маркер по каждой из входных дуг и, одновременно, выполняется условие активации (защита) перехода.
В момент активации события произведённые маркеры перемещаются в целевые позиции выходных дуг. Для того, чтобы определить семантику операций, проверить выполняются ли заданные условия и вычислить выходные термы, как правило используют техники переписывания термов[5].
Алгебраические сети Петри послужили базой для развития более сложных вариантов того же формализма, в частности Шаблон:Iw (Шаблон:Lang-en2).
Пример
Пример алгебраической сети Петри, предназначенной для моделирования задачи об обедающих философах:
Используются два алгебраических типа данных. Один из них (Fork) задаёт алгебру вилок, другой (Philosopher) — алгебру философов. Поскольку все философы могут взять левую вилку, не взяв правую, выполнение этой модели может привести ко взаимной блокировке. На старте работы модели возможен только переход goEat. Если хотя бы один goEat был активирован, разрешёнными становятся также переходы takeL и takeR.
Примечания
- ↑ Шаблон:Книга
- ↑ Jensen K. Coloured Petri Nets — Berlin: Springer-Verlag, 1997. — 236 p.
- ↑ Vautherin J. Parallel systems specifications with Coloured Petri nets and algebraic specifications. European Workshop on Applications and Theory of Petri Nets — Berlin, N.Y.: Springer-Verlag, 1987. — P. 293—308.
- ↑ Reisig W. Petri Nets and Algebraic Specifications // Theor. Comput. Sci. — 1991. — Vol. 80. — № 1. — P. 1—34.
- ↑ Dick A. J., Watson P. Order-sorted term rewriting // Comput. J. — 1991. — Vol. 34. — № 1. — P. 16—19.
