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

• Дубцов, Роман Сергеевич
• кандидат физико-математических наук
• 2008

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

Введение.

1 Известные результаты

1.1 Элементы теории категорий.

1.2 Области Скотта.

1.3 Структуры событий

1.4 Системы переходов с независимостью

1.5 Сети-процессы и сети Петри.

2 Семантика помеченных областей временных структур событий

2.1 Категория помеченных областей Скотта.

2.2 Категории временных структур событий

2.3 Взаимосвязи категорий временных структур событий и помеченных областей

2.4 Выводы.

3 Семантика помеченных областей временных систем переходов с независимостью.

3.1 Категории временных систем переходов с независимостью

3.2 Развертка временных систем переходов с независимостью

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

3.4 Выводы.

4 Семантика помеченных областей временных сетевых моделей

4.1 Категории временных сетей-процессов.

4.2 Свойства категорий временных сетей-процессов

4.3 Взаимосвязи категорий временных сетей-процессов и помеченных областей

4.4 Категория временных сетей Петри

4.5 Взаимосвязи категорий временных сетей Петри и помеченных областей

4.6 Выводы.

Введение диссертации (часть автореферата) на тему «Теоретико-категорное исследование семантики областей Скотта параллельных моделей с реальным временем»

Актуальность. В настоящее время сфера применения аппаратных и программных систем с параллельной/распределенной архитектурой непрерывно расширяется, охватывая все новые области в самых различных отраслях науки, техники, образования, бизнеса и производства. К таким системам относятся коммуникационные протоколы, системы управления производством, распределенные операционные системы, параллельные базы данных и т.д. Параллельные/распределенные системы, как правило, состоят из большого числа компонентов со сложным характером взаимодействий, что затрудняет понимание природы протекающих в них разнообразных процессов. Проектирование и реализация корректных параллельных/распределенных систем возможны только при использовании формальных методов н средств, которые должны быть, с одной стороны, «дружественными» для разработчиков, а с другой - математически строгими, а также адекватно представлять структуру и поведение 'моделируемых систем.

Среди отечественных исследований по спецификации, моделированию и анализу сложных (в том числе, параллельных/распределенных) систем отметим работы Н.А. Аннсимова, O.JI. Бандман, И.Б. Вирбиц-кайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.Э. Малышкина, В.А. Непомнящего, А.К. Петренко, P.JI. Смелянского, В.А. Соколова, JI.A. Черкасовой.

Теория параллельных систем и процессов — активно развивающаяся область компьютерных наук - изучает фундаментальные понятия и законы параллельной обработки информации и на основе обнаруженных закономерностей строит более частные формальные модели исследуемых объектов, на которых ставит и решает прикладные задачи. На основе результатов и рекомендаций теоретических исследований ведется поиск и проверка новых архитектурных принципов конструирования систем, изучаются методы распараллеливания алгоритмов и программ, разрабатываются новые конструкции параллельных языков программирования, проверяются способы анализа и верификации программных систем и т.д. За последние четыре десятилетия в теории параллелизма появилось большое разнообразие моделей и методов, предназначенных для спецификации, разработки и верификации систем. Среди формальных структурных моделей следует отметить сети Петри, системы переходов, системы переходов с независимостью, автоматы высших порядков, I/O-автоматы и т.д. Особое внимание в теории параллелизма отводится абстрактным семантическим моделям, позволяющим описывать и исследовать поведения параллельных систем. К таким моделям относятся деревья синхронизации, причинные деревья, структуры событий и т.д. Известно, что денотационная семантика и теория областей Скотта активно используются как математический базис для описания семантики последовательных программ, установления взаимосвязей между языками программирования, исследования типов данных языков программирования. Примененимость таких абстрактных методов к моделям параллельных систем и процессов всегда вызывало некоторый скептицизм. Однако в работах Винскеля было показано, что модели областей Скотта адекватно и полностью представляют семантику известных моделей параллелизма.

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

