ライブネス
安全性と有効性の区別は、 P ( t ) {\displaystyle P(t)} という述語によって形式的に確立することができる。 ここで、 t {\displaystyle t} は時間を意味する。 t 0 {\displaystyle t_{0}} をlivenessとsafetyの特性が評価される出発点となる瞬間とする。以下の例では、 x {\displaystyle x} をデッドロックフリーであることを保証したいプロセス(またはスレッド)とする。
安全性: ∀ t ≥ t 0 : P ( t ) = False . {\displaystyle \forall t\geq t_{0}:P(t)={\textrm {False}}.}
事例: P ( t ) {\displaystyle P(t)} は " x {\displaystyle x} が時間 t {\displaystyle t} でデッドロックの状態にある"ことを意味する。
ライブネス: ∀ t 1 ≥ t 0 , ∃ t ≥ t 1 , t < ∞ : P ( t ) = True . {\displaystyle \forall t_{1}\geq t_{0},\exists t\geq t_{1},t<\infty :P(t)={\textrm {True}}.}
事例: P ( t ) {\displaystyle P(t)} は " x {\displaystyle x} が時間 t {\displaystyle t} で待機、停止する"ことを意味する。