Алгебраическая сеть Петри
Алгебраическая сеть Петри (англ. algebraic Petri net, APN) — расширение обычных сетей Петри, в котором обычные маркеры заменены на элементы алгебраических типов данных[1]. Этот формализм во многом подобен раскрашенным сетям Петри[2], однако в случае алгебраических сетей семантика типов данных задаётся системой аксиом, позволяющей осуществлять с её использованием доказательства и вычисления над типами.
Впервые введены Жаком Вотереном в 1985 году[3], усовершенствованы Вольфгангом Райзигом[4].
Формализм включает две составляющие:
- управляющую часть, задаваемую сетью Петри;
- часть данных, задаваемую одним или несколькими алгебраическими типами данных.
Сами алгебраические типы данных могут быть разделены на две части:
- сигнатура, которая задаёт допустимые константы и операции в алгебре термов[англ.].
- аксиоматизация, задающая семантику операций, определённых сигнатурой.
Управляющая часть включает:
- позиции, содержащие мультимножества маркеров; маркеры являются элементами алгебры термов, построенной с использованием сигнатуры, каждая позиция содержит одно и только одно мультимножество термов, позиция типизирована приписанным ей мультимножеством;
- дуги могут быть отмаркированы мультмножествами определённых или свободных термов, также как и для позиций, термы определяются из алгебраических типов сигнатуры;
- переходы — это события, которые активируются каждый раз, когда достаточно маркеров во входных позициях, чтобы переместить маркер по каждой из входных дуг и, одновременно, выполняется условие активации (защита) перехода.
В момент активации события произведённые маркеры перемещаются в целевые позиции выходных дуг. Для того, чтобы определить семантику операций, проверить выполняются ли заданные условия и вычислить выходные термы, как правило используют техники переписывания термов[5].
Алгебраические сети Петри послужили базой для развития более сложных вариантов того же формализма, в частности CO-OPN[англ.] (Concurrent Object-Oriented Petri Nets).
Пример
[править | править код]Пример алгебраической сети Петри, предназначенной для моделирования задачи об обедающих философах:
Используются два алгебраических типа данных. Один из них (Fork
) задаёт алгебру вилок, другой (Philosopher
) — алгебру философов. Поскольку все философы могут взять левую вилку, не взяв правую, выполнение этой модели может привести ко взаимной блокировке. На старте работы модели возможен только переход goEat
. Если хотя бы один goEat
был активирован, разрешёнными становятся также переходы takeL
и takeR
.
Примечания
[править | править код]- ↑ Ehrig, Hartmut. Fundamentals of Algebraic Specification 1 : Equations and Initial Semantics (англ.). — Berlin: Springer Berlin Heidelberg, 1985. — 321 p. — ISBN 978-3-642-69962-7, 3-642-69962-6, 978-3-642-69964-1, 3-642-69964-2. Архивировано 4 сентября 2020 года.
- ↑ 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.