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

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

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

Введение

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

1.1 Обзор исследований в области потоковой обработки информации

1.1.1 Архитектуры потоковых вычислительных систем

1.1.2 Потоковые языки программирования

1.2 Потоковые схемы с тегированными фишками.

1.2.1 Определение потоковой схемы с тегированными фишками (п-схемы).

1.2.2 Структурированные п-схемы.

1.2.3 П-схемы с массивами.

1.2.4 П-схемы с процедурами.

1.3 Автоматическое построение потоковых схем с тегированными фишками.

1.3.1 Некоторые атрибуты с-схем.

1.3.2 Преобразование ациклических с-схем в потоковый

1.3.3 Преобразование с-схем, содержащих циклические фрагменты, в потоковый вид.

1.3.4 Преобразование обогащенных с-схем в обогащенные структурированные п-схемы.

2 Сравнительный анализ семантических моделей параллельных процессов и процессов реального времени

2.1 'Аксиомы параллельности' как базовые свойства параллельных недетерминированных процессов.

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

2.1.2 Локальные структуры событий и их свойства параллельности

2.2 Семантические модели потоковых вычислений с тегированными фишками.

2.2.1 Графы зависимостей.

2.2.2 Семантика структур событий.

2.3 Бисимуляционные эквивалентности параллельных недетерминированных процессов и их логическая характеризация

2.3.1 Бисимуляционные эквивалентности.

2.3.2 Логическая характеризация обычных бисимуляций

2.3.3 Логическая характеризация локальных бисимуляций

2.3.4 Разрешимость бисимуляционных эквивалентностей

2.4 Исследование параллельной семантики процессов реального времени.

2.4.1 Временные структуры событий.

2.4.2 Интерливинговая семантика.

2.4.3 Шаговая семантика

2.4.4 Семантика временных частично упорядоченных мультимножеств

2.4.5 Сравнение временных эквивалентностей.

3 Анализ корректности параллельных моделей реального времени

3.1 Верификация временных сетей Петри с использованием аппарата темпоральных логик реального времени.

3.1.1 Базовый метод верификации.

3.1.2 Метод с использованием техники частичных порядков

3.1.3 Метод с использованием техники временных зон

3.1.4 Метод с использованием техники параметризации

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

3.2.1 Временные процессы и эквивалентностные понятия временных сетей Петри.

3.2.2 Распознавание временной трассовой и временной тестовой эквивалентностей.

3.2.3 Распознавание временной бисимуляции.

3.3 Автоматические анализ и верификация сетевых параллельных моделей реального времени

3.3.1 Обзор инструментальных средств, поддерживающих сетевые модели.

3.3.2 Краткое описание возможностей системы PEP

3.3.3 Концепции, организация и возможности системы RT-МЕС.

Введение диссертации (часть автореферата) на тему «Формальные модели и анализ корректности параллельных систем и систем реального времени»

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

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

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

Формальные модели параллелизма.

Структурные модели. При первых шагах развития теории параллелизма использовался тот факт, что параллельная программа является обобщением последовательной, и поэтому в известные последовательные модели и методы добавлялись элементы, позволяющие описывать и изучать параллельные программы и процессы. Например, теория последовательного программирования разработала схематологи-ческий подход, в основе которого лежало стремление отказаться от изучения самих программ в пользу более абстрактных объектов - схем программ. Данное направление в теории параллелизма восходит к параллельным операторным схемам Карпа и Миллера [24], счетчиковым схемам [24], А-схемам [26], схемам потоков данных [108] и т.д. С использованием этих моделей изучались структурные и функциональные особенности параллельных программ и систем, а также взаимодействие составляющих их компонентов. Развитие формальных моделей параллелизма достигла своей кульминации в период становления теории сетей Петри, предложенной немецким ученым К. Петри в середине 60-х гг. и разработанной на основе теорий физических процессов и автоматов. К настоящему времени сложилась хорошо развитая теория сетей Петри, к достоинствам которых можно отнести удобное графическое представление и эффективные методы анализа их поведения. С помощью сетевых моделей установлен ряд фундаментальных фактов, которые позволили лучше понять природу параллельных вычислений. Так, например, выделены три базовых отношения между событиями параллельных систем: причинная зависимость, параллелизм и недетерминированный выбор (конфликт). Дальнейшее продвижение в данной области, с одной стороны, связано с изучением обоснованных с теоретической точки зрения подклассов сетевых моделей (например, элементарных сетевых систем (elementary net systems) [260], систем с условиями/событиями (condition/event systems) [231], сетей со свободным выбором (free choice nets) [113]), позволяющих рассматривать сети Петри как математические объекты и формально исследовать их свойства, правила конструирования и преобразования. С другой стороны, появились различные расширения сетей Петри: временные и стохастические сети [194, 201, 240, 248], сети с предикатами (predicate/transition nets) [21], сети Петри с раскрашенными фишками (coloured Petri nets) [166] и т.д., призванные служить математическим инструментом для моделирования и анализа реальных параллельных систем сложной структуры.

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

К настоящему времени известно большое многообразие абстрактных семантических моделей: сети-процессы [68, 69, 94], системы переходов [173], трассы Хоара [158], трассы Мазуркевича [32, 196], частично упорядоченные множества [72, 123, 235], структуры событий [218, 302], причинные деревья (causal trees) [105], деревья синхронизации (synchronization trees) [202] и т.д. С помощью этих моделей исследуются поведенческие свойства параллельных/распределенных систем, определяются различные семантические представления параллельных процессов, а также разрабатываются методы их анализа и синтеза, устанавливаются взаимосвязи между существующими подходами к изучению семантики параллельных программ. Такое многообразие моделей требует их систематизации и унификации. Установлением глубоких взаимосвязей между различными семантическими моделями занимается специальный раздел теории параллелизма — компаративная семантика. Часто отношения между моделями могут быть охарактеризованы в терминах поведенческих эквивалент-ностей. В настоящее время в теории параллелизма известно большое многообразие эквивалентностных понятий. Особо следует отметить такие подходы, как трассовый

158], бисимуляционный [150, 224] и тестовый [213]. Взаимосвязи между различными вариантами этих эквивалентностей к настоящему времени особенно хорошо изучены для моделей систем переходов [133].

Алгебры процессов (исчисления процессов). В основе алгебраического подхода лежит математическая теория, описанная в виде систематического набора алгебраических законов, что позволяет представлять и изучать параллельные системы как элементы алгебры. Такая алгебраическая теория дает строгое определение понятия процесса и способы построения и взаимодействия параллельных процессов. Эти определения составляют основу алгебраических законов, реализаций и правил доказательств корректности процессов. Изначально многие исследователи надеялись получить универсальную процессную алгебру, ведущую к 'тезису Черча' для параллельных вычислительных процессов. Как предполагалось, универсальная алгебра должна иметь несколько фундаментальных операторов, и должно быть возможным моделирование любых параллельных процессов и доказательство их корректности алгебраически. К сожалению, универсальная алгебра пока не найдена, однако надежда получить ее остается.

Наиболее яркими представителями алгебраического подхода являются теория взаимодействующих последовательных процессов (CSP) [158], исчисление взаимодействующих систем (CCS) [194], алгебра параллельных процессов (АСР) [64], тг-исчисление [203] и т.д. Исследуются методы композиции процессов и способы их взаимодействия, а также методы описания операционной и денотационной семантик исчислений процессов посредством различных, но непротиворечивых абстрактных моделей, отличающихся степенью детализации и удобством описания базовых понятий. Наиболее очевидной сферой применения алгебраического подхода является спецификация, разработка и реализация систем, которые состоят из набора компонентов, непрерывно взаимодействующих друг с другом и с внешним окружением.

Логики процессов. Исследования концентрируются на разработке методов и средств спецификации и верификации параллельных процессов с помощью аппарата различных логических языков. Для этих целей было предложено большое разнообразие темпоральных логик (LTL, CTL, CTL* и т.д.), проведено сравнение их выразительных мощностей [115], что дало толчок к появлению модального ^-исчисления [180], обладающего в некотором смысле канонической выразительной мощностью. Последние годы делаются попытки адаптировать традиционные темпоральные логики для более адекватного описания параллелизма процессов в контексте трассовых моделей [261] и моделей структур событий [207, 208, 228]. Также был разработай ряд языков динамических логик [227] и логик знаний [145].

