Современные проблемы информатики Лекция 1 Введение Транзиционные системы

2 План лекций Теория взаимодействующих процессов (CCS, CSP, ACP) Инсерционное программирование (агенты и среды) Темпоральная логика и проверка моделей (model checking) Верификация софтвера (MSC, SDL, UML) Пруверы и солверы

3 Теории взаимодействия и параллелизма (communication, interaction and concurrency) Структурная теория автоматов Сети Петри CCS => π-calculus (R.Milner) CSP (T.Hoar) ACP (J.A.Bergstra, J.W.Klop) => Handbook on Process Algebra (2000) Коалгебры (J.J.M.M.Rutten, TCS 249(2000)) Mobile ambients (L.Cardelli, A.Gordon) Агенты и среды (инсерционное программирование) (A.Letichevsky, D.Gilbert, 1999)

4 Транзиционные системы Ординарные транзиционные (динамические) системы : S – пространство состояний Т – отношение переходов Транзитивное замыкание Движение в фазовом пространстве (поток) Изменение состояния электронной системы Изменение состояния софтверной системы

5 D.Park (1981) Размеченные транзиционные системы А – множество меток символы, события, действия Автоматы: входные символы, вход/выход Программы: операторы, условия Исчисления: состояния – формулы, действия – правила вывода Взаимодействующие распределенные системы: передача (прием) сообщений Базы данных запросы, ответы

6 Смешанные системы наблюдаемые переходы скрытые переходы

7 Атрибутные транзиционные системы D={0,1} (Не размеченные переходы) Автоматы Мура Программы над памятью Типизированная память Системы Крипке (модальная логика)

8 Настроенные системы Другие важные классы транзиционных систем: Стохастические и нечеткие; Системы реального времени. начальные состояния заключительные состояния неопределенные состояния

9 Применения Моделирование поведения и взаимодействия Исследование моделей и предсказание Спецификация Верификация Генерация кода Генерация тестов Софтвер Хардвер Экологические Социальные Средства исследования моделей ДоказательстваМоделирование + Системы Биологические

10 Трассовая эквивалентность История: Трасса: Трасса для атрибутной системы: трассы из в

11 Система детерминирована:

12 s s's'

13 Бисимуляционная эквивалентность bisimilarity (Milner 1980, D.Park 1981) Отношение бисимуляции (bisimulation): a R s a t R a R s a t R

14 Бисимуляция есть эквивалентность Бисимуляционная эквивалентность состояний совпадает с максимальной бисимуляцией на S. a s a t a

15 Отношение бисимуляции распространяется на состояния разных систем. Для детерминированных систем бисимуляционная эквивалентность состояний совпадает с трассовой. Бисимуляционная эквивалентность систем R R R R R R

16 Бисимуляционная эквивалентность смешанных систем

17 Редукция смешанных систем Добавляем новые переходы и настройку состояний: ss ssss a a, * )()(, * SSsSSsss Удаляем скрытые переходы

18 Смешанная транзиционная система и ее редукция бисимуляционно эквивалентны бисимуляция смешанная система ее редукция