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

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

Грибовская Наталия Сергеевна

Теоретико-категорное исследование эквивалентностей параллельных моделей с реальным временем

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

Автореферат

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

Новосибирск, 2004

Работа выполнена на кафедре вычислительных систем механико-математического факультета Новосибирского государственного университета

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

руководитель: Вирбицкайте Ирина Бонавентуровна

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

оппоненты:

доктор технических наук Бандман Ольга Леонидовна

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

Томский

политехнический университет

Защита состоится 28 декабря 2004 года в 16 часов на заседании диссертационного совета КООЗ.032.01 в Институте систем информатики им. А. П. Ершова Сибирского отделения РАН по адресу:

630090, г. Новосибирск, пр. Акад. Лаврентьева, 6.

С диссертацией можно ознакомится в читальном зале ИСИ СО РАН (г. Новосибирск, пр. Акад. Лаврентьева, 6).

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

Ученый секретарь диссертационного совета К003.032.01

Мурзин Федор Александрович

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

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

Среди отечественных исследований в этой области отметим работы Н.А. Анисимова, О.Л. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, В.Е. Котова, И.А. Ломазовой, В.А. Соколова, В.А. Непомнящего, Л.А. Черкасовой, а среди зарубежных — работы Г. Винскеля, М. Нильсена, В. Пратта, М. Хеннеси, Р. Милнера, Дж.-П. Катоена, Д. Мерфи, Л. Чайя.

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

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

Большое многообразие моделей, предложенных в теории параллелизма, требует их систематизации и унификации. Часто отношения между моделями могут быть охарактеризованы в терминах пове-

РЭС. НАЦИОНАЛЬНА* i

3 ВКМЧОТМА I

УЩВУ j

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

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

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

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

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

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

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

1. Исследование и развитие формальных методов эквивалентных преобразований параллельных программ, функционирующих в режиме реального времени.

2. Построение теоретико-категорных основ исследования временных трассовых, тестовых и бисимуляционных эквивалентностей моделей в семантиках интерливинг/истинный параллелизм.

3. Исследование проблемы распознавания указанных временных эквивалентностей с использованием методов теории категорий.

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

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

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

• Введены временные варианты поведенческих (трассовых, тестовых и бисимуляционных) эквивалентностей в семантиках интерливинг/истинный параллелизм.

• Дана теоретико-категорная характеризация вышеуказанных эк-вивалентностей в терминах открытых морфизмов на основе их 'зиг-заг' характеризации.

• Решены проблемы и даны оценки сложности распознавания указанных эквивалентностей.

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

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

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

1. Разработка и исследование семантических методов и средств спецификации и верификации сложных распределенных систем реального времени. РФФИ, грант 0001 00898, руководитель к.ф.-м.н. И.Б. ВИРБИЦКАЙТЕ, 2000-2001.

2. Программа РАН "Научные проекты молодых ученых", грант 114, руководитель к.ф.-м.н И.В. ТАРАСЮК, 1999-2001.

3. Исследование параллельных процессов реального времени методами теории категорий. Министерство образования, грант А03-2.8-353, руководитель д.ф.-м.н. И.Б. ВИРБИЦКАЙТЕ, 2003-2004.

4. Исследование параллельных процессов реального времени методами теории категорий. Федеральное агентство по образованию, грант А04-3.16-217, руководитель д.ф.-м.н. И.Б. ВИРБИЦКАЙТЕ, 2004.

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

• International Symposium on Fundamentals of Computation Theory (Riga, Latvia, 2001);

• International Seminar Concurrency: Specification and Programming (Berlin, Germany, 2002; Charna, Poland, 2003);

• A. P. Ershov International Memorial Conference on Perspectives of System Informatics (Novosibirsk, Russia, 2003);

• International conference on practical and theoretical programming UkrProg'04 (Kiev, Ukraine, 2004).

Кроме того, полученные результаты обсуждались на семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры вычислительных систем НГУ.

Публикации. По теме диссертации написано 11 научных работ, среди которых 4 работы опубликованы в зарубежных периодических изданиях и журналах, 1 — в отечественном журнале, 3 — в трудах международных конференций и семинаров.

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

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

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

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

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

В разделе 2.1 вводится и исследуется временная интерливинговая трассовая эквивалентность на ВСП. Данная эквивалентность определяется в терминах равенства временных интерливинговых языков систем. Приводится формальное определение и свойства категории ВСП, СТТ5е, построенной Хунэм и Нильсеном в 1998 году. Выделяется подкатегория Т^ этой категории, содержащая все временные слова и тождественные морфизмы и морфизмы с пустой областью определения между ними. По данной подкатегории стандартным способом определяется понятие -открытого морфизма и доказывается его критерий в терминах сохранения выполнений временных слов. Затем формулируется понятие абстрактной Ти-бисимуляции в терминах существования симметричной конструкции

-открытых морфизмов. Доказывается следующая

