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

• Кузьмин, Егор Владимирович
• кандидат физико-математических наук
• 2004

Оглавление диссертации кандидат физико-математических наук Кузьмин, Егор Владимирович

Введение

1 Предварительные сведения

1.1 Мультимножества.

1.2 Квазиупорядоченные множества.

1.2.1 Свойство вполне упорядочиваемости.

1.3 Системы помеченных переходов.

1.3.1 Определение

1.3.2 Вполне структурированные системы переходов

1.3.3 Покрывающее дерево системы переходов

1.3.4 Метод насыщения.

1.3.5 Системы переходов с совместимостью по убыванию

1.4 Счётчиковые машины.

1.5 Темпоральные логики и проверка модели.

1.5.1 Логики ветвящегося времени.

1.5.2 Логики линейного времени.

1.5.3 Сравнение логик.

2 Темпоральные свойства вполне структурированных систем переходов

2.1 Системы переходов автоматного типа.

2.1.1 Разрешимые темпоральные свойства.

2.1.2 Неразрешимые темпоральные свойства.

2.2 Вполне структурированные системы переходов.

2.2.1 Разрешимые темпоральные свойства.

2.2.2 Неразрешимые темпоральные свойства.

2.3 Дерево логик.

3 Взаимодействующие раскрашивающие процессы

3.1 Взаимодействующие процессы независимые от данных.

3.2 Взаимодействующие раскрашивающие процессы.

3.3 ССР - вполне структурированная система переходов.

3.4 Пример.

4 Недетерминированные счётчиковые машины

4.1 Введение.

4.2 Недетерминированные счётчиковые машины.

4.3 Проблема ограниченности.

4.4 Проблемы включения и эквивалентности.

4.4.1 Слабое вычисление.

4.4.2 Проблема включения.

4.4.3 Проблема эквивалентности.

4.5 Проблема достижимости.

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

В настоящее время большое внимание уделяется моделированию и анализу корректности параллельных и распределённых систем, каковыми являются, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов. Под корректностью понимается полное соответствие системы задачам, для которых она создаётся. Корректность определяется абстрактным образом в соответствии с формальной спецификацией, описывающей желаемое поведение системы. Процесс проверки соответствия поведения системы требованиям, заданным в спецификации, называется верификацией [23, 6].

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

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

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

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

Чтобы преодолеть этот недостаток, были разработаны методы, применимые по крайней мере, для некоторых ограниченных классов систем с бесконечным числом состояний. Можно упомянуть здесь работы, например, P. Abdulla, К. Cerans, A. Finkel, В. Jonsson, F. Moller, Ph. Schnoebelen

27, 52, 76]. Более того, оказалось;, что метод проверки модели, широко используемый при автоматической верификации систем с конечным числом состояний, может быть применён для некоторых классов систем с бесконечным числом состояний и подмножеств темпоральных логик [48, 50, 38, 49, 35].

Исследования систем переходов с бесконечным числом состояний были мотивированы теорией формальных языков и грамматик [60, 26, 5].

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

Классическим примером является мм^^а^гштоьш^Ъ теории формальных языков он используется для описания контекстно свободных языков. Но этот автомат может быть также рассмотрен как модель системы переходов с бесконечным числом состояний. Каждое управляющее состояние (множество которых конечно) вместе с содержимым стека (магазина) описывает состояние системы переходов. Поскольку размер стека не ограничен, то может быть бесконечно много различных состояний системы. Состояние меняется, когда автомат принимает терминальный символ. Однако, это можно интерпретировать как совершение действия системой и переход её в другое состояние.

Примерами других формальных моделей (систем переходов с бесконечным числом состояний), позволяющих описывать параллельные и распределённые системы, являются сети Петри [9], ВРР (Basic Parallel Processes) [41], LCS (Lossy Channel Systems - системы с каналами, теряющими послания) [30, 31], Real-Time Automata (автоматы реального времени) [33] и др.

Указанные формализмы, как и многие другие, могут быть рассмотрены как вполне структурированные системы переходов [27, 52].

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

