Развертки раскрашенных сетей Петри и их применение для верификации моделей распределенных систем тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Козюра, В.Е.

• Козюра, В.Е.
• кандидат физико-математических наук
• 2004

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

Введение.

Глава

Предварительные понятия.

1.1 Развертки сетей Петри.

1.1.1. Ветвящиеся процессы.

1.1.2. Определения разверток сетей Петри.

1.1.3. Методы обнаружения тупиков.

1.2 Раскрашенные сети Петри.

1.2.1 Общие определения.

1.2.2 Симметрия и эквивалентность.

1.2.3 Раскрашенные сети Петри со временем.

1.2.3.1 Модель интервального времени.

1.2.3.2 Модель временных штампов.

1.3 Метод проверки моделей.

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

1.3.2 Логика мю-исчисления.

1.3.3 Алгоритм проверки моделей для логики линейного времени.

1.3.4 Алгоритм проверки моделей для логики мю-исчисления.

Глава

Развертки раскрашенных сетей Петри.

2.1 Ветвящийся процесс для раскрашенных сетей Петри.

2.2 Определения и основные свойства разверток.

2.3 Алгоритмы построения разверток.

2.4 Алгоритмы обнаружения тупиков.

Глава

Развертки раскрашенных сетей Петри, расширенных эквивалентностью и временем.

3.1 Применение эквивалентности в развертках.

3.2 Развертки сетей с интервальным временем.

3.3 Развертки сетей с временными штампами.

Глава

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

4.1 Метод проверки моделей и обоснование его корректности.

4.2 Применение метода проверки моделей к сетям, расширенным свойством эквивалентности.

4.3 Применение метода проверки моделей для временных сетей.

4.3.1 Модель интервального времени.

4.3.2 Модель временных штампов.

Глава

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

5.1 Системы верификации раскрашенных сетей Петри.

5.1.1 Система PNV.

5.1.2 Реализация метода проверки моделей с использованием разверток. и 5.2 Экспериментальные результаты.

7 5.2.1 Задача об обедающих философах.

5.2.2 Битовый протокол.

5.2.3 Кольцевой протокол.

5.2.4 Протокол "Отправитель - получатель".

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

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

Теории и приложениям сетей Петри посвящена богатая литература, см., например, [9]. В России велись исследования по моделированию, спецификации и верификации распределенных систем с использованием сетей Петри. Отметим, в частности, работы O.JI. Бандман [2,3] по спецификации поведения сетевых протоколов, Н.А. Анисимова [15] по спецификации протоколов, В.А. Соколова [12] по анализу паралельных программ и И.Б. Вирбицкайте [4] по использованию техники частичного порядка для верификации временных сетей Петри.

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

Последние два десятилетия метод проверки моделей активно развивался в работах многих авторов и показал себя как эффективное и многообещающее средство для верификации распределенных систем. Благодаря своей естественности и возможности быть интегрированным в среду разработки и анализа распределенных систем, метод проверки моделей был принят в качестве одного из стандартов для верификации спецификаций систем, описанных на каком-либо формальном языке. В качестве входных данных для процедуры проверки моделей поступают описание самой системы (чаще всего задаваемое в виде некоторой структуры с конечным числом состояний) и логическая спецификация (обычно, формула временной логики), описывающая проверяемое свойство системы. В качестве формализмов для описания структуры системы чаще всего используются такие модели, как структуры Крипке и помеченные системы переходов [19, 20, 51]. Активно используемые логические спецификации подразделяются на логики линейного времени (LTL) и логики ветвящегося времени. Среди наиболее используемых логик ветвящегося времени следует отметить логику Хеннесси-Милнера, логику модального мю-исчисления, базирующуюся на теории неподвижных точек, и логику вычислимых деревьев (CTL - Computational Tree Logic) [51]. Методы проверки моделей подразделяются на локальную и глобальную проверку моделей. При локальной проверке моделей по заданной логической спецификации и некоторому участку (состоянию) системы необходимо определить, является ли данная спецификация истинной на заданном участке или нет. При глобальной проверке моделей по заданной логической спецификации и описанию системы необходимо определить те состояния системы, в которых формула логической спецификации является истинной. Методы проверки моделей предоставляют полностью автоматический способ решения данных задач. Обзор современного состояния теории проверки моделей можно найти, например, в работе [19].

