ПРОГРАММИРОВАНИЕ, 2015, No 3, с. 20-31
- ПЕРСПЕКТИВЫ СИСТЕМ ИНФОРМАТИКИ -
УДК 519.681
КОМПАРАТИВНАЯ ТРАССОВАЯ СЕМАНТИКА ВРЕМЕННЫХ
СЕТЕЙ ПЕТРИ *
© 2015 г. Д.И. Бушин*, И.Б. Вирбицкайте* **,
* Институт систем, информатики СО РАН, 630090 Новосибирск, пр. Ак. Лаврентьева, 6 **Новосибирский государственный университет, 630090 Новосибирск, ул. Пирогова, 2
E-mail: virb@iis.nsk.su, dima.bushin@gmail.com Поступила в редакцию 01.12.2014
В данной работе определяется и исследуется семейство трассовых эквивалентностей в иптерли-винговой, шаговой, частичпо-упорядочеппой и недетерминированной семантиках в контексте временных безопасных сетей Петри. Изучаемые эквивалентности основываются как на классическом понятии последовательностей срабатываний переходов, так и на временных процессах, т.е. временных расширениях сетей-процессов за счет сопоставления глобальных моментов времени срабатываниям переходов. Устанавливаются взаимосвязи эквивалентностей и строится иерархия классов эквивалентных временных сетей Петри.
1. ВВЕДЕНИЕ
Поведенческие эквивалентности обычно используются при спецификации и верификации систем с целью сравнения их поведения, а также упрощения их структуры. В теории параллельных систем и процессов известно большое разнообразие поведенческих эквивалентностей, взаимосвязи между которыми хорошо изучены в литературе (см., например, [1]). Трассовые эквивалентности являются базовыми и позволяют сравнивать поведения систем в терминах их языков. В интерливинговой семантике язык — это множество последовательностей действий, выполняемых системой. Однако такое представление поведения не позволяет судить о степени параллелизма и недетерминизма, присущих системам. Было сделано много попыток выйти за пределы интерливингового подхода, что привело к появлению эквивалентностей, базирующихся на "истинно параллельной" и недетерминированной семантиках (см., например, [2, 3, 4]), которые позволяют лучше понять природу и установить закономерности процессов, про-
*Данная работа частично финансируется DFG
и РФФИ (проект CAVER, грант N BE 1267/14-1, грант No 14-01-91334).
текающих в параллельных/распределенных системах.
Отправной точкой в исследованиях по неин-терливинговым семантикам в контексте моделей сетей Петри (СП) стала статья [5], где были показаны тесные взаимосвязи между моделями сетей-процессов и первичных структур событий. В 1980-х годах наиболее активно изучались особенности и свойства семантики сетей-процессов различных подклассов СП (см., например, [6, 7]). В 1990-м году авторы статьи [8] показали, что такие семантические представления, как сети-процессы, трассы Мазуркеви-ча, частично упорядоченные множества, первичные структуры событий, совпадают с точностью до изоморфизма в контексте безопасных СП. Семантика локальных структур событий, которые являются обобщением первичных структур событий и базируются на понятии шагов — множеств параллельно выполняемых действий — была разработана для СП в статье [9]. Далее асимметричные структуры событий контекстных СП были построены в [10]. Кроме того, семантики решеток и структур событий были предложены в работе [11] в контексте СП с ин-гибиторными дугами. В статьях в [12, 13, 14, 15] представлены новые методы построения и изуче-
ния семантики сетей-процессов на основе последовательностей шагов параллельных переходов для СП и их ингибиторных обобщений.
Функционирование реальных параллельных систем в значительной степени зависит от временных параметров, поэтому многие модели СП были обогащены понятием времени, что позволило описывать и исследовать не только качественные, но и количественные аспекты поведения систем. Однако введение и изучение временных характеристик в более абстрактные (семантические) "истинно-параллельные" и недетерминированные модели были не настолько активными. Семантика моделей сетей-процессов, включающих события и условия, находящиеся в отношениях причинной зависимости и параллелизма, была предложена в работе [16] для временных ограниченных СП, где с каждым переходом связана длительность его срабатывания, а также в статье [17] для временных безопасных СП, где каждому переходу сопоставлен интервал временных задержек его срабатывания. В более поздних работах (см., например, [18]) была исследована семантика сетей-процессов, расширенных отношением недетерминированного выбора (конфликта), где с каждым событием связан временной интервал его выполнения, для временных ограниченных ординарных СП. Однако, насколько нам известно, в литературе не представлены исследования по семантике структур событий (моделей, в которых события находятся в отношениях причинной зависимости, параллелизма и конфликта) временных расширений СП. Кроме того, в контексте временных моделей также практически не изучались и поведенческие эквивалентности. Исключением является статья [19], где тестовые эквивалентности были введены и исследованы для СП с временными характеристиками, сопоставленными фишкам и с временными интервалами, связанными с дугами из мест в переходы.
В данной работе для временных безопасных СП определяется и исследуется семейство трассовых эквивалентностей в интерливинговой, шаговой, частично-упорядоченной и недетерминированной семантиках. Устанавливаются взаимосвязи эквивалентностей и строится
иерархия классов эквивалентных временных сетей Петри.
Оставшаяся часть статьи организована следующим образом. В разделе 2 вводятся основные понятия и обозначения, связанные со структурой и интерливинговой/шаговой семантикой, построенной на состояниях временных СП. Определения базовых семантических представлений — временных расширений частично упорядоченных множеств, структур событий и сетей-процессов — приводятся в разделе 3. В разделе 4 данные семантики изучаются в контексте временных СП. Взаимосвязи трассовых эквивалентностей исследуются в заключительном разделе 5.
2. ВРЕМЕННЫЕ СЕТИ ПЕТРИ
Рассмотрим ряд понятий, связанных со структурой и поведением временной сети Петри (ВСП) [17]. Под ВСП понимается элементарная сетевая система, в которой с каждым переходом связан временной интервал, указывающий моменты времени, когда переход, готовый по наличию фишек в его входных местах, может сработать, только если достигнута нижняя граница интервала, и обязан сработать, если достигнута верхняя граница интервала.
Область T временных значений — множество натуральных чисел. Считаем, что [ti,7"2] — замкнутый интервал между двумя временными значениями Ti,T2 £ T. Бесконечность может появляться как правая граница в открытых справа интервалах. Пусть Interv — множество всех таких интервалов. Кроме того, множество Act обозначает алфавит действий.
Act
пая сеть Петри — это кортеж TN = ((P, T, F, Ы0, L), D), где (P,T,F,M0,L) - сеть Петри с множеством P мест, множеством T переходов (P П T = 0), отношением инцидентности F С (P х T) U (T х P); начальной разметкой 0 = Mo С P. помечающей функцией L : T ^ Act и D : T ^ Interv — статическая временная функция, связывающая с каждым, переходом временной интервал.
Введем ряд вспомогательных понятий и обозначений. Для элемента x £ P U T пусть
•х = {у | (у, ж) е Е} и = {у | (ж, у) е Е} -множества его входных и выходных элементов соответственно. Для подмножества X С Р иТ^^^^^^м множества •Х = и•х и X• = УхеХ х\ Для перехода г е Т границы интервала называются ранним временем
Е/г и поз^нм^ временем срабатывания
данного перехода.
Любое подмножество М С Р — разметка ВСП ТМ Переход г является готовым при разметке М, если С М. Пусть Еп(М) — множество готовых переходов при М. Тогда 0 = и С Т — шаг, готовый при разметке ^^и е и ♦ ♦г е Еп(М)) и = г' е и ♦ п •г' = 0).
Рассмотрим поведение ВСП ТМ. Состояние ВСП ТМ ^ это тройка (М, I, СТ), где М — разметка, I : Еп(М) —^ Т — динамическая временная функция и СТ е Т — момент глобального времени. Начальное состояние ВСП ТМ — это тройка Бо = (Мо, 1о, СТо), где Мо — начальная разметка, 1о(г) = 0 для всех г е Еп(Мо) и СТо = 0.
Шаг и С Т, готовый при разметке М, может выполниться, из состояния Б = (М, I, СТ) после временной задержки в е Т, если верно: (V* е и ♦ Е/г(г) < I(г) + в) и (м7 е Еп(М) ♦ ♦ I(г')+ в < Пусть Сопгасг(Б) = {г е
е и | шаг и может выполниться из состояния Б = (М, I, СТ) после временной задержки в е Т и (М \ •г) п -г = 0)}.
Если шаг и может выполниться из состояния Б = (М, I, СТ) после временной задержки
ви
Б' = (М', I', СТ'), которое определяется следующим образом:
• М' = (М \ •и) и и•,
7(г') + в, если г' е
Еп(М \ •и), если г' е Еп(М')\ Еп(М \ •и), иначе,
TN
Vt' е T. I'(t') = <
void,
GT' = GT + в.
(Ufi)
S' а также
Б
Б ^ Б', если А = Ь(и) = ^геи Ь(г). Конечная или бесконечная последовательность вида:
S = s0 s1
(U2,02) С2
Б2 ... — шаговая последовательность выполнений ВСП ТМ из состояния Б. Тогда (и1,в1) (и2,в2) ... — шаго-
[1, 3] с__[2, 3]
РзО Р4 t^_[1,1] [0, 5]
___) t5
P6
Рис. 1.
вое расписание выполнений ВСП ТМ из Б. Эта последовательность называется интерливинго-вым расписанием выполнений ВСП ТМ из Б, если |и^ | = 1 для всех г > 1. Определим шаговый (интерливинговый) язык ВСП ТМ следующим образом: £^)(ТМ) = {(Аь в1) ... (Ак, вк) | | к > 0 (и1,в1) ... (ик,вк) — шаговое (интерлп-
ТМ
Бои Ак = Ь(ик)}•
Б ТМ
м,ы,м,, если оно присутствует в некоторой шаго-
ТМ
из начального состояния Бо- Пусть ДБ (ТМ) обозначает множество достижимых состояний ВСП ТМ ТМ Т
для любого перехода г е Т верно, что •г = 0 = свободной от контактов, если для всех состояний Б е ДБ (ТМ) верно, что Сопгасг(Б) = 0; прогрессирующей по времени, если в каждом беско-
( и1 , в1 )
(и2,в2) (и3,в3) .. .ВСП ТМ го некоторого Б е е ДБ (ТМ) последовательность в1 + в2 + в3 + ... дпвергирует. В дальнейшем будем рассматри-Т
тактов и прогрессирующие по времени ВСП и называть их просто ВСП.
Пример 1. Рисунок 1 показывает, пример ВСП ТМ. Обе последователь ноет,и а = ({г1,г4}, 3) и а' = ({¿174, 3)(^2}, 1)({*з }, 1)(Ы, 2)... являются шаговыми расписаниями выпол-
ТМ
Бо = (Мо,!о,СТо), где
о, еслм г е {г1,г3, г4},
Mo = {P1,P2} io(t) = « GTo = 0.
,
Кроме того, а = ({¿2}, 1)№э}, 1)({*б}, 2)... -шаговое расписание выпо
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.