Современные проблемы информатики Лекция 2 Алгебра поведений
2 Что такое поведение? (инвариант бисимуляционной эквивалентности) 1.Domain theory approach (S.Abramsky 1991) 2.ACP with recursion (J.A.Bergstra and J.W.Klop, 1984) 3.Coalgebraic approach (P.Aczel, 1988, later B.Jecobs and J.Rutten) 4.Continuous algebras (A.Letichevsky,D.Gilbert,1997) В теории автоматов: Автомат есть транзиционная система, размеченная парами вход/выход Поведение есть автоматное отображение Или Автомат есть настроенная транзиционная система, размеченная входными символами Поведение есть язык
3 Алгебра поведений Два сорта: –U – поведения –A – действия Сигнатура: –префиксинг a.u –недетерминированный выбор u + v –константы –отношение аппроксимации Аксиомы: –аci для недетерминированного выбора –0 есть нейтральный элемент недетерминированного выбора – есть отношение частичного порядка с наименьшим элементом –Обе операции монотонны и непрерывны (сохраняют наименьшие верхние грани) Дополнительные структуры: Действия: комбинация действий, невозможное и нейтральное действия Атрибуты: функции на поведениях
4 Монотонность
5 Непрерывность Направленное множество Наименьшая верхняя грань Непрерывность
6 Монотонность следует из непрерывности
7 Поведение есть элемент алгебры поведений a a b a b a a a.(a+b+ )+b.a.(a+a.0) a. = a
8 Как построить алгебру всех поведений произвольных систем над множеством действий А? )()()(AFAFAF fin Алгебра конечных поведений Алгебра поведений конечной высоты Алгебра бесконечных поведений
9 Алгебра конечных поведений F fin (A) Порождается терминальными константами 0, Состоит из выражений в сигнатуре +, (().()) Отношение аппроксимации: v 1 v 2 v n
10 Каноническая форма I – конечное множество индексов, Если все a i. u i различны и u i представлены в такой же форме, то представление u единственно с точностью до коммутативности недетерминированного выбора. Индукция по высоте терма h(u) u сходится, если и расходится в противном случае
11 Критерий аппроксимации Индукция по высоте u
12 F fin (A) есть инициальная алгебра поведений Антисимметричность (индукция) Свободные алгебры поведений F fin (A,X)
13 Алгебра поведений конечной высоты I произвольное множество (может быть пустое) Критерий аппроксимации – определение. Операции:
14 Полная алгебра поведений F(A) Элементы: классы эквивалентности направленных множеств поведений конечной высоты От классов к представителям. Предел направленного множества направленных множеств = их объединение. Бесконечные суммы:
15 Каноническая форма в алгебре F(A) Такое представление единственно, если все различны
16 Теорема о неподвижной точке Добавление переменных:
17 Следующая лекция Поведение транзиционных систем Транзиционная система => поведение => транзиционная система