Кроме того, в данной проблематике сформировались два подхода к верификации параллельных процессов: аксиоматический и алгоритмический. При первом подходе разрабатываются система аксиом (с помощью которой может быть описана как сама система, так и ее свойства) и правила вывода. Для верификационных целей используется механический доказатель теорем. В качестве теорем выводимы утверждения о корректности программ. Системы доказательств разработаны для различных логических языков [164]. Основу второго подхода составляют алгоритмы проверки на модели (model checking) [96], объединяющие в себе традиционные и логические методы анализа свойств процессов. Проверка на модели является эффективным методом верификации поведенческих свойств параллельных систем с конечным числом состояний. При таком подходе свойство системы задается в виде логической формулы, истинность которой проверяется на графе состояний, представляющем поведение системы. Очевидно, что при верификации реальных систем приходится анализировать огромное число состояний. Известен ряд методов для преодоления этой проблемы: частичных порядков [138,198, 266], символьных состояний [86], симметрии [117], 'развертки' [119, 198] и т.д.

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

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

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

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

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

3. Семантика линейного времени (linear time) и ветвящегося времени (branching time). Модели линейного и ветвящегося времени различаются тем, как рассматриваются точки недетерминированного выбора. В моделях линейного времени поведение системы представляется в виде множества возможных последовательностей реализаций ее событий. При этом теряется информация не только о параллелизме, но также и о недетерминированном выборе (конфликтующих событиях), т.е. информация о ветвящейся структуре процесса. Чтобы избежать этого недостатка, в моделях ветвящегося времени поведение системы описывается древовидными структурами, которые показывают точки, где при вычислениях должен быть сделан недетерминированный выбор. Вопросы описания недетерминизма проработаны в исчислениях процессов, а также в таких моделях, как деревья синхронизации, причинные деревья, структуры событий и т.д.

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

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

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

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

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

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

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

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

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

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

Практическая ценность. Разработанные автором диссертации методы могут лечь в основу широкого спектра промышленных программных систем: блоков автоматического распараллеливания в трансляторах и интерпретаторах, систем построения семантических представлений и эквивалентных преобразований параллельных процессов, систем верификации процессов реального времени. Результаты диссертационной работы были успешно реализованы в рамках экспериментальной системы RT-MEC (Real-Time Model and Equivalence Checker), которая поддерживает различные методы спецификации, анализа, верификации параллельных систем и систем реального времени, представленных различными сетевыми моделями с временными характеристиками, и которая является частью системы PEP (Programming Envi-ronement based on Petri nets), совместно разрабатываемой несколькими немецкими университетами (г. Хильдесхайма, г. Ольдеибурга, г. Мюнхена).

Апробация работы. Основные идеи и конкретные результаты диссертационной работы обсуждались на следующих всесоюзных и международных научных симпозиумах, конференциях и семинарах: Всесоюзная школа-семинар 'Распределенная обработка информации' (Львов, 1987, Львов 1989); Всесоюзная конференция 'Однородные вычислительные среды и систолические структуры' (Львов, 1990); International Conference of Young Computer Scientists (Beijing, 1993); International Seminar 'Concurrency: Specification and Programming' (Nieborow, Poland, 1993; Berlin 1994;

Warsaw, 1999; Berlin, 2000); International Conference 'Formal Methods in Programming and their Applications' (Novosibirsk, 1993); A.P Ershov International Memorial Conferences on Perspectives of System Informatics (Novosibirsk, 1996; Novosibirsk, 2001); International Conference 'CONPAR 94 - VAPP VI' (Linz, Austria, 1994); 4th International Conference on Applied Logics (Irkutsk, Russia, 1995); International Symposium on Fundamentals of Computation Theory (Krakow, Poland, 1997; Iassy, Romania 1999; Riga, 2001); International Workshop on Logic, Language, Information and Computation (Fortaleza, Brazil, 1997; Natal, Brazil, 2000); IMACS World Congress on Scientific Computation, Modelling and Applied Mathematics (Berlin, 1997); International Workshop on Distributed Data Processing (Novosibirsk, 1998); International Workshop on Discrete Event Systems (Cagliari, Italy, 1998); MFCS'98 International Workshop on Concurrency (Brno, Chezh Republic, 1998); International Conference on Parallel Computing Technology (Sankt-Peterburg, 1999; Novosibirsk 2001).

Кроме того, доклады no теме работы были сделаны на ряде семинаров Института информатики Университета г. Хильдесхайма (Германия), Института прикладной математики (г. Гренобль, Франция), Института кибернетики (г. Киев), Киевского государственного университета, Московского государственного университета, Московского электротехнического института, Института программных систем РАН (г. Переславль-Залесский), Института математики СО РАН (г. Новосибирск), Института систем информатики СО РАН (г. Новосибирск), кафедр Новосибирского государственного университета и др.

Публикации. По теме диссертации опубликовано 69 научных работ, в том числе одна монография, 17 работ — в зарубежных периодических изданиях и журналах, 16 — в трудах международных симпозиумов, конференций и семинаров, 7 — в отечественной центральной печати.

Структура и объем работы. Диссертация состоит из введения, трех глав, заключения, списка литературы и приложения.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Вирбицкайте, Ирина Бонавентуровна

Выводы к главе

• Разработан алгоритм верификации поведенческих свойств безопасных временных сетей Петри на основе темпоральной логики реального времени TCTL, который позволяет проверять не только качественные, но и количественные временные свойства сети: построено конечное представление поведения временной сети Петри в виде графа регионов; предложен алгоритм пометки графа регионов TCTL-формулой; показана корректность и дана оценка сложности предложенного алгоритма.

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

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

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

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

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

Заключение

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

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

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

• Разработана и практически реализована концепция анализа корректности параллельных систем реального времени, представленных различными временными сетевыми моделями, с использованием аппарата темпоральных логик реального времени и временных эквивалентностных отношений: предложены методы верификации систем реального времени, представленных сетевыми моделями с непрерывным временем. Временные свойства представляются в виде формул известной темпоральной логики реального времени TCTL. Продемонстрирована возможность применения техники частичных порядков для редукции числа анализируемых сетевых состояний. Даны оценки сложности предложенных алгоритмов и доказана их корректность; с целью повышения эффективности верификационных алгоритмов введены и исследованы новые модели параллельных систем реального времени — временные сети с зонами и параметрические временные сети, а также предложены и оценены методы поведенческого анализа данных моделей; решены проблемы распознавания временных трассовой, тестовой и би-симуляционной эквивалентностей в контексте конечного варианта вновь разработанной временной семантической модели — временных процессов (сетевых процессов с глобальным непрерывным временем). Распознавание временной трассовой и временной тестовой эквивалентностей осуществляется с использованием техник графов регионов, детерминированных графов и сведения указанных эквивалентностей к соответствующим вариантам бисимуляционной эквивалентности на детерминированных графах временных процессов. Распознавание временных бисимуляционных эквивалентностей базируется на методах теории категорий (понятии открытых морфизмов). Предложены алгоритмы распознавания указанных временных эквивалентностей для дискретно-временных сетей Петри с использованием вновь введенного понятия временной экспансии раскрутки МакМиллана. Показана корректность предложенных алгоритмов и даны оценки их сложности; разработана и программно реализована экспериментальная система RT-MEC, поддерживающая методы спецификации, анализа, верификации параллельных систем и систем реального времени, представленных различными моделями временных сетей Петри. Средствами RT-MEC проведены эксперименты, демонстрирующие целесообразность и эффективность предложенных формальных методов.

Список литературы диссертационного исследования доктор физико-математических наук Вирбицкайте, Ирина Бонавентуровна, 2001 год

1. Алгоритмы, математическое обеспечение и архитектура многопроцессорных вычислительных систем. М.: Изд-во Наука, 1982. - 336с.

2. Ачасова С.М., Бандман О.Л. Корректность параллельных вычислительных процессов. Новосибирск: Наука, 1990. - 252с.

3. Барский А. Б. Структура и архитектура потоковой вычислительной системы / / Вопросы кибернетики. Эффективное использование высокопроизводительных ЭВМ. 1985. - С. 136-151.

4. Борисенко В.И. Трансляция схем программ в схемы потоков данных. Киев, 1979. - 40с. - (Преп./АН УССР. Институт кибернетики; № 79-42).

5. Бураченко Т. Е., Орлова И. А., Погребинский С.Б. Управляющий процессор ма-кроконвейерной ЭВМ. Программные и аппаратные средства многопроцессорных вычислительных комплексов. Киев, 1989. (Преп./АН УССР. Институт кибернетики; № 89-15).6 7

6. Вальковский В.А., Вирбицкайте И.Б. Потоковые вычислительные системы // Системная информатика. Новосибирск: Наука, 1993. - Т. 2. - С. 38-72.

