強い公平性と弱い公平性

強い公平性
実行過程において、ある時点以降、あるスレッドが無限回動作可能状態であるにも関わらず、一度も動作しない時、その実行過程は強い公平性(strong fairness)を満たさないという。
スレッド i が動作可能であることを　ei で、動作することを ri で表せば、強い公平性を満たすことはLTLにより以下で表せる。
( []<> e1 -> []<> r1) ∧ ... ∧ ( []<> en -> []<> rn )

弱い公平性
実行過程において、ある時点以降、あるスレッドが常に動作可能状態であるにも関わらず、一度も動作しない時、その実行過程は弱い公平性(weak fairness)を満たさないという。
スレッド i が動作可能であることを　ei で、動作することを ri で表せば、弱い公平性を満たすことはLTLにより以下で表せる。
[]<> ( e1 -> r1) ∧ ... ∧ []<> ( en -> rn )