Ранее в ряде публикаций таких авторов, как A. Bouajjani, О. Burkart, J. Esparza, A. Kiehn, R. Мауг, из которых, например, можно выделить [38, 35, 49, 50], исследовались вопросы разрешимости задачи проверки модели для некоторых конкретных представителей класса вполне структурированных систем переходов, а именно, магазинных автоматов, сетей Петри, ВРР, LVAS (Lossy Vector Addition Systems), и различных темпоральных логик линейного времени и ветвящегося времени.

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

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

Для демонстрации этого факта в данной работе представлен новый формализм, названный взаимодействующие раскрашивающие процессы (Communicating Colouring Processes - ССР), позволяющий строить модели распределённых системы, где поведение каждого компонента описывается последовательным процессом n между ними организовано взаимодействие, направленное на обмен и передачу пакетов информации. Формализм ССР принимает во внимание факт передачи данных, а также позволяет отслеживать перемещение данных различного типа между компонентами системы. Но переход из одного состояния в другое не зависит от оперируемых данных, а определяется только управляющими состояниями.

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

Указанные формализмы представляют собой конкретные реализации специального подмножества (фрагмента) алгебры процессов, построенной на основе таких хорошо известных алгебр процессов, как CCS (Calculus ■ of Communicating Systems - исчисление взаимодействующих систем) Мил-нера [74] и SCP (Communicating Sequential Processes - взаимодействующие последовательные процессы) Хоара [59], позволяющего строить формальные модели (параллельных программ), которые могут быть рассмотрены как независимые от данных помеченные системы переходов, а более конкретно, как вполне структурированные системы переходов автоматного типа.

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

Достижение цели связывается с решением следующих задач:

• Нахождение семантически нетривиального подкласса вполне структурированных систем переходов и исследование разрешимости его темпоральных и семантических свойств.

• Построение достаточно выразительного формализма для моделирования и анализа распределённых систем, являющегося примером выявленного подкласса систем переходов.

• Для разработанного формализма определить математическую семантику и исследовать разрешимость проблем достижимости, ограниченности, включения и эквивалентности.

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

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

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

Апробация работы. Результаты диссертации докладывались на Международном симпозиуме "Temporal Representation and Reasoning" (Tatihou, Франция, 2004), Международном рабочем совещании "Распределенные информационно-вычислительные ресурсы и математическое моделирование" (Новосибирск, 2004), Международном рабочем совещании "Program Understanding" (Новосибирск - Алтай, 2003), Всероссийской научной конференции, посвящённой 200-летию Ярославского государственного университета им. П.Г. Демидова (2003), семинаре "Моделирование и анализ информационных систем" кафедры теоретической информатики Ярославского государственного университета им. П.Г. Демидова (2001-2004).

Гранты. Работа по теме диссертации проводилась в соответствии с планами исследований по проектам, поддержанными следующими грантами: РФФИ №03-01-00-804 "Разработка новых методов и средств моделирования и анализа процессов обработки информации в распределённых системах", №99-01-00-309 "Методы моделирования, анализа и верификации распределённых систем", Федеральная целевая программа "Интеграция".

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

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

Структура и объём работы. Диссертационная работа изложена на

149 страницах и состоит из введения, четырех глав и заключения. Иллюстративный материал включает 18 рисунков. Список литературы состоит из 99 наименований.

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

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

В третьей главе представлен новый (специальный) фрагмент алгебры процессов, определяемой в стиле CSP Хоара и CCS Милнера, позволяющий строить формальные модели (параллельных и распределённых систем), которые могут быть рассмотрены как независимые от данных помеченные системы переходов, а более конкретно, вполне структурированные системы переходов с совместимостью по возрастанию и убыванию (т.е. автоматного типа). Более того, предлагается к рассмотрению конкретная реализация данного класса систем переходов, новый формализм для моделирования распределённых систем, позволяющий отслеживать перемещение данных различного типа между компонентами системы, названный взаимодействующие раскрашивающие процессы (Communicating Colouring Processes - ССР).

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

