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

• Кузьмин, Егор Владимирович
• кандидат наук
• 2010

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

Содержание

Введение

Глава 1. Структурированные системы помеченных переходов

1.1. Мультимножество и квазипорядок

1.2. Структурированные системы помеченных переходов

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

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

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

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

1.2.5. Совместимость по убыванию

Глава 2. Автоматные структурированные системы переходов

2.1. Определение

2.2. Семантические свойства

2.3. Темпоральные свойства

2.4. Заключение к главе

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

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

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

3.3. Заключение к главе

Глава 4. Счетчиковые машины Минского

4.1. Счетчиковые машины Минского

4.2. Двухсчетчиковые машины

4.2.1. Неразрешимые проблемы

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

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

4.3. Однорегистровые машины

4.4. Односчетчиковые машины

4.4.1. Односчетчиковые машины

4.4.2. Свойства односчетчиковых машин

4.4.3. Алгоритм представления исполнения

4.4.4. Обоснование алгоритма и трудоемкость

4.4.5. Проблемы тотальности

4.5. Заключение к главе

Глава 5. Слабые счетчиковые машины

5.1. Счетчиковые машины с потерями

5.1.1. Отношения потери

5.1.2. Ограниченность для счетчиковых машин с потерями

5.1.3. Ограниченность для двухсчетчиковых машин

с обнулениями

5.2. Слабые счетчиковые машины

5.3. Заключение к главе

Глава 6. Автоматные счетчиковые машины

6.1. Автоматные счетчиковые машины

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

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

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

6.5. Автоматные счетчиковые машины малой размерности

6.5.1. Автоматная 3-счетчиковая машина с неполулинейным множеством достижимости

6.5.2. Автоматные односчетчиковые машины

6.6. Автоматные счетчиковые машины с ограничениями

6.7. Заключение к главе

Глава 7. Языки автоматных счетчиковых машин

7.1. Автоматная счетчиковая машина-распознаватель

7.2. Основные теоремы по проблемам пустоты

и распознавания слов

7.3. Свойства замкнутости

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

Глава 8. Моделирование, спецификация и верификация «автоматных» программ

8.1. Введение

8.2. Иерархическая модель автоматных программ

8.3. Автоматная модель системы управления кофеваркой

8.4. Спецификация и верификация автоматных моделей

8.5. Структура Крипке автоматной модели

8.6. Темпоральная логика LTL

8.7. Темпоральная логика CTL

8.8. Темпоральные свойства автоматных моделей

8.9. Редукция модели

8.10. Практическая реализация

8.11. Автоматные модели систем реального времени

8.12. Применение метода формальных утверждений о трассах

8.13. Заключение к главе

Заключение

Литература

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

Введение

Актуальность работы. Современный период развития информатики и вычислительной техники характеризуется широким использованием параллельных и распределенных систем (вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов), поведение которых отличается высокой степенью сложности. Это обстоятельство выдвигает новые задачи в области моделирования и анализа корректности таких систем. Под корректностью понимается полное соответствие системы задачам, для которых она создаётся. Корректность определяется абстрактным образом в соответствии с формальной спецификацией, описывающей желаемое поведение системы. Процесс проверки соответствия поведения системы требованиям, заданным в спецификации, называется верификацией [14, 18, 22, 65].

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

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

Многочисленные методы и средства анализа параллельных и распреде-

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

Для того чтобы преодолеть этот недостаток, были разработаны методы, применимые, по крайней мере, для некоторых ограниченных классов систем с бесконечным числом состояний. Можно упомянуть здесь работы, например, П. Абдуллы, К. Чёранса, А. Финкеля, Б. Йонссона, Ф. Моллера, Ф. Шнебле-на [79, 115, 152]. Более того, оказалось, что метод проверки модели, широко используемый при автоматической верификации систем с конечным числом состояний, может быть применен для некоторых классов систем с бесконечным числом состояний и подмножеств темпоральных логик [92, 93, 110-112].

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

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

дены новые формализмы для описания бесконечных систем переходов.

Примерами формальных моделей (систем переходов с бесконечным числом состояний), позволяющих описывать параллельные и распределенные системы, являются сети Петри [19, 66], базовые параллельные процессы (ВРР — Basic Parallel Processes) [97], системы с каналами, теряющими сообщения (LCS — Lossy Channel Systems) [80, 81], автоматы реального времени (RealTime Automata) [84] и др.

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

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

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

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

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

Ранее в ряде публикаций таких авторов, как А. Буаджани, О. Буркарт, X. Эспарза, Р. Майр [92, 93, 110, 112], исследовались вопросы применимости метода проверки модели для некоторых формализмов, модели в рамках которых могут быть рассмотрены как вполне структурированные системы переходов, а именно: сетей Петри, ВРР, систем сложения векторов с потерями (ЬУАЯ). В данной же работе, исходя из позиции обобщения, акцентируется внимание на проблеме разрешимости темпоральных свойств для класса вполне структурированных систем помеченных переходов в целом.

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

класс автоматных структурированных систем переходов, особенностью которого является одновременное выполнение свойств совместимости по возрастанию и совместимости по убыванию правильного квазипорядка с отношением переходов. В литературе практически не уделяется внимание системам переходов этого класса (за исключением систем переходов с конечным числом состояний). Тем не менее, как будет показано в данной работе, формализмы, порождающие автоматные структурирвоанные системы переходов могут быть достаточно выразительными и нетривиальными. Для демонстрации этого факта в диссертации предлагается специальный фрагмент алгебры процессов, построенный на основе таких хорошо известных алгебр процессов, как CCS (Calculus of Communicating Systems — исчисление взаимодействующих систем) Милнера [151] и SCP (Communicating Sequential Processes — взаимодействующие последовательные процессы) Хоара [129], позволяющий строить формальные модели (параллельных и распределенных систем), которые могут быть рассмотрены как автоматные структурированные системы переходов.

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

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

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

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

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

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

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

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

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

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

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

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

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

