Теория процессов
 Скачать 1.62 Mb.
|
|
. Не исключено, что после выполнения действия α? • будет невозможно выполнить ни одного действия, работая в соответствии с процессом P 0 1 • хотя в этот момент появится возможность выполнить пер- вое действие в P 2 Но в этот момент процесс P уже не может изменить свой выбор (т.е. выбрать P 2 вместо P 0 1 ). Процесс P может лишь находиться в состоянии ожидания того, когда появится возможность работать в соответствии с процессом P 0 1 Если же в начальный момент времени окружающая среда может ввести в P как α, так и β, то P выбирает процесс, в соот- ветствии с которым он будет работать, • недетерминированно (т.е. произвольно), или • с учётом некоторых дополнительных факторов. Точное определение операции альтернативной композиции вы- глядит следующим образом. 30 Пусть процессы P 1 и P 2 имеют вид P i = (S i , s 0 i , R i ) (i = 1, 2) причём множества состояний S 1 и S 2 не имеют общих элементов. Альтернативной композицией процессов P 1 и P 2 называ- ется процесс P 1 + P 2 = (S, s 0 , R) компоненты которого определяются следующим образом. • S получается добавлением к S 1 ∪ S 2 нового состояния s 0 , которое будет начальным состоянием процесса P 1 + P 2 • R содержит все переходы из R 1 и R 2 • для каждого перехода из R i (i = 1, 2) вида s 0 i - a s R содержит переход s 0 - a s Если же множества S 1 и S 2 имеют общие элементы, то для определения процесса P 1 + P 2 сначала надо заменить в S 2 те состояния, которые входят также и в S 1 , на новые элементы, а также модифицировать соответствующим образом R 2 и s 0 2 Рассмотрим в качестве примера торговый автомат, который продаёт газированную воду, причём • если покупатель опускает в него монету мон_1 достоин- ством в 1 копейку, то автомат выдаёт стакан воды без си- ропа, • а если покупатель опускает в него монету мон_3 достоин- ством в 3 копейки, то автомат выдаёт стакан воды с сиро- пом 31 причём сразу после продажи одного стакана воды автомат лома- ется. Поведение данного автомата описывается следующим процес- сом: P газ_вода = мон_1 ? . вода_без_сиропа ! . 0 + + мон_3 ? . вода_с_сиропом ! . 0 (3.2) Рассмотрим графовое представление процесса (3.2). Графовые представления слагаемых в сумме (3.2) имеют вид s 10 s 20 s 11 s 21 s 12 s 22 ? ? ? ? мон_1? вода_без_сиропа! мон_3? вода_с_сиропом! Согласно определению альтернативной композиции, графо- вое представление процесса (3.2) получается добавлением к преды- дущей диаграмме нового состояния и соответствующих перехо- дов, в результате чего получается следующая диаграмма: 32 s 10 s 0 s 20 s 11 s 21 s 12 s 22 ? ? ? ? @ @ @ @ @ @ @ @ @ R мон_1? мон_3 ? мон_1? мон_3 ? вода_без_сиропа! вода_с_сиропом! Поскольку состояния s 10 и s 20 недостижимы, то, следователь- но, их (а также связанные с ними переходы) можно удалить, в результате чего получится диаграмма s 0 s 11 s 21 s 12 s 22 ? ? @ @ @ @ @ @ @ @ @ R мон_1 ? мон_3 ? вода_без_сиропа! вода_с_сиропом! 33 которая и является искомым графовым представлением процес- са (3.2). Рассмотрим другой пример. Опишем разменный автомат, в который можно вводить купюры достоинством в 1000 рублей. Автомат должен выдать • либо 2 купюры по 500 рублей, • либо 10 купюр по 100 рублей причем выбор способа размена осуществляется независимо от желания клиента. Сразу после одного сеанса размена автомат ломается. P размен = = 1_по_1000 ? .(2_по_500 ! .0 + 10_по_100 ! .0) На этих двух примерах видно, что альтернативная компо- зиция может использоваться для описания как минимум двух принципиально различных ситуаций. 1. Во-первых, она может выражать зависимость поведения системы от поведения её окружения. Например, в случае автомата P газ_вода , реакция автомата определяется действием покупателя, а именно, достоинством монеты, которую он ввел в автомат. В данном случае процесс, представляющий поведение мо- делируемого торгового автомата, является детерминиро- ванным, то есть его фукнционирование однозначно опре- деляется входными действиями. 2. Во-вторых, на примере автомата P размен мы видим, что при одних и тех же входных действиях возможна различная реакция автомата. Это - пример недетерминизма, то есть неопределенности поведения системы. Неопределённость в поведении систем может происходить по крайней мере по двум причинам. 34 (a) Во-первых, поведение систем может зависеть от слу- чайных факторов. Такими факторами могут быть, например, • сбои в аппаратуре, • коллизии в компьютерной сети • отсутствие купюр необходимого достоинства в бан- комате • или что-либо еще (b) Во-вторых, модель всегда есть некоторая абстракция или упрощение реальной системы. А при этом некото- рые факторы, влияющие на поведение этой системы, могут быть просто исключены из рассмотрения. В частности, на примере процесса P размен мы видим, что ре- альная причина выбора варианта поведения автомата мо- жет не учитываться в процессе, представляющем собой мо- дель поведения этого автомата. Можно схематически изобразить вышеперечисленные варианты использования альтернативной композиции следующим образом: Зависи- мость от вх. данных Альтер- нативная композиция @ @ @ R Случайные факторы Недетер- минизм @ @ @ R Неуч- тенные факторы 3.4 Параллельная композиция Операция параллельной композиции используется для построе- ния моделей поведения динамических систем, состоящих из несколь- 35 ких взаимодействующих компонентов. Прежде чем дать формальное определение этой операции, мы обсудим понятие параллельного функционирования двух систем Sys 1 и Sys 2 , которые мы рассматриваем как компоненты одной системы Sys, т.е. Sys def = {Sys 1 , Sys 2 } (3.3) Пусть поведение систем Sys 1 и Sys 2 представлено процессами P 1 и P 2 соответственно. Поведение системы Sys i (i = 1, 2) в со- ставе системы Sys описывается тем же процессом P i , которым описывается поведение этой системы, рассматриваемой индиви- дуально. Обозначим символом {P 1 , P 2 } процесс, описывающий поведе- ние системы (3.3). Целью этого параграфа является явное опре- деление процесса {P 1 , P 2 } (т.е. построение множеств его состоя- ний и переходов) по информации о процессах P 1 и P 2 Ниже для упрощения изложения мы будем отождествлять понятия “процесс P ”, и “система, поведение которой описывается процессом P ” Как было отмечено выше, функционирование произвольного процесса P может быть интерпретировано как обход графа, соот- ветствующего этому процессу, с выполнением действий, которые являются метками проходимых рёбер. Мы будем предполагать, что при прохождении каждого ребра s - a s 0 • переход от s к s 0 происходит мгновенно, и • факт выполнения действия a имеет место именно в момент этого перехода. В действительности, выполнение каждого из действий проис- ходит в течение некоторого промежутка времени, но мы будем считать, что для каждого проходимого ребра s - a s 0 • до завершения выполнения действия a процесс P находится в состоянии s, и 36 • после завершения выполнения действия a процесс P мгно- венно переходит в состояние s 0 Поскольку выполнение разных действий имеет разную про- должительность, то мы будем считать, что во время своего функ- ционирования процесс P находится каждом состоянии, в которое он попадает, неопределённый промежуток времени. Таким образом, работа процесса P предсталяет собой чередо- вание следующих двух видов деятельности: • ожидание в течение неопределённого промежутка времени в одном из состояний, и • мгновенный переход из одного состояния в другое. Ожидание в одном из состояний может происходить • не только по причине того, что в этот момент происходит выполнение некоторого действия, • но также и по причине того, что процесс P в текущий мо- мент просто не может выполнить какое-либо действие. Например, если • P = α?. P 0 , и • в начальный момент никто не предлагает процессу P объ- ект α то P будет ждать, когда какой-либо процесс предложит ему объ- ект α. Как мы знаем, для каждого процесса • его действия являются либо входными, либо выходными, либо внутренними, и • каждое входное и выходное действие является результатом взаимодействия этого процесса с другим процессом. Каждое входное или выходное действие процесса P i (i = 1, 2) представляет собой 37 • либо результат взаимодействия P i с процессом, не входя- щим в совокупность {P 1 , P 2 }, • либо результат взаимодействия P i с процессом P j , где j ∈ {1, 2} \ {i}. С точки зрения процесса {P 1 , P 2 }, действия второго типа явля- ются внутренними действиями этого процесса, так как они • не представляют собой результат взаимодействия процесса {P 1 , P 2 } с окружающей средой, а • являются результатом взаимодействия компонентов этого процесса. Таким образом, каждое действие процесса {P 1 , P 2 } представляет собой (a) либо результат взаимодействия одного из процессов P i с процессом, не входящим в {P 1 , P 2 }, (b) либо внутреннее действие одного из процессов, входящих в {P 1 , P 2 } (т.е. внутреннее действие P 1 или P 2 ), (c) либо внутреннее действие, которое является результатом взаимодействия процессов P 1 и P 2 , и заключается в том, что – один из этих процессов P i (i = 1, 2) передаёт другому процессу P j (j ∈ {1, 2} \ {i}) некоторый объект, и – процесс P j в тот же самый момент времени принимает от процесса P i этот объект (такой вид взаимодействия называют синхронным взаи- модействием, или рукопожатием). Каждому возможному варианту поведения процесса P i (i = 1, 2) можно сопоставить нить, обозначаемую символом σ i , и пред- ставляющую собой вертикальную линию, на которой нарисованы точки с метками, где 38 • метки точек обозначают действия, исполняемые процессом P i , и • помеченные точки расположены в хронологическом поряд- ке, т.е. – сначала идёт точка, помеченная первым действием про- цесса P i , – под ней - точка, помеченная вторым действием про- цесса P i , – и т.д. Для каждой помеченной точки p на нити мы будем обозна- чать знакосочетанием act(p) метку этой точки. Представим себе, что на плоскости параллельно нарисованы нити σ 1 σ 2 (3.4) где σ i (i = 1, 2) представляет возможный вариант поведения процесса P i в составе процесса {P 1 , P 2 }. Рассмотрим те помеченные точки на нитях из (3.4), которые соответствуют действиям типа (c), т.е взаимодействиям процес- сов P 1 и P 2 . Пусть p - одна из таких точек, и пусть она находится, например, на нити σ 1 Согласно определению понятия взаимодействия, в тот же са- мый момент времени, в который выполняется действие act(p), процесс P 2 выполняет комплементарное действие, т.е. на нити σ 2 есть точка p 0 , такая, что • act(p 0 ) = act(p), и • действия act(p) и act(p 0 ) исполняются в один и тот же мо- мент времени. Отметим, что • на нити σ 2 может быть несколько точек с меткой act(p), но ровно одна из этих точек соответствует тому действию, которое исполняется совместно с действием, соответствую- щим точке p, и 39 • на нити σ 1 может быть несколько точек с меткой act(p), но ровно одна из этих точек соответствует тому действию, которое исполняется совместно с действием, соответствую- щим точке p 0 Преобразуем нашу диаграмму нитей (3.4) следующим образом: для каждой пары точек p, p 0 с вышеуказанными свойствами • соединим точки p и p 0 стрелкой, начало которой - та из этих точек, которая имеет метку вида α!, а конец - точка с меткой α?, • нарисуем на этой стрелке метку α, и • заменим метки точек p и p 0 на τ . Стрелка, соединяющая точки p и p 0 , называется синхронизаци- онной стрелкой. Такие стрелки обычно рисуют горизонтально, для чего точки на нитях располагают так, чтобы соединяемые стрелками точки располагались на одинаковой высоте. После того, как мы сделаем такие преобразования для всех пар точек, в которых происходят действия вида (c), у нас полу- чится диаграмма, которую в литературе по параллельным вы- числениям принято называть Message Sequence Chart (MSC). Эта диаграмма представляет собой один из вариантов функцио- нирования процесса {P 1 , P 2 }. Мы будем обозначать знакосочетанием Beh{P 1 , P 2 } совокупность всех MSC, каждая из которых соответствует неко- торому варианту функционирования процесса {P 1 , P 2 }. Рассмотрим следующий пример: {P 1 , P 2 } состоит из двух про- цессов P 1 и P 2 , где • P 1 - торговый автомат, поведенние которого задается вы- ражением P 1 = мон?. шок!.0 (3.5) (т.е. он получает монету, выдаёт шоколадку, и после этого ломается) 40 • P 2 - покупатель, поведенние которого задается выражением P 2 = мон!. шок?.0 (3.6) (т.е. он опускает монету, получает шоколадку, и после этого перестаёт функционировать в роли покупателя) Нити этих процессов имеют вид мон? шок! мон! шок? Если все действия на этих нитях являются действиями типа (c), то данная диаграмма преобразуется в следующую MSC: τ мон - шок τ τ τ Однако возможен и следующий вариант функционирования процесса {P 1 , P 2 }: • первое действие P 1 и P 2 имеет тип (c), т.е. покупатель опус- кает в автомат монету, а автомат её принимает • второе действие автомата P 1 является взаимодействием с процессом, который является внешним по отношению к {P 1 , P 2 }, т.е., например, к автомату подошёл вор, и взял шоколадку, прежде чем это смог сделать покупатель P 2 41 В этой ситуации покупатель не может выполнить второе дей- ствие как внутреннее действие процесса {P 1 , P 2 }. Согласно опи- санию процесса, в данном случае возможны два варианта пове- дения. 1. P 2 будет находиться в состоянии бесконечного ожидания. Соответствующая этому варианту MSC имеет вид τ мон шок! τ 2. P 2 сможет успешно завершить работу. Это произойдёт в том случае, если некоторый процесс, внеш- ний по отношению к {P 1 , P 2 }, передаст шоколадку процессу P 2 Соответствующая этому варианту MSC имеет вид τ мон шок! τ шок? Теперь рассмотрим вопрос о том, каким образом процесс {P 1 , P 2 } может быть определён явно, т.е. в терминах состояний и перехо- дов с метками из множества Act. 42 На первый взгляд, данный вопрос является некорректным, так как {P 1 , P 2 } представляет собой модель параллельного функ- ционирования процессов P 1 и P 2 , при котором • в один и тот же момент времени могут быть исполнены действия обоими процессами, входящими в {P 1 , P 2 }, и, • следовательно, процесс {P 1 , P 2 } может совершать такие дей- ствия, которые представляют собой пары действий из мно- жества Act, т.е. они не принадлежат множеству Act. Заметим на это, что абсолютная одновременность имеет ме- сто лишь для тех пар действий, которые порождают одно внут- реннее действие процесса {P 1 , P 2 } типа (c). Для всех остальных пар действий процессов P 1 и P 2 , даже если они произошли с точ- ки зрения внешнего наблюдателя одновременно, мы можем пред- полагать без ограничения общности, что одно из них произошло немного раньше или немного позже другого. Таким образом, мы можем считать, что процесс {P 1 , P 2 } функ- ционирует последовательно, т.е. что при любом варианте функ- ционирования процесса {P 1 , P 2 } выполняемые им действия обра- зуют некоторую линейно упорядоченную последовательность tr = (act 1 , act 2 , . . .) (3.7) в которой действия упорядочены по времени их выполнения: сна- чала произошло act 1 , затем - act 2 , и т.д. Поскольку каждый возможный вариант функционирования процесса {P 1 , P 2 } представляется некоторой MSC, то можно счи- тать, что последовательность (3.7) получается некоторой линеа- ризацией этой MSC (т.е. “вытягиванием” её в цепочку). Для определения понятия линеаризации MSC мы введём несколь- ко вспомогательных понятий и обозначений. Пусть C – некото- рая MCS. Тогда • знакосочетание P oints(C) обозначает множество всех то- чек, входящих в MSC C, • для каждой точки p ∈ P oints(C) знакосочетание act(p) обо- значает действие, приписанное точке p 43 • для каждой пары точек p, p 0 ∈ P oints(C) знакосочетание p → p 0 означает, что имеет место одно из следующих условий: – p и p 0 находятся на одной и той же нити, и p 0 располо- жена ниже, чем p, или – существует синхронизационная стрелка с началом в p и концом в p 0 • для каждой пары точек p, p 0 ∈ P oints(C) знакосочетание p ≤ p 0 означает, что либо p = p 0 , либо существует последователь- ность точек p 1 , . . . , p k , такая, что – p = p 1 , p 0 = p k – для каждого i = 1, . . . , k − 1 p i → p i+1 Отношение ≤ на точках MSC можно рассматривать как отноше- ние хронологической упорядоченности, т.е. знакосочетание p ≤ p 0 можно интерпретировать как утверждение о том, что • точки p и p 0 совпадают или соединены синхронизационной стрелкой (т.е. действия в p и в p 0 совпадают), • или действие в p 0 произошло позже, чем произошло дей- ствие в p. Точное определение понятия линеаризации MSC имеет следу- ющий вид. Пусть заданы MSC C и последовательность действий tr вида (3.7). Обозначим множество индексов элементов после- довательности tr знакосочетанием Ind(tr), т.е. Ind(tr) = {1, 2, . . .} (данное множество может быть как конечным, так и бесконеч- ным). 44 Последовательность tr называется линеаризацией MSC C, если существует сюрьективное отображение lin : P oints(C) → Ind(tr) удовлетворяющее следующим условиям. 1. для каждой пары p, p 0 ∈ P oints(C) p ≤ p 0 ⇒ lin(p) ≤ lin(p 0 ) 2. для каждой пары p, p 0 ∈ P oints(C) соотношение lin(p) = lin(p 0 ) имеет место тогда и только тогда, когда • p = p 0 , или • существует синхронизационная стрелка с началом в p и концом в p 0 3. для каждой точки p ∈ P oints(C) act(p) = act lin(p) т.е. отображение lin • сохраняет хронологический порядок, • отождествляет те точки MSC C, которые соответствуют од- ному действию процесса {P 1 , P 2 }, и • не отождествляет никакие другие точки. Обозначим символом Lin(C) совокупность всех линеаризаций MSC C. Теперь задачу явного описания процесса {P 1 , P 2 } можно сфор- мулировать следующим образом: построить процесс P , удовле- творяющий условию T r(P ) = [ C∈Beh{P 1 ,P 2 } Lin(C) (3.8) 45 т.е. в процессе P должны быть представлены все линеаризации любого возможного совместного поведения процессов P 1 и P 2 Условие (3.8) обосновывается следующим соображением: по- скольку мы не знаем, • как согласованы между собой часы в процессах P 1 и P 2 , и • какова продолжительность пребывания в каждом из состо- яний, в которые эти процессы попадают то мы должны считать возможным любой порядок исполнения действий, который не противоречит отношению хронологической упорядоченности. Приступим к построению процесса P , удовлетворяющему усло- вию (3.8). Пусть процессы P 1 и P 2 имеют вид P i = (S i , s 0 i , R i ) (i = 1, 2) Рассмотрим произвольную линеаризацию tr произвольной MSC из Beh{P 1 , P 2 } tr = ( a 1 , a 2 , . . . ) Нарисуем линию, которую мы будем интерпретировать как временн´ ую шкалу. Выделим на ней точки p 1 , p 2 , . . ., помеченные действиями a 1 , a 2 , . . ., причём помеченные точки расположены в том порядке, в котором соответствующие действия перечислены в tr, т.е. сначала идёт точка p 1 с меткой a 1 , за ней - точка p 2 с меткой a 2 , и т.д. Обозначим символами I 0 , I 1 , I 2 , . . . следующие участки этой линии: • I 0 представляет собой совокупность всех точек линии перед точкой p 1 , т.е. I 0 def = ] − ∞, p 1 [ • для каждого i ≥ 1 участок I i состоит из точек между p i и p i+1 , т.е. I i def = ]p i , p i+1 [ 46 Каждый из этих участков I i можно интерпретировать как про- межуток времени, в течение которого процесс P не выполняет никаких действий, т.е. в моменты времени между p i и p i+1 про- цессы P 1 и P 2 находятся в фиксированных состояниях (s 1 ) i и (s 2 ) i соответственно. Обозначим символом s i пару ((s 1 ) i , (s 2 ) i ). Данную пару мож- но интерпретировать как состояние всего процесса P , в котором он находится в каждый момент времени из промежутка I i По определению последовательности tr, имеет место одна из двух ситуаций. 1. Действие a i имеет тип (a) или (b), т.е. оно было выполнено одним из процессов, входящих в P . Возможны два случая. (a) Это действие было выполнено процессом P 1 В этом случае мы имеем следующую связь между со- стояниями s i и s i+1 : • (s 1 ) i - a i (s 1 ) i+1 ∈ R 1 • (s 2 ) i+1 = (s 2 ) i (b) Это действие было выполнено процессом P 2 В этом случае мы имеем следующую связь между со- стояниями s i и s i+1 : • (s 2 ) i - a i (s 2 ) i+1 ∈ R 2 • (s 1 ) i+1 = (s 1 ) i 2. Действие a i имеет тип (c). В этом случае мы имеем следующую связь между состоя- ниями s i и s i+1 : • (s 1 ) i - a (s 1 ) i+1 ∈ R 1 • (s 2 ) i - a (s 2 ) i+1 ∈ R 2 для некоторого a ∈ Act \ {τ }. 47 Сформулированные выше свойства последовательности tr мож- но переформулировать следующим образом: tr является трассой процесса (S, s 0 , R) (3.9) компоненты которого определяются следующим образом: • S def = S 1 × S 2 def = {(s 1 , s 2 ) | s 1 ∈ S 1 , s 2 ∈ S 2 } • s 0 def = (s 0 1 , s 0 2 ) • для – каждого перехода s 1 - a s 0 1 из R 1 , и – каждого состояния s ∈ S 2 R содержит переход (s 1 , s) - a (s 0 1 , s) • для – каждого перехода s 2 - a s 0 2 из R 2 , и – каждого состояния s ∈ S 1 R содержит переход (s, s 2 ) - a (s, s 0 2 ) • для каждой пары переходов с комплементарными метками s 1 - a s 0 1 ∈ R 1 s 2 - a s 0 2 ∈ R 2 R содержит переход (s 1 , s 2 ) - τ (s 0 1 , s 0 2 ) 48 Нетрудно показать и обратное: каждая трасса в вышеопреде- лённом процессе (3.9) является линеаризацией некоторой MSC C из множества Beh{P 1 , P 2 }. Таким образом, в качестве искомого процесса P можно взять процесс (3.9). Данный процесс называется параллельной ком- позицией процессов P 1 и P 2 , и обозначается знакосочетанием P 1 | P 2 Приведём в качестве примера процесс P 1 | P 2 , где процессы P 1 и P 2 представляют поведение торгового автомата и покупателя (см. (3.5) и (3.6)). Графовые представления этих процессов имеют вид s 10 s 20 s 11 s 21 s 12 s 22 ? ? ? ? мон? шок! мон! шок? 49 Графовое представление процесса P 1 |P 2 имеет вид (s 10 , s 20 ) (s 11 , s 20 ) (s 12 , s 20 ) (s 10 , s 21 ) (s 11 , s 21 ) (s 12 , s 21 ) (s 10 , s 22 ) (s 11 , s 22 ) (s 12 , s 22 ) ? мон? ? мон? ? мон? ? шок! ? шок! ? шок! - мон! - шок? - мон! - шок? - мон! - шок? @ @ @ @ @ @ @ @ R τ @ @ @ @ @ @ @ @ R τ Заметим, что размер множества состояний процесса P 1 |P 2 ра- вен произведению размеров множеств состояний процессов P 1 и P 2 , т.е. размер описания процесса P 1 | P 2 может существенно превышать суммарную сложность размеров описаний его компо- нентов P 1 и P 2 . Это может сделать невозможным анализ такого процесса по причине его высокой сложности. Поэтому в практических задачах при анализе процессов вида P 1 | P 2 , вместо явного построения процесса P 1 | P 2 строится про- цесс, в котором каждая MSC из Beh{P 1 , P 2 } представлена не все- ми возможными линеаризациями, а хотя бы одной линеаризаци- ей. Сложность такого процесса может быть существенно меньше по сравнению со сложностью процесса P 1 |P 2 Построение процесса такого вида имеет смысл, например, в том случае, когда анализируемое свойство ϕ процесса P 1 | P 2 об- ладает следующим качеством: • если ϕ истинно для одной из линеаризаций произвольной MSC C ∈ Beh{P 1 , P 2 }, • то ϕ истинно для всех линеаризаций этой MSC. 50 Как правило, процесс, в котором каждая MSC из Beh{P 1 , P 2 } представлена не всеми возможными линеаризациями, а хотя бы одной линеаризацией, строится как некоторый подпроцесс про- цесса P 1 |P 2 , т.е. получается из P 1 |P 2 удалением некоторых состо- яний и связанных с ними переходов. Поэтому такие процессы называют редуцированными. Проблема построения редуцированных процессов называет- ся проблемой редукции частичных порядков (partial order reduction). Эта проблема интенсивно исследуется многими ве- дущими специалистами в области верификации. Приведём в качестве примера редуцированный процесс для рассмотренного выше процесса P 1 | P 2 , состоящего из торгового автомата и покупателя. (s 10 , s 20 ) (s 10 , s 21 ) (s 11 , s 21 ) (s 11 , s 22 ) (s 12 , s 22 ) ? мон? ? шок! - мон! - шок? @ @ @ @ @ @ @ @ R τ @ @ @ @ @ @ @ @ R τ В заключение отметим, что задача анализа процессов, состо- ящих из нескольких взаимодействующих компонентов, наиболее часто возникает в ситуации, когда такими компонентами явля- ются компьютерные программы и аппаратные устройства, функ- ционирующие совместно в рамках единого программно-аппарат- ного комплекса. Взаимодействие между такими программами осуществляется 51 при помощи процессов-посредников, т.е. программы взаимодей- ствуют друг с другом через посредство некоторых процессов, которые синхронно взаимодействуют с каждой из программ. Взаимодействие между параллельно работающими програм- мами обычно реализуется одним из следующих двух способов. 1. Взаимодействие через общую память. В данном случае такими посредниками являются ячейки памяти, к которым имеют доступ обе программы. Взаимодействие может осуществляться, например, так: од- на программа пишет информацию в эти ячейки, а другая читает содержимое ячеек. 2. Взаимодействие путем посылки сообщений. В данном случае посредником является канал, с которым программы могут осуществлять следующие операции: • посылка сообщения в канал передающей программой, и • приём сообщения принимающей программой. Канал может представлять собой буфер, хранящий несколь- ко сообщений. Сообщения в канале могут быть организова- ны по принципу очереди (т.е. сообщения покидают канал в том же порядке, в котором они в него поступают). 3.5 Ограничение Пусть P = (S, s 0 , R) некоторый процесс, и L – произвольное под- множество множества N ames. Ограничением P по L называется процесс P \ L = (S, s 0 , R 0 ) который получается из P удалением тех переходов, которые име- ют метки с именами из L, т.е. R 0 def = ( ( s - a s 0 ) ∈ R a = τ, или name(a) 6∈ L ) 52 Операция ограничения используется, как правило, совместно с операцией параллельной композиции для представления таких процессов, которые • состоят из нескольких компонентов, и • взаимодействие между этими компонентами должно удо- влетворять некоторым ограничениям. Например, пусть P 1 и P 2 – торговый автомат и покупатель, которые рассматривались в предыдущем параграфе. Мы хотели бы описать процесс, являющийся моделью такого параллельного функционирования процессов P 1 и P 2 , при кото- ром эти процессы могут совершать действия, связанные с поку- пкой-продажей шоколадки, только совместно. Искомый процесс может быть получен из процесса P 1 |P 2 при- менением операции ограничения по множеству имён всех дей- ствий, которые связаны с покупкой-продажей шоколадки, т.е. данный процесс описывается выражением P def = (P 1 |P 2 ) \ {мон, шок} (3.10) Графовое представление процесса (3.10) имеет вид (s 10 , s 20 ) (s 11 , s 20 ) (s 12 , s 20 ) (s 10 , s 21 ) (s 11 , s 21 ) (s 12 , s 21 ) (s 10 , s 22 ) (s 11 , s 22 ) (s 12 , s 22 ) @ @ @ @ @ @ @ @ R τ @ @ @ @ @ @ @ @ R τ 53 После удаления недостижимых состояний получится процесс, имеющий следующее графовое представление: (s 10 , s 20 ) (s 11 , s 21 ) (s 12 , s 22 ) - τ - τ Рассмотрим другой пример. Немного изменим определения торгового автомата и покупателя: пусть они еще и сигнализи- руют об успешном выполнении своей работы, т.е. их процессы имеют, например, следующий вид: P 1 def = мон?.шок!.звяк!.0 P 2 def = мон!.шок?.ура!.0 В этом случае графовое представление процесса (3.10) после удаления недостижимых состояний имеет вид - τ - τ ? ура! ? ура! - звяк! - звяк! Данный процесс допускает исполнение тех невнутренних дей- ствий, которые не связаны с покупкой и продажей шоколадки. Отметим, что в данном случае в процессе (3.10) присутствует недетерминизм, хотя в компонентах P 1 и P 2 его нет. Причиной возникновения этого недетерминизма является наше неполное знание о моделируемой системе: поскольку мы не имеем точных знаний о длительности действий звяк! и ура!, то модель системы должна допускать любой порядок их выполнения. 54 3.6 Переименование Следующая операция, которую мы рассмотрим - это унарная операция переименования. Для задания этой операции необходимо определить функцию f : N ames → N ames называемую переименованием. Действие данной операции на процесс P заключается в изме- нении меток переходов: • метки вида α? заменяются на f (α)?, и • метки вида α! заменяются на f (α)! Получившийся процесс обозначается знакосочетанием P [f ]. Если переименование f действует нетождественно лишь на имена из списка α 1 , . . . , α n и отображает их в имена β 1 , . . . , β n соответственно, то для P [f ] мы будем иногда использовать эк- вивалентное обозначение P [β 1 /α 1 , . . . , β n /α n ] Операция переименования позволяет многократно использо- вать один и тот же процесс P в качестве компоненты при по- строении более сложного процесса P 0 . Эта операция использует- ся для предотвращения “конфликтов” между именами действий, используемых в различных вхождениях P в P 0 3.7 Свойства операций на процессах В этом параграфе мы приводим некоторые простейшие свойства определённых выше операций на процессах. Все эти свойства 55 имеют вид равенств. Для первых двух свойств мы даём их обос- нование, остальные свойства приводятся без комментариев ввиду их очевидности. Напомним (см. параграф 2.7), что мы считаем два процесса равными, если • они изоморфны, или • один из этих процессов можно получить из другого путём удаления некоторых недостижимых состояний и связанных с ними переходов. 1. Операция + ассоциативна, т.е. для любых процессов P 1 , P 2 и P 3 верно равенство (P 1 + P 2 ) + P 3 = P 1 + (P 2 + P 3 ) Действительно, пусть процессы P i (i = 1, 2, 3) имеют вид P i = (S i , s 0 i , R i ) (i = 1, 2, 3) (3.11) причём множества состояний S 1 , S 2 и S 3 попарно не пересе- каются. Тогда обе части данного равенства равны процессу P = (S, s 0 , R), компоненты которого определяются следую- щим образом: • S def = S 1 ∪ S 2 ∪ S 3 ∪ {s 0 }, где s 0 – новое состояние, не входящее в S 1 , S 2 и S 3 • R содержит все переходы из R 1 , R 2 и R 3 • для каждого перехода из R i (i = 1, 2, 3) вида s 0 i - a s R содержит переход s 0 - a s Из свойства ассоциативности операции + следует, что до- пустимы выражения вида P 1 + . . . + P n (3.12) 56 так как при любой расстановке скобок в выражении (3.12) получится один и тот же процесс. Процесс, являющийся значением выражения (3.12) можно описать явно следущим образом. Пусть процессы P i (i = 1, . . . , n) имеют вид P i = (S i , s 0 i , R i ) (i = 1, . . . , n) (3.13) причём множества состояний S 1 , . . . , S n попарно не пересе- каются. Тогда процесс, являющийся значением выражения (3.12), имеет вид P = (S, s 0 , R) где компоненты S, s 0 , R определяются следующим образом: • S def = S 1 ∪ . . . ∪ S n ∪ {s 0 }, где s 0 – новое состояние, не входящее в S 1 , . . . , S n • R содержит все переходы из R 1 , . . . , R n • для каждого перехода из R i (i = 1, . . . , n) вида s 0 i - a s R содержит переход s 0 - a s 2. Операция | ассоциативна, т.е. для любых процессов P 1 , P 2 и P 3 верно равенство (P 1 | P 2 ) | P 3 = P 1 | (P 2 | P 3 ) Действительно, пусть процессы P i (i = 1, 2, 3) имеют вид (3.11). Тогда обе части данного равенства равны процессу P = (S, s 0 , R) компоненты которой определяются следую- щим образом: • S def = S 1 × S 2 × S 3 def = def = {(s 1 , s 2 , s 3 ) | s 1 ∈ S 1 , s 2 ∈ S 2 , s 3 ∈ S 3 } • s 0 def = (s 0 1 , s 0 2 , s 0 3 ) • для 57 – каждого перехода s 1 - a s 0 1 из R 1 , и – каждой пары состояний s 2 ∈ S 2 , s 3 ∈ S 3 R содержит переход (s 1 , s 2 , s 3 ) - a (s 0 1 , s 2 , s 3 ) • для – каждого перехода s 2 - a s 0 2 из R 2 , и – каждой пары состояний s 1 ∈ S 1 , s 3 ∈ S 3 R содержит переход (s 1 , s 2 , s 3 ) - a (s 1 , s 0 2 , s 3 ) • для – каждого перехода s 3 - a s 0 3 из R 3 , и – каждой пары состояний s 1 ∈ S 1 , s 2 ∈ S 2 R содержит переход (s 1 , s 2 , s 3 ) - a (s 1 , s 2 , s 0 3 ) • для – каждой пары переходов с комплементарными мет- ками s 1 - a s 0 1 ∈ R 1 s 2 - a s 0 2 ∈ R 2 и – каждого состояния s 3 ∈ S 3 R содержит переход (s 1 , s 2 , s 3 ) - τ (s 0 1 , s 0 2 , s 3 ) • для – каждой пары переходов с комплементарными мет- ками s 1 - a s 0 1 ∈ R 1 s 3 - a s 0 3 ∈ R 3 и 58 – каждого состояния s 2 ∈ S 2 R содержит переход (s 1 , s 2 , s 3 ) - τ (s 0 1 , s 2 , s 0 3 ) • для – каждой пары переходов с комплементарными мет- ками s 2 - a s 0 2 ∈ R 2 s 3 - a s 0 3 ∈ R 3 и – каждого состояния s 1 ∈ S 1 R содержит переход (s 1 , s 2 , s 3 ) - τ (s 1 , s 0 2 , s 0 3 ) Из свойства ассоциативности операции | следует, что до- пустимы выражения вида P 1 | . . . | P n (3.14) так как при любой расстановке скобок в выражении (3.14) получится один и тот же процесс. Процесс, являющийся значением выражения (3.14) можно описать явно следущим образом. Пусть процессы P i (i = 1, . . . , n) имеют вид (3.13). Тогда процесс, являющийся значением выражения (3.14), имеет вид P = (S, s 0 , R) где компоненты S, s 0 , R определяются следующим образом: • S def = S 1 × . . . × S n def = def = {(s 1 , . . . , s n ) | s 1 ∈ S 1 , . . . , s n ∈ S n } • s 0 def = (s 0 1 , . . . , s 0 n ) • для – каждого i ∈ {1, . . . , n} 59 – каждого перехода s i - a s 0 i из R i , и – каждого списка состояний s 1 , . . . , s i−1 , s i+1 , . . . , s n где ∀ j ∈ {1, . . . , n} s j ∈ S j R содержит переход (s 1 , . . . , s n ) - a (s 1 , . . . , s i−1 , s 0 i , s i+1 , . . . , s n ) • для – каждой пары индексов i, j ∈ {1, . . . , n}, где i < j – каждой пары переходов с комплементарными мет- ками s i - a s 0 i ∈ R i s j - a s 0 j ∈ R j и – каждого списка состояний s 1 , . . . , s i−1 , s i+1 , . . . , s j−1 , s j+1 , . . . , s n где ∀ k ∈ {1, . . . , n} s k ∈ S k R содержит переход (s 1 , . . . , s n ) - τ s 1 , . . . , s i−1 , s 0 i , s i+1 , . . . , s j−1 , s 0 j , s j+1 , . . . , s n ! 3. Операция + коммутативна, т.е. для любых процессов P 1 и P 2 верно равенство P 1 + P 2 = P 2 + P 1 4. Операция | коммутативна, т.е. для любых процессов P 1 и P 2 верно равенство P 1 | P 2 = P 2 | P 1 60 5. 0 является нейтральным элементом относительно операции | : P | 0 = P Для операции + аналогичное свойство тоже имеет место, если вместо равенства процессов будет использовано поня- тие сильной эквивалентности процессов (которое определя- ется ниже). Данное свойство, а также свойство идемпотент- ности операции + доказываются в параграфе 4.5 (теорема 4). 6. 0 \ L = 0 7. 0[f ] = 0 8. P \ L = P , если L ∩ names(Act(P )) = ∅. (напомним, что Act(P ) обозначает множество действий a ∈ Act \ {τ }, таких, что P содержит переход с меткой a) 9. (a.P ) \ L = ( 0, если a 6= τ и name(a) ∈ L a.(P \ L), иначе 10. (P 1 + P 2 ) \ L = (P 1 \ L) + (P 2 \ L) 11. (P 1 | P 2 ) \ L = (P 1 \ L) | (P 2 \ L), если L ∩ names(Act(P 1 ) ∩ Act(P 2 )) = ∅ 12. (P \ L 1 ) \ L 2 = P \ (L 1 ∪ L 2 ) 13. P [f ] \ L = (P \ f −1 (L))[f ] 14. P [id] = P , где id – тождественная функция 15. P [f ] = P [g], если сужения функций f и g на множество names(Act(P )) совпадают. 16. (a.P )[f ] = f (a).(P [f ]) 17. (P 1 + P 2 )[f ] = P 1 [f ] + P 2 [f ] 61 18. (P 1 | P 2 )[f ] = P 1 [f ] | P 2 [f ], если сужение функции f на мно- жество names(Act(P 1 ) ∪ Act(P 2 )) является инъективной функцией. 19. (P \ L)[f ] = P [f ] \ f (L), если f иньективна. 20. P [f ][g] = P [g ◦ f ] 62 Глава 4 Эквивалентность процессов 4.1 Понятие эквивалентности процессов и связанные с ним задачи Одно и то же поведение может быть представлено различными процессами. Например, рассмотрим два процесса: a - a - a - a Хотя у первого процесса всего одно состояние, а у второго множество состояний бесконечно, но эти процессы представля- ют одно и то же поведение, которое заключается в постоянном выполнении одного и того же действия a. Представляет интерес поиск подходящего определения экви- валентности процессов, согласно которому процессы эквивалент- ны тогда и только тогда, когда они имеют одно и то же поведе- ние. В этой главе мы излагаем несколько определений понятия эк- вивалентности процессов. Выбор того или иного варианта данно- го понятия в конкретной ситуации должен определяться тем, как именно в данной ситуации понимается одинаковость поведения процессов. 63 В параграфах 4.2 и 4.3 вводятся понятия трассовой эквива- лентности и сильной эквивалентности процессов. Данные поня- тия используются в той ситуации, когда все действия, выполня- ющиеся в процессах, имеют одинаковый статус. В параграфах 4.8 и 4.9 предлагаются другие варианты поня- тия эквивалентности процессов: наблюдаемая эквивалентность и наблюдаемая конгруэнция. Данные понятия используются в тех ситуациях, когда мы рассматриваем невидимое действие τ как несущественное, и считаем две трассы одинаковыми, если одна может быть получена из другой путём вставок и/или удалений невидимых действий τ . С каждым из возможных вариантов понятия эквивалентно- сти процессов связаны две естественные задачи. 1. Распознавание для двух заданных процессов, являются ли они эквивалентными. 2. Построение по заданному процессу P такого процесса P 0 , который является наименее сложным (например, имеет ми- нимальное число состояний) среди всех процессов, которые эквивалентны P . 4.2 Трассовая эквивалентность процес- сов Как уже было сказано выше, мы хотели бы рассматривать два процесса как эквивалентные, если они описывают одно и то же поведение. Поэтому, если мы рассматриваем поведение процесса как порождение некоторой трассы, то необходимым условием эк- вивалентности процессов P 1 и P 2 является совпадение множеств их трасс: T r(P 1 ) = T r(P 2 ) (4.1) В некоторых ситуациях условие (4.1) можно использовать в качестве определения эквивалентности между P 1 и P 2 . Однако нижеследующий пример показывает, что это условие не отража- ет один важный аспект поведения процессов. 64 ? A A A A U a b c A A A U ? ? a a b c (4.2) Множества трасс этих процессов совпадают: T r(P 1 ) = T r(P 2 ) = {ε, a, ab, ac} (где ε – пустая последовательность). Однако эти процессы отличаются тем, что • в левом процессе после выполнения первого действия (a) сохраняется возможность выбора следующего действия (b или c), в то время как • в правом процессе после выполнения первого действия та- кого выбора нет: – если первый переход был совершён по левому ребру, то вторым действием может быть только действие b, – а если по правому - то только действие c, т.е. второе действие было предопределено ещё до выполне- ния первого действия. Если мы не хотели бы рассматривать эти процессы как эк- вивалентные, то условие (4.1) надо некоторым образом усилить. Один из вариантов такого усиления излагается ниже. Для того, чтобы его сформулировать, определим сначала понятие трассы из некоторого состояния процесса. Каждый вариант поведения процесса P = (S, s 0 , R) мы интер- претируем как порождение некоторой последовательности пере- ходов s 0 - a 1 s 1 - a 2 s 2 - a 3 (4.3) 65 начинающейся с начального состояния, т.е. s 0 = s 0 Мы можем рассматривать порождение последовательности (4.3) не только с начального, а с произвольного состояния s ∈ S, т.е. рассматривать последовательность вида (4.3), в которой s 0 = s. Последовательность (a 1 , a 2 , . . .) меток этих переходов мы будем называть трассой с началом в s. Множество всех таких трасс мы будем обозначать знакосочетанием T r s (P ). Пусть P 1 и P 2 – процессы вида P i = (S i , s 0 i , R i ) (i = 1, 2) Рассмотрим произвольную конечную последовательность пе- реходов в P 1 вида s 0 1 = s 0 - a 1 s 1 - a 2 - a n s n (n ≥ 0) (4.4) (случай n = 0 соответствует пустой последовательности перехо- дов (4.4), к которой s n = s 0 1 ) Последовательность (4.4) можно рассматривать как началь- ный этап функционирования процесса P 1 , а каждую трассу из T r s n (P 1 ) – как некоторое продолжение этого этапа. Процессы P 1 и P 2 называются трассово эквивалентными, если • для каждого начального этапа (4.4) функционирования про- цесса P 1 существует начальный этап функционирования процесса P 2 s 0 2 = s 0 0 - a 1 s 0 1 - a 2 - a n s 0 n (4.5) который имеет точно такую же трассу a 1 . . . a n , что и (4.4), и в конце которого имеется точно такой же выбор дальней- шего продолжения, что и в конце этапа (4.4), т.е. T r s n (P 1 ) = T r s 0 n (P 2 ) (4.6) • и, кроме того, имеет место симметричное условие: для каж- дой последовательности переходов в P 2 вида (4.5) долж- на существовать последовательность переходов в P 1 вида (4.4), такая, что имеет место равенство (4.6). 66 Данные условия имеют недостаток: в их формулировке участву- ют потенциально неограниченные множества последовательно- стей переходов вида (4.4) и (4.5), а также потенциально неогра- ниченные множества трасс из (4.6). Поэтому проверка данных условий представляется затруднительной даже в том случае, ко- гда процессы P 1 и P 2 конечны. Представляет интерес задача нахождения условий, равносиль- ных условиям трассовой эквивалентности, которые можно было бы алгоритмически проверять для заданных процессов P 1 и P 2 в том случае, когда эти процессы конечны. Иногда рассматривают такую эквивалентность между про- цессами, которая отличается от трассовой эквивалентности за- меной условия (4.6) на более слабое условие: Act(s n ) = Act(s 0 n ) где для каждого состояния s знакосочетание Act(s) обозначает множество всех действий a ∈ Act, таких, что существует переход с началом в s и помеченный действием a. 4.3 Сильная эквивалентность Ещё одним вариантом понятия эквивалентности процессов явля- ется сильная эквивалентность. Для определения этого поня- тия мы введём вспомогательные обозначения. После того, как процесс P = (S, s 0 , R) (4.7) выполнит первое действие и перейдёт в новое состояние s 1 , его поведение будет неотличимо от поведения процесса P 0 def = (S, s 1 , R) (4.8) имеющего те же компоненты, что и P , за исключением началь- ного состояния. Мы будем использовать обозначение P - a P 0 (4.9) как сокращённую запись утверждения о том, что 67 • P и P 0 – процессы вида (4.7) и (4.8) соответственно, и • R содержит переход s 0 - a s 1 (4.9) можно интерпретировать как утверждение о том, что про- цесс P , может • выполнить действие a, и после этого • вести себя как процесс P 0 Понятие сильной эквивалентности основано на следующем понимании эквивалентности процессов: если мы рассматриваем процессы P 1 и P 2 как эквивалентные, то должно быть выполнено следующее условие: • если один из этих процессов P i может – выполнить некоторое действие a ∈ Act, – и после этого вести себя как некоторый процесс P 0 i • то и другой процесс P j (j ∈ {1, 2} \ {i}) тоже должен об- ладать способностью – выполнить то же самое действие a, – после чего вести себя как некоторый процесс P 0 j , кото- рый эквивалентен P 0 i Таким образом, искомая эквивалентность должна представ- лять собой некоторое бинарное отношение µ на множестве всех процессов, обладающее следующими свойствами. (1) Если (P 1 , P 2 ) ∈ µ, и для некоторого процесса P 0 1 верно утверждение P 1 - a P 0 1 (4.10) то должен существовать процесс P 0 2 , такой, что выполнены условия P 2 - a P 0 2 (4.11) и (P 0 1 , P 0 2 ) ∈ µ (4.12) 68 (2) Симметричное свойство: если (P 1 , P 2 ) ∈ µ, и для некоторого процесса P 0 2 верно (4.11), то должен существовать процесс P 0 1 , такой, что выполнены условия (4.10) и (4.12). Заметим, что мы не требуем, чтобы µ было отношением эквива- лентности. Обозначим символом M совокупность всех бинарных отно- шений, которые обладают вышеприведёнными свойствами. Множество M непусто: оно содержит, например, диагональ- ное отношение, которое состоит из всех пар вида (P, P ), где P – произвольный процесс. Встаёт естественный вопрос о том, какое же из отношений, входящих в M, можно использовать для определения понятия сильной эквивалентности. Мы предлагаем наиболее простой ответ на этот вопрос: мы будем считать P 1 и P 2 сильно эквивалентными в том и только в том случае, когда существует хотя бы одно отношение µ ∈ M, которое содержит пару (P 1 , P 2 ). Таким образом, искомое отношение сильной эквивалентности на множестве всех процессов мы определяем как объединение всех отношений из M. Данное отношение обозначается символом ∼. Нетрудно доказать, что • ∼ ∈ M, и • ∼ является отношением эквивалентности, т.к. – рефлексивность ∼ следует из того, что диагональное отношение принадлежит M, – симметричность ∼ следует из того, что если µ ∈ M, то µ −1 ∈ M – транзитивность ∼ следует из того, что если µ 1 ∈ M и µ 2 ∈ M, то µ 1 ◦ µ 2 ∈ M. Если процессы P 1 и P 2 сильно эквивалентны, то этот факт обозначается знакосочетанием P 1 ∼ P 2 69 Нетрудно доказать, что если процессы P 1 и P 2 сильно экви- валентны, то они трассово эквивалентны. Для иллюстрации понятия сильной эквивалентности рассмот- рим пару примеров. 1. Процессы ? A A A A U a b c A A A U ? ? a a b c (4.13) не являются сильно эквивалентными, так как они не явля- ются трассово эквивалентными 2. Процессы ? A A A A U a b b A A A U ? ? a a b b являются сильно эквивалентными. 70 4.4 Критерии сильной эквивалентности 4.4.1 Логический критерий сильной эквивалент- ности Обозначим символом F m множество формул, определяемое сле- дующим образом. • Символы > и ⊥ являются формулами. • Если ϕ – формула, то ¬ϕ тоже формула. • Если ϕ и ψ – формулы, то ϕ ∧ ψ тоже формула. • Если ϕ – формула и a ∈ Act, то haiϕ тоже формула. Пусть заданы процесс P и формула ϕ ∈ F m. Значение фор- мулы ϕ на процессе P представляет собой элемент P (ϕ) множе- ства {0, 1}, определяемый следующим образом. • P (>) = 1, P (⊥) = 0 • P (¬ϕ) = 1 − P (ϕ) • P (ϕ ∧ ψ) = P (ϕ) · P (ψ) • P (haiϕ) = 1, если существует процесс P 0 : P - a P 0 , P 0 (ϕ) = 1 0, в противном случае Теория процесса P – это совокупность T h(P ) формул, опреде- ляемая следующим образом: T h(P ) = {ϕ ∈ F m | P (ϕ) = 1} Теорема 1. Пусть процессы P 1 и P 2 конечны. Тогда P 1 ∼ P 2 ⇔ T h(P 1 ) = T h(P 2 ) Доказательство. Импликация “⇒” доказывается индукцией по структуре фор- мулы ϕ. 71 Докажем импликацию “⇐”. Пусть имеет место равенство T h(P 1 ) = T h(P 2 ) (4.14) Обозначим символом µ бинарное отношение на множестве всех процессов, которое состоит из всех пар процессов с одинаковыми теориями, т.е. µ def = {(P 1 , P 2 ) | T h(P 1 ) = T h(P 2 )} Докажем, что µ удовлетворяет определению сильной экви- валентности. Пусть это не так, т.е., например, для некоторого a ∈ Act (a) существует процесс P 0 1 , такой, что P 1 - a P 0 1 (b) но не существует процесса P 0 2 , такого, что P 2 - a P 0 2 (4.15) и T h(P 0 1 ) = T h(P 0 2 ). Условие (b) может иметь место в двух ситуациях: 1. не существует процесса P 0 2 , для которого верно (4.15) 2. существует процесс P 0 2 , для которого верно (4.15), но для каждого такого процесса T h(P 0 1 ) 6= T h(P 0 2 ) Докажем, что в обоих ситуациях существует формула ϕ, удовле- творяющая условию P 1 (ϕ) = 1, P 2 (ϕ) = 0 что будет противоречить предположению (4.14). 1. Если имеет место первая ситуация, то в качестве ϕ можно взять формулу hai>. 72 2. Если имеет место вторая ситуация, то пусть список всех таких процессов P 0 2 , для которых верно (4.15), имеет вид P 0 2,1 , . . . , P 0 2,n По предположению, для каждого i = 1, . . . , n имеет место неравенство T h(P 0 1 ) 6= T h(P 0 2,i ) т.е. для каждого i = 1, . . . , n существует формула ϕ i , такая, что P 0 1 (ϕ i ) = 1, P 0 2,i (ϕ i ) = 0 В этой ситуации в качестве искомой формулы ϕ можно взять формулу hai(ϕ 1 ∧ . . . ∧ ϕ n ). Например, пусть P 1 и P 2 – процессы, изображённые на ри- сунке (4.13). Как было сказано выше, эти процессы не являются сильно эквивалентными. В качестве обоснования утверждения P 1 6∼ P 2 можно, например, предъявить формулу ϕ def = hai(hbi> ∧ hci>) Нетрудно доказать, что P 1 (ϕ) = 1 и P 2 (ϕ) = 0. Представляет интерес задача нахождения по двум заданным процессам P 1 и P 2 списка формул ϕ 1 , . . . , ϕ n как можно меньшего размера, таких, что P 1 ∼ P 2 тогда и только тогда, когда ∀ i = 1, . . . , n P 1 (ϕ i ) = P 2 (ϕ i ) 4.4.2 Критерий сильной эквивалентности, ос- нованный на понятии бимоделирования Теорема 2. Пусть заданы два процесса P i = (S i , s 0 i , R i ) (i = 1, 2) 73 P 1 ∼ P 2 тогда и только тогда, когда существует отношение µ ⊆ S 1 × S 2 удовлетворяющее следующим условиям. 0. (s 0 1 , s 0 2 ) ∈ µ. 1. Для каждой пары (s 1 , s 2 ) ∈ µ и каждого перехода из R 1 вида s 1 - a s 0 1 существует переход из R 2 вида s 2 - a s 0 2 такой, что (s 0 1 , s 0 2 ) ∈ µ. 2. Для каждой пары (s 1 , s 2 ) ∈ µ и каждого перехода из R 2 вида s 2 - a s 0 2 существует переход из R 1 вида s 1 - a s 0 1 такой, что (s 0 1 , s 0 2 ) ∈ µ. Отношение µ, удовлетворяющее данным условиям, называется бимоделированием (БМ) между P 1 и P 2 4.5 Алгебраические свойства сильной эк- вивалентности Теорема 3. Сильная эквивалентность является конгруэнцией, т.е. если P 1 ∼ P 2 , то • для каждого a ∈ Act a.P 1 ∼ a.P 2 • для каждого процесса P P 1 + P ∼ P 2 + P 74 • для каждого процесса P P 1 |P ∼ P 2 |P • для каждого L ⊆ N ames P 1 \ L ∼ P 2 \ L • для каждого переименования f P 1 [f ] ∼ P 2 [f ] Доказательство. Как было установлено в параграфе 4.4.2, соотношение 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 1 , s), (s 2 , s)) | (s 1 , s 2 ) ∈ µ, q ∈ S} является БМ между P 1 |P и P 2 |P . • Отношение µ является БМ 75 – между P 1 \ L и P 2 \ L, и – между P 1 [f ] и (P 2 [f ]. Теорема 4. Для каждого процесса P = (S, s 0 , R) имеют место следующие свойства. 1. P + 0 ∼ P 2. P + P ∼ P Доказательство. 1. Обозначим символом символом s 0 0 начальное состояние про- цесса P + 0. БМ между P + 0 и P имеет вид {(s 0 0 , s 0 )} ∪ Id S 2. Согласно определению операции +, процессы в левой части доказываемого соотношения следует рассматривать как две дизъюнктные изоморфные копии процесса P вида P (i) = (S (i) , s 0 (i) , R (i) ) (i = 1, 2) где S (i) = {s (i) | s ∈ S}. Обозначим символом символом s 0 0 начальное состояние про- цесса P + P . БМ между P + P и P имеет вид {(s 0 0 , s 0 )} ∪ {(s (i) , s) | s ∈ S, i = 1, 2} Ниже для • каждого процесса P = (S, s 0 , R), и • каждого состояния s ∈ S 76 мы будем использовать знакосочетание P (s) для обозначения процесса (S, s, R) который отличается от P только начальным состоянием. Теорема 5. Пусть P = (S, s 0 , R) – некоторый процесс, и совокупность всех выходящих из s 0 переходов имеет вид { s 0 - a i s i | i = 1, . . . , n} Тогда P ∼ a 1 .P 1 + . . . + a n .P n (4.16) где для каждого i = 1, . . . , n P i def = P (s i ) def = (S, s i , R) Доказательство. Для построения БМ, доказывающего соотношение (4.16), мы заменим все процессы P i в его правой части на их дизъюнктные копии, т.е. будем считать, что для каждого i = 1, . . . , n процесс P i имеет вид P i = (S (i) , s i (i) , R (i) ) и для каждого i = 1, . . . , n соответствующая биекция между S и S (i) сопоставляет каждому состоянию s ∈ S состояние, обознача- емое символом s (i) Таким образом, можно считать, что каждое из слагаемых a i .P i в правой части (4.16) имеет вид s 0 (i) - a i ' & $ % P i s i (i) и множества состояний этих слагаемых попарно не пересекаются. Согласно определению операции +, правая часть (4.16) имеет вид 77 s 0 0 * H H H H H H H H j a 1 a n ' & $ % P 1 s 1 (1) ' & $ % P n s n (n) БМ между левой и правой частями (4.16) имеет вид {(s 0 , s 0 0 )} ∪ {(s, s (i) ) | s ∈ S, i = 1, . . . , n} Теорема 6 (теорема о разложении). Пусть P – процесс вида P = P 1 | . . . | P n (4.17) где для каждого i ∈ {1, . . . , n} процесс P i имеет вид P i = n i X j=1 a ij . P ij (4.18) Тогда P сильно эквивалентен сумме 1. всех процессов вида a ij P 1 | . . . | P i−1 | P ij | P i+1 | . . . | P n (4.19) 2. и всех процессов вида τ. P 1 | . . . | P i−1 | P ik | P i+1 | . . . . . . | P j−1 | P jl | P j+1 | . . . | P n ! (4.20) где 1 ≤ i < j ≤ n, a ik , a jl 6= τ , и a ik = a jl 78 Доказательство. По теореме 5, P сильно эквивалентен сумме, каждое слагае- мое в которой соответствует некоторому переходу, выходящему из начального состояния s 0 процесса P : для каждого перехода в P вида s 0 - a s эта сумма содержит слагаемое a.P (s). Согласно (4.18), для каждого i = 1, . . . , n процесс P i имеет вид s 0 i * H H H H H H H H j a i1 a in i ' & $ % P i1 s 0 i1 ' & $ % P in i s 0 in i где s 0 i , s 0 i1 , . . . , s 0 in i – начальные состояния процессов P i , P i1 , . . . , P in i соответственно. Обозначим • символом S i множество состояний процесса P i , и • символом S ij (где j = 1, . . . , n i ) – множество состояний про- цесса P ij Мы можем считать, что S i является дизъюнктным объединением S i = {s 0 i } ∪ S i1 ∪ . . . ∪ S in i (4.21) Согласно описанию процесса вида (4.17), которое приведено в пункте 2 параграфа 3.7, можно считать, что компоненты про- цесса P имеют следующий вид. 79 • Множество состояний процесса P имеет вид S 1 × . . . × S n (4.22) • Начальным состоянием s 0 процесса P является список (s 0 1 , . . . , s 0 n ) • Переходы процесса P , выходящие из его начального состо- яния, имеют следующий вид. – Переходы вида s 0 - a ij (s 0 1 , . . . , s 0 i−1 , s 0 ij , s 0 i+1 , . . . , s 0 n ) (4.23) – Переходы вида s 0 - τ s 0 1 , . . . , s 0 i−1 , s 0 ik , s 0 i+1 , . . . . . . s 0 j−1 , s 0 jl , s 0 j+1 , . . . , s 0 n ! (4.24) где 1 ≤ i < j ≤ n, a ik , a jl 6= τ , и a ik = a jl Таким образом, множество переходов процесса P , выходящих из s 0 , находится во взаимно однозначном соответствии с мно- жеством слагаемых вида (4.19) и (4.20). Для доказательства теоремы 6 достаточно доказать, что • Для каждого i = 1, . . . , n, и каждого j = 1, . . . , n i имеет место эквивалентность P (s 0 1 , . . . , s 0 i−1 , s 0 ij , s 0 i+1 , . . . , s 0 n ) ∼ ∼ P 1 | . . . | P i−1 | P ij | P i+1 | . . . | P n (4.25) • Для – любых i, j, таких, что 1 ≤ j < j ≤ n, и – любых k = 1, . . . , n i , l = 1, . . . , n j имеет место эквивалентность P s 0 1 , . . . , s 0 i−1 , s 0 ik , s 0 i+1 , . . . . . . s 0 j−1 , s 0 jl , s 0 j+1 , . . . , s 0 n ! ∼ ∼ P 1 | . . . | P i−1 | P ik | P i+1 | . . . . . . | P j−1 | P jl | P j+1 | . . . | P n ! (4.26) 80 Мы докажем лишь эквивалентность (4.25) (эквивалентность (4.26) доказывается аналогично). Множество состояний процесса P 1 | . . . | P i−1 | P ij | P i+1 | . . . | P n (4.27) имеет вид S 1 × . . . × S i−1 × S ij × S i+1 × . . . × S n (4.28) Из (4.21) следует, что S ij ⊆ S i , т.е. множество (4.28) является подмножеством множества (4.22) состояний процесса P (s 0 1 , . . . , s 0 i−1 , s 0 ij , s 0 i+1 , . . . , s 0 n ) (4.29) Определим искомое БМ µ между процессами (4.27) и (4.29) как диагональное отношение µ def = {(s, s) | s ∈ (4.28)} Очевидно, что • пара начальных состояний процессов (4.27) и (4.29) при- надлежит µ, • каждый переход процесса (4.27) является также переходом процесса (4.29), и • если начало некоторого перехода процесса (4.29) принад- лежит подмножеству (4.28), то конец этого перехода тоже принадлежит подмножеству (4.28) (для обоснования этого утверждения отметим, что все переходы в P i с началом в S ij имеют конец тоже в S ij ). Таким образом, µ является БМ, и это доказывает эквивалент- ность (4.25). Следующая теорема является усилением теоремы 6. Для её формулировки мы будем использовать следующее обозначение. Если f – произвольное переименование, то тот же символ f обо- значает функцию вида f : Act → Act определяемую следующим образом. 81 |