В заключении сформулированы основные результаты работы.

Заключение диссертации по теме «Дискретная математика и математическая кибернетика», Кузьмин, Егор Владимирович

Заключение

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

Перечислим основные научные результаты, полученные в диссертации:

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

2. Представлен новый специальный фрагмент алгебры процессов, определяемой в стиле CSP Хоара и CCS Милнера, позволяющий строить формальные модели (параллельных и распределённых систем), которые могут быть рассмотрены как независимые от данных помеченные системы переходов, а более конкретно, вполне структурированные системы переходов автоматного типа.

3. Предложена к рассмотрению конкретная реализация данного класса взаимодействующих процессов независимых от данных, новый формализм для моделирования распределённых систем, позволяющий отслеживать перемещение данных различного типа между компонентами системы, названный взаимодействующие раскрашивающие процессы (Communicating Colouring Processes - ССР).

Для ССР доказана разрешимость проблем покрытия, субпокрытия, достижимости управляющего состояния, проблем неизбежности и останова.

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

Список литературы диссертационного исследования кандидат физико-математических наук Кузьмин, Егор Владимирович, 2004 год

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

2. Борщев А.В., Карпов Ю.Г., Рудаков В.В. О корректности параллельных алгоритмов // Программирование, N 4, 1996. С. 5-17.

3. Грис Д. Наука программирования. М.: Мир, 1984. - 416 с.

4. Дейкстра Э. Дисциплина программирования. М.: Мир, 1978.

5. Карпов Ю.Г. Теория автоматов. СПб.: Питер, 2003. - 208 с.

6. Карпов Ю. Г. Формальное описание и верификация протоколов на основе CSS // Автоматика и вычислительная техника. Рига, 1986. - № 6. - С.21-30.

7. Карпов Ю.Г. Анализ корректности параллельной программы разделения множеств // Программирование, N 6, 1996. С. 27-33.

8. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Пер. с англ. / Под ред. Р. Смелянского. - М.: МЦНМО, 2002. - 416 с.

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

10. Кузьмин Е.В., Соколов В.А. Взаимодействующие раскрашивающие процессы // Моделирование и анализ информационных систем, т. 11 (2), 2004.

11. Кузьмин Е. О разрешимости задачи проверки модели для автоматной логики и вполне структурированных систем переходов автоматного типа // Моделирование и анализ информационных систем, т. 11 (1), 2004. С. 8-17.

12. Кузьмин Е.В., Соколов В.А. Проверка свойств вполне структурированных моделей // Мат. Всероссийской научной конференции, по-свящённой 200-летию Ярославского государственного университета им. П.Г. Демидова, 2003. С. 50-54.

13. Кузьмин Е. Недетерминированные счётчиковые машины // Моделирование и анализ информационных систем, т. 10 (2), 2003. С. 41-49.

14. Кузьмин Е. О разрешимости задачи проверки модели для модального /i-исчисления и некоторых классов вполне структурированных систем переходов // Моделирование и анализ информационных систем, т. 10 (1), 2003. С. 50-55.

15. Кузьмин Е. Верификация графов потоков данных с использованием символьной проверки модели для CTL // Моделирование и анализ информационных систем, т.8 (1), 2001. С. 38-43.

16. Куратовский К., Мостовский А. Теория множеств. М.: Мир, 1970.

17. Ломазова И.А. Моделирование мультиагентных динамических систем вложенными сетями Петри // Программные системы: Теоретические основы и приложения. М.: Наука. Физматлит, 1999. С. 143-156.

18. Ломазова И.А. Некоторые алгоритмы анализа для многоуровневых вложенных сетей Петри // Известия РАН. Теория и системы управления, т, 2000. С. 965-974.

19. Ломазова И.А. Рекурсивные вложенные сети Петри: анализ семантических свойств и выразительность // Программирование, 2001.

20. Мальцев А.И. Алгоритмы и рекурсивные функции. М.: Наука, 1965.

