Сперва дадим несколько определений, необходимых для дальнейшего понимания материала доклада



Скачать 105.84 Kb.
Pdf просмотр
Дата04.04.2017
Размер105.84 Kb.
Просмотров382
Скачиваний0

Теория трасс
Сперва дадим несколько определений, необходимых для дальнейшего понимания материала доклада.
Определение. Множество M называется моноидом, если на нём введена операция "?", такая, что (a ? b) ? c = a ? (b ? c)
Определение. Произведением двух подмножеств моноида A, B ? M
называется множество X · Y = {x ? y : x ? X, y ? Y }
Определение. Пусть M
1
, M
2
- моноиды. M
1
Ч M
2
= {(a, b) : a ? M
1
, b ?
M
2
}
Замечание. Тогда (a, b) ? (c, d) = (a ? c, b ? d), единица - (1
M
1
, 1
M
2
)
Определение. Для X ? M возведение в степень:
X
0
= 1
X
n
= X
n?1
· X
Определение. Таким образом для X ? M можно определить операцию звезда(star) :
X
?
= {X
n
: n ? 0}
Замечание. Далее будем рассматривать множество ? и называть его алфавитом. ?
?
множество всех слов алфавита ? (напомним, что словом называется конечная последовательность "букв"из ?)
Определение. Свободным моноидом называется тройка (?
?
, ?, ?)
, где
?
- оператор.
Определение. Языком называется подмножество свободного моноида.
Определение. A называется M?автоматом называется тройка (Q, q
0
, F )
,
где
1. Q - подмножество множества всех функций из M в Q
2. q
0
? Q
- начальное состояние
3. F ? Q - множество конечных состояний
1

4. ?q ? Qq(xy) = q(x)q(y)
Замечание 1. Автомат называется конечным, если множество Q конечно.
Замечание 2. M-автомат рассматривается как устройство по распознанию подмножеств моноида M
Определение. Подмножество K множества M, распозноваемое автоматом
A
обозначается L(A) = {m ? K : q
0
(m) ? F }
Определение. Множество K ? M называется распознаваемым, если существует такой конечный автомат A, что L(A) = K
Определение. Множество всех подмножество M, распозноваемых каким- либо автоматом обозначается REC(M).
Определение. M-моноид. K ? M, m ? M. Левым частным называется множество K/m = {w ? M : mw ? K}
Определение. K ? M. Левым синтаксическим ограничением называется отношение эквивалентности ?
K
= {(m
1
, m
2
) ? M Ч M : K/m
1
= K/m
2
}
Теперь мы готовы к тому, чтобы сформулировать и доказать следующие утверждения:
Утверждение 1. M-моноид, K ? M. X ? REC(M) ??
K
- конечно
Доказательство:
?
: q
0
(m
1
) = q
0
(m
2
) ?
?
:
ч.т.д.
Утверждение 2. M-моноид ?
1. ?, M ? REC(M)
2. X, Y ? REC(M) ? X ? Y, X ? Y, X \ Y ? REC(M)
Доказательство:
1. ?m ? M : ?/m = ? ??
K
- конечно
?m ? M : M/m = M ??
K
- конечно Следовательно ?, M ? REC(M)
2. (X ? Y )/m = X/m для ?Y/m Пусть | ?
X
| = p,
| ?
Y
| = q
2
ч.т.д.
Определение. ? - алфавит, I ? ? Ч ? , для ?(a, b) ? I : ab = ba, I
называется множество независимых букв
Определение. Моноид M = (?
?
, I)
(где ?
?
- свободный моноид) называется моноид трасс (или trace-моноид). Обозначение: M(?, I)
Определение. Трассой (trace) называется множество всех слов полученное одно из дркгого последовательной перестановкой пар независимых букв.
Иначе говоря, трасса есть элемент моноида трасс.
Теперь мы готовы сформулировать основную проблему (Star problem):
Если T ? REC(M), верно ли, что T
?
? REC(M )
?
Этот вопрос остаётся открытым. Были сформулированы и доказаны несколко теорем, позволяющих приблизиться к ответу на этот вопрос.
Теорема (Mezei): Пусть M = A
?
Ч B
?
, где A, B - алфавиты, T ? M ?
T ? REC(M ) ?
T - конечное объединение множеств вида X Ч Y , где X ?
REC(A
?
), B ? REC(B
?
)
Теорема : Star Problem разрешима, если M = A
?
Ч {b}
?
Рассмотрим теперь практические применения сформулированных утверждений.
Трассовые структуры (trace structures) используются в
1. структурах Хоара
2. структурах, обрабатывающих события
3. основных областях алгебры
4. сетях Петри
5. системых асинхронной передачи данных
Рассмотрим следующий пример: пусть два процесса, P
1
и P
2
, будучи запущенны одновременно работают независимо, но время от времени обращаются к одной и той же критической области. Необходимо убедиться, что обращения процессов к критическим регионам не происходили одновременно: третий процесс S будет синхронизировать P
1
и P
2
, разрешая или запрещая обращение к "критической области".
3

