Изменения

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

Стабильные предикаты можно формализовать следующим образом:Пусть G и H согласованные срезы, будем говоритьГоворить "предикат сейчас верен" или "предикат сейчас неверен" некорректно, потому что G <= H, если H достижимо из Gнет "сейчас". Тогда B стабильный предикат тогда и тогда тогда, когда ∀ G, H: G <= H : B(G) ⇒ B(H), т.е В стабильный предикатМожно говорить "существует/не существует согласованный срез", но если однажды дав trueу нас система ещё работает, то остается true навсегда"не существует" мы можем заявить лишь на каком-то префиксе срезов системе.

{{Определение|definition=Предикат $P$ является '''стабильным''', если для любых согласованных срезов $G \le H$ из $P(G)$ следует $P(H)$.}}Примеры стабильных предикатов: deadlock, terminationзавершение работы, потеря токена в алгоритм передаче токена по кругу. Такие предикаты можно найти наивно: снимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, получилась ли истина.Если да — то был верен, если нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени"). Также в некоторых случаях их можно искать по-другому: как нестабильные предикаты (тогда можно найти наименьший согласованный срез), [[диффундирующие вычисления]], [[Локально стабильный предикат|локально-стабильные предикаты]]. {{Определение|definition=Предикат $P$ является '''нестабильным''', если он не является стабильным.}}Нестабильные предикаты сложно искать, потому что может быть множество разных согласованных срезов, которые не вкладываются друг в друга.Поэтому просто снять несколько согласованных срезов не поможет: мы можем не попасть в нужный.{{Определение|definition=Предикат $P$ является '''локальным''', если он зависит только от состояния одного конкретного процесса.Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).}}Если у нас нестабильный предикат, но являющийся дизъюнкцией локальных предикатов, то надо просто попросить каждый процесс отследить свой локальный предикат на протяжении некоторого интервала и узнать, loss of tokenвыполнялся ли там предикат хотя бы у одного.