3状態相互排他アルゴリズムの安定時間の下限について

摘要

The three state mutual exclusion algorithm is the first self-stabilizing algorithm which was proposed by E. W. Dijkstra. Although many years have elapsed since then, no accurate analysis has been conducted on its stabilization time. In this paper, we analyze the stabilization time from the result obtained by model checking. As a result, we obtain closed-form formulas for the lower bound on the stabilization time.%3状態相互排他アルゴリズムは，ダイクストラによって提唱された最初の自己安定アルゴリズムの一つである.その正しさについてはいくつもの研究で証明されているが，安定時間に関しては精度の高い解析がなされてこなかった.本研究では，モデル検査によって得られた知見から安定時間に関する解析を試みる.結果として安定時間の下限を表す式が得られた.