Апробация работы. Результаты диссертации докладывались на Международном симпозиуме «Temporal Representation and Reasoning» (Tatihou, Франция, 2004), Международном семинаре «Распределенные информационно-вычислительные ресурсы и математическое моделирование» (Новосибирск, 2004), Международном семинаре «Program Understanding» (Новосибирск — Алтай, 2003, 2009), Всероссийской научной конференции, посвященной двухсотлетию ЯрГУ им. П. Г. Демидова (2003), Всероссийской научной конференции «Методы и средства обработки информации» (Москва, МГУ, 2005, 2009), Научно-методической конференции преподавателей математического факультета и факультета ИВТ ЯрГУ им. П. Г. Демидова (2007), семинаре «Go4IT — шаг к новым технологиям Интернета» (Москва, Институт системного программирования РАН, 2007), Областной научно-методической конференции (Ярославль, ЯрГУ, 2007), Международной научной конференции «Образование, наука и экономика в вузах. Интеграция в международное образовательное пространство» (Польша, Плоцк, 2008), Международной научно-практической конференции «Информационно-коммуникативная культура: наука и образование» (Ростов-на-Дону, 2009), Международной конференции «Компьютерные науки и информационные технологии» (Саратов, 2009), Междуна-

родном рабочем совещании «Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010)» (Казань, 2010), семинаре Института программных систем им. А.К. Айламазяна РАН, семинаре кафедры распределенных вычислений и компьютерных сетей СПбГПУ, семинаре «Теоретические основы информатики» кафедры информатики ТвГУ (2010), семинаре «Моделирование и анализ информационных систем» кафедры теоретической информатики ЯрГУ им. П. Г. Демидова (2001-2010).

Гранты. Работа по теме диссертации проводилась в соответствии с планами исследований по проектам, поддержанными следующими грантами: РФФИ №99-01-00-309 «Методы моделирования, анализа и верификации распределенных систем», №03-01-00-804 «Разработка новых методов и средств моделирования и анализа процессов обработки информации в распределенных системах», №07-01-00702а «Разработка формальных моделей распределенных систем и исследование их семантических свойств», №05-07095008 (публикация монографии «Структурированные системы переходов»), Федеральная целевая программа «Интеграция», гранты ФАНИ №2007-4-1.4-18-02-041 «Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода» ФЦП «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007—2012 годы», №2009-1.1-113-050-013 «Разработка фундаментальных принципов и инновационных прикладных методов для моделирования, анализа и верификации информационных систем» ФЦП «Научные и научно-педагогические кадры инновационной России на 2009-2013 годы».

Авторские свидетельства. Свидетельство об официальной регистрации программы для ЭВМ «Система моделирования и анализа автоматных программ», Федеральная служба по интеллектуальной собственности, патентам и товарным знакам, №2007611856. Зарегистрировано в Реестре программ

для ЭВМ 7 мая 2007 г. Правообладатель: Ярославский госуниверситет им. П.Г. Демидова. Авторы: Е. В. Кузьмин, P.A. Виноградов, В. А. Соколов.

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

Публикации. Материалы диссертации опубликованы в 41 печатной работе, из них 11 статей в журналах из перечня ВАК, 9 статей в рецензируемых журналах, не вошедших в этот перечень, 13 статей в сборниках трудов конференций и 3 тезисов докладов, 4 учебных пособия (1 с грифом УМО) и 1 монография (изд-во «Физматлит»). Получено 1 свидетельство о регистрации программы для ЭВМ.

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

Глава 1

Структурированные системы помеченных переходов

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

Глава написана на основе источников [37, 59, 115].

1.1. Мультимножество и квазипорядок

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

Пусть X — это некоторое множество. Тогда мультимножеством т над X называется функция

где N — множество целых неотрицательных чисел.

Полагаем хеш, если т(х) > 0, и х ф т, если т(х) = 0. Для х е X значение т(х) называют кратностью, или числом вхождений, х в т.

В том случае, когда Ух е X : т(х) ^ 1, т является обычным множеством. Мощность мультимножества определяется как

\т\ =

Мультимножество конечно, если для всех х £ X, за исключением, может быть, конечного их числа, имеем т(х) = 0. В дальнейшем будем рассматривать только конечные мультимножества. Множество всех конечных мультимножеств над множеством X обозначим через М(Х).

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

Операции и отношения теории множеств естественным образом расширяются на конечные мультимножества.

Пусть т1,т2 £ М(Х), х е X, X' С X и к <Е N. Полагаем

(mi + т2)(х) = mi (ж) + т2(х), (к • mi)(ж) — к • mi(x),

dcf

(mi - 7712) (ж) = mi (ж) 0 тг(ж) = тах(0, mi (ж) - 7712(0;)), (mi U 7712)(ж) = max(mi(x), тг(ж)), (mi П тг)(ж) = min(mi(ж), 7712(2?)),

mi с 7772 Ух £ X : 77li(ж) < "72(ж),

Символ 0 обозначает пустое мультимножество, т. е. такое мультимножество те М(Х), что т(ж) = 0 для всех х.

Бинарное отношение Е называется отношением частичного порядка, если оно рефлексивно (хЯх), транзитивно (хИу Л у Яг => хЯг) и антисимметрично (жЛт/ Л г/Лж =>■ х = у).

\/n,ke N: п 0 /с = тах(0,77 - к).

Если отношение только рефлексивно и транзитивно, то оно называется отношением квазипорядка, или предпорядка.

Вместо xRy обычно пишут х у или просто х ^ у. Будем также говорить, что множество X, являющееся носителем отношения R, частично упорядочено (или квазиупорядочено), не указывая явно отношения R, если из контекста ясно, о каком упорядочении идет речь. Если х ^ у и у ^ ж, то пишут х < у и говорят, что х строго меньше у. Очевидно, что строгий порядок есть транзитивное и иррефлексивное отношение.