7. Вирбицкайте И.Б. О программной реализации системы имитации потоковых вычислений // Тр. VI Всесоюз. шк.-сем. "Распределенная обработка информации".- Львов, 1987. С. 20-22.

8. Вирбицкайте И.Б. О преобразовании схем программ в потоковые модели // Высокопроизводительные вычислительные системы и их программное обеспечение.- Новосибирск, 1987. С. 115-129.

9. Вирбицкайте И.Б. Рекурсивный алгоритм конструирования потоковых схем // Теория и методы параллельной обработки информации. Новосибирск, 1987. -С. 65-82.

10. Вирбицкайте И. Б. ЭВМ, управляемые потоками данных. Новосибирск, 1989.- 60с. (Препр./АН СССР. Сиб. отд-ние. ВЦ; № 822).

11. Вирбицкайте И. Б. Обработка последовательных фрагментов на устройствах потокового типа // Тр. VII Всесоюз. шк-сем. "Распределенная обработка информации". Львов, 1989. - С. 75.

12. Вирбицкайте И.Б. Комплекс программ для экспериментов для экспериментов над потоковыми вычислениями // Архитектура и программное обеспечение многопроцессорных вычислительных комплексов. Новосибирск, 1989. - С. 105-116.

13. Вирбицкайте И.Б. О некоторых свойствах структур событий // Кибернетика и системный анализ. 1997. - № 3. - С. 45-55.

14. Вирбицкайте И.Б. Семантические модели в теории параллелизма. Новосибирск: ИСИ СО РАН, 2000. - 196с.

15. Вирбицкайте И.В., Боженкова Е.Н. Исследование тестовой эквивалентности временных структур событий // Программирование. 2000. - № 5. - С. 18-30.

16. Вирбицкайте И.В., Вотинцева А.В., Шкляев Д.А. О семантических аспектах потоковых вычислений с цветными фишками // Программирование. 1996. - № 3. - С. 17-35.

17. Вирбицкайте И.В., Покозий Е.А. Использование техники частичных порядков для верификации временных сетей Петри // Программирование. 1999. - № 1.- С. 28-41.

18. Вирбицкайте И.В., Покозий Е.А. Метод параметрической верификации поведения временных сетей Петри // Программирование. 1999. - № 4. - С. 16-29.

19. Вишневский Ю. JL, Дорожевец М. Н. Система Марс-М. Исходные предпосылки и конечные цели разработки // Высокопроизводительные вычислительные системы и их программное обеспечение. Новосибирск, 1987. - С. 6-16.

20. Водяхо А. И., Емелин В. П. и др. Векторно-потоковые суперЭВМ // Изв. вузов. Приборостроение. 1987. - Т. 30, 10. - С.35-40.

21. Годьо Ж.-Л. Применение многопроцессорных ЭВМ, управляемых данными, в цифровой обработке сигналов // Тр. ин-т. инж. по электротехн. и радиоэлектрон. М.: Мир, 1987. - Т. 97, № 9. - С. 90-106.

22. Каляев А. В., Макаревич О. В., Николаев И. А., Бабенко Л. К. СуперЭВМ с программируемой архитектурой // ЭВТ/ - 1988. - Вып. 2. - С. 5-33.

23. Капитонова Ю. В., Летичевский А. А. Синтез макроконвейерных программ // Кибернетика. 1987. - № 5. - С. 11-18.

24. Карп P.M., Миллер Р.Е. Параллельные схемы программ // Кибернетический сборник. М.: Мир. - 1976. - Т. 13. - С. 5-61.

25. Котов В.Е. Сети Петри. М.: Наука, 1984. - 160с.

26. Котов В.Е., Нариньяни А.С. Асинхронные вычислительные процессы над памятью // Кибернетика. 1966. - № 3. - С. 64-71.

27. Котов В.Е., Черкасова Л.А. Исчисления процессов // Системная информатика.- Новосибирск: Наука, 1993. Т. 2. - С. 6-38.

28. Прангишвили П. В., Стецюра Г. Г. Современное состояние проблемы создания ЭВМ с нетрадиционной структурой и архитектурой, управляемых потоком данных // Измерения, контроль, автоматизация. 1981. - № 1/35. - С. 36-48.

29. Торгашев В. А., Плюснин В. У., Понамарев В. М. Мультипроцессор с динамической архитектурой // ЭВТ. - 1988. - Вып. 2. - С. 172-182.

30. Устименко А.П. Отображение временных причинно-следственных структур во временные сети Петри // Кибернетика и системный анализ. 1997. - № 2. - С. 44-54.

31. Шилов В. В. Использование языков высокого уровня в вычислительных системах с потоковой обработкой информации // Вопросы кибернетики. Проблемы организации высокопроизводительных ЭВМ. М., 1984. - С. 142-154.

32. Aalbersberg I.J., Rozenberg G. Theory of traces. Univ. Leiden, Tech. Rep. 86-16, 1986.33. van der Aalst W.M.P. Timed coloured Petri nets and their application to logistics // PhD Thesis, Eindhoven University of Technology, 1992.

33. Abramsky S. On semantic foundations for applicative multiprogramming // Lect. Notes Comput. Sci. 1985. - Vol. 154. - P. 1-14.

34. Aceto L., De Nicola R., Fantechi A. Testing equivalences for event structures // Lect. Notes Comput. Sci. 1987. - Vol. 280. - P. 1-20.

35. Aceto L., Murphi D. Timing and causality in process algebra // Acta Informatica. -1996. Vol. 33, N 4. - P. 317-350.

36. Ackerman W. B. Data flow languages // Computer. 1982. - Vol. 15(2). - P. 15-25.

37. Ackerman W. В., Dennis J. B. VAL-a value oriented algorithmic language: Preliminary Reference Manual. Lab. Comput. Sci., MIT. Cambridge, Mass. Tech. Rep. 218, 1979.

38. Adler M. An algebra for data flow diagram process decomposition // IEEE Trans. Soft. Engen. 1988. - Vol. 14(2). - P. 169-183.

39. Akaza M., Lee D., Kumagai S. Optimal cycle time and facility utilisation of production systems including repetitive process with set-up time modelled by time marked graphs // IEICE Transactions. 1992. - Vol. E75-A(10).

40. Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems // Proc. 5th Symp. Logic in Comput. Sci, 1990, P. 414-425.

41. Alur R., Courcoubetis C., Henzinger T.A. The observational power of clocks // Lect. Notes Comput. Sci. 1994. - Vol. 836. - P. 162-177.

42. Alur R., Courcoubetis C., Halbwachs N., Dill D., Wong-Toi H. Minimization of timed transition systems // Lect. Notes Comput. Sci. 1992. - Vol. 630. - P. 340-354.

43. Alur R., Dill D. The theory of timed automata // Lect. Notes Comput. Sci. 1991. - Vol. 600. - P. 45-73.

44. Alur R., Henziger T.A. A really temporal logic // Proc. 30th Ann. Symp. Found. Comput. Sci. IEEE Computer Society Press, 1989. - P. 164-169.

45. Alur, R., Henziger, T.A. Real-time logics: complexity and expressiveness // Proc. 5th Symp. Logic in Comput. Sci, 1990, P. 390-401.

46. Alur R., Henziger T.A. Logics and models of real time: a survey // Lect. Notes Comput. Sci. 1992. - Vol. 600. - P. 74-106.

47. R. Alur, R.P. Kurshan. Timing analysis in Cospan // Lect. Notes Comput. Sci.1996. Vol. 1066. - P. 220-231.

48. Amamiya M., Takesue M., Hasegawa R., Mikamu M. Implementation and evaluation of a list processing-oriented dataflow machine // Proc. 13th Ann. Internat. Sympos. Comput. Archit., Tokyo, June 2-5, 1986. Washington, D.C., 1986. - P. 10-19.

49. Andreeva M.V., Bozhenkova E.N., Virbitskaite I.B. Analysis of timed concurrent models based on testing equivalence // Fundamenta Informaticae. 2000. - Vol. 43, N 1-4. - P. 1-20.

50. Anisimov N.A. A disabling of event structure // Lect. Notes Comput. Sci. 1993. -Vol. 694. - P. 724-727.

51. Arvind, Culler D. E. Dataflow architectures. Lab. Comput. Sci., MIT. Cambridge, Mass. Tech. Rep. TM-294, 1986.

52. Arvind, Gostelow, K.P. U-interpretator // Computer. 1982. - Vol. 15(2). - P. 42-49.