К сожалению, при полном моделировании работы сети мы сталкиваемся с так называемой "проблемой взрыва числа состояний" (state explosion problem). Эта проблема состоит в том, что при росте размеров рассматриваемой сети, ее полная модель достаточно быстро становится необозримо большой. Это не позволяет надеяться на построение полной модели для реальных протоколов. Отдельным и, как это следует из вышесказанного, достаточно важным направлением верификации распределенных систем является разработка методов, направленных на решение проблемы взрыва числа состояний. Среди таких методов можно выделить следующие: метод упрямых множеств (stubborn set method), использование двоичных разрешающих диаграмм (symbolic binary decision diagrams ), методы, основанные на частичном порядке (partial order methods), а также использование симметрии и эквивалентности на рассматриваемых моделях [54].

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

Среди различных расширений стандартных сетей Петри выделяются сети Петри высокого уровня — раскрашенные сети Петри (РСП) [35, 36], для которых развит теоретический аппарат, накоплен значительный опыт использования и реализована система симуляции и анализа Design/CPN [46]. В РСП вместо обычных фишек используются типизированные знаковые элементы. Также есть возможность задания функций на дугах и переходах. Это расширение позволяет выражать в достаточно компактном виде сложные системы, не теряя при этом возможностей применять методы, разработанные для стандартных сетей Петри. Данная работа посвящена применению метода проверки моделей с использованием разверток к раскрашенным сетям Петри.

Использование разверток для анализа стандартных сетей Петри было предложено МакМилланом в работе [48]. Было предложено использовать конечный префикс максимального ветвящегося процесса вместо полного графа достижимости. Размер развертки является экспоненциальным в общем случае, и в последующих работах были предложены некоторые улучшения определений и алгоритмов построения развертки [25, 45]. Так в работе [25] было предложено рассматривать обобщенное понятие порядка на конфигурациях, и с его помощью, был предложен критерий финитизации, являющийся оптимальным для одно-безопасных сетей Петри. В работе [45] было показано, что для п-безопасных сетей Петри данный критерий не является оптимальным и было предложено существенное улучшение критерия для n-безопасных сетей Петри. В работе [45] также был предложен алгоритм построения развертки, линейно зависящий от произведения числа мест и переходов развертки.

Первоначально МакМиллан предложил использовать развертки для анализа достижимости и обнаружения тупиков. Эти методы были улучшены в последующих работах [31, 50]. В работе [31] предложено улучшение метода определения достижимости данного состояния сети. В работе [50] дается метод обнаружения тупиковых состояний с использованием системы неравенств, описывающих рассматриваемую сеть Петри. Дж. Эспарца в работе [24] предложил метод проверки моделей для одно-безопасных сетей Петри и логики S4 с использованием развертки. В работе [16] для сетей Петри с интервальным временем была построена развертка и применен алгоритм проверки моделей Эспарцы. В работе [57] Ф. Валнер предложил алгоритм проверки моделей для LTL логики, основанный на развертках сети Петри. В его работе известный теоретико-автоматный подход к верификации LTL формул [56] был перенесен на одно-безопасные сети Петри без тупиковых состояний. Этот подход был развит в последующих работах

14, 22, 27, 28, 33]. На последнем этапе алгоритма Валнера строится дополнительный граф, состоящий из точек сечения рассматриваемой развертки. В работах [27, 28] была показана возможность модификации алгоритма, позволяющая избежать построения данного дополнительного графа и описана реализация данного подхода с приведением экспериментальных результатов. Работы [14, 33] посвящены теоретическим аспектам методов проверки моделей с использованием разверток. В работе [33] были доказаны некоторые сложностные оценки алгоритмов проверки моделей с использованием разверток. Работа [14] посвящена рассмотрению возможностей применения методов развертки к неограниченным сетям Петри. Стоит также отметить работу [26], в которой метод развертки был применен к синхронизированному произведению двух сетей Петри.

