автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Теоретико-категорное исследование семантики областей Скотта параллельных моделей с реальным временем

003460565

На правах рукрписи

С

Дубцов Роман Сергеевич

ТЕОРЕТИКО-КАТЕГОРНОЕ ИССЛЕДОВАНИЕ СЕМАНТИКИ ОБЛАСТЕЙ СКОТТА ПАРАЛЛЕЛЬНЫХ МОДЕЛЕЙ С РЕАЛЬНЫМ ВРЕМЕНЕМ

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов, систем и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Новосибирск - 2008

003460565

Работа выполнена в Институте систем информатики им. А.П. Ершова Сибирского отделения Российской академии наук

Научный руководитель:

доктор физико-математических наук Вирбицкайте И.Б.

Официальные оппоненты: доктор физико-математических наук

Ломазова И.А.

доктор физико-математических наук,

профессор

Морозов A.C.

Ведущая организация:

Ярославский государственный университет имени П.Г. Демидова

Защита состоится 26 декабря 2008 года в 16 час. 00 мин. на заседании диссертационного совета К 003.032.01 в Институте систем информатики имени А.П. Ершова СО РАН по адресу: 630090, Новосибирск, пр. Ак. Лаврентьева, 6

С диссертацией можно ознакомиться в читальном зале библиотеки Института систем информатики СО РАН

Автореферат разослан 25 ноября 2008 г.

Ученый секретарь

специализированного совета К 003.032.01

к.ф.-м.н. ¡\ Мурзин Ф.А.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность. В настоящее время сфера применения аппаратных и программных систем с параллельной/распределенной архитектурой непрерывно расширяется, охватывая все новые области в самых различных отраслях науки, техники, образования, бизнеса и производства. К таким системам относятся коммуникационные протоколы, системы управления производством, распределенные операционные системы, параллельные базы данных и т.д. Параллельные/распределенные системы, как правило, состоят из большого числа компонентов со сложным характером взаимодействий, что затрудняет понимание природы протекающих в них разнообразных процессов. Проектирование и реализация корректных параллельных/распределенных систем возможны только при использовании формальных методов и средств, которые должны быть, с одной стороны, «дружественными» для разработчиков, а с другой - математически строгими, а также адекватно представлять структуру и поведение моделируемых систем.

Среди отечественных исследований по спецификации, моделированию и анализу сложных (в том числе, параллельных/распределенных) систем отметим работы H.A. Анисимова, О.Л. Бандман, И.Б. Вирбиц-кайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.Э. Малышкина, В.А. Непомнящего, А.К. Петренко, Р.Л. Смелянского, В.А. Соколова, Л.А. Черкасовой.

Теория параллельных систем и процессов — активно развивающаяся область компьютерных наук - изучает фундаментальные понятия и законы параллельной обработки информации и на основе обнаруженных закономерностей строит более частные формальные модели исследуемых объектов, на которых ставит и решает прикладные задачи. На основе результатов и рекомендаций теоретических исследований ведется поиск и проверка новых архитектурных принципов конструирования систем, изучаются методы распараллеливания алгоритмов и программ, разрабатываются новые конструкции параллельных языков программирования, проверяются способы анализа и верификации программных систем и т.д. За последние четыре десятилетия в теории параллелизма появилось большое разнообразие моделей и методов, предназначенных

для спецификации, разработки и верификации систем. Среди формальных структурных моделей следует отметить сети Петри, системы переходов, системы переходов с независимостью, автоматы высших порядков, 1/О-автоматы и т.д. Особое внимание в теории параллелизма отводится абстрактным семантическим моделям, позволяющим описывать и исследовать поведения параллельных систем. К таким моделям относятся деревья синхронизации, причинные деревья, структуры событий и т.д. Известно, что денотационная семантика и теория областей Скотта активно используются как математический базис для описания семантики последовательных программ, установления взаимосвязей между языками программирования, исследования типов данных языков программирования. Примененимость таких абстрактных методов к моделям параллельных систем и процессов всегда вызывало некоторый скептицизм. Однако в работах Винскеля было показано, что модели областей Скотта адекватно и полностью представляют семантику известных моделей параллелизма.

Большое мнообразие моделей, предложенных в теории параллелизма, требует их систематизации и унификации. Последнее десятилетие методы теории категорий стали активно использоваться для описания, изучения и сравнительного анализа параллельных моделей. Основная идея подхода заключается в следующем. Объекты категорий представляют процессы, морфизмы соответствуют взаимосвязям между поведениями процессов. Тот факт, что одна модель более выразительна, чем другая, формально выражается в терминах вложений (или прообразов). На основе данного подхода были исследованы взаимосвязи между различными параллельными моделями: сетями Петри, сетями-процессами, структурами событий и областями Скотта; системами переходов с независимостью (высших порядков) и структурами событий (высших порядков), системами переходов с независимостью и асинхронными системами переходов; (асинхронными) системами переходов и сетями Петри; автоматами высших порядков и асинхронными системами переходов и т.д.

В последнее десятилетие резко возрос интерес к разработке и исследованию параллельных систем, поведение которых в значительной

степени зависит от количественных временных характеристик, — параллельных систем реального времени. Поэтому в литературе были сделаны попытки ввести понятие времени в различные формальные модели. В результате появились такие модели, как временные автоматы, временные системы переходов, временные сети-процессы, временные структуры событий, временные частично-упорядоченные множества и т.д. За последние пять лет были хорошо изучены взаимосвязи между временными сетями Петри и временными автоматами. Однако известно не так много результатов по сравнительному анализу других временных параллельных моделей. Причем работы с использованием теоретико-категорных методов, на сколько нам известно, совсем отсутсвуют. Кроме того, следует отметить, что семантика «истинного параллелизма» моделей с реальным временем также недостаточна изучена в литературе.

В рамках диссертационной работы предпринимается попытка заполнить указанные пробелы.

Все вышесказанное говорит об актуальности исследований, проводимых в рамках диссертационной работы.

Цель диссертации состоит в развитии и обобщении теоретико-ка-тегорных методов спецификации и верификации параллельных систем реального времени. Достижение цели связывается с решением следующих задач:

1. разработка и развитие формальных моделей параллельных систем реального времени;

2. построение и исследование абстрактной семантики временных параллельных моделей в терминах областей Скотта;

3. развитие и применение теоретико-категорных методов сравнительного анализа, классификации и унификации параллельных моделей с реальным временем.

Методы исследований. В рамках данной работы использовались методы и понятия теории категорий, теории множеств, теории графов, теории автоматов и теории частичных порядков. В качестве формальных моделей параллелизма применялись первичные, расслоенные и стабильные структуры событий, сети Петри и системы переходов с неза-

висимостью и их временные расширения.

Научная новизна. В результате выполненных исследований автором разработаны оригинальные методы решения задач построения семантики «истинного параллелизма» и установления взаимосвязей моделей параллельных систем реального времени. Следующие результаты, полученные в диссертации, полностью раскрывают научную новизну:

• Разработаны временные расширения моделей с семантикой «истинного параллелизма» — временные первичные/расслоенные/стабильные структуры событий, а также временные системы переходов с независимостью.

• Построена семантика помеченных областей Скотта для временных структур событий, временных систем переходов с независимостью и временных сетей Петри.

• Определены и изучены категории введенных временных моделей, между которыми установлены строгие взаимосвязи в терминах существования коррефлексий.

Практическая ценность. Полученные результаты носят в основном теоретически характер. Тем не менее, они могут быть применены при разработке модулей автоматического построения семантических представлений, эквивалентных преобразований и верификации параллельных процессов, а также оптимизации параллельных программных систем.