53. Arvind, Gostelow K. P., Plouffe W. An asynchronous programming language and computing machine. Dept. Inform. Comput. Sci., Univ. California, Irvine, California. Tech. Rep. 114a, 1978.

54. Arvind, Kathail V. A multiple processor data flow that supports generalized procedures // Proc. 8th Ann. Sympos. Comput. Archit., Minneapolis, May, 1981. New York, 1981. - P. 291-302.

55. Arvind, Kathail V. A data flow architecture with tagged tokens. Lab. Comput. Sci., MIT. Cambridge, Mass. Tech. Rep. TM-174, 1980.

56. Arvind, Nikhil R. S., Pingali К. K. I-structures: Data structures for parallel computing // Lect. Notes Comput. Sci. 1987. - Vol. 279. - P. 336-369.

57. Arvind, Thomas R. I-structures: An efficient data type for functional languages. -Lab. Comput. Sci., MIT. Cambridge, Mass. Tech. Rep. TM-178, Sept. 1980.

58. Ashcroft E. A., Wadge W. W. Lucid, a nonprocedural language with iteration // Communication of ACM. 1977. - Vol. 20(7). - P. 519-526.

59. Aura Т., Lilius J. Time processes for time Petri nets // Lect. Notes Comput. Sci.1997. Vol. 1248. - P. 136-155.

60. Babb R. G., Ragsdale W. A large-grain data flow sheduler for parallel processing on CYBERPLUS // Proc. Internat. Conf. Paral. Process., Aug. 19-22, 1986. Washington, D.C., 1986. - P. 845-848.

61. Baier C., Katoen J.-P., Latella D. Metric semantics for true concurrent real time // Proc. 25th Internat. Colloquium, 1998. Aalborg, Denmark, 1998. - P. 568-579.

62. Bengtsson J., Jonsson В., Lilius J., Yi W. Partial order reductions for timed systems. // Proc. Inter. Conf. CONCUR, 1998. P. 485-496.64 65 [666768 69 [70 [71 [727374 75 [76 [77 [78 [79

63. Bergstra, J.A., Klop, J.W. A process algebra for the operational semantics of static data flow networks. CWI, Amsterdam. Tech. Rep. IW 222/83, 1983.

64. Berkowski F. J. A multiuser data flow architecture // Proc. 8th Ann. Sympos. Com-put. Archit., Minneapolis, May 1981. New York, 1981.

65. Berthomieu В., Diaz M. Modelling and verification of time dependent systems using time Petri nets // IEEE Transaction on Software Engineering. 1991. - Vol. 17, N 3. - P. 259-273.

66. Berthomieu В., Menasche M. A state enumeration approach for analyzing time Petri nets // Proc. 3th Europ. Workshop Applicat. and Theory of Petri Nets, 1982, P. 27-65.

67. Best E. The relative strength of K-density // Lect. Notes Comput. Sci. 1980. -Vol. 84. - P. 261-276.

68. Best E. A theorem on the characteristics of non-sequential processes // Fundamenta Informaticae. 1980. - Vol. 3. - P. 77-94.

69. E. Best. Partial order verification with PEP // Proc. POMIV'96, Princeton, P. 305328. Am. Math. Soc., 1996.

70. E. Best, R. Devillers, J.G. Hall. The box calculus: A new causal algebra with multi-label communication // Lect. Notes Comput. Sci. 1992. - Vol. 609. - P. 21-69.

71. Best E, Fernandez C, Pliinnecke H. Concurrent systems and processes. GMD, Sankt Augustin, FDR. Final Report on the Foundational Part of the Project BEGRUND. FMP-Studien, 107, 1985.

72. E. Best, H. Fleischhack, W. Fraczak, R.P. Hopkins, H. Klaudel, E. Pelz. A class of composable high level Petri nets // Lect. Notes Comput. Sci. 1995. Vol. 935. - P. 103-118.

73. E. Best, H. Fleischhack, W. Fraczak, R.P. Hopkins, H. Klaudel, E. Pelz. A M-net Semantics of B(PN)2 // Proc. STRICT Workshops in Computing, 1995, P. 85-100.

74. Best E., Grahlmann B. PEP — more than a Petri net tool // Lect. Notes Comput. Sci. 1996. - Vol. 1055. - P.397-401.

75. E. Best, R.P. Hopkins. B(PN)2 a basic Petri net programming notation // Lect. Notes Comput. Sci. - 1993. - Vol. 694. - P. 379-390.

76. B. Bieber, H. Fleischhack. Model checking of time Petri nets based on partial order semantics // Lect. Notes Comput. Sci. 1999. - Vol. 1662. - P. 211-225.

77. Boudol G., Castellani I. Permutation of transitions: an event structure semantics for CCS and SCCS // Lect. Notes Comput. Sci. 1988. - Vol. 354. - P. 411-427.

78. Boudol G., Castellani I. Three equivalent semantics for CCS // Lect. Notes Comput. Sci. 1990. - Vol. 469. - P.96-141.80 81 [8283 84 [85 [86 [8788

79. Boudol G., Castellani I. Concurrency and atomicity // Theoretical Computer Science. 1988. - Vol. 59. - P.25-84.

80. Boyer R.S., Moore J.S. Computation Logic Handbook. Academic Press. Perspectives in Computing, Vol. 23, 1988.

81. Browne M.C., Clarke E.M., Grumberg 0. Characterizing finite kripke structures in propositional temporal logic // Lect. Notes Comput. Sci. 1988. - Vol. 354. - P. 115-131.

82. Brock J. D. Operational semantics of a data flow language. Lab. Comput. Sci., MIT. Tech. Mem. TM-120, 1978.

83. Brock J.D., Ackerman W.B. Scenarios: a model of nondeterminate computation // Lect. Notes Comput. Sci. 1981. - Vol. 107. - P. 252-259.

84. Broy, M. Nondeterministic dataflow programs: how to avoid the merge anomaly // Science of Computer Programming. 1988. - Vol. 10. - P.65-85.

85. Burch J.R., Clarke E.M., McMillan L., Dill D., Hwang J. Symbolic model checking: Ю20 and beyond // Proc. 5th Symp. Logic in Comput. Sci, 1990, P. 428-439.

86. Caluwaerts L .J., DeBacker J., Peperstraete J. A data flow architecture with a paged memory system // Proc. 9th Ann. Sympos. Comput. Archit., Apr. 26-29, 1982. -Aug., Texas, 1982.

87. Caluwaerts L. J., DeBacker J., Peperstraete J. Implementing stream on a data flow computer system with paged memory // Proc, 10th Ann. Internat. Sympos. Comput. Archit., Stockholm, Sept. 1983. New York, 1983. - P. 76-83.

88. Campbell M. L. Static allocation for a dataflow multiprocessor // Proceedings of the Internat. Conf. Parall. Process., Aug. 20-23, 1985. Washington, 1985. - P. 511-517.

89. Carlson W. W., Fortes J. A. On the performance of combined data flow and control flow systems: Experiments using two iterative algorithms // J. Paral. Distrib. Comput. 1988. - Vol. 5(4). - P. 359-382.

90. R.T. Casley, R.F. Crew, J. Meseguer, V.R. Pratt. Temporal structures // Mathematical Structures in Computer Science. 1991. - Vol.l(2). - P. 79-213.

91. Castellani I. Bisimulations and abstraction homomorphisms // J. Comput. System Sci. 1987. - Vol. 34. - P. 210-235.

92. Castellani I., Zhang G.Q. Parallel product of event structures. Centre Sophia An-tipolis. Tech. Report N1078/INRIA, 1989.

93. A. Cherkasova, V. E. Kotov. Descriptive and analytical process algebras // Lect. Notes Comput. Sci. 1989. - Vol. 424. - P. 77-104.

94. Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic // Lect. Notes Comput Sci. 1981. - Vol. 131. - P. 52-71.

95. Clarke E.M., Emerson E.A., Sistla A.P. Automatic verification of finite-state concurrent systems using temporal logic specifications // JACM Trans. Programming Languages Systems. 1986. - Vol. 8(2). - P. 244-263.

96. Clarke E.M., Long D.E., Mc Millan K.L. Compositional model checking // Proc. 4th Symp. Logic in Comput. Sci, 1990, P. 353-362.

97. Clarke E., McMillan K., Campos S., Hartonas-Gramhausen V. Symbolic model checking // Lect. Notes Comput. Science. 1996. - Vol. 1102.

98. Cleaveland R., Hennessy M. Testing equivalence as a bisimulation equivalence // Lect. Notes Comput. Sci. 1989. - Vol. 407. - P. 11-23.