Развертка РСП без применения критериев финитизации в общем случае была рассмотрена в работе [55] для использования её в методе упрямых множеств. В этой работе, помимо отсутствия финитизации, также использовалось старое представление раскрашенных сетей Петри. Все это заставило автора сделать вывод о неэффективности использования разверток РСП, и в его дальнейших работах было показано, как применять метод упрямых множеств для РСП без построения развертки. Развертки РСП не рассматривались более в литературе. Хотя для стандартных сетей Петри были развиты критерии финитизации, эффективные алгоритмы построения разверток, техника работы со свойством достижимости и по обнаружению тупиков, а также алгоритмы проверки моделей для логики LTL, возможность применения данной техники к РСП оставалась открытым вопросом.

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

- Разработка эффективных методов построения разверток РСП без временных конструкций.

- Исследование метода развертки для РСП, расширенных спецификациями эквивалентности и временными конструкциями.

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

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

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

В диссертациионой работе формально строится максимальный ветвящийся процесс для РСП, используя их современное представление [35, 36], и конструктивно доказывается его существование. В работе определены развертки РСП как конечный префикс максимального ветвящегося процесса, полученный с помощью некоторого критерия финитизации, для которых доказываются свойства конечности, безопасности и полноты. Первое свойство дает нам конечность развертки, полученной при применении трех заданных критериев финитизации. Второе гарантирует отсутствие в развертках лишней информации о поведении РСП. Третье свойство дает нам существование во всех трех типах развертки полной информации о графе достижимости РСП. Методы финитизации, разработанные для стандартных сетей Петри, были применены для построенного максимального ветвящегося процесса РСП. В работе описаны два алгоритма построения разверток РСП и даны оценки сложности данных алгоритмов. Первый алгоритм является удобным средством для проведения теоретических рассуждений, в то время как второй алгоритм является эффективным с точки зрения практики. Показано, как применять методы обнаружения тупиков, описанные в [50], к РСП. Методы работы с развертками интервально-временных сетей Петри [16] также формально применены к интервально-временным РСП. Следующим логичным шагом было применение методов проверки моделей, развитых для стандартных сетей Петри, к РСП. В диссертационной работе описана основанная на состояниях семантика LTL для РСП и разработан метод проверки моделей для логики LTL и РСП с использованием разверток. Метод позволяет эффективно проверять многие свойства, выразимые в логике линейного времени, для раскрашенных сетей Петри. Корректность полученного алгоритма формально доказана. Также показана возможность применения данного алгоритма к РСП с интервальным временем.

Вся описанная выше работа связана с перенесением методов, разработанных для стандартных сетей Петри на РСП. Однако, описанные в [35, 36] РСП имеют два существенные расширения. Во-первых, благодаря развитому аппарату работы с типами данных (цветами), имеются большие возможности по определению спецификаций симметрии и эквивалентности для РСП, основанные на цветовых значениях. Новым шагом, сделанным в данной работе, является разработка методов развертки РСП, расширенных спецификацией . эквивалентности. Теории построения разверток с использованием отношения эквивалентности не существовало ранее также и для стандартных сетей Петри, хотя некоторый шаг в этом направлении был сделан в работе [53]. Использование таких разверток РСП позволяет дополнительно существенно уменьшить размер рассматриваемой модели. В работе также показано, как можно использовать отношение эквивалентности при проведении проверки моделей с применением разверток. Второй особенностью РСП, отсутствующей в стандартной модели сетей Петри, является применение специальной временной модели, так называемой модели временных штампов. В диссертации показывается возможность применения методов развертки к РСП с временными штампами, а также возможность применения к ним метода проверки моделей для логики LTL. Заметим здесь, что получаемые развертки для РСП с временными штампами являются, в общем случае, бесконечными. Та же проблема возникает и при рассмотрении графа достижимости модели РСП с временными штампами [36]. В работе [36] было предложено использовать спецификации эквивалентности по времени для финитизации графа достижимости. В диссертации предлагается использовать аналогичный подход при построении разверток. Здесь основные методы, развитые в работе, а именно, развертки РСП, развертки РСП, расширенных временными конструкциями, и развертки РСП, расширенные спецификациями эквивалентности, применяются одновременно. В диссертации также показана возможность применения метода проверки моделей к РСП, расширенным спецификациями эквивалентности и временной моделью, основанной на временных штампах.

