РАЗРАБОТКА И ИССЛЕДОВАНИЕ СЕМАНТИЧЕСКИХ МЕТОДОВ И СРЕДСТВ СПЕЦИФИКАЦИИ И ВЕРИФИКАЦИИ ПАРАЛЛЕЛЬНЫХ СИСТЕМ И ПРОЦЕССОВ
Вирбицкайте И.Б., Боженкова Е.Н., Вотинцева А.В., Покозий Е.А., Тарасюк И.В.
Институт систем информатики СО РАН (ИСИ СО РАН)
630090, г. Новосибирск, ул. Лаврентьева, 6 Тел.: (3832)355652 Факс: 323494
|
В области теории и применения сетевых моделей проведены исследования различных классов структур событий, потоковых схем и сетей Петри. В контексте структур событий введены и изучены фундаментальные аксиомы параллельности (свойства дискретности, плотности, непрерывности и т.д.), позволяющие адекватно представлять поведение реальных параллельных/распределенных систем. Разработаны и исследованы слабые и сильные варианты поведенческих эквивалентностей (бисимуляций), непосредственно отображающих базовые отношения (причинной зависимости, параллелизма и недетерминизма) между событиями в структурах. Построены диаграммы зависимостей между новыми и известными из литературы бисимуляциями. Исследован вопрос сохранения введенных эквивалентностей при выполнении алгебраических операций. На различных классах сетей Петри установлена полная картина взаимосвязей базисных поведенческих (следовых, бисимуляционных, сохраняющих конфликт и т.д.) эквивалентностей в семантиках "интерливинг/истинный параллелизм" и "линейное/ветвистое время". Все рассмотренные эквивалентности исследованы на конгруентность относительно SM-детализации, и дана их логическая характеризация в терминах формул темпоральных языков. Для временных сетей Петри введен и исследован ряд эквивалентностных понятий, способных в разной степени учитывать временные аспекты поведения моделируемых систем. Разработан композициональный подход к проверке эквивалентности систем реального времени. Установлена взаимосвязь эквивалентностей на подклассах временных сетей. Предложен язык алгебраических спецификаций, позволяющий описывать структурированные потоковые схемы с цветными фишкамии. Для данного класса схем построен ряд семантических моделей (последовательностей срабатываний, языков трасс, информационно-логических графов, структур событий). Установлено совпадение между этими моделями с точностью до изоморфизма. Разработано новое алгебраическое исчисление AFLP2 помеченных недетерминированных параллельных процессов - расширение известной алгебры AFP2 (введенной В.Е. Котовым и Л.А. Черкасовой) функцией пометки. Для данного исчисления предложена полная и корректная система аксиом. Выяснены взаимосвязи алгебраических и сетевых эквивалентностей. В рамках логического подхода на структурах событий введен и исследован ряд темпоральных логик, позволяющих учитывать параллелизм и недетерминизм моделируемых процессов. Найдены бисимуляционные эквиваленты для всех рассмотренных логик. Разработаны эффективные алгоритмы верификации поведенческих свойств временных сетей Петри с использованием аппарата темпоральной логики реального времени TCTL. Осуществлена реализация модулей экспериментальной системы PEP (Programming Environment based on Petri nets), поддерживающих спецификацию, верификацию и симуляцию временных сетей Петри, а также проверку на эквивалентность различных классов сетей Петри. Net models investigations are related to different classes of event structures, data flow schemes and Petri nets. Axioms of concurrency (discreteness, density, continuity, etc.), allowing specification of "real life" concurrent processes have been characterized and examined in terms of events structures. We have formulated necessary and sufficient conditions for the above properties to hold. An algebraic system whose terms are interpreted as dense event structures has been developed. A number of strong and weak variants of bisimulations which explicitly reflect all the relations (causality, concurrency, conflict) between event occurrences in the structures have been introduced. Building a lattice of implications, we have shown the close relationships between the introduced and existing bisimulation notions. The question of preservation of the considered equivalences under some algebraic operations has been treated. In the framework of different classes of Petri nets, new variants of trace, bisimulation and conflict preserving equivalences have been proposed and compared, giving rise to a complete set of basic equivalence notions in interleaving/true concurrency and linear/branching time semantics. All the considered equivalence relations have been considered for the resistence with respect to SM-refinements and logically characterized in terms of temporal languages. A family of equivalence notions for real-time systems represented by Petri nets with time delays (timed nets) has been developed. The interrelations of all the equivalence notions are examined for some subclasses of timed nets. Further we define a timed variant of action refinement and investigate how the proposed equivalence notions behave with respect to this class of refinements. We have introduced a new algebraic language for specification of well-behaved data flow schemes. For this class of schemes, a number of behavioural notions (firing sequences, trace languages, dependence graphs and event structures) have been formalized. We have proved the coincidence of the above notions up to an isomorphism. A new algebra of labelled nondeterministic processes, called AFLP2, has been proposed which is an extension of the calculus AFP2 (introduced by V.E. Kotov and L.A. Cherkasova) by labelling function. The sound and complete axiomatization of the algebra has been presented. We have compared algebraic and net equivalences, resulting in a lattice of implications. A number of new temporal logics that explicitly exibit the interplay between concurrency and nondeterminism have been put forward. A bisimulation matches for the equivalences induced by the logics have been established in the context of event structures. In order to specify and verify behavioural properties of time Petri nets, an efficient model checking algorithms of real time temporal logic TCTL have been developed. The experimental system PEP (Programming Environment based on Petri nets) has been extended by facilities suppoting specification, verification and simulation of time Petri nets and eqiuvalence checking of different classes of Petri nets.
|
|
Объявленные ранее цели проекта: Разработать, исследовать и программно реализовать методы и средства описания, анализа и моделирования параллельных/распределенных систем на основе сетевых, алгебраических и логических моделей. Степень выполнения поставленных задач: Все задачи, поставленные в проекте, выполнены полностью. Полученные важнейшие результаты: В области теории и применения сетевых моделей проведены исследования различных классов структур событий, потоковых схем и сетей Петри. В контексте структур событий введены и изучены фундаментальные аксиомы параллельности (свойства дискретности, плотности, непрерывности и т.д.) с целью получения моделей, адекватно представляющих поведение реальных параллельных/распределенных систем. Сформулированы необходимые и достаточные условия, гарантирующие выполнение указанных свойств. Предложено описание плотных структур событий в терминах алгебраического языка. Введены и исследованы слабые и сильные варианты поведенческих эквивалентностей (бисимуляций), непосредственно отображающих базовые отношения (причинной зависимости, параллелизма и недетерминизма) между событиями в структурах. Построены диаграммы зависимостей между введенными и известными из литературы эквивалентностными понятиями. Исследован вопрос сохранения рассмотренных бисимуляций при выполнении алгебраических операций. Установлена полная картина взаимосвязей базисных поведенческих эквивалентностей как на всем классе сетей Петри, так и на их подклассах, в семантиках: "интерливинг/истинный параллелизм" и "линейное/ветвистое время". Для этих целей были введены некоторые новые варианты таких эквивалентностей, как следовых, бисимуляционных, сохраняющих конфликт. Дана логическая характеризация рассмотренных эквивалентностей в терминах формул темпоральных языков типа логики HML (введенной Хеннеси и Милнером). Показано, какие эквивалентностные понятия могут быть использованы при разработке систем по методу "сверху-вниз". Для сетей Петри с временными характеристиками введен и исследован ряд эквивалентностных понятий, способных в разной степени учитывать временные аспекты поведения моделируемых систем. Разработан композиционный подход к проверке эквивалентности систем реального времени. Установлена взаимосвязь эквивалентностей на подклассах временных сетей. Предложен язык алгебраических спецификаций, позволяющий описывать структурированные потоковые (data flow) схемы с цветными фишками. Для данного класса схем построен ряд семантических моделей (последовательностей срабатываний, языков трасс, информационно-логических графов, структур событий). Установлено совпадение между этими моделями с точностью до изоморфизма. Разработано новое алгебраическое исчисление помеченных недетерминированных параллельных процессов $AFLP_2$ - расширение известной алгебры $AFP_2$ (введенной В.Е. Котовым и Л.А. Черкасовой) функцией пометки. Для данного исчисления предложена полная и корректная система аксиом. Выяснены взаимосвязи алгебраических и сетевых эквивалентностей. В рамках логического подхода получены следующие результаты. Введены и исследованы темпоральные логики частичного порядка $L_1^*$ и $L_1^r$, являющиеся рассширениями языка $L_1$ (введенного М.Мукундом и П.Тиагараджяном), интерпретированного на структурах событий. $L_1^*$ получена посредством добавления бинарных операторов "будущего" и "прошлого", а также унарных операторов "непосредственного конфликта", "непосредственного будущего" и "непосредственного прошлого". $L_1^r$ включает дополнительный символ для обозначения максимальной конфигурации структуры событий. Указанные логики сравниваются посредством сопоставления порождаемых ими эквивалентностей с бисимуляционными. С целью увеличения выразительных возмощностей темпоральной логики ветвистого времени $CTL^*$ введен ряд дополнительных операторов, позволяющих представлять параллелизм, конфликт и ветвление "прошлого". Установлены поведенческие эквиваленты для полученных $CTL^*$-расширений. Разработаны и оценены алгоритмы верификации поведения временных сетей Петри модели Мерлина с использованием аппарата известной темпоральной логики реального времени TCTL (расширение известной темпоральной логики CTL за счет введения количественных временных характеристик). Для повышения эффективности разрабатываемых алгоритмов применен метод частичных порядков, позволяющий использовать параллелизм сети для упрощения структуры графа состояний, представляющего поведение временной сети. Осуществлена реализация модулей экспериментальной системы PEP (Programming Environment based on Petri nets), поддерживающих спецификацию, верификацию и симуляцию поведенческих свойств временных сетей Петри, а также проверку на эквивалентность различных классов сетей Петри.
Степень новизны полученных результатов: Все полученные теоретические и экспериментальные результаты являются оригинальными. Рассмотрение аксиом параллельности в контексте структур событий позволило ввести ряд новых вариантов свойств плотности, редуцируемости, когерентности и т.д. и тем самым дать унифицированное формальное определение процессов, протекающих в реальных параллельных системах. Бисимуляционные эквивалентности, в разной степени учитывающие параллелизм и недетерминированный выбор между событиями моделируемых систем, ранее не изучались в литературе. Также впервые введены и исследованы так называемые локальные бисимуляции (эквивалентностные понятия, определенные на локальных конфигурациях структур событий), которые, как оказалось, являются наиболее удобными для распознавания эквивалентных процессов, представленных структурами событий. До сих в пор в литературе не была ясна полная картина взаимосвязей базисных поведенческих эквивалентностей как на всем классе сетей Петри, так и на их подклассах, в семантиках: "интерливинг/истинный параллелизм" и "линейное/ветвистое время". Для этих целей в рамках проекта были введены некоторые новые варианты таких эквивалентностей, как следовых, бисимуляционных, сохраняющих конфликт. Ряд известных из литературы и вновь введенные эквивалентности впервые проверены на сохранение при выполнении операции SM-детализации. И также впервые дана их логическая характеризация в контексте сетей Петри. Поведенческие эквивалентности систем реального времени, представленных временными сетями Петри, на сколько нам известно, не рассматривались в литературе. Тем более было интерсно изучить взаимосвязи между эквивалентностями такого типа и разработать композиционный подход к выявлению систем с эквивалентным временным поведением. Также в литературе не известны аналоги разработанным алгебраическому языку и методу унификации семантических моделей потоковых схем с цветными фишками. Введенное алгебраическое исчисление $AFP_2$ с механизмом синхронизации по именам представляется новым, поскольку позволяет специфицировать процессы с событиями, помеченными одинаковыми действиями, и с семантикой частичного порядка. Впервые установлена взаимосвязь семантической эквивалентности алгебры подобного типа с широким набором базисных поведенческих эквивалентностей сетей Петри. Доказательство совпадения некоторых вариантов бисимуляций с эквивалентностями, предполагаемыми темпоральными логиками, интерпретированными на структурах событий, проведено впервые и заполняет пробел в литературе, посвященной поведенческим и логическим характеризациям структур событий. Алгоритмы верификации поведенческих свойств временных сетей Петри с использованием аппарата темпоральной логики реального времени TCTL являются уникальными, поскольку традиционно для таких целей использовались методы теории расписаний. Предложенные в рамках проекта оригинальные методы спецификации, верификации и анализа на эквивалентность сетевых моделей были реализованы в виде программных модулей экспериментальной системы PEP (Programming Environment based on Petri nets), что также является в определенном смысле уникальным в области программных средств, поддерживающих сетевые модели.
Сопоставление с мировым уровнем: Все полученные теоретические и прикладные результаты соответствуют мировому уровню. Фундаментальные аксиомы параллельности (свойства дискретности, плотности, редуцируемости, когерентности, непрерывности и т.д.) были впервые введены в классических работах К.Петри с целью адекватного представления реальных параллельных процессов посредством ациклических сетей Петри. В последующих работах А.Беста, Х.Плюннеке, П.Тиагаранджяна и др. были установлены тесные взаимосвязи между этими свойствами для частично упорядоченных множеств. Структуры событий, введенные Г.Винскелем в 80-х гг., стали одной из центральных моделей параллельных недетерминированных процессов и фактически включают указанные выше модели. Поэтому изучение аксиом параллельности в контексте структур событий, выполненное в рамках проекта, позволило обобщить данные свойства и дать унифицированное определение процессов, претекающих в реальных параллельных системах. Понятие эквивалентности является важнейшим для любой теории систем. Поведенческие (бисимуляционные) эквивалентности обычно используются при спецификации и верификации с целью сравнения поведения систем, а также упрощения их структуры. Традиционно бисимуляционные эквивалентности на параллельных процессах строятся на основе интерливинговой семантики и поэтому отображают только причинную зависимость и косвенно параллелизм между событиями моделируемых систем. Известно, что одно из достоинств структур событий состоит в том, что они позволяют естественным образом представлять и изучать базовые отношения (причинной зависимости, параллелизма, недетерминизма) на событиях параллельных систем. Введение и изучение вариантов бисимуляционных эквивалентностей, непосредственно представляющих параллелизм и недетерминизм событий, установление взаимосвязей между новыми и известными из литературы эквивалентностями позволили глубже понять природу недетерминированных процессов, представленных структурами событий. В настоящее время для сетей Петри разработано большое разнообразие эквивалентностных понятий. Однако как для всего класса сетей, так и для их подклассов (например, последовательных сетей, Т-сетей и сетей со строгой пометкой) нет достаточно полной картины взаимосвязей эквиалентностей в семантиках "интерливинг/истинный параллелизм" и "линейное/ветвистое время". Все эти пробелы были заполнены результатами, полученными в рамках проекта. При разработке параллельных систем по методу "сверху-вниз" используется важное свойство эквивалентностей - сохранение при преобразовании детализации, в соответствии с которым элементарные компоненты систем приобретают некоторую внутреннюю структуру. Ряд рассмотренных в литературе эквивалентностей был проверен на сохранение при этом преобразовании. В то же время, например, не было известно, являются ли конгруэнтностями относительно операции детализации следовая эквивалентность на частичных словах, а также процессные аналоги обычных, ST-, сохраняющих историю бисимуляционных и следовых эквивалентностей и т.д. В рамках проекта все указанные эквивалентности проверены на сохранение при SM-детализации. Известные из литературы эквивалентности, как правило, не отображают временных характеристик поведения систем, функционирующих в режиме реального времени. Существуют только немногочисленные работы, посвященные исследованию вопросов разрешимости временных эквивалентностей для таких моделей, как временные автоматы. Поэтому было целесообразным в рамках проекта ввести различные варианты временных эквивалентностей в контексте сетей Петри с временными характеристиками, которые представляют собой обобщение временных автоматов, а также разработать композиционный подход к сравнению поведения сетей такого типа. Потоковые (dataflow) схемы являются инструментом спецификации, анализа и моделирования параллельных вычислительных систем и их программного обеспечения. Известные из литературы потоковые модели можно разбить на две группы - статические и динамические. Статические модели допускают не более одной фишки на дуге схемы, тем самым ограничивая степень моделируемого параллелизма. Динамические модели свободны от этого недостатка за счет использования механизмов копирования фрагментов схем и раскрашивания фишек. В литературе исследовались различные подходы к представлению поведения статических потоковых схем в терминах понятий, облегчающих выявление параллелизма. Для динамических моделей этот вопрос, насколько нам известно, практически не был изучен. Поэтому исследования, выполненные в проекте, помогут унифицировать и установить взаимосвязи между различными моделями параллельных процессов в контексте потоковых вычислений. Для описания и анализа конечных недетерминированных параллельных процессов В.Е.Котовым и Л.А.Черкасовой было разработано алгебраическое исчисление $AFP_2$ с семантикой, учитывающей "истинный параллелизм", и удобным механизмом синхронизации. Представление недетерминизма с помощью "не-действий", примененное в данной алгебре, ранее не было описано в литературе. Однако исчисление $AFP_2$ имеет недостаточные описательные возможности. Чтобы разрешить эту проблему, в рамках проекта была предложена алгебра $AFLP_2$, позволяюшая специфицировать процессы с несколькими одинаково помеченными событиями. При совместном рассмотрении сетевых и алгебраических спецификаций важно установить соответствие между эквивалентностями сетей Петри и семантическими эквивалентностями процессных алгебр, чтобы переходить от сетевого представления к формульному и обратно с сохранением требуемых свойств моделируемых систем. В рамках проекта семантическая эквивалентность исчисления $AFLP_2$ была перенесена на сети Петри, а сетевые эквивалентности - на формулы алгебры, установлены взаимосвязи между этими эквивалентностями. Сравнение семантических эквивалентностей алгебр процессов с таким полным набором сетевых эквивалентностей, на сколько нам известно, ранее не проводилось в литературе. Одно из важных свойств эквивалентностей на алгебраических формулах, используемое при разработке параллельных систем по методу "снизу-вверх", - композициональность, то есть сохранение относительно алгебраических операций, что позволяет комбинировать из простых эквивалентных формул более сложные с сохранением эквивалентности. В рамках проекта формульные аналоги сетевых эквивалентностей проверены на композициональность, что также ранее не было сделано для такого ширoкого набора эквивалентностных понятий. Темпоральные логики являются удобным формализмом для спецификации и верификации поведения параллельных/распределенных систем. Из литературы известно большое многообразие темпоральных языков, основные черты которых присущи логике $CTL^*$. В традиционных определениях $CTL^*$-формул используются только операторы "будущего" и (иногда) "прошлого", отражающие причинную зависимость между событиями систем. С целью увеличения выразительной мощности $CTL^*$ целесообразно было ввести дополнительные операторы, позволяющие рассуждать о параллельных и альтернативных поведениях систем. Чтобы лучше понять природу и смысл логических формализмов, используемых для спецификации и верификации поведения параллельных/распределенных систем, в литературе достаточно часто изучался вопрос о сопоставлении эквивалентностей, предполагаемых этими логиками, с поведенческими (как правило, бисимуляционными) эквивалентностями. Однако данная проблема совсем не изучена для темпоральных логик, непосредственно разработанных на структурах событий. Для устранения этого пробела в рамках проекта выразительные мощности известных из литературы языков темпоральной логики для структур событий сравнивались на основе сопоставления логических и бисимуляционных эквивалентностей. Для верификации свойств поведения параллельных систем, функционирующих в режиме реального времени, был предложен ряд языков темпоральной логики, в операторы которых введены явные временные характеристики. Это позволяет осуществлять не только качественный, но и количественный анализ временных свойств моделируемых систем. К таким темпоральным логикам относится язык TCTL, введенный Алуром и др. и представляющий собой расширение хорошо известной логики CTL за счет введения временных границ в формулы языка. Известно, что одним из эффективных методов автоматической верификации систем является алгоритм проверки на модели (model checking algorithm). Свойства системы задаются в виде логических формул и автоматически сопоставляются с графом состояний, представляющим поведение системы. Однако при верификации систем со сложной структурой приходится анализировать огромное число их состояний. Один из методов преодоления этой проблемы состоит в использовании частичных порядков, чтобы избежать конструирования эквивалентных состояний (т.е. состояний, достижимых различными интерливинговыми последовательностями срабатываний). В рамках проекта в качестве модели систем реального времени рассматривались временные сети Петри, предложенные Мерлином, и разрабатывались алгоритмы проверки на моделях с использованием аппарата логики TCTL. А также был применен подход, основанный на частичных порядках, для сокращения числа состояний временных сетей Петри с целью упрощения верификационных алгоритмов.
Использованные методы и подходы: При систематическом исследовании поведения параллельных/распределенных систем полезно разработать классификацию семантик их процессов, что приведет к лучшему пониманию важнейших свойств таких систем. Данный метод "сравнительной семантики" был развит в рамках проекта на различных моделях структур событий, потоковых схем и сетей Петри с целью установления взаимосвязей между процессами в семантиках: "интерливинг/истиный параллелизм" и "линейное/ветвистое время". В области алгебраических исчислений разработан метод композиции процессов с одинаково помеченными событиями и механизмом синхронизации по именам. Для данного метода характерны: модульность, хорошо разработанные понятия эквивалентностей, алгебраические правила и полные системы доказательств. В рамках логического подхода к изучению поведения систем, функционирующих в режиме реального времени, метод проверки на моделях (model checker) языка TCTL обобщен на временные сети Петри, в которых временные интервалы связаны с условиями готовности переходов. При этом TCTL-семантика интерпретируется относительно обобщенного графа состояний, конечность которого обеспечивается тем, что вершины графа представляют собой классы эквивалентных по времени состояний.
|
ПУБЛИКАЦИИ
| 1. |
Investigating Equivalence Notions for Nondeterministic Processes Вирбицкайте Ирина Бонавентуровна Вотинцева Анжелика Вячеславовна, Бест Айке Proc. Andrei Ershov Second International Memorial Conference "Perspectives of System Informatics", Novosibirsk, June 25-28, 1996 (1996) 220-226 | |
| Структуры событий - одна из базовых моделей параллельных недетерминированных процессов. Данная модель представляет собой множество событий, связанных отношениями причинной зависимости, параллелизма и конфликта. Известно, что прямые и обратные варианты бисимуляций отражают отношения причинности и (косвенно) параллелизма между событиями структур, однако информация о конфликте потеряна. Поэтому одна из целей данной работы состоит в том, чтобы ввести и исследовать ряд вариантов бисимуляций, которые явно отражают параллелизм и конфликт между событиями. Для получения полной картины эквивалентностных понятий на структурах событий строится диаграмма взаимосвязей между вновь введенными и уже существующими бисимуляциями. | ||
| 2. |
Investigating Semantic Notions for Coloured Dataflow Networks Вирбицкайте Ирина Бонавентуровна Вотинцева Анжелика Вячеславовна, Шкляев Дмитрий Алексеевич Hildesheimer Informatik-Berichte 27 (1996) 1-31 | |
| Потоковые (dataflow) сети являются одной из формальных моделей, предназначенных для представления, анализа и моделирования структуры параллельных вычислительных систем и их программного обеспечения. В данной работе разрабатываются различные семантические представления потоковых сетей с цветными фишками в терминах таких абстрактных моделей, как последовательности срабатываний, языки трасс, графы зависимостей и структуры событий. Также устанавливаются строгие взаимосвязи между перечисленными семантическими представлениями с точностью до изоморфизма. Такого рода исследования призваны не только разработать семантику "истинного параллелизма", но также позволяют классифицировать и унифицировать различные формальные модели параллельных процессов в контексте потоковых вычислений. | ||
| 3. |
О семантических аспектах потоковых вычислений с цветными фишками Вирбицкайте Ирина Бонавентуровна Вотинцева Анжелика Вячеславовна, Шкляев Дмитрий Алексеевич Программирование 3 (1996) 17-35 | |
| Немногочисленные потоковые модели, известные из литературы, могут быть условно разбиты на две группы - статических и динамических. Статические модели позволяют не более, чем по одной фишке на дугах потоковой сети, что приводит к ограничению параллелизма моделируемых вычислений. Динамические модели свободны от этого ограничения за счет использования механизмов копирования фрагментов сетей и раскрашивания фишек. В данной работе в качестве абстрактной модели рассматривается класс правильно построенных потоковых сетей с цветными фишками, который определяется с помощью специально разработанных алгебраических операций. Также был формализован и исследован ряд понятий (последовательностей срабатываний, языка трасс, графов зависимостей и структур событий), описывающих поведение указанного класса потоковых сетей. | ||
| 4. |
О некоторых свойствах структур событий Вирбицкайте Ирина Бонавентуровна Кибернетика и системный анализ 3 (1997) 45-55 | |
| В данной работе в контексте структур событий исследуется ряд "аксиом параллельности" (в частности, свойства дискретности, K-плотности, "перекрестности"), которые изначально были предложены К. Петри для сетей-процессов (occurrence nets) с целью получения моделей, адекватно представляющих поведение реальных параллельных систем. Для рассматриваемой модели устанавливаются взаимосвязи между перечисленными выше свойствами и формулируются необходимые и достаточные условия, гарантирующие свойства такого типа. | ||
| 5. |
Equivalence Notions for Event Structures and Refinement of Actions Вотинцева Анжелика Вячеславовна Joint NCC and IIS Bulletin, Series Computer Science (1996) 91-104 | |
| В данной работе структуры событий рассматриваются как одна из моделей параллельных недетерминированных процессов. Вводятся различные эквивалентностные понятия, отражающие особенности данной модели. Одним из главных свойств эквивалентностных понятий является их сохранение при выполнении операции детализации, которая позволяет исследовать системы при изменении уровня абстракции, интерпретируя действия высшего уровня более сложными процессами на нижнем уровне. В данной статьи было показано, что бисимуляции, принимающие во внимание (возможно, неявно) структуру причинных зависимостей, сохраняются при смене уровня абстракции, тогда как варианты интерливинговой, шаговой и ЧУММ-бисимуляций - нет. | ||
| 6. |
Petri net equivalences for design of concurrent systems Тарасюк Игорь Валерьевич Informatik-Berichte 69 (1996) 190-204 | |
| Понятие эквивалентности является центральным в теории систем. Различные эквивалентностные отношения используются для сравнения параллельных систем и процессов с учетом тех или иных аспектов их поведения. Для систематического исследования таких систем важно проверить для них все возможности быть эквивалентными. В данной работе в качестве формальной модели параллельных систем выбраны сети Петри, которые наиболее полно и естественно отражают такие важные понятия, как недетерминизм, параллелизм и причинную зависимость. Базисные поведенческие эквивалентности, известные из литературы и определенные в рамках различных формальных моделей, были перенесены на сети Петри и дополнены новыми понятиями следовых, бисимуляционных и сохраняющих конфликт эквивалентностей с целью получить полное множество эквивалентностных отношений в семантиках от интерливинговой до "истинного параллелизма" и от "линейного" до "ветвистого" времени. Были установлены взаимосвязи между всеми рассмотренными базисными эквивалентностями как на всем классе сетей Петри, так и на таких подклассах, как последовательные сети, Т-сети и сети со строгой пометкой. Исследовано также сохранение эквивалентностных понятий при операции детализации для того, чтобы понять, какие из них могут быть использованы для разработки параллельных систем по методу "сверху-вниз". | ||
| 7. |
Понятия эквивалентностей для разработки параллельных систем с использованием сетей Петри Тарасюк Игорь Валерьевич Программирование | |
| Исследуются поведенческие эквивалентности систем, моделируемых сетями Петри. Основные эквивалентностные понятия, известные из литературы, дополнены новыми. В результате получен методологически полный набор базисных эквивалентностей, в различной степени учитывающих аспекты параллелизма и конфликта в поведении моделируемых систем. Взаимосвязи эквивалентностей исследованы на всем классе сетей Петри и на подклассе последовательных сетей (сети без параллелизма), что позволило глубже понять их природу, а также сходство и различие данных отношений. Получена полная диаграмма взаимосвязей эквивалентностей, дающая возможность выбора наиболее подходяшего критерия равенства (семантики) при моделировании систем. Также изучены композициональные аспекты эквивалентностных понятий. Выяснено, какие эквивалентности сохраняются при операции "детализации", соответствующей переходу на более низкий уровень абстракции при нисходящей разработке параллельных систем. | ||
| 8. |
Back-forth equivalences for design of concurrent systems Тарасюк Игорь Валерьевич Lecture Notes in Computer Science 1234 (1997) 374-384 | |
| Изучаются обратные-прямые бисимуляционные эквивалентности в рамках модели сетей Петри. Указанные отношения дают операционную характеризацию эквивалентностей такого интересного формализма, как темпоральные логики с модальностями прошлого. Эти логики могут использоваться для спецификации свойств "прошлого" в поведении моделируемых систем, что бывает актуально, когда требуется провести обратные вычисления для возврата в прежнее состояние. Рассмотрен широкий набор бисимуляционных эквивалентностей, у которых могут различаться виды обратного и прямого моделирования. Вид моделирования может меняться в зависимости от учитываемых аспектов параллелизма. Выяснены взаимосвязи всех указанных эквивалентностей между собой и с группой базисных отношений. Показано, что ряд обратных-прямых эквивалентностей совпадает с важнейшими "сохраняющими историю" бисимуляционными отношениями и позволяет дать логическую характеризацию последних. Все эквивалентности проверены на сохранение при операции детализации и выяснено, какие из них могут быть использованы в процессе разработки систем по методу "сверху-вниз". Изучены взаимосвязи всех эквивалентностей на подклассе последовательных сетей, что позволило глубже понять роль аспектов параллелизма в определениях данных отношений. | ||
| 9. |
An investigation of back-forth and place bisimulation equivalences Тарасюк Игорь Валерьевич Hildesheimer Informatik-Berichte 8 (1997) | |
| Изучается широкий набор эквивалентностных отношений сетей Петри, включающий базисные, обратные-прямые и бисимуляционные эквивалентности мест. Эквивалентности мест - отношения на местах сетей Петри, а не на их состояниях, как обычно. Важное свойство данных эквивалентностей - возможность их эффективной проверки. За счет слияния эквивалентных мест и удаления излишних переходов возможна эффективная редукция сетей Петри с сохранением поведения по модулю эквивалентностей. В данной работы выясняется взаимосвязь эквивалентностей мест с базисными и обратными-прямыми отношениями, что дает возможность выяснить, какой набор поведенческих свойств сохраняется в процессе редукции сетей Петри. Исследовано сохранение всех эквивалентностей при операции детализации. Найден вариант бисимуляционной эквивалентности мест, который может использоваться для редукции систем в процессе их нисходящей разработки. Выяснена взаимосвязь эквивалентностей на подклассе последовательных сетей, что позволило упростить сравнение поведения систем без параллелизма, моделируемых сетями этого подкласса. | ||
| 10. |
Investigating equivalence notions for time Petri nets Вирбицкайте Ирина Бонавентуровна Тарасюк Игорь Валерьевич Logic Journal of the IGPL 5(6) (1997) | |
| Исследованы эквивалентности для временных сетей Петри с невидимыми переходами. Невидимые перехолы помечены специальным символом "невидимого" действия и соответствуют элементарным компонентам моделируемой системы, влияние которых на поведение не учитывается явно. Определен ряд временных, не-временных и региональных эквивалентностей в следовой и бисимуляционной семантиках, в разной степени учитывающих влияние невидимых действий. Дана региональная характеризация временных эквивалентностей, упрощающая их проверку за счет слияния неограниченного числа промежуточных состояний, разлицающихся лишь некоторыми параметрами временной компоненты. Исследована взаимосвязь всех отношений на временных сетях и их подклассе не-временных сетей (с нулевыми временными задержками). Введена новая операции временной детализации. Проверено сохранение эквивалентностей при применении этой операции и установлено, что временная бисимуляционная эквивалентность может быть использована в процессе нисходящей разработки параллельных систем реального времени. | ||
| 11. |
Исследование слабых бисимуляций для структур событий Вотинцева Анжелика Вячеславовна Препринт ИСИ СО РАН 41 (1997) 1-30 | |
| В данной работе рассматриваются обратные варианты бисимуляционных эквивалентностей на структурах событий в различных семантиках, определяется ряд бисимуляций, явно отражающих параллелизм и конфликт между событиями структуры. Для перечисленных эквивалентностей вводятся их слабые варианты, которые используют понятие ``невидимых'' действий. Установлена полная иерархия всех рассмотренных эквивалентностных понятий. Исследовано сохранение/ несохранение под действием операции уточнения для всех вновь введенных бисимуляций. | ||
| 12. |
Temporal Logics for Concurrent Nondeterministic Processes Вирбицкайте Ирина Бонавентуровна Вотинцева Анжелика Вячеславовна Logical Journal of IGPAL 5(6) (1997) | |
| С целью увеличения выразительной мощности темпоральной логики CTL* рассмотрен ряд ее расширений посредством дополнительных операторов конфликта, параллелизма и оператора, допускающего ветвление прошлого, а также их комбинация. Установлены поведенческие эквиваленты для полученных расширений. | ||
| 13. |
Partial Order Logics and Equivalences for Event Structures Вирбицкайте Ирина Бонавентуровна Вотинцева Анжелика Вячеславовна Proc. 15-th IMACS World Congress on Scientific Computation, Modelling and Applied Mathematics 5 (1997) 505--510 | |
| Для лучшего понимания значения логических формализмов в литературе довольно часто различные логики сравниваются с поведенческими эквивалентностями. В данной статье рассматриваются логики частичного порядка: L_1, введенная М. Мукундом и П. Тиагараджаном, и L_1^r --- расширение логики L_1 за счет дополнительного понятия максимального вычисления, заимствованного из логики В. Пенчека. В отличие от других логических формализмов, рассмотренные в данной статье языки позволяют описывать параллелизм и недетерминизм. | ||
| 14. |
Towards Efficient Verification of Time Petri Nets. Вирбицкайте Ирина Бонавентуровна Покозий Екатерина Александровна Logical Journal of IGPAL 5(6) (1997) | |
| Разработан метод верификации временных поведенческих свойств параллельных систем, представленных безопасными временными сетями Мерлина, на основе аппарата темпоральных логик реального времени TCTL. Для сокращения числа состояний временных сетей Петри с целью упрощения алгоритма верификации применен подход, основанный на частичных порядках. | ||
| 15. |
An Event Structure Model for Dataflow Computing Вирбицкайте Ирина Бонавентуровна Computers and Artificial Intelligence (1998) | |
| В данной работе сначала определятся понятие потоковой схемы, а затем вводится алгебраический язык структурированных потоковых схем с цветными фишками. Для этих целей рассматривается ряд элементарных схем: операторная, альтернативная и итеративная. При определении структурированных потоковых схем используются перечисленные выше элементарные схемы и алгебраические операции параллельной, последовательной, альтернативной и итеративной композиций. Изучаются поведенческие свойства структурированных потоковых схем с цветными фишками. | ||
| 16. |
Comparing Logical and Behavioural Equivalences for Event Structures Вирбицкайте Ирина Бонавентуровна Вотинцева Анжелика Вячеславовна, Бест Айке Hildesheimer Informatik-Berichte 22 (1996) 1-30 | |
| Основная цель данной статьи - установить взаимосвязи между эквивалентностью, налагаемой логикой $L_1$, введенной М. Мукундом и П.С. Тиагараджаном, и бисимуляциями на структурах событий. В отличие от других логических формализмов, язык $L_1$ содержит наряду с традиционными модальностями прошлого и будущего дополнительные модальности параллелизма и конфликта. Семантика данного языка определяется с использованием структур событий в качестве Крипке-фреймов. Логическая эквивалентность отличает только те структуры, которые различаются некоторой формулой языка. Для установления соответствия между логической и поведенческими эквивалентностями в данной работе вводится ряд бисимуляций, областью определения которых является множество локальных конфигураций структур событий. | ||
| 17. |
An algebra of labelled nondeterministic processes Тарасюк Игорь Валерьевич Joint NCC and IIS Bulletin, Series Computer Science 5 (1996) 75-90 | |
| Для описания и анализа конечных недетерминированных процессов В.Е. Котовым и Л.А. Черкасовой была разработана алгебра $AFP_2$ с семантикой, учитывающей "истинный параллелизм", и удобными механизмами синхронизации и описания недетерминизма. Однако, данное алгебраическое исчисление имеет недостаточные описательные возможности. В данной работе исчисление $AFP_2$ расширяется функцией пометки. В результате получена новая алгебра помеченных конечных недетерминированных процессов $AFLP_2$, в которой можно специфицировать процессы с несколькими событиями, помеченными одинаковыми действиями. Исследованы синтаксис и семантика $AFLP_2$. Дана полная и корректная аксиоматизация семантической эквивалентности. Важная задача, возникающая при совместном рассмотрении сетевых и алгебраических спецификаций, - установление соответствия между эквивалентностями сетей Петри и семантическими эквивалентностями процессных алгебр. Решение этой задачи дает возможность переходить от сетевого представления к формульному и обратно с сохранением требуемых свойств моделируемых систем. В данной работе исследованы взаимосвязи базисных эквивалентностей сетей Петри с семантическими эквивалентностями $AFLP_2$. Аналоги сетевых эквивалентностей были определены на формулах $AFLP_2$. Важное свойство эквивалентностей процессных алгебр - композициональность, то есть сохранение относительно алгебраических операций. В данной работе аналоги сетевых эквивалентностей были исследованы на композициональность относительно операций $AFLP_2$. | ||
| 18. |
Equivalence notions for design of concurrent systems using Petri nets. Algebra $AFLP_2$: a calculus of labelled nondeterministic processes. Тарасюк Игорь Валерьевич Hildesheimer Informatik-Berichte 4 (1996) | |
| Множество базисных поведенческих эквивалентностей, в разной степени учитывающих такие важные понятия теории параллельных процессов, как причинная зависимость и конфликт, было рассмотрено в рамках моделей сетей Петри и процессных алгебр. Построена диаграмма взаимосвязей эквивалентностных отношений как на всем классе сетей Петри, так и на подклассах последовательных и строго помеченных сетей. Проведено исследование сохранения эквивалентностных понятий при переходе на более низкий уровень абстракции для того, чтобы понять, какие из них могут быть использованы для разработки многоуровневых параллельных систем. Изучена взаимосвязь базисных эквивалентностей сетей Петри с семантической эквивалентностью алгебры помеченных недетерминириванных процессов $AFLP_2$. Аналоги сетевых эквивалентностей определены на формулах данной алгебры и проверены на композициональность относительно операций исчисления. | ||