21. Минский М. Вычисления и автоматы. М.: Мир, 1971.

22. Непомнящий В.А. Практические методы верификации программ // Кибернетика, №2, 1984. С. 21-28, 43.

23. Питерсон Дж. Теория сетей Петри и моделирование систем. М.: Мир, 1984. - 263 с.

24. Хоар Ч. Взаимодействующие последовательные процессы: Пер. с англ. М.: Мир, 1989. - 264 с.

25. Хопкрофт Д., Мотвани Р., Ульман Д. Введение в теорию автоматов, языков и вычислений. 2-е изд.: Пер. с англ. М.: "Вильяме", 2002, 528 с.

26. Abdulla P.A., Cerans К., Jonsson В., Yih-Kuen Т. General decidability theorems for infinite-state systems. // Proc. 11th IEEE Symp. Logic in Computer Science (LICS'96), 1996. P. 313-321.

27. Abdulla P.A., Cerans К., Jonsson В., Yih-Kuen Т. Algorithmic analysis of programs with well quasi-ordered domains // Information and Computation, 1997.

28. Abdulla P., Bouajjani A., Jonsson B. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels // Proc. 10th Intern. Conf. on Computer Aided Verification (CAV'98). LNCS 1427, 1998.

29. Abdulla P., Jonsson B. Verifying Programs with Unreliable Channels // Proc. LICS'93, 1993. P. 160-170.

30. Abdulla P., Jonsson B. Undecidable verification problems for programs with unreliable channels // Information and Computation, 130(1), 1996. P. 71-90.

31. Alur R., Kannan S., Yannakakis M. Communicating hierarchical automata // ICALP'99, Springer LNCS 1644, 1999. P. 169-178.

32. Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems // Proc. 5th IEEE Int. Symp. on Logic in Computer Science, Philadelphia, 1990. P. 414-425.

33. Araki Т., Kasami T. Some decision problems related to the reachability problem for Petri nets // Theoretical Computer Science, 3(1), 1977. P. 85-104.

34. Bouajjani A., Mayr R. Model Checking Lossy Vector Addition Systems // Proc. 16th Intern. Symp. on Theoretical Aspects in Computer Science (STACS'99) , LNCS 1563, Trier (Germany), March 1999.

35. Biichi J.R. On a decision method in restricted second order arithmetic // Proc. Int. Congr. Logic, Method and Philos. Sci. 1960, Stanford, 1962. P. 1-12.

36. Burkart 0., Caucal D., Moller F., Steffen B. Verification over Infinite States. Chapter in the Handbook of Process Algebra, J. Bergstra, A. Ponse and S.A. Smolka (editors), Elsevier Publishers, 2001. P. 545-623.f

37. Burkart 0., Esparza J. More infinite results // Electronic Notes in Theoretical Computer Science, 6, 1996.

38. Clarke E., Grumberg O., Peled D. Model Checking. The MIT Press, 2001.

39. Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic // LNCS 131, 1981. P. 52-71.

40. Christensen S., Hirshfeld Y., Moller F. Bisimulation equivalence is decidable for basic parallel processes // Proc. CONCUR'93, LNCS 715, P. 143-157.

41. Dam M. Fixpoints of Biichi automata // International Conference on the Foundations of Software Technology and Theoretical Computer Science (FST&TCS), LNCS, vol. 652, 1992. P. 39-50.

42. Daniele M,, Giunchiglia F., Vardi M.Y. Improved automata generation for linear temporal logic // Computer-Aided Verification, Proc. 11th Int. Conference, v. 1633, 1999. P. 249-260.

43. Dickson L. E. Finiteness of the odd perfect and primitive abundant numbers with r distinct prime factors // Amer. Journal Math. 1913. 35. P. 413-422.

44. Dufourd C., Jancar P., Schnoebelen Ph. Boundedness of Reset P/T nets // In Proc. ICALP'99, LNCS 1644, Springer, 1999. P. 301-310.