Теорема 2.3. Две ВСП являются Р-5исимуляционно эквивалентными они временно интерливингово трассово эквивалентны. Далее рассматривается проблема распознавания временной интер-ливииговой трассовой эквивалентности в контексте класса конечных ВСП, TTSn- При помощи техники регионов Алура доказывается разрешимость Vtr-открытости морфизма. Сложность этого распознавания оценивается как |Si| • • |-Xi|! • • {2с + где Х1 и Х2 — множества временных переменных

ВСП, Sj и S2 — множества состояний ВСП, а с — наибольшее натуральное число, встречающаяся во временных конструкциях. Для ВСП из класса TTSn доказывается, что из существования симметричной конструкции Р^-открытых морфизмов следует существование аналогичной конструкции с вершиной из класса TTSn На основе этого факта и разрешимости Vtr-открытости морфизмов формулируется

Следствие 2.5. Для ВСП из класса TTSм временная интерливинго-вая трассовая эквивалентность разрешима.

В разделе 2.2 вводится и исследуется частично-упорядоченная эквивалентность Пратта на ВСС. Эта эквивалентность определяется в терминах равенства временных частично-упорядоченных языков Прат-та, которые содержат все приращения, определяемые относительно частичного порядка, для всех временных рот-множеств, выполняемых ВСС. Определяется категория ВСС CT£SP и доказывается ряд полезных свойств этой категории. Далее выделяется подкатегория TS'PL категории CT£SP, содержащая все временные рот-множества и тождественные морфизмы и морфизмы с пустой областью определения между ними. По данной подкатегории стандартным способом определяется понятие открытого морфизма и доказывается

его критерий в терминах сохранения выполняемых рот-множеств. Затем формулируется понятие абстрактной TV'P^-бисимуляции в терминах существования симметричной конструкции открытых

морфизмов. Доказывается следующая

Теорема 2.8. Две ВСС являются ТР'^-бисимуляционно эквивалентными они временно частично-упорядоченно эквивалентны по Пратту.

Далее рассматривается проблема распознавания частично-упорядочен-ной эквивалентности Пратта в контексте класса конечных ВСС, При помощи техники регионов Алура доказывается разрешимость ГР'^-открытости морфизма. Сложность этого распознавания оценивается как N ■ 22N ■ (с + 1)N, где N = \Ei\ * \Е2\ (|£i| и

\Е2\ — число событий ВСС), а с — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса ТЕБн доказывается, что из существования симметричной конструкции ТР'^-открытых морфизмов следует существование аналогичной конструкции с вершиной из класса 7~£5м. На основе этого факта и разрешимости ТР'^-открытости морфизмов формулируется

Следствие 2.5. Для ВСС из Т5N временная частично-упорядоченная эквивалентность Пратта разрешима.

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

полезных свойств этой категории. Далее в построенной категории выделяется подкатегория , содержащая все временные рот-

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

Далее рассматривается проблема распознавания частично-упорядо-ченной трассовой эквивалентности в контексте класса При