Введём следующие обозначение элементарных операций:
1. w i
- работа вне "критической области"
2. e i
- вход в "критическую область"
3. c i
- работа в "критической области"
4. l i
- выход из "критической области"
В алгебре процессов введены следующие обозначения:
1.
- паралельное выполнение
2. + - недерминированный выбор
3. . - предшествующее действие
Пусть
1. SY S = P
0
S P
1 2. P
0
= w
0
. e
0
. l
0
. P
0 3. P
1
= w
1
. e
1
. l
1
. P
1 4. S = (e
0
. l
0
. S) + (e
1
. l
1
.S)
Моделирование процессов SY S с точки зрения множеств, состоящих из последовательностей выполняемых операций, можно представить множествами
P
i и S:
P
i
= { , w i
, w i
e i
, w i
e i
c i
, ...}
S = { , e
0
, e
1
, e
0
l
0
, e
1
l
1
, ...}
где - нулевой элемент
Теперь можно сформулировать
Определение. Структура Хоара это пара (H, ?), где ? это алфавит
(из элементарных операций), а H это непустое, замкнутое относительно операции взятия префикса подмонжество моноида ?
?
Мы помним I - множество независимых букв. Для нашего примера
I = {w
0
, c
0
} Ч {e
1
, l
1
, w
1
, c
1
} ? {w
1
, c
1
} Ч {e
0
, l
0
, w
0
, c
0
}
4

Основываясь на множестве независимых букв, поведение нашей системы будет моделироваться в терминах трасс, то есть классов эквивалентности:
?
I
- наименьшее синтаксическое ограничение, такое, что aIb ? ab
I
ba
В нашем примере w
0
w
1
e
0
I
w
0
e
0
w
1
и класс эквивалентности, содержащий w
0
w
1
e
0
- < w
0
w
1
e
0
>= {w
0
w
1
e
0
, w
0
w
0
e
1
, w
1
w
0
e
0
}
Определение. Трассовой структурой (trace structure) называется тройка
(M, ?, I)
, где (?, I) - независимый алфавит, I нерефлексивное, симметричное отношение ? ? Ч ?, для M верно:
1. ?t
I
t ? M ? t ? M
2. ?ta ? M ? t ? M
3. ?ta, tb ? M&aIb ? tab ? M
Замечание. M/
I
= {< w >: w ? M }
Логично определть некое соотношение между двумя разными трассовыми структурами, обладающими похожими свойствами. Для этого испльзуются морфизмы. Чтобы перейти к последним, необходимо дать следующее определение:
Определение. Частично вычислимая функция ? : ? ?
?
?
определяет
?(sa) = ?(s)?(a)
, если ?(a) определена и ?(s), если ?(a) не определена.
Определение. Морфизм структур Хоара (H, ?) ? (H , ? ) состоит из частично вычислимой функции ? : ? ?
?
?
, такой, что ?s ? H?(s) ? H
Определение. Морфизм трассовых структур (M, ?, I) ? (M , ? , I )
состоит из частично вычислимой функции ? : ? ?
?
?
, такой, что
1. если aIb, определены ?(a) & ?(b) ? ?(a)I ?(b) ?a, b ? ?
2. s ? M ? ?(s) ? M ?s ? M
5



Поделитесь с Вашими друзьями:


База данных защищена авторским правом ©nethash.ru 2019
обратиться к администрации

войти | регистрация
    Главная страница


загрузить материал