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

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

Теоретико-категорное исследование

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

с реальным временем

05.13.11 — математическое и программное обеспечение

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

Автореферат

диссертации на соискание ученой степени

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

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

Работа выполнена на кафедре вычислительных систем механико-математического факультета Новосибирского государственного университета Научный доктор физико-математических наук руководитель: Вирбицкайте Ирина Бонавентуровна Официальные доктор физико-математических наук оппоненты: Ломазова Ирина Александровна доктор технических наук Бандман Ольга Леонидовна Ведущая Томский организация: политехнический университет

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

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

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

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

Ученый секретарь диссертационного совета K003.032.01 Мурзин Федор Александрович

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Следующие результаты, полученные в данной диссертации, полностью раскрывают научную новизну:

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

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

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

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

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

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

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

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

3. Исследование параллельных процессов реального времени методами теории категорий. Министерство образования, грант A03руководитель д.ф.-м.н. И.Б. Вирбицкайте, 2003–2004.

4. Исследование параллельных процессов реального времени методами теории категорий. Федеральное агентство по образованию, грант A04-3.16-217, руководитель д.ф.-м.н.

И.Б. Вирбицкайте, 2004.

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

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

• International Seminar Concurrency: Specication 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 вводится и исследуется времення интерливинговая трассовая эквивалентность на ВСП. Данная эквивалентность определяется в терминах равенства временных интерливинговых языков систем. Приводится формальное определение и свойства категории ВСП, CT T S, построенной Хунэм и Нильсеном в 1998 году. Выделяется подкатегория Ptr этой категории, содержащая все временные слова и тождественные морфизмы и морфизмы с пустой областью определения между ними. По данной подкатегории стандартным способом определяется понятие Ptr -открытого морфизма и доказывается его критерий в терминах сохранения выполнений временных слов. Затем формулируется понятие абстрактной Ptr бисимуляции в терминах существования симметричной конструкции Ptr -открытых морфизмов. Доказывается следующая Теорема 2.3. Две ВСП являются Ptr -бисимуляционно эквивалентными они временн интерливингово трассово эквивалентны.

Далее рассматривается проблема распознавания временнй интер- о ливинговой трассовой эквивалентности в контексте класса конечных ВСП, T T S N. При помощи техники регионов Алура доказывается разрешимость Ptr -открытости морфизма. Сложность этого распознавания оценивается как |S1 | · |S2 | · |X1 |! · |X2 |! · 2|X1 |+|X2 | · (2c + 2)|X1 |+|X2 |, где X1 и X2 — множества временных переменных ВСП, S1 и S2 — множества состояний ВСП, а c — наибольшее натуральное число, встречающаяся во временных конструкциях.

Для ВСП из класса T T S N доказывается, что из существования симметричной конструкции Ptr -открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T T S N.

На основе этого факта и разрешимости Ptr -открытости морфизмов формулируется Следствие 2.5. Для ВСП из класса T T S N времення интерливингоа вая трассовая эквивалентность разрешима.

В разделе 2.2 вводится и исследуется частично-упорядоченная эквивалентность Пратта на ВСС. Эта эквивалентность определяется в терминах равенства временных частично-упорядоченных языков Пратта, которые содержат все приращения, определяемые относительно частичного порядка, для всех временных pom-множеств, выполняемых ВСС. Определяется категория ВСС CT ES p и доказывается ряд полезных свойств этой категории. Далее выделяется подкатегория T S L категории CT ES p, содержащая все временные pom-множества и тождественные морфизмы и морфизмы с пустой областью определения между ними. По данной подкатегории стандартным способом определяется понятие T P L -открытого морфизма и доказывается его критерий в терминах сохранения выполняемых pom-множеств.

Затем формулируется понятие абстрактной T P L -бисимуляции в терминах существования симметричной конструкции T P L -открытых морфизмов. Доказывается следующая Теорема 2.8. Две ВСС являются T P L -бисимуляционно эквивалентными они временн частично-упорядоченно эквивалентны по Пратту.

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

