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

Российская академия наук ПГр ЛИ

Сибирское отделение Пи 1/Д Институт систем информатики

им. А.П.Ершова , ! АВГ 2003

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

Боженкова Елена Николаевна

АНАЛИЗ СВОЙСТВ ПАРАЛЛЕЛЬНЫХ ПРОЦЕССОВ И ПРОЦЕССОВ

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

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

Автореферат

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

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

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

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

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

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

Евстигнеев В.А.

кандидат физико-математических наук, Соколов В.А.

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

Институт программных систем РАН (г. Переяславль-Залесский)

Защита состоится 26 июня 2000 года в 14 час. 30 мин. на заседании диссертационного совета К0003.93.01 в Институте систем информатики Сибирского отделения РАН по адресу:

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

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

Автореферат разослан мая 2000 г.

Ученый секретарь специализированного совета К0003.93.01 к.ф.-м.н.

М.А.Бульонков

#•/¿2. г 3 4

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

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

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

При исследовании системы обычно используют два подхода. При первом подходе отпрайной точкой является сама система,.-и-ее поведенческие'свойства изучаются в терминах абстрактной модели. Другой подход — изначально рассматривать модель, которая может быть проинтерпретирована как реальный процесс. С целью адейзатного представления реальных параллельных процессов посредством ациклических бесконфликтных сетей-процессов К. Петри ввел 'аксиомы параллельности' (свойства дискретности, плотности, перекрестности, когерентности, непрерывности). Эти свойства позволили лучше понять взаимосвязи между отношениями причинной зависимости' и параллелизма. И в дальнейшем возможности новых формальных моделей исследовались с помощью 'аксиом параллельности'. А именно, свойства дискретности и непрерывности были обобщены и детально изучены А. Вестом, X. Плюннеке, П. Тиагараджаном для частично-упорядоченных множеств и В.Е. Котовым и Л.А. Черкасовой для кл^ссй сетей-процессов с недетерминированным выбором. Первичные структуры .событий, вве-

денные Г. Винскелем, стали одной из центральных моделей параллельных и недетерминированных процессов и фактически обобщают указанные выше модели. Одно из основных приложений структур событий состоит в определении семантики "истинного"параллелизма для алгебраических языков процессов. Было показано, что ряд свойств плотности позволяет строить простые и, элегантные системы алгебраических спецификаций параллельных процессов. Поэтому изучение 'аксиом параллельности' в контексте структур событий — важная задача для исследования. Для класса первичных; структур событий ряд свойств дискретности был сформулирован и изучен в работах Й.Б. Вирбицрайте. Далее Г. Будолем и И. Кастеллани был предложен более общий класс структур событийлокальные структуры событий. И стало важно обобщить 'аксиомы параллельности' для этой модели, чтобы понять взаимосвязи трех, базовых отношений: причинной зависимости, недетерминированного выбора и параллелизма.

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

Тестовые эквивалентности и предпорадки ,ц. контексте первичных структур событий исследовались в работах У. Гольтц и Л. Арето. ,: Для -учета временных аспектов поведения параллельных/распределенных систем традиционные .формальные модели расширяются-введе-

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

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

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

1. Введение и изучение:'аксиом параллельности' (свойств дискретности и непрерывности) в контексте локальных структур событий, которые являются обобщением первичных структур событий за счет снятия некоторых структурных ограничений.

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

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

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

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

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

• Введен и исследован ряд новых вариантов 'аксиом параллельности' в контексте локальных структур событий. Установлена иерархия взаимосвязей, а также критерии выполнимости различных свойств дискретности и непрерывности.

• Введен и исследован ряд эквивалентностных понятий параллельных моделей реального времени: временные тестовые эквивалентности и предпорядки в контексте структур событий как с дискретными, так и с непрерывными временными характеристиками.

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

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

Практическая ценность данных исследований состоит в возможности их использования при создании автоматизированных систем верификации систем реального времени. В частности, результаты диссертационной работы использовались при создании модуля верификации в ' системе PEP (Programming Environment based on Petri nets), совместно разрабатываемой Институтом информатики Университета г. Хиль-десхайма (Германия) и лабораторией теоретического программирования ИСИ СО РАН-

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

1. International Conference CONPAR 94 - VAPP VI, Linz, Austria, September 1994,