Практическая часть данной работы состоит в применении методов проверки моделей к раскрашенным сетям Петри. Данная часть включает применение стандартного метода проверки моделей для логики мю-исчисления к РСП и реализацию описанного в работе метода проверки моделей для LTL логики с использованием разверток РСП. Для применения первого подхода была реализована система PNV. В системе PNV процесс верификации РСП является полностью автоматическим и требует задания спецификации сети и формул во входных языках системы. Реализованная система проверки моделей с использованием разверток является прототипной реализацией и требует выполнения некоторых операций вручную. Цель реализации данной системы была показать принципиальную возможность и целесообразность использования данного метода на практике и дать несколько примеров верификации моделей распределенных систем. В дипломной работе [13] описана полная реализация системы проверки моделей для РСП с применением разверток, не использующая отношение эквивалентности и временные конструкции, которая базируется на предложенных в данной диссертации методах.

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

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

1. International Conference on Parallel Computing in Electrical Engineering (PARELEC

2002), Warsaw, Poland.

2. 4th International Conference of Perspectives of System Informatics (PSI'01), Novosibirsk,

Russia, 2001.

3. 5th International Workshop on Concurrency, Specification and Programming, Warsaw,

Poland, 2001.

4. Четвертый Сибирский Конгресс no Прикладной и Индустриальной Математике

ИНПРИМ - 2000), Новосибирск, Россия, 2000.

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

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

Структура работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы из 57 наименований. Содержание составляет 85 страниц. Работа включает 26 иллюстраций и 4 таблицы.

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

Заключение

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

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

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

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

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

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

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

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

2. Бандман О Л. Проверка корректности сетевых протоколов с помощью сетей Петри. Автоматика и вычислительная техника. N 6. 1986. с. 82-91.

3. Вирбицкайте И.Б., Покозий Е.А. Использование техники частичных порядков для верификации временных сетей Петри. Программирование N 1.1999. с.28 — 41.

4. Коз юра В.Е. Реализация системы проверки моделей раскрашенных сетей Петри с использованием разверток. Препринт N 94. Новосибирск 2002. 32 стр.

5. Козюра В.Е., Непомнящий В.А., Новиков P.M. Верификация раскрашенных сетей Петри методом проверки моделей. Препринт N 89. Новосибирск 2001. 24 стр.

6. Козюра В.Е., Новиков P.M. Использование метода проверки моделей для верификации коммуникационных протоколов, представленных раскрашенными сетями

7. Петри. Четвертый сибирский конгресс по прикладной и индустриальной математике (ИНПРИМ 2000). Тезисы докладов. Часть V. Стр. 44.

8. Козюра В.Е., Новиков Р.М. Верификация коммуникационных протоколов с использованием системы PNV. Материалы молодежной научной конференции, посвященной 10-летию ИВТ СО РАН, Новосибирск, Академгородок, 25 26 декабря, 2000.

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

10. Соколов В.А., Легалов А.И. Применение сетей Петри для анализа программ, написанных на языке параллельного программирования. Моделирование и анализ информационных систем. Ярославский государственный университет. N 1. 1993. с. 27 -44.

