Читать онлайн «Вполне стуктурированные системы помеченных переходов»

Е. В. Кузьмин В. А. Соколов ВПОЛНЕ СТРУКТУРИРОВАННЫЕ СИСТЕМЫ ПОМЕЧЕННЫХ ПЕРЕХОДОВ МОСКВА ФИЗМАТЛИТ 2005 УДК 519. 68/. 69 ББК В18 К89 Кузьмин Е. В. , Соколов В. А. Вполне структурированные системы помеченных переходов. — М. : ФИЗМАТЛИТ, 2005. — 176 с. - ISBN 5-9221-0598-1 В монографии рассматривается класс вполне структурированных систем помеченных переходов, представляющих собой формализм для моделирования и анализа корректности параллельных и распре- распределённых систем, таких как вычислительные машины и комплек- комплексы с параллельной и распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов, при этом основное внимание уделяется разрешимо- разрешимости классических проблем ограниченности, достижимости, покрытия, неизбежности, поддержки управляющего состояния, останова, эквива- эквивалентности и других важных семантических и темпоральных свойств. Книга предназначена для научных работников, преподавателей, аспирантов и студентов, интересующихся формальными методами мо- моделирования, анализа и верификации параллельных и распределенных систем. Рис. 23. Библиогр. : 90 назв. Рецензенты: доктор технических наук, профессор, главный научный сотрудник Института вычислительной математики и математической геофизики СО РАН О. Л. Бандман; лаборатория теоретического программирования Института систем информатики им. А. П. Ершова СО РАН Работа выполнена при поддержке Российского фонда фундаментальных исследований (проект 03-01-00804). © ФИЗМАТЛИТ, 2005 © Е. В. Кузьмин, 2005 ISBN 5-9221-0598-1 © В. А. Соколов, 2005 ОГЛАВЛЕНИЕ Предисловия рецензентов 5 Предисловие авторов 8 Введение 11 Глава 1. Вполне структурированные системы помеченных переходов 17 1. 1. Предварительные сведения 17 1. 1. 1. Мультимножества 17 1. 1. 2. Квазиупорядоченные множества 18 1. 1. 3. Правильный квазипорядок 19 1. 2. Системы помеченных переходов 25 1. 2. 1. Определение 25 1. 2. 2. Вполне структурированные системы помеченных переходов 27 1. 2. 3. Метод насыщения 28 1. 2. 4. Покрывающее дерево системы переходов 34 1. 2. 5. Строгая совместимость 37 1. 2. 6. Совместимость по убыванию 40 1. 2. 7. Системы переходов автоматного типа 43 1. 3. Примеры вполне структурированных систем помеченных переходов 46 1. 3. 1. Сети Петри 46 1. 3. 2. Системы с ненадёжными каналами 51 1. 3. 3. Системы переходов, независимых от данных 60 Глава 2. Счетчиковые машины 75 2. 1. Счетчиковые машины Минского 76 2. 2. Счетчиковые машины с потерями 80 2. 3. Счетчиковые машины с обнулениями и ошибками проверки на нуль 90 2. 4. Недетерминированные счетчиковые машины 102 Оглавление Глава 3. Темпоральные свойства систем переходов ... 113 3. 1. Метод проверки модели 113 3. 1. 1. Логики ветвящегося времени 116 3. 1. 2. Логики линейного времени 124 3. 1. 3. Сравнение логик 127 3. 2. Темпоральные свойства систем переходов 138 3. 2. 1. Системы переходов автоматного типа 138 3. 2. 2. Системы переходов с сильной и транзитивной совместимостью 155 3. 2. 3.