Теоретико-категорное исследование эквивалентностей параллельных моделей с реальным временем тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Грибовская, Наталия Сергеевна

• Грибовская, Наталия Сергеевна
• кандидат физико-математических наук
• 2004

Оглавление диссертации кандидат физико-математических наук Грибовская, Наталия Сергеевна

Введение

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) Получены результаты, касающиеся проблемы разрешимости исследуемых эквивалентностей, на различных конечных классах и оценена сложность распознавания.

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

Список литературы диссертационного исследования кандидат физико-математических наук Грибовская, Наталия Сергеевна, 2004 год

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.