2. Workshop Concurrency, Specification and Programming (CS&P'94), Berlin, October 1994.

3. Distributed data processing (DDP'98), Novosibirsk, Russia, June 1998.

4. 1st International conference on practical and theoretical programming (UkrProg'98), Kiev," Ukraine. September 1998.

5. Workshop Concurrency, Specification and Programming (CS&P'99), Warsaw, Poland, September 1999.

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

Публикации. По теме диссертации опубликовано 11 научных работ.

Структура и объем работы. Диссертация состоит из введения; четырех глав, заключения, списка литературы из 79 наименований и списка публикаций по теме диссертации из 11 наименований. Содержание составляет 108 страниц. Работа включает 21 утверждение, 8 теорем и 32 рисунка.

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

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

Первая глава является обзорной, в ней определяются базовые понятия и приводятся основные результаты теории первичных структур событий. В разделе 1.1 дается определение помеченной над алфавитом Act первичной структуры событий S = {Е,<,#,1), где Е — счетное множество событий, на котором определены непересекающиеся отношения: причинной зависимости <С (Е х Е) (частичный порядок, удовлетворяющий аксиоме конечности причин) и конфликта # С (Е х Е) (иррефлексивное и симметричное отношение, наследуемое по

причинной зависимости), и I : Е Act — функция пометки. Два события параллельны если они не связаны ни отношением причинной зависимости, ни отношением конфликта. Дополнительно определяются отношения непосредственной причинной зависимости (нетранзитивного подмножества отношения <) и минимального (не наследованного по отношению <) конфликта. Подмножества событий, соответствующие состояниям в первичной структуре событий, называются конфигурациями. Конфигурация — это бесконфликтное (нет конфликтующих событий) и левозамкнутое (событие включается в конфигурацию вместе с предшествующими ему событиями) множество событий.

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

В разделе 1.3 с целью выделения класса первичных структур событий, адекватно моделирующих процессы, протекающие в реальных системах, рассматриваются свойства К-, L- и ii-плотности, а также N-и М-плотности, определяются необходимые и достаточные условия выполнения этих свойств и устанавливается иерархия их взаимосвязей.

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

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

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

Локальная структура событий S = (Е, <, #) характеризуется множеством событий Е, непересекающимися отношениями причинной зависимости ,<С {Е х Е) (частичный порядок) и конфликта # С (Е х Е) (иррефлексивнре и симметричное отношение). Два события параллельны (v), если они не связаны ни отношением причинной зависимости, ци

отношением конфликта. Для этих базовых отношений (связок) V Е {<.

вводятся симметричное замыкание (У); рефлексивное и симметричное замыкание (Vе)', иррефлексивное и нетранзйт'ивное отношение (V5), являющееся 'непосредственным' отношением V; иррефлексивное и симметричное отношение (XV), являющееся дополнением к V. Множество, в котором все события находятся в отношении V", называется V-множеством. Максимальное по отношению множественного включения У-множество будем называть V-сечением. Локальную структуру событий назовем V-конечной, если любое У-сечение в ней конечно. Далее ограничимся рассмотрением локальных структур событий, в которых между любой пары событий е,е' нет бесконечного <множества.

Локальная структура событий 5' = (Е', <',#') будет подструктурой в 5, если ее компоненты являются подмножествами соответствующих компонент 5. Подструктура называется максимальной, если она максимальна по отношению множественного включения. Будем называть 5' УЕ-подструктурой в Я, если она является подструктурой в 5 и никакие события из 5' не находятся в отношении У.

В разделе 2.2 вводится ряд унифицированных понятий плотности и перекрестности, а именно Л"у-плотность, У-перекрестность, ./Уу-плотность и Му-плотность. С этой целью для множества АСЕ дополнительно определяется 4- -<4 — множество событий 'меньших или равных', чем события из А в смысле отношения < (множество предшественников А), и А — множество событий 'больших или равных', чем события из А (множество потомков А). Пусть далее V, У1 и VI — непересекающиеся связки. Локальная структура событий называется Куплетной, если в каждой ее максимальной У/^-подструктуре каждое У\-сечение пересекается с каждым Т^-сечением ровно по одному элементу. Локальная структура событий называется V-перекрестной, если в каждой ее максимальной У/^-подструктуре пересечение любого У-сечения со множествами предшественников и потомков любого ^-сечения не пусто. Понятие Му-плотности рассматривает связь подструктур структуры событий. Локальная структура событий будет Му-плотной, если каждая ее максимальная У /^-подструктура пересекается с каждой ее максимальной Уг^-под структурой пересекаются по У-сечению. В следующих утверждениях определяются необходимые и достаточные условия для выполнения введенных свойств, устанавливаются их взаимосвязи.

Утверждение 2.1 Пусть 5 — ТУу-плотная локальная структура.

Тогда 5 — /Су-плотная -о 5 — ^-перекрестная.

Утверждение 2.2 Пусть 5 — Иу-плотная локальная структура событий Тогда 5 — .Ку-плотная, если 5 — -конечная или Уо-коиечная.

Будем говорить, что локальная структура событий 5 удовлетворяет свойству у-свободы, если в ней нет событий 61,62,03 таких, что е^ V ег, е2 V! е3, и е\ У2 е3.

Утверждение 2.3 Пусть 5 — усв°бодная локальная структура Если 5 — Ух-конечная или Ъ^-конечная, то

5 — Ау-плотная 5 — Му-плотная.

В разделе 2.3 рассматриваются другие 'аксиомы параллельности', в частности свойство ^-непрерывности и V-конусного пересечения.

Аксиома ^-непрерывности является обобщением аксиомы Дедекин-да множества действительных чисел на частично упорядоченные модели. В данном пункте понятие ^-непрерывности обобщается на класс локальных структур событий, которые позволяют дать унифицированное его определение. О-сечение — это пара непересекающихся непустых подмножеств (А, А), на которые разбивается множество событий таким образом, что А предшествует А в смысле причинной зависимости. Выделяется специальное множествЬ с(Л), состоящее из максимальных элементов множества А и минимальных элементов А. Локальная структура событий называется И у -непрерывной, если в каждой ее максимальной ^^-подструктуре для каждого £>-сечения (Л, А) верно, что с(Л) пересекается с любым <-сёченйеК1 ровно по одному событию. Для характе-ризации £)у-непрерывности вводятся следующие понятия. Локальная структура событий — строго Су-ограниченная, если в каждой се максимальной V^-подструктуре каждое событие любого Д-сечения (Л, Л) находится в отношении причинной зависимости с некоторым событием из с(Л). Локальная структура обладает Бу-свойством, если в каждой ее максимальной У/^-подструктуре для любой пары событий, находящихся в отношении непосредственной причинной зависимости, существует событие, связанное отношением причинной зависимости только с одним событием из данной пары.

Утверждение 2.5 5— Ду-непрерывная 5 — Л'у-плотная,

строго Су-ограниченная и имеет 5у-свойство.

Далее свойство строгой Су-ограниченности сводится к двум менее строгим понятиям Су-ограниченности и ^у-свойству. Локальная структура событий — С'у-ограниченная, если в каждой ее максимальной ,УР-

подструктуре любое событие каждого -О-ссчения (А, А) находится в отношении причинной зависимости с объединением множеств максимальных элементов А и минимальных элементов А. Ру-свойство отражает ограничение на разветвленность структуры событий. Локальная структура событий удовлетворяет Ру-свойству, если в каждой ее максимальной V/""-подструктуре для каждой пары событий е <' е' выполняется следующее: если одно из данных событий входит во все <'-сечения данной подструктуры, то существует событие, для которого данное событие является единственным предшественником (в случае е) или единственным потомком (в случае е'). Локальная структура событий является у -редуцируемой, если в каждой ее максимальной УР-подструктуре для различных событий множества событий, связанных с данными событиями отношением V, не совпадают. Для ¿^/-свойства найдена взаимосвязь со свойством <у-редуцируемости.

Следующая рассматриваемая 'аксиома параллельности' — свойство V-конусного пересечения. Локальная структура событий удовлетворяет свойству V-конусного пересечения, если в каждой ее максимальной VР-подструктуре любая пара событий е и е' имеет общий элемент как среди предшественников (т.е. 4- е п ^ е' ф 0), так и среди потомков (т.е. | е п "(" е' ф 0). Устанавливается взаимосвязь свойств /^-плотности и У-конусного пересечения со свойством Су-ограниченности. При этом оказалось еще необходимым свойство V-бесконечности (в каждой максимальной VР-подструктуре любое событие должно иметь хотя бы одного предшественника и потомка).

Утверждение 2.8

(а) Если 5 — У-бесконечная и Су-ограниченная, то 5 имеет свойство У-конусного пересечения.

(б) Если Б — Ку-плотная и имеет свойство У-конусного пересечения, то 5 — Су-ограниченная.

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

В разделе 3.1 определяются понятия, связанные с дискретно-временными структурами событий.

В качестве базовой модели вводится дискретно-временная структура событий ИБ = (в = (Е, <, I), И), являющаяся помеченной над Ac.tr первичной структурой событий, где функция П приписывает каждому событию некоторый непустой интервал множества натуральных

чисел, и алфавит AclT состоит из множества видимых действий Act и невидимого действия т. Состпояпиш DS назовем пару М — (С, 6), состоящую из конфигурации С и функции времени <5, которая сопоставляет событиям количество единиц времени, прошедших с момента, когда событие стало готовым к выполнению, то есть с момента, когда все события, ему предшествующие, уже вошли в данную конфигурацию. Вычисление в DS представляется последовательностью переходов из состояния в состояние. Переход из одного состояния в другое осуществляется либо посредством выполнения события, либо посредством истечения некоторого количества единиц времени. Последовательность выполняемых событий и проходящих единиц времени составляют слово в DS. Множество слов образует язык L(DS) дискретно-временной структуры событий DS. Также важно понятие Асс-множества, обозначаемого Acc(DS, (w,d)), которое состоит из множеств действий, которые могут выполниться, и единиц времени, которые могут пройти в состояниях DS, полученных посредством выполнения слова (w,d).

В разделе 3.2 определяется и исследуется ряд понятий временных тестовых предпорядков и эквивалентностей в контексте рассматриваемой модели.

Дискретно-временную структуру событий, некоторые из событий которой могут помечаться специальным символом успешного завершения и> $ Actf, назовем тестом. Совместным вычислением произвольной DS и, произвольного теста назовем максимальную последовательность пар, которые составляются из состояний DS и теста и связываются выполнением события или истечением единиц времени в каждом из состояний пары. Будем говорить, что совместное вычисление DS и теста — успешно, если одно из событий, помеченных w, в тесте может выполниться при этом вычислении. DS всегда проходит тест, если любое их совместное вычисление успешно. DS иногда проходит тест, если хоть одно их совместное вычисление с тестом успешно. Дискретно-временные структуры событий DS и DS' эквивалентны в смысле тестовой семантики при совпадении множеств тестов, которые они всегда (DS —must DS') или иногда (DS —тау DS') проходят.

Для облегчения применения тестовых эквивалентностей найдены их альтернативные характеризации. Оказалось, что шоу-предпорядок связан с включением языков, а miisi-иредпорядок с особым включением но отношению С С на Лсс-множествах. Будем писать, что Acc(DS,(w,d)) ССAcc{DS',(w,d)\ если для любого множества S' из Acc(DS'i(w,d))

существует множество из Acc(DS, (w,d)), которое является подмножеством S'.

Утверждение 3.1

а) DS <тау DS' L(DS) С L(DS'),

б) DS<must DS' <=> V(w, d) . Acc(DS,(w,d)) CC Acc(DS', (w,d)).

В разделе 3.3 вводятся понятия бисимуляций и нребисимуляций, а также дается их характеризация.

Сначала вводится понятие графа классов, являющегося абстрактным представлением вычислений в дискретно-временной структуре событий. Граф классов G(DS) (Vos, Eus, Ids) для дискретно-временной структуры событий DS строится путем объединения состояний, связанных выполнением события, помеченного специальным невидимым действием г, в один класс и склеивания одинаково помеченных дуг, выходящих из одного класса. Каждому классу приписывается информационное поле, являющееся минимальным по отношению множественного включения множеством подмножеств действий, которые могут выполниться, и единиц времени, котрые могут пройти в состояниях, входящих в данный класс.

П-бисимуляция (~п) между графами классов G(DS) и G(DS') (П С Vos х Vos1) ~ это отношение fi С Vps х Vos' такое, что ¡3 С П, (Qds,Qds') £ /?> гДе Qds и Qds' ~ начальные вершины соответствующих графов классов, и для всех (Q,Q') € /? и z £ Act U {1} выполняется: 1) если Q 4 Qi, то найдется такой класс Q\ в Vos», что Q' A Q\ и {Qi, Q'y) 6 fi, 2) то же самое относительно Q'. Понятие (П, tpz, ф~)-пребисимуляции между G{DS) и G(DS') аналогично понятию

П-бисимуляции, только условие 1) проверяется, если Q' 6 фг, и условие 2) проверяется, если Q 6,^1 где tpz и ф, — некоторые предикаты на множестве классов. Заметим, что обычно отношение П отражает сравнимость информационных полей классов. Найдены характеризации, показывающие, что для любых П Ç Vos х Vos' и ф2, ф, € {0, V¡js U Vos'} верно, что G(DS) и G(DS') являются (П,?/;2,^2)-пребисимулятивными (П-бисимулятивными), если и только если множество ¡3(DS, DS'), образованное парами вершин, которые достижимы посредством одинаковых путей в G(DS) и G{DS'), соответственно, является (П, фг)-иребисимуляцией (П-бисимуляцией, соответственно).

Раздел 3.4 посвящен решению проблемы распознавания временных тестовых эквивалентностсй и предпорядков. Устанавливаются вза-

имосвязи между временными тестовыми эквивалентностями (предпо-рядками) для дискретно-временных структур событий и отношениями бисимуляции (нребисимуляции) для соответствующих графов классов. В следующей теореме U — декартово произведение объединения множеств классов G(DS) и G(DS'), а Щ состоит из пар классов, у которых информационные поля взаимно включаются в смысле отношения СС, упоминаемом при введении альтернативной характеризации must-предпорядка между дискретно-временными структурами событий.

Теорема 3.2

(а) DS ~тау DS' ^ G(DS) G{DS').

(б) DS 2та,, DS' G(DS) ~п, G(DS').

(в) DS ~test DS' -w G(DS) ~ni G(DS').

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

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

В разделе 4.1 вводится понятие непрерывно-временной структуры событий. Непрерывно^-временная структура событий TS=(S=(E, <,

I), D) является помеченной над ActT первичной структурой, где функция D приписывает каждому событию некоторый интервал с целочисленными границами из множества действительных чисел. Понятия состояния TS, перехода из состояния в состояние, а также языка L(TS) и Лсс-множества определяются аналогично соответствующим понятиям главы 3, но с учетом непрерывности временных интервалов.

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

Для облегчения применения тестовых эквивалентностей найдены их альтернативные характеризации. May-предпорядок связан с включением языков, а musi-предпорядок — с включением по отношению С С Лес-множеств. Требования на включение по отношению С С отличаются от аналогичных для случая дискретно-временных структур событий, а именно, если непрерывно-временная структура событий TS' больше TS в смысле must, то для любого слова (и), d) для любого множества S'

из Acc(TS',(w,d)) существует множество S из Acc(TS, (w,d)), сужение которого на множество видимых действий Act является подмножеством S', и если S включает некоторый непустой временной интервал, то и S' также включает какой-то непустой временной интервал.

В разделе 4.3 вводятся понятия символьных бисимуляций и пре-бисимуляций. Но сначала для синхронизации вычислений TS и TS' определяется понятие расширенного состояния М\М', которое является элементом декартового произведения множеств состояний TS и TS'. Тогда совместное вычисление двух произвольных TS' и TS' — это последовательность переходов из одного расширенного состояния в другое расширенноё состояние посредством либо выполнения действия, либо истечения некоторого времени в каждой составляющей расширенного состояния. Так как множество расширенных состояний TS и TS' в силу непрерывности ряда действительных чисел является бесконечным, то для того чтобы получить дискретное представление совместных вычислений TS и TS', используется понятие региона Алюра" Идея региона состоит; в объединении расширенных состояний с одинаковыми конфигурациями, а также с одинаковыми целыми частями и одинаковым порядком дробных частей соответствующих значений Временных функций.' 1

■Далее строим граф регионов RG(TS,TS') = (Vrg, Erg ', Iво) Для TS и TS'. Из графа регионов путем объединения регионов, соединенных дугой, помеченной специальным невидимым действием г, в один класс и склеивания одинаково помеченных дуг, выходящих из одного класса, строим граф классов CG(TS,TS') = (Vcg,EcgJcg) для TS и TS'. На полученном'графе классов вводятся понятия символьных П-бисимуляции и (П-,ф2,фг)-пребисимуляции между TS и TS', которые являются аналогом понятий П-бисимуляции и (П, ipz, <^г)-пребисимуля-ции. Найдены характеризации этих бисимуляционных отношений.

Утверждение 4.2 Для любых П С Vcg и гр~,фг Е {0, Vea}

(а) TS TS' <=$■ Vcg ~ символьная (П,т/>2,<^г)-пребисимуля-ция между TS и TS',

(б) TS TS' <=> Vcg — символьная П-бисимуляция между TS и TS'.

Далее.также дводится понятие достижимости расширенного состояние посредством данного слова и доказывается корректность этого определения.

Bp аз деле 4.4 вводится и исследуется подкласс непрерывно-времен-

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

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

Для класса непрерывно-временных структур событий, удовлетворяющих свойствам детерминированности и г-дискретности, Т>£а-т, показываем, что существование символьной пребисимуляции (бисимуляции) между TS и TS' является необходимым и достаточным условием для существования тестового предпорядка (эквивалентности) между TS и TS'. Используемое в следующей теореме отношение Щ состоит из вершин графа классов таких, что для регионов, входящих в данный класс выполняется следующее: множество подмножеств действий; помечающих дуги в графе регионов, полученные Йри сужении множества Vrg на TS, включается в аналогичное,множество, полученное при сужении множества Vrg на TS'. Включение рассматривается в смысле отношения СС, упоминаемом при введении альтернативной хйрактеризации ínusí-предпорядка между непрерывнО-временцыми структурами событий.

Теорема 4.1 TS,TS' € V£d_T, CG{TS,TS') = (VCG, ECG,Icg) и У — Vcg- Тогда ■

(а) TS <may TS1 TS TS'.....

(б) TS <must TS' <=> TS>.

(в) TS <iesi TS' TS Çn'2V TS'.

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

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

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

1. - Даны унифицированные определения и введен ряд новых вариантов 'аксиом параллельности' в контексте локальных структур событий.

- Установлена иерархия взаимосвязей 'аксиом параллельности' (свойств Х-плотности, пёрекрестности, ^-непрерывности, конусного пересечения):1

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

2. - Введена модель структур событий с дискретным временем — дискретно-временные структуры событий (ДВСС).

- В контексте ДВСС пр.?цложены понятия временных тестовых - эквивалентностей и предпорядков, а также варианты бисимуля-

ционных эквивалентностей и предпорядков. Даны характеризации введенных эквивалентностей и предпорядков.

- Установлено совпадение соответствующих вариантов временных тестовых и бисимуляциоЦных отношений для ДВСС.

- Решена проблема распознавания временных тестовых предпорядков и эквивалентностей для ДВСС.

3. - Введена модель структур событий с непрерывным временем — непрерывно-временные структуры событий (НВСС).

" ' - В контексте НВСС определены варианты временных тестовых эквивалентностей и предпорядков и даны их альтернативные характеризации.

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. ВОЖЕНКОВА E.H. Эквивалентностные понятия для структур событий с реальным временем// Proceedings of the 1-st Int. Conf. on Programming "UkrPROG'98", Sept. 2-4. - Институт кибернетики им. Глушкова и институт программных систем Национальной Академии Наук Украины, Киев, Украина, 1998. - стр. 106-110.

¡2,гБфКЕНКОВА E.H. Разрешимость тестовой эквивалентности для распределенных систем реального времени// Вторая международная конференция "Tools for Mathematical Modelling", С.- Петербург. - С.-ПетербургскийТос; Техн. Унив.-т, 1999, - стр1' 158-159.

'; 3- БржЕНКОВА E.H. Исследование разрешимости временйой тестовой эквивалентности// Новосибирск, 1999. - (Препр./РАН. Сиб. отд-ние. ИСИ; N. 62).

4. БОЖЕНКОВА E.H. Исследование эквивалентностных отношений

''' для структур событий с дискретным временем// Новосибирск, 2000.

... - (Препр./РАН. Сиб. отд-ние. ИСИ; N. 75).

5. AndreeVa M.V., Bozhenkova E.Ni, Virbitskaite I.B. Analysis

.....of Timed Concurrent Models Based on Testing Equivalence// Proc. of

the Workshop "Concurrency: Specification and Programming", Warsaw, Poland, September 1999. - 1999. - pp. 1-22

6. Andreeva M.V., Bozhenkova E.N., Virbitskaite I.B. Analysis of Timed Concurrent Models,,Biased on Testing Equivalence// Fundamenta ЩощщЦсае. - 2000. -.Vol. 141. ,

7. Viiibitskaite L, Bozhenkova E. Unified characterization of some properties.p£.event' structures// Proc. Intern.,Conf. CONPAR 94 -VAPP VI, Linz, Austria, September 1994, RISC-Lin^Report Series. -1994. - N 94-48. - P. 29-32.

8. Virbitskaite I., Bozhenkova E. Unified characterization of some properties of event structures// Hildesheimer Informatic-Bericht. - Institut fuer Informatik, Universität Hildesheim, Germany, 1994. - N. 22/94

9. Virbitskaite I., Bozhenkova E. Investigating Nondeterministic Processes// Bull. Novosibirsck Computing Center, Series Computer Science. - Computer Center, Novosibirsk, 1994. - N 2. - P. 79-90.

10. Virbitskaite I, Bozhenkova E. Towards Algebraic Specification of Event Structures// Proc. of the Workshop "Concurrency: Specification and Programming", Berlin, October 1994. - 1994.

11. virbitskaite I., bozhenkova E. Event Structures and their Properties// Specification, Verification and Net Models of Concurrent Systems. - IIS, Novosibirsck, 1994. - P. 7-19

Введение

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

1.1 Основные понятия и определения

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

1.3 'Аксиомы параллельности'.

1.4 Эквивалентностные понятия.

2 Локальные структуры событий и 'аксиомы параллельности'

2.1 Основные определения

2.2 Свойства плотности и перекрестности.

2.3 Свойства непрерывности.

3 Дискретно-временные структуры событий и тестовые эквивалентности

3.1 Дискретно-временные структуры событий.

3.2 Временные тестовые эквивалентности и их характеризации

3.3 Бисимуляция, пребисимуляция и их характеризации

3.4 Распознавание временных тестовых эквивалентностей и предпо-рядков.

4 Непрерывно-временные структуры событий и тестовые эквивалентности

4.1 Непрерывно-временные структуры событий.

4.2 Временные тестовые эквивалентности и их характеризации

4.3 Символьные бисимуляция и пребисимуляция и их характеризации

4.4 Распознавание временных тестовых эквивалентностей и предпо-рядков.

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

При изучении формальных моделей был установлен ряд фундаментальных фактов, которые позволили лучше понять природу параллельных вычислений. Для исследования семантических аспектов параллельных программ и процессов было предложено большое количество абстрактных моделей как интерливинго-вых (системы переходов, автоматы, алгебры процессов [36]), так и моделей "истинного" параллелизма (частично-упорядоченные множества [59], языки трасс [45], причинно-следственные структуры [27], структуры событий [52, 77]).

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

При исследовании системы обычно используют два подхода. При первом подходе отправной точкой является сама система, и ее поведенческие свойства изучаются в терминах абстрактной модели. Другой подход — изначально рассматривать модель, которая может быть проинтерпретирована как реальный процесс. Однако, известно, что не всякая синтаксически корректная модель приемлема для представления процессов, протекающих в реальных системах. Для избежания такого несоответствия К. Петри [56, 57] ввел 'аксиомы параллельности' (свойства дискретности, плотности, перекрестно-сти, когерентности и непрерывности) с целью адекватного представления реальных параллельных процессов посредством ациклических бесконфликтных сетей-процессов. И в дальнейшем возможности новых формальных моделей исследовались с помощью 'аксиом параллельности'. В работах А. Беста, X. Плюн-неке, П. Тиагараджана и др. были установлены тесные взаимосвязи между этими свойствами для сетей-процессов [15, 30, 41] и частично-упорядоченных множеств [16, 58]. Обобщая и развивая полученные результаты на исследование взаимосвязей между отношениями причинной зависимости и альтернативы, для класса сетей-процессов с недетерминированным выбором в статьях В.Е. Котова и Л.А. Черкасовой [23, 6] были предложены понятия L- и М-плотности. Первичные структуры событий, введенные Г. Винскелем [52] в 80-х гг., позволяют естественным образом представлять три базовых отношения — причинной зависимости, параллелизма и альтернативы (конфликта) — между событиями параллельных систем и процессов. Они стали одной из центральных моделей параллельных и недетерминированных процессов и фактически обобщают указанные выше модели. Одно из основных приложений структур событий состоит в определении семантики "истинного" параллелизма для алгебраических языков процессов [21, 77, 40]. В работах [20, 64] было показано, что ряд свойств плотности позволяет строить простые и элегантные системы алгебраических спецификаций параллельных процессов. Поэтому изучение 'аксиом параллельности' в контексте структур событий является важной задачей для исследования.

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

Первичная структура событий (prime event structure) рассматривается как множество событий, связанных отношениями причинной зависимости и конфликта. В локальных структурах событий (flow event structures), которые были введены Г. Будолем и И. Кастеллани в [19] как обобщение первичных структур событий, отношение причинной зависимости (частичного порядка) заменяется на локальное отношение "потока" (flow), и отношение конфликта не наследуется между событиями, связанными отношением "потока".

Для класса первичных структур событий в работах И.Б. Вирбицкайте [64, 65] сформулированы и изучены свойства дискретности (/^-плотности, пере-крестности и др.). Для этой модели установлены взаимосвязи между перечисленными выше свойствами, и сформулированы необходимые и достаточные условия, гарантирующие свойства такого типа. В контексте более общего класса структур событий, локальных структур событий, 'аксиомы параллельности' еще не были изучены. И потому обобщение 'аксиом параллельности' и их исследование в контексте локальных структур событий с целью изучения взаимосвязей между тремя базовыми отношениями — причинной зависимости, параллелизма и недетерминированного выбора — интересная и необходимая задача.

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

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

В работах [33, 34, 73] в контексте структур событий были исследованы различные бисимуляции: интерливинговая, шаговая, частичного порядка, сохраняющая историю.

Тестовые эквивалентности и предпорядки для первичных структур событий исследовались в работах Л. Асето [8] и У. Гольтц [35]. В данных работах были введены тестовые эквивалентности в контексте различных семантик (ин-терливинговой, пошаговой, частичного порядка), изучены взаимосвязи между ними на различных подклассах первичных структур событий.

Однако данные эквивалентностные понятия не отображают временных характеристик поведения систем реального времени. А для систем реального времени важны не только модели вычислений, но и модели времени. Для учета временных аспектов поведения параллельных/распределенных систем традиционные формальные модели расширяются введением количественных и качественных временных характеристик. Известны следующие дихотомии при задании временных характеристик: явное [60]/неявное [26], линейное / ветвистое [32], ссылками на временные точки/интервалы, в непрерывной [40, 46, 50]/дискретной [60] временной области. Введение временных характеристик привело к появлению многих специализированных моделей вычислений с известными различиями: синхронные [40]/ асинхронные [7, 49], с глобальным [40] / локальным временем [7, 28, 46, 79], интерливинговые [11, 38, 51, 61]/"истинно" параллельные ([31, 40, 50, 46, 60, 62]).

К настоящему времени известно очень незначительное число временных расширений моделей с семантикой "истинного" параллелизма, к ним можно отнести временные причинно-следственные структуры [28], временные причинные деревья [31], асинхронные системы переходов [7, 49], временные конфигурации [43]. Также Дж.-П. Катоеном и Д. Мерфи были введены временные расширения структур событий, но, как оказалось, эти модели не пригодны для изучения поведенческих эквивалентностей, поэтому интересна задача введения новых моделей структур событий, расширенных различными временными характеристиками.

С введением временных характеристик в формальные модели в литературе были сделаны попытки ввести понятие времени в эквивалентностные отношения. Разрешимость временной бисимуляции для автоматных моделей с непрерывным временем была показана с использованием техники регионов Алю-ром [10] и Черансом [22], а также техники зон Вайзе [74]. Характеризация временной тестовой эквивалентности в контексте алгебры процессов была рассмотрена в [26]. Проблема распознавания временной тестовой эквивалентности для автоматов с непрерывным временем была исследована в работе [63].

Но эти результаты, как оказалось, не переносятся на временные структуры событий. Таким образом, проблема характеризации и разрешимости временной тестовой эквивалентности для структур событий, расширенных временными характеристиками, остается открытой. И поэтому интересно определить и исследовать временные тестовые отношения в контексте моделей структур событий как с дискретными, так и непрерывными временными характеристиками.

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

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

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

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

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

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

• Введен и исследован ряд новых вариантов 'аксиом параллельности' в контексте локальных структур событий. Установлена иерархия взаимосвязей, а также критерии выполнимости различных свойств дискретности и непрерывности.

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

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

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

Практическая ценность данных исследований состоит в возможности их использования при создании автоматизированных систем верификации систем реального времени. В частности, результаты диссертационной работы использовались при создании модуля верификации в системе PEP (Programming Environment based on Petri nets), совместно разрабатываемой Институтом информатики Университета г. Хильдесхайма (Германия) и лабораторией теоретического программирования ИСИ СО РАН.

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

1. Formal methods in design of concurrent/distributed systems. Volkswagen Stiftung (VS), грант 1/70 564, руководители Prof. Dr. elke Best и к.ф.-м.н. И.Б. ВИРБИЦКАЙТЕ, 1995-1997. (Публикации [66, 67].)

2. Разработка и исследование семантических методов и средств спецификации и верификации параллельных систем и процессов. РФФИ, грант 96-01-01655, руководитель к.ф.-м.н. И.Б. ВИРБИЦКАЙТЕ, 1995-1997. (Публикации [66, 67].)

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

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

1. International Conference CONPAR 94 - VAPP VI, Linz, Austria, September 1994,

2. Workshop Concurrency, Specification and Programming (CS&P'94)-, Berlin, October 1994.

3. Distributed data processing (DDP'98'), Novosibirsk, Russia, June 1998.

4. 1st International conference on practical and theoretical programming (Ukr-Prog'98), Kiev, Ukraine. September 1998.

5. Workshop Concurrency, Specification and Programming (CS&P'99), Warsaw, Poland, September 1999.

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

Публикации. По теме диссертации опубликовано 11 научных работ. Из них 5 работ [66, 69, 12, 2, 3] — на международных конференциях, 2 работы [67, 13] — в зарубежных изданиях и 4 работы [68, 70, 4, 5] — в местных изданиях.

Структура работы.

В первой главе напоминаются основные понятия теории структур событий. В разделе 1.1 определяется первичная структура событий и основные связанные с ней понятия. Раздел 1.2 посвящен связи структур событий с частично упорядоченными множествами и О-сетями. Иерархия свойств плотности вводится в разделе 1.3. Понятия бисимуляционных и тестовых эквивалентностей рассматриваются в разделе 1.4.

Во второй главе в контексте локальных структур событий, являющихся расширением первичных структур событий, исследуется ряд 'аксиом параллельности'. Для рассматриваемой модели устанавливаются взаимосвязи между исследуемыми свойствами, и формулируются необходимые и достаточные условия, гарантирующие свойства такого типа. Основные определения, касающиеся локальных структур событий, даны в разделе 2.1. Иерархия свойств плотности и перекрестности изучается в разделе 2.2. В разделе 2.3 определяются другие 'аксиомы параллельности', в частности свойства ^-непрерывности и конусного пересечения, устанавливаются взаимосвязи этих свойств^,.

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

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

Заключение

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

1. - Даны унифицированные определения и введен ряд новых вариантов 'аксиом параллельности' в контексте локальных структур событий.

- Установлена иерархия взаимосвязей 'аксиом параллельности' (свойств /"i-плотности, перекрестности, ^-непрерывности, конусного пересечения).

- Сформулированы необходимые и достаточные условия, гарантирующие свойства А'-плотности и ^-непрерывности.

2. - Введена модель структур событий с дискретным временем — дискретно-временные структуры событий (ДВСС).

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

- Установлено совпадение соответствующих вариантов временных тестовых и бисимуляционных отношений для ДВСС.

- Решена проблема распознавания временных тестовых предпорядков и эквивалентностей для ДВСС.

3. - Введена модель структур событий с непрерывным временем — непрерывно-временные структуры событий (НВСС).

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

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

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

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

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

2. КОТОВ В.Е. Сети Петри// М: Наука. 1984.7. aceto L., Murphi D. Timing and causality in process algebra// Acta Informática. 1996. - Vol. 33(4). - P. 317-350.

3. Aceto L., De Nicola R., Fantechi A. Testing equivalences for event struc-tures// Lect. Notes Сотр. Sci. 1987. - Vol. 280. - P. 1-20.9. alur R., courcoubetis C., Dill D. Model checking in dense real time// Inform, and Comput. 1993. - Vol. 104. - P. 2-34.

4. Alur R., Courcoubetis C., Henzinger T.A. The observational power of clocks// Led. Notes Com]). Sci. 1994. - Vol. 836. - P. 162-177.

5. Best E., Fernandez Q., PlÜNNECKE H. Concurrent systems and processes// Final Report on the Foundational Part of the Project BEGRUND, FMP-Studien. GMD, Sankt Augustin, FDR, 1985. - N 107.

6. Boudol G., castellani I. Three equivalent semantics for CCS// Led. Notes Comp. Sci 1990. - Vol, 469. - P. 96-141.ceràns K. Decidability of bisimulation equivalences for parallel timer processes// Led. Notes Comp. Sci. 1993. - Vol. 663. - P. 302-315.

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

8. De Nicola R., hennessy M. Testing equivalence for processes// Theoretical Comput. Sci. 1984. - Vol. 34. - P. 83-133.

9. Fernandez C., ThiagaRAJAN P.S. D-continuous causal nets: A model of non-sequential processes// Theoretical Comput. Sci. 1984. - Vol. 284. - P. 171-196.

10. Goltz U., WehrHEIM H. Causal testing// Led. Notes Comp. Sri. 1996. -Vol. 1113. - P. 394-406.

11. Hennessy M. Theory of processes// MITPress Cambridge, 1988.

12. HENNESSY M., MiLNER R. Algebraic laws for nondeterminism and concurrency// J. ACM. 1985. - Vol. 32. - P. 137-162.

13. Henzinger T.A., Manna Z., Pnueli A. Timed transition systems// Led. Notes Comp. Sci. 1991. Vol. 600. - P. 226-251.

14. Hoar C. Communicating Sequential Processes// Prentice Hall, 1985.

15. Katoen J.-P., Langerak R., Latella D., Brinksma E. On specifying real-time systems in a causality-based setting// Led. Notes Comp. Sci. 1996. - Vol. 1135. - P. 385-404.

16. KUMMER O., STEHR M.O. Petri's axioms of concurrency: A selection of recent results// Led. Notes Comp. Sci. 1997. - Vol. 1248. - P. 195-214.

17. Lodaya K., thiagarajan P.S., A modal logic for a subclass of event structures// Led. Notes Comp. Sci. 1987. - Vol. 267. - P. 290-303.

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

19. MURPHY D. Timed process algebra, Petri nets, and event refinement// Proc. 4th Refinement Workshop, Workshops in Computing. 1991. - P. 456-478.

20. MURPHY D. Time and duration in noninterleaving concurrency// Fundamenta Informaticae. 1993. - Vol. 19. - P. 403-416.

21. NlCOLIN X., SlFAKlS J. An overview and synthesis on timed process algebras// Lect. Notes Comp. Sci. 1992. - Vol. 600. - P. 526-548.

22. Nielsen M., Plotkin G., Winskel G. Petri nets, event structures and domains// Theoretical Comput. Sci. 1981. - Vol. 1, N. 13. - P. 85-108.

23. Nielsen M., Rozenberg G., Thiagarajan P.S. Behavioural notions for elementary net systems// Distrib. Comput. 1990. - V. 1, N. 4. - P. 45-57.

24. PARK D. Concurrency and automata on infinite sequences// Led. Notes Comp. Sci. 1981. - Vol. 154. - P. 561-572.

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

26. Schneider S., Davies J., Jackson D.M., Reed G.M., Reed J.M., roscoe A.W. Timed CSP: theory and practice// Led. Notes Comp. Sci. 1991. - Vol. 600. - P. 640-675.

27. VlRBITSKAITE I. Observing some properties of event structures// Led. Notes Comp. Sei. 1993. - V. 735. - P. 259-270.

28. VlRBITSKAITE I. Some Characteristics of Nondeterministic Processes// Parallel Processing Letters. 1993. - Vol. 3. - P. 99-106.

29. VlRBITSKAITE I., Bozhenkova E. Unified characterization of some properties of event structures// Proc. Intern. Conf. CONPAR 94 VAPP VI, Linz, Austria, September 1994, RISC-Linz Report Series. - 1994. - N 94-48. - P. 29-32.

30. VlRBITSKAITE I., BOZHENKOVA E. Unified characterization of some properties of event structures// Hildesheimer Informatic-Bericht. Institut fuer Informatik, Universität Hildesheim, Germany, 1994. - N. 22/94

31. VlRBITSKAITE I., Bozhenkova E. Investigating Nondeterministic Processes// Bull. Novosibirsck Computing Center. Series Computer Science. Computer Center, Novosibirsk, 1994. - N 2. - P. 79-90.

32. VlRBITSKAITE I., Bozhenkova E. Towards Algebraic Specification of Event Structures// Proc. of the Workshop "Concurrency: Specification and Programming", Berlin, October 1994. 1994.

33. VlRBITSKAITE I., Bozhenkova E. Event Structures and their Properties// Specification, Verification and Net Models of Concurrent Systems. IIS, Novosibirsck, 1994. - P. 7-19

34. VlRBITSKAITE I, VOTINTSEVA A. Notes on logical axiomatization of density concepts// Specification, Verification and Net Models of Concurrent Systems. IIS, Novosibirsk, 1994. P. 18-32.

35. VlRBITSKAITE I., VOTINTSEVA A. Behavioural Characterizations of Partial Order Logics// Led. Notes Comp. Sei. 1997. - V. 1279. - P. 463-474.

36. VOGLER W. Modular Construction and Partial Order Semantics of Petri Nets// Led. Notes Comp. Sei. 1992. - Vol. 625. - 252 p.

37. Weise C., Lenzkes D. Efficient scaling-invariant checking of timed bisimu-lation// Led. Notes Comp. Sei. 1997. - Vol. 1200. - P. 176-188.

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

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

40. WlNSKEL G. Event structures// Led. Notes Сотр. Sci. 1987. - Vol. 255. -P.325-392.

41. WlNSKEL G. An introduction to event structures// Lect. Notes Сотр. Sci. -1989. Vol. 354. - P. 364-397.

42. Список публикаций по теме диссертации

43. БОЖЕНКОВА Е.Н. Исследование разрешимсти временной тестовой эквивалентности// Новосибирск, 2000. (Препр./РАН. Сйб. отд-ние. ИСИ; N. 62).

44. БОЖЕНКОВА Е.Н. Исследование эквивалентностных отношений для структур событий с дискретным временем// Новосибирск, 2000. (Препр./РАН. Сиб. отд-ние. ИСИ; N. 75).

45. Andreeva M.V., Bozhenkova E.N., Virbitskaite I.B. Analysis of Timed Concurrent Models Based on Testing Equivalence// Proc. of the Workshop "Concurrency: Specification and Programming", Warsaw, Poland, September 1999. 1999. - pp. 1-22

46. Andreeva M.V., Bozhenkova E.N., Virbitskaite I.B. Analysis of Timed Concurrent Models Based on Testing Equivalence// Fundamenta Informat-icae. 2000. - Vol. 41. - P. 1-20

47. Virbitskaite I., Bozhenkova E. Unified characterization of some properties of event structures// Proc. Intern. Conf. CONPAR 94 VAPP VI, Linz, Austria, September 1994, RISC-Linz Report Series. - 1994. - N 94-48. - P. 29-32.

48. Virbitskaite I., Bozhenkova E. Unified characterization of some properties of event structures// Hildesheimer Informatic-Bericht. Institut fuer Informatik, Universität Hildesheim, Germany, 1994. - N. 22/94

49. Virbitskaite I., Bozhenkova E. Investigating Nondeterministic Processes// Bull. Novosibirsck Computing Center, Series Computer Science. Computer Center, Novosibirsk, 1994. - N 2. - P. 79-90.