Теория процессов
 Скачать 1.62 Mb.
|
|
• оператора проверки условия op = b? знакосочетание Op · op обозначает объект, который 203 • либо является СО, • либо не определён. Данный объект определяется рекурсивно следующим обра- зом. Если n = 1, то Op · op def = ((cond (Op) ∧ b) ?) иначе – • если op n – оператор присваивания вида (x := e), то Op · op def = ((op 1 , . . . , op n−1 ) · op n (op)) | {z } (∗) ·op n где – op n (op) – оператор проверки условия, получаемый из op заменой всех вхождений в него переменной x на выражение e – если объект (∗) не определён, то Op · op тоже не определён • если op n – оператор вывода, то Op · op есть СО ((op 1 , . . . , op n−1 ) · op) · op n (7.19) • если op n – оператор ввода, и имеет вид α ? x, то Op · op – не определён, если op зависит от x – равен СО (7.19), в противном случае. Теперь можно сформулировать определение конкатенации СО. Пусть заданы два СО Op 1 , Op 2 , причём Op 2 имеет вид Op 2 = (op 1 , . . . , op n ) Мы будем говорить, что определена конкатенация СО Op 1 и Op 2 , если выполнены следующие условия: • хотя бы один из СО Op 1 , Op 2 является внутренним 204 • определены все объекты в скобках в выражении (. . . ((Op 1 · op 1 ) · op 2 ) · . . .) · op n (7.20) Если эти условия выполнены, то конкатенацией Op 1 и Op 2 назы- вается СО Op 1 · Op 2 который равен значению выражения (7.20). 7.8.8 Редукция процессов с СО Пусть P - процесс с СО. Редукция процесса P представляет собой последовательность P = P 0 - P 1 - - P n (7.21) преобразований этого процесса, каждое из которых производит- ся согласно какому-либо из излагаемых ниже правил. Каждое из этих преобразований (кроме первого) производится над резуль- татом предыдущего преобразования. Результатом редукции (7.21) является результат последнего из преобразований (т.е. процесс P n ). Правила редукции имеют следующий вид. Правило 1 (конкатенация). Пусть s – некоторое состояние процесса с СО, которое не является начальным, и • совокупность всех переходов этого процесса с концом s имеет вид s 1 - Op 1 s, . . . , s n - Op n s • совокупность всех переходов этого процесса с началом s имеет вид s - Op 0 1 s 0 1 , . . . , s - Op 0 m s 0 m • s 6∈ {s 1 , . . . , s n , s 0 1 , . . . , s 0 m } 205 • для каждого i = 1, . . . , n и каждого j = 1, . . . , m опре- делена конкатенация Op i · Op j Тогда данный процесс можно преобразовать в процесс, • состояниями которого являются состояния исходного процесса, за исключением s • переходами которого являются – те переходы исходного процесса, началом или кон- цом которых не является s, – а также переходы вида s i - Op i ·Op 0 j s 0 j для каждого i = 1, . . . , n и каждого j = 1, . . . , m • – начальное состояние которого, а также – множество переменных, и – начальное условие совпадают с соответствующими компонентами исход- ного процесса. Правило 2 (склейка). Пусть P – процесс с СО, который содержит два перехода с общим началом и общим концом s 1 - Op s 2 , s 1 - Op 0 s 2 (7.22) причём метки этих переходов различаются только в первой компоненте, т.е. Op и Op 0 имеют вид Op = (op 1 , op 2 , . . . , op n ) Op 0 = (op 0 1 , op 2 , . . . , op n ) Правило 2 заключается в замене пары переходов (7.22) на один переход вида s 1 - Op s 2 где Op = ((cond (Op) ∨ cond (Op 0 )) ?, op 2 , . . . , op n ) 206 Правило 3 (удаление несущественных присваиваний). Пусть P – некоторый процесс с СО. Обозначим знакосочетанием op(P ) совокупность всех опе- раторов, входящих в какой-либо из СО процесса P . Будем называть переменную x ∈ X P несущественной, если • x не входит ни в один из – операторов проверки условия, и – операторов вывода из op(P ) • если x входит в правую часть какого-либо оператора присваивания из op(P ) вида (y := e), то переменная y – несущественная. Правило 3 заключается в удалении из всех СО редуцируе- мого процесса операторов присваивания вида (x := e), где переменная x – несущественная. 7.8.9 Пример редукции Рассмотрим в качестве примера редукцию процесса Buffer n (гра- фовое представление которого приведено в параграфе 7.5.3). Ниже мы будем использовать следующее соглашение: • если в СО Op cond (Op) = > то первый оператор в таком СО мы писать не будем • операторы, входящие в СО, можно располагать не только по горизонтали, но и по вертикали • скобки, в которые заключена последовательность операто- ров, из которых состоит СО, можно опускать. Исходный процесс Buffer n имеет следующий вид: 207 B D C E L F M ? @ @ @ @ @ @ @ @ @ R ? ? ? ? - - O P - k := k + 1 k := k − 1 In ? f Out ! ˆ q q := q · [f ] q := q 0 In ? f Out ! ˆ q (k > 0) ? (k < n) ? (k ≤ 0) ? (k ≥ n) ? Первый шаг редукции заключается в удалении состояния C (применяется правило 1 для s = C): B D E L F M ? @ @ @ @ @ @ @ @ @ R ? ? ? ? - - O P - k := k + 1 k := k − 1 In ? f Out ! ˆ q q := q · [f ] q := q 0 In ? f Out ! ˆ q ( k < n k > 0 ) ? ( k < n k ≤ 0 ) ? (k ≥ n) ? 208 Поскольку n > 0, то формулу (k < n) ∧ (k ≤ 0) в метке перехода из B в D можно заменить на равносильную формулу k ≤ 0. Второй и третий шаги редукции – удаление состояний O и P : B D E L F M ? @ @ @ @ @ @ @ @ @ R ? ? ? ? - - In ? f Out ! ˆ q q := q · [f ] k := k + 1 q := q 0 k := k − 1 In ? f Out ! ˆ q (0 < k < n) ? (k ≤ 0) ? (k ≥ n) ? Четвёртый и пятый шаги редукции – удаление состояний D и E: 209 B L F M ? @ @ @ @ @ @ @ @ @ @ ? ? ? ? - - In ? f Out ! ˆ q q := q · [f ] k := k + 1 q := q 0 k := k − 1 (0 < k < n) ? (k ≤ 0) ? In ? f (k ≥ n) ? Out ! ˆ q Шестой шаг редукции – удаление состояния F : B L M A A A A A A A A A A A A A A A A A A U @ @ @ @ @ @ @ @ @ @ ? ? - q := q · [f ] k := k + 1 q := q 0 k := k − 1 (0 < k < n) ? In ? f (0 < k < n) ? Out ! ˆ q (k ≤ 0) ? In ? f (k ≥ n) ? Out ! ˆ q 210 Седьмой и восьмой шаги редукции – применение правила 2 к переходам вида B → L и B → M . В получившемся процессе мы заменяем • формулу (0 < k < n) ∨ (k ≤ 0) – на равносильную ей фор- мулу (k < n) • формулу (0 < k < n) ∨ (k ≥ n) – на равносильную ей формулу (k > 0) B L M A A A A A A A A A A A A A A A A A A U - q := q · [f ] k := k + 1 q := q 0 k := k − 1 (k > 0) ? Out ! ˆ q (k < n) ? In ? f Девятый и десятый шаги редукции – удаление состояний L и M . В результате мы получаем не редуцируемый далее процесс с СО с одним состоянием: B - (k < n) ? In ? f q := q · [f ] k := k + 1 (k > 0) ? Out ! ˆ q q := q 0 k := k − 1 (7.23) 211 7.8.10 Понятие конкретизации процесса с СО Для процессов с СО можно определить понятие конкретизации, аналогично тому, как это было сделано для обычных процессов с передачей сообщений в параграфе 7.7.1. Для каждого процесса с СО P знакосочетание Conc(P ) обо- значает процесс в исходном смысле данного понятия (см. пара- граф 2.4), который называется конкретизацией процесса P , и имеет следующие компоненты. 1. Состояниями Conc(P ) являются • всевозможные означивания из Eval(X P ), • а также дополнительное состояние s 0 , которое являет- ся начальным в Conc(P ) 2. Для • каждого перехода s 1 - Op s 2 процесса P , и • каждого означивания ξ ∈ Eval(X P ), такого, что – ξ(at P ) = s 1 , и – Op открыт на ξ Conc(P ) содержит переход ξ - a ξ 0 если ξ 0 (at P ) = s 2 , и имеет место один из следующих случа- ев: (a) Op – внутренний, a = τ , и имеет место соотношение ξ - Op ξ 0 которое означает следующее: если Op имеет вид (op 1 , . . . , op n ) то существует последовательность ξ 1 , . . . , ξ n означива- ний из Eval(X P ), такая, что 212 • ∀ x ∈ X P \ {at P } ξ(x) = ξ 1 (x), ξ 0 (x) = ξ n (x), и • ∀ i = 2, . . . , n, если op i имеет вид (x := e), то ξ i (x) = ξ i−1 (e), ∀y ∈ X P \{x, at P } ξ i (y) = ξ i−1 (y) (b) • Op = Op 1 · (α ? x) · Op 2 , • a = α ? v, где v – произвольное значение из D t(x) , и • существуют означивания ξ 1 и ξ 2 из Eval(X P ), та- кие, что ξ - Op 1 ξ 1 , ξ 2 - Op 2 ξ 0 ξ 2 (x) = v, ∀y ∈ X P \ {x, at P } ξ 2 (y) = ξ 1 (y) (c) • Op = Op 1 · (α ! e) · Op 2 , • существует означивание ξ 1 из Eval(X P ), такое, что ξ - Op 1 ξ 1 , ξ 1 - Op 2 ξ 0 , a = α ! ξ 1 (e) 3. Для • каждого означивания ξ ∈ Eval(X P ), такого, что ξ(I P ) = 1 • и каждого перехода в Conc(P ) вида ξ - a ξ 0 Conc(P ) содержит переход s 0 - a ξ 0 Читателю предлагается самостоятельно исследовать взаимо- связь между • конкретизацией произвольного процесса с передачей сооб- щений P , в том смысле, в каком это понятие было опреде- лено в параграфе 7.7.1, и • конкретизацией процесса с СО, полученного в результате редукции процесса P . 213 7.8.11 Отношения эквивалентности на процес- сах с СО Пусть P 1 и P 2 – процессы с СО. Мы будем говорить, что P 1 и P 2 наблюдаемо эквивалент- ны, и обозначать этот факт знакосочетанием P 1 ≈ P 2 если их конкретизации наблюдаемо эквивалентны (в исходном смысле данного понятия, см. параграф 4.8). Аналогичным образом определяется отношение + ≈ наблюдае- мой конгруэнции на процессах с СО. Используя понятие редукции процессов с СО, можно опреде- лить ещё одно отношение эквивалентности на множестве процес- сов с СО. Данное отношение • обозначается символом r ≈ , и • представляет собой минимальную конгруэнцию на множе- стве процессов с СО, обладающую следующим свойством: если P 0 получается из P в результате применения какого- либо правила редукции, то P r ≈ P 0 (т.е. r ≈ является пересечением всех конгруэнций на множестве процессов с СО, обладающих вышеуказанным свойством). Читателю предлагается самостоятельно • исследовать связь операций на процессах с СО с отноше- ниями ≈ и + ≈, т.е. установить свойства, аналогичные свой- ствам, изложенным в параграфах 3.7, 4.5, 4.8.4, 4.9.5 • сформулировать и обосновать необходимые и достаточные условия наблюдаемой эквивалентности процессов с СО, не использующие понятие конкретизации • исследовать взаимосвязь между отношениями ≈, + ≈ и r ≈ • найти такие правила редукции, чтобы было верно включе- ние r ≈ ⊆ + ≈ 214 7.8.12 Метод доказательства наблюдаемой эк- вивалентности процессов с СО Один из возможных методов доказательства наблюдаемой экви- валентности процессов с СО основан на излагаемой ниже теореме 34. Для формулировки этой теоремы мы введём вспомогатель- ные понятия и обозначения. 1. Пусть P – процесс с СО. Составной переход (СП) в P – это (возможно пустая) последовательность CT переходов процесса P вида CT = s 0 - Op 1 s 1 - Op 2 - Op n s n (n ≥ 0) (7.24) такая, что • среди Op 1 , . . . , Op n – не более одного СО ввода или вывода • определена конкатенация (. . . (Op 1 · Op 2 ) · . . .) · Op n которую мы будем обозначать тем же символом CT . Если последовательность (7.24) пуста, то её конкатенацией CT по определению является СО (>?). Состояние s 0 называется началом СП (7.24), а состояние s n – его концом. Знакосочетание s 0 - CT s n является сокращённой запи- сью утверждения о том, что CT – это • СП с началом s 0 и концом s n • а также – СО, соответствующий этому СП. 2. Пусть ϕ и ψ – формулы. Знакосочетание ϕ ≤ ψ является сокращённой записью утвер- ждения о том, что формула ϕ → ψ является тождественно истинной. 215 3. Пусть Op = (op 1 , . . . , op n ) – внутренний СО, и ϕ – формула. Знакосочетание Op(ϕ) обозначает формулу, определяемую рекурсивно: Op(ϕ) def = ( cond (Op) → ϕ, если n = 1 (op 1 , . . . , op n−1 ) (op n (ϕ)), если n > 1 где op n (ϕ) обозначает формулу, определяемую следующим образом: если op n имеет вид (x := e), то op n (ϕ) получается из ϕ заменой каждого вхождения в неё переменной x на выражение e. 4. Пусть ϕ, ψ – формулы, и Op 1 , Op 2 – СО. Мы будем говорить, что верна диаграмма A B ϕ ? Op 1 ? Op 2 C D ψ (7.25) если выполнено одно из следующих условий. (a) Op 1 и Op 2 – внутренние СО, и верно неравенство ϕ ≤ (Op 1 · Op 2 )(ψ) (b) Op 1 и Op 2 можно представить в виде конкатенаций Op 1 = Op 3 · (α ? x) · Op 4 Op 2 = Op 5 · (α ? y) · Op 6 где Op 3 , Op 4 , Op 5 , Op 6 – внутренние СО, и верно нера- венство ϕ ≤ (Op 0 1 · Op 0 2 )(ψ) где 216 • Op 0 1 = Op 3 · (x := z) · Op 4 • Op 0 2 = Op 5 · (y := z) · Op 6 • z – новая переменная (т.е. не входящая в ϕ, ψ, Op 1 , Op 2 ) (c) Op 1 и Op 2 можно представить в виде конкатенаций Op 1 = Op 3 · (α ! e 1 ) · Op 4 Op 2 = Op 5 · (α ! e 2 ) · Op 6 где Op 3 , Op 4 , Op 5 , Op 6 – внутренние СО, и верно нера- венство ϕ ≤ ( (Op 3 · Op 5 )(e 1 = e 2 ) (Op 3 · Op 4 · Op 5 · Op 6 )(ψ) ) Теорема 34. Пусть P 1 и P 2 – два процесса с СО: P i = (X P i , I P i , S P i , s 0 P i , R P i ) (i = 1, 2) не имеющие общих состояний и общих переменных. P 1 и P 2 находятся в отношении ≈, если существует функция µ вида µ : S P 1 × S P 2 → F m обладающая следующими свойствами. 1. I P 1 ∧ I P 2 ≤ µ(s 0 P 1 , s 0 P 2 ). 2. Для • каждой пары (A 1 , A 2 ) ∈ S P 1 × S P 2 , и • каждого перехода A 1 - Op A 0 1 процесса P 1 , такого, что cond (Op) ∧ µ(A 1 , A 2 ) 6= ⊥ (7.26) существует совокупность СП процесса P 2 с началом A 2 { A 2 - CT i A i 2 | i ∈ =} (7.27) удовлетворяющая следующим условиям: 217 (a) имеет место неравенство cond (Op) ∧ µ(A 1 , A 2 ) ≤ _ i∈= cond (CT i ) (7.28) (b) для каждого i ∈ = верна диаграмма A 1 A 2 µ(A 1 , A 2 ) ? Op ? CT i A 0 1 A i 2 µ(A 0 1 , A i 2 ) (7.29) 3. Свойство, симметричное предыдущему: для • каждой пары (A 1 , A 2 ) ∈ S P 1 × S P 2 , и • каждого перехода A 2 - Op A 0 2 процесса P 2 , такого, что верно (7.26) существует совокупность СП процесса P 1 с началом A 1 { A 1 - CT i A i 1 | i ∈ =} (7.30) удовлетворяющая следующим условиям: (a) имеет место неравенство (7.28) (b) для каждого i ∈ = верна диаграмма 218 A 1 A 2 µ(A 1 , A 2 ) ? CT i ? Op A i 1 A 0 2 µ(A i 1 , A 0 2 ) (7.31) 7.8.13 Пример доказательства наблюдаемой эк- вивалентности процессов с СО В качестве примера использования теоремы 34 докажем наблю- даемую эквивалентность Buffer 1 ≈ Buf где • Buffer 1 – это рассмотренный выше процесс Buffer n (см. (7.23)) при n = 1, т.е. процесс, имеющий вид A - (k < 1) ? In ? f q := q · [f ] k := k + 1 |