45. Dufourd С., Finkel A., Schnoebelen Ph. Reset nets between decidability and undecidability // Proc. ICALP'98, LNCS 1443, Springer, 1998. P. 103-115.

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

47. Esparza J. On the decidabilty of model checking for several /i-calculi and Petri nets // Proc. CAAP'94, LNCS 787, 1994. P. 115-129.

48. Esparza J. Decidability of model-checking for infinite-state concurrent systems // Acta Informatica, 34, 1997. P. 85-107.

49. Esparza J., Kiehn A. On the model checking problem for branching time logics and basic parallel processes // Proc. of CAV'95, LNCS 939, Springer-Verlag, 1995. P. 353-366.

50. Finkel A. Reduction and covering of infinite reachability trees. // Information and Computation, 89(2), 1990. P. 144-179.

51. Finkel A., Schnoebelen Ph. Well-structured transition systems everywhere! // Theoretical Computer Science, 256(1-2), 2001. P. 63-92.

52. Finkel A., Schnoebelen Ph. Fundamental structures in well-structured infinite transition systems // Proc. 3rd Latin American Theoretical Informatics Symposium (LATIN'98), Campinas, Brazil, Apr. 1998, LNCS 1380, Springer, 1998. P. 102-118.

53. Gerth R., Peled D., Vardi M.Y., Wolper P. Simple on-the-fly automatic verification of linear temporal logic // Proc. of the 15th Workshop on Protocol Specification, Testing, and Verification, 1995.

54. Hennessy M. Algebraic Theory of Processes. MIT Press, 1988.

55. Hennessy M., Milner R. On observing nondeterminism and concurrency. // Lecture Notes in Computer Science, 85 (1980). P. 295-309.

56. Hennessy M., Milner R. Algebraic laws for nondeterminism and concurrency // Journal of Association of Computer Machinery, 32, 1985. P. 137-162.

57. Higman G. Ordering by divisibility in Abstract Algebra // Proc. London Math. Soc., 3(2), 1952. P. 326-336.

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

59. Hopcroft J.E., Ullman J.D. Introduction to Automata Theory, Languages and Computation. Addison Wesley, 1979.

60. Jensen K. Coloured Petri Nets // Vol.1. Eatcs Monographs on TCS, Springer-Verlag, 1994.

61. Jonsson В., Parrow J. Deciding bisimulation equivalences for a class of non-finite-state programs // Information and Computation, 107(2), 1993. P. 272-302.

62. Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking /i-Calculus in Well-Structured Transition Systems // Proc. of 11th International Symposium on Temporal Representation and Reasoning, Tatihou, France, 2004.

63. Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking д-Calculus . in Well-Structured Transition Systems // Joint Bulletin of NCC к IIS, Сотр. Science, Novosibirsk, 2004.

64. Kouzmin E., Sokolov V. Communicating Colouring Automata // Int. Workshop on Program Understanding (sat. of PSI'03), 2003. P. 40-46.

65. Kouchnarenko О., Schnoebelen Ph. A model for recursive-parallel programs // Proc. 1st Int. Workshop on Verification of Infinite State Systems (INFINITY'96), Pisa, Italy, Aug. 1996, vol. 5 of Electronic Notes in Theor. Сотр. Sci. Elsevier, 1997.

66. Kozen D. Results on the prepositional /i-calculus // Theoret. Comput. Sci. 27 (1983). P. 242-272.

67. Larsen K. Proof systems for satisfiability in Hennesy-Milner logic with recursion // Theoret. Comput. Sci. 72 (1990). P. 265-288.

68. Lomazova I.A. Nested Petri nets a Formalism for Specification and Verification of Multi-Agent Distributed Systems // Fundamenta Informaticae, vol. 43, №1-4, 2000. P. 195-214.

69. Lomazova I.A., Schnoebelen Ph. Some Decidability Results for Nested Petri Nets // Proc. Andrei Ershov 3rd Int. Conf. Perspectives of System Informatics (PSI'99), Novosibirsk, Russia, Jul. 1999, LNCS 1755. Springer-Verlag, 2000. P. 207-219.