11. Чаплыгин С.М. Верификация распределенных систем, представленных раскрашенными сетями Петри, методом проверки моделей. Выпускная квалификационная работа. НГУ. Новосибирск 2003.

12. Abdulla А.Р., Purushothaman I., Nylen A. Unfoldings of Unbounded Petri Nets. Proc. of CAV 2000. Lect. Notes Comput. Sci. 2000. Vol. 1855. P. 495-507.

13. Anisimov N.A., Kovalenko A.A., Postupalski P.A. Two-levels Formal Model for Protocol Specification Based on Petri Nets. Proc. IFIP TC6 Intern. Symp. Network Information Systems. Bulgaria, 1993. P. 143 -154.

14. Bieber В., Fleischhack H. Model Checking of Time Petri Nets Based on Partial Order Semantics. Proc. CONCUR'99. Lect. Notes Comput. Sci. 1999. Vol. 1664. P. 210-225.

15. Bodin E.V., Kozura V.E., Shilov N.V. Experiments with Model Checking for ц-Calculus in specification and verification project REAL. Proceedings of the Fifth New Zealand Formal Program Development Colloquium. 1999. P. 1-18.

16. Cheng A., Christensen S., Mortensen К. H. Model Checking Coloured Petri Nets Exploiting Strongly Connected Components. DAIMIPB 519, March 1997.

17. Clarke E.M., Grumberg O., Peled D.A. Model Checking, MIT Press, 1999.

18. Cleaveland R., Klein M., Steffen B. Faster Model Cheking for Modal Mu-Calculus. Proc of CAV-92, Mjntreal, Canada. Lect. Notes Comput. Sci. 1992. Vol. 663. P. 410-422.

19. Cohen R., Segall A. An efficient reliable ring protocol. IEEE Transact. Communs. 1991. Vol.39, N.ll.P.l 616-1624.

20. Couvreur J.-M., Grivet S., Poitrenaud D. Designing an LTL Model-Checker Based on Unfolding Graphs. Lect. Notes Comput. Sci. 2000. Vol. 1825. P. 123-145.

21. Engelfriet J. Branching Processes of Petri Nets. Acta Informatica. 1991. Vol. 28. P. 575591.

22. Esparsa J. Model-Checking Using Net Unfoldings. Lect. Notes Comput. Sci. 1993. Vol. 668. P. 613-628.

23. Esparsa J., Romer S., Volger W. An Improvement of McMillan's Unfolding Algorithm. Proc. TACAS'96. Lect. Notes Comput. Sci. 1997. Vol. 1055. P. 87-106.

24. Esparsa J., Romer S. An unfolding algorithm for synchronous product of transition systems. In Proc. of CONCUR'99. Lect. Notes Comput. Sci. 1999. Vol. 1664. P. 2-20.

25. Esparza J., Heljanko K. A New Unfolding Approach to LTL Model-Checking. Lect. Notes Comput. Sci. 2000. Vol. 1853. P. 475^86.

26. Esparza J., Heljanko K. Implementing LTL Model Checking with Net Unfoldings. Lect. Notes Comput. Sci. 2001. Vol. 2057. P. 37-56.

27. Farwer В., Lomazova I. A Systematic Approach towards Object-based Petri Net Formalisms Proc.PSI 2001, Lecture Notes Comput. Sci. 2001. Vol. 2244. P. 255-267.

28. Gerth R., Peled D., Vardi M., Wolper P. Simple On-the-fly Automatic Verification of Lineal Temporal Logic. In Protocol Specification, Testing, and Verification PSTV'95. 1995. P. 3-18.

29. Godefroid P., Wolper P. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2). 1993. P. 149-164.

30. Graves B. Computing reachability properties hidden in finite net unfoldings. Lect. Notes Comput. Sci. 1997. Vol. 1346. P. 327-341.

31. Heljanko K. Model Checking with Finite Complete Prefixes is PSPACE-Complete. Proc. of CONCUR'2000. Lect. Notes Comput. Sci. 2000. Vol. 1877. P. 108-122.