При помощи техники регионов Алура доказывается разрешимость T P L -открытости морфизма. Сложность этого распознавания оценивается как N · 22N · (c + 1)N, где N = |E1 | |E2 | (|E1 | и |E2 | — число событий ВСС), а c — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса T ES N доказывается, что из существования симметричной конструкции T P L -открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T ES N. На основе этого факта и разрешимости T P L -открытости морфизмов формулируется Следствие 2.5. Для ВСС из T SN времення частично-упорядоченная эквивалентность Пратта разрешима.

В разделе 2.3 вводится и исследуется частично-упорядоченная трассовая эквивалентность на ВСС. Такая эквивалентность определяется в терминах равенства временных выполняемые ВСС. Такая эквивалентность сильнее временной частично-упорядоченной эквивалентности Пратта в том смысле, что любые временн частично-упорядоченно трассово эквивалентные ВСС являются также временно частично-упорядоченно эквивалентными по Пратту. Строится категория ВСС, CT ES s, и приводится ряд полезных свойств этой категории. Далее в построенной категории выделяется подкатегория T P s, содержащая все временные pomL множества и тождественные морфизмы и морфизмы с пустой областью определения между ними. По этой подкатегории определяется T P s L открытый морфизм и доказывается его критерий в терминах полного сохранения выполняемых pom-множеств. Затем формулируется понятие абстрактной T P s -бисимуляции в терминах существования конструкции T P s -открытых морфизмов и доказывается следующая Теорема 2.14. Две ВСС являются T P s -бисимуляционно эквивалентL ными они временн частично-упорядоченно трассово эквивалентны.

Далее рассматривается проблема распознавания частично-упорядоченной трассовой эквивалентности в контексте класса T ES N. При помощи техники регионов Алура доказывается разрешимость T P s - L открытости морфизмов. Сложность этого распознавания оценивается как N · 22N · (c + 1)N, где N = |E1 | |E2 | (|E1 | и |E2 | — число событий ВСС), а c — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса T ES N доказывается, что из существования симметричной конструкции T P s -открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T ES N. На основе этого факта и разрешимости T P s -открытости L морфизмов формулируется Следствие 2.7. Для ВСС из T SN времення частично-упорядоченная трассовая эквивалентность разрешима.

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

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

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

интерливинговой тестовой эквивалентности на классе конечных дискретных ВСП, T T S disc. При помощи техники регионов Алура доказывается разрешимость Ptest -открытости для морфизмов выделенного класса. Сложность этого распознавания оценивается 2|S1 |·|S2 |·2, где X1 и X2 — множества временных переменных ВСП, а S1 и S2 — множества состояний ВСП. Для ВСП из класса T T S disc N доказывается, что из существования симметричной конструкции Ptest открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T T S disc. На основе этого факта и разрешимости Ptest -открытости морфизмов доказывается Следствие 3.1. Для ВСП из класса T T S disc времення интерливина говая тестовая эквивалентность разрешима.

В разделе 3.2 вводится и исследуется времення частично-а упорядоченная тестовая эквивалентность на ВСС. Такая эквивалентность определяется в терминах совпадения набора выполняемых частично-упорядоченных тестов. Определяется категория ВСС CT ES t и доказываются основные свойства этой категории. Далее в этой категории выделяется подкатегория T T L, содержащая ВСС и тождественные морфизмы и морфизмы с пустой областью определения.

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

Затем формулируется понятие абстрактной T T L -бисимуляции в терминах существования конструкции T T L -открытых морфизмов и доказывается следующая Теорема 3.7. Две ВСС являются T T L -бисимуляционно эквивалентными они временн частично-упорядоченно тестово эквивалентны.

Далее рассматривается проблема распознавания временнй частич- о но-упорядоченной тестовой эквивалентности на классе конечных дискретных ВСС, T ES disc. При помощи техники регионов Алура доказывается разрешимость T T L -открытости морфизмов для выделенного класса. Сложность такого распознавания оценивается как 2N, где N = |E1 | |E2 | (|E1 | и |E2 | — число событий ВСС). Для ВСС из класса T T S disc доказывается, что из существования симметричной конструкции T T L -открытых морфизмов следует существование T T L открытого морфизма из одной ВСС в другую. На основе этого факта и полученной разрешимости доказывается Следствие 3.2. Для ВСС из класса T ES disc времення частичноа упорядоченная тестовая эквивалентность разрешима.

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