помощи техники регионов Алура доказывается разрешимость ТР£ открытости морфизмов. Сложность этого распознавания оценивается как ЛГ. 2Ш ■ (с + где N = |Ег| * \Е2\ (|£а| и \Е2\ - число событий ВСС), а с — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса доказывается, что из

существования симметричной конструкции открытых морфизмов следует существование аналогичной конструкции с вершиной из класса На основе этого факта и разрешимости ТТ^- открытости морфизмов формулируется

Следствие.2.7. Для ВСС из Т^ временнаячастично-упорядоченная трассовая эквивалентность разрешима.

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

В разделе 3.1 вводится и исследуется временная интерливинговая тестовая эквивалентность на ВСП. Такая эквивалентность формулируется в терминах равенства набора выполняемых интерливинговых тестов. Определяется категория ВСП СТТвгеаг и доказываются некоторые свойства этой категории. Далее в указанной категории выделяется подкатегория содержащая

наблюдения (ВСП специального вида) и морфизмы между ними. По этой подкатегории определяется Тгезь-открытый морфизм и доказывается его критерий в терминах сохранения отношения перехода на достижимых множествах и вложения множеств последующих временных действий. Затем определяется абстрактная Т^е«! бисимуляция в терминах существования конструкции -открытых морфизмов и доказывается следующая

Теорема 3.3. Две ВСП являются Т^ев^бисимуляционно эквивалентными они временно интерливингово тестово эквивалентны.

Далее рассматривается проблема распознавания временной интерливинговой тестовой эквивалентности на классе конечных дискретных ВСП, ТТБ^30. При помощи техники регионов Алура доказывается разрешимость -открытости для морфизмов

выделенного класса. Сложность этого распознавания оценивается З^М^-г1*1' |Хг1 ^ где ^ иХ2 — множества временных переменных ВСП, а и — множества состояний ВСП. Для ВСП из класса доказывается, что из существования симметричной конструкции "Рьеяг открытых морфизмов следует существование аналогичной конструкции с вершиной из класса ТТБ^0. На основе этого факта и разрешимости Тгеаь -открытости морфизмов доказывается

Следствие 3.1. Для ВСП из класса временная интерливин-

говая тестовая эквивалентность разрешима.

В разделе 3.2 вводится и исследуется временная частично -упорядоченная тестовая эквивалентность на ВСС. Такая эквивалентность определяется в терминах совпадения набора выполняемых частично-упорядоченных тестов. Определяется категория ВСС СГЕБг и доказываются основные свойства этой категории. Далее в этой категории выделяется подкатегория Т7*ь, содержащая ВСС и тождественные морфизмы и морфизмы с пустой областью определения. По данной подкатегории определяется ТТ/,-открытый морфизм и доказывается его критерий в терминах сохранения отношения следования на множествах состояний ВСС, достижимых по рот-множеству, и вложения множеств последующих временных действий. Затем формулируется понятие абстрактной ТТ^-бисимуляции в терминах существования конструкции ТТ^-открытых морфизмов и доказывается следующая

Теорема 3.7. Две ВСС являются Т7~г,-бисимуляционно эквивалентными они временно частично-упорядоченно тестово эквивалентны.

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

Алура доказывается разрешимость ТТ^-открытости морфизмов для выделенного класса. Сложность такого распознавания оценивается как Т, где N = \Ег\.* \Е2\ (|£а| и \Е2\ - число событий ВСС). Для ВСС из класса доказывается, что из существования симметричной

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

Следствие 3.2. Для ВСС из класса временная частично-

упорядоченная тестовая эквивалентность разрешима.

В четвертой главе вводятся и исследуются временные варианты бисимуляционных эквивалентностей: временная интерливинговая слабая бисимуляция по Милнеру и Сангиорги и временная частично-упорядоченная сильная сохраняющая историю бисимуляция. Бисимуляционные эквивалентности являются наиболее сильными в том смысле, что в отличии от трассовых и тестовых они учитывают точки недетерминированного выбора.

В разделе 4.1 вводится и исследуется временной вариант интерливинговой слабой бисимуляции по Милнеру и Сангиорги на В СП. Такая бисимуляция отличается от сильной бисимуляции,

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

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

Теорема 4.5. Две ВСС являются Р^ь^-бисимуляционно эквивалентными они временнб интерливингово слабо бисимуляционно эквивалентны по Милнеру и Сангиорги.

Далее рассматривается проблема распознавания временной интерливинговой слабой бисимуляции по Милнеру и Сангиорги на классе ТТ5N. При помощи техники регионов Алура доказывается разрешимость Т^ь^-открытости для морфизмов указанного класса. Сложность данного распознавания оценивается как N • |5а| • \Х!\\ ■ \Х2\\ ■ 21а''1+№1 • (2с + 2)№НХ=1, где и Х2 — множества временных переменных ВСП, S1 и S2 - множества состояний ВСП, а с — наибольшее натуральное число, встречающееся во временных конструкциях. Для ВСП из класса доказывается,

что из существования симметричной конструкции -открытых

морфизмов следует существование аналогичной конструкции с вершиной из класса . На основе этого факта и полученной

разрешимости доказывается следующее

Следствие 4.3. Для ВСП из класса ТТвц временная интерли-винговая слабая бисимуляция по Милнеру и Сангиорги разрешима.

В разделе 4.2 вводится и исследуется временная частично-упоря-доченная сильная сохраняющая историю бисимуляция на ВСС. При исследовании этой эквивалентности используется ранее построенная категория СТ£5р. В этой категории выделяется подкатегория IVг, содержащая временные рот-множества и морфизмы между

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

Теорема 4.10. Две ВСС являются ТР^-бисимуляционно эквивалентными они временно частично-упорядоченно сильно бисимуляционно эквивалентны с сохранением истории.

Далее рассматривается проблема распознавания временной частично-упорядоченной сильной сохраняющей историю бисимуляции на классе ТЕБи При помощи техники регионов Алура доказывается разрешимость ТР£-открытости для морфизмов указанного класса. Сложность этого распознавания оценивается как N • 2"1 • (с + 1)", где N = 1^1 * \Е2\ (1^1 и |£2| - число событий ВСС), а с — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса 7"£<5>м доказывается, что из существования симметричной конструкции -открытых морфизмов следует существование аналогичной конструкции с вершиной из класса На основе этого факта и полученной разрешимости

доказывается

Следствие 4.5. Для ВСС из Т^м временная частично-упорядоченная сильная сохраняющая историю бисимуляция разрешима.

ОСНОВНЫЕ ВЫВОДЫ И РЕЗУЛЬТАТЫ

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

1. Построены различные категории параллельных моделей — временных систем переходов и временных структур событий — и доказаны некоторые их свойства.

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

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

4. Определены и проанализированы временные варианты бисимуляционных эквивалентностей. В том числе временная

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

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

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

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ Н.С. ГРИБОВСКОЙ (МОСКАЛЕВОЙ)

1. Н.С. Грибовская. Теоретико-категорная характеризация языковых эквивалентностей временных параллельных моделей // Труды школы-конкурса "Новые подходы и решения". - ИСИ СО РАН, Новосибирск. - 2003. - С. 32-41.

2. Н.С. Грибовская. Теоретико-категорная характеризация трассовой эквивалентности для временных автоматных моделей // Проблемы программирования, 2004. - № 2-3. - С. 16-22.

3. Н.С. Грибовская. Теоретико-категорная характеризация различных эквивалентностей на временных автоматных моделях // Препринт ИСИ СО РАН, 2004. - № 119.

4. Н.С. Москалева. Теоретико-категорная характеризация трассовой эквивалентности временных параллельных моделей // Препринт ИСИ СО РАН, 2002. - № 99.

5. Н.С. Москалева. Теоретико-категорное исследование параллельных процессов реального времени // Вестник НГУ, серия: Математика, механика, информатика, 2002. - Т. II, выпуск 3. - С. 46-66.

6. N.S. Moskaleva, I.B. Virbitskaite. On the Category of Event Structures with Dense Time // Lectures Notes Computer Science, 2001. - Vol. 2138. - p. 287-298.

7. N.S. Moskaleva, I.B. Virbitskaite. Observing Time-Sensitive Partial

Order Equivalences Categorically // In Proc. Workshop on Concurrency, Specification and Programming, Berlin, 2002. - p. 243-254.

8. N.S. Moskaleva, I.B. Virbitskaite. Open Maps and Trace Semantics for Timed Partial Order Models // In Proc. of the Andrei Ershov Fifth International Conference "Perspectives of System Informatics", 2003. - p. 160-167.

9. Virbitskaite I. B., Gribovskaya N. S. Open Maps and Testing Equivalences for Timed Partial Order Models // In Proc. Workshop on Concurrency, Specification and Programming, Poland, 2003. - p. 195-206.

10. I.B. Virbitskaite, N.S. Gribovskaya. Open Maps and Trace Semantics for Timed Partial Order Models // Lecture Notes in Computer Science, 2003. - Vol. 2890. - p. 248-259.

11. I.B. Virbitskaite, N.S. Gribovskaya. Open Maps and Observational Equivalences for Timed Partial Order Models // Fundamenta Infor-maticae, 2004. - Vol. 61. - p. 383-399.

ЛИЧНЫЙ ВКЛАД АВТОРА

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

БЛАГОДАРНОСТИ

Автор выражает свою признательность своему научному руководителю д.ф.-м.н. Вирбицкайте Ирине Бонавентуровне за помощь и понимание.

1- - 95 3

Грибовская Наталия Сергеевна

Теоретикокатегорное исследование эквивалентностей параллельных моделей с реальным временем

Подписано в печать 18.11.2004 Формат бумаги 60 х84 1 /16

50*Щ а/ £¡/9

Объем 1,0 п.л. Тираж 100 экз.

ЗАО РИЦ "Прайс-курьер" 630090, г. Новосибирск, пр. Акад. Лаврентьева, б, тел. (383-2) 34-22-02

Введение

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

1.1. Сравнительная характеристика безвременных моделей.

1.1.1. Модели параллельных процессов.

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

1.2. Анализ эквивалентностей методами теории категорий.

1.2.1. Открытые морфизмы.

1.2.2. Теоретико-категорная характеризация эквивалентностей

2. Трассовые эквивалентности для временных моделей

2.1. Интерливинговая трассовая эквивалентность.

2.1.1. Модель временных систем переходов.

2.1.2. Категория временных систем переходов СТТБ^.

2.1.3. 7\г-открытые морфизмы.

2.1.4. Теоретико-категорная характеризация эквивалентности

2.1.5. Разрешимость для конечного подкласса.

2.2. Частично-упорядоченная эквивалентность Пратта.

2.2.1. Модель временных структур событий.

2.2.2. Категория временных структур событий СТ££Р.

2.2.3. ТР'^-открытые морфизмы.

2.2.4. Теоретико-категорная характеризация эквивалентности

2.2.5. Разрешимость для конечного подкласса.

2.3. Частично-упорядоченная трассовая эквивалентность

2.3.1. Категория временных структур событий СТ

2.3.2. ТР^-открытые морфизмы.

2.3.3. Теоретико-категорная характеризация эквивалентности

2.3.4. Разрешимость для конечного подкласса.

3. Тестовые эквивалентности для временных моделей

3.1. Интерливинговая тестовая эквивалентность.

3.1.1. Категория временных систем переходов СТТЭгевг.

3.1.2. ^¿¡¿-открытые морфизмы.

3.1.3. Теоретико-категорная характеризация эквивалентности

3.1.4. Разрешимость для дискретного подкласса.

3.2. Частично-упорядоченная тестовая эквивалентность.

3.2.1. Категория временных структур событий СТ£5(.

3.2.2. ТТ^-открытые морфизмы.

3.2.3. Теоретико-категорная характеризация эквиваленстности

3.2.4. Разрешимость для дискретного подкласса.

4. Бисимуляционные эквивалентности для временных моделей

4.1. Интерливинговая слабая бисимуляция по Милнеру и Сангиорги

4.1.1. Категория временных систем переходов CTTSwus.

4.1.2. Ргу^з-открытые морфизмы

4.1.3. Теоретико-категорная характеризация эквивалентности

4.1.4. Разрешимость для конечного подкласса.

4.2. Частично-упорядоченная сильная сохраняющая историю бисимуляция

4.2.1. TVPL-открытые морфизмы

4.2.2. Теоретико-категорная характеризация эквивалентности

4.2.3. Разрешимость для конечного подкласса.

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

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

Среди отечественных исследований по формальным моделям и спецификации и верификации распределенных и параллельных систем отметим работы H.A. Анисимова, O.JI. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, В.Е. Котова, И.А. Ломазовой, В.А. Соколова, В.А. Непомнящего, J1.A. Черкасовой, а среди зарубежных — работы Г. Винскеля, М. Нильсена, В. Пратта, М. Хеннеси, Р. Милнера, Дж.-П. Катоена, Д. Мерфи, J1. Чайя.

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

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

Одной из наиболее популярной классификацией формальных моделей является подход Интерливинговая семантика и 'истинный параллелизм'. При интер-ливинговом подходе параллелизм событий моделируемой системы линеаризуется, т.е. моделируется последовательной реализацией параллельных событий в произвольном недетерминированном порядке. Другими словами, интерливинговые модели описывают параллельные процессы точно так же, как однопроцессорная система исполняет программы в мультизадачном режиме. Это означает, что параллелизм вычислений сводится к некоторой форме недетерминизма. Из вышеупомянутых моделей к этой группе относятся системы переходов и деревья синхронизации. Альтернативный подход — 'истинный параллелизм' — предполагает, что все события системы изначально считаются независимыми. Кроме того, отношение причинной зависимости на событиях (например, готовность данных, наличие ресурсов) задается частичным порядком, а отношение параллелизма — отсутствием такого порядка. Данные модели являются более приемлемыми для изучения таких свойств параллельных процессов, как отсутствие тупиков, 'справедливость' (fairness), максимальный параллелизм и т.д. Типичные представители этого подхода — сети Петри, частично упорядоченные множества, структуры событий, системы переходов с независимостью и др.

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

• дискретное/непрерывное время. Для моделей дискретного времени таких, как модель временных сетей Петри, предложенная Рамчандани [82], время определяется на целых числах. Такой подход обычно используется для описания поведения систем с общим глобальным счетчиком времени. Время делится на счетное количество интервалов: п + 1-й интервал начинается во время п и заканчивается во время п + 1. Дальнейшее определение времени внутри интервалов не предусматривается.

В моделях непрерывного времени таких, как модели Мерлина, Фабера, Ка-тоена и Мерфи [43, 60, 65, 73], время измеряется по непрерывной временной шкале. Эта модель подразумевает возможность выполнения неограниченного числа событий между двумя последовательными переходами системы. Для моделей систем реального времени, например для моделей Алура и Дилла [17], более подходящим является подход непрерывного времени.

• явное/неявное понятие прохождения времени. Известно, что прогрессиро-вание временной системы всегда идет одним из двух способов — выполнение действия или прохождение некоторого отрезка времени. В случае явного введения понятия времени, время добавляется полностью ортогональным способом, разделяя прохождение времени и выполнение действий. Первый подход рассмотрен Йонедой и Кларком [97], а второй — Катоеном, Асето, Мерфи, Мерлином и Фабером [16, 60, 65, 73].

• задерживающиеся/мгновенные действия. В моделях, введенных Дженсе-ном, Поелем, By, Рамчандани, Асето и Мерфи [16, 54, 73, 82] задержка действия смоделирована в качестве временного промежутка между началом действия и его окончанием. Во втором подходе выполнение действия само не требует времени, но может быть отложено на определенный срок. Такой подход использовался при построении моделей такими учеными как Катоен, Фабер, Мерлин [43, 60, 65].

• с/без использования локальных счетчиков. Локальные счетчики позволяют записать эволюцию различных частей дистрибутивных состояний. Иначе говоря, это означает, что каждое событие имеет таймер задержки, который начинает отсчитывать время, когда событие становится активным и останавливается, когда событие пассивно либо начинает исполнение. Это позволяет достаточно легко изучать систему локально. Такие модели были введены Кларком, Йонедой, Фабером, Милнером, Асето и Мерфи [16, 65, 97]. С другой стороны, что было продемонстрировано в Катоеном [60], операционная семантика временных алгебраических процессов более проста, если не использовать локальные счетчики.

• несвоевременные/последовательные следы. Несвоевременность — это явление, которое зачастую старательно избегается ([65, 97]) так, как старшинство временных событий следа не отражает их временного порядка. В [16, 60] сообщалось, что несвоевременные следы позволяют построить семантику реального параллелизма временных интерливинговых процессов алгебры и показывалось, что время позволяет связать реальный параллелизм и интерливинг.

• срочные/несрочные действия. Понятие срочного действия означает, что действие вынуждено выполниться, как только оно готово. Такие модели были изучены Милнером, Фабером, Винковским, Асето и Мерфи ([16, 64, 65]). Однако, иногда это означает полное затягивание временных действий. Один из способов решения этой проблемы — это добавление несрочных действий. Например, в [21, 60] были представлены оба вида действий.

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

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

В рамках теории категорий также были предложены абстрактные определения ряда поведенческих эквивалентностей для различных безвременных моделей, что позволило решить проблему разрешимости таких эквивалентностей для систем с конечным числом состояний. В этой области были получены следующие результаты: эквивалентности, определенные на категориях интерливинговых моделей, согласуются с интерливинговой бисимуляцией Милнера, тогда как эквивалентности на категориях моделей с 'истинным параллелизмом' требуют более сильной эквивалентности — некоторого варианта сохраняющей историю бисимуляции Трахтенброта.

В 90-х годах прошлого столетия в литературе были сделаны попытки ввести понятие времени в эквивалентностные отношения, чтобы позволить исследовать временные аспекты поведения систем. Для различных моделей с дискретным временем Хеннесси и др. были найдены альтернативные характеризации тестовых эквивалентностей, позволяющие строить алгоритмы их распознавания за счет сведения тестовых эквивалентностей к различным вариантам бисимуляционных эквивалентностей. Коррадини, Фоглером и Дженнаром было установлено совпадение дискретно-временных и непрерывно-временных тестовых эквивалентностей в контексте модели алгебр процессов, в которой время, приписываемое действию, представляет собой ограничение на наиболее позднее выполнение данного действия. Однако эти авторы нашли только необходимые условия существования временной тестовой эквивалентности, что не позволило построить алгоритм ее распознавания. Проблемы распознавания временных тестовых эквивалентностей для интерливинговых автоматных моделей с непрерывным временем были исследованы в работах Штефана и Вайзе. Суть изложенного в этих статьях подхода состоит в том, что временная тестовая эквивалентность сводится к некоторому варианту 'невременной' бисимуляции, что позволяет адаптировать уже известные алгоритмы распознавания бисимуляционной эквивалентности. Разрешимость временной бисимуляции для временных интерливинговых моделей, а именно, автоматов с непрерывным временем, была показана Черансом. Альтернативное решение проблемы распознавания временной бисимуляции для другой временной интерливинговой модели — временных систем переходов — с использованием методов теории категорий было предложено Хунэм и Нильсеном.

На основе вышесказанного можно прийти к заключению, что уже сложившийся подход к разработке корректных параллельных систем имеет ряд ограничений: недостаточно проработаны временные аспекты функционирования параллельных систем; имеет место проблема 'взрыва состояний' при анализе систем такого типа; временные эквивалентностные понятия введены только для ограниченного числа параллельных моделей с реальным временем, а также недостаточно изучены их взаимосвязи и разрешимость и т.д.

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

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

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

1) Исследование и развитие формальных методов эквивалентных преобразований параллельных программ, функционирующих в режиме реального времени.

2) Построение теоретико-категорных основ исследования временных трассовых, тестовых и бисимуляционных эквивалентностей моделей в семантиках интерливинг/истинный параллелизм.