В последнее десятилетие резко возрос интерес к разработке и исследованию параллельных систем, поведение которых в значительной степени зависит от количественных временных характеристик, — параллельных систем реального времени. Для таких систем важны как модели вычислений, так и модели времени. В литературе параллельные системы реального времени часто представляются временными автоматами [13], временными системами переходов [46] и алгебрами временных процессов (см., например, [81]). Однако все эти формализмы базируются на интерливннговой семантике и не позволяют моделировать параллелизм естественным образом (напрямую). К временным моделям с семантикой «истинного параллелизма» относятся временные расширения моделей структур событий [15, 34, 42, 52, 63], сетей-процессов [17, 82], сетей Петри [8, 58, 74], причинных деревьев [37], частично-упорядоченных множеств [55, 80], систем конфигураций [56], асинхронных систем переходов [10]. Перечисленные выше временные модели могут быть классифицированы относительно семи дихотомий: дискретное/непрерывное время. В дискретных моделях (см., например, [74, 82]) время задается целыми числами. Такой подход обычно используется для описания систем с общим глобальным счетчиком времени. Время делится на счетное количество тактов: п + 1-й такт начинается в га-ый момент времени и заканчивается в п + 1-ый. Дальнейшее разбиение времени внутри тактов не предусматривается. В непрерывных моделях [37, 52, 56, 58, 63] время измеряется по непрерывной временной шкале и возможно неограниченное число событий при переходе системы из одного состояния в другое; абсолютное/относительное время. В процессе функционирования системы временные характеристики связываются либо с началом ее функционирования (абсолютное время) [42, 52], либо отсчитывают-ся от конца предыдущего действия системы (относительное время) [58]; явное/неявное понятие прохождения времени. Известно, что временная система функционирует двумя способами: посредством выполнения действия и посредством прохождения некоторого времени. Эти два понятия становятся ортогональными при явном введении понятия прохождения времени. Такой подход рассмотрен в [56], а альтернативный — в [10, 52, 58, 63]; задержанные/мгновенные действия. В моделях, описанных в [10, 55, 63, 74], задержка действия смоделирована как временной промежуток между началом выполнения действия и его окончанием. При втором подходе выполнение действия само не требует времени, но, как правило, может быть отложено на определенный срок [37, 52, 56, 58]; с/без локальных часов. Использование локальных часов [10, 17, 58] позволяет описывать эволюцию различных частей распределенных систем. Иначе говоря, каждое событие имеет свой таймер задержки, который начинает отсчитывать время с того момента, когда событие становится активным, и останавливается, когда событие становится пассивным. Такой подход позволяет достаточно легко изучать поведение системы локально. С другой стороны, как было продемонстрировано в [52], операционная семантика алгебр временных процессов может быть описана проще, если не использовать локальные часы; несогласованные/согласованные по времени трассы. В несогласованных по времени трассах предшествование событий не отражает их временного порядка, поэтому во многих работах такой подход не используется (см., например, [58, 82]). Однако, как сообщалось в статьях [10, 52], несогласованные по времени трассы позволяют построить семантику 'истинного параллелизма' для временных ин-терливинговых алгебр процессов, т.е. установить связи между 'истинным параллелизмом' и интерливингом; срочные У'несрочные' действия. Понятие 'срочного' действия подразумевает, что действие должно быть выполнено сразу, как только оно готово, т.е. все его предшественники выполнились и его временные ограничения также выполнены (см. [10, 56, 58]). Однако иногда требование 'срочного' выполнения временных действия является слишком жестким. Один из способов решения этой проблемы — добавление 'несрочных' действий. Например, в работе [52] были использованы оба вида действий.

За последние пять лет были хорошо изучены взаимосвязи между временными сетями Петри и временными автоматами [77]. Однако известно не так много результатов по сравнительному анализу других временных параллельных моделей. Причем работы с использованием теоретико-ка-тегорных методов, на сколько нам известно, совсем отсутсвуют. Кроме того, следует отметить, что семантика «истинного параллелизма» моделей с реальным временем также недостаточна изучена в литературе.

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

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

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

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

2. построение и исследование абстрактной семантики временных параллельных моделей в терминах областей Скотта;

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

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

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

