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

На правахрукописи

Кузьмин Егор Владимирович

ИССЛЕДОВАНИЕ СВОЙСТВ КЛАССА ВПОЛНЕ СТРУКТУРИРОВАННЫХ СИСТЕМ ПЕРЕХОДОВ

Специальность 01.01.09 - Дискретная математика и математическая кибернетика

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата физико-математических наук

Ярославль - 2004

Работа выполнена в Ярославском государственном университете им. П.Г. Демидова.

Научный

руководитель кандидат физико-математических наук, профессор

Соколов Валерий Анатольевич

Официальные

оппоненты: доктор технических наук, г.н.с.

Бандман Ольга Леонидовна

доктор физико-математических наук, профессор Бондаренко Владимир Александрович

Ведущая

организация Институт систем информатики

им. АЛ. Ершова СО РАН

Защита состоится « У »д/Сят&Зр^Ь 2004 г. в /¿час. на заседании диссертационного совета К 212.002.06 при Ярославском государственном университете им. П.Г. Демидова по адресу: 150008, г. Ярославль, ул. Союзная, 144.

С диссертацией можно ознакомиться в научной библиотеке Ярославского государственного университета им. П.Г. Демидова.

Автореферат разослан

2004 г.

Учёный секретарь диссертационного совета

Яблокова СИ.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

. ограниченности, включения и эквивалентности.

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

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

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

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

1. Методымоделирования, анализа и верификациираспределенных

систем. РФФИ, грант № 99-01-00-309.

2. Разработка новых методов и средств моделирования и анализа

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

РФФИ, грант № 03-01-00-804.

3. Федеральная целевая программа "Интеграция".

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

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

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

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

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

В разделе 1.1 определяются операции на мультимножествах.

В разделе 1.2 определяются: вполне упорядочиваемый квазипорядок, верхние и нижние конусы и описываются их свойства.

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

Система помеченных переходов есть четвёрка ЬТ5— Г,—>, я о) где S есть множество состояний с элементами Яс, ..., Т- неко-

торый алфавит пометок (множество имён действий), —► с (5хГх5) -отношение перехода между состояниями, е Б - начальное состояние системы.

Последовательное исполнение для 1.есть конечная или бесконечная цепочка переходов - начальное состояние системы.

Вполне структурированной системой переходов с совместимостью по возрастанию (соот. по убыванию) WTS называется система переходов , дополненная отношением квазипоряд-

ка удовлетворяющим следующим условиям: 1) отношение

<. является вполне упорядочиваемым квазипорядком; 2) квазипорядок <, совместим (по возрастанию) с отношением переходов —>, а именно, для любых состояний 5/ <, д/ и перехода 5/—существу-ет переход такой что,