99. Cleaveland R., Zwarico A.E. A theory of testing for real-time. Proc. 6th Symp. Logic in Comput. Sci, 1991, P. 110-119.

100. Comte D., Hifdi N., Syre J. C. The data driven LAU multiprocessor system: Result and perspectives // Proc. IFIP Cong., Tokyo, Japan, Oct. 6-9, 1980. New York, 1980. - P. 175-180.

101. Cornish M. The TI data flow architectures: The power of concurrency for avionics // Proc. 3rd Conf. Digital Avionics Systems, Fort Worth, Tex., Nov. 1979. New York, 1979. - P. 19-25.

102. Culler D. E., Arvind. Resouce requirements of dataflow programs // Proc. 15th Ann. Internat. Sympos. on Comput. Archit. Honolulu, Hawaii, 1988.

103. Cerans K. Decidability of bisimulation equivalences for parallel timer processes // Lect. Notes Comput. Sci. 1993. Vol. 663. - P. 302-315.

104. Darondeau P., Degano P. Causal trees // Lect. Notes Comput. Sci. 1989. - Vol. 372. - P. 234-248.

105. Davis A. L. A data flow evaluation system based on the concept of recursive locality // Proc. Nat. Comput. Conf., New York, June 4-7, 1979. Arlington: AFIPS Press, 1979. - Vol. 48. - P. 1079-1086.

106. Davis A. L., Keller R. M. Data flow program graphs // Computer. 1982. - Vol. 15(2). - P. 26-41.

107. Dennis J.B. Data flow schemata // Lect. Notes Comput. Sci. 1972. - Vol. 5. - P. 187-216.

108. Dennis J. B. First version of a data flow procedure language // Lect. Notes Comput. Sci. 1974. - Vol. 19. - P. 362-376.

109. Dennis J. B. Data flow supercomputers // Computer. 1980. - Vol. 13(11). - P. 48-56.

110. Dennis J. В., Gao G. R. Maximum pipelining of array operations on static data flow machine // Proc. Conf. Parall. Process., 1983. P. 231-238.

111. Dennis J. В., Lim W. Y.-P., Ackerman W. B. The MIT data flow engineering model // Proc. IFIP World Computer Congr., Paris, France, Sept. 19-23, 1983.

112. Dezel J. Esparza J. Free-choice Petri nets. Cambridge Tracts in Theoretical Computer Science, 1994. - P. 553-560.

113. Emerson E.A. Temporal and modal logic // Handbook of Theoretical Computer Science. 1990. - Vol. B. - P. 995-1072.

114. Emerson E.A., Halpern J.Y. 'Sometimes' and 'Not Never' revisited: on branching versus linear time temporal logic // JACM. 1986. - Vol. 33(1). - P. 151-178.

115. Emerson E.A., Мок А.К., Sistla A.P., Srinivasan J. Quantitative temporal reasoning // Proc. 1st Ann. Workshop on Computer-Aided Verification, 1989.

116. Emersen E., Sistla A. Symmetry and model Checking // Lect. Notes Comput. Sci. 1993. - Vol. 697. - P. 463-478.

117. Engelfriet J. Branching processes of Petri nets // Acta Informatica. 1991. - Vol. 28. - P. 576-591.

118. Esparza J. Model checking using net unfoldings // Science of Computer Programming. 1994. - Vol. 23. - P. 151-195.

119. Esparza J., Roemer S., Vogler W. An improvement of McMillan's unfolding algorithm // Lect. Notes Comput. Sci. 1996. - Vol. 1055. - P. 87-106.

120. Faustini, A.A. An operational semantics for pure dataflow // Lect. Notes Comput. Sci. 1982 . - Vol. 140. - P. 212-224.

121. Feldbrugge F. Petri net tools overview 1992 // Lect. Notes Comput. Sci. 1993. -Vol. 674. - P. 169-209.

122. Fernandez C. Non-sequential processes // Lect. Notes Comput. Sci. 1986. - Vol. 254. - P. 95-116.

123. Fernandez J.-C., Mounier L. 'On the fly' verification of behavioral equivalences and preorders // Lect. Notes Comput. Sci. 1991. - Vol. 577. - P. 181-191.

124. Fernandez C., Thiagarajan P.S. D-continuous causal nets: A model of non-sequential processes // Theoret. Comput. Sci. 1984. - Vol. 28. - P. 171-196.

125. Fidge C. A constraint-oriented real-time process calculus // Formal Description Techniques V, IFIP Transactions. 1993. Vol. C-10. - P. 363-378.

126. Gajski D. D., Padua D. A. et al. A second opinion on data flow machines and languages // Computer. 1982. - Vol. 15(2). - P. 58-62.

127. Gaudiot J. L. Structure handing in data-flow system // IEEE Trans. Comput. -1986. Vol. 35(6). - P. 489-502.

128. Gaudiot J. L., Dubois M., et al. The TX16: highly programmable multi-microprocessor architecture // IEEE Micro. 1986. - Vol. 6. - P. 18-31.

129. Gaudiot J. L., Lee L. T. Multiprocessor systems programming in a high-level data flow language // Lect. Notes Comput. Sci. 1987. - Vol. 258. - P. 134-151.

130. Gaudiot J. L., Vedder R. W., et al. A distributed VLSI architecture for efficient signal and data processing // IEEE Trans. Comput. 1985. - Vol. 34. - P. 1072-1087.

131. C.Ghezzi, d. Mandrioli, S. Moraska, M. Pezze. A general way to put time in Petri nets // Proc. 5th Internat. Workshop on Software Specification and Design, Pittsburg, Pennsylvania, May 1989, P. 60-67.

132. Glauert J.R.W. High-level languages for dataflow computers. Pergamon-Infotech, 1982. State of the Art Report on Programming Technology.

133. Godefroid P. Partial-order methods for the verification of concurrent systems. An approach for state-explosion problem // Lect. Notes Comput. Sci. 1996. - Vol. 1032. - 143p.

134. Goltz U., Kuiper R., Penczek W. Propositional temporal logics and equivalences // Lect. Notes Comput. Sci. 1992. - Vol. 630. - P. 222-236.

135. Goltz U., Wehrheim H. Causal testing // Lect. Notes Comput. Sci. 1996. - Vol. 1113. - P. 394-406.

136. Goto A., Uchida S. Towards a high performance parallel inference machine: The intermediate stage plan of PIM // Lect. Notes Comput. Sci. 1987. - Vol. 272. - P. 299-320.

137. Grosh S., Bandyopadhyay S. et al. Study of a simulated stream machine for data flow com-putation // Perform. Eval. 1986. - Vol. 6(4). - P. 269-291.

138. Gurd J. R. The Manchester data flow machine // Future Comput. 1985. - Vol. 1(4). - P. 201-212.

139. Gurd J. R., Barahona P. M. С. C., Bohn A. P. W. et al. Fine grain parallel computing: The data flow approach // Lect. Notes Comput. Sci. 1987. - Vol. 272. -P. 82-152.

140. Halpern J., Moses Y. Knowledge and common knowledge in a distributed environment // J. ACM. 1990. - Vol. 37, N 3. - P. 549-587.

141. Hanisch H.-M. Analysis of timed Petri Nets by means of dynamic graphs // Petri Net Newletter. 1990. - N36. - P. 24-31.

142. Hartimo I., Kranlof K., Simula 0., Skytta J. DFSP: a data flow signal processor // IEEE Trans. Comput. 1986. - Vol. 35(1). - P. 23-33.

143. Hasegawa R., Amamiya M. Dataflow computing and eager and lazy evaluations // New Gener. Comput. 1985. - Vol. 2(2). - P. 105-130.

144. Heller S. K. An I-structure memory controlle. Master Th., Dept. of Electr. Engineer. Computer Sci., MIT. Cambridge, Mass., 1983.

145. Hennesy M., Milner R. Algebraic laws for nondeterminism and concurrency // JACM. 1985. - Vol. 32(1). - P. 137-161.

146. Henzinger T.A., Но P.H., Wong-Toi H. A Model checking for hybrid systems // Lect. Notes Comput. Sci. 1997. - Vol. 1254. - P. 220-231.

147. Henzinger T.A., Manna Z., Pnueli A. An interleaving model for real time // Proc. 5th Jerusalem Conference on Information Technology, 1990. P. 717-730.

148. Henzinger T.A., Manna Z., Pnueli A. Timed transition systems // Lect. Notes Comput. Sci. 1991. - Vol. 600. - P. 226-251.

