Самостабилизация: различия между версиями

Многие самостабилизирующиеся протоколы имеют многослойную конструкцию. Обозначим за <math>\{ A_i \}^{m - 1}_{i = 0}</math> множество программ, обладающих следующим свойством: для каждой переменной состояния x, если программа <math>A_i</math> записывает x, то ни одна программа <math>A_j</math> для j > i не записывает x. Программы в <math>\{ A_j \}^{m - 1}_{j = i + 1}</math> могут читать переменные, записанные <math>A_i</math>, то есть использовать выходное значение <math>A_i</math> в качестве входа. Справедливая композиция программ B и C, записываемая в виде B [] C, предполагает справедливое планирование шагов B и C. Обозначим за <math>X_j</math> множество переменных, прочитанных <math>A_j</math> и, возможно, записанных <math>\{ A_i \}^{m - 1}_{i = 0}</math>.