(COOT, квазипорядок < совместим по убыванию с отношением переходов ->, а именно, для любых состояний. Si^qi и перехода существует переход такой что

В разделе 1.4 рассматриваются счётчиковые машины с потерями (lossy counter machines), т.е. машины со счётчиками, значения та-торых могут уменьшаться самопроизвольно в любое время; Эти машины слабее по выразительной мощности чем машины Тьюринга и-могут быть заданы (моделироваться) многими системами. Счётчико-вые машины с потерями были введены R: Mayer в качестве общего средства для демонстрации алгоритмической неразрешимости ряда проблем для систем с потерями, которые используются для моделирования передачи данных через ненадёжные каналы связи, например, проблемы верификации систем с ненадёжными очередями (lossy FIFO-channel systems), задачи проверки модели для сетей Петри c потерями, некоторых проблем для сетей Петри с обнуляющими дугами и параметрических проблем таких, как справедливость для протоколов передачи данных.

В разделе 1.5 рассматривается задача проверки модели.(model checking), описываются темпоральные логики ветвящегося времени, (логика Хеннеси-Милнера, CTL, модальное ц-исчисление) и линейного времени (слабая логика линейного времени, LTL), позволяющие выражать свойства исполнений систем переходов. Вводятся расширения широко известных логик CTL (computation tree logic) и LTL (linear-time logic), которые обозначаются CTLA и LTLA соответственно, позволяющие строигь темпоральные. формулы с учётом пометок действий систем переходов. Описывается автоматная логика AL, представляющая собой обобщение и расширение логик CTLA и LTLA.

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

Производится сравнение логик по выразительной силе.

Логики 3AL(P) и VAL(P) - это подмножества логики AL, содержащие формулы, построенные из элементарных высказываний р е Р, операторов конъюнкции, дизъюнкции и соответственно кванторов существования и всеобщности. Если L - подмножество логики AL, тогда Lf (coot. L01, L^) обозначается подмножество логики L, где используются только конечные автоматы (соот. автоматы Бюхи, замкнутые ©-автоматы). Условимся обозначать Рис множество элементарных высказываний, интерпретирующихся верхними конусами состояний системы переходов (5", Т, s0), т.е. V р е Рис выполняется условие s о Vj'^5: s'\-p, где s, s' 6 S, а Рос - множество элементарных высказываний, интерпретирующихся нижними конусами, т.е. V р q Ррс выполняется условие s \=р о \/s'<, s: р.

Локальная проверка модели: для заданной модели (системы переходов) LTS определить истинность формулы темпоральной логики (р в состоянии 5, т.е. проверить, выполняете,; ли s j- <р.

Глобальная проверка модели: построить множество всех состояний модели LTS, в которых формула <р темпоральной логики является истинной.

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

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

. . В разделе 2.1 выделяется новый подкласс вполне структурированных систем переходов и рассматриваются его свойства.

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

-> с (ЗУГх,!?) такое, что 3 с (@хТх()): для любых состояний (д, с/), (</' Л1) и некоторой метки перехода / переход сО—'—>(д\с1*) существует тогда и только тогда, когда существует переход д—— отношение ^определяется так, что (¡) о д = д'и. с1 <,<!'.

Теорема 2.1.1. Класс вполне структурированных систем переходов с совместимостью по возрастанию и убыванию совпадает с классом вполне структурированных систем переходов автоматного типа.

Пусть 1¥А — класс вполне струюурированных систем переходов: автоматного типа с разрешимым предбазисом.

В пункте 2.1.1 представлены подмножества темпоральных логик, позволяющие выражать свойства систем переходов, которые являются разрешимыми для класса №А.

Теорема 2.1.2. Задача глобальной проверки модели является разрешимой для класса 1УА и формул модального ц-исчисления, находящихся в позитивной нормальной форме, при интерпретации элементарных высказываний как верхних конусов (т.е. любое элементарное высказывание р е Рис)-

Следствие 2.1.1. Задача глобальной проверки модели разрешима для класса \УА и логики СТЬА/Рис)-

Теорема 2.1.3. Задача локальной проверки модели разрешима для класса и логики АЬ/Рос)-

Следствие 2.1.2. Задача локальной проверки модели разрешима для класса Ш и логик СТЫ/Ррс), ЬТЫ/Ррс) и -¿Т1Л/Рос).

Теорема 2.1.4. Задача локальной проверки модели разрешима для класса ЖА и логики А1шс(Р1/С)-

Следствие 2.1.3. Задача локальной проверки модели разрешима для класса \УА и логик СТЬА^Рцс), ЬТ1Л^Рцс) и -¿ТЬА^ис)-

Теорема 2.1.5. Задача глобальной проверки модели разрешима для класса 1К4 и формул логики АЬ/Рцс) вида ЗА/р/,...,рп) и УА/р!,...,р„).

Следствие 2.1.4. Задача глобальной проверки модели разрешима для класса 1УА и логик ЬТЬА/Рцс) и -¿ТЬА/Рцс).

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

Основная идея доказательств следующих теорем состоит в построении с помощью оператора недетерминированного перехода и

и

отношения потери значения счетчиков из машины Минского её "слабой" модели, принадлежащей к классу систем переходов ЖЛ. Затем для этой "слабой" машины описывается свойство в виде формулы темпоральной логики, разрешимость которого для "слабой" машины'приводила бы к разрешимости неразрешимых проблем для счётчиковой машины с потерями или машины Минского, например, проблемы останова;