149. Henzinger T.A. Half-order modal logic: how to prove real-time properties // Proc. 9th Annual Symposium on Principles of Distributed Computing. ACM Press, 1990. - P. 281-296.

150. Herath J., Saito N., et al. Dataflow models, languages, and machines for intelligence computations // IEEE Trans. Software Eng. 1988. - Vol. 14(12). - P. 1805-1828.

151. Herath J., Yuba Т., Saito N. Dataflow computing // Lect. Notes Comput. Sci. -1987. Vol. 269. - P. 25-36.

152. Hiraki K., Shimada Т., Hishida K. A hardware design of the SIGMA-1 a data flow computer for scientific computations // Proc. Internat. Conf. Parall. Process., 1984. - IEEE, 1984. - P. 524-531.

153. Hoare C.A.R. Communicating sequential processes. Prentice-Hall, London, 1985.

154. Hogenauer E. В., Newbold R. F. et al. DDSP a data flow computer for signal processing // Proc. Internat. Conf. Parall. Process. - New York, 1984.

155. Hoogers P.W., Kleijn H.C.M., Thiagarajan P.S. An event structure semantics for general Petri nets // Theor. Comput. Sci. 1996. - Vol. 153. - P. 129-170.

156. Howell R.R., Rosier L.E., Yen H.-C. A taxonomy of fairness and temporal logic problems for Petri nets // Lect. Notes Comput. Sci. 1988. - Vol. 324. - P. 351-359.

157. Hune Т., Nielsen M. Timed bisimulation and open maps // Lect. Notes Comput. Sci. 1998. - Vol. 1450. - P. 378-387.

158. Jaffe J. The use of queues in parallel dataflow evaluation of 'if-then-while' programs.- MIT, Laboratory for Computer Science. Tech. Rep. TM-104, May 1978.

159. Lamport L. The 'Hoare ligic' of concurrent programs // Acta Informatica. 1980.- Vol. 14. P. 21-37.

160. Janssen W., Poel M., Wu Q., Zwiers J. Layering of real-time distributed processes // Lect. Notes Comput. Sci. 1994. - Vol. 863. - P. 393-417.

161. Jensen K. Coloured Petri nets. Springer-Verlag. - Vol. 1,2. - 1996.

162. Jonsson, B.A. A fully abstract trace model for dataflow networks // Proc. POPL'89, 1989. P. 155-165.

163. Joyal A., Nielsen M., Winskel W. Bisimulation from open maps // Information and Computation. 1996. - Vol. 127(2). - P. 164-185.

164. Kahn G. The semantics of a simple language for parallel programming // Proc. Information Processing 74. North-Holland, 1977. - P. 993-998.

165. Katoen J.-P. Quatitative and Qualitative Extensions of Event Structures. PhD Thesis, Twente University. 1996.

166. Katoen J.-P., Langerak R., LatellaD., Brinksma E. On specifying real-time systems in a causality-based setting // Lect. Notes Comput. Sci. 1996. - Vol 1135. - P. 385-404.

167. Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs // Lect. Notes Comput. Sci. 1989. - Vol. 354. - P. 489 - 507.

168. Keller R. Formal verification of parallel programs // CACM 1976. - Vol. 19(7).- P. 371-384.

169. Keller R.M., Panangaden P. Semantics of networks containing indeterminate operators // Lect. Notes Comput. Sci. 1985. - Vol. 197. - P. 479-496.

170. Kis Т., Neuendorf K.-P. The benefit of waiting // Proc. CS&P'97, October 1997, Warsaw, Poland. 1997. - P. 93-104.

171. Kishi M., Yasuhara H., Kavamura Y. DDDP: a disrtibuted data driven processor // Proc. 10th Ann. Sympos. Comput. Archit., Stockholm, Sept., 1983. New York, 1983. - P. 236-242.

172. Kok, J.N. An iterative metric fully abstract semantics for nondeterministic dataflow // Lect. Notes Comput. Sci. 1989. - Vol. 379. - P. 321-330.

173. Koren I., Silberman G. M. A direct mapping of algorithms onto VLSI processor arrays based on the data flow approach // IEEE Trans. Comput. 1983. - Vol. 32(1). - P. 335-337.

174. Koymans R. Specifying real-time properties with metric temporal logic // Real-time Systems. 1990. - Vol. 2(4). - P. 255-299.

175. Kozen D. Results on propositional /x-Calculus // Theoretical Comput. Sci. 1983. - Vol. 27. - P. 333-354.

176. Kummer O., Stehr M.-O. Petri's axioms of concurrency A selection of recent results // Lect. Notes Comput. Sci. - 1997. - Vol. 1248. - P. 195-214.

177. Kung S.-Y. On supercomputing with systolic/wavefront array processors // Proc. IEEE. 1984. - Vol. 72, N 7.

178. Kung S.-Y. Lewis P. S., Lo S. C. Timing analysis and design optimization of VLSI dataflow arrays // Proc. ICPP'86. IEEE. Chicago, IL, 1986.

179. Kung S.-Y., Arun K. S., Rao D. V. B. Wavefront array processor: Language, architecture, and applications // IEEE Trans, on Comput. 1982. - Vol. 31(11). - P. 1054-1056.

180. Laroussenie F., Larsen K.G. CMC: a tool for compositional model checking of realtime systems // Proc. FORTE XI/PSTV XVIII, November 1998. Paris, France, 1998. - P. 439-456.

181. Laroussinie F., Larsen K.G., Weise C. From timed automata to logic and back // Lect. Notes Сотр. Sci. 1995. - Vol. 969. - P. 529-539.

182. Laroussinie F., Schnoebelen Ph. A hierarchy of temporal logics with past // Theor. Comput. Sci. 1995. - Vol. 148. - P. 303-324.

183. Larsen K.G., Pettersson P., Yi W. UPPAAL: status and developments // Lect. Notes Comput. Sci. 1997. - Vol. 1254. - P. 456-459.

184. Lilius J. Efficient state space search for time Petri nets // Proc. MFCS'98 Workshop on Concurrency, August 1998. Brno (Czech Republic), FIMU Report Series, FIMU RS-98-06, 1998. - P. 123-130.

185. Lodaya K., Thiagarajan P.S. A modal logic for a subclass of event structures. Automata, Languages and Programming // Lect. Notes Comput. Sci. 1987. - Vol. 267. - P. 290-303.

186. Loogen R., Goltz U. Modelling nondeterministic concurrent processes with event structures // Fundamenta Informaticae. 1991. - Vol. 14. - P. 39-73.

187. Lynch N., Star, W. A proof of the Kahn principle for input/output automata // Information and Computation. 1989. - Vol. 82(1). - P. 91-92.

188. Maggiolo-Schettini A., Winkowski J. Towards an algebra for timed behaviours // Theoretical Computer Science. 1992. - Vol. 103. - P. 335-363.

189. Marsan M.A. Stochastic Petri nets: elementary introduction // Lect. Notes Comput. Sci. 1989. - Vol. 424. - P. 1-29.

190. Marczynski R. W., Milewski J. A data driven system based on a microprogrammed processor module // Proc. 10th Ann. Sympos. Comput. Archit., Stockholm, Sept., 1983. New York, 1983. - P. 236-242.

191. Mazurkiewicz A. Basic notions of trace theory // Lect. Notes Comput. Sci. 1988. - Vol. 354. - P. 285-363.

192. McGraw J. R., Skedzielewski S., Allan S. et al. SISAL: Streams and interation in a single-assignment language: Language Reference Manual. Version 1.2, M-146. -Lawrence Livermore National Laboratory, Livermore, CA March, 1985.

193. McMilan K. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits // Lect. Notes Comput. Sci. 1992. - Vol. 663. - P. 164-177.

194. Meseguer J., Montanari U. Petri neTN are monoids // Information and Computation. 1990. - Vol. 88. - P. 105-154.

195. Meseguer J., Montanari U., Sassone V. Process versus unfolding semantics for Place/Transition Petri nets // Theor. Comput. Sci. 1996. - Vol. 153. - P. 171-210.

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

197. Milner R. A Calculus of communicating systems // Lect. Notes Comput. Sci. -1980. Vol. 92.

198. Milner R., Parrow J., Walker D. A Calculus of mobile processes. Parts I and II // Information and Computation. 1992. - Vol. 100.

199. Misunas D. P. A computer architecture for data flow computation. Lab. Comput. Sci., MIT. Cambridge, Mass. Tech. Rep. TM-100, 1978.

200. Montanari U., Corradini A., Heckel R. Tile Transition Systems as Structured Coal-gebras // Lect. Notes Comput. Sci. 1999. - Vol. 1684. - P. 13-38.