32. Holzmann G. I. Design and validation of computer protocols. Englewood Cliffs, NJ: Prentice Hall, 1991.

33. Jensen K. Coloured Petri Nets. Vol. 1. — Berlin a.o.: Springer, 1995.

34. Jensen K. Coloured Petri Nets. Vol. 2. — Berlin a.o.: Springer, 1995.

35. Kaivola R. Using compositional preorders in the verification of sliding window protocol. In Proc. of CAV'97, Lecture Notes Comput. Sci. Vol. 1254, P. 48-59.

36. Khomenko V., Koutny M., Vogler W. Canonical Prefixes of Petri Net Unfoldings. Proc. of CAV 2002, Lecture Notes Comput. Sci. 2002. Vol. 2404, P. 582=59^—

37. Kozura V.E. Unfoldings of Coloured Petri Nets. Tech. Rep. N80. Novosibirsk 2000. 34 pages.

38. Kozura V.E. Unfoldings of Coloured Petri Nets. Proc. of Perspectives of System Informatics 2001 (PSI'01), Lect. Notes Comput. Sci. 2001. Vol 2244. P. 268-278.

39. Kozura V.E. Unfoldings of Timed Coloured Petri Nets. Tech. Rep. N82. Novosibirsk 2001. 33 pages.

40. Kozura V.E. Unfoldings of Timed Coloured Petri Nets. Proceedings of the Workshop on Concurrency, Specification and Programming 2001 (CS&P'2001) Warsaw 3-5 October 2001. P. 128-139.

41. Kozura V.E. LTL model checking of coloured Petri nets based on net unfoldings. Joint Bulletin of,the Novosibirsk Computing Center and A.P.Ershov Institute of Informatics Systems, Series: Computer Science, V.15. Novosibirsk, 2001. P. 83-101.

42. Kristensen L.M., Christensen S., Jensen K. The practitioner's guide to coloured Petri nets. Intern. Journal on Software Tools for Technology Transfer. 1998. Vol.2, N 2. P. 98-132.

43. Lamport L. What good is temporal logic? Information Processing 83.1983. P.657-668.

44. McMillan K.L. Using Unfolding to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. Lect. Notes Comput. Sci. 1992. Vol.663. P. 164-174.

45. McMillan K.L. A technique of a state space search based on unfoldings. Formal Methods in System Design, 6(1). 1995. P. 45-65.

46. Melzer S., Romer S. Deadlock Checking Using Net Unfoldings. Proc. of the Conf. on Computer Aided Verification (CAV'97), Haifa 1997. Lect. Notes Comput. Sci. Vol.1254. P. 352-363.

47. Mueller-Olm M., Schmidt D., Stefen B. Model-Checking. A Tutorial Introduction. Lect. Notes Comput. Sci. 1999. Vol. 1694. P. 330-354.

48. V. A. Nepomniaschy, Nikolay V. Shilov, E. V. Bodin, Vitaly E. Kozura: Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems. IFM 2002. P. 69-88.

49. Schmidt K. How to calculate symmetries of Petri nets. Acta Informatica 36. 2000. P. 545590.

50. Valmari A. The State Explosion Problem. Lect. Notes Comput. Sci. 1998. Vol. 1491. P. 429528.

51. Valmari A. Stubborn Sets of Coloured Petri Nets. Proc. of the 12th Intern. Conf. on Application and Theory of Petri Nets. Gjern, 1991. P. 102-121.

52. Vardy M.Y., Wolper P. An automata-theoretic approach to automatic program verification. In Proc. of 1st IEEE Symp. on Logic in Computer Science. 1986. P. 322-331.

53. Wallner F. Model-Checking LTL Using Net Unfoldings. Proc. of the Conf. on Computer Aided Verification (CAV'95), Vancouver, 1995. Lect. Notes Comput. Sci. 1998. Vol. 1427. P. 207-218.