Алгебраическая сеть Петри
Алгебраическая сеть Петри ( APN ) — это развитие хорошо известной сети Петри , в которой элементы определяемых пользователем типов данных (называемых алгебраическими абстрактными типами данных (AADT) [1] ) заменяют черные жетоны. Этот формализм можно сравнить с цветными сетями Петри (CPN). [2] во многих аспектах. Однако в случае APN семантика типов данных задается аксиоматизацией , позволяющей проводить доказательства и вычисления на ее основе.
Алгебраические сети Петри [3] были изобретены Жаком Вотереном в 1985 году в его докторской диссертации и позже усовершенствованы Вольфангом Райзигом. [4]
Формализм имеет два аспекта:
- Управляющая часть, обрабатываемая сетью Петри.
- Часть данных, которая обрабатывается одним или несколькими AADT.
AADT можно разделить на две части:
- Сигнатура термина (Sort и Ops в примере ниже), которая дает действительные константы и операции алгебра .
- Аксиоматизация (аксиомы в примере ниже) , которая дает семантику операций, описанных в сигнатурной части.
На следующем рисунке описана алгебраическая модель сети Петри « проблемы обедающих философов ». В этой модели есть два AADT: один для алгебры вилок, другой для алгебры философов. Обратите внимание, что AADT философов использует вилку AADT. Поскольку все философы могут пойти на левую вилку, не пойдя на правую, выполнение этой модели может привести к тупику .
В состав управляющей части входят:
- Места содержат мультинаборы (мешки) жетонов. Эти токены являются элементами алгебры терминов, построенной на основе сигнатуры AADT (в данном примере термины представляют либо философа, либо вилку). Каждое место содержит один и только один мультимножество терминов, место типизируется по своему мультимножеству.
- Дуги могут быть помечены мультимножествами закрытых или свободных терминов. Опять же, термины создаются на основе сигнатуры AADT.
- Переходы — это события, которые могут быть запущены всякий раз, когда имеется достаточно ресурсов (а именно, достаточно токенов во входных позициях, чтобы удовлетворить все входные дуги) и сохраняется защита (условия срабатывания) перехода. Затем произведенные фишки кладутся в целевые места выходных дуг. Обычно переписывание терминов [5] используется для операционной семантики, чтобы проверить выполнение условий и вычислить выходные условия.
В приведенном ниже примере только переход goEat в начале возможен один goEat . Был запущен , takeL и takeR также включены и, следовательно, также могут быть запущены.
Алгебраические сети Петри — это базовый формализм более продвинутых сетей, таких как CO-OPN .
Ссылки
[ редактировать ]- ^ Эриг, Х. и Мар, Б. 1985 Основы алгебраической спецификации I. Springer-Verlag New York, Inc.
- ^ К. Дженсен. Цветные сети Петри. Шпрингер, Берлин, 1996 г.
- ^ Жак Вотерен: Спецификации параллельных систем с цветными сетями Петри и алгебраическими спецификациями. Европейский семинар по приложениям и теории сетей Петри 1986: 293-308.
- ^ Вольфганг Райзиг: Сети Петри и алгебраические характеристики. Теор. Вычислить. наук. 80(1): 1-34 (1991)
- ^ Дик, А.Дж. и Уотсон, П. 1991. Переписывание терминов с сортировкой по порядку. Вычислить. Дж. 34, 1 (февраль 1991 г.), 16–19.
Дальнейшее чтение
[ редактировать ]- Вотерен, Жак (1985). Алгебраическая модель, основанная на сетях Петри, для изучения параллельных систем . Диссертация доктора технических наук, унив. из Парижа-Юг, Центр Орсе.
- Дженсен, Курт. Цветные сети Петри . Спрингер Верлаг. ISBN 3-540-62867-3 .
Внешние ссылки
[ редактировать ]