201. Moslemie A. Automated interpretation of S-invariants of predicate/transition nets: An application of non-classicall logics. Helsinki University of Technology, Digital Systems Laboratory. Tech. rep. N 15, 1991.

202. Mukund, M., Thiagarajan, P.S. An axiomatization of event structures // Lect. Notes Comput. Sci. 1989. - Vol. 405. - P. 143 - 160.

203. Mukund M., Thiagarajan P.S. A logical characterization of well branching event structures // Theor. Comput. Sci. 1992. - Vol. 96. - P. 35-72.

204. Murphy D. Testing, betting and timed true concurrency // Lect. Notes Comput. Sci. 1991. - Vol. 575. - P. 439-453.

205. Murphy D. Timed process algebra, Petri nets, and event refinement // Proc. 4th Refinement Workshop, Workshops in Computing. Springer Verlag, 1991. - P. 456478.

206. Murphy D. Time and duration in noninterleaving concurrency // Fundamenta In-formaticae. 1993. - Vol. 19. - P. 403-416.

207. Neuendorf K.-P., Kiritsis D., Kis Т., Xirouchakis P. Two-level Petri net modelling for integrated process and job shop production planning // Proc. workshop Manufc-turing and Petri Nets, 1997. P. 135-150.

208. Nicolin X., Sifakis J. An overview and synthesis on timed process algebras // Lect. Notes Comput. Sci. 1992. - Vol. 600. - P. 526-548.

209. Nielsen M., Cheng A. Observing behaviour categorically // Lect. Notes Comput. Sci. 1996. - Vol. 1026. - P. 263-278.

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

211. Nielsen, M. Rozenberg, G. Thiagarajan, P.S. Behavioural notions for elementary net systems // Distributed Computing. 1990. - Vol. 4, No. 1. - P. 45-57.

212. Nielsen M., Winskel G. Petri nets and bisimulation // Theoret. Comput. Sci. -1996. Vol. 153.

213. Oldehoeft A.E. Allan S., et.al. Translation of high level programs to data flow and their execution on a feedback interpreter. Dep. Сотр. Sci., Iowa State Univ. Tech. Rep. TR-87-2, 1978.

214. Ostroff J.S. Temporal logic of real-time systems. Research Studies Press, 1990.

215. Panangaden P., Stark E.W. Computations, residuals, and the power of indeterminacy // Lect. Notes Comput. Sci. 1988. - Vol. 317. - P. 439-454.

216. Park D. Concurrency and automata on infinite sequences // Lect. Notes Comput. Sci. 1981. - Vol. 104. - P. 167-183.

217. Park D. The 'fairness problem' and nondeterministic computing networks // Foundations of Computer Science IV. 1983. - Part 2. - Mathematical Centre Tracts 159. - P. 133-161.

218. Patnaik L. M., Govindarajan R., Ramadoss N. S. Design and performance evaluation of EXMAN: An Extended Manchester Data Flow Computer // IEEE Trans. Comput. 1986. - Vol. 35, N. 3. - P. 229-244.

219. Peleg D. Concurrent dynamic logic // J. ACM. 1987. - Vol. 34, N 2. - P. 450-479.

220. Penczek W. A temporal logic for the local specification of concurrent systems // Proc. Information Processing 89. North-Holland, Amsterdam, 1989. - P. 857-862.

221. Penczek W. Partial order reductions for checking branching properties of time Petri nets // Proc. CS&P'2000, October 2000, Berlin, Germany. P. 189-202.

222. Petri, C. Concurrency as a basis for system thinking. St. Augustin: Gesellschaft fur Mathematik und Detenverarbeitung. ISP-Rep. N 78.06, 1978.

223. C. Petri. Concurrency // Lect. Notes Comput. Sci. 1980. - Vol. 84. - P. 261-276.

224. Pinchinat, S., Laroussinie, F., Schnoebelen, PH. Logical characterization of truly concurrent bisimulation. Research Report RT 114, IMAG-23, LIFIA, Grenoble, 1994.

225. H. Pliinnecke. K-density, N-density and fmiteness properties // Lect. Notes Comput. Sci. 1984. - Vol. 188. - P. 392-412.

226. Pnueli A., Harel E. Application of temporal logic to the specification of real-time systems // Lect. Notes Comput. Sci. 1988. - Vol. 331. - P. 84-98.

227. Pratt V.R. The pomset model of parallel processes: unifying the temporal and the spatial // Lect. Notes Comput. Sci. 1985. - Vol. 197. - P. 180-196.

228. Preiss B. R., Hamacher V. C. Data flow on a queue machine // Proc. 12th Ann. Internat. Sympos. Comput. Archit., Boston, June 17-19, 1985. Silver Spring, Md, 1985. - P. 342-351.

229. Rabinovich A. Pomset semantics is consistent with data flow semantics // Bulletin of EATCS. 1987. - Vol. 32.

230. Rabinovich A., Trakhtenbrot B.A. Behaviour structures and nets // Fundamenta Informatica. 1988. - Vol. 11, N 4.

231. Rabinovich A., Trakhtenbrot B.A. Nets of processes and data flow // Lect. Notes Comput. Sci. 1988. - Vol. 354. - P. 574-602.

232. Ramchandani C. Analysis of asynchronous concurrent systems by timed Petri nets // PhD Thesis. Cambridge, Mass.: MIT, Dept. Electrical Engineering, 1974.

233. Requa J. E. The piecewise data flow architecture control flow and register management // Proc. 10th Ann. Internat. Sympos. Comput. Archit., Stockholm, Sept., 1983. New York, 1983. - P. 84-89.

234. Rokey M. The data flow architecture: A suitable base for the implementation of expert systems // SIGARCH Comput. Archit. News. 1985. - Vol. 13, N. 4. - P. 8-14.

235. Roux J.-L., Berthomieu B. Verification of local area network protocol with Tine, a software package for time Petri nets // Proc. 7th Europ. Workshop on Application and Theory of Petri Nets, 1986. P. 183-205.

236. Rumbaugh J. A parallel asynchronous computer architecture for data flow programs. MIT, Project MAC. Tech. Rep. TR-150, May 1975.

237. Rumbaugh J. A data flow multiprocessor // IEEE Trans. Comput. 1977. - Vol. 26, N. 2. - P. 138-146.

238. Sassone V. On the category of Petri Net Computations // Lect. Notes Comput. Sci.- 1995. Vol. 915. - P. 334-348.

239. Schneider S., Davies J., Jackson D.M., Reed G.M., Reed J.M., Roscoe A.W. Timed CSP: theory and practice // Lect. Notes Comput. Sci. 1991. - Vol. 600. - P. 640-675.

240. Sifakis J. Performance evaluation of systems using nets // Lect. Notes Comput. Sci.- 1981. Vol. 84. - P. 307-320.

241. Sinachopoulos, A. Partial order logics for elementary net systems: state- and event Approaches // Lect. Notes Comput. Sci. 1990. - Vol. 458.

242. Sowa M. A method for speeding up serial processing in dataflow computers by means of a program counter // Computer J. 1987. - Vol. 30, N. 4. - P. 289-294.

243. Sowa M., Murata T. A data flow computer architecture with program and token memories // IEEE Trans. Comput. 1982. - Vol. 31, N. 9. - P. 820-824.

244. Srini V. P. A fault-tolerant data flow system // Computer. 1985. - Vol. 18, N. 3.- P. 54-68.

245. Srini V. P. An architectural comparison of data flow systems // Computer. 1986.- Vol. 19, N. 3. P. 68-88.

246. Staples, J.-Nguyen, V.L. A fixpoint semantics for nondeterministic dataflow // Journal of the ACM. 1985. - Vol. 32, N 2. - P. 411-445.

247. Some properties of timed nets under the earliest firing time // Lect. Notes Comput. Sci. 1990. - Vol. 424 . - P. 418-432.

248. Starke P. INA: Integrated net analyzer. Handbuch, 1992.

249. Steffen В., Weise C. Deciding testing equivalence for real-time processes with dense time // Lect. Notes Comput. Sci. 1993. - Vol. 711. - P. 703-713.

250. Storrle H. Tool comparison, to be published, 1998.

251. Takahashi N., Amamiya M. A data flow processor array system: Design and analysis // Proc. 10th Ann. Internat. Sympos. Comput. Archit., Stockholm, Sept., 1983. -New York, 1983. P. 243-250.

252. Thiagarajan P.S. Elementary net systems. Lect. Notes Comput. Sci. 1987. - Vol. 254. - P. 26-59.