Теорема 2.1.6. Задача проверки модели неразрешима для класса И7А и автоматных логик ЗАЬ/Рис ,Ре>с) и ЗАЬ^Рцо.Рос)-

Теорема -2:1.7. Задача проверки модели неразрешима для класса ]¥А и темпоральных логик 3СТ1А/Рис„Рос), 3СТЬАа/Рис,.Рос), —¿.ТМ/Рис ,Рос) и -лЬТЫ^РисРод-

Теорема 2.1.8. Задача проверки модели неразрешима для класса ]¥А и автоматной логики ЗАЬа/Рцс).

Теорема 2.1.9. Задача проверки модели неразрешима для класса УУА и темпоральных логик ЪСТЬА(Рцс) и —1ТЫ(Рис)-

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

Пусть ЖУ- класс вполне структурированных систем переходов. В пункте 2.2.1 представлены подмножества темпоральных логик, позволяющие выражать свойства систем переходов, которые являются разрешимыми для класса ЖУ.

Теорема 2.2.1. Задача глобальной проверки модели разрешима для класса ЖУ и формул модального ц-исчисления, находящихся в позитивной нормальной форме без модального оператора [I], при интерпретации элементарных высказываний как верхних конусоз.

Следствие 2.1.1. Задача глобальной проверки модели разрешима для классаЖЯ и логики ЗСТЬА/Рцс)-

Теорема 22.2: Задача локальной проверки модели разрешима для класса Ж5 и логики 3АЬ^Рос)-

Следствие 2.2.2. Задача локальной проверки модели разрешима для класса ЖУ и логики ЗСТЬА^Рцс) и —1ТЬА а/Рис)-

Теорема 2.2.3. Задача глобальной проверки модели разрешима для класса Ж? и формул логики А1/Рцс) вида ЗА/р],...,рп).

Следствие 2.2.З.' Задача глобальной проверки модели разрешима для класса ЖУ и логики —¿Т1А/Рис)-

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

Теорема 2.2.4. Задача проверки модели неразрешима для класса 1Г8 и темпоральных логик 3СТЫ/Ррс), ЗСТЫ^Рос), -ХТЫ/Рос) и

-пШЛЛРос).

В пункте 2.2.2 подводится итог главы. На рисунках 2.4, 2.5; 2.6, 2.7 наглядно представлены границы разрешимости для темпоральных логик ЬТЬА и СТЬА и рассматриваемых классов систем переходов )УА и Ш.

СТЫ^поРвс)

СТЬА/Рцс) СТЫ/Рос)

дъА/Ря^

ЗСТЫ/Р^Рос) 3СТЩРис) ЗСТШРиаРос)

Рис. 2.4. Граница разрешимости логики СТЬА длх класса 1УА.

ЛЦРюРп

пЬТЬА/РсъР

---7- , +

1ТЩРис) ПЬА/Рос) ЬТЫ^Рцс) -.ЬТЬА/Род -,ША/Рис) -.ЬТЬА^Р,^ Рис. 2.5. Граница разрешимости логики ЬТЬА для класса №А.

ЗСПАГРааРк}

ЗСШ/Р1Х) ЗСТи^Рис) ЗСТЬА/Р¡х) ЗСТЬА^Рос)

Рис. 2.6. Граница разрешимости логики CTLA для класса ЖЪ.

Рис. 2.7. Граница разрешимости логики LTLA для класса

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

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

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

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

С другой стороны, существует много формализмов, таких как машины Тьюринга и счётчиковые машины, сети Петри, системы с ненадёжными каналами (Lossy Channel Systems), которые имеют семантическое расширение и производят манипуляции с данными. Модель в рамках этих формализмов состоит из системы переходов с конечным числом управляющих состояний (управляющая. часть), работающая с потенциально бесконечным множеством D значений данных. Состояние такой системы может быть представлено в виде пары (q, d), где q - управляющее состояние, а Переход

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