3) Исследование проблемы распознавания указанных временных эквивалентностей с использованием методов теории категорий.

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

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

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

• Введены временные варианты поведенческих (трассовых, тестовых и биси-муляционных) эквивалентностей в семантиках интерливинг/истинный параллелизм.

• Дана теоретико-категорная характеризация вышеуказанных эквивалентностей в терминах открытых морфизмов на основе их 'зиг-заг' характе-ризации.

• Решены проблемы и даны оценки сложности распознавания указанных эквивалентностей.

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

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

1) Разработка и исследование семантических методов и средств спецификации и верификации сложных распределенных систем реального времени. РФФИ, грант 0001 00898, руководитель к.ф.-м.н. И.Б. Вирбицкайте, 2000-2001. (Публикации [69].)

2) Программа РАН "Научные проекты молодых ученых", грант 114, руководитель к.ф.-м.н И.в. тарасюк, 1999-2001. (Публикации [12, 13])

3) Исследование параллельных процессов реального времени методами теории категорий. Министерство образования, грант АОЗ-2.8-353, руководитель д.ф.-м.н. И.Б. Вирбицкайте, 2003-2004. (Публикации [6, 7, 85, 86].)

4) Исследование параллельных процессов реального времени методами теории категорий. Федеральное агентство по образованию, грант А04-3.16-217, руководитель д.ф.-м.н. И.Б. Вирбицкайте, 2004. (Публикации [8].)

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