Разработаны временные расширения моделей с семантикой «истинного параллелизма» — временные первичные/расслоенные/стабильные структуры событий, а также временные системы переходов с независимостью.

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

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

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

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

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

XLI Международная научная студентческая конференция «Студент и научно-технический прогресс» (Россия, Новосибирск, 2003);

Международная научно-практическая конференция по прорамми-рованию УкрПРОГ'2004 (Украина, Киев, 2004);

International Conference on Parallel Computing Technologies PaCT'2005 (Krasnoyarsk, Russia, 2005);

International Andrei Ershov Memorial Conference on Perspectives of System Informatics oil (Novosibirsk, Russia, 2006);

15th International Workshop «Concurrency, Specification and Programming» (Vandlidz, Germany, 2006);

IX всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (Россия, Кемерово, 2008);

17th International Workshop «Concurrency, Specification and Programming» (Gross Vaeter See, Germany, 2008).

Кроме того, доклады по теме работы были сделаны на ряде семинаров Института систем информатики СО РАН (г. Новосибирск) и кафедр Новосибирского государственного университета.

Публикации. По теме диссертации опубликовано 9 научных работ, в том числе 1 — в изданиях, рекоммендуемых ВАК, 1 — в научном журнале, 6 — в трудах международных и отечественных конференций и семинаров.

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

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

4.6 Выводы

В данной главе были изучены временные расширения сетевых моделей — временные сети-процессы и временные сети Петри. Для данных расширений были получены следующие результаты. Построены категории ТРгосе и TProci временных сетей-процессов с «энергичной» и «ленивой» семантиками соответственно. Выделена полная подкатегория ТРгос, для объектов которой данные семантики совпадают. е3 : 1

TPN" Рис. 4.5.

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

Установлено существование корефлексии между категорией ТРгос и категорией TPES временных первичных структур событий.

Построена развертка временных сетей Петри во временные сети-процессы и дана ее теоретико-категорная характеризация.

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

Заключение

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

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

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

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

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

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

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

2. Вирбицкайте И. Б., Дубцов Р. С. Семантические области временных структур событий // Программирование. — 2008. — Т. 3. — С. 119.

3. Дубцов Р. С. Критерии эпи- и мономорфизма в категориях моделей с реальным временем. — Новосибирск, 2004. — 23 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; №113).

4. Дубцов Р. С. Теоретико-категорная характеризация развертки временных сетей петри // Труды международной конференции Укр-Прог'04. — Т. 2-3 из Проблемы программирования. — Киев: 2004. — С. 30-36.

5. Дубцов Р. С. Теоретико-категорные исследования систем переходов с независимостью // Материалы IX Всероссийской конференции молодых ученых по математическому моделированию и информационных технологий. — Кемерово: 2008. — С. 78.

6. Дубцов, Р. С. Исследование свойств категорий параллельных процессов с реальными временем // Материалы XLI международной научной конференции «Студент и научно-технический прогресс».— Новосибирск: 2003. — С. 109.

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

8. A General Way То Put Time in Petri Nets / C. Ghezzi, D. Mandrioli, S. Morasca, M. Pezze // 5th Int. Workshop on Software Specification and Design. — 1989. — May. — Pp. 60-67.

9. Aceto L., De Nicola R., Fantechi A. Testing equivalences for event structures // Lecture Notes in Computer Science. — 1987. — Vol. 280. — Pp. 1-20.

10. Aceto L., Murphy D. Timing and Causality in Process Algebra // Acta Informatica. — 1996. — Vol. 33, no. 4. Pp. 317-350.

11. Alur R., Courcoubetis C., Dill D. Modcl-checking in dense real-time // Information and Computation. — 1993. — Vol. 104, no. 1. — Pp. 2-34.

12. Alur R., Courcoubetis C., Henzmger T. The observational power of clocks // Lccture Notes in Computer Science. — 1994. — Vol. 836. — Pp. 162-177.

13. Alur R., Dill D. A Theory of Timed Automata // Theoretical Computer Science. 1994. - Vol. 126, no. 2. - Pp. 183-235.