Частично упорядоченное множество, в котором любые два элемента сравнимы, называется линейно упорядоченным, или цепью.

Подмножество У квазиупорядоченного множества (X, называется антицепью, если элементы У попарно несравнимы, т. е. для любой пары элементов х Ф у из У не выполняется ни х ^ у, ни у ^ х.

Элемент а квазиупорядоченного множества X называется минимальным элементом этого множества, если в X нет ни одного элемента х, удовлетворяющего условию х < а.

Квазипорядок R на множестве X называется фундированным, или квазипорядком с условием минимальности (well-founded), если всякое непустое подмножество множества X имеет минимальный (в этом подмножестве) элемент. Это эквивалентно тому, что в X нет бесконечно строго убывающих цепей вида xq > х\ > Х2 > ■ ■ ■ ■

Квазипорядок ^ на множестве X называется правильным (well-quasi-ordering), если для любой бесконечной последовательности xq, Xi, ...

элементов из X существуют индексы г < j такие, что хъ ^ Xj.

Утверждение 1.1. Квазипорядок ^ на множестве X является правильным в том и только том случае, когда одновременно выполняются два следующих условия:

1) множество X не содержит бесконечных строго убывающих цепей > х\ > Х2 > .. •;

2) всякая содержащаяся в X антицепь конечна.

Доказательство см., например, в [59]. □

Следствие 1.1.

1. Любой правильный квазипорядок является фундированным.

2. Для линейного порядка условия правильности и фундируемости являются эквивалентными.

Утверждение 1.2. Пусть отношение < — правильный квазипорядок на множестве X. Тогда всякая бесконечная последовательность хо, х\, х2, . ■ ■ элементов из множества X содержит бесконечную монотонно возрастающую подпоследовательность Х{0 ^ х^ ^ жг-2 ^ ..., где го < ч < %2 < ■ • • •

Доказательство см., например, в [115]. □

Пусть отношение ^ — правильный квазипорядок на множестве X. Идеалом, или замкнутым кверху множеством, называется подмножество / С1 такое, что для х € I, у X и х ^у следует, что у € /.

Пусть ^ — правильный квазипорядок на X. Замкнутым книзу множеством называется подмножество / С1 такое, что для х£1,уеХих^у следует, что у £ /.

Идеал может быть получен замыканием кверху некоторого множества. Каждый элемент х £ X порождает идеал ]х {у | у > ж}.

Базисом замкнутого кверху множества I называется множество пнп(/) такое, что I = ижбшт(1) Следующее свойство впервые было установлено Хигманом.

Утверждение 1.3 ([127]). Если отношение < — это правильный квазипорядок на множестве X, то всякий идеал I имеет конечный базис.

Далее нам понадобится следующее свойство идеалов.

Утверждение 1.4. Если отношение ^ —- это правильный квазипорядок на множестве X, то любая бесконечно возрастающая по отношению вложения множеств последовательность /о С 1\ С /2 С ... идеалов стабилизируется, т. е. найдется такое к € Н, что 1к — Ь+1 — Ь+2 — —

Доказательство см., например, в [115]. П

