Изменения

'''Глобальные свойства системы''' -- — это предикатыот согласованных срезов системы (состояния процессов плюс сообщения в пути), которые бывают двух видов:* стабильные предикаты ;* нестабильные предикаты.

Пусть $G $ и $H $ — согласованные срезы, будем . Будем говорить, что $G <= \le H$, если H достижимо из G(т. Тогда B будет е. $G \subseteq H$ в смысле событий).{{Определение|definition=Предикат $P$ является '''стабильным предикатом тогда и только тогда''', когда ∀ если для любых согласованных срезов $G, \le H: G <= H : B$ из $P(G) ⇒ B$ следует $P(H), т$.е В стабильный предикат}}Примеры стабильных предикатов: deadlock, если однажды дав trueзавершение работы, он остается true навсегдапотеря токена в алгоритм передаче токена по кругу.

Примеры стабильных предикатовТакие предикаты можно найти наивно: deadlockснимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, terminationполучилась ли истина.Если да — то был верен, loss of tokenесли нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени").

{{Определение|definition=Предикат $P$ является '''нестабильным''', если он не является стабильным.}}Нестабильные предикаты этосложно искать, соответственно, предикатыпотому что может быть множество разных согласованных срезов, которые не удовлетворяют условию стабильного предикатавкладываются друг в друга.Поэтому просто снять несколько согласованных срезов не поможет: мы можем не попасть в нужный.{{Определение|definition=Предикат $P$ является '''локальным''', если он зависит только от состояния одного конкретного процесса.}}Если у нас нестабильный предикат, но являющийся дизъюнкцией локальных предикатов, то надо просто попросить каждый процесс отследить свой локальный предикат на протяжении некоторого интервала и узнать, выполнялся ли там предикат хотя бы у одного.