• International Symposium on Fundamentals of Computation Theory (Riga, Latvia, 2001);

• International Seminar 'Concurrency: Specification and Programming' (Berlin, Germany, 2002; Charna, Poland, 2003);

• A.P. Ershov International Memorial Conference on Perspectives of System Informatics (Novosibirsk, Russia, 2003);

• International conference on practical and theoretical programming UkrProg'04 (Kiev, Ukraine, 2004).

Публикации. По теме диссертации написано 11 научных работ, Среди этих работ 4 работы опубликованы в зарубежных периодических изданиях и журналах, 1 — в отечественном журнале, 3 — в трудах международных конференций и семинаров.

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

Основные результаты главы

В данной главе были введены и исследованы временные варианты различных бисимуляционных эквивалентностей: временная интерливинговая слабая бисиму-ляция по Милнеру и Сангиорги на модели временных систем переходов и временная частично-упорядоченная сильная сохраняющая историю бисимуляция на модели временных структур событий. Первая из эквивалентностей определяется для временных систем переходов, множества помечающих действий которых содержит невидимое действие г. В рамках исследования была простроена и изучена категория временных систем переходов CTTSwMa. Для этой категории и категории временных структур событий CT£Sp, построенной во второй главе, были выделены следующие подкатегории: Vwbis в категории CTTSwus» содержащая т-ветви и морфизмы между ними, и TVvL в категории CT£SP, содержащая временные рот-множества и морфизмы между ними. На основе выделенных подкатегорий были определены варианты открытых морфизмов и получены их 'зиг-заг' характеризации, которые позволили определить теоретико-категорные аналоги вышеуказанных эквивалентностей в терминах существования конструкций соответствующих вариантов открытых морфизмов. На базе полученных результатов была решена проблема распознавания исследуемых бисимуляционных эквивалентностей в контексте классов конечных моделей и получены оценки сложности такого распознавания.