Личный вклад автора. Все результаты, представленные в диссертации, получены автором лично. Постановки задач выполнены научным руководителем И.Б. Вирбицкайте.

Апробация работы. Основные идеи и конкретные результаты диссертационной работы обсуждались на следующих международных и отечественных научных конференциях и семинарах:

• XLI Международная научная студентческая конференция «Студент и научно-технический прогресс» (Россия, Новосибирск, 2003);

• Международная научно-практическая конференция по прорам-мированию УкрПРОГ'2004 (Украина, Киев, 2004);

• International Conference on Parallel Computing Technologies

PaCT'2005 (Krasnoyarsk, Russia, 2005);

• Internationa] Andrei Ershov Memorial Conference on Perspectives of System Informatics on (Novosibirsk, Russia, 2006);

• 15th International Workshop «Concurrency, Specification and Programming» (Vandlidz, Germany, 2006);

• IX всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (Россия, Кемерово, 2008);

• 17th International Workshop «Concurrency, Specification and Programming» (Gross Vaeter See, Germany, 2008).

Кроме того, доклады по теме работы были сделаны на ряде семинаров Института систем информатики СО РАН (г. Новосибирск) и кафедр Новосибирского государственного университета.

Публикации. По теме диссертации опубликовано 9 научных работ, в том числе 1 — в изданиях, рекоммендуемых ВАК, 1 — в научном журнале, 6 — в трудах международных и отечественных конференций и семинаров.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и списка литературы.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ В первой главе рассматриваются определения базовых понятий, связанных с теорией категорий, областями Скотта и моделями теории параллельных систем и процессов: структурами событий, системами переходов с независимостью, сетями Петри и сетями-процессами.

Вторая глава посвящена теоретико-категорному исследованию различных классов временных структур событий и построению для них семантических областей Скотта.

