Теоретико-категорное исследование эквивалентностей параллельных моделей с реальным временем
На правах рукописи
Грибовская Наталия Сергеевна Теоретико-категорное исследование эквивалентностей параллельных моделей с реальным временем 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 2.8-353, руководитель д.ф.-м.н. И.Б. Вирбицкайте, 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 и доказывается ряд полезных свойств этой категории. Далее выделяется подкатегория p T S L категории CT ES p, содержащая все временные pom-множества и тождественные морфизмы и морфизмы с пустой областью определения между ними. По данной подкатегории стандартным способом p определяется понятие T P L -открытого морфизма и доказывается его критерий в терминах сохранения выполняемых pom-множеств.
p Затем формулируется понятие абстрактной T P L -бисимуляции в p терминах существования симметричной конструкции T P L -открытых морфизмов. Доказывается следующая p Теорема 2.8. Две ВСС являются T P L -бисимуляционно эквива лентными они временн частично-упорядоченно эквивалентны по о Пратту.
Далее рассматривается проблема распознавания частично-упорядочен ной эквивалентности Пратта в контексте класса конечных ВСС, T ES N.
При помощи техники регионов Алура доказывается разрешимость p T P L -открытости морфизма. Сложность этого распознавания оценивается как N · 22N · (c + 1)N, где N = |E1 | |E2 | (|E1 | и |E2 | — число событий ВСС), а c — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса T ES N доказывается, что из существования симметричной конструкции p T P L -открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T ES N. На основе этого факта и p разрешимости T P L -открытости морфизмов формулируется Следствие 2.5. Для ВСС из T SN времення частично-упорядоченная а эквивалентность Пратта разрешима.
В разделе 2.3 вводится и исследуется частично-упорядочен ная трассовая эквивалентность на ВСС. Такая эквивалентность определяется в терминах равенства временных частично упорядоченных языков, содержащих все все временные pom-множества, выполняемые ВСС. Такая эквивалентность сильнее временной частично-упорядоченной эквивалентности Пратта в том смысле, что любые временн частично-упорядоченно трассово эквивалентные ВСС о являются также временно частично-упорядоченно эквивалентными по Пратту. Строится категория ВСС, CT ES s, и приводится ряд полезных свойств этой категории. Далее в построенной категории выделяется подкатегория T P s, содержащая все временные pom L множества и тождественные морфизмы и морфизмы с пустой областью определения между ними. По этой подкатегории определяется T P s L открытый морфизм и доказывается его критерий в терминах полного сохранения выполняемых pom-множеств. Затем формулируется понятие абстрактной T P s -бисимуляции в терминах существования L конструкции T P s -открытых морфизмов и доказывается следующая L Теорема 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 -открытых морфизмов L следует существование аналогичной конструкции с вершиной из класса T ES N. На основе этого факта и разрешимости T P s -открытости L морфизмов формулируется Следствие 2.7. Для ВСС из T SN времення частично-упорядоченная а трассовая эквивалентность разрешима.
В третьей главе вводятся и исследуются временные варианты тестовых эквивалентностей для временных параллельных моделей, представленных моделями ВСП и ВСС. Два процесса считаются тестово эквивалентными, если наборы их выполняемых тестов совпадают. В интерливинговой семантике тест состоит из временнго слова и набора о временных действий, а в частичной упорядоченной семантике — из временнго pom-множества и набора временных действий. Считается, о что процесс прошел этот тест, если после любого выполнения данного временнго слова или временного pom-множества может выполнится о какое-нибудь временне действие из вышеупомянутого набора.
о В разделе 3.1 вводится и исследуется времення интерливинговая а тестовая эквивалентность на ВСП. Такая эквивалентность формулируется в терминах равенства набора выполняемых интерливинговых тестов. Определяется категория ВСП CT T S test и доказываются некоторые свойства этой категории. Далее в указанной категории выделяется подкатегория Ptest, содержащая наблюдения (ВСП специального вида) и морфизмы между ними.
По этой подкатегории определяется Ptest -открытый морфизм и доказывается его критерий в терминах сохранения отношения перехода на достижимых множествах и вложения множеств последующих Затем определяется абстрактная Ptest временных действий.
бисимуляция в терминах существования конструкции Ptest -открытых морфизмов и доказывается следующая Теорема 3.3. Две ВСП являются Ptest -бисимуляционно эквивалент ными они временн интерливингово тестово эквивалентны.
о Далее рассматривается проблема распознавания временнй о интерливинговой тестовой эквивалентности на классе конечных дискретных ВСП, T T S disc. При помощи техники регионов Алура N доказывается разрешимость Ptest -открытости для морфизмов выделенного класса. Сложность этого распознавания оценивается |X1 |·|X2 | 2|S1 |·|S2 |·2, где X1 и X2 — множества временных переменных ВСП, а S1 и S2 — множества состояний ВСП. Для ВСП из класса T T S disc N доказывается, что из существования симметричной конструкции Ptest открытых морфизмов следует существование аналогичной конструкции с вершиной из класса T T S disc. На основе этого факта и разрешимости N Ptest -открытости морфизмов доказывается Следствие 3.1. Для ВСП из класса T T S disc времення интерливин а N говая тестовая эквивалентность разрешима.
В разделе 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. При помощи техники регионов N Алура доказывается разрешимость T T L -открытости морфизмов для выделенного класса. Сложность такого распознавания оценивается как 2N, где N = |E1 | |E2 | (|E1 | и |E2 | — число событий ВСС). Для ВСС из класса T T S disc доказывается, что из существования симметричной N конструкции T T L -открытых морфизмов следует существование T T L открытого морфизма из одной ВСС в другую. На основе этого факта и полученной разрешимости доказывается Следствие 3.2. Для ВСС из класса T ES disc времення частично а N упорядоченная тестовая эквивалентность разрешима.
В четвертой главе вводятся и исследуются временные варианты бисимуляционных эквивалентностей: времення интерливинговая а слабая бисимуляция по Милнеру и Сангиорги и времення частично а упорядоченная сильная сохраняющая историю бисимуляция.
Бисимуляционные эквивалентности являются наиболее сильными в том смысле, что в отличии от трассовых и тестовых они учитывают точки недетерминированного выбора.
В разделе 4.1 вводится и исследуется временнй вариант о интерливинговой слабой бисимуляции по Милнеру и Сангиорги на ВСП. Такая бисимуляция отличается от сильной бисимуляции, по крайней мере, по трем аспектам. Во-первых, такая бисимуляция предполагает, что множество действий содержит так называемое невидимое действие, обозначаемое. Во-вторых, в данном случае бисимуляционно подобными должны быть только невидимые переходы, то есть переходы, помеченные невидимым действием. В-третьих, данная бисимуляция требует совпадения лишь факта существования видимых действий. В разделе определяется категория ВСП, CT T S wbis, и доказываются некоторые ее свойства. Далее в данной категории выделяется подкатегория Pwbis, содержащая так называемые -ветви и морфизмы между ними. По этой подкатегории определяется Pwbis -открытый морфизм и доказывается его критерий в терминах сохранения отношения перехода на всех достижимых по невидимому временнму действию состояний и фактов существования видимых о Затем определяется абстрактная Pwbis -бисимуляция в переходов.
терминах существования конструкции Pwbis -открытых морфизмов и доказывается следующая Теорема 4.5. Две ВСС являются Pwbis -бисимуляционно эквива лентными они временн интерливингово слабо бисимуляционно о эквивалентны по Милнеру и Сангиорги.
Далее рассматривается проблема распознавания временнй о интерливинговой слабой бисимуляции по Милнеру и Сангиорги на классе T T S N. При помощи техники регионов Алура доказывается Pwbis -открытости разрешимость для морфизмов указанного класса. Сложность данного распознавания оценивается как |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-множества и морфизмы между L ними. По этой подкатегории определяется T P p -открытый морфизм, L доказывается его критерий в терминах совпадения поведения ВСС и доказывается следующая Теорема 4.10. Две ВСС являются T P p -бисимуляционно эквивалент L ными они временн частично-упорядоченно сильно бисимуляционно о эквивалентны с сохранением истории.
Далее рассматривается проблема распознавания временнй частично о упорядоченной сильной сохраняющей историю бисимуляции на классе T ES N. При помощи техники регионов Алура доказывается разрешимость T P p -открытости для морфизмов указанного класса.
L Сложность этого распознавания оценивается как N · 22N · (c + 1)N, где N = |E1 | |E2 | (|E1 | и |E2 | — число событий ВСС), а c — наибольшее натуральное число, упоминаемое в определении временных функций. Для ВСС из класса T ES N доказывается, что из существования симметричной конструкции T P p -открытых морфизмов L следует существование аналогичной конструкции с вершиной из класса 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 Struc tures 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 Concur rency, 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 Equi valences for Timed Partial Order Models // In Proc. Workshop on Concurrency, Specication and Programming, Poland, 2003. – p.
195–206.
10. I.B. Virbitskaite, N.S. Gribovskaya. Open Maps and Trace Seman tics 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.
ЛИЧНЫЙ ВКЛАД АВТОРА Все включенные в диссертацию результаты, касающиеся вопросов разрешимости эквивалентностей параллельных моделей с реальным временем, получены автором самостоятельно. Теоретико-категорные характеризации эквивалентностей, введенных на интерливинговых моделях, представленных временными системами переходов, также получены самостоятельно. При получении теоретико-катерных характеризаций для эквивалентностей, введенных на истинно параллельных моделях, представленных временными структурами событий, Н.С. Грибовская внесла следующий вклад: получила теоретико-категорную характеризацию временнй о частично упорядоченной трассовой и временнй частично-упорядоченной о тестовой эквивалентностей.
БЛАГОДАРНОСТИ Автор выражает свою признательность своему научному руководителю д.ф.-м.н. Вирбицкайте Ирине Бонавентуровне за помощь и понимание.
Грибовская Наталия Сергеевна Теоретико-категорное исследование эквивалентностей параллельных моделей с реальным временем ———————————————————————————————————————– Подписано в печать 18.11.2004 Объем 1,0 п.л.
Формат бумаги 60 84 1 /16 Тираж 100 экз.
——————————————————————————————————————— ЗАО РИЦ “Прайс-курьер” 630090, г. Новосибирск, пр. Акад. Лаврентьева, 6, тел. (383-2) 34-22-