70. Mayr R. Lossy counter machines. Tech. Report TUM-I9827, Institut fur Informatik, TUM, Munich, Germany, October 1998.

71. Mayr R. Decidability and complexity of model checking problems for infinite-state systems. Technischen Universitat Miinchen, dissertation, 1998.

72. Milner R. A Calculus of Communicating Systems // LNCS 92, Springer-Verlag, 1980.

73. Milner R. Communication and Concurrency. Prentice Hall Int., 1989.

74. Minsky M. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.

75. Moller F. Infinite results // Proc. CONCUR'96, LNCS 1119, 1996. P. 195-216.

76. Moller F., Birtwistle. Logic for Concurrency // LNCS 1043, 1996.

77. Nepomniaschy V.A., Shilov N.V. , Bodin E.V., Kozura V.E. Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems // LNCS 2335, 2002. P. 69-88.

78. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T.G., Mylnikov S.P., Okunishnikova E.V. Petri Net Modelling of Estelle-specified Communication Protocols // LNCS 964, 1995. P. 94-108.

79. Nepomniaschy V.A., Shilov N.V., Bodin E.V. A concurrent systems specification language based on SDL and CTL // Proc. of Workshop on Concurrency, Specifications and Programming, Berlin, Humboldt University, Informatik-Bericht Nr.36, 1994. P. 15-26.

80. Nepomniaschy V.A., Shilov N.V. REAL92: A Combined Specification Language for Real-Time Concurrent Systems and Properties // LNCS 735, 1993. P. 377-393.

81. Peterson J. L. Petri Net Theory and the Modeling of Systems. Prentice-Hall Int., 1981.

82. Pnueli A. The temporal logic of programs // FOCS'77, IEEE, 1977.

83. Pratt V. A decidable //-calculus // Proc. 22nd FOCS (1981). P. 421-427.

84. Shilov N.V., Yi К. Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers // Electr. Notes Theor. Comput. Sci. 43, 2001.

85. Shilov N.V., Yi K. On Expressive and Model Checking Power of Prepositional Program Logics // Ershov Memorial Conference, 2001. P. 39-46.

86. Shilov N.V., Yi K. How to find a coin: prepositional program logics made easy // Bulletin of the European Association for Theoretical Computer Science, v.75, 2001. P. 127-151.

87. Shilov N.V. Program Schemata vs. Automata for Decidability of Program Logics // Theor. Comput. Sci. 175(1), 1997. P. 15-27.

88. Somenzi F., Bloem R. Efficient Biichi automata from LTL formulae // Computer-Aided Verification, Proc. 12th Int. Conference, v. 1633, 2000. P. 247-263.

89. Steffen B. Characteristic formulae // Proc. ICALP (1989).

90. Stirling C. P. Temporal logics for CCS. Proc. of REX Workshop, 1988.

91. Stirling C. P. Modal and temporal logics // Handbook of Logic in Computer Science. Vol. 2. Oxford University Press. 1992. P. 477-563.

92. Stirling C. P. Modal and temporal logics for processes // LNCS 1043, 1996, P. 149-237.

93. Stirling C., Walker D. Local model checking in the modal /z-calculus // Theoretical Computer Science, 89 (1991), P. 161-177.

94. Vardi M.Y. An automata-theoretic approach to linear temporal logic // Logics for Concurrency, LNCS 1043, 1996. P. 238-266.

95. Vardi M.Y., Wolper P. Reasoning about infinite computations // Information and Computation, 115(1), 1994. P. 1-37.

96. Vardi M.Y., Wolper P. An automata-theoretic approach to automatic program verification // Proc. of the First Symposium on Logic in Computer Science, 1986. P. 322-331.

97. Wolper P. Temporal logic can be more expressive // Information and Control, 56, 1983.

98. Wolper P., Vardi M.Y., Sistla A.P. Reasoning about infinite computation paths // Proc. 24th IEEE Symposium on Foundations of Computer Science, 1983. P. 185-194.