Заключение

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

1) Построены различные категории параллельных моделей — временных систем переходов и временных структур событий — и доказаны некоторые их свойства.

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

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

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

5) Выделен ряд подкатегорий, по ним определены соответствующие варианты открытых морфизмов и получена 'зиг-заг' характеризация для этих мор-физмов.

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

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

8) Получены результаты, касающиеся проблемы разрешимости исследуемых эквивалентностей, на различных конечных классах и оценена сложность распознавания.

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

1. Алгоритмы, математическое обеспечение и архитектура многопроцессорных вычислительных систем. // Под редакцией А.П. Ершова, Новосибирск, Наука, 1982.

2. А. Ахо, Дж. Хопкрофт, Дж. Ульман. Построение и анализ вычислительных алгоритмов // Москва, Мир, 1979.

3. С.М. Ачасова, О.Л. Бандман. Корректность параллельных вычислительных процессов. //Новосибирск, Наука, 1990.

4. И.Б. Вирбицкайте. Семантические модели в теории параллелизма // Новосибирск, 2000.

5. И.Б. Вирбицкайте. Формальные модели и анализ корректности параллельных систем и систем реального времени / / Диссетрация на соискание степени д.ф-м.н., Новосибирск, 2001.

6. Н.С. Грибовская. Теоретико-категорная характеризация языковых эквива-лентностей временных параллельных моделей // Труды школы-конкурса "Новые подходы и решения". ИСИ СО РАН, Новосибирск. - 2003. - С. 32-41.

7. Н.С. Грибовская. Теоретико-категорная характеризация трассовой эквивалентности для временных автоматных моделей // Проблемы программирования, 2004. № 2-3. - С. 16-22.

8. Н.С. Грибовская. Теоретико-категорная характеризация различных эквива-лентностей на временных автоматных моделях // Препринт ИСИ СО РАН, 2004. № 119.

9. P.M. Карп, P.E. Милнер. Параллельные схемы программ // Кибернетический сборник, Москва, Мир. 1976. - Т. 13. - с. 5-61.

10. В.Е. Котов. Сети Петри // Москва, Наука, 1984.

11. В.Е. Котов, A.C. Нариньяни. Асинхронные вычислительные процессы над памятью // Кибернетика, 1984. № 3. - с. 64-71.

12. Н.С. Москалева. Теоретико-категорная характеризация трассовой эквивалентности временных параллельных моделей // Препринт ИСИ СО РАН, 2002. № 99.

13. Н.С. Москалева. Теоретико-категорное исследование параллельных процессов реального времени // Вестник НГУ, серия: Математика, механика, информатика, 2002. Т. II, выпуск 3. - С. 46-66.

14. М.Ш. Цаленко, Е.Г. Шульгейфер. Лекции по теории категорий. М: Наука, 1974. - 438 с.

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

16. L. Aceto, D. Murphi. Timing and causality in process algebra. // Acta Informática, 1996. Vol. 33(4). - p. 317-350.

17. R. Alur, C. Courcoubetis, D. Dill. Model checking in dense real time. // Information and Computation, 1993. Vol. 104. - p. 2-34.

18. R. Alur, C. Courcoubetis, T.A. Henzinger. The observational power of clocks. // Lecture Notes in Computer Science, 1994. Vol. 836. - p. 162-177.

19. R. Alur, D. Dill. The theory of timed automata. // Theoretical Computer Science, 1994. Vol. 126. - p. 183-325.

20. M. V. Andreeva, E. N. Bozhenkova, I. B. Virbitskaite. Analysis of Timed Concurrent Models Based on Testing Equivalence. // Fundamenta Informaticae, 2000. Vol. 34. - p. 1-19.

21. C. Baier, J.-P. Katoen, D. Latella. Metric semantics for true concurrent real time.// Proc.25th Int. Colloquium, ICALP'98, Aalborg, Denmark, 1998. p. 568579.

22. M.A. Bendarczyk. Hereditory history preserving bisimulation or what is the power of the future perfect in program logics // Technical Report, Polish Academy of Science, Gdansk, 1991.

23. E. Best. A Theorem on the Characteristics of Non-Sequential Processe. // Fundamenta Informaticae, 1980. Vol. 3. - p. 77-94.

24. E. Best. The relative strength of K-density // Lect. Notes Сотр. Sci. 1980. -Vol. 84. - P. 261-276.

25. E. Best, C. Fernandez, H. Plünnecke. Concurrent systems and processes // Final Report on the Foundational Part of the Project BEGRUND, FMP-Studien. -GMD, Sankt Augustin, FDR, 1985. N 107.