14. Andreeva M. V., Bozhenkova E. N., Virbitskaite I. B. Analysis of timed concurrent models based on testing equivalence // Fundament a Informaticae. — 2000. — Vol. 43, no. 1-4. — Pp. 1-20.

15. Andreeva M. V., Virbitskaite I. B. Timed Equivalences for Timed Event Structures // Lecture Notes in Computer Science. — 2005. — Vol. 3606. — Pp. 16-25.

16. Andreeva M. V., Virbitskaite I. B. Observational Equivalences for Timed Stable Event Structures j j Fundamenta Informaticae. — 2006. — Vol. 72, no. 1. —Pp. 1-19.

17. Aura Т., Lilius J. Time processes for time petri-nets. // Lecture Notes in Computer Science. — 1997. — Vol. 1248. — Pp. 136-155.

18. Bednarczyk M. Categories of asynchronous systems: Ph.D. thesis / University of Sussex, UIC. — 1987.

19. Berthornieu В., Diaz M. Modelling and verification of Time dependent systems using time Petri Nets // IEEE Transactions on Soft,ware Engineering. — 1991. — Vol. 17, no. 3. — Pp. 259-273.

20. Borceux F. Handbook of Categorical Algebra 1: Basic Category Theory. — Cambridge University Press, 1994.

21. Boudol G., Castellani I. Concurrency and atomicity // Theoretical Computer Science. — 1988. — Vol. 59, no. 1-2. — Pp. 25-84.

22. Bouyer P., Haddad S., Reynier P. Extended Timed Automata and Time Petri Nets // Proc. of the 6t,h Intl. Conf. on Application of Concurrency to System Design. — 2006. — Pp. 91-100.

23. Bouyer P., Haddad S., Reynier P. Timed Unfoldings for Networks of Timed Automata // Lecture Notes in Computer Science. — 2006. — Vol. 4218. Pp. 292-306.

24. Cattani G., Sassone V. Higher dimensional transition systems // Logic in Computer Science, 1996. LICS'96. Proceedings., Eleventh Annual IEEE Symposium on. — 1996. — Pp. 55-62.

25. Cerans K. Decidability of Bisimulation Equivalences for Parallel Timer Processes // Lecture Notes in Computer Science. — 1993. — Vol. 663.— Pp. 302-315.

26. Chatain Т., Jard C. Time supervision of concurrent systems using symbolic unfoldings of time petri nets. // Lecture Notes in Computer Science. 2005. — Vol. 3829. — Pp. 196-210.

27. Cheng A., Nielsen M. Open maps (at) work // Research Series RS-95-23, BRICS, Department of Computer Science, University of Aarhus, April. — 1995.

28. Cleaveland R., Zwarico A. A theory of testing for real-time // Lecture Notes in Computer Science.— 1991. — Vol. 663. — Pp. 110-119.

29. Darondeau P., Degano P. Event Structures, Causal Trees, and Refinements // Lecture Notes in Computer Science.— 1990.— Vol. 452. — Pp. 239-245.

30. De Nicola R., Hennessy M. Testing equivalence for processes // Theoretical Computer Science. — 1984. — Vol. 34. — Pp. 83-133.

31. Degano P., Gorrieri R., Vigna S. On Relating Some Models for Concurrency // Lecture Notes in Computer Science.— 1993.— Vol. 668. Pp. 15-30.

32. Dubtsov R. S. Real-time event structures and scott domains // Lecture Notes in Computer Science. — 2005. — Vol. 3606. — Pp. 42-48.

33. Dubtsov R. S. Semantic domains for real-time event structures // Proceedings of the International Workshop on Concurrency, Specification and Programming. — 2006. — Pp. 186-194.

34. Dubtsov R. S. Real-Time Stable Event Structures and Marked Scott Domains: An Adjunction // Lecture Notes in Computer Science. — 2007. Vol. 4378. - Pp. 443-450.