Формализм ССР принимает во внимание факт передачи данных, а также позволяет отслеживать перемещение данных различного типа между компонентами системы. Но переход из одного состояния в другое не зависит от оперируемых данных, а определяется только управляющими состояниями. Таким образом, формализм ССР занимает промежуточное положение среди указанных формализмов.

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

Предполагаем наличие следующих множеств: Pr - {X, У, Х\,.} - конечное множество имён процессов; Var = {х, у, Х/,...} - конечное множество переменных; - конечное множество

каналов; Exp = fe, е/, ej,...} - конечное множество выражений над множеством переменных Var\ Actvar ~ {х! е,..., х?у,...} -множество простых действий процессов; Actai = {(v! е, v ? х), (vt! е, vt ? x),...J - множество взаимодействий между процессами (передача данных через каналы v. v/,...); D = {d, di, d2,...} - бесконечное множество допустимых значений переменных.

Опишем абстрактный синтаксис выражений (для) процессов.

Выражения процессов Е, £',.•• задаются следующей грамматикой: Е,Е' ::= 0 | Х е Pr | v?x.E | v.'e.E | Е + Е' | Е || Е'

Дадим интуитивное представление смысла приведённых выше конструкций. Процесс 0 представляет собой процесс, который не является активным, т.е. никакое действие не может быть выполнено. Процессы v?x.E и v.'e.E совершают действия v?x й v!e соответственно, а затем продолжаются как процесс Е. Действие v?x означает копирование (присвоение) в переменную х значения из v, где в данном случае г' может быть как обычной переменной, так и синхронизирующим каналом передачи данных; т.е. , v е For и Chi. Действие v'e представляет собой копированием v е VarxjChl значения выражения е. Вместо е будем также писать е(х/,...,х„). Для двух процессов Е'лЕ'оператор суммы даёт процесс Е + Е', который ведёт себя либо как Е, либо как Е'. Для двух данных процессов ЕнЕ' параллельная композиция даёт процесс Е ¡| Е\ способный выполнять действия Ей Е'параллельно, т.е. либо произвольно чередуя их, либо синхронизируя работу (в случае передачи данных по каналу).

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

Декларацией процесса называется совокупность Д рекурсивных уравнений процессов Д = {X ] 1 < i < п}, где п е N, переменные X, все различны, и где выражения Е, используют только те переменные, которые принадлежат множеству PHA)=def {Xt, Более того,

если выражение Et строится с помощью оператора параллельной композиции ||, запретим использование в этом выражении переменной Х-,.

Каждая декларация процессов А задаёт систему помеченных переходов: управляющими состояниями в ней являются выражения процессов (в данной семантике их конечное число), построенные на множестве Рг{А), множество меток задаётся как Act = Actyar kj ActCM, и отношение переходов определяется с помощью следующих правил вывода.

Е а >Е' «Г

cc.E-2-^E; Х = Е е А; -J—-j е /;

E

E-^E' F v?* >F' veCihU -------г e Exp,

E\\F (vtev?J) >£'ЦГ XeVar.

Последнее правою означает одновременное взаимодействие между процессами, связанное с передачей значения выражения е в переменную х через канал v, т.е. после срабатызанля перехода с пометкой а - (v!e, v?x) переменная х становится равной значению выражения е. Если есть процесс вида v\e.E (или coot. vIx.E), где v е Chi, е € Ехр, он; может перейти в процесс Е тогда и только тогда, когда в параллельной композиции будет процесс vIxF (coot. vlc.F), который при одновременном срабатывании перейдёт в F.

Для того, чтобы система переходов, порождаемая декларацией процессов Д, была вполне структурированной системой переходоз автоматного типа WTA - (S, Г, -», s0), где Т-Act, необходимо на Д наложить дополнительные ограничения. Положим, что на множестве D задан вполне упорядочиваемый квазипорядок <. Далее, нами будут рассматриваться только те выражения е(х/,...,xr) е Ехр, которые представляют, собой монотонную функцию по своим переменным относительно вполне упорядочиваемого квазипорядка <;, т.е. для любых двух векторов значений переменных (rf/,..., d„) < (с//'..., d„) должно выполняться условие e{di.....¿4) <e(rf/',...,</„).

Тогда, состояние s системы WTA будет представлять собой пару (q, d), где q е Q-это выражение процессов, a d = (d\,...,¿4) - вектор значений всех переменных (при условий, что переменные некоторым образом упорядочены), к - \Var\. Начальное состояние sg есть (qo, do), где qo соответствует выражению процесса Xi, a do - вектор начальных значений переменных. Из определения декларации процессов Д следует, что множество Q конечно. Но множество S системы fJTA бесконечное, т.к. векторов значений переменных может быть бесконечно много. Более того, на множестве S можно задать вполне упорядочиваемый квазипорядок <!VTA так, что 5 = (q, d) <im s'=(q'y d') о q = q'u d£d'.

В разделе 3.2 рассматривается конкретная реализация взаимодействующих процессов независимых от данных - взаимодействующие раскрашивающие процессы (ССР).

Для этого определяется новое множество Ц типов (или цветов) данных. Описывается тип переменных из Var как мультимножество над Без нарушения условия монотонности задаются допустимые для данного формализма выражения eQcj,..., х„).

Итак, выражение е(х;,..., х„) в рамках ССР может быть одного из следующих видов:

= х, + х2\ eJxiji) = х,и х2\