26. E. Best, A. Marceron. D-continuity and Petri's axioms of concurrency for nonsequential process models/ / Fundamenta Informaticae. 1987. - Vol. X. -P. 161-212.

27. F. Borceux. Handbook of Categorical Algebra, vol. 2, 3. Encyclopedia of Mathematics and its Applications, vol. 51,52. // Cambridge University Press, 1994.

28. G. Boudol. Flow event structures and Flow Nets// Lect. Notes Сотр. Sci 1990. - Vol. 469. - P. 62-95.

29. G. Boudol, I. Castellani. Concurrency and atomicity. // Theoretical Computer Science, 1989. Vol. 59 - p. 25-84.

30. R.T. Casley, R.F. Crew, J. Meseguer, V.R. Pratt. Temporal structures. // Mathematical Structures in Computer Science 1(2), 1991, 179-213.

31. G.L. Cattani, V. Sassone. Higher dimentional transition systems// In Proc. LICS'96, 1996, 55-62.

32. A. Cheng, M. Nielsen. Open Maps (at) Work. // Technical Report RS-95-23, BRICS, 1995.

33. K. Cerans. Decidability of bisimulation equivalences for parallel timer processes. // Lecture Notes in Computer Science, 1993. Vol. 663. - p. 302-315.

34. L. A. Cherkasova, V.E. Kotov. Descriptive and analytical process algebras// Led. Notes Comp. Sci. 1989. - Vol. 424. - P. 77-104.

35. R. Cleaveland, M. Hennessy. Testing equivalence as a bisimulation equivalence. // Lecture Notes in Computer Science, 1989. Vol. 407. - p. 11-23.

36. R. Cleaveland, J. Parrow, B. Steffen The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems// J. ACM. 1993. - Vol. 15, N. 1. - P. 36-72.

37. R. Cleaveland, A.E. Zwarico. A theory of testing for real-time// Proc. 6th IEEE Logic, Information and Comput. Sci. Amsterdam, 1991. - P. 110-119.

38. L. Czaja. Cause-Effect Structures// Inform. Process. Letters. 1987/88. - V. 26(6).

39. L. Czaja. Minimal-Maximal Time Cause-Effect Structures// Fundamenta Informaticae. 1998. - Vol. 33. - P. 1-16.

40. C. Fernandez, P.S. Thiagarajan. D-continuous causal nets: A model of nonsequential processes// Theoretical Comput. Sci. 1984. - Vol. 284. - P. 171-196.

41. M. Fiore, G.L. Cattani, G. Winskel. Weak bisimulation and open maps //In Proc. LICS'99, 1999, 214-225.

42. S. Froeschle. Decidability of plain and hereditary history-preserving bisimilatiry for BPP //In Proc. EXPRESS' 99, 1999.

43. C. Fidge. A constraint-oriented real-time process calculus. // Formal Description Techniques V, IFIP Transactions, 1993. C-10. - p. 363-378.

44. R.J. van Glabbeek. The linear time branching time spectrum II: the semantics of sequential systems with silent moves. Extended abstract. // Lecture Notes in Computer Science, 1993. - Vol. 715. - p. 66-81.

45. R. Glabbeek, U. Goltz. Equivalence notions for concurrent systems and refinement of action / / Lecture Notes in Computer Science 379, 1989, 237-248.

46. U. Goltz, H. Wehrheim. Causal testing. // Lecture Notes in Computer Science, 1996. Vol. 1113. - p. 394-406.

47. M. Hennessy, R. Milner Algebraic laws for nondeterminism and cocurrency // Journal of ACM, 1985. Vol. 32. - p. 137-162.

48. M. Hennessy. Algebraic Theory of Processes. MIT Press series in the foundations of computing, 1988.

49. T.A. Henzinger, Z. Manna, A. Pnueli. Timed transition systems // Lecture Notes in Computer Science, 1991. Vol. 600. - p. 226-251.

50. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

51. T. Hune, M. Nielsen. Timed bisimulation and open maps. // Lecture Notes in Computer Science, 1998. Vol. 1450. - p. 378-387.

52. T. Hune, M. Nielsen. Timed bisimulation and open maps. // Technical Report RS-98-4, BRICS, 1998.

53. B. Jacobs, J. Rutten. A tutorial on (Co)algebras and (Co)induction // EATCS Bulletin, 1997. Vol. 62. - p. 222-259.

54. W. Janssen, M. Poel, Q. Wu, J. Zwiers Layering of real-time distributed processes. // Lecture Notes in Computer Science, 1994. Vol. 863. - p. 393-417.

55. K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Vol. 1: Basic Concepts, 1992. Vol. 2: Analysis Methods, 1994. // EATCS Monographs in Computer Science, Springer.

56. A. Joyal, M. Nielsen, G. Winskel. Bisimulation and open maps. //In Proc. Annual Symposium on Logic in Computer Science, 1993. p. 418-427.

57. A. Joyal, M. Nielsen, G. Winskel. Bisimulation from open maps. // Information and Computation, 1996. Vol. 127(2). - p. 164-185.

58. M. Jurdzinski, M. Nielsen. Hereditory history preserving bisimilarity is undecidable // Lecture Notes in Computer Science, 2000. Vol. 1770. - p. 358-372.

59. J.-P. Katoen. Quantitative and qualitative extensions of event structures // PhD thesis, University of Twente, The Netherlands, 1996.

60. J.-P. Katoen, R. Langerak, D. Latella, E. Brinksma. On specifying real-time systems in a causality-based setting. // Lecture Notes in Computer Science, 1996. Vol. 1135. - p. 385-404.

61. O. Kummer, M.O. Stehr. Petri's axioms of concurrency: A selection of recent results// Lect. Notes Comp. Sci. 1997. - Vol. 1248. - P. 195-214.

62. F. Laroussinie, K.G. Larsen, C. Weise. Prom timed automata to logic and back // Lecture Notes in Computer Science, 1995. Vol. 969. - p. 529—539.