253. Thiagarajan P.S. A Trace based extension of linear time temporal logic // Proc. 9th Symp. Logic in Comput. Sci, 1994, P. 438-447.

254. Trompedeller M. Petri net tools, 1993. Last update: 1995, www.dsi.unimi.it/Users/Tesi/trompede / petri/alfa.html.

255. Tuominen H. Logic in Petri net analysis. Helsinki Univ. of Technology, Digital Systems Laboratory. Tech. rep. N 5, 1988.

256. Vaandrager F.W. Determinism (event structure isomorphism = step sequence equivalence) // Theor. Comput. Sci. 1991. - Vol. 79(2). - P. 275-294.

257. Valero V., de Frutos D., Cuartero F. Timed processes of timed Petri nets // Lect. Notes Comput. Sci. 1995. - Vol. 935. - P. 490-509.

258. Valmari A. A stubborn attack on state explosion // Lect. Notes Comput. Sci. -1990. Vol. 535.

259. Varpaaniemi K., Halme J., Hiekkanen K., Pyssysalo T. PROD Reference Manual. University of Helsinki. Technical Report В 13, 1995.

260. Veen, A.H. A formal model for data flow programs with token coloring. CWI, Amsterdam. Tech. Rep. IW 179, 1981.

261. Veen A.H. Reconciling data flow machines and conventional languages // Lect. Notes Comput. Sci. 1981. - Vol. 111. - P. 127-140.

262. Veen A. H. The misconstructed semicolon. Reconciling imperative languages and data flow machines // Proefschrift grad doct. techn. werenschappen, Techn. Hogesch, Eindhoven, 1985.

263. Veen A.H. Dataflow machine archetecture // ACM Computing Survey. 1986. -Vol. 18, N 4. - P. 365-396.

264. Virbitskaite I.B. Investigating dataflow networks with token colouring // Methods of Theoretical and Experimental Computer Science. Novosibirsk, 1989. - P. 142157.

265. Virbitskaite I.B. Behavioral notions for eager data flow computing with I-structures // Current Topics in Informatics Systems Research. Novosibirsk, 1991. - P. 81-92.

266. Virbitskaite I. Observing some properties of event structures // Lect. Notes Comput. Sci. 1993. - Vol. 735. - P. 229-250.

267. Virbitskaite I. Some characteristics of nondeterministic processes // Parallel Processing Letters. 1993. - Vol. 3, N 1. - P. 99-106.

268. Virbitskaite I. The relative strength of density and crossing properties for event structures // Proc. Internat. Conf. Young Computer Scientists. Bei jing, China, 1993. - P. 547-552.

269. Virbitskaite I. On the semantics of concurrency and nondeterminism: bisimulations and temporal logics // Electronic Notes in Theoretical Computer Science. 1998. -Vol. 18.

270. Virbitskaite I. An event structure model for dataflow computing // Computers and Artificial Intelligence. 1999. - Vol. 18, N 1. - P. 73-93.

271. I.B. Virbitskaite. A verification method for timed concurrent systems using timing zones // Proc. Internat. Conf. on Concurrency, Specification and Programming. -Berlin: Humbold University, 2000. P. 323-334.

272. I.B. Virbitskaite. Characterizing time net processes categorically // Lect. Notes Сотр. Sci. 2001. - Vol. 2127. - P. 128-141.

273. I.B. Virbitskaite. An observation semantics for timed event structures // Lect. Notes Comput. Sci. 2001. - Vol. 2244. - P. 215-225.

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

275. Virbitskaite I.B., Bystrov A.V. Implementing model checking and equivalence checking for time Petri nets by the RT-MEC tool // Lect. Notes Comput. Sci. -1999. Vol. 1662. - P. 194-200.

276. Virbitskaite I.B., Pokozy E.A. A partial order algorithm for verifying time Petri nets // Proc. Internat. Workshop on Discr. Event Systems, August 1998, Cagliari, Italy. IEE Publisher, London, 1998. - P. 514-517.

277. Virbitskaite I.В., Pokozy E.A. Towards efficient verification of time Petri nets // Logical Journal of IGPL. Oxford University Press, 1997. - Vol. 5(6). - P. 921-924.

278. Virbitskaite I.B., Pokozy E.A. A partial order algorithm for verifying time Petri nets // Proc. Internat. Workshop on Discr. Event Systems, August 1998, Cagliari, Italy. IEE Publisher, London, 1998. - P. 514-516.

279. Virbitskaite I.B., Pokozy E.A. Parametric behaviour analysis for time Petri nets // Lect. Notes Comput. Sci. 1999. - Vol. 1662. - P 134-140.

280. Virbitskaite I.B., Pokozy E.A. A partial order method for the verification of time Petri nets // Lect. Notes Comput. Sci. 1999. - Vol. 1684. - P. 547-558.

281. Virbitskaite I., Votintseva A. Notes on logical characterization of density concepts // Specification, Verification and Net Models of Concurrent Systems. IIS, Novosibirsk. - 1994. - P. 20-34.

282. Virbitskaite I., Votintseva A. Partial order logics and equivalences for event structures // Proc. 15th IMACS World Congress on Scientific Computation, Modelling and Applied Mathematics. 1997. - Vol.5. - P. 505-510.

283. Virbitskaite I., Votintseva A. Behavioural characterizations of partial order logics // Lect. Notes Comput. Sci. 1997. - Vol. 1279. - P. 463-474.

284. Vogler W. Modular construction and partial order semantics of Petri nets // Lect. Notes Comput. Sci. 1992. - Vol. 625. - 252 P.

285. Wadge W. W., Ashcroft E. et al. Lucid, the dataflow programming language. -Academ. Press., 1985. 312p.

286. Walter B. Timed Petri Nets for modelling and Analyzing Protocols with real-time characteristics // Protocol Specification, Testing and Verification III. Elsevier Science Publ. - 1983. - P. 149-159.

287. Wang F. Timing behavior analysis for real-time systems // Proc. 10th Symp. Logic in Comput. Sci, 1995, P. 112-122.

288. Weise C., Lenzkes D. Efficient scaling-invariant checking of timed bisimulation // Lect. Notes Comput. Sci. 1997. - Vol. 1200. - P. 176-188.

289. Weng K.-S. An abstract implementation for a generalized data flow language. -Lab. Сотр. Sci., MIT, Cambridge, Mass. Tech. Rep. TR-228, 1979.

290. Whitelock P.J. A conventional language for data flow computing // M.Sc. Dissertation. Dep. Сотр. Sci., Univ. Manchester, Oct. 1978.

291. D. Wikarski Petri net tools a comparative study. - TU Berlin. Tech. Rep. N 97-4, 1997.

292. Winkowski J. Event structure representation of the behaviour of place/transition systems // Fundamenta Informatica. 1988. - Vol. 11. - P. 405-432.

293. Winskel G. Petri nets, algebras, morphisms, compositionality // Information and Computation. 1987. - Vol. 72. - P. 197-238.

294. Winskel G. An introduction to event structures // Lect. Notes Comput. Sci. 1988.- Vol. 354. P. 364-397.

295. Winskel G., Nielsen M. Models for concurrency // Handbook of Logic in Comput. Sci. 1995. - Vol. 4.

296. Yamaguchi Y., Toda K., Yuba T. A performance evaluation of a Lisp-based data-driven machine (EM-3) // Proc. 10th Ann. Internat. Sympos. Comput. Archit., Stockholm, Sept., 1983. New York, 1983. - P. 363-369.

297. Yetes R.K, Gao G.R. A Kahn principle of networks of nonmonotonic real-time processes // Lect. Notes Comput. Sci. 1993. - Vol. 694. - P. 209-227.

298. Yoneda Т., Shibayama A., Schlingloff B.H., Clarke E.M. Efficient verification of parallel real-time systems // Lect. Notes Comput. Sci. 1993. - Vol. 697. - P. 321333.

299. Yoneda Т., Ryuba H. CTL model checking of time Petri nets using geometric regions // IEE Trans. Inf. and Syst. 1998. - Vol. 3. - P. 305-332.

300. Yuba T. Reseach and development efforts on data-flow computer architecture in Japan // J. Inform. Process. 1986. - Vol. 9, N. 2. - P. 51-62.

301. Yuba Т., Kashiwagi H. The Japanese national projects for new generation computing systems. Techn. Rep. ETL-RM-86-1.

302. Zuberek W.M. Timed Petri nets and preliminary performance evaluation // Proc. 7th Annual Symp. on Сотр. Archit., 1980, P. 88-96.