В разделе 2.1 вводится модель помеченных областей. Помеченная область (D, С, т) состоит из первично-алгебраической, финитарной, когерентной области Скотта (£), С) и пометки т : / —» {0,1}, где I — {[<i, d'] | d -< d'} — множество первичных интервалов ы d -< d' (d С d') Л (d ф d') A (Vd" . (d С d" С d') => (d" = d V d" = d')) -отношение покрытия. Пометка позволяет моделировать два типа действий системы: мгновенные, которые не потребляют времени, и поме-

чаются нулем, и задержанные, которые потребляют единицу времени и помечаются единицей. При этом естественно потребовать, чтобы эквивалентные первичные интервалы, соответствующие одному и тому же действию системы, были помечены одинаково. Пометка позволяет задать новые отношения между элементами области: помеченное покрытие d d! d -< d! Л m([d, d']) = i, d =i* d! <i=> d Vd = d! и помеченное отношение порядка С*= (-<*)*. Далее, вводится понятие нормы элемента. Для компактного элемента d € D его норма вдоль покрывающей цепи а = ± -<kl di -<k2 ■ ■ ■ -<kn dn = d определяется как ||d||CT = Yl^i Так как (D, С) — первично-алгебраическая область Скотта, то это определение не зависит от выбора о, т.е. можно говорить о норме ||d||. Для произвольного элемента d € D норма определяется следующим образом ||d|] = sup{||d'|] | d' С. dhd! — компактный}. Неформально говоря, норма показывает, какое количество задержанных действий должна совершить система чтобы попасть в состояние, задаваемое данным элементом. Определяются свойства помеченных областей. Помеченная область (D,Q,m) называется

• регулярной, если для любых d, d' 6 D таких, что d | d' (т.е. существует d" 6 D такой, что d Q d" и d' Q d") справедливо, что для всех di,d[ 6 D, таких, что d С1 di и d' С1 d[, верно di f d[;

• линейной, если для каждого элемента d 6 D такого, что ||d|| < оо, частично-упорядоченное множество ({d' 6 D | d С* d'},C) изоморфно (N, <), где N — множество натуральных чисел.

Рассмотрим помеченные области (£>, С,т) и (D', С', тп'). Для г = 0,1, будем говорить, что отображение / : D D' сохраняет -<г (=$*), если для всех d,d' е D из d d! следует /(d) f{d') (f{d) ^ f(d')). Было показано, что регулярные линейные помеченные области вместе с морфизмами — аддитивными, стабильными отображениями, сохраняющими =<;° и X1 — образуют категорию MDom.

В разделе 2.2 вводятся модели временных первичных, расслоенных и стабильных структур событий. Предполагается, что время задается неотрицательными целыми числами и делится на счетное количество тактов. При этом имеются глобальные часы, которые запускаются вместе с началом функционирования структуры и значение которых уве-

личивается на единицу при каждом тиканье часов. Начальное значение часов обычно предполагается равным 0. Временная первичная/расслоенная/стабильная структура — это четверка (Е, □, #, А), где (Е, #)

— первичная/расслоенная/стабильная структура событий1 и Д : Е —> N

— функция временных задержек. Если Д(е) = t, то событие е может произойти не раньше, чем все его предшественники произойдут и часы покажут значение t. При этом само событие происходит мгновенно. Состояния временных структур описываются в терминах временных конфигураций. Временная конфигурация — это пара (С, t), где С — конфигурация (бесконфликтное, левозамкнутое относительно □ множество событий) и £ € N (N = N U {оо}) — текущее значение глобальных часов такое, что Д(е) < t для каждого е € С. Пусть ТСоп/(ТЕ) — множество временных конфигураций временной структуры ТЕ. Определим (С, £) —> (С, £'), если С С С' и t < t' - отношение перехода на временных конфигурациях. Очевидно, что отношение —> задает частичный порядок на множестве TConf(TE). Кроме того, верна следующая

Теорема 2.1. Пусть ТЕ = (Е = (Е, □,#), Д) — временная структура и TConf(TE) — множество ее временных конфигураций. Тогда (TConf(TE),—>) — первично-алгебраическая, финитарная, когерентная область Скотта.

Определим —> \ —>2 — отношение непосредственного перехода между временными конфигурациями. Понятно, что отношение может быть разбито на два непересекающихся отношения: (С, I) (С, t') <=> С' \ С = {е} A t = t' (непосредственный переход по событию) и (C,t) 1 (С', t') С" = С A t < оо A t + 1 = f

(непосредственный переход по времени).

Пусть ТЕ = (Е, □, #, Д) и ТЕ' = (£', □', #', Д') - временные структуры и 0 : Е -*т Е' — частичное отображение. Тогда 0 : ТЕ —» ТЕ' — морфизм, если в : (Е, О, #) —» (Е', □', #') — морфизм структур событий и для каждого события е 6 dom<? верно А'(т](е)) < Д(е). Было показано,

'Тройка (£,□,#) — первичная/расслоенная/стабильная структура, если Е — счетное множество событий, □ — отношение причинной зависимости/расслоения/разрешения и # — иррефлексивное, семетричное отношение конфликта.

что временные первичные, расслоеные и стабильные структуры событий с морфизмами, определенными выше, образуют категории ТРЕБ, ТВЕБ и ТБЕБ соответственно.

В разделе 2.3 сначала устанавливается, что множества временных конфигураций временных структур событий образуют линейные, регулярные помеченные области, пометка в которых определяется при помощи отношений и . Используя этот факт, строятся функторы ¿ре^.тйот : ТРЕБ -> МБот, ЬЬеБ.тЛот : ТВЕБ —> МБога и ¿вез.т^тп : ТБЕБ -+ МБот.

Затем, определяется отображение rn.dom.tpes, переводящее помеченные области во временные первичные структуры, в которых события соответствуют классам эквивалентных первичных интервалов области, помеченных 0, и временные задержки событий определяются при помощи нормы. Доказывается следующий факт.

Теорема 2.2 (МБот = ТРЕБ). Отображение тЛотАрев расширяется до функтора, сопряженного слева к функтору Ьрев.тйога, причем это сопряжение задает сопряженную эквивалентность категорий МБош и ТРЕБ.

Далее, исследуются теоретико-категорные взаимосвязи между помеченными областями и временными расслоенными и стабильными структурами событий. Для этого сначала определяются функторы ЬревЛЬез : ТРЕБ -» ТВЕБ и ¿рез.^ел : ТРЕБ -> ТБЕБ, которые переводят временные первичные структуры во временные расслоенные и стабильные структуры соответственно. Это позволяет построить функторы тйотЛЬев — tpes.tbesomdom.tpes : МБот —> ТВЕБ и 7nd.om.tses = ¿реб'.^ево тйотЛрез : МБога —► ТБЕБ, а также показать, что верна следующая

Теорема 2.3.

1. {тйотЛЬев Ч Их'.в .тс1от) Функтор тйотЛЬеэ сопряжен слева к функтору tЬes.mdom, причем это сопряжение является коре-флек спей.

2. (тйотЛбев Н tses.mdom) Функтор mdom.tses сопряжен слева к функтору tses.mdom, причем это сопряжение является коре-флексией.

В заключение, устанавливаются теоретико-категорные взаимосвязи между различными классами временных структур событий. Определяются функторы 1ЪезЛрез = тпйот.Ьрев о tbes.md.om : ТВЕБ —» ТРЕБ и ЬзсвЛрез = 7n.dom.tpes о ¿зез.тс1от : ТБЕв —* ТРЕБ, для которых верно следующее Следствие 2.1.

1. ^ревЛЬез Ч СЬсзЛрсв) Функтор ЬрезЛЬев является левым сопряженным к функтору ЬЬезЛрев, причем это сопряжение является корефлексией.

2. {ЬрезЛзсз Ч 1.зсвЛрсв) Функтор ЬревЛзез является левым сопряженным к функтору ЬзевЛрез, причем это сопряжение является корефлексией.

Результаты, полученные во второй главе, представлены на следующей диаграмме.

ЬЬезЛрез ЬзевЛрез

В третьей главе в рамках теорети-категорного подхода исследуются временные расширения систем переходов с независимостью и строится семантика помеченных областей данной модели.

В разделе 3.1 сначала определяется понятие временной системы переходов с независимостью (ВСПН) как пятерки ТТ1 = {3, в1, Ь, ТТгап, Т1), где 5 — множество состояний, в1 — начальное состояние, Ь — множество меток, ТТгап С 5 х Ь х х 5 — множество переходов такое, что для любых переходов (в, а, 6, а'), (в, а, ¿', У) 6 ТТгапэ верно 6 = 6' (здесь

N+ — множество непустых конечных или бесконечных последовательностей натуральных чисел) и TI С TTran х ТТгап — иррефлексивное, симметричное отношение независимости на переходах, для которых верно:

1. [XT/J = (S,so,L,Tran,I) — система переходов с независимостью, где, если обозначить [(s, о, 5, s')J = (s, а, s') для каждого перехода (s,a,6,s') £ ТТгап, то Tran = {[[¿f | t 6 ТТгап], и И / li'l t TI t';

2. (s, а, 5, s') ~ (s, a, <5, s') <5 =

Таким образом, с каждым переходом t связывается последовательность 5t = (<5i(0),..., 15t (п),...) целочисленных задержек относительно глобального дискретного времени. Поведение ВСПН описывается в терминал временных вычислений. Временное вычисление — это (возможно, пустая) последовательность П = (<i, di)... (tn,dm), где пара (¿¿,di) обозначает выполнение перехода U в момент времени di такая, что переход ii осуществляется из начального состояния s1 и соблюдены временные задержки переходов. Пусть TComp(TTJ) — множество всех временных вычислений ВСПН TTI. Определяется подкласс временных систем переходов с независимостью — событийные ВСПН (сВСПН) — ацикличные ВСПН, в которых с каждым переходом связана последовательность задержек, состоящая из единственного элемента.

Пусть TTI = (S, sl, L, ТТгап, TI) и TTI' = {S', s1', V, ТТгап', TI') — ВСПН. Тогда пара h = {а, Л), где а : S —♦ 5" и Л : L —>* L', является морфизмом h : TTI —* TTI', если для любого временного вычисления П € TPath(TT7) верно /¿(II) 6 ТСошр(TTI'), где /i(II) естественным образом определяется по индукции, и для любых временных вычислений П,П' е ТСотр(ТТ7) таких, что П = П' (т.е. данные временные вычисления отличаются только порядком выполнения независимых переходов) верно Л(П) == /г(П'). Было показано, что ВСПН и сВСПН с мор-физмами, определенными выше, образуют категории TTSI и oTTSI соотвественно.

Раздел 3.2 посвящен построению развертки ВСПН в сВСПН. Для этого определяется отображение ttsi.ottsi : TTSI —* oTTSI, соспоста-вющее ВСПН TTI ее развертку OTTI. Состояниями OTTI являются

классы =-эквивалентных временных вычислений [П] в TTI. Из состояния [П] существует переход t' в состояние [П'], если в TTI существует переход t такой, что П' = n(i,d) для некоторого d е N. Было дана теоретико-категорная характеризация построенному отображению.

Теорема 3.1 (^-Н ttsi.ottsi). Отображение ttsi.ottsi может быть расширено до функтора, который сопряжен к функтору включения oTTSI —> TTSI справа. Более того, это сопряжение является коре-флексией.

В разделе 3.3 строится семантика помеченных областей ВСПН. Для этого сначала устанавливаются теоретико-категорные взаимосвязи между сВСПН и временными первичными структурами. Определяется отображение ottsi.tpes : oTTSI -+ TPES, переводящее сВСПН OTTI во временную первичную структуру TP, события которой представлены классами эквивалентных переходов OTTI. Далее, вводится функтор tpes.ottsi : TPES —> oTTSI, строящий по временной первичной структуре TP сВСПН OTTI, состояниями которой являются определенного вида временные конфигурации TP и переходы которой соответствуют осуществлению событий ТР. Доказывается следующий факт. Теорема 3.2 (tpes.ottsi Ч ottsi.tpes). Отображение tpes.ottsi может быть расширено до функтора tpes.ottsi : TPES —> oTTSI который является сопряженным к функтору ottsi.tpes слева. Более того, данное сопряжение является корефлексией.

Чтобы завершить построение семантики помеченных областей ВСПН, доказывается

Теорема 3.3. Пара функторов <—» о tpes.ottsi omdom.tpes и tpes.mdomo ottsi.tpes о ttsi.ottsi задает сопряжение между категориями TTSI и MDom. Более того, данное сопряжение является корефлексией.

Установленные взаимосвязи приведены на диаграмме

ttsi.ottsi ottsi.tpes tpes.mdom

TTSI ( т J ч oTTSI < T 1 TPES ( иг ' MDom

tpes.ottsi mdom.tpes

В четвертой главе изучаются временные расширения сетевых моделей и определяется их семантика в терминах помеченных областей.

В разделе 4-1 сначала вводится определение понятия временных сетей-процессов как четверки (В, Е, G, Д), где (В, Е, G) — сеть-процесс и А : Е —* Interv — функция временных интервалов, где Interv = {[а, 6] | a6NAieN = NU {оо}}. При этом Д должна быть согласована с порядком причинной зависимости на событиях.

Будем называть Д±(е) минимальной задержкой, а Дт(е) — максимальной задержкой события е. Поведение временных сетей-процессов описывается в терминал временных вычислений. Временное вычисление — это пара (и, Т), состоящая из вычисления 7г безвременной сети-процесса (т.е. бесконфликтной подсети, имеющей те же входные условия) и функции Т : Еп —* N, сопоставлюящей каждому событию вычисления момент времени, в который оно произошло. Существует два подхода к определению семантики временных сетей-процессов — «энергичный» и «ленивый». В «энергичной» семантике осуществление события форсируется, если все его предшественники произошли и счетчик глобального времени достиг значения, равного максимальной задержке этого события. Напротив, в «ленивой» семантике событие может и не произойти, даже если условия его осуществления выполнены. Множество временных вычислений временной сети-процесса TNP в «энергичной» и «ленивого» семантиках обозначим TComp(TNP)e и ТСошр(TNP)i соответственно.

Пусть TNP = {B,E,G, Д) и TNP' = (B',E',G',A') - временные сети-процессы. Тогда пара (/?, 77), где ß С В х В' — отношение и г] : Е —>* Е' — частичное отображение, является морфизмом (ß,rj) : TNP —► TNP', если для каждого временного вычисления (7Г,Т) 6 TComp,.(TNP) верно (и(тг),Т')х е TCompx(7W), где образ вычисления я- определяется естественным образом, Т" о 77 = Г, и для всех событий е, е' е Еп верно rj(e) = г](е') => е = е'. Здесь х = I, если определение дается в рамках «ленивой» семантики, и х = е, если — в рамках «энергичной».

Было показано, что временные сети-процессы с «энергичной» и «ленивой» семантиками вместе с определенными выше морфизмами образуют категории ТРгосе и TProci соответственно. В каждой из них были выделены полные подкатегории TProc£° (х = е,1) с объектами в

виде временных сетей-процессов, в которых всем событиям присвоены максимальные задержки, равные оо. Было показано, что построенные категории совпадают, т.е. ТРгос£° = ТРгос^0, а также для них было введено новое обозначение ТРгос.

Раздал 4-2 посвящен изучению построенных выше категорий. Доказываются теоремы 4.1 и 4.2, в которых формулируются необходимые и достаточные условия, при которых морфизм категорий ТРгосе и ТРгос) является эпи- или мономорфизмом соответственно. Полученные результаты переносятся в категорию ТРгос.

В разделе 4-3 строится семантика помеченных областей временных сетей-процессов. Сначала установливаются взаимосвязи между категорией ТРгос и категорией ТРЕБ временных первичных структур событий в терминах существования корефлексии. Для этого определяется функтор ЬргосЛрев : ТРгос —> ТРЕЭ, переводящий временную сеть-процесс ТИР во временную первичную структуру событий ТР, наследующую события, их задержки, конфликт и порядок причинной зависимости от ТИР. Далее, определяется отображение ЬревЛргос : ТРЕЭ —> ТРгос, действующее в обратную сторону и сопоставляющее каждой временной первичной структуре событий ТР временную сеть-процесс ТИР, наследующий события и временные задержки ТР. Доказывается Теорема 4.3 (£ревАргос Ч ¿ргоаЛрев). Отображение ¡резЛргос может быть расширено до функтора ЬреэЛргос : ТРЕБ —> ТРгос, который сопряжен к функтору ЬргосЛрез : ТРгос —♦ ТРЕБ слева. Более того, это сопряжение является корефлексией.

Чтобы завершить построение семантики помеченных областей временных сетей-процессов, показывается справедливость

Теорема 4.4 (tpes.tprocomdom.tpes Н 1рсз .тйот о ЬргосЛреэ). Пара функторов <-♦ о tpes.ottsi отйотЛрез и tpes.mdom о оИзгЛрсь о Шг.оШг задает сопряжение между категориями ТТБ1 и МБот. Более того, данное сопряжение является корефлексией.

Установленные взаимосвязи приведены на диаграмме

ЬргосЛрез

Ьрев.тАотп

ТРгос ( Т

Ьрез Лргос

В разделе 4-4 определяются структура и поведение временных сетей Петри. Временная сеть Петри — это пятерка ТРИ = (Р,Т,Р,Мо,6), где (Р,Т, Р, Мо) — сеть Петри и <5 : Т —> N — функция статических задержек. Поведение временных сетей Петри описывается в терминах состояний (М,т), которые представляют собой текущую разметку М и динамическую временную функцию г, связанную с переходами сети, возможными в данной разметке.

Пусть ТРЛГ = (Р,Т,Р,Мо,5) и ТРЛГ = (Р', Т', Р', Мд, - временные сети Петри. Тогда пара (/?, г/), где (3 С Р х Р' — отношение и ту : Т —>* Т" — частичное отображение, является морфизмом (/?, г;) : ТРАТ -> ТРЛ^', если {(5, г)) : (Р,Т,Р,М0) -> (Р', Т', Р', Л^) - морфизм сетей Петри и для любого перехода 4 е с!от верно ¿'(г/Щ) < Было показано, что временные сети Петри вместе с морфизмами, определенными выше, образуют категорию ТРе1п.

Раздел 4-5 посвящен построению семантики помеченных областей временных сетей Петри. Для этого вводится понятие развертки временных сетей Петри во временные сети-процессы. Для этого определяется функтор Ьр&ггЛргос, которое переводит временную сеть Петри ТРМ во временную сеть-процесс являющуюся копределом по-

следовательности ТЫР^ разверток ТИР на конечную глубину г 6 N. Установленные взаимосвязи приведены на диаграмме

ipeirt.ii) гос 1ргосЛрез Ьрсз .тв-оггг

ТРекп —-—*■ ТРгос -ТРЕЭ -МБот

ОСНОВНЫЕ ВЫВОДЫ И РЕЗУЛЬТАТЫ В рамках диссертационной работы были получены следующие результаты.

1. Введены временные расширения моделей параллельных процессов — первичных, расслоенных и стабильных структур событий. Для данных моделей построены и изучены категории, между которыми установлены взаимосвязи в терминах существования корефлексий.

2. Определены временные расширения моделей систем переходов с независимостью и событийных систем переходов с независимостью.

Построены и изучены категории этих моделей. Дана теоретико-категорная характеризация развертки временных систем переходов с независимостью в событийные временные системы переходов с независимостью. Установлена взаимосвязь между категорией временных первичных структур событий и категорией событийных систем переходов с независимостью в терминах существования корефлексии.

3. Построены и изучены категории временных расширений сетей Петри и сетей-процессов. Дана теоретико-категорная характеризация развертки временных сетей Петри во временные сети-процессы. Установлена взаимосвязь между категорией временных первичных структур событий и категорией временных сетей-процессов в терминах существования корефлексии.

4. Введена модель помеченных областей Скотта. На основе теоретико-категорных методов построена семантика помеченных областей для временных расширений моделей структур событий, систем переходов с независимостью и сетей Петри.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ P.C. ДУБЦОВА

1. Дубцов P.C. Исследование свойств категорий параллельных моделей с реальным временем // Материалы XLI международной научной студентческой конференции «Студент и научно-технический прогресс». - Новосибирск: 2003. - С. 109.

2. Дубцов P.C. Критерии эпи- и мономорфизма в категориях моделей с реальным временем // Новосибирск, 2004. - (Препр./РАН. Сиб. отд-ние. ИСИ; .ЧН13) - 23 с.

3. Дубцов Р. С. Теоретико-категорная характеризация развертки временных сетей Петри // Проблемы программирования - 2004. - № 2-3 - С. 30-36.

4. Dubtsov R. Real-Time Event Structures and Scott Domains // Para-Ile] Computing Technologies: Proc. / Ed. by V. Malyshkin. - Berlin a.o.: Springer-Verlag, 2005. - P. 42-48 - (Lect. Notes Сотр. Sci.; 3606).

5. Dubtsov R. Semaiitic Domains for Real-Time Event Structures // Proc. 15th Intl. Workshop «Concurrency, Spécification and Programming». - Wandlitz (Germany): 2006. - P. 186-194.

6. Dubtsov R. Real-Time Stable Event Structures and Marked Scott Domains: an Adjunction // Perspectives of System Informatics: Proc. / Ed. by A. Voronkov, et al. - Berlin a.o: Springer-Verlag, 2007. - P. 443-450. - (Lect. Notes Comp. Sei.; 4378).

7. Вирбицкайте И.В., Дубцов P.C. Семантические области временных структур событий // Программирование. - 2008. - Л"«3. - С. 1-19.

8. Дубцов P.C. Теоретико-категорные исследования систем переходов с независимостью // Материалы IX Всероссийской конференции молодых ученых по математическому моделированию и информационных технологий. - Кемерово: 2008. - С. 78.

9. Dubtsov R.S, Virbitskaite I.B. A Comparative Account of Timed Event Structures // Proc. 17th Intl. Workshop «Concurrency, Specification and Programming». - Gross Vaeter See (Germany): 2008. - P. 500-511.

Подписано в печать 20.11.2008.

Формат бумаги 60x84 1/16 Усл. печ. л. 1

Тираж 100 экз.

Центр оперативной печати "Оригинал 2" г.Бердск, ул. Островского, 55, оф. 02, тел. (383) 214 45 35

Введение.

1 Известные результаты

1.1 Элементы теории категорий.

1.2 Области Скотта.

1.3 Структуры событий

1.4 Системы переходов с независимостью

1.5 Сети-процессы и сети Петри.

2 Семантика помеченных областей временных структур событий

2.1 Категория помеченных областей Скотта.

2.2 Категории временных структур событий

2.3 Взаимосвязи категорий временных структур событий и помеченных областей

2.4 Выводы.

3 Семантика помеченных областей временных систем переходов с независимостью.

3.1 Категории временных систем переходов с независимостью

3.2 Развертка временных систем переходов с независимостью

3.3 Взаимосвязи категорий временных систем переходов с независимостью и помеченных областей

3.4 Выводы.

4 Семантика помеченных областей временных сетевых моделей

4.1 Категории временных сетей-процессов.

4.2 Свойства категорий временных сетей-процессов

4.3 Взаимосвязи категорий временных сетей-процессов и помеченных областей

4.4 Категория временных сетей Петри

4.5 Взаимосвязи категорий временных сетей Петри и помеченных областей

4.6 Выводы.

Актуальность. В настоящее время сфера применения аппаратных и программных систем с параллельной/распределенной архитектурой непрерывно расширяется, охватывая все новые области в самых различных отраслях науки, техники, образования, бизнеса и производства. К таким системам относятся коммуникационные протоколы, системы управления производством, распределенные операционные системы, параллельные базы данных и т.д. Параллельные/распределенные системы, как правило, состоят из большого числа компонентов со сложным характером взаимодействий, что затрудняет понимание природы протекающих в них разнообразных процессов. Проектирование и реализация корректных параллельных/распределенных систем возможны только при использовании формальных методов н средств, которые должны быть, с одной стороны, «дружественными» для разработчиков, а с другой - математически строгими, а также адекватно представлять структуру и поведение 'моделируемых систем.

Среди отечественных исследований по спецификации, моделированию и анализу сложных (в том числе, параллельных/распределенных) систем отметим работы Н.А. Аннсимова, O.JI. Бандман, И.Б. Вирбиц-кайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.Э. Малышкина, В.А. Непомнящего, А.К. Петренко, P.JI. Смелянского, В.А. Соколова, JI.A. Черкасовой.

Теория параллельных систем и процессов — активно развивающаяся область компьютерных наук - изучает фундаментальные понятия и законы параллельной обработки информации и на основе обнаруженных закономерностей строит более частные формальные модели исследуемых объектов, на которых ставит и решает прикладные задачи. На основе результатов и рекомендаций теоретических исследований ведется поиск и проверка новых архитектурных принципов конструирования систем, изучаются методы распараллеливания алгоритмов и программ, разрабатываются новые конструкции параллельных языков программирования, проверяются способы анализа и верификации программных систем и т.д. За последние четыре десятилетия в теории параллелизма появилось большое разнообразие моделей и методов, предназначенных для спецификации, разработки и верификации систем. Среди формальных структурных моделей следует отметить сети Петри, системы переходов, системы переходов с независимостью, автоматы высших порядков, I/O-автоматы и т.д. Особое внимание в теории параллелизма отводится абстрактным семантическим моделям, позволяющим описывать и исследовать поведения параллельных систем. К таким моделям относятся деревья синхронизации, причинные деревья, структуры событий и т.д. Известно, что денотационная семантика и теория областей Скотта активно используются как математический базис для описания семантики последовательных программ, установления взаимосвязей между языками программирования, исследования типов данных языков программирования. Примененимость таких абстрактных методов к моделям параллельных систем и процессов всегда вызывало некоторый скептицизм. Однако в работах Винскеля было показано, что модели областей Скотта адекватно и полностью представляют семантику известных моделей параллелизма.

Большое мнообразие моделей, предложенных в теории параллелизма, требует их систематизации и унификации. Последнее десятилетие методы теории категорий стали активно использоваться для описания, изучения и сравнительного анализа параллельных моделей. Основная идея подхода заключается в следующем. Объекты категорий представляют процессы, морфизмы соответствуют взаимосвязям между поведениями процессов. Тот факт, что одна модель более выразительна, чем другая, формально выражается в терминах вложений (или прообразов). На основе данного подхода были исследованы взаимосвязи между различными параллельными моделями: сетями Петри, сетями-процессами, структурами событий и областями Скотта; системами переходов с независимостью (высших порядков) и структурами событий (высших порядков) , системами переходов с независимостью и асинхронными системами переходов; (асинхронными) системами переходов и сетями Петри; автоматами высших порядков и асинхронными системами переходов и т.д.

В последнее десятилетие резко возрос интерес к разработке и исследованию параллельных систем, поведение которых в значительной степени зависит от количественных временных характеристик, — параллельных систем реального времени. Для таких систем важны как модели вычислений, так и модели времени. В литературе параллельные системы реального времени часто представляются временными автоматами [13], временными системами переходов [46] и алгебрами временных процессов (см., например, [81]). Однако все эти формализмы базируются на интерливннговой семантике и не позволяют моделировать параллелизм естественным образом (напрямую). К временным моделям с семантикой «истинного параллелизма» относятся временные расширения моделей структур событий [15, 34, 42, 52, 63], сетей-процессов [17, 82], сетей Петри [8, 58, 74], причинных деревьев [37], частично-упорядоченных множеств [55, 80], систем конфигураций [56], асинхронных систем переходов [10]. Перечисленные выше временные модели могут быть классифицированы относительно семи дихотомий: дискретное/непрерывное время. В дискретных моделях (см., например, [74, 82]) время задается целыми числами. Такой подход обычно используется для описания систем с общим глобальным счетчиком времени. Время делится на счетное количество тактов: п + 1-й такт начинается в га-ый момент времени и заканчивается в п + 1-ый. Дальнейшее разбиение времени внутри тактов не предусматривается. В непрерывных моделях [37, 52, 56, 58, 63] время измеряется по непрерывной временной шкале и возможно неограниченное число событий при переходе системы из одного состояния в другое; абсолютное/относительное время. В процессе функционирования системы временные характеристики связываются либо с началом ее функционирования (абсолютное время) [42, 52], либо отсчитывают-ся от конца предыдущего действия системы (относительное время) [58]; явное/неявное понятие прохождения времени. Известно, что временная система функционирует двумя способами: посредством выполнения действия и посредством прохождения некоторого времени. Эти два понятия становятся ортогональными при явном введении понятия прохождения времени. Такой подход рассмотрен в [56], а альтернативный — в [10, 52, 58, 63]; задержанные/мгновенные действия. В моделях, описанных в [10, 55, 63, 74], задержка действия смоделирована как временной промежуток между началом выполнения действия и его окончанием. При втором подходе выполнение действия само не требует времени, но, как правило, может быть отложено на определенный срок [37, 52, 56, 58]; с/без локальных часов. Использование локальных часов [10, 17, 58] позволяет описывать эволюцию различных частей распределенных систем. Иначе говоря, каждое событие имеет свой таймер задержки, который начинает отсчитывать время с того момента, когда событие становится активным, и останавливается, когда событие становится пассивным. Такой подход позволяет достаточно легко изучать поведение системы локально. С другой стороны, как было продемонстрировано в [52], операционная семантика алгебр временных процессов может быть описана проще, если не использовать локальные часы; несогласованные/согласованные по времени трассы. В несогласованных по времени трассах предшествование событий не отражает их временного порядка, поэтому во многих работах такой подход не используется (см., например, [58, 82]). Однако, как сообщалось в статьях [10, 52], несогласованные по времени трассы позволяют построить семантику 'истинного параллелизма' для временных ин-терливинговых алгебр процессов, т.е. установить связи между 'истинным параллелизмом' и интерливингом; срочные У'несрочные' действия. Понятие 'срочного' действия подразумевает, что действие должно быть выполнено сразу, как только оно готово, т.е. все его предшественники выполнились и его временные ограничения также выполнены (см. [10, 56, 58]). Однако иногда требование 'срочного' выполнения временных действия является слишком жестким. Один из способов решения этой проблемы — добавление 'несрочных' действий. Например, в работе [52] были использованы оба вида действий.

За последние пять лет были хорошо изучены взаимосвязи между временными сетями Петри и временными автоматами [77]. Однако известно не так много результатов по сравнительному анализу других временных параллельных моделей. Причем работы с использованием теоретико-ка-тегорных методов, на сколько нам известно, совсем отсутсвуют. Кроме того, следует отметить, что семантика «истинного параллелизма» моделей с реальным временем также недостаточна изучена в литературе.

В рамках диссертационной работы предпринимается попытка заполнить указанные пробелы.

Все вышесказанное говорит об актуальности исследований, проводимых в рамках диссертационной работы.

Цель диссертации состоит в развитии и обобщении теоретико-ка-тегорных методов спецификации и верификации параллельных систем реального времени. Достижение цели связывается с решением следующих задач:

1. разработка и развитие формальных моделей параллельных систем реального времени;

2. построение и исследование абстрактной семантики временных параллельных моделей в терминах областей Скотта;

3. развитие и применение георетико-категорных методов сравнительного анализа, классификации и унификации параллельных моделей с реальным временем.

Методы исследований. В рамках данной работы использовались методы и понятия теории категорий, теории множеств, теории графов, теории автоматов и теории частичных порядков. В качестве формальных моделей параллелизма применялись первичные, расслоенные и стабильные структуры событий, сети Петри и системы переходов с независимостью н их временные расширения.

Научная новизна. В результате выполненных исследований автором разработаны оригинальные методы решения задач построения семантики «истинного параллелизма» и установления взаимосвязей моделей параллельных систем реального времени. Следующие результаты, полученные в диссертации, полностью раскрывают научную новизну:

Разработаны временные расширения моделей с семантикой «истинного параллелизма» — временные первичные/расслоенные/стабильные структуры событий, а также временные системы переходов с независимостью.

Построена семантика помеченных областей Скотта для временных структур событий, временных систем переходов с независимостью и временных сетей Петри.

Определены и изучены категории введенных временных моделей, между которыми установлены строгие взаимосвязи в терминах существования коррефлексий.

Практическая ценность. Полученные результаты носят в основном теоретически характер. Тем не менее, они могут быть применены при разработке модулей автоматического построения семантических представлений, эквивалентных преобразований и верификации параллельных процессов, а также оптимизации параллельных программных систем.

Личный вклад автора. Все результаты, представленные в диссертации, получены автором лично. Постановки задач выполнены научным руководителем И.Б. Вирбицкайте.

Апробация работы. Основные идеи и конкретные результаты диссертационной работы обсуждались на следующих международных и отечественных научных конференциях и семинарах:

XLI Международная научная студентческая конференция «Студент и научно-технический прогресс» (Россия, Новосибирск, 2003);

Международная научно-практическая конференция по прорамми-рованию УкрПРОГ'2004 (Украина, Киев, 2004);

International Conference on Parallel Computing Technologies PaCT'2005 (Krasnoyarsk, Russia, 2005);

International Andrei Ershov Memorial Conference on Perspectives of System Informatics oil (Novosibirsk, Russia, 2006);

15th International Workshop «Concurrency, Specification and Programming» (Vandlidz, Germany, 2006);

IX всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (Россия, Кемерово, 2008);

17th International Workshop «Concurrency, Specification and Programming» (Gross Vaeter See, Germany, 2008).

Кроме того, доклады по теме работы были сделаны на ряде семинаров Института систем информатики СО РАН (г. Новосибирск) и кафедр Новосибирского государственного университета.

Публикации. По теме диссертации опубликовано 9 научных работ, в том числе 1 — в изданиях, рекоммендуемых ВАК, 1 — в научном журнале, 6 — в трудах международных и отечественных конференций и семинаров.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и списка литературы.

4.6 Выводы

В данной главе были изучены временные расширения сетевых моделей — временные сети-процессы и временные сети Петри. Для данных расширений были получены следующие результаты. Построены категории ТРгосе и TProci временных сетей-процессов с «энергичной» и «ленивой» семантиками соответственно. Выделена полная подкатегория ТРгос, для объектов которой данные семантики совпадают. е3 : 1

TPN" Рис. 4.5.

Сформулированы необходимые и достаточные условия, при которых морфизмы указанных категорий являются эпи- и мономорфизмами.

Установлено существование корефлексии между категорией ТРгос и категорией TPES временных первичных структур событий.

Построена развертка временных сетей Петри во временные сети-процессы и дана ее теоретико-категорная характеризация.

Определена семантика помеченных областей для временных сетевых моделей, используя эквивалентность категорий TPES и MDom.

Заключение

В рамках диссертационной работы были получены следующие результаты.

1. Введены временные расширения моделей параллельных процессов — первичпых, расслоенных и стабильных структур событий. Для данных моделей построены и изучены категории, между которыми установлены взаимосвязи в терминах существования корефлексий.

2. Определены временные расширения моделей систем переходов с независимостью и событийных систем переходов с независимостью. Построены и изучены категории этих моделей. Дана теоретико-категорная характеризация развертки временных систем переходов с независимостью в событийные временные системы переходов с независимостью. Установлена взаимосвязь между категорией временных первичных структур событий и категорией событийных систем переходов с независимостью в терминах существования корефлексии.

3. Построены и изучены категории временных расширений сетей Петри и сетей-процессов. Дана теоретико-категорная характеризация развертки временных сетей Петри во временные сети-процессы. Установлена взаимосвязь между категорией временных первичных структур событий и категорией временных сетей-процессов в терминах существования корефлексии.

4. Введена модель помеченных областей Скотта. На основе теоретико-категорных методов построена семантика помеченных областей для временных расширений моделей структур событий, систем переходов с независимостью и сетей Петри.

1. Вирбицкайте И. Б. Семантические модели в теории параллелизма. — Новосибирск: ИСИ СО РАН, 2000. 196 с.

2. Вирбицкайте И. Б., Дубцов Р. С. Семантические области временных структур событий // Программирование. — 2008. — Т. 3. — С. 119.

3. Дубцов Р. С. Критерии эпи- и мономорфизма в категориях моделей с реальным временем. — Новосибирск, 2004. — 23 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; №113).

4. Дубцов Р. С. Теоретико-категорная характеризация развертки временных сетей петри // Труды международной конференции Укр-Прог'04. — Т. 2-3 из Проблемы программирования. — Киев: 2004. — С. 30-36.

5. Дубцов Р. С. Теоретико-категорные исследования систем переходов с независимостью // Материалы IX Всероссийской конференции молодых ученых по математическому моделированию и информационных технологий. — Кемерово: 2008. — С. 78.

6. Дубцов, Р. С. Исследование свойств категорий параллельных процессов с реальными временем // Материалы XLI международной научной конференции «Студент и научно-технический прогресс».— Новосибирск: 2003. — С. 109.

7. Котов В. Е. Сети Петри. — М.: Наука, 1984. — 160 с.

8. A General Way То Put Time in Petri Nets / C. Ghezzi, D. Mandrioli, S. Morasca, M. Pezze // 5th Int. Workshop on Software Specification and Design. — 1989. — May. — Pp. 60-67.

9. Aceto L., De Nicola R., Fantechi A. Testing equivalences for event structures // Lecture Notes in Computer Science. — 1987. — Vol. 280. — Pp. 1-20.

10. Aceto L., Murphy D. Timing and Causality in Process Algebra // Acta Informatica. — 1996. — Vol. 33, no. 4. Pp. 317-350.

11. Alur R., Courcoubetis C., Dill D. Modcl-checking in dense real-time // Information and Computation. — 1993. — Vol. 104, no. 1. — Pp. 2-34.

12. Alur R., Courcoubetis C., Henzmger T. The observational power of clocks // Lccture Notes in Computer Science. — 1994. — Vol. 836. — Pp. 162-177.

13. Alur R., Dill D. A Theory of Timed Automata // Theoretical Computer Science. 1994. - Vol. 126, no. 2. - Pp. 183-235.

14. Andreeva M. V., Bozhenkova E. N., Virbitskaite I. B. Analysis of timed concurrent models based on testing equivalence // Fundament a Informaticae. — 2000. — Vol. 43, no. 1-4. — Pp. 1-20.

15. Andreeva M. V., Virbitskaite I. B. Timed Equivalences for Timed Event Structures // Lecture Notes in Computer Science. — 2005. — Vol. 3606. — Pp. 16-25.

16. Andreeva M. V., Virbitskaite I. B. Observational Equivalences for Timed Stable Event Structures j j Fundamenta Informaticae. — 2006. — Vol. 72, no. 1. —Pp. 1-19.

17. Aura Т., Lilius J. Time processes for time petri-nets. // Lecture Notes in Computer Science. — 1997. — Vol. 1248. — Pp. 136-155.

18. Bednarczyk M. Categories of asynchronous systems: Ph.D. thesis / University of Sussex, UIC. — 1987.

19. Berthornieu В., Diaz M. Modelling and verification of Time dependent systems using time Petri Nets // IEEE Transactions on Soft,ware Engineering. — 1991. — Vol. 17, no. 3. — Pp. 259-273.

20. Borceux F. Handbook of Categorical Algebra 1: Basic Category Theory. — Cambridge University Press, 1994.

21. Boudol G., Castellani I. Concurrency and atomicity // Theoretical Computer Science. — 1988. — Vol. 59, no. 1-2. — Pp. 25-84.

22. Bouyer P., Haddad S., Reynier P. Extended Timed Automata and Time Petri Nets // Proc. of the 6t,h Intl. Conf. on Application of Concurrency to System Design. — 2006. — Pp. 91-100.

23. Bouyer P., Haddad S., Reynier P. Timed Unfoldings for Networks of Timed Automata // Lecture Notes in Computer Science. — 2006. — Vol. 4218. Pp. 292-306.

24. Cattani G., Sassone V. Higher dimensional transition systems // Logic in Computer Science, 1996. LICS'96. Proceedings., Eleventh Annual IEEE Symposium on. — 1996. — Pp. 55-62.

25. Cerans K. Decidability of Bisimulation Equivalences for Parallel Timer Processes // Lecture Notes in Computer Science. — 1993. — Vol. 663.— Pp. 302-315.

26. Chatain Т., Jard C. Time supervision of concurrent systems using symbolic unfoldings of time petri nets. // Lecture Notes in Computer Science. 2005. — Vol. 3829. — Pp. 196-210.

27. Cheng A., Nielsen M. Open maps (at) work // Research Series RS-95-23, BRICS, Department of Computer Science, University of Aarhus, April. — 1995.

28. Cleaveland R., Zwarico A. A theory of testing for real-time // Lecture Notes in Computer Science.— 1991. — Vol. 663. — Pp. 110-119.

29. Darondeau P., Degano P. Event Structures, Causal Trees, and Refinements // Lecture Notes in Computer Science.— 1990.— Vol. 452. — Pp. 239-245.

30. De Nicola R., Hennessy M. Testing equivalence for processes // Theoretical Computer Science. — 1984. — Vol. 34. — Pp. 83-133.

31. Degano P., Gorrieri R., Vigna S. On Relating Some Models for Concurrency // Lecture Notes in Computer Science.— 1993.— Vol. 668. Pp. 15-30.

32. Dubtsov R. S. Real-time event structures and scott domains // Lecture Notes in Computer Science. — 2005. — Vol. 3606. — Pp. 42-48.

33. Dubtsov R. S. Semantic domains for real-time event structures // Proceedings of the International Workshop on Concurrency, Specification and Programming. — 2006. — Pp. 186-194.

34. Dubtsov R. S. Real-Time Stable Event Structures and Marked Scott Domains: An Adjunction // Lecture Notes in Computer Science. — 2007. Vol. 4378. - Pp. 443-450.

35. Dubtsov R. S., Virbitskaite I. B. A Comparative Account of Timed Event Structures. // Proc. of 17th International Workshop «Concurrency, Specification and Programming».— Gross Vaeter See (Germany): 2008. Pp. 500-511.

36. Engelfriet J. Branching processes of Petri nets // Acta Informatica. — 1991. — Vol. 28, no. 6. Pp. 575-591.

37. Fidge C. A constraint-oriented real-time process calculus. // FORTE. — Vol. C-10 of IFIP Transactions. 1992. — Pp. 363-378.

38. Goltz U., Gotz N. Modelling a simple communication protocol in a language with action refinement // Draft version. — 1991.

39. Goltz U., Wehrheim H. Causal Testing // Lecture Notes in Computer Science. 1996. - Vol. 1113. — Pp. 394-406.

40. Goubault E. Domains of Higher-Dimensional Automata // Proceedings of the 4th International Conference on Concurrency Theory.— 1993.— Pp. 293 307.

41. Goubault E., Jensen T. Homology of Higher Dimensional Automata // International Conference on Concurrency Theory. — 1992. — Pp. 254268.

42. Gribovskaya N., Virbitskaite I. Open Maps and Observational Equivalences for Timed Partial Order Models / / Fundamenta Informaticae. — 2004. — Vol. 60, no. 1. — Pp. 383-399.

43. Hennessy M. Algebraic theory of processes. Series in the Foundations of Computing. MIT Press, 1988.

44. Hennessy M., Cleaveland R. Testing equivalence as bisimulation equivalence // Lecture Notes in Computer Science.— 1989.— Vol. 407. Pp. 11-23.

45. Hennessy M., Milner R. Algebraic laws for nondeterminism and concurrency // Journal of the ACM (JACM). — 1985. — Vol. 32, no. 1. — Pp. 137 161.

46. Henzinger Т., Pnucli A., Manna Z. Timed Transition Systems // Lecture Notes in Computer Science. — 1992. — Vol. 600. — Pp. 226-251.

47. Hildebrandt Т., Sassone V. Comparing Transition Systems with Independence and Asynchronous Transition Systems // International Conference on Concurrency Theory. — 1996. — Pp. 84-97.

48. Hoare C. Communicating Sequential Processes. Series in Computer Science. — Prentice-Hall International, 1985.

49. Hoogers P., Kleijn H., Thiagarajan P. An event structure semantics for general Petri nets // Theoretical Computer Science. — 1996. — Vol. 153, no. 1-2. Pp. 129-170.

50. Hune Т., Nielsen M. Timed bisimulation and open maps // Lecture Notes in Computer Science. — 1998. — Vol. 1450. — Pp. 378-387.

51. Joyal A., Nielsen M., Winskel G. Bisimulation from open maps // Information and Computation. — 1996. — Vol. 127, no. 2. — Pp. 164185.

52. Katoen J. Quantitative and Qualitative Extensions of Event Structures: Ph.D. thesis / University of Twente. — 1996.

53. Maggiolo-Schettini A., Winkowski J. Towards an algebra for timed behaviours // Theoretical Computer Science. — 1992. — Vol. 103, no. 2. Pp. 335-363.

54. McLane S. Categories for the Working Mathematician // Graduate Texts in Mathematics. Springer, Berlin.— 1971.

55. Merlin P., Farber D. Recoverability of Communication Protocols Implications of a Theoretical Study // IEEE Transactions on Communications. — 1976. — Vol. 24, no. 9. — Pp. 1036-1043.

56. Meseguer J., Montanari U., Sassone V. On the Semantics of Petri Nets // Lecture Notes in Computer Science. — 1992. — Vol. 630. — Pp. 286-301.

57. Milner R. A Calculus of Communicating Systems. — Springer-Verlag New York, Inc. Secaucus, NJ, USA, 1982.

58. Milner R. Communication and concurrency. — 1989.

59. Milner R., Sangiorgi D. Barbed bisimulation // Proceedings of 1С ALP. 1992. - Vol. 92. - Pp. 685-695.

60. Murphy D. Time and duration in noninterleaving concurrency // Fundamenta Informaticae. — 1993. — Vol. 19, no. 3-4. — Pp. 403-416.

61. Nielsen M., Hune T. Timed bisimulation and open maps // Research Series RS-98-4, BRICS, Department of Computer Science, University of Aarhus, February. — 1998.

62. Nielsen M., Plotkin G., Winskel G. Petri Nets, Event Structures and Domains, Part If/ Theoretical Computer Science. — 1981.— Vol. 13, no. 1. Pp. 85-108.

63. Nielsen M., Rozenberg G., Thiagarajan P. Behavioural notions for elementary net systems // Distributed Computing. — 1990. — Vol. 4, no. 1, —Pp. 45-57.

64. Nielsen M., Winskel G. Petri nets and bisimulation // Theoretical Computer Science. — 1996. — Vol. 153, no. 1-2. — Pp. 211-244.

65. On Specifying Real-Time Systems in a Causality-Based Setting / J. Katoen, R. Langerak, D. Latella, E. Brinksma // Lecture Notes in Computer Science. — 1996. — Vol. 1135. — Pp. 385-404.

66. Park D. Concurrency and automata on infinite sequences // Theoretical Computer Science. — 1981. — Vol. 104. — Pp. 167-183.

67. Pinna G., Poigne A. On the nature of events: another perspective in concurrency // Theoretical Computer Science. — 1995.— Vol. 138, no. 2. Pp. 425-454.

68. Popova L. On Time Petri Nets // Journal Information Processing and Cybernetics, EIK. — 1991. — Vol. 27, no. 4. — Pp. 227-244.

69. Pratt V. Modeling Concurrency with Geometry // Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages. — 1991. — Pp. 311-322.

70. Rabinovich A., Trakhtenbrot B. Behavior structures and nets // Fundamenta Informaticae. — 1988. — Vol. 11, no. 4. — Pp. 357-404.

71. Ramchandani C. Analysis of asynchronous concurrent systems using timed Petri nets: Ph.D. thesis / Massachusetts Institute of Technology Cambridge, Dept. Electronical Engineering, MA, USA. — 1974.

72. Sassone V., Nielsen M., Winskel G. Models for concurrency: towards a classification // Theoretical Computer Science. — 1996. — Vol. 170, no. 1-2. Pp. 297-348.

73. Shields M. Concurrent Machines // The Computer Journal. — 1985.— Vol. 28, no. 5. — Pp. 449-465.

74. Srba J. Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets // Lecture Notes in Computer Science. — 2008. Vol. 5215. - Pp. 15-32.

75. Starke P. Some properties of timed nets under the earliest firing rule // Lecture Notes in Computer Science. — 1990. — Vol. 424. — Pp. 418-432.

76. Steffen В., Weise C. Deciding Testing Equivalence for Real-Time Processes with Dense Time // Lecture Notes in Computer Science. — 1993. Pp. 703-713.

77. Temporal structures / R. Casley, R. Crew, J. Meseguer, V. Pratt //

78. Mathematical Structures in Computer Science. — 1982. — Vol. 1, no. 2. — Pp. 179-213.

79. Timed CSP: Theory and Practice / S. Schneider, J. Davies, D. Jackson et al. // Proceedings of the Real-Time: Theory in Practice, REX Workshop. 1991. - Pp. 640-675.

80. Weise C., Lenzkes D. Efficient Scaling-Invariant Checking of Timed Bisimulation // Proceedings of the 14th Annual Symposion on Theoretical Aspects of Computer Science (STACS 1997), LNCS. — Vol. 1200. Pp. 177-188.

81. Winskel G. Events in Computation: Ph.D. thesis / University of Edingurgh. — 1980.

82. Winskel G. Event structures // Lecture Notes in Computer Science. — 1987. — Vol. 255. Pp. 325-392.

83. Winskel G. An introduction to event structures j j Lecture Notes in Computer Science. — 1988. Vol. 384. — Pp. 364-397.

84. Winskel G., Nielsen M. Models for concurrency // Handbook of Logic in Computer Sciencc. — 1995. — Vol. 4. — Pp. 1-148.