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

Е. В. Кузьмин В. А. Соколов СТРУКТУРИРОВАННЫЕ СИСТЕМЫ ПЕРЕХОДОВ 2006 УДК 519. 68, 519. 69 *j Издание осуществлено при поддержке ББК В18 I* <з!рж Российского фонда фундаментальных К 39 ** исследований по проекту 05-017-95008д Кузьмин Е. В. , Соколов В. А. Структурированные системы переходов. - М. : ФИЗМАТЛИТ, 2006. — 176 с. — ISBN 5-9221-0692-9. В монографии рассматривается класс вполне структурированных систем помеченных переходов, представляющих собой формализм для моделирования и анализа корректности параллельных и распределен- распределенных систем, таких как вычислительные машины и комплексы с па- параллельной и распределённой архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процес- бизнес-процессов, при этом основное внимание уделяется разрешимости классиче- классических проблем ограниченности, достижимости, покрытия, неизбежно- неизбежности, поддержки управляющего состояния, останова, эквивалентности и других важных семантических и темпоральных свойств. Для научных работников, преподавателей, аспирантов и студентов, интересующихся формальными методами моделирования, анализа и верификации параллельных и распределенных систем. Ил. 23. Библиогр. 90 назв. © ФИЗМАТЛИТ, 2006 ISBN 5-9221-0692-9 © Е. В. Кузьмин, В. А. Соколов, 2006 ОГЛАВЛЕНИЕ Предисловие 5 Введение 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. Дерево разрешимости темпоральных логик 162 Заключение 163 Список литературы 166 Предметный указатель 172 Список обозначений 174 Предисловие Современный период развития информатики и вычислитель- вычислительной техники характеризуется широким использованием парал- параллельных и распределенных систем, поведение которых отличает- отличается высокой степенью сложности. Это обстоятельство выдвигает новые задачи в области моделирования и анализа корректности таких систем.