63. J. Lilius. Efficient state space search for time Petri nets //In Proc. MFCS'98 Workshop on Concurrency, August 1998. Brno (Czech Republic), FIMU Report Series, FIMU RS-98-06, 1998. p. 123-130.

64. A. Maggiolo-Schettini, J. Winkowski. Towards an algebra for timed behaviours. // Theoretical Computer Science, 1992. Vol. 103. - p. 335-363.

65. P. Merlin, D. J. Faber. Recoverability of communication protocols. // IEEE Trans, of Communication, 1976. COM-24(9).

66. R. Milner. Calculus of Communicating Systems. // Lecture Notes in Computer Science, 1980. Vol. 92.

67. R. Milner. Communication and Concurrency. // Prentice Hall International Series In Compter Science, C.A.R. Hoare series editor, 1989.

68. R. Milner, D.Sangiorgi. Barbed Bisimulation. //In Automata, Languarges and Programming, 19th International Colloquium Wien, Austria (Proc. ICALP'92), 1992. p. 685-695.

69. N.S. Moskaleva, I.B. Virbitskaite. On the Category of Event Structures with Dense Time // Lectures Notes Computer Science, 2001. Vol. 2138. - p. 287298.

70. N.S. Moskaleva, I.B. Virbitskaite. Observing Time-Sensitive Partial Order Equivalences Categorically //In Proc. Workshop on Concurrency, Specification and Programming, Berlin, 2002. p. 243-254.

71. N.S. Moskaleva, I.B. Virbitskaite. Open Maps and Trace Semantics for Timed Partial Order Models //In Proc. of the Andrei Ershov Fifth International Conference "Perspectives of System Informatics", 2003. p. 160-167.

72. M. Mukund. Hereditary history preserving bisimulation is decidable for trace-labelled systems // Lecture Notes in Computer Science, 2002. Vol. 2255. - p. 289-300.

73. D. Murphy. Time and duration in noninterleaving concurrency. // Fundamenta Informaticae, 1993. Vol. 19 - p. 403-416.

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

75. M. Nielsen, A. Cheng. Observing behaviour categorically. // Lectures Notes Computer Science, 1996. Vol. 1026. - p. 263-278.

76. M. Nielsen, V. Sassone, G. Winskel. Relationships Between Models of Concurrency. // Lectures Notes Computer Science, 1993. Vol. 803. - p. 425-476.

77. M. Nielsen, G. Winskel. Petri Nets and Bisimulation. // Technical Report RS-95-4, BRICS, 1995.

78. M. Nielsen, G. Winskel. Petri nets and bisimulation. // Theoretical Computer Science, 1996. Vol. 153.

79. D. Park. Concurrency and automata on infinite sequences.// Lectures Notes Computer Science, 1981. Vol. 154. - p. 561-572.

80. V.R. Pratt. Modeling concurrency with partial orders // Int. Journal of Parallel Programming, 1986. Vol. 15(1). - p. 33-71.

81. A. Rabinovitch, B. Tranktenbrot. Behaviour structures and nets // Fundamenta Informaticae, 1988. Vol. 11, №4. - p. 357-404.

82. C. Ramchandani. Analysis of asynchronous concurrent systems by timed Petri nets. // Cambridge, Mass.: MIT, Dept. Electronical Engineering, PhD Thesis, 1974.

83. B. Steffen, C. Weise. Deciding testing equivalence for real-time processes with dense time. // Lecture Notes in Computer Science, 1993. Vol. 711 - p. 703713.

84. Virbitskaite I. B., Gribovskaya N. S. Open Maps and Testing Equivalences for Timed Partial Order Models //In Proc. Workshop on Concurrency, Specification and Programming, Poland, 2003. p. 195-206.

85. I.B. Virbitskaite, N.S. Gribovskaya. Open Maps and Trace Semantics for Timed Partial Order Models // Lecture Notes in Computer Science, 2003. Vol. 2890. - p. 248-259.

86. I.B. Virbitskaite, N.S. Gribovskaya. Open Maps and Observational Equivalences for Timed Partial Order Models // Fundamenta Informaticae, 2004. Vol. 61. -p. 383-399.

87. I.B. Virbitskaite. An observation semantics for timed event structures // Lecture Notes in Computer Science, 2001. Vol. 2244. - p. 215—225.

88. I.B. Virbitskaite. Observing some properties of event structures// Lect. Notes Comp. Sei 1993. - Vol. 735. - P. 259-270.

89. I.B. Virbitskaite. Some Characteristics of Nondeterministic Processes// Parallel Processing Letters. 1993. - Vol. 3. - P. 99-106.

90. W. Vogler. Bisimulation and action refinement // Lecture Notes in Computer Science, 1991. Vol. 480. - p. 309-321.

91. C. Weise, D. Lenzkes. Efficient scaling-invariant checking of timed bisimulation. // Lecture Notes in Computer Science, 1997. Vol. 1200 - p. 176-188.

92. J. Winkowski. Event structure representation of the behaviour of place/transition systems// Fundamenta Informaticae. 1988. - Vol. 11. - P. 405-432.

93. J. Winkowski. An Algebra of Time-Consuming Computetions// Proc. of the Workshop "Concurrency: Specification and Programming", Nieborow, Poland, October 1993. 1993. - P. 258-273.

94. G. Winskel. Event Structures // Lecture Notes in Computer Science, 1987. -Vol. 255.

95. G. Winskel. An introduction to event structures // Lecture Notes in Computer Science, 1989. Vol. 354 - p. 364-397.

96. G. Winskel, M. Neilsen. Models for concurrency, // Handbook of Logic in Computer Science, 1995. Vol. 4.

97. T. Yoneda, A. Shibayama, B. H. Schligloff, E. M. Clarke. Efficient verification of parallel real-time systems. // Lecture Notes in Computer Science, 1993. Vol. 697. - p. 321-333.

98. W.M. Zuberek. Timed Petri Nets and Preliminary Performance Evaluation // Proc. 7th Annual Symposium on Comp. Architecture. 1980. - P. 88-96.