ГЛАВА 2. АТРИБУТНЫЕ ТРАНЗИЦИОННЫЕ СИСТЕМЫ И БАЗОВЫЕ ПРОТОКОЛЫ.
2.1 Атрибутные транзиционные системы
В этой главе рассматриваются спецификации взаимодействующих систем, представляемых в виде композиции среды и погружаемых в нее агентов. Среды, рассматриваемые в работе, представляют собой атрибутные транзиционные системы. Это значит, что помимо разметки переходов (действиями) используется также разметка состояний. Формально, атрибутная транзиционная система определяется как набор следующих компонент:
* S - множество состояний;
* А - множество действий;
* - множество размеченных переходов и неразмеченных (скрытых) переходов ;
* L - множество атрибутных разметок;
* - частично определенная функция разметки состояний.
Первые три компоненты задают обычную размеченную транзиционную систему, остальные две добавляют атрибутные характеристики. Множества A и L образуют сигнатуру системы. Если l(s) не определено, то состояние s называется неразмеченным. Разметку состояний можно вносить в обозначения переходов. Например, обозначает переход, размеченный действием a, из состояния s, размеченного разметкой , в состояние , а выражение обозначает скрытый переход из состояния s в неразмеченное состояние (таким образом, символ 1 используется для обозначения отсутствия разметки). Для унификации обозначений, скрытый переход будем также записывать в виде (наряду с ). Таким образом, в выражении либо , либо (т.е. разметка отсутствует). Разметку состояний можно совместить с разметкой переходов, введя расширенное множество размеченных действий . Теперь переход можно записать в виде .
Неразмеченные переходы вида (назовем их избыточными), при необходимости, могут быть элиминированы следующим образом: сначала добавляем переходы по правилам:
где , до тех пор, пока возможно (для этого может потребоваться бесконечное число шагов, на каждом из которых одновременно применяются все правила ко всем состояниям), затем удаляем все избыточные переходы. После такого преобразования в каждом неразмеченном переходе одно из состояний будет размечено. Интуиция этих преобразований состоит в следующем. Для атрибутных систем наблюдаемыми являются не только разметки переходов, но и разметки состояний. Неразмеченный переход, в котором хотя бы одно состояние размечено, наблюдаем, поскольку происходит смена разметок состояний (даже, если эти разметки совпадают). Изменения, которые происходят при прохождении последовательности избыточных переходов, не наблюдаемы, поэтому, после добавления новых переходов, их можно удалить. Если же допустить возможность переходов, размеченных размеченными действиями из неразмеченных состояний, то можно добавить также еще одно правило элиминации скрытых переходов:
где a - неразмеченное действие. После добавления таких переходов можно удалить не только избыточные, но и "полуизбыточные" переходы вида . Заметим, что эта конструкция требует расширения понятия атрибутной системы, но сводится к исходному понятию, путем применения последнего правила в обратном направлении.
Рассматривая введение и удаление избыточных и полуизбыточных переходов как эквивалентные преобразования, приходим к двум эквивалентным понятиям атрибутных транзиционных систем: системы с размеченными переходами и системы с размеченными состояниями. В дальнейшем, если не оговорено обратное, будем считать, что рассматриваются системы с размеченными переходами.
К основной структуре атрибутной транзиционной системы могут добавляться дополнительные структуры. Система может быть настроенной путем выделения множества начальных, заключительных и неопределенных состояний (обозначения , соответственно). В этом случае перед удалением избыточных переходов применяются правила расширения настройки:
Множество атрибутных отметок обычно структурируется тем или иным образом. Например, возможна такая структуризация: , где R - множество пропозициональных переменных (бинарных атрибутов). Если при этом все переходы скрытые, а все состояния размеченные, то получаем систему Крипке, наиболее часто используемый тип модели в теории проверки моделей (model checking [24]). Далее будет рассматриваться разметка состояний формулами некоторого логического языка, называемого базовым.
Состояния транзиционных систем обычно рассматриваются с точностью до бисимуляционной эквивалентности. Для атрибутных систем это понятие отличается от обычного только тем, что отношение бисимуляции требует сохранения атрибутных разметок для размеченных состояний.
Инвариантом бисимуляционной эквивалентности состояний является поведение системы в данном состоянии. Для обычных систем оно задается как элемент полной алгебры поведений F(A) (префиксинг a.u, недетерминированный выбор u+v, константы 0, , , отношение аппроксимации и наименьшие верхние грани направленных множеств поведений). Для атрибутных систем в качестве инвариантов бисимуляционной эквивалентности следует рассматривать размеченные поведения.
Алгебра размеченных поведений строится как трех основная алгебра. Основным множеством является множество U поведений. Некоторые из них могут быть размечены атрибутными разметками из L. К этим двум множествам добавляется множество действий А. Добавляется также операция разметки поведения атрибутной разметкой . Префиксинг и недетерминированный выбор определяются как обычно. Константы 0, и , могут быть как размеченными, так и неразмеченными, т.е. иметь вид , и . Отношение аппроксимации распространяется на размеченные поведения таким образом, что .
Построение полной алгебры F(A,L) размеченных поведений вполне аналогично построению алгебры F(A), равно как и доказательство теоремы о том, что два состояния атрибутной транзиционной системы бисимуляционно эквивалентны тогда и только тогда, когда их размеченные поведения совпадают. Имеет место также каноническая форма произвольного размеченного поведения, которая совпадает с канонической формой обычного поведения
если использовать размеченные действия и добав
- Київ+380960830922