Изменения

'''Слабый конъюнктивный предикат (WCP)''' – — [[Глобальные свойства системы|предикат]], удовлетворяющий двум условиям:* имеет имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса; .{{Определение|definition=* его истинность есть истинность Слабый конъюнктивный предикат $P$ '''истинен''', если он истинен на хотя бы на одном согласованном срезе}}Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов.

'''Локальный предикат''' – предикат по состоянию одного процессаБолее того: некоторые сложные нелокальные предикаты тоже можно так записать. Например, если у процесса есть состояние (переменная) предикат на булевских переменных из разных процессов: $x= y$, то локальным предикатом может быть можно записать формулу: $(x < = 0\land y = 0) \lor (x = 1 \land y = 1)$.

Используется для нежелательных предикатов'''Теорема''': если слабый конъюктивный предикат верен хоть на одном согласованном срезе, напримерто в множестве согласованных срезов с верным предикатом существует наименьший элемент (т.е. который вкладывается во все остальные). Это следует из того, классическая проблема взаимного исключениячто пересечение согласованных срезов является согласованным срезом: пересечение всех срезов с верными предикатом будет срезом и, более того, в каждом процессе граница этого среза включается хотя бы в один из исходных, следовательно, на границе в каждом процессе соответствующий локальный предикат будет верен.

Пример Например, классическую проблема взаимного исключения для двух процессов: локальный предикат "процесс в критической секции".Если есть срез, в котором два процесса в критической секции, то всё плохо.А если такого нет, то любые две критические секции упорядочены. Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.