35. Dubtsov R. S., Virbitskaite I. B. A Comparative Account of Timed Event Structures. // Proc. of 17th International Workshop «Concurrency, Specification and Programming».— Gross Vaeter See (Germany): 2008. Pp. 500-511.

36. Engelfriet J. Branching processes of Petri nets // Acta Informatica. — 1991. — Vol. 28, no. 6. Pp. 575-591.

37. Fidge C. A constraint-oriented real-time process calculus. // FORTE. — Vol. C-10 of IFIP Transactions. 1992. — Pp. 363-378.

38. Goltz U., Gotz N. Modelling a simple communication protocol in a language with action refinement // Draft version. — 1991.

39. Goltz U., Wehrheim H. Causal Testing // Lecture Notes in Computer Science. 1996. - Vol. 1113. — Pp. 394-406.

40. Goubault E. Domains of Higher-Dimensional Automata // Proceedings of the 4th International Conference on Concurrency Theory.— 1993.— Pp. 293 307.

41. Goubault E., Jensen T. Homology of Higher Dimensional Automata // International Conference on Concurrency Theory. — 1992. — Pp. 254268.

42. Gribovskaya N., Virbitskaite I. Open Maps and Observational Equivalences for Timed Partial Order Models / / Fundamenta Informaticae. — 2004. — Vol. 60, no. 1. — Pp. 383-399.

43. Hennessy M. Algebraic theory of processes. Series in the Foundations of Computing. MIT Press, 1988.

44. Hennessy M., Cleaveland R. Testing equivalence as bisimulation equivalence // Lecture Notes in Computer Science.— 1989.— Vol. 407. Pp. 11-23.

45. Hennessy M., Milner R. Algebraic laws for nondeterminism and concurrency // Journal of the ACM (JACM). — 1985. — Vol. 32, no. 1. — Pp. 137 161.

46. Henzinger Т., Pnucli A., Manna Z. Timed Transition Systems // Lecture Notes in Computer Science. — 1992. — Vol. 600. — Pp. 226-251.

47. Hildebrandt Т., Sassone V. Comparing Transition Systems with Independence and Asynchronous Transition Systems // International Conference on Concurrency Theory. — 1996. — Pp. 84-97.

48. Hoare C. Communicating Sequential Processes. Series in Computer Science. — Prentice-Hall International, 1985.

49. Hoogers P., Kleijn H., Thiagarajan P. An event structure semantics for general Petri nets // Theoretical Computer Science. — 1996. — Vol. 153, no. 1-2. Pp. 129-170.

50. Hune Т., Nielsen M. Timed bisimulation and open maps // Lecture Notes in Computer Science. — 1998. — Vol. 1450. — Pp. 378-387.

51. Joyal A., Nielsen M., Winskel G. Bisimulation from open maps // Information and Computation. — 1996. — Vol. 127, no. 2. — Pp. 164185.

52. Katoen J. Quantitative and Qualitative Extensions of Event Structures: Ph.D. thesis / University of Twente. — 1996.

53. Maggiolo-Schettini A., Winkowski J. Towards an algebra for timed behaviours // Theoretical Computer Science. — 1992. — Vol. 103, no. 2. Pp. 335-363.

54. McLane S. Categories for the Working Mathematician // Graduate Texts in Mathematics. Springer, Berlin.— 1971.

55. Merlin P., Farber D. Recoverability of Communication Protocols Implications of a Theoretical Study // IEEE Transactions on Communications. — 1976. — Vol. 24, no. 9. — Pp. 1036-1043.

56. Meseguer J., Montanari U., Sassone V. On the Semantics of Petri Nets // Lecture Notes in Computer Science. — 1992. — Vol. 630. — Pp. 286-301.

57. Milner R. A Calculus of Communicating Systems. — Springer-Verlag New York, Inc. Secaucus, NJ, USA, 1982.

58. Milner R. Communication and concurrency. — 1989.

59. Milner R., Sangiorgi D. Barbed bisimulation // Proceedings of 1С ALP. 1992. - Vol. 92. - Pp. 685-695.

60. Murphy D. Time and duration in noninterleaving concurrency // Fundamenta Informaticae. — 1993. — Vol. 19, no. 3-4. — Pp. 403-416.

