Теория процессов
 Скачать 1.62 Mb.
|
|
0 тоже будет эквивалент- ностью). Поэтому каждый из членов последовательности (4.33) определяет некоторое разбиение множества S 0 , и для каждого i ≥ 1, если µ i+1 6= µ i , то разбиение, соответствующее отноше- нию µ i+1 , является измельчением разбиения, соответствующего отношению µ i . Нетрудно показать, что таких измельчений может быть не больше, чем количество элементов в множестве S 0 Теорема 12. Процесс P 0 ∼ имеет наименьшее число состояний среди всех конечных процессов, которые сильно эквивалентны P . Доказательство. Пусть P 1 – некоторый конечный процесс, такой, что P 1 ∼ P . Выделим из P 1 достижимую часть P 0 1 и построим процесс (P 0 1 ) ∼ Как было установлено выше, P 1 ∼ P 0 1 ∼ (P 0 1 ) ∼ Кроме того, поскольку P ∼ P 0 ∼ P 0 ∼ и P ∼ P 1 , то, следовательно, P 0 ∼ ∼ (P 0 1 ) ∼ (4.45) Как было доказано в теореме 11, процессы P 0 ∼ и (P 0 1 ) ∼ минималь- ны. Отсюда и из (4.45) по теореме 10 следует, что процессы P 0 ∼ и (P 0 1 ) ∼ изоморфны. В частности, они имеют одинаковое число состояний. Поскольку • число состояний процесса (P 0 1 ) ∼ не превосходит числа со- стояний процесса P 0 1 , так как состояния процесса (P 0 1 ) ∼ яв- ляются классами разбиения множества состояний процесса P 0 1 , и • число состояний процесса P 0 1 не превосходит числа состо- яний процесса P 1 , так как множество состояний процесса P 0 1 является подмножеством множества состояний процес- са P 1 , 95 то, следовательно, число состояний процесса P 0 ∼ не превосходит числа состояний процесса P 1 4.8 Наблюдаемая эквивалентность 4.8.1 Определение наблюдаемой эквивалентно- сти Ещё одним вариантом понятия эквивалентности процессов яв- ляется наблюдаемая эквивалентность. Данное понятие ис- пользуется в тех ситуациях, когда мы рассматриваем невидимое действие τ как несущественное, и считаем две трассы одинако- выми, если одна может быть получена из другой путём вставок и/или удалений невидимых действий τ . Для определения понятия наблюдаемой эквивалентности мы введём вспомогательные обозначения. Пусть P и P 0 – некоторые процессы. 1. Знакосочетание P - τ ∗ P 0 (4.46) означает, что • или P = P 0 • или существует последовательность процессов P 1 , . . . , P n (n ≥ 2) таких, что – P 1 = P, P n = P 0 – для каждого i = 1, . . . , n − 1 P i - τ P i+1 (4.46) можно интерпретировать как утверждение о том, что процесс P , может незаметным для наблюдателя образом превратиться в процесс P 0 96 2. Для каждого действия a ∈ Act \ {τ } знакосочетание P - a τ P 0 (4.47) означает, что существуют процессы P 1 и P 2 со следующими свойствами: P - τ ∗ P 1 , P 1 - a P 2 , P 2 - τ ∗ P 0 (4.47) можно интерпретировать как утверждение о том, что процесс P , может • некоторым образом эволюционировать, так, что внеш- ним проявлением этой эволюции будет лишь исполне- ние действия a, • после чего вести себя как процесс P 0 Если имеет место (4.47), то мы будем говорить, что процесс P может наблюдаемо выполнить a, и после этого вести себя как P 0 Понятие наблюдаемой эквивалентности основано на следую- щем понимании эквивалентности процессов: если мы рассмат- риваем процессы P 1 и P 2 как эквивалентные, то должны быть выполнены следующие условия. 1. • Если один из этих процессов P i может незаметно пре- вратиться в некоторый процесс P 0 i , • то и другой процесс P j (j ∈ {1, 2} \ {i}) тоже дол- жен обладать способностью незаметно превратиться в некоторый процесс P 0 j , который эквивалентен P 0 i 2. • Если один из этих процессов P i может – наблюдаемо выполнить некоторое действие a ∈ Act \ {τ }, – и после этого вести себя как некоторый процесс P 0 i • то и другой процесс P j (j ∈ {1, 2} \ {i}) должен об- ладать способностью – наблюдаемо выполнить то же действие a, 97 – после чего вести себя как некоторый процесс P 0 j , который эквивалентен P 0 i Используя обозначения (4.46) и (4.47), вышеприведённое нефор- мально описанное понятие наблюдаемой эквивалентности можно выразить равносильным образом как некоторое бинарное отно- шение µ на множестве всех процессов, обладающее следующими свойствами. (1) Если (P 1 , P 2 ) ∈ µ, и для некоторого процесса P 0 1 верно утверждение P 1 - τ P 0 1 (4.48) то должен существовать процесс P 0 2 , такой, что выполнены условия P 2 - τ ∗ P 0 2 (4.49) и (P 0 1 , P 0 2 ) ∈ µ (4.50) (2) Симметричное свойство: если (P 1 , P 2 ) ∈ µ, и для некоторого процесса P 0 2 верно утверждение P 2 - τ P 0 2 (4.51) то должен существовать процесс P 0 1 , такой, что выполнены условия P 1 - τ ∗ P 0 1 (4.52) и (4.50). (3) Если (P 1 , P 2 ) ∈ µ, и для некоторого процесса P 0 1 верно утверждение P 1 - a P 0 1 (4.53) то должен существовать процесс P 0 2 , такой, что выполнены условия P 2 - a τ P 0 2 (4.54) и (4.50). 98 (4) Симметричное свойство: если (P 1 , P 2 ) ∈ µ, и для некоторого процесса P 0 2 верно утверждение P 2 - a P 0 2 (4.55) то должен существовать процесс P 0 1 , такой, что выполнены условия P 1 - a τ P 0 1 (4.56) и (4.50). Заметим, что мы не требуем, чтобы µ было отношением эк- вивалентности. Обозначим символом M τ совокупность всех бинарных отно- шений, которые обладают вышеприведёнными свойствами. Множество M τ непусто: оно содержит, например, диагональ- ное отношение, которое состоит из всех пар вида (P, P ), где P – произвольный процесс. Как и в случае сильной эквивалентности, встаёт естествен- ный вопрос о том, какое же из отношений, входящих в M τ , мож- но использовать для определения понятия наблюдаемой эквива- лентности. Так же, как и в случае сильной эквивалентности, мы предла- гаем следующий ответ на этот вопрос: мы будем считать P 1 и P 2 наблюдаемо эквивалентными в том и только в том случае, когда существует хотя бы одно отношение µ ∈ M τ , которое содержит пару (P 1 , P 2 ), т.е. искомое отношение наблюдаемой эквивалент- ности на множестве всех процессов мы определяем как объеди- нение всех отношений из M τ . Данное отношение обозначается символом ≈. Нетрудно доказать, что • ≈ ∈ M τ , • ≈ является отношением эквивалентности, т.к. – рефлексивность ≈ следует из того, что диагональное отношение принадлежит M τ , – симметричность ≈ следует из того, что если µ ∈ M τ , то µ −1 ∈ M τ 99 – транзитивность ≈ следует из того, что если µ 1 ∈ M τ и µ 2 ∈ M τ , то µ 1 ◦ µ 2 ∈ M τ Если процессы P 1 и P 2 наблюдаемо эквивалентны, то этот факт обозначается знакосочетанием P 1 ≈ P 2 Нетрудно доказать, что если процессы P 1 и P 2 сильно экви- валентны, то они наблюдаемо эквивалентны. 4.8.2 Логический критерий наблюдаемой экви- валентности Логический критерий наблюдаемой эквивалентности ана- логичен критерию из параграфа 4.4.1. В данном критерии ис- пользуется то же самое множество формул. Понятие значения формулы на процессе отличается от аналогичного понятия в па- раграфе 4.4.1 лишь для формул вида haiϕ: • значение формулы hτ iϕ на процессе P равно 1, если существует процесс P 0 : P - τ ∗ P 0 , P 0 (ϕ) = 1 0, в противном случае • значение формулы haiϕ (где a 6= τ ) в P равно 1, если существует процесс P 0 : P - a τ P 0 , P 0 (ϕ) = 1 0, в противном случае Для каждого процесса P мы будем обозначать знакосочета- нием T h τ (P ) совокупность всех формул, которые имеют на этом процессе значение 1 (относительно модифицированного опреде- ления понятия значения формулы на процессе). Теорема 13. 100 Пусть процессы P 1 и P 2 конечны. Тогда P 1 ≈ P 2 ⇔ T h τ (P 1 ) = T h τ (P 2 ) Как и в случае ∼, представляет интерес задача нахождения по двум заданным процессам P 1 и P 2 списка формул ϕ 1 , . . . , ϕ n как можно меньшего размера, таких, что P 1 ≈ P 2 тогда и только тогда, когда ∀ i = 1, . . . , n P 1 (ϕ i ) = P 2 (ϕ i ) Используя теорему 13, можно легко доказать, что для каждого процесса P P ≈ τ.P (4.57) Заметим, что, согласно (4.57), имеет место соотношение 0 ≈ τ. 0 однако соотношение 0 + a.0 ≈ τ. 0 + a.0 (где a 6= τ ) (4.58) неверно, в чём нетрудно убедиться при рассмотрении графового представления левой и правой частей в (4.58): ? a C C C C C CW τ a Формула, которая принимает разные значения на этих про- цессах, может иметь, например, такой вид: ¬hτ i¬hai> 101 Таким образом, отношение ≈ не является конгруэнцией, т.к. оно не сохраняет операцию +. Другой пример: если a, b ∈ Act \ {τ } и a 6= b, то a.0 + b.0 6≈ τ.a.0 + τ.b.0 хотя a.0 ≈ τ.a.0 и b.0 ≈ τ.b.0. Графовое представление этих процессов имеет вид A A A U a b A A A U ? ? τ τ a b Отсутствие наблюдаемой эквивалентности между этими про- цессами обосновывается формулой hτ i¬hai> 4.8.3 Критерий наблюдаемой эквивалентности, основанный на понятии наблюдаемого БМ Для отношения ≈ также имеет место аналог критерия, основан- ного на понятии БМ (теорема 2 из параграфа 4.4.2). Для его формулировки мы введём вспомогательные обозначения. Пусть P = (S, s 0 , R) – некоторый процесс, и s 1 , s 2 – пара его состояний. Тогда • знакосочетание s - τ ∗ s 0 означает, что – или s = s 0 , 102 – или существует последовательность состояний s 1 , . . . , s n (n ≥ 2) такая, что s 1 = s, s n = s 0 , и ∀ i = 1, . . . , n − 1 ( s i - τ s i+1 ) ∈ R • знакосочетание s - a τ s 0 (где a 6= τ ) означает, что существуют состояния s 1 и s 2 , такие, что s - τ ∗ s 1 , s 1 - a s 2 , s 2 - τ ∗ s 0 Теорема 14. Пусть заданы два процесса P i = (S i , s 0 i , R i ) (i = 1, 2) P 1 ≈ P 2 тогда и только тогда, когда существует отношение µ ⊆ S 1 × S 2 удовлетворяющее следующим условиям. 0. (s 0 1 , s 0 2 ) ∈ µ. 1. Для каждой пары (s 1 , s 2 ) ∈ µ и каждого перехода из R 1 вида s 1 - τ s 0 1 существует состояние s 0 2 ∈ S 2 , такое, что s 2 - τ ∗ s 0 2 и (s 0 1 , s 0 2 ) ∈ µ (4.59) 103 2. Для каждой пары (s 1 , s 2 ) ∈ µ и каждого перехода из R 2 вида s 2 - τ s 0 2 существует состояние s 0 1 ∈ S 1 , такое, что s 1 - τ ∗ s 0 1 и (4.59). 3. Для каждой пары (s 1 , s 2 ) ∈ µ и каждого перехода из R 1 вида s 1 - a s 0 1 (a 6= τ ) существует состояние s 0 2 ∈ S 2 , такое, что s 2 - a τ s 0 2 и (4.59). 4. Для каждой пары (s 1 , s 2 ) ∈ µ и каждого перехода из R 2 вида s 2 - a s 0 2 (a 6= τ ) существует состояние s 0 1 ∈ S 1 , такое, что s 1 - a τ s 0 1 и (4.59). Отношение µ, удовлетворяющее данным условиям, называется наблюдаемым БМ (НБМ) между P 1 и P 2 4.8.4 Алгебраические свойства наблюдаемой эк- вивалентности Теорема 15. Отношение наблюдаемой эквивалентности сохраняет все опе- рации на процессах, за исключением операции +, т.е. если P 1 ≈ P 2 , то • для каждого a ∈ Act a.P 1 ≈ a.P 2 104 • для каждого процесса P P 1 |P ≈ P 2 |P • для каждого L ⊆ N ames P 1 \ L ≈ P 2 \ L • для каждого переименования f P 1 [f ] ≈ P 2 [f ] Доказательство. Как было установлено в параграфе 4.8.3, соотношение P 1 ≈ P 2 эквивалентно тому, что существует НБМ µ между P 1 и P 2 Используя это µ, мы построим НБМ для обоснования каждого из вышеприведённых соотношений. • Пусть символы s 0 (1) и s 0 (2) обозначают начальные состояния a.P 1 и a.P 2 соответственно. Тогда отношение µ ∪ {(s 0 (1) , s 0 (2) )} является НБМ между a.P 1 и a.P 2 • Пусть символ S обозначает множество состояний процесса P . Тогда отношение {((s 1 , s), (s 2 , s)) | (s 1 , s 2 ) ∈ µ, q ∈ S} является НБМ между P 1 |P и P 2 |P . • Отношение µ является НБМ – между P 1 \ L и P 2 \ L, и – между P 1 [f ] и P 2 [f ]. 4.8.5 Распознавание наблюдаемой эквивалент- ности и минимизация процессов относи- тельно ≈ Для решения задач 1. распознавания для двух заданных конечных процессов, яв- ляются ли они наблюдаемо эквивалентными, и 105 2. построения по заданному конечному процессу P такого про- цесса P 0 , который имеет наименьшее число состояний среди всех процессов, наблюдаемо эквивалентных P могут быть построены теория и основанные на ней алгоритмы, которые аналогичны теории и алгоритмам, изложенным в пара- графах 4.6 и 4.7. Мы не будем детально излагать эту теорию, т.к. она почти дословно повторяет соответствующую теорию для случая ∼. В этой теории для произвольной пары процессов P i = (S i , s 0 i , R i ) (i = 1, 2) тоже определяется функция на отношениях из S 1 × S 2 , которая сопоставляет каждому отношению µ некоторое отношение µ 0 τ , такое, что µ удовлетворяет условиям 1, 2, 3, 4 из определения НБМ ⇔ µ ⊆ µ 0 τ В частности, µ – НБМ между P 1 и P 2 ⇔ ( (s 0 1 , s 0 2 ) ∈ µ µ ⊆ µ 0 τ Обозначим символом µ τ (P 1 , P 2 ) объединение всех отношений из совокупности {µ ⊆ S 1 × S 2 | µ ⊆ µ 0 τ } (4.60) Данное отношение является наибольшим элементом совокуп- ности (4.60), и обладает свойством P 1 ≈ P 2 ⇔ (s 0 1 , s 0 2 ) ∈ µ τ (P 1 , P 2 ) Из определения отношения µ τ (P 1 , P 2 ) вытекает, что оно со- стоит из всех пар (s 1 , s 2 ) ∈ S 1 × S 2 , таких, что P 1 (s 1 ) ≈ P 2 (s 2 ) Отношение µ τ (P 1 , P 2 ) можно рассматривать как ещё одну ме- ру близости между P 1 и P 2 При построении полиномиального алгоритма вычисления от- ношения µ τ (P 1 , P 2 ), аналогичного алгоритму из параграфа 4.6.2, 106 следует учитывать следующее соображение. Всякий раз, когда для заданной пары s, s 0 состояний некоторого процесса P требу- ется проверить условие s - τ ∗ s 0 достаточно анализировать последовательности переходов вида s - τ s 1 - τ s 2 - τ длина которых не превосходит числа состояний процесса P . 4.8.6 Другие критерии эквивалентности процес- сов Доказать сильную или наблюдаемую эквивалентность процессов P 1 и P 2 можно также с помощью излагаемых ниже критериев. В некоторых случаях использование этих критериев гораздо про- ще всех других способов доказательства соответствующей экви- валентности P 1 и P 2 Бинарное отношение µ на множестве процессов называется • БМ (mod ∼), если µ ⊆ (∼ µ ∼) 0 • НБМ (mod ∼), если µ ⊆ (∼ µ ∼) 0 τ • НБМ (mod ≈), если µ ⊆ (≈ µ ≈) 0 τ Нетрудно доказать, что • если µ – БМ (mod ∼), то µ ⊆ ∼, и • если µ – НБМ (mod ∼ или mod ≈), то µ ⊆ ≈. Таким образом, для доказательства P 1 ∼ P 2 или P 1 ≈ P 2 доста- точно найти подходящее • БМ (mod ∼), или • НБМ (mod ∼ или mod ≈) соответственно, такое, что (P 1 , P 2 ) ∈ µ 107 4.9 Наблюдаемая конгруэнция 4.9.1 Мотивировка понятия наблюдаемой кон- груэнции Понятие эквивалентности процессов может быть определено неод- нозначно. В предыдущих параграфах уже были рассмотрены различные виды эквивалентности процессов, каждый из кото- рых отражал определённую точку зрения на то, какие виды по- ведения следует считать одинаковыми. В добавление к этим по- нятиям эквивалентности процессов, можно ещё определить, на- пример, такие эквивалентности, которые • учитывают длительность исполнения действий, т.е., в част- ности, одно из условий эквивалентности процессов P 1 и P 2 может иметь следующий вид: – если один из этих процессов P i может в течение неко- торого промежутка времени незаметно превратиться в процесс P 0 i , – то и другой процесс P j (j ∈ {1, 2} \ {i}) тоже должен обладать способностью в течение примерно такого же промежутка времени незаметно превратиться в про- цесс P 0 j , который эквивалентен P 0 i (понятие “примерно такого же промежутка времени” может уточняться различным образом) • или учитывают свойство справедливости (fairness) в по- ведении процессов, т.е. не позволяют рассматривать как эк- вивалентные такие два процесса, – один из которых обладает свойством справедливости, – а другой - не обладает где одно из определений свойства справедливости имеет следующий вид: процесс называется справедливым, если не существует бесконечной последовательности переходов этого процесса вида s 0 - τ s 1 - τ s 2 - τ 108 такой, что состояние s 0 достижимо, и для каждого i ≥ 0 Act(s i ) \ {τ } 6= ∅ отметим, что отношение наблюдаемой эквивалентности не учитывает свойство справедливости: существуют два про- цесса P 1 и P 2 , такие, что P 1 ≈ P 2 , но P 1 обладает свойством справедливости, а P 2 не обладает этим свойством, напри- мер – в качестве P 1 можно взять процесс a.0, где a 6= τ , – а в качестве P 2 – процесс a.0 | τ ∗ , где процесс τ ∗ имеет одно состояние и один переход с меткой τ • и т.д. Решение о том, какое именно из понятий эквивалентности между процессами следует выбрать в конкретной ситуации, су- щественно зависит от целей, для достижения которых предна- значено данное понятие. В настоящем параграфе мы определяем ещё один вид экви- валентности процессов, называемый наблюдаемой конгруэн- цией, Данная эквивалентность обозначается символом + ≈. Мы определяем эту эквивалентность, исходя из следующих условий, которым она должна удовлетворять. 1. Процессы, находящиеся в отношении + ≈, должны быть на- блюдаемо эквивалентными. 2. Пусть • процесс P построен в виде композиции процессов P 1 , . . . , P n в которой используются операции a., +, | , \L, [f ] (4.61) 109 • и мы решили заменить одну из частей этой компози- ции (например, P i ), на другой процесс P 0 i , который мы считаем – эквивалентным компоненте P i , но – более предпочтительным для нас по некоторым причинам, чем P i (например, P 0 i имеет меньшую сложность, чем P i ). Мы хотели бы, чтобы процесс, получаемый из P в результа- те такой замены, был бы эквивалентен исходному процессу P . Нетрудно доказать, что эквивалентность µ на множестве про- цессов удовлетворяет сформулированным выше условиям тогда и только тогда, когда µ ⊆ ≈ µ является конгруэнцией относительно операций (4.61) (4.62) Условия (4.62) определяют искомую эквивалентность неоднознач- но. Например, данным условиям удовлетворяют • тождественное отношение (состоящее из пар вида (P, P )), и • сильная эквивалентность (∼). Ниже мы докажем, что среди всех эквивалентностей, удо- влетворяющих условиям (4.62), существует наибольшая (отно- сительно включения). Вполне естественно считать именно эту эквивалентность искомой эквивалентностью. 4.9.2 Определение понятия наблюдаемой кон- груэнции Для определения понятия наблюдаемой конгруэнции мы введём вспомогательное обозначение. Пусть P и P 0 – некоторые процессы. Знакосочетание P - τ + P 0 110 означает, что существует последовательность процессов P 1 , . . . , P n (n ≥ 2) таких, что • P 1 = P, P n = P 0 • для каждого i = 1, . . . , n − 1 P i - τ P i+1 Мы будем говорить, что процессы P 1 и P 2 находятся в от- ношении наблюдаемой конгруэнции, и обозначать этот факт знакосочетанием P 1 + ≈ P 2 если выполнены следующие условия. (0) P 1 ≈ P 2 (1) Если для некоторого процесса P 0 1 верно утверждение P 1 - τ P 0 1 (4.63) то существует процесс P 0 2 , такой, что P 2 - τ + P 0 2 (4.64) и P 0 1 ≈ P 0 2 (4.65) (2) Симметричное условие: если для некоторого процесса P 0 2 верно утверждение P 2 - τ P 0 2 (4.66) то существует процесс P 0 1 , такой, что P 1 - τ + P 0 1 (4.67) и (4.65). Нетрудно доказать, что наблюдаемая конгруэнция является отношением эквивалентности. 111 4.9.3 Логический критерий наблюдаемой кон- груэнтности Логический критерий наблюдаемой конгруэнтности двух процессов получается небольшой модификацией логического кри- терия наблюдаемой эквивалентности, из параграфа 4.8.2. Множество формул F m + , используемых в данном критерии, является расширением множества формул F m из параграфа 4.4.2 путём использования дополнительной модальной связки hτ + i: • каждая формула из F m принадлежит F m + , и • для каждой формулы ϕ ∈ F m знакосочетание hτ + iϕ является формулой из множества F m + Для каждой формулы ϕ ∈ F m + её значение на процессе P опре- деляется следующим образом. • Если ϕ ∈ F m, то её значение в P определяется так же, как в параграфе 4.8.2. • Если ϕ = hτ + iψ, где ψ ∈ F m, то P (ϕ) def = 1, если существует процесс P 0 : P - τ + P 0 , P 0 (ψ) = 1 0, в противном случае Для каждого процесса P мы будем обозначать знакосочетанием T h + τ (P ) совокупность всех формул из F m + , которые имеют на этом процессе значение 1. Теорема 16. Пусть процессы P 1 и P 2 конечны. Тогда P 1 + ≈ P 2 ⇔ T h + τ (P 1 ) = T h + τ (P 2 ) Как и в случаях ∼ и ≈, представляет интерес задача нахож- дения по двум заданным процессам P 1 и P 2 списка формул ϕ 1 , . . . , ϕ n ∈ F m + 112 как можно меньшего размера, таких, что P 1 + ≈ P 2 тогда и только тогда, когда ∀ i = 1, . . . , n P 1 (ϕ i ) = P 2 (ϕ i ) 4.9.4 Критерий наблюдаемой конгруэнтности, основанный на понятии НБМ Введём вспомогательное обозначение. Пусть • P – процесс вида (S, s 0 , R), и • s 1 , s 2 – пара состояний из S. Тогда знакосочетание s - τ + s 0 означает, что существует последовательность состояний s 1 , . . . , s n (n ≥ 2) такая, что s 1 = s, s n = s 0 , и для каждого i = 1, . . . , n − 1 ( s i - τ s i+1 ) ∈ R Теорема 17. Пусть заданы два процесса P i = (S i , s 0 i , R i ) (i = 1, 2) P 1 + ≈ P 2 тогда и только тогда, когда существует отношение µ ⊆ S 1 × S 2 удовлетворяющее следующим условиям. 0. µ – НБМ между P 1 и P 2 (понятие НБМ изложено в параграфе 4.8.3). 113 1. Для каждого перехода из R 1 вида s 0 1 - τ s 0 1 существует состояние s 0 2 ∈ S 2 , такое, что s 0 2 - τ + s 0 2 и (s 0 1 , s 0 2 ) ∈ µ (4.68) 2. Для каждого перехода из R 2 вида s 0 2 - τ s 0 2 существует состояние s 0 1 ∈ S 1 , такое, что s 0 1 - τ + s 0 1 и (4.68). Ниже знакосочетание НБМ + является сокращённой записью фразы “НБМ, удовлетворяющее условиям 1 и 2 теоремы 17”. 4.9.5 Алгебраические свойства наблюдаемой кон- груэнции Теорема 18. Наблюдаемая конгруэнция действительно является конгру- энцией, т.е. если P 1 + ≈ P 2 , то • для каждого a ∈ Act a.P 1 + ≈ a.P 2 • для каждого процесса P P 1 + P + ≈ P 2 + P • для каждого процесса P P 1 |P + ≈ P 2 |P • для каждого L ⊆ N ames P 1 \ L + ≈ P 2 \ L 114 • для каждого переименования f P 1 [f ] + ≈ P 2 [f ] Доказательство. Как было установлено в параграфе 4.9.4, соотношение P 1 + ≈ P 2 эквивалентно тому, что существует НБМ + µ между P 1 и P 2 . Ис- пользуя это µ, для обоснования каждого из вышеприведённых соотношений мы построим соответствующее НБМ + • Пусть символы s 0 (1) и s 0 (2) обозначают начальные состояния a.P 1 и a.P 2 соответственно. Тогда отношение {(s 0 (1) , s 0 (2) )} ∪ µ является НБМ + между a.P 1 и a.P 2 • Пусть – символы s 0 (1) и s 0 (2) обозначают начальные состояния P 1 + P и P 2 + P соответственно, и – символ S обозначает множество состояний процесса P . Тогда отношение {(s 0 (1) , s 0 (2) )} ∪ µ ∪ Id S является НБМ + между P 1 + P и P 2 + P • Пусть символ S обозначает множество состояний процесса P . Тогда отношение {((s 1 , s), (s 2 , s)) | (s 1 , s 2 ) ∈ µ, q ∈ S} является НБМ + между P 1 |P и P 2 |P • Отношение µ является НБМ + – между P 1 \ L и P 2 \ L, и – между P 1 [f ] и P 2 [f ]. 115 Теорема 19. Для любых процессов P 1 и P 2 P 1 ≈ P 2 ⇔ P 1 + ≈ P 2 или P 1 + ≈ τ.P 2 или τ.P 1 + ≈ P 2 Доказательство. Импликация “⇐” следует из включения + ≈ ⊆ ≈, и того, что для любого процесса P P ≈ τ.P (4.69) Докажем импликацию “⇒”. Предположим, что P 1 ≈ P 2 (4.70) и неверно, что P 1 + ≈ P 2 (4.71) (4.71) может иметь место, например, в следующем случае: существует процесс P 0 1 , такой, что P 1 - τ P 0 1 (4.72) и не существует процесса P 0 2 ≈ P 0 1 , такого, что P 2 - τ + P 0 2 (4.73) Докажем, что в этом случае имеет место соотношение P 1 + ≈ τ.P 2 Согласно определению наблюдаемой конгруэнции, надо доказать, что выполнены следующие условия. (0) P 1 ≈ τ.P 2 Это условие следует из (4.70) и (4.69). (1) Если для некоторого процесса P 0 1 верно утверждение P 1 - τ P 0 1 (4.74) 116 то для некоторого процесса P 0 2 ≈ P 0 1 верно утверждение τ.P 2 - τ + P 0 2 (4.75) Из (4.70), (4.74), и из определения наблюдаемой эквива- лентности следует, что для некоторого процесса P 0 2 ≈ P 0 1 верно утверждение P 2 - τ ∗ P 0 2 (4.76) (4.75) следует из τ.P 2 - τ P 2 и (4.76). (2) Если для некоторого процесса P 0 2 верно утверждение τ.P 2 - τ P 0 2 (4.77) то для некоторого процесса P 0 1 ≈ P 0 2 верно утверждение P 1 - τ + P 0 1 Из определения операции префиксного действия и из (4.77) следует, что P 0 2 = P 2 Таким образом, надо доказать, что для некоторого процесса P 0 1 ≈ P 2 верно утверждение P 1 - τ + P 0 1 (4.78) Пусть P 0 1 есть в точности тот процесс, который упоминается в предположении (4.72). Из предположения (4.70) следует, что существует процесс P 0 2 ≈ P 0 1 , такой, что P 2 - τ ∗ P 0 2 (4.79) Сопоставляя (4.79) и (4.73), получаем, P 0 2 = P 2 , т.е. мы до- казали (4.78). Другая причина, по которой может иметь место (4.71) заключа- ется в том, что • существует процесс P 0 2 , такой, что P 2 - τ P 0 2 , и 117 • не существует процесса P 0 1 ≈ P 0 2 , такого, что P 1 - τ + P 0 1 В этом случае аналогичными рассуждениями можно доказать, что имеет место соотношение τ.P 1 + ≈ P 2 Теорема 20. Отношение + ≈ совпадает с отношением {(P 1 , P 2 ) | ∀ P P 1 + P ≈ P 2 + P } (4.80) Доказательство. Включение + ≈ ⊆ (4.80) следует из того, что • + ≈ – конгруэнция (т.е., в частности, + ≈ сохраняет операцию +), и • + ≈ ⊆ ≈. Докажем включение (4.80) ⊆ + ≈. Пусть (P 1 , P 2 ) ∈ (4.80). Поскольку для каждого процесса P имеет место соотношение P 1 + P ≈ P 2 + P (4.81) то, полагая в (4.81) P def = 0, имеем: P 1 + 0 ≈ P 2 + 0 (4.82) Поскольку • для любого процесса P имеет место свойство P + 0 ∼ P • и, кроме того, ∼ ⊆ ≈ 118 то из (4.82) следует, что P 1 ≈ P 2 (4.83) Если неверно, что P 1 + ≈ P 2 , то из (4.83) по теореме 19 следует, что • либо P 1 + ≈ τ.P 2 • либо τ.P 1 + ≈ P 2 Рассмотрим, например, случай P 1 + ≈ τ.P 2 (4.84) (другой случай разбирается аналогично). Так как + ≈ – конгруэнция, то из (4.84) следует, что для любого процесса P P 1 + P + ≈ τ.P 2 + P (4.85) Из (4.81), (4.85) и включения + ≈ ⊆ ≈ следует, что для любого процесса P P 2 + P ≈ τ.P 2 + P (4.86) Докажем, что имеет место соотношение P 2 + ≈ τ.P 2 (4.87) (4.87) равносильно существованию процесса P 0 2 ≈ P 2 , такой, что P 2 - τ + P 0 2 (4.88) Выберем произвольное действие b ∈ Act \ {τ }, которое не входит в P 2 (здесь мы используем предположение из параграфа 2.3 о том, что множество N ames, а значит, и множество Act, является бесконечным). Соотношение (4.86) должно быть верно в случае, когда P име- ет вид b.0, т.е. должно быть верно соотношение P 2 + b.0 ≈ τ.P 2 + b.0 (4.89) 119 Так как имеет место соотношение τ.P 2 + b.0 - τ P 2 то из (4.89) по определению отношения ≈ следует, что для неко- торого процесса P 0 2 ≈ P 2 имеет место соотношение P 2 + b.0 - τ ∗ P 0 2 (4.90) Случай P 2 + b.0 = P 0 2 невозможен, так как процесс в левой части этого равенства содержит действие, которое не содержит процесс в правой части этого равенства. Согласно (4.90), отсюда следует соотношение P 2 + b.0 - τ + P 0 2 (4.91) Из определения операции + следует, что (4.91) возможно в том и только в том случае, когда имеет место (4.88). Таким образом, мы доказали, что для некоторого процесса P 0 2 ≈ P 2 имеет место (4.88), т.е. мы доказали (4.87). Из (4.84) и (4.87) следует, что P 1 + ≈ P 2 Теорема 21. + ≈ является наибольшей конгруэнцией, содержащейся в ≈, т.е. для каждой конгруэнции ν на множестве всех процессов имеет место импликация: ν ⊆ ≈ ⇒ ν ⊆ + ≈ Доказательство. Докажем, что если (P 1 , P 2 ) ∈ ν, то P 1 + ≈ P 2 Пусть (P 1 , P 2 ) ∈ ν. Так как ν – конгруэнция, то для каждого процесса P (P 1 + P, P 2 + P ) ∈ ν (4.92) Если ν ⊆ ≈, то из (4.92) следует, что для каждого процесса P P 1 + P ≈ P 2 + P (4.93) Согласно теореме 20, из (4.93) следует, что P 1 + ≈ P 2 Теорема 22. 120 Для отношений ∼, ≈ и + ≈ верны включения ∼ ⊆ + ≈ ⊆ ≈ (4.94) Доказательство. Включение + ≈ ⊆ ≈ верно по определению + ≈. Включение ∼ ⊆ + ≈ следует • из включения ∼ ⊆ ≈, и • из того, что если P 1 ∼ P 2 , то данная пара удовлетворяет условиям, изложенным в определении отношения + ≈. Отметим, что оба включения в (4.94) – собственные: • a.τ.0 6∼ a.0, но a.τ.0 + ≈ a.0 • τ.0 + ≈ / 0, но τ.0 ≈ 0 Теорема 23. 1. Если P 1 ≈ P 2 , то для каждого a ∈ Act a.P 1 + ≈ a.P 2 В частности, для каждого процесса P a.τ.P + ≈ a.P (4.95) 2. Для любого процесса P P + τ.P + ≈ τ.P (4.96) 3. Для любых процессов P 1 и P 2 и любого a ∈ Act a.(P 1 + τ.P 2 ) + a.P 2 + ≈ a.(P 1 + τ.P 2 ) (4.97) 4. Для любых процессов P 1 и P 2 P 1 + τ.(P 1 + P 2 ) + ≈ τ.(P 1 + P 2 ) (4.98) 121 Доказательство. Для каждого из доказываемых соотношений мы построим НМБ + между его левой и правой частями. 1. Как было установлено в теореме 14 из параграфа 4.8.3, соотношение P 1 ≈ P 2 эквивалентно тому, что существует НБМ µ между P 1 и P 2 Пусть символы s 0 (1) и s 0 (2) обозначают начальные состояния a.P 1 и a.P 2 соответственно. Тогда отношение {(s 0 (1) , s 0 (2) )} ∪ µ является НБМ + между a.P 1 и a.P 2 (4.95) следует • из вышедоказанного утверждения, и • из соотношения τ.P ≈ P , которое верно согласно (4.57). 2. Пусть P имеет вид P = (S, s 0 , R) Обозначим символами S (1) и S (2) дубликаты множества S в процессах P и τ.P соответственно, входящих в левую часть соотношения (4.96). Элементы этих дубликатов мы будем обозначать символами s (1) и s (2) соответственно, где s – про- извольный элемент множества S. Пусть символы s 0 l и s 0 r обозначают начальные состояния процессов в левой и правой частях соотношения (4.96) со- ответственно. Тогда отношение {(s 0 l , s 0 r )} ∪ {(s (i) , s) | s ∈ S, i = 1, 2} является НБМ + между левой и правой частями соотноше- ния (4.96). 3. Пусть P i = (S i , s 0 i , R i ) (i = 1, 2). Мы можем считать, что S 1 ∩ S 2 = ∅. Обозначим 122 • символом s 0 τ начальное состояние процесса P 1 + τ.P 2 (4.99) • символом s 0 – начальное состояние процесса a.(P 1 + τ.P 2 ) (4.100) Заметим, что (4.100) совпадает с правой частью (4.97). Левая часть (4.97) сильно эквивалентна процессу P 0 , кото- рый получается из (4.100) добавлением перехода s 0 - a s 0 2 это легко увидеть при рассмотрении графового представ- ления процесса P 0 , которое имеет вид s 0 s 0 τ s 0 2 s 0 1 s 1 ' & $ % ' & $ % P 1 P 2 A A A A A A A A U @ @ @ @ R ? ? a a τ Нетрудно доказать, что процесс P 0 наблюдаемо конгруэн- тен процессу (4.100). Множества состояний этих процессов можно рассматривать как дубликаты S (1) и S (2) одного и того же множества S, и НБМ + между P 0 и (4.100) имеет вид {(s (1) , s (2) ) | s ∈ S} (4.101) Поскольку 123 • по теореме 22, имеет место включение ∼ ⊆ + ≈, и • (4.100) совпадает с правой частью (4.97), то мы доказали наблюдаемую конгруэнтность левой и пра- вой частей соотношения (4.97). 4. Рассуждения в данном случае аналогичны рассуждениям в предыдущем случае. Мы не будем излагать их детально, отметим лишь, что • левая часть соотношения (4.98) находится в отноше- нии сильной эквивалентности с процессом P 0 , графо- вое представление которой имеет вид s 0 s 0 12 s 0 2 s 0 1 s 1 s 2 ' & $ % ' & $ % P 1 P 2 A A A A A A A A A U ? ? ? τ где – s 0 1 и s 0 2 – начальные состояния процессов P 1 и P 2 , – s 0 12 – начальное состояние процесса P 1 + P 2 • правая часть соотношения (4.98), которую мы обозна- чим символом P 00 , получается из P 0 удалением перехо- дов вида s 0 - s 1 124 Нетрудно доказать, что P 0 + ≈ P 00 . Множества состояний этих процессов можно рассматривать как дубликаты S (1) и S (2) одного и того же множества S, и НБМ + между P 0 и P 00 имеет вид (4.101). 4.9.6 Распознавание наблюдаемой конгруэнтно- сти Для решения задачи распознавания для двух заданных конеч- ных процессов, являются ли они наблюдаемо конгруэнтными, можно использовать следующую теорему. Теорема 24. Пусть P 1 и P 2 - конечные процессы. Соотношение P 1 + ≈ P 2 имеет место тогда и только тогда, когда ( (s 0 1 , s 0 2 ) ∈ µ τ (P 1 , P 2 ) µ τ (P 1 , P 2 ) − НБМ + 4.9.7 Минимизация процессов относительно на- блюдаемой конгруэнции Для решения задачи минимизации конечных процессов относи- тельно наблюдаемой конгруэнции можно использовать следую- щие теоремы. Теорема 25. Пусть P = (S, s 0 , R) - произвольный процесс. Обозначим символом P ≈ фактор-процесс процесса P по эк- вивалентности µ τ (P, P ), т.е. процесс, компоненты которого име- ют следующий вид. • Множество состояний процесса P ≈ представляет собой со- вокупность классов эквивалентности множества S по отно- шению µ τ (P, P ). 125 • Начальным состоянием является класс [s 0 ]. • Переходы процесса P ≈ имеют вид [s 1 ] - a [s 2 ] где s 1 - a s 2 – произвольный переход из R. Тогда P + ≈(P ≈ ). Теорема 26. Пусть процесс P 0 получается из процесса P путём удаления недостижимых состояний. Тогда P 0 ≈ имеет наименьшее число со- стояний среди всех процессов, которые наблюдаемо конгруэнтны P. 126 Глава 5 Рекурсивные определения процессов В некоторых случаях процесс удобнее задавать не явным описа- нием множеств его состояний и переходов, а при помощи рекур- сивного определения. 5.1 Процессные выражения Для того, чтобы сформулировать понятие рекурсивного опреде- ления процессов, мы введём понятие процессного выражения. Множество P Expr процессных выражений (ПВ) опреде- ляется индуктивно, т.е. • указываются элементарные ПВ, и • описываются правила построения новых ПВ из уже имею- щихся. Каждое из правил построения ПВ имеет своё название, кото- рое указывается жирным шрифтом перед описанием этого пра- вила. процессные константы: Мы будем предполагать, что задано счётное множество про- цессных констант, причём каждой процессной константе 127 сопоставлен некоторый процесс, называемый значением этой константы. Существует процессная константа, значением которой яв- ляется пустой процесс 0, эта константа обозначается тем же символом 0. Каждая процессная константа является ПВ. процессные имена: Мы будем предполагать, что задано счётное множество про- цессных имён. Каждое процессное имя является ПВ. префиксное действие: Для каждого a ∈ Act и каждого ПВ P знакосочетание a.P является ПВ. выбор: Для любых ПВ P 1 , P 2 знакосочетание P 1 + P 2 является ПВ. параллельная композиция: Для любых ПВ P 1 , P 2 знакосочетание P 1 | P 2 является ПВ. ограничение: Для каждого подмножества L ⊆ N ames и каждого ПВ P знакосочетание P \ L является ПВ. переименование: Для каждого переименования f и каждого ПВ P знакосо- четание P [f ] является ПВ. 5.2 Понятие рекурсивного определения процессов Рекурсивным определением (РО) процессов называется список формальных равенств вида A 1 = P 1 A n = P n (5.1) 128 где • A 1 , . . . , A n – различные процессные имена, и • P 1 , . . . , P n – ПВ, удовлетворяющие следующему условию: для каждого i = 1, . . . , n каждое процессное имя, входящее в P i , совпадает с одним из имён A 1 , . . . , A n Мы будем предполагать, что каждому процессному имени со- ответствует единственное РО, в котором это имя является левой частью одного из равенств. В параграфе 5.5 мы определим соответствие, которое сопо- ставляет каждому ПВ P некоторый процесс [[P ]]. Для определе- ния этого соответствия мы сначала изложим • понятие вложения процессов, и • понятие предела последовательности вложенных процес- сов. а также утверждения, связанные с этими понятиями. 5.3 Вложение процессов Пусть заданы два процесса P i = (S i , s 0 i , R i ) (i = 1, 2) и f – инъективное отображение из S 1 в S 2 Мы будем говорить, что f является вложением P 1 в P 2 , если • f (s 0 1 ) = s 0 2 , и • для любых s 0 , s 00 ∈ S 1 и любого a ∈ Act (s 0 a → s 00 ) ∈ R 1 ⇔ (f (s 0 ) a → f (s 00 )) ∈ R 2 Для каждой пары процессов P 1 , P 2 знакосочетание P 1 ,→ P 2 является сокращённой записью утверждения о том, что суще- ствует вложение P 1 в P 2 Теорема 27. Пусть P 1 ,→ P 2 . Тогда 129 • a.P 1 ,→ a.P 2 • P 1 + P ,→ P 2 + P • P 1 | P ,→ P 2 | P • P 1 \ L ,→ P 2 \ L, и • P 1 [f ] ,→ P 2 [f ]. Ниже мы рассматриваем выражения, построенные из процес- сов, и символов операций над процессами (a., +, | , \L, [f ]). По- нятие такого выражения отличается от понятия ПВ, и мы назы- ваем такие выражения выражениями над процессами. Для каждого выражения над процессами определён процесс, являю- щийся значением этого выражения. В нижеследующих рассуж- дениях мы будем обозначать выражение над процессами и его значение одним и тем же символом. Теорема 28. Пусть • P – выражение над процессами, в которое входят процессы P 1 , . . . , P n • для каждого i = 1, . . . , n P i ,→ P 0 i , и • P 0 – выражение, получаемое из P заменой для каждого i = 1, . . . , n каждого вхождения процесса P i на соответ- ствующий процесс P 0 i Тогда P ,→ P 0 Доказательство. Данная теорема доказывается индукцией по структуре выра- жения P : мы докажем, что для каждого подвыражения Q выра- жения P верно утверждение Q ,→ Q 0 (5.2) где Q 0 – подвыражение выражения P 0 , которое соответствует подвыражению Q . 130 базис индукции: Если Q = P i , то Q 0 = P 0 i , и (5.2) верно по предположению. индуктивный переход: Из теоремы 27 следует, что для каждого подвыражения Q выражения P имеет место импликация: если для каждого собственного подвыражения Q 1 выражения Q (т.е. Q 1 6= Q) Q 1 ,→ Q 0 1 то верно (5.2). Таким образом, (5.2) верно для каждого подвыражения Q выра- жения P . В частности, (5.2) верно для P . 5.4 Предел последовательности вложен- ных процессов Пусть задана последовательность процессов {P k | k ≥ 0} (5.3) такая, что ∀k ≥ 0 P k ,→ P k+1 (5.4) Последовательность процессов (5.3), удовлетвряющая условию (5.4), называется последовательностью вложенных процес- сов. Определим процесс P , называемый пределом последователь- ности (5.3). Пусть процессы P k (k ≥ 0) имеют вид P k = (S k , s 0 k , R k ) Мы можем считать, что все множества S k (k ≥ 0) попарно не пересекаются. Из (5.4) следует, что для каждого k ≥ 0 существует инъек- тивное отображение f k : S k → S k+1 такое, что 131 • f k (s 0 k ) = s 0 k+1 , и • для любых s 0 , s 00 ∈ S k и любого a ∈ Act (s 0 a → s 00 ) ∈ R k ⇔ (f k (s 0 ) a → f k (s 00 )) ∈ R k+1 Обозначим • символом S объединение S k≥0 S k , и • символом ρ – минимальную эквивалентность на S, облада- ющую следующим свойством: ∀ k ≥ 0, ∀s ∈ S k (s, f k (s)) ∈ ρ Компоненты искомого процесса P имеют следующий вид. 1. Состояниями процесса P являются классы разбиения мно- жества S по эквивалентности ρ. 2. Начальным состоянием процесса P является класс, содер- жащий s 0 0 3. Переходы процесса P имеют вид [s 0 ] - a [s 00 ] где ( s 0 - a s 00 ) ∈ R k для некоторого k ≥ 0. Определённый выше предел последовательности (5.3) мы будем обозначать знакосочетанием lim k→∞ P k Из определения предела последовательности (5.3) непосред- ственно следует, что для каждого k ≥ 0 P k ,→ lim k→∞ P k Теорема 29. Пусть заданы последовательности вложенных процессов {P k | k ≥ 0} и {Q k | k ≥ 0} Тогда 132 • lim k→∞ (a.P k ) = a.( lim k→∞ P k ) • lim k→∞ (P k + Q k ) = ( lim k→∞ P k ) + ( lim k→∞ Q k ) • lim k→∞ (P k | Q k ) = ( lim k→∞ P k ) | ( lim k→∞ Q k ) • lim k→∞ (P k \ L) = ( lim k→∞ P k ) \ L • lim k→∞ (P k [f ]) = ( lim k→∞ P k )[f ] Ниже мы будем использовать следующее обозначение: если • P – ПВ, в которое входят процессные имена A 1 , . . ., A n , и • P 1 , . . . , P n – некоторые процессы то знакосочетание P (P 1 /A 1 , . . . , P n /A n ) обозначает выражение над процессами (а также его значение), получаемое из P заменой для каждого i = 1, . . . , n каждого вхож- дения процессного имени A i на соответствующий процесс P i Теорема 30. Пусть заданы • ПВ P , в которое входят процессные имена A 1 , . . ., A n , и • последовательности вложенных процессов {P (k) i | k ≥ 0} (i = 1, . . . , n) Тогда P (( lim k→∞ P (k) 1 )/A 1 , . . . , ( lim k→∞ P (k) n )/A n ) = = lim k→∞ P (P (k) 1 /A 1 , . . . , P (k) n /A n ) Доказательство. Данная теорема доказывается индукцией по структуре ПВ P , с использованием теоремы 29. 133 5.5 Процессы, определяемые процессны- ми выражениями В этом параграфе мы излагаем правило, которое сопоставляет каждому ПВ P процесс [[P ]], определяемый этим ПВ. Процессы, определяемые процессными константами, являют- ся значениями этих констант. Процессы, определяемые ПВ вида a.P, P 1 + P 2 , P 1 | P 2 , P \ L, P [f ] являются результатами применения соответствующих операций к процессам определяемым ПВ P , P 1 и P 2 , т.е. [[a.P ]] def = a.[[P ]] [[P 1 + P 2 ]] def = [[P 1 ]] + [[P 2 ]] [[P 1 | P 2 ]] def = [[P 1 ]] | [[P 2 ]] [[P \ L]] def = [[P ]] \ L [[P [f ] ]] def = [[P ]] [f ] Опишем теперь правило, сопоставляющее процессы процесс- ным именам. Пусть задано РО вида (5.1). Определим последовательность списков процессов {(P (k) 1 , . . . , P (k) n ) | k ≥ 0} (5.5) следующим образом: • P (0) 1 def = 0, . . . , P (0) n def = 0 • если процессы P (k) 1 , . . ., P (k) n уже определены, то для каж- дого i = 1, . . . , n P (k+1) i def = P i (P (k) 1 /A 1 , . . . , P (k) n /A n ) Докажем, что для каждого k ≥ 0 и для каждого i = 1, . . . , n P (k) i ,→ P (k+1) i (5.6) Доказательство будем вести индукцией по k. 134 базис индукции: Если k = 0, то P (0) i по определению совпадает с процессом 0, который можно вложить в любой процесс. индуктивный переход: Пусть для каждого i = 1, . . . , n P (k−1) i ,→ P (k) i По определению процессов из совокупности (5.5), имеют место соотношения P (k) i = P i (P (k−1) 1 /A 1 , . . . , P (k−1) n /A n ) P (k+1) i = P i (P (k) 1 /A 1 , . . . , P (k) n /A n ) Соотношение P (k) i ,→ P (k+1) i следует из теоремы 28. Определим для каждого i = 1, . . . , n процесс [[A i ]] как предел [[A i ]] def = lim k→∞ P (k) i Из теоремы 30 следует, что для каждого i = 1, . . . , n верна цепочка равенств P i ([[A 1 ]]/A 1 , . . . , [[A n ]]/A n ) = = P i (( lim k→∞ P (k) 1 )/A 1 , . . . , ( lim k→∞ P (k) n )/A n ) = = lim k→∞ P i (P (k) 1 /A 1 , . . . , P (k) n /A n ) = = lim k→∞ (P (k+1) i ) = [[A i ]] т.е. список процессов [[A 1 ]], . . . , [[A n ]] является решением системы уравнений, соответствющей РО (5.1) (переменными в этой системе уравнений являются процессные имена). 5.6 Эквивалентность РО Пусть заданы два РО вида A (1) 1 = P (1) 1 A (1) n = P (1) n и A (2) 1 = P (2) 1 A (2) n = P (2) n (5.7) 135 Для каждого списка процессов Q 1 , . . ., Q n мы будем обозначать выражение над процессами (и его значение) P (j) i (Q 1 /A (j) 1 , . . . , Q n /A (j) n ) (i = 1, . . . , n; j = 1, 2) сокращённо в виде знакосочетания P (j) i (Q 1 , . . . , Q n ) Пусть задана некоторая эквивалентность µ на множестве всех процессов. Мы будем говорить, что РО (5.7) являются эквивалентны- ми относительно µ, если для • каждого списка процессов Q 1 , . . ., Q n , и • каждого i = 1, . . . , n имеет место соотношение P (1) i (Q 1 , . . . , Q n ) , P (2) i (Q 1 , . . . , Q n ) ∈ µ Теорема 31. Пусть заданы • два РО вида (5.7), и • конгруэнция µ на множестве процессов. Если РО (5.7) эквивалентны относительно µ, то процессы, опре- деляемые этими РО, т.е. {[[A (1) i ]] | i = 1, . . . , n} и {[[A (2) i ]] | i = 1, . . . , n} тоже эквивалентны относительно µ, т.е. для каждого i = 1, . . . , n имеет место соотношение [[A (1) i ]] , [[A (2) i ]] ∈ µ 136 5.7 Переходы на P Expr Существует другой способ определения соответствия между ПВ и процессами. Данный способ связан с определением множества переходов R на совокупности P Expr всех ПВ. Каждый переход из R представляет собой тройку (P, a, P 0 ) (5.8) где P, P 0 ∈ P Expr, и a ∈ Act. Если (5.8) ∈ R, то мы сокращённо обозначаем этот факт в виде знакосочетания P - a P 0 (5.9) Понятие перехода определяется индуктивно, т.е. • указываются тройки вида (5.8), которые являются перехо- дами по определению, и • описываются правила построения новых переходов из уже имеющихся. В этом параграфе мы предполагаем, что • значением каждой процессной константы является конеч- ный процесс, и • каждый конечный процесс является значением некоторой процессной константы. В нижеследующих правилах, определяющих множество пере- ходов R, символы P, P 0 обозначают произвольные ПВ, и символ a обозначает произвольное действие из Act. 1. если P – процессная константа, то P - a P 0 где P 0 – процессная константа, такая, что • значения P и P 0 имеют вид (S, s 0 , R) и (S, s 1 , R) соответственно, и 137 • R содержит переход s 0 - a s 1 2. a.P - a P 3. если P - a P 0 , то • P + Q - a P 0 , и • Q + P - a P 0 • P | Q - a P 0 | Q , и • Q | P - a Q | P 0 • если L ⊆ N ames, a 6= τ , и name(a) 6∈ L, то P \ L - a P 0 \ L • для каждого переименования f P [f ] - f (a) P 0 [f ] 4. если a 6= τ , то из P 1 - a P 0 1 и P 2 - ¯ a P 0 2 следует, что P 1 | P 2 - τ P 0 1 | P 0 2 5. для каждого РО (5.1) и каждого i ∈ {1, . . . , n} если P i - a P 0 то A i - a P 0 (5.10) Можно доказать, что для каждого ПВ P существует лишь конечное множество переходов с началом P , т.е. имеющих вид P - a P 0 Для каждого ПВ P ∈ P Expr процесс [[P ]], соответствующий этому ПВ, имеет вид (P Expr, P, R) 138 При данном определении соответствия между ПВ и процес- сами имеет место следующая теорема. Теорема 32. Для каждого РО (5.1) и каждого i = 1, . . . , n [[A i ]] ∼ P i ([[A 1 ]]/A 1 , . . . , [[A n ]]/A n ) (т.е. список процессов [[A 1 ]], . . . , [[A n ]] является решением системы уравнений, соответствующей РО (5.1) с точностью до ∼). 5.8 Доказательство эквивалентности про- цессов при помощи РО Можно доказывать эквивалентность (∼ или + ≈) двух процессов путём предъявления РО, такого, что оба этих процесса являют- ся компонентами с одинаковыми номерами некоторых решений системы уравнений, соответствующей этому РО. Соответствующие эквивалентности обосновываются теоремой 33. Для формулировки этой теоремы мы введём следующее вспо- могательное понятие. Пусть заданы • бинарное отношение µ на множестве всех процессов, и • РО вида (5.1). Мы будем говорить, что список процессов, определяемый РО (5.1), единствен с точностью до µ, если для каждой пары списков процессов (Q (1) 1 , . . . , Q (1) n ) и (Q (2) 1 , . . . , Q (2) n ) удовлетворяющей следующему условию: для каждого i = 1, . . . , n ( [[Q (1) i ]] , P i (Q (1) 1 /A 1 , . . . , Q (1) n /A n ) ) ∈ µ ( [[Q (2) i ]] , P i (Q (2) 1 /A 1 , . . . , Q (2) n /A n ) ) ∈ µ имеет место соотношение ∀i = 1, . . . , n [[Q (1) i ]] , [[Q (2) i ]] ∈ µ 139 Теорема 33. Пусть задано РО вида (5.1). 1. Если каждое вхождение каждого процессного имени A i в каждое ПВ P j содержится в подвыражении вида a.Q, то список процессов, определяемый РО (5.1), единствен с точ- ностью до ∼. 2. Если • каждое вхождение каждого A i в каждое P j содержит- ся в подвыражении вида a.Q, где a 6= τ , и • каждое вхождение каждого A i в каждое P j содержит- ся только в подвыражениях вида a.Q и Q 1 + Q 2 то список процессов, определяемый РО (5.1), единствен с точностью до + ≈. 5.9 Проблемы, связанные с понятием РО 1. Распознавание существования конечных процессов, эквива- лентных (относительно ∼, ≈, + ≈) процессам вида [[A]]. 2. Построение алгоритмов нахождения минимальных процес- сов, эквивалентных процессам вида [[A]] в том случае, когда эти процессы конечны. 3. Распознавание эквивалентности процессов вида [[A]] (эти процессы могут быть бесконечными, и методы из гла- вы 4 для них не подходят). 4. Распознавание эквивалентности РО. 5. Нахождение необходимых и достаточных условий единствен- ности списка процессов, определяемого РО (с точностью до ∼, + ≈). 140 Глава 6 Примеры доказательства свойств процессов 6.1 Потоковые графы Если процесс P можно представить в виде алгебраического вы- ражения P (P 1 , . . . , P n ) (6.1) в которое входят процессы P 1 , . . . , P n , соединённые символами операций • параллельной композиции, • ограничения, и • переименования то P называется структурной композицией процессов P 1 , . . ., P n Если процесс P является структурной композицией, то ему можно сопоставить некоторый графический объект G(P ) называемый потоковым графом (ПГ) процесса P . Представление структурной композиции в виде ПГ повышает наглядность и облегчает понимание взаимосвязи между её ком- понентами. 141 Для построения ПГ G(P ) для процесса P вида (6.1) строятся ПГ, соответствующие всем подвыражениям выражения (6.1). Элементарные ПГ: Для каждого i = 1, . . . , n, и каждого вхождения P i в выра- жение (6.1), ПГ G(P i ), соответствующий этому вхождению, имеет вид овала, внутри которого написано знакосочетание P i На периметре овала рисуется несколько кружочков, назы- ваемых портами. Каждый порт соответствует некоторому действию из мно- жества Act(P i ), причём • если это действие имеет вид α!, то соответствующий этому действию порт рисуется чёрным цветом, и • если это действие имеет вид α?, то соответствующий этому действию порт рисуется белым цветом. Около каждого порта написана его метка, равная тому дей- ствию из Act(P i ), которому соответствует этот порт. Отметим, что если P i имеет несколько вхождений в вы- ражение (6.1), то для каждого такого вхождения рисуется отдельный элементарный ПГ G(P i ). Параллельная композиция: Если выражение (6.1) содержит подвыражение вида P 0 | P 00 , то G(P 0 | P 00 ) получается • дизъюнктным объединением G(P 0 ) и G(P 00 ), и • соединением стрелочками в этом дизъюнктном объ- единении портов ПГ G(P 0 ) и G(P 00 ) с комплементар- ными метками: если – один из этих ПГ содержит порт с меткой α!, и – другой из этих ПГ содержит порт с меткой α?, то рисуется стрелочка с меткой α от первого порта к второму. 142 Ограничение: G(P 0 \L) получается из G(P 0 ) удалением меток портов, име- на которых принадлежат L. Переименование: G(P 0 [f ]) получается из G(P 0 ) соответствующим переимено- ванием меток портов. В излагаемых ниже примерах процессов приводятся ПГ, со- ответствующие этим процессам. 6.2 Мастерская Рассмотрим модель мастерской, в которой работают двое рабо- чих, пользующиеся для работы одним молотком. Поведение каждого рабочего в мастерской описывается про- цессом J obber J obber Start U sing F inish - ? 6 in? put! get_and_work! out! • Действия in? и out! используются для взаимодействия ра- бочего с заказчиком, и обозначают соответственно – прием материала, и – выдачу готового изделия. • Действия get_and_work! и put! используются для взаимо- действия рабочего с молотком, и обозначают соответствен- но 143 – взятие молотка и выполнение с его помощью некото- рых действий, и – возвращение молотка на место. Обратим внимание, что действие get_and_work! состоит из нескольких действий, которые мы не детализируем и агрегируем все их в одно действие. Согласно графовому представлению процесса J obber, рабо- чий • сначала принимает материал, • затем берет молоток и работает, • после чего кладет молоток, • выдает готовое изделие, • и все повторяется сначала. Поведение молотка мы представляем при помощи следующе- го процесса M allet: M allet Busy - |