еф,) = xi (-) т\ en(xi)=x, пт,

е,(х,) = х,\С; efai) = xj/C,

где CcZ, а т принадлежит множеству всех возможных мультимножеств над

Выражения вида e+(yj) = y + z или ejy,z) - у и г моделируют формирование (построение) нового пакета данных из данных других пакетов, находящихся в переменных у и г, который, например, с помощью действия х\в помещается в переменную х.

Выражения е\(х) =х\С, е{х) = х/ С или ¿(.)(х) - х (-) т в сочетании с действием х!е(д;) могут интерпретироваться как извлечение данных из пакета переменной х.

Выражения v!e(x;,x2) и v?x означают отправку и приём пакета данных через канал v соответственно.

Оператор Г\ может быть использован для формирования пакета данных определённого формата. Например, последовательность действий z!(jnm), х!(х (-) т), v!z означает передачу пакета данных формата т через канал v; оператор п ограничивает размер передаваемых за один раз данных. .

Таким образом, состояние ССР - это набор (д, ..,т„), где q -локальное состояние (определяемое декларацией процессов А, представляющее собой выражение процессов, a mt,..., т„ - мультимножества, являющиеся содержимым соответствующих переменных.

Раскраска (colouring) ССР - это отображение М множества переменных Var на множество всех возможных мультимножеств над £.

Определим на множестве переменных Var некоторый порядок, т.е. Var = (xi,...jc„), тогда раскраска М - это вектор из мультимножеств М=(т/,.. .,тп), где V/ (1 й i<. и) mt - М(х,), п = \ Varf.

Тогда состояние ССР может быть представлено как {q, М).

Исполнение ССР - это последовательность состояний, начинающаяся в начальном состоянии (qo, Mo), где q0 представляет собой начальное выражение процесса Xi, которая строится в соответствии с правилами переходов.

Каждое срабатывание перехода q—'—^q'переводит ССР из состояния (q, М) в некоторое последующее состояние {q^M1), где М' вычисляется в соответствии с выражением, ассоциированным с меткой действия перехода t.

В разделе 3.3 формальные модели ССР рассматриваются как вполне структурированные системы переходов автоматного типа.

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

В разделе 3.4 приводится пример модели ССР.

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

В разделе 4.1 приводится мотивация построения-недетермини-рованных счётчиковых машин.

Распределенные и параллельные системы обычно моделируются системами переходов с конечным числом управляющих состояний! и с различными видами переменных и структур данных, таких как. счётчики, очереди и т.д. Многие системы переходов можно рассматривать как машины Тьюринга (системы равномощные машинам-Тьюринга) с ослаблениями, такими как наличие недетерминизма в; правилах переходов из одной конфигурации в другую или же включения отношения потери. Чтобы оценить уровень ослабления для некоторых классов систем, вводятся абстрактные машины, с помощью которых определяется круг задач, которые по-прежнему остаются неразрешимыми. К таким абстрактным машинам можно отнести счётчиковые машины с потерями, которые были введены, R. Mayer для систем с потерями, использующихся для моделирования передачи данных через ненадёжные каналы связи (например, FIFO-канальные системы с потерями).

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

В разделе 4.2 даётся следующее

Определение 4.2.1 Недетерминированная счётчиковая машина псМ-это набор из четырёх элементов (Q, Г), где X/ - счётчик, Q - {go,-.., qn) - конечное множество состояний, q0 - начальное состояние, q„ - финальное состояние, Г- конечное множество меток действий, соответствующих выражению над счётчиками, -> Q Q\q„ х Тх Q- отношение переходов. Переход из одной конфигурации в другую может быть одного из следующих видов

(при?—'-±q'):

(q. ci,...,ci,...,c„)—-->(</', ci,...,ci+\,...,c,n), если t соответствует выражению Xj := x, + 1;

(q, Ci,..:,Ci.....cm)—^-»О?', c/,...,c',...,cv), где = О при с,-О и

с, - 1 при Cj > 0, если метка t соответствует выражению х, := х,- (-) 1;

(q, ch....ch...,cm)—L~>( q', с;,..., 0,...,cm), если / соответствует выражению Xi := 0;

(q,Ci,...,ch...,cm)-J-*( q,,cj,..,,c/i,..,>cm), где c', = c,+ 1 при С/й1и с\-с, при с,—0, если метка перехода t соответствует выражению Xi :=*,+ min(^,l)-

Недетерминированная ш-счёршкоЕая машина псМ рассматривается как помеченная система переходов. Естественным образом задаётся отношение ¿ вполне упорядоченного квазипорядка па множестве конфигураций машины псМ{т.е. на множестве состояний системы переходов).

Утверягдение 4.2.1. Система переходов (?;сЛ/, <) является эффективной по пересечению вполне структурированной системой переходов с совместимостью по возрастанию и убыванию (автоматного типа) и с эффективным предбазисом.

В разделе 4.3 доказывается, что проблемы ограниченности и тотальной ограниченное! и для недетерминированной 4-х счётчико-вой машины неразрешимы (следствие 4.3.1 и утверждение 4.3.2).

В разделе 4.4 доказывается неразрешимость для недетерминированных счётчикоаых машин проблем включения и эквивалентности (теоремы 4.4.1 и 4.4.2).

В разделе 4.5 рассматривается задача достижимости.

Утверждение 4.5.1; Для недетерминированных счётчиковых машин задача достижимости некоторой нулевой конфигурации (q, 0,...,0) разрешима.

Теорема 4.5.1. Проблема достижимости является неразрешимой для недетерминированной 4-х счётчикосой машины и вектора значений счётчиков (с/, с2, Сз, с4) > (0, 0, 0, 0).

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ И ВЫВОДЫ

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

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

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Kouzmin E.Y., Shilov N.Y., Sokolov YA. Model Checking ц- Calculus in Well-Structured Transition Systems // Proc. of 11th International Symposium on Temporal Representation and Reasoning, Tatihou, France, IEEE Press, 2004. P. 152-155.

2. Kouzmin EY., Shilov NY., Sokolov YA. Model Checking ц-Calculus in Well-Structured Transition Systems // Joint Bulletin of NCC & IIS, Сотр. Science, Novosibirsk, n. 20, 2004. P. 97-107.

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

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

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

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

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

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

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

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

Лицензия ПД 00661 от 30.06.2002 г. Заказ 1294. Тираж 100. Печ. л. 1. Отпечатано в типографии Ярославского государственного технического университета г. Ярославль, ул. Советская, 14 а, тел. 30-56-63.

04 "1 5838

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.4 Пример.

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

4.1 Введение.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Заключение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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