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

Содержание

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

Слайды и текст этой презентации

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

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

Слайд 2План лекций
Теория взаимодействующих процессов (CCS, CSP, ACP)
Инсерционное программирование (агенты и

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

Слайд 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)
Теории взаимодействия и параллелизма (communication, interaction and concurrency) Структурная теория автоматов Сети

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

переходов

Транзитивное замыкание

Движение в фазовом пространстве (поток)

Изменение состояния электронной системы

Изменение состояния софтверной системы

Транзиционные системы Ординарные транзиционные (динамические) системы : S – пространство состояний Т

Слайд 5D.Park (1981)
Размеченные транзиционные системы
А – множество меток
символы,

события,
действия

Автоматы:
входные символы, вход/выход

Программы:
операторы, условия

Исчисления:
состояния – формулы,
действия – правила вывода

Взаимодействующие распределенные системы:
передача (прием) сообщений

Базы данных
запросы, ответы

D.Park (1981) Размеченные транзиционные системы А – множество меток

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

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

Слайд 7Атрибутные транзиционные системы
D={0,1}

(Не размеченные переходы)
Автоматы Мура
Программы над памятью
Типизированная память
Системы Крипке (модальная

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

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

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

Слайд 9


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

Средства исследования моделей


Доказательства

Моделирование

+

Системы

Биологические

Применения Моделирование поведения и взаимодействия Исследование моделей и предсказание

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

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

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



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

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


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

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

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

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


эквивалентность состояний совпадает с трассовой.

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

Отношение бисимуляции распространяется на  состояния разных систем.  Для детерминированных систем

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

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

Слайд 17Редукция смешанных систем

Добавляем новые переходы и настройку состояний:



Удаляем скрытые переходы



Редукция смешанных систем   Добавляем новые переходы и настройку состояний:

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

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

Обратная связь

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

Email: Нажмите что бы посмотреть 

Что такое ThePresentation.ru?

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


Для правообладателей

Яндекс.Метрика