Бисимуляционные эквивалентности являются наиболее сильными в том смысле, что в отличии от трассовых и тестовых они учитывают точки недетерминированного выбора.

В разделе 4.1 вводится и исследуется временнй вариант интерливинговой слабой бисимуляции по Милнеру и Сангиорги на ВСП. Такая бисимуляция отличается от сильной бисимуляции, по крайней мере, по трем аспектам. Во-первых, такая бисимуляция предполагает, что множество действий содержит так называемое невидимое действие, обозначаемое. Во-вторых, в данном случае бисимуляционно подобными должны быть только невидимые переходы, то есть переходы, помеченные невидимым действием. В-третьих, данная бисимуляция требует совпадения лишь факта существования видимых действий. В разделе определяется категория ВСП, CT T S wbis, и доказываются некоторые ее свойства. Далее в данной категории выделяется подкатегория Pwbis, содержащая так называемые -ветви и морфизмы между ними. По этой подкатегории определяется Pwbis -открытый морфизм и доказывается его критерий в терминах сохранения отношения перехода на всех достижимых по невидимому временнму действию состояний и фактов существования видимых Затем определяется абстрактная Pwbis -бисимуляция в переходов.

терминах существования конструкции Pwbis -открытых морфизмов и доказывается следующая Теорема 4.5. Две ВСС являются Pwbis -бисимуляционно эквивалентными они временн интерливингово слабо бисимуляционно эквивалентны по Милнеру и Сангиорги.

интерливинговой слабой бисимуляции по Милнеру и Сангиорги на классе T T S N. При помощи техники регионов Алура доказывается класса. Сложность данного распознавания оценивается как |S1 | · |S2 | · |X1 |! · |X2 |! · 2|X1 |+|X2 | · (2c + 2)|X1 |+|X2 |, где X1 и X — множества временных переменных ВСП, S1 и S2 — множества состояний ВСП, а c — наибольшее натуральное число, встречающееся во временных конструкциях. Для ВСП из класса T T S N доказывается, что из существования симметричной конструкции Pwbis -открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T T S N. На основе этого факта и полученной разрешимости доказывается следующее Следствие 4.3. Для ВСП из класса T T S N времення интерли- а винговая слабая бисимуляция по Милнеру и Сангиорги разрешима.

В разделе 4.2 вводится и исследуется времення частично-упоряа доченная сильная сохраняющая историю бисимуляция на ВСС. При исследовании этой эквивалентности используется ранее построенная категория CT ES p. В этой категории выделяется подкатегория T P p, содержащая временные pom-множества и морфизмы между ними. По этой подкатегории определяется T P p -открытый морфизм, доказывается его критерий в терминах совпадения поведения ВСС и доказывается следующая Теорема 4.10. Две ВСС являются T P p -бисимуляционно эквивалентL ными они временн частично-упорядоченно сильно бисимуляционно эквивалентны с сохранением истории.

Далее рассматривается проблема распознавания временнй частичноо упорядоченной сильной сохраняющей историю бисимуляции на классе T ES N. При помощи техники регионов Алура доказывается разрешимость T P p -открытости для морфизмов указанного класса.

Сложность этого распознавания оценивается как N · 22N · (c + 1)N, где N = |E1 | |E2 | (|E1 | и |E2 | — число событий ВСС), а c — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса T ES N доказывается, что из существования симметричной конструкции T P p -открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T ES N. На основе этого факта и полученной разрешимости доказывается Следствие 4.5. Для ВСС из T SN времення частично-упорядоченная сильная сохраняющая историю бисимуляция разрешима.

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

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

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, Specication 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, Specication and Programming, Poland, 2003. – p.

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 Informaticae, 2004. – Vol. 61. – p. 383–399.

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

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

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

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

Теоретико-категорное исследование эквивалентностей параллельных моделей с реальным временем ———————————————————————————————————————– Подписано в печать 18.11.2004 Объем 1,0 п.л.

Формат бумаги 60 84 1 /16 Тираж 100 экз.

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