Conference publications

Abstracts

XXII conference

Замечание о сетях Петри с состояниями

Белов Ю.А.

150049, Ярославль, ул. С-Щедрина, д. 59, кв. 12

Автоморфизмы моделей Крипке были предложены в [1]. Аналогичные свойства симметрии для сетей Петри и векторных систем сложения (VAS, VASS) изучались автором, где были отмечены также некоторые результаты о группах автоморфизмов этих систем. В работах F. Avellaneda and R. Morin (2012 г.) предложена более общая модель – сеть Петри с (управляющими) состояниями -- (PNS). Естественно попробовать перенести отмеченные результаты на общий случай.

Определения. Пусть имеется конечное множество P, элементы которого называются позициями, |P|=n – размерность сети. Маркировка μ сети – мультимножество над P. Можно считать, что множество всех маркировок есть Nn, где N={0, 1, 2, …k…} -- множество натуральных чисел и μ ϵ Nn -- распределяет фишки по позициям. Далее определим конечное множество R правил переходов – R  LNnNn; здесь L—конечное множество символов -- имён (меток), и любое правило есть тройка r=(λ,α,β ) ϵ R, записываемое обычно так: λ: α→β. Здесь α=in(r), β=out(r) –векторы поглощения и производства при данном переходе r соответственно. Переход r называется активным при данной маркировке μ, если μ⩾ in(r), (т.е. (μ-α) ϵ Nn).

Определение. PNS (Petri Net with States) с множеством правил R есть четвёрка

D=(i, μ0, Q, T). Здесь R – определено ранее, Q – абстрактное конечное множество управляющих состояний, i ϵ Q -- начальное состояние, μ0 ϵ Nn – начальная маркировка; T  QRQ – конечное множество дуг (переходов), помеченных правилами из R.

D определяет следующий механизм преобразования конфигураций: пусть имеется текущая конфигурация (q, μ). Тогда, если существуют r ϵ R и q׳ ϵ Q такие, что дуга (q, r, q׳) ϵ T, то от конфигурации (q, μ) можно перейти к конфигурации (q׳, μ׳), где μ׳= μ—in(r)+out(r), если переход r активен в исходной маркировке μ. В таком случае переход по дуге (q, r, q׳) называется допустимым и обозначается q □(→┴r ) q'. Если задана сеть D, то определяется множество достижимых маркировок M – это множество маркировок, которые могут быть получены из начальной конфигурации (i, μ0) за конечное число допустимых переходов.

Автоморфизмом сети D называется пара биекций h=(f, g), где f: M → M, g: Q → Q, таких что q □(→┴r ) q' тогда и только тогда, когда g(q) □(→┴(f(r)) ) g(q'). Покомпонентно определяется суперпозиция автоморфизмов и относительно этой операции множество всех автоморфизмов Aut(D) является группой. Можно построить примеры таких PNS, для которых группа Aut(D) бесконечна.

Литература

Э.М. Кларк мл., О. Грамберг, Д. Пелед Верификация моделей программ М., МЦНМО, 2002, 414 стр.

• view as PDF (in Russian) (PDF)