Пусть отношение ^ — некоторый квазипорядок на множестве X. Отношение ^п на множестве Хп векторов размерности п с элементами из X определим, полагая для х, у е Хп, х = (х\,х2,..., У = (У1,У2, • • •, Уп), х у в том и только том случае, когда Уг, 1 < г < п: Х{ ^ у{.

Утверждение 1.5 ([106]). Пусть отношение < — правильный квазипорядок на множестве X. Тогда отношение на множестве векторов размерности п из Хп также является правильным квазипорядком.

Это утверждение известно как лемма Диксона.

Необходимо отметить, что не является линейным порядком на Хп, даже если < — линейный порядок на X.

Если X — конечное множество, на котором задан некоторый порядок, то из утверждения 1.5 следует

Утверждение 1.6. Отношение С на множестве М(Х) является правильным квазипорядком.

Доказательство. Для двух мультимножеств т\,т2 £ М(Х)

ггц С т2 Ух е Х\ тг(х) < т2(х).

19

Поскольку элементы множества X упорядочены, то мультимножества т е М(Х) можно рассматривать как векторы вида (т^х),.. .,т(хп)), где п — |Х|. п

1.2. Структурированные системы помеченных переходов

Система помеченных переходов — одна из наиболее распространенных моделей для описания поведения различных систем (в том числе параллельных и распределенных).

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

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

Система помеченных переходов представляет собой набор из четырех элементов ЬТЯ = (5, Г, —«о), где

• 5 — множество состояний с элементами 5о, «1, «2, • • •,

• Т — некоторый конечный алфавит пометок (множество имен действий),

• —»с (в хТ х Б) — отношение перехода между состояниями системы,

• йо £ £ — начальное состояние системы.

Переход (з, з') обычно записывается как з Л э' и означает, что действие с именем £ переводит состояние 5 в состояние в'. Состояние в' в этом случае называется по следующим, или просто последующим для б, а состояние 5 — предыдущим, или просто предыдущим для в'. Состояния, не имеющие последующих состояний, называются финальными.

Через Succ(s) обозначается множество последующих состояний для s, через Pred(s) — множество его предыдущих состояний.

Система LTS будет конечно ветвящейся, если для любого s множество Succ(s) конечно. Далее будут рассматриваться системы переходов, имеющие только конечное ветвление.

Система помеченных переходов LTS имеет вычислимое отображение Succ (coot. Pred), если существует эффективная процедура вычисления множества Succ(s) (coot. Pred(s)) для любого состояния s.

Последовательное исполнение для LTS есть конечная или бесконечная

j. J.

цепочка переходов s0 ^ si -A s2 —> ..., где s0 — начальное состояние системы. Запись s Д s' означает, что имеется (конечная) последовательность переходов, переводящая состояние s в состояние s'.

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

Литература

[1] Анисимов H.A., Голенков Е.А., Харитонов Д.И. Композициональный подход к разработке параллельных и распределенных систем на основе сетей Петри // Программирование. 2001. №6. С. 30-43.

[2] Анишев П. А., Бандман О. JI. Алгоритмы и программы анализа свойств сетей Петри. Новосибирск, ВЦ СО АН СССР, 1988.

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

[4] Валиев М. К., Дехтярь М. И., Диковский А. Я. Системы агентов, управляемых логическими программами: сложность верификации // Программирование. 2009. №5. 22 с.

[5] Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Ч. 2: Языки и исчисления. М.: МЦНМО, 2002. 288 с.

[6] Вирбицкайте И. Б. Семантические модели в теории параллелизма. Новосибирск, 2000. 190 с.

[7] Воеводин В. В., Воеводин Вл. В. Параллельные вычисления. СПб.: БХВ-Петербург, 2002. 608 с.

[8] Гинзбург С. Математическая теория контекстно-свободных языков. М.: Мир, 1970. 328 с.

[9] Гинзбург С., Грейбах Ш. Абстрактные семейства языков // Сборник «Языки и автоматы». М.: Мир, 1975. С. 233-281.

[10] Грис Д. Наука программирования. Пер. с англ. М.: Мир, 1984. 416 с.

[11] Дурнев В. Г. Элементы математической логики. Ярославль, 2006. 221 с.

[12] Захаров В. А., Коннов И. В. Об одном подходе к верификации симметрических параметризованных распределенных систем // Программирование. 2005. №5. С. 3-17.

[13] Захаров В. А., Царьков Д. В. Эффективные алгоритмы проверки выполнимости формул темпоральной логики CTL и их применение для верификации параллельных программ // Программирование. №4. С. 3—18.

[14] Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.

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

[16] Карп Р. М., Миллер Р. Е. Параллельные схемы программ // Кибернетический сборник. Вып. 13 (новая серия). М.: Мир, 1976. С. 5-61.

[17] Кессель C.B. Разработка системы управления кофеваркой на основе автоматного подхода. СПбГУ ИТМО, 2003. http://is.ifmo.ru/projects/coffee2/

[18] Кларк, Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. M.: МЦНМО, 2002. 416 с.

[19] Котов В.Е. Сети Петри. М.: Наука, Физматлит, 1984. 160 с.

[20] Котов В. Е., Сабельфельд В. К. Теория схем программ. М.: Наука, Физматлит, 1991. 248 с.

[21] Кузьмин Е. В. Счетчиковые машины. Уч. пособие. Ярославль, ЯрГУ, 2010. 128 с.

[22] Кузьмин Е. В. Верификация моделей программ. Уч. пособие. Ярославль, ЯрГУ, 2008. 176 с.

[23] Кузьмин Е. В. Проблема ограниченности для счетчиковых машин с потерями // Моделирование и анализ информационных систем. Ярославль, 2008. Т. 15, №3. С. 14-27.

295

[24] Кузьмин Е. В. Верификация программ // Сборник материалов IX областной научно-методической конференции «Актуальные проблемы совершенствования подготовки специалистов в вузе». Ярославль, ЯрГУ, 2007. С. 18-21.

[25] Кузьмин Е. В. Введение в теорию вычислительных процессов и структур. Уч. пособие. Ярославль, ЯрГУ, 2006. 140 с.

[26] Кузьмин Е. В. Иерархическая модель автоматных программ // Моделирование и анализ информационных систем. Ярославль, 2006. Т. 13, №1. С. 27-34.

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

[28] Кузьмин Е.В. Недетерминированные счетчиковые машины // Моделирование и анализ информационных систем. Ярославль, 2003. Т. 10, №2. С. 41-49.

[29] Кузьмин Е. В. О разрешимости задачи проверки модели для модального /¿-исчисления и некоторых классов вполне структурированных систем переходов // Моделирование и анализ информационных систем. Ярославль, 2003. Т. 10, №1. С. 50-55.

[30] Кузьмин Е.В. Верификация графов потоков данных с использованием символьной проверки модели для СТЬ // Моделирование и анализ информационных систем. Ярославль, 2001. Т. 8, №1. С. 38—43.

[31] Кузьмин Е. В., Васильева К. А. Верификация автоматных программ с использованием ЬТЬ // Моделирование и анализ информационных систем. Ярославль, 2007. Т. 14, №1. С. 3-14.

[32] Кузьмин Е. В., Рубцов С. А. Модели и инструментальные средства для разработки и анализа графов потоков данных // Материалы межвузовской научно-технической конференции «Управляющие и вычислительные системы», Вологда, ВоГТУ, 2000. С. 96-97.

[33] Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных программ» // Программирование. Москва, Наука, 2008. Т. 34, №1. С. 38-60.

[34] Кузьмин Е. В., Соколов В. А. О верификации «автоматных» программ // Сборник статей к 20-летию факультета ИВТ «Актуальные проблемы математики и информатики». Ярославль, ЯрГУ, 2007. С. 31—35.

[35] Кузьмин Е. В., Соколов В. А. О дисциплине специализации «Верификация программ» // Материалы II науч-но-методической конференции преподавателей математического факультета и факультета ИВТ ЯрГУ им. П.Г. Демидова «Преподавание математики и компьютерных наук в классическом университете». Ярославль, ЯрГУ, 2007. С. 91-101.

[36] Кузьмин Е. В., Соколов В. А. О некоторых подходах к верификации автоматных программ // Сборник докладов семинара «Со41Т — шаг к новым технологиям Интернета». Москва, Институт системного программирования, 2007. С. 43—48.

[37] Кузьмин Е. В., Соколов В. А. Структурированные системы переходов. Уч. пособие. М.: Наука, Физматлит, 2006. 176 с.

[38] Кузьмин Е. В., Соколов В. А. Вполне структурированные системы помеченных переходов. Монография. М.: Наука, Физматлит, 2005. 176 с.

[39] Кузьмин Е. В., Соколов В. А. Исследование свойств класса вполне структурированных систем переходов // Труды Второй Всероссийской

научной конференции «Методы и средства обработки информации». Москва, МГУ, 2005. С. 388-393.

[40] Кузьмин Е. В., Соколов В. А. Взаимодействующие раскрашивающие процессы // Моделирование и анализ информационных систем. Ярославль, 2004. Т. 11, №2. С. 8-17.

[41] Кузьмин Е. В., Соколов В. А. Проверка модели для вполне структурированных систем переходов автоматного типа // Материалы Международного рабочего совещания «Распределенные информационно-вычислительные ресурсы и математическое моделирование» (DICR'04). Новосибирск, 2004. С. 73-85.

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

[43] Кузьмин Е. В., Соколов В. А., Виноградов P.A. Система моделирования и анализа автоматных программ. Свидетельство об официальной регистрации программы для ЭВМ №2007611856. Федеральная служба по интеллектуальной собственности, патентам и товарным знакам. Зарегистрировано в Реестре программ для ЭВМ 7 мая 2007 г. Правообладатель: Ярославский госуниверситет им. П.Г. Демидова.

[44] Кузьмин Е.В., Соколов В.А., Виноградов P.A. Верификация автоматных программ средствами CPN/Tools // Моделирование и анализ информационных систем. Ярославль, 2006. Т. 13, №2. С. 4-15.

[45] Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. О языках автоматных счет-чиковых машин // Материалы Международного рабочего совещания «Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010)». Казань, 2010. С. 70-75.

298

[46] Кузьмин Е.В., Соколов В. А., Чалый Д.Ю. Проблемы ограниченности счетчиковых машин Минского // Программирование. Москва, Наука, 2010. Т. 36, М. С. 3-10.

[47] Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Формальное построение автоматных программ // Труды Третьей Всероссийской научной конференции «Методы и средства обработки информации». Москва, МГУ, 2009. С. 130-135.

[48] Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Об одном формальном подходе к построению автоматных программ // Труды межд. конференции «Компьютерные науки и информационные технологии». Саратов, 2009. С. 239-240.

[49] Кузьмин Е.В., Соколов В.А., Чалый Д.Ю. Применение метода формальных утверждений о трассах для спецификации, построения и верификации автоматных программ // Программирование. Москва, Наука, 2009. Т. 35, №1. С. 61-77.

[50] Кузьмин Е.В., Соколов В.А., Чалый Д.Ю. Автоматные счетчиковые машины // Сб. статей международной научно-практической конференции «Информационно-коммуникативная культура: наука и образование». Ростов-на-Дону, 2009. С. 321-325.

[51] Кузьмин Е.В., Соколов В. А., Чалый Д.Ю. Проблемы ограниченности счетчиковых машин Минского // Доклады Академии наук. Москва, 2008. Т. 421, №6. С. 741-743.

[52] Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Об одном классе алгоритмических проблем для машин Минского // Сборник материалов международной научной конференции «Образование, наука и экономика в вузах. Интеграция в международное образовательное пространство». Польша, Плоцк, 2008. С. 536-537.

[53] Кузьмин Е. В., Чалый Д. Ю. О языках автоматных счетчиковых машин // Моделирование и анализ информационных систем. Ярославль, 2010. Т. 17, №2.

[54] Кузьмин Е. В., Чалый Д. Ю. О множестве достижимости автоматных счетчиковых машин // Моделирование и анализ информационных систем. Ярославль, 2010. Т. 17, №1. С. 52-64.

[55] Кузьмин Е.В., Чалый Д.Ю. О множестве достижимости автоматных трехсчетчиковых машин // Моделирование и анализ информационных систем. Ярославль, 2009. Т. 16, №3. С. 77-84.

[56] Кузьмин Е.В., Чалый Д.Ю. Об одном классе счетчиковых машин // Моделирование и анализ информационных систем. Ярославль, 2009. Т. 16, №2. С. 75-82.

[57] Кузьмин Е. В., Чалый Д.Ю. Алгоритмы для проблемы ограниченности счетчиковых машин // Моделирование и анализ информационных систем. Ярославль, 2008. Т. 15, №4. С. 42-55.

[58] Кузьмин Е. В., Чалый Д. Ю. О разрешимости проблем ограниченности для счетчиковых машин Минского // Моделирование и анализ информационных систем. Ярославль, 2008. Т. 15, №1. С. 16-26.

[59] Ломазова И. А. Вложенные сети Петри: моделирование и анализ распределенных систем с объектной структурой. М.: Научный мир, 2004.

[60] Ломазова И. А., Башкин В. А. Эквивалентность ресурсов в сетях Петри. М.: Научный мир, 2008. 208 с.

[61] Мальцев А. И. Алгоритмы и рекурсивные функции. 2-е изд. М.: Наука, Физматлит, 1986. 386 с.

[62] Матиясевич Ю. В. Диофантовость перечислимых множеств // Доклады Академии наук СССР. Москва, 1970. Т. 191, №2. С. 279-282.

300

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

[64] Непомнящий В. А., Аргиров В. С., Велоглазов Д. М., Быстров А. В., Четвертаков Е. А., Чурина Т. Г. Моделирование и верификация коммуникационных протоколов, представленных на языке SDL, с помощью сетей Петри высокого уровня // Программирование. 2008. №6.

[65] Непомнящий В. А., Рякин О. М. Прикладные методы верификации программ. М.: Радио и связь, 1988. 256 с.

[66] Питерсон Дж. Теория сетей Петри и моделирование систем. М.: Мир, 1984. 264 с.

[67] Поликарпова Н.И., Шалыто A.A. Автоматное программирование. Уч. пособие. СПбГУ ИТМО. Санкт-Петербург, 2007 г. 108 с.

[68] Роджерс X. Теория рекурсивных функций и эффективная вычислимость. М.: Мир, 1972. 624 с.

[69] Смелянский P. JI. Модель функционирования распределенных вычислительных систем // Вестник Московского Университета, сер. 15, Вычислительная Математика и Кибернетика. 1990. №3. С. 3-21.

[70] Солон Б. Я. Тотальные и ко-тотальные степени перечислимости // Известия высших учебных заведений. Математика. 2005. №9. С. 60-68.

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

[72] Шалыто А. А. Автоматное проектирование программ. Алгоритмизация и программирование задач логического управления // Известия академии наук. Теория и системы управления. 2000. №6. С. 63-81.

[73] Шалыто А. А. Алгоритмизация и программирование для задач логического управления и «реактивных» систем // Автоматика и телемеханика. Обзоры. 2001. №1. С. 3-39.

[74] Шалыто А. А. Switch-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998. 628 с.

[75] Шалыто А. А., Туккель Н.И. SWITCH-технология — автоматный подход к созданию программного обеспечения «реактивных» систем // Программирование. Москва, Наука, 2001. Т. 27, №5. С. 45-62.

[76] Шилов Н. В., Ануреев И. С., Бодин Е. В. О генерации условий корректности для императивных программ // Программирование. 2008. №6.

[77] Aho А. V. Indexed grammars — an extension of context-free grammars // Journal of the ACM. 1968. V. 15, №4. P. 647-671.

[78] Abdulla P. A., Bouajjani A., Jonsson B. On-the-fly Analysis of Systems with Unbounded, Lossy Fife Channels // Lecture Notes in Computer Science. Springer, 1998. V. 1427.

[79] Abdulla P. A., Cerans K., Jonsson В., Tsay Y.-K. General decidability theorems for infinite-state systems // Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996). IEEE Computer Society Press, 1996. P. 313-321.

[80] Abdulla P. A., Jonsson B. Verifying programs with unreliable channels // Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993). IEEE Computer Society Press, 1993. P. 160-170.

[81] Abdulla P. A., Jonsson B. Undecidable verification problems for programs with unreliable channels // Information and Computation. 1996. V. 130, №1. P. 71-90.

[82] Araki Т., Kasami T. Some Decision Problems Related to the Reachability Problem for Petri Nets // Theoretical Computer Science. 1976. V. 3, M. P. 85-104.

[83] Alur R., Dill D.L. A theory of timed automata // Theoretical Computer Science. 1994. V. 126, №2. P. 183-235.

[84] Alur R., Dill D.L. Automata-theoretic verification of real-time systems // Formal Methods for Real-Time Computing, Trends in Software Series. John Wiley and Sons Publishers, 1996. P. 55-82.

[85] Alur R., Coucoubetis C., Henzinger T. A., Ho P.-H., Nicollin X., Olivero A., Sifakis J., Yovine S. The algorithmic analysis of hybrid systems // Theoretical Computer Science. 1995. V. 138, №1. P. 3-34.

[86] Alur R., Coucoubetis C., Henzinger T. A., Ho P.-H. Hybrid Automata: An algorithmic approach to the specification and verification of hybrid systems // Lecture Notes in Computer Science. Springer, 1993. V. 736. P. 209-229.

[87] Alur R., Kannan S., Yannakakis M. Communicating hierarchical automata // Lecture Notes in Computer Science. Springer, 1999. V. 1644. P. 169-178.

[88] Baber R.L., Parnas D.L., Vilkomir S.A., Harrison P., O'Connor T. Disciplined methods of software specification: a case study // Int. Conf. on Information Technology: Coding and Computing. 2005. Vol. 2. P. 428-437.

[89] Bartussek W., Parnas D.L. Using assertions about traces to write abstract specifications for software modules // Lecture Notes in Computer Science. Springer, 1978. V. 65. P. 211-236.

[90] Bojanowski J., Iglewski M., Madey J., Obaid A. Functional Approach to Protocol Specification // Protocol Specification, Testing and Verification XIV. Chapman&Hall. 1995. P. 195-402.

[91] Bouajjani A., Habermehl P. Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations // Lecture Notes in Computer Science. Springer, 1997. V. 1256.

[92] Bouajjani A., Mayr R. Model Checking Lossy Vector Addition Systems // Lecture Notes in Computer Science. Springer, 1999. V. 1563.

[93] Burkart 0., Esparza J. More infinite results // Electronic Notes in Theoretical Computer Science. 1996.

[94] Campos S., Clarke E., Marrero W., Minea M. Verus: a tool for quantitative analysis of finite-state real-time systems // Workshop on Languages, Compilers and Tools for Real-Time Systems. 1995.

[95] Cece, G., Finkel A., Purushothaman I.S. Unreliable Channels are Easier to Verify than Perfect Channels // Information and Computation. 1996. V. 124, №1. P. 20-31.

[96] Chitic C., Rosu D. On validation of XML streams using finite state machines // WebDB. Paris, 2004. P. 85-90.

[97] Christensen S., Hirshfeld Y., Moller F. Bisimulation equivalence is decidable for basic parallel processes // Lecture Notes in Computer Science. Springer, 1993. V. 715. P. 143-157.

[98] Clarke E.M., Emerson E. A. Design and synthesis of synchronization skeletons using branching time temporal logic // Lecture Notes in Computer Science. Springer, 1981. V. 131. P. 52-71.

[99] Clarke E, Grumberg O, Peled D. Model Checking. The MIT Press, 2001.

[100] Cooper D.C. Theorem Proving in Arithmetic without Multiplication // Machine Intelligence. Edinburgh University Press, 1972. P. 91-100.

[101] CPNTools. http://www.daimi.au.dk/CPNTools/

[102] CADP — Construction and Analysis of Distributed Processes, http: //www.inrialpes.fr/vasy/cadp/

[103] Dekhtyar M. I., Dikovsky A. Ja., Valiev M.K. Applying temporal logic to analysis of behavior of cooperating logic programs // Lecture Notes in Computer Science. Springer, 2000. V. 1755. P. 228-234.

[104] Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K. On complexity of verification of interacting agent's behavior // Annals of Pure and Applied Logic. Elsevier, 2006. V. 141. P.336-362.

[105] Demri S., Lazic R., Sangnier A. Model checking freeze LTL over one-counter automata // Lecture Notes in Computer Science. Springer, 2008. V. 4962. P. 490-504.

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

[107] Dufourd C., Janear P., Schnoebelen Ph. Boundedness of Reset P/T nets // Lecture Notes in Computer Science. Springer, 1999. V. 1644. P. 301-310.

[108] Dufourd C., Finkel A., Schnoebelen Ph. Reset Nets Between Decidability and Undecidability // Lecture Notes in Computer Science. Springer, 1998. V. 1443. P. 103-115.

[109] Emerson E. A. Temporal and modal logic // Handbook of Theoretical Computer Science. 1990. V. B. P. 995-1072.

[110] Esparza J. Decidability of model-checking for infinite-state concurrent systems // Acta Informática. 1997. V. 34. P. 85-107.

[111] Esparza J. On the decidabilty of model checking for several //-calculi and Petri nets // Lecture Notes in Computer Science. Springer, 1994. V. 787. P. 115-129.

[112] Esparza J., Kiehn A. On the model checking problem for branching time

logics and basic parallel processes // Lecture Notes in Computer Science. Springer, 1995. V. 939. P. 353-366.

[113] Finkel A. Reduction and covering of infinite reachability trees // Information and Computation. 1990. V. 89, №2. P. 144-179.

[114] Finkel A., Leroux J. How to compose Presburger-accelerations: Applications to broadcast protocols // Lecture Notes in Computer Science. Springer, 2002. V. 2556. P. 145-156.

[115] Finkel A., Schnoebelen Ph. Well-Structured Transition Systems Everywhere! // Theoretical Computer Science. 2001. V. 256, №1-2. P. 63-92.

[116] Finkel A., Sangnier A. Reversal-bounded Counter Machines Revisited // Lecture Notes in Computer Science. Springer, 2008. V. 5162. P. 323-334.

[117] Finkel A., Schnoebelen Ph. Fundamental Structures in Well-Structured Infinite Transition Systems // Lecture Notes in Computer Science. Springer, 1998. V. 1380. P. 102-118.

[118] Finkel A., Sutre G. An Algorithm Constructing the Semilinear Post* for 2-Dim Reset/Transfer VASS // Lecture Notes in Computer Science. Springer, 2000. V. 1893. P. 353-362.

[119] Finkel A., Sutre G. Decidability of Reachability Problems for Classes of Two-Counter Automata // Lecture Notes in Computer Science. Springer, 2000. V. 1770. P. 346-357.

[120] Fischer M.J., Rabin M.O. Super-Exponential Complexity of Presburger Arithmetic // Proceedings of the SIAM-AMS Symposium in Applied Mathematics. 1974. V. 7. P. 27-41.

[121] Ginsburg S. Algebraic and Automata-Theoretic Properties of Formal Languages. Elsevier Science Inc., 1975.

[122] Ginsburg S., Greibach S. Abstract families of languages // «Studies in Abstract Families of Languages», Amer. Math. Soc. 1969. V. 87. P. 1-32.

[123] Hack M. Decision problems for Petri nets and vector addition systems. Project MAC Memo 59. Cambridge, 1975.

[124] Hack M. The equality problem for vector addition systems is undecidable // Theoretical Computer Science. 1976. V. 2, №. P. 77-96.

[125] Hennessy M. Algebraic Theory of Processes. MIT Press, 1988.

[126] Henzinger T. A., Kopke P.W., Puri A., Varaiya P. What's decidable about hybrid automata? // Proceedings of the 27th Annual Symposium on Theory of Computing (STOC). ACM Press, 1995. P. 373-382.

[127] Higman G. Ordering by Divisibility in Abstract Algebras // Proc. London Math. Soc. 1952. V. s3-2, №1. P. 326-336.

[128] HyTech. http://embedded.eecs.berkeley.edu/research/hytech/

[129] Hoare C. A. R. Communicating sequential processes. Prentice-Hall, 1985.

[130] Hoffman D.M. The Trace Specification of Communication Protocols // IEEE Tran. on Computers. 1985. V. C-34, № 12. P. 1102-1113.

[131] Hopcroft J. E., Pansiot J.-J. On the Reachability Problem for 5-Dimensional Vector Addition Systems. Computer science technical report. Cornell University, 1976. http://hdl.handle.net/1813/6102

[132] Ibarra 0. H. Reversal-Bounded Multicounter Machines and Their Decision Problems // Journal of the ACM. 1978. V. 25, №1. P. 116-133.

[133] Iglewski M., Kubica M., Madey J. Trace Specifications of Non-Deterministic Multi-Object Modules // Lecture Notes in Computer Science. Springer, 1995. V. 1023. P. 381-395.

[134] Iglewski M., Kubica M., Madey J. Editor for the Trace Assertion Method // Proc. 10th Int. Conf. of CAD/CAM, Robotics and Factories of the Future: CARs&FOF'94. Ottawa, 1994. P. 876-881.

[135] Janicki R., Khedri R. On a formal semantics of tabular expressions // Sei. Comput. Program. 2001. V. 39, № 2-3. P. 189-213.

[136] Janicki R., Sekerinski E. Foundations of the trace assertion method of module interface specification // IEEE Trans. Software Eng. 2001. V. 27, № 7. P. 577-598.

[137] Karp R. M., Miller R. E. Parallel Program Schemata // Journal of Computer and System Sciences. 1969. V. 3. P. 147-195.

[138] Kozen D. Results on the propositional /¿-calculus // Theoretical Computer Science. 1983. V. 27. P. 242-272.

[139] König D. Theorie der Endlichen und Unendlichen Graphen // Akademische Verlagsgesellschaft. Leipzig, 1936.

[140] Kouchnarenko O., Schnoebelen Ph. A model for recursive-parallel programs // Electr. Notes Theor. Comput. Sei. 1996. V. 5.

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

[142] Kuzmin E.V., Sokolov V.A., Chalyy D. Ju. Automaton Counter Machines // Proc. Int. Workshop on Program Understanding (sat. of PSI'09). 2009. P. 1-4.

[143] Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking /¿-Calculus in Well-Structured Transition Systems // Proc. 11th Int. Symposium on Temporal Representation and Reasoning. Tatihou, France, IEEE Press, 2004. P. 152-155.

[144] Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking //-Calculus in Well-Structured Transition Systems // Joint Bulletin of NCC k IIS, Comp. Science. Novosibirsk, 2004. №20. P. 49-59.

[145] KRONOS. http://www-verimag.imag.fr/TEMPORISE/kronos

[146] Lafourcade P., Lugiez D., Treinen R. Intruder deduction for AC-like equa-tional theories with homomorphisms // Lecture Notes in Computer Science. Springer, 2005. V. 3467. P. 308-322.

[147] Larsen K. Proof systems for satisfiability in Hennesy-Milner logic with recursion // Theoretical Computer Science. 1990. V. 72. P. 265-288.

[148] Leroux J., Sutre G. Flat counter almost everywhere! // Lecture Notes in Computer Science. Springer, 2005. V. 3707. P. 474-488.

[149] Mayr R. Lossy counter machines. TUM-I9827. Institut für Informatik, TUM, Germany, 1998.

[150] Milner R. A Calculus of Communicating Systems // Lecture Notes in Computer Science. Springer, 1980. V. 92.

[151] Milner R. Communication and Concurrency. Prentice-Hall Int., 1989.

[152] Moller F. Infinite results // Logic for Concurrency // Lecture Notes in Computer Science. Springer, 1996. V. 1119. P. 195-216.

[153] Moller F., Birtwistle G. Logic for Concurrency // Lecture Notes in Computer Science. Springer, 1996. V. 1043.

[154] Oppen D. C. A 2^ Upper Bound on the Complexity of Presburger Arithmetic // Journal of Computer and System Sciences. 1978. V. 16, №3. P. 323-332.

[155] Oppen D.C., Nelson G. A simplifier based on efficient decision algorithms // Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 1978. P. 141-150.

309

[156] Parnas D. L. Tabular representation of relations // CRL Report 260. Telecom. Research Institute. McMaster University. Ontario, Canada. 1992. 17 p.

[157] Parnas D. L., Vilkomir S. A. Precise Documentation of Critical Software // 10th IEEE High Assurance Systems Engineering Symposium. IEEE, 2007. P. 237-244.

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

[159] Peters D.K., Lawford M, Trancön-y-Widemann B. An IDE for software development using tabular expressions // Proc. of conference of the Centre for Advanced Studies on Collaborative Research(CASCON). Ontario, 2007. P. 248-251

[160] Pnueli A. The temporal logic of programs // FOCS'77. IEEE, 1977.

[161] Pratt V. A decidable /¿-calculus // Proceedings of 22nd FOCS'81. IEEE, 1981. P. 421-427.

[162] Presburger M. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt //Sprawozdanie z I Kongresu matematyköw krajöw slowianskich. Warsaw, 1930. P. 92-101,395.

[163] Schroeppel R. A Two Counter Machine Cannot Calculate 2N. Memo 257. Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972. 32 p.

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

[165] Shilov N. V., Yi K. Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers // Electr. Notes Theor. Comput. Sci. 43, 2001.

[166] Shilov N. V., Yi K. On Expressive and Model Checking Power of Proposi-tional Program Logics // Ershov Memorial Conference, 2001. P. 39-46.

[167] van Schouwen A. J. The A-7 Requirements model: Re-examination of realtime systems and an application to monitoring systems // Tech. report 90-276. Queen's Ck IS, TRIO. Kingston, Ontario, Canada, 1990. 93 p.

[168] SMV. Symbolic Model Verificator. Carnegie Mellon University, http://www.cs.cmu.edu/ modelcheck/smv.html

[169] SPIN, http://spinroot.com/spin/whatispin.html

[170] Steffen B. Characteristic formulae // Lecture Notes in Computer Science. Springer, 1989. V. 372. P. 723-732.

[171] Stirling C. P. Modal and temporal logics for processes // Lecture Notes in Computer Science. Springer, 1996. V. 1043. P. 149-237.

[172] Stirling C. P. Modal and temporal logics // Handbook of Logic in Computer Science. Oxford University Press, 1992. V. 2. P. 477-563.

[173] Stirling C.P., Walker D. Local model checking in the modal //-calculus // Theoretical Computer Science. 1991. V. 89. P. 161-177.

[174] UPPAAL. http://www.uppaal.com

[175] Wakatsuki M., Teraguchi K., Tomita E. Polynomial time identification of strict deterministic restricted one-counter automata in some class from positive data // Lecture Notes in Artificial Intelligence. Springer, 2004. V. 3264. P. 260-272.

[176] Wassyng A., Lawford M. Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project // Lecture Notes in Computer Science. Springer, 2003. V. 2805. P. 133-153.

[177] Zakharov V. A. On the verification of PLTL formulae by means of monotone disjunctive normal forms // Lecture Notes in Computer Science. Springer, 1997. V. 1234. P. 419-429.