61. Nielsen M., Hune T. Timed bisimulation and open maps // Research Series RS-98-4, BRICS, Department of Computer Science, University of Aarhus, February. — 1998.

62. Nielsen M., Plotkin G., Winskel G. Petri Nets, Event Structures and Domains, Part If/ Theoretical Computer Science. — 1981.— Vol. 13, no. 1. Pp. 85-108.

63. Nielsen M., Rozenberg G., Thiagarajan P. Behavioural notions for elementary net systems // Distributed Computing. — 1990. — Vol. 4, no. 1, —Pp. 45-57.

64. Nielsen M., Winskel G. Petri nets and bisimulation // Theoretical Computer Science. — 1996. — Vol. 153, no. 1-2. — Pp. 211-244.

65. On Specifying Real-Time Systems in a Causality-Based Setting / J. Katoen, R. Langerak, D. Latella, E. Brinksma // Lecture Notes in Computer Science. — 1996. — Vol. 1135. — Pp. 385-404.

66. Park D. Concurrency and automata on infinite sequences // Theoretical Computer Science. — 1981. — Vol. 104. — Pp. 167-183.

67. Pinna G., Poigne A. On the nature of events: another perspective in concurrency // Theoretical Computer Science. — 1995.— Vol. 138, no. 2. Pp. 425-454.

68. Popova L. On Time Petri Nets // Journal Information Processing and Cybernetics, EIK. — 1991. — Vol. 27, no. 4. — Pp. 227-244.

69. Pratt V. Modeling Concurrency with Geometry // Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages. — 1991. — Pp. 311-322.

70. Rabinovich A., Trakhtenbrot B. Behavior structures and nets // Fundamenta Informaticae. — 1988. — Vol. 11, no. 4. — Pp. 357-404.

71. Ramchandani C. Analysis of asynchronous concurrent systems using timed Petri nets: Ph.D. thesis / Massachusetts Institute of Technology Cambridge, Dept. Electronical Engineering, MA, USA. — 1974.

72. Sassone V., Nielsen M., Winskel G. Models for concurrency: towards a classification // Theoretical Computer Science. — 1996. — Vol. 170, no. 1-2. Pp. 297-348.

73. Shields M. Concurrent Machines // The Computer Journal. — 1985.— Vol. 28, no. 5. — Pp. 449-465.

74. Srba J. Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets // Lecture Notes in Computer Science. — 2008. Vol. 5215. - Pp. 15-32.

75. Starke P. Some properties of timed nets under the earliest firing rule // Lecture Notes in Computer Science. — 1990. — Vol. 424. — Pp. 418-432.

76. Steffen В., Weise C. Deciding Testing Equivalence for Real-Time Processes with Dense Time // Lecture Notes in Computer Science. — 1993. Pp. 703-713.

77. Temporal structures / R. Casley, R. Crew, J. Meseguer, V. Pratt //

78. Mathematical Structures in Computer Science. — 1982. — Vol. 1, no. 2. — Pp. 179-213.

79. Timed CSP: Theory and Practice / S. Schneider, J. Davies, D. Jackson et al. // Proceedings of the Real-Time: Theory in Practice, REX Workshop. 1991. - Pp. 640-675.

80. Weise C., Lenzkes D. Efficient Scaling-Invariant Checking of Timed Bisimulation // Proceedings of the 14th Annual Symposion on Theoretical Aspects of Computer Science (STACS 1997), LNCS. — Vol. 1200. Pp. 177-188.

81. Winskel G. Events in Computation: Ph.D. thesis / University of Edingurgh. — 1980.

82. Winskel G. Event structures // Lecture Notes in Computer Science. — 1987. — Vol. 255. Pp. 325-392.

83. Winskel G. An introduction to event structures j j Lecture Notes in Computer Science. — 1988. Vol. 384. — Pp. 364-397.

84. Winskel G., Nielsen M. Models for concurrency // Handbook of Logic in Computer Sciencc. — 1995. — Vol. 4. — Pp. 1-148.