Глобальные свойства системы

Глобальные свойства системы -- это предикаты, которые бывают двух видов:

• стабильные предикаты
• нестабильные предикаты

Стабильные предикаты можно формализовать следующим образом:

Пусть G и H согласованные срезы, будем говорить, что G <= H, если H достижимо из G. Тогда B будет стабильным предикатом тогда и только тогда, когда ∀ G, H: G <= H : B(G) ⇒ B(H), т.е В стабильный предикат, если однажды дав true, он остается true навсегда.

Примеры стабильных предикатов: deadlock, termination, loss of token.

Нестабильные предикаты это, соответственно, предикаты, которые не удовлетворяют условию стабильного предиката.