Содержание к диссертации
Введение
1 Предварительные сведения 15
1.1 Мультимножества 15
1.2 Квазиупорядоченные множества 16
1.2.1 Свойство вполне упорядочиваемое 17
1.3 Системы помеченных переходов 22
1.3.1 Определение 22
1.3.2 Вполне структурированные системы переходов . 23
1.3.3 Покрывающее дерево системы переходов . 24
1.3.4 Метод насыщения 28
1.3.5 Системы переходов с совместимостью по убыванию 32
1.4 Счётчиковые машины 34
1.5 Темпоральные логики и проверка модели 44
1.5.1 Логики ветвящегося времени 48
1.5.2 Логики линейного времени 58
1.5.3 Сравнение логик 61
2 Темпоральные свойства вполне структурированных систем переходов 74
2.1 Системы переходов автоматного типа 74
2.1.1 Разрешимые темпоральные свойства 78
2.1.2 Неразрешимые темпоральные свойства 87
2.2 Вполне структурированные системы переходов 95
2.2.1 Разрешимые темпоральные свойства 95
2.2.2 Неразрешимые темпоральные свойства 97
2.3 Дерево логик 98
3 Взаимодействующие раскрашивающие процессы 100
3.1 Взаимодействующие процессы независимые от данных 103
3.2 Взаимодействующие раскрашивающие процессы 108
3.3 ССР - вполне структурированная система переходов 111
3.4 Пример 115
4 Недетерминированные счетчиковые машины 118
4.1 Введение 118
4.2 Недетерминированные счетчиковые машины 119
4.3 Проблема ограниченности 123
4.4 Проблемы включения и эквивалентности 127
4.4.1 Слабое вычисление 128
4.4.2 Проблема включения 130
4.4.3 Проблема эквивалентности 133
4.5 Проблема достижимости 134
Заключение 137
Литература 139
- Системы помеченных переходов
- Темпоральные логики и проверка модели
- Вполне структурированные системы переходов
- ССР - вполне структурированная система переходов
Введение к работе
В настоящее время большое внимание уделяется моделированию и анализу корректности параллельных и распределённых систем, каковыми являются, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов. Под корректностью понимается полное соответствие системы задачам, для которых она создаётся. Корректность определяется абстрактным образом в соответствии с формальной спецификацией, описывающей желаемое поведение системы. Процесс проверки соответствия поведения системы требованиям, заданным в спецификации, называется верификацией [23, б].
За время исследований по проблеме верификации был разработан ряд методов проверки корректности параллельных и распределенных систем и накоплено большое количество теоретических результатов и практического опыта в этой области. Среди отечественных исследований по спецификации, моделированию и анализу распределенных систем отметим работы Н.А. Анисимова, О.Л. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А. Непомнящего, Р.Л. Смелянского, В.А. Соколова, Л.А. Черкасовой, Н.В. Шилова.
Проверка модели (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. Mayr, из которых, например, можно выделить [38, 35, 49, 50], исследовались вопросы разрешимости задачи проверки модели для некоторых конкретных представителей класса вполне структурированных систем переходов, а именно, магазинных автоматов, сетей Петри, ВРР, LVAS (Lossy Vector Addition Systems), и различных темпоральных логик линейного времени и ветвящегося времени.
В данной же работе акцентируется внимание на разрешимости тех темпоральных свойств, которые являются общими для всего класса вполне структурированных систем переходов, а также для специального подкласса таких систем, вполне структурированных систем переходов автоматного типа, обладающих свойствами верхней и нижней совместимости отношения квазипорядка с отношением переходов. Из-за своей специфической структуры, вполне структурированные системы переходов автоматного типа можно также отнести и к классу систем переходов независимых от данных.
В литературе практически не уделяется внимание системам переходов независимых от данных (за исключением систем переходов с конечным числом состояний). Тем не менее, системы, принадлежащие к этому классу, могут быть достаточно выразительными и нетривиальными.
Для демонстрации этого факта в данной работе представлен новый формализм, названный взаимодействующие раскрашивающие процессы (Communicating Colouring Processes - ССР), позволяющий строить модели распределённых системы, где поведение каждого компонента опи- сывается последовательным процессом и между ними организовано взаимодействие, направленное на обмен и передачу пакетов информации. Формализм ССР принимает во внимание факт передачи данных, а также позволяет отслеживать перемещение данных различного типа между компонентами системы. Но переход из одного состояния в другое не зависит от оперируемых данных, а определяется только управляющими состояниями.
Более того, вводится класс недетерминированных счётчиковых машин в качестве общего средства для демонстрации неразрешимости ряда классических проблем для систем переходов независимых от данных, которые могут моделировать эти машины, в частности, для взаимодействующих раскрашивающих процессов.
Указанные формализмы представляют собой конкретные реализации специального подмножества (фрагмента) алгебры процессов, построенной на основе таких хорошо известных алгебр процессов, как 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.3.1 Система помеченных переходов представляет собой четвёрку LTS — (S, Т, —, SQ), где S множество состояний с элементами $Q, $I, s%,..., Т - некоторый алфавит пометок (множество имён действий), —С [S х Т х S) - отношение перехода между состояниями, so Є S - начальное состояние системы. Переход (s,t,s() обычно обозначается как $ — $ , что означает, что действие с именем t переводит состояние s в состояние s . Состояния s в этом случае называется t последующим., или просто последующим для s, а состояние s - t-предыдущим, или просто предыдущим для s . Состояния, не имеющие последующих состояний, называются финальными. Через Succ(s) обозначается множество последующих состояний для s, через Pred(s) - множество его предыдущих состояний. Система LTS будет конечно ветвящейся, если для любого s множество Succ(s) конечно. В данной работе рассматриваются системы с конечным ветвлением. Последовательное исполнение для LTS есть конечная или бесконеч 4- + ная цепочка переходов so -A si - S2 —» ..., где so - начальное состояние системы. Запись s A s означает, что имеется (конечная) последовательность переходов, переводящая состояние 5 в состояние s . Диаграмма переходов (дерево достижимости) для LTS есть помеченный, ориентированный граф GLTS-, В котором вершинами являются элементы множества состояний S, а дуги определяются отношением переходов так, что дуга, помеченная t, соединяет вершину s с вершиной s в том и только том случае, когда s . Очевидно, что каждому последовательному исполнению для LTS соответствует ориентированный путь с началом в вершине so в графе GLTS Для решения задач анализа семантических свойств систем переходов полезной оказывается теория вполне структурированных систем переходов [51, 52]. Определение 1.3.2 Вполне структурированной системой переходов (со свойством совместимости по возрастанию) называется система переходов LTS (S,Т,— ,so), дополненная отношением квазипорядка С S х S, удовлетворяющим следующим условиям: 1. отношение является вполне упорядочиваемым квазипорядком; 2. квазипорядок совместим (по возрастанию) с отношением пере t ходов — , а именно, для любых состояний s q и перехода s —» $ существует переход q -+ q , такой что s q ; Свойство совместимости может быть представлено в виде следующей диаграммы: Для анализа некоторых свойств вполне структурированных систем переходов используется конструкция покрывающего дерева [51]. Определение 1.3.3 Покрывающим деревом вполне структурированной системы переходов (LTS, ) для состояния so Є S называется конечный ориентированный граф (дерево), такой что 1. Вершины дерева помечены состояниями системы LTS; 2. Каждая вершина объявлена либо живой, либо мёртвой; 3. Корню дерева приписана пометка $Q, и эта вершина объявлена эюи-вой; 4- Мёртвые вершины не имеют потомков; 5. Живая вершина с пометкой $ имеет по одному потомку, помечен-ному sf, для каждого состояния s1 Є Succ(s); 6.
Если на пути от состояние 5 в состояние s . Диаграмма переходов (дерево достижимости) для LTS есть помеченный, ориентированный граф GLTS-, В котором вершинами являются элементы множества состояний S, а дуги определяются отношением переходов так, что дуга, помеченная t, соединяет вершину s с вершиной s в том и только том случае, когда s . Очевидно, что каждому последовательному исполнению для LTS соответствует ориентированный путь с началом в вершине so в графе GLTS Для решения задач анализа семантических свойств систем переходов полезной оказывается теория вполне структурированных систем переходов [51, 52]. Определение 1.3.2 Вполне структурированной системой переходов (со свойством совместимости по возрастанию) называется система переходов LTS (S,Т,— ,so), дополненная отношением квазипорядка С S х S, удовлетворяющим следующим условиям: 1. отношение является вполне упорядочиваемым квазипорядком; 2. квазипорядок совместим (по возрастанию) с отношением пере t ходов — , а именно, для любых состояний s q и перехода s —» $ существует переход q -+ q , такой что s q ; Свойство совместимости может быть представлено в виде следующей диаграммы: Для анализа некоторых свойств вполне структурированных систем переходов используется конструкция покрывающего дерева [51]. Определение 1.3.3 Покрывающим деревом вполне структурированной системы переходов (LTS, ) для состояния so Є S называется конечный ориентированный граф (дерево), такой что 1. Вершины дерева помечены состояниями системы LTS; 2. Каждая вершина объявлена либо живой, либо корня дерева до некоторой вершины с пометкой sf встречается вершина с пометкой $ такой, что $ s1, то говорят, что sf покрывает s, и вершина sf объявляется мёртвой; в противном случае sf - живая вершина. Листья в покрывающем дереве помечены финальными или покрывающими состояниями. Для вполне структурированных систем переходов частичный порядок является вполне упорядочиваемым. Благодаря этому все пути в покрывающем дереве конечны, так как всякий бесконечный путь должен был бы содержать покрывающую вершину. В силу леммы
Темпоральные логики и проверка модели
Темпоральные логики играют важную роль в формальной верификации. Они используются для выражения свойств процессов. Такими свойствами, например, являются "процесс никогда не достигнет тупикового состояния" или "в любом бесконечном исполнении процесса действие Ь происходит бесконечно часто". Задачо, проверки модели - это задача, состоящая в том, чтобы определить выполнимость для процесса, который задаётся помеченной системой переходов, свойства, выраженного формулой темпоральной логики. Задача проверки модели Дано: помеченная система переходов, состояние s этой системы и формула if темпоральной логики. Вопрос: удовлетворяет ли состояние s формуле (р? Существует два основных класса темпоральных логик, которые различаются их интерпретацией. Логики ветвящегося времени определяются над деревом достижимости (диаграммой переходов). Логики линейного времени интерпретируются через множество всех исполнений системы переходов. Существует большое количество темпоральных логик, которые отличаются друг от друга по выразительной силе [47, 77, 92]. В данной работе рассматриваются наиболее известные и широко используемые темпоральные логики и их некоторые интересные подмножества. Прежде чем темпоральные логики будут описаны подробно, обозначим мотивацию их определения, Логика Хеннеси-Милнера и слабая логика линейного времени являются очень слабыми по выразительной силе логиками и едва ли могут выражать какие-либо интересные свойства. Поэтому они почти не используются в формальной верификации. Исторически темпоральная логика линейного времени (linearime temporal logic - LTL) [83] и темпоральная логика ветвящегося времени (branchingime temporal logic или computationree logic - CTL) [40] определялись как расширения этих логик путём добавления новых темпоральных операторов, которые значительно увеличили выразительную мощность. Таким образом стало возможным описание ряда интересных свойств. В насто ящее время LTL и CTL широко известные и часто используемые в формальной верификации логики. Одной из самых мощных логик является модальное //-исчисление [67, 92].
Эта логика более выразительная чем LTL и CTL. Модальное //-исчисление основывается на применении операторов наибольшей и наименьшей неподвижных точек, что и придаёт ей такую выразительность. В действительности, эта логика является слишком мощной и не используется в полном объёме на практике. Более того, она весьма трудна в понимании. В наиболее общем смысле формулы темпоральных логик интерпретируются через исполнения процессов, заданных произвольными (возможно бесконечными) помеченными системами переходов. Они могут быть определены в семантике с акцентом на состояния или действия систем переходов (или же в комбинации). В формулы, построенные в семантике с акцентом на состояния, включаются так называемые элементарные высказывания, которые соответствуют множествам состояний системы переходов, удовлетворяющих этим элементарным высказываниям. Информация о том, какие метки действий на дугах переходов, игнорируется. Поэтому, в действительности, речь идёт об интерпретации темпоральных формул через исполнения непомеченной системы переходов. В семантике действий не принимается в расчёт какая-либо информация о состояниях системы, и отдаётся предпочтение только меткам переходов, т.е. действиям, которые осуществляются при переходе из одного состояния в другое. В этом случае логики обычно содержат операторы следования, которые позволяют задавать свойства вида "действие Ь в данном состоянии возможно". В данной работе одновременно используются оба подхода, представляет интерес и семантика состояний, и семантика действий, поскольку, с одной стороны, объектом исследований являются помеченные системы переходов, а с другой стороны, использование элементарных высказываний над множеством состояний позволяет учитывать особенности тех или иных состояний системы, например, количество ресурсов (в случае сетей Петри и т.п.). Введём несколько обозначений, являющихся общими для всех описываемых логик.
Рассмотрим вполне структурированную систему переходов S = (5,Г,-», s0). Обозначим Р множество элементарных высказываний над множеством S состояний системы переходов S. Пусть L : S — 2Р - отображение, сопоставляющее каждому состоянию множество элементарных высказываний, истинных в этом состоянии. Условимся обозначать Рис множество элементарных высказываний, интерпретирующихся верхними конусами состояний системы переходов S, т.е. для любого р Є Рис выполняется условие, что s \= р = Vs s : s = р, где s, s Є S, a PDC - множество элементарных высказываний, интерпретирующихся нижними конусами, т.е. для любого р Є Рос выполняется условие, что s \= р =$
Вполне структурированные системы переходов
Теорема 2.2.1 Задача глобальной проверки модели разрешима для класса вполне структурированных систем переходов и формул модального {і-исчисления, находящихся в позитивной нормальной форме без модального оператора [t], при интерпретации элементарных высказываний как верхних конусов. Доказательство почти полностью повторяет доказательство теоремы 2.1.2 с поправкой на общий случай вполне структурированных систем переходов. Следствие 2.2.1 Задача глобальной проверки модели является разрешимой для класса вполне структурированных систем переходов и ло-3UKu3CTLAf{Puc). Теорема 2.2.2 Задача локальной проверки модели разрешима для класса вполне структурированных систем переходов и логики ЗАЬшс{РисДоказательство. Проводится аналогично доказательству теоремы 2.1.4 структурной индукцией по вложению подформул в формуле (р логики ЗАЬшс(Рис). Базис индукции. Рассмотрим разрешимость данной задачи для произвольного состояния so вполне структурированной системы переходов S и формулы вида ЗЛ сіРі, чРп), где р{ Є Рис Как и ранее (см. док. теоремы 2.1.3) построим вполне структурированную систему переходов S1 — (S",T", — ,Sg), представляющую собой произведение системы S — (S, Т, —», so) и замкнутого ш-автомата Ave — (E,QiQ0i5iF=Q) гДе — Рис x - Затем, для системы S1 построим дерево покрытия с корнем в начальном состоянии s0 = (so,9o) Состояние SQ системы переходов $ будет удовлетворять формуле (р = ЗД сІРі) )Рп) тогда и только тогда, когда в дереве покрытия будет существовать лист, представляющий собой покрывающее состояние для некоторого предыдущего состояния на этой же ветке. Действительно, поскольку элементарные высказывания интерпретируются верхними конусами, наличие такого покрывающего состояния (листа) обеспечивает существование бесконечного пути, состоящего из финальных состояний. Все состояния этого пути будут покрывающими и, следовательно, будут удовлетворять тому же элементарному высказыванию, что и покрываемое состояние. Если же все листья дерева покрытия не являются покрывающими, т.е. все листья тупиковые состояния, которые не имеют потомков, это означает, что не существует бесконечных исполнений системы S, удовлетворяющих формуле (р. Поскольку все элементарные высказывания интерпретируются верхними конусами, если для состояния SQ формула р вида ЭАшС(Ръ... ,рп) выполнена, т.е. SQ \= tp, то эта формула будет также верна и для любого состояния s SQ. Предположение индукции.
Рассмотрим автомат A d iрп) с ал фавитом = { i,..., ipn} х Г, где (pi - произвольные формулы логики ЭАЬшс(Рис)- Предполагая, что для произвольного состояния $ системы $ и формулы (fi существует алгоритм проверки s \= fi, и проводя постро ения и рассуждения аналогичные указанным выше получим алгоритм проверки формул в общем случае. Следствие 2.2.2 Задача локальной проверки модели является разрешимой для класса вполне структурированных систем переходов и логик ЗСТЬАш(Рис) и -nLTLA Pvc) Теорема 2.2.3 Задача глобальной проверки модели является разрешимой для, класса вполне структурированных систем переходов и формул логики ALf(Pjjc) вида 3Af(pi-,... ,рп) Доказательство. Полностью повторяет первую часть доказательства теоремы 2.1.5. Следствие 2.2.3 Задача глобальной проверки модели является разрешимой для класса вполне структурированных систем переходов и логики - LTLAf(Puc) Теорема 2.2.4 Задача проверки модели является неразрешимой для класса вполне структурированных систем переходов и темпоральных логик 3CTLAf(Рос), ЗСТЬАш(Рос), - LTLAf{PDC) u LTLA {PDC). Доказательство. Рассмотрим 2-х счётчиковую машину с обнулениями 2гсМ как вполне структурированную систему переходов. Для каждого счётчика Xj все переходы (из состояний первого типа) с выражением Xj := Xj 4- 1 пометим как incj, переходы (из состояний второго типа) с выражением Xj : Xj — 1 как decj, а переходы с выражением Xj := О обозначим nulj (j — 1, 2). Если переходы incj, decj, пиЦ переводят машину в финальное состояние, то обозначим (переименуем) их соответственно haltj j halt J НаЩ. Для доказательства этого утверждения достаточно построить формулы соответствующих темпоральных логик, такие что выполнимость каждой такой формулы означала бы существование у системы 2гсМ ис
ССР - вполне структурированная система переходов
В зависимости от используемых операторов взаимодействующие раскрашивающие процессы можно рассматривать как системы переходов с конечным или бесконечным числом состояний. Во втором случае ССР ляется вполне структурированной системой переходов, что влечёт разрешимость ряда классических проблем для этого формализма. Вполне структурированные системы переходов - это весьма широкий класс систем переходов с бесконечным числом состояний, для которых разрешимость многих свойств следует из существования совместимого с отношением переходов вполне упорядочиваемого квазипорядка на множестве состояний. Рассмотрим ССР как систему помеченных переходов S — (5, Т, — , SQ). Определим естественным образом частичный порядок на множестве состояний S системы S. Определение 3.3.1 Пусть (q,M), (q ,M ) - это состояния ССР. Положим (q, М) (q } М ) тогда и только тогда, когда q = q и М М , где М М УхеУаг: М(х) С М (х). Утверждение 3.3.1 Отношение порядка на множестве состояний S является вполне упорядочиваемым квазипорядком. Доказательство. По лемме Диксона [44]. D Утверждение 3.3.2 Пусть S — (5, Т, —»,$о) - это взаимодействующие раскрашивающие процессы, - вполне упорядочиваемый квазипорядок на множестве состояний S. Тогда ( ?, ) есть вполне структурированная система переходов с совместимостью по возрастанию и убыванию. Доказательство. Пусть (q,M), (q ,Mf) - состояния ССР. По определению 3.3.1 (q,M) - (q ,Mf) тогда и только тогда, когда q = q and М X М!. Отсюда, для всех состояний (q, М) г (д , М ): (q, М) Л (q2, М2) (q ,Mf) (q2,M . Легко проверить, что для всех операторов, которые используются в выражениях е(#1,2:2) Є Exp , выполняются следующие условия: У(тит2) {т ът 2) : ор(тит2) ор(т[,т 2), ор Є {U,+}; Vmi mi и Ш2 : ор(т\,т2) : op(mi,m2), op Є {П, 0}; Vmi mi и С С Е : op(mi, С) op(wi i, С), op Є {\, /}, ті;т\ - мультимножества. Следовательно, для всех состояний (q, М) ( /, М1) и перехода q — q2 имеем (q2, М2) (q2, М2), где М2 и Мз вычисляются в соответствии с вы ражением e(#i,a:2), которое используется в действии , из М и М! соот ветственно, т.е. выполняется условие монотонности выражений e(a;i,:c2) Утверждение 3.3.3 Пусть система переходов (S, : ) представляет собой ССР с вполне упорядочиваемым квазипорядком на мноэюестве состояний. Тогда для каждого состояния s и действия t множество miniPredt s)) вычислимо. Доказательство. Построим множество Ч минимальных состояний, при которых переход с пометкой t может сработать. Для любого локального состояния q, из которого существует переход t, состояние (q, 0,..., 0) принадлежит множеству % т.е. t — {(q: 0,..., 0) { 3q : q — q }. Обозначим через t множество состояний, получаемых в результате срабатывания перехода t на состояниях из множества Ч.
Рассмотрим множество "fsOtt0, состоящее из таких состояний s , что s может быть получена в результате срабатывания перехода t и s s . Это множество является направленным вверх конусом и в силу вполне упо-рядочиваемости отношения имеет конечный базис, который обозначим lub(s,t). Конечный базис lub(s, t) состоит из одного состояния и может быть эффективно построен следующим образом. Рассмотрим некоторое состояния ( /,mi,... , гоп) Є , s — {q(,т ъ ... ,m n). Для того, чтобы пересечение конусов js П не было пустым, необходимо выполнение условия q — q . Тогда ЫЬ(з, ) = (q, т[ U mi,..., т п U mn). Пусть теперь некоторое состояние s Є Predi(fs). Тогда возможно срабатывание перехода t, которое переводит s в состояние в" Є ]s. Отсюда следует, что s" t. С другой стороны, для любого состояния s" такого, что sff Є s и s" Є Т можно построить Predt($"), т.к. каждое действие изменяет значение только одной переменной с помощью простого выражения є Є зф. Получаем Predt{\s) — Predt( lub(s,t0)) = ]Predt{lub(s,t)). Эта формула задаёт эффективное построение конечного базиса мно жества Predt{]$) по конечному базису lub(s,t).О Мы получили разрешимость следующих проблем для ССР [27, 52]: проблема покрытия, которая состоит в том, чтобы для двух состояний (q, М) и ( /, М ) определить, возможно ли, начиная исполнение из ( ?, М), покрыть состояние (ql, М ), т.е. может ли быть достигнуто состояние (q", М") У (qf, М )\ проблема субпокрытия, состоящая в том, чтобы для двух состояний (q, М) и {of, М ) определить, возможно ли, начиная исполнение из (g, М), попасть в состояние, которое покрывается состоянием (У, М ), т.е. может ли быть достигнуто состояние (#", М") (qf, М )\ проблема достижимости, т.е. определить достижимо ли из состояния s данное множество Q управляющих (локальных) состояний; проблема неизбежности, т.е. по данному множеству Q локальных состояний и начальному состоянию SQ определить верно ли, что всякое исполнение приводит к некоторому локальному состоянию из Q (частным случаем является проблема останова: определить верно ли, что всякое исполнение завершается, т.е. приводит к некоторому финальному состоянию). Следовательно, например, имеем разрешимость проблемы передачи данных определённого цвета во внешнюю среду через некоторый канал. Большое количество формализмов, таких как сети Петри [82], Lossy Channel Systems [30], Basic Parallel Process, Realime Automata [33] и мн. др., могут быть рассмотрены как вполне структурированные системы переходов или вполне структурированные системы переходов с совместимостью по убыванию. Формализм ССР - это вполне структурированная система переходов, обладающая свойствами совместимости и по возрастанию, и по убыванию. Это влечёт разрешимость некоторых новых проблем для ССР. Например, задачи проверки модели для различных специальных подмножеств темпоральных логик при интерпретации элементарных высказываний верхними и нижними конусами состояний (см. предыдущую главу). Пример (рис. 3.3) демонстрирует, помимо возможности моделирования взаимодействия между сотрудниками, секретарём и начальником, возможность отслеживания перемещения данных различных типов. Действия начальника: Wi - сформировать пакет заданий для сотрудников (а,Ь,с - типы зада,-ний);
