自己安定化理論の「合成」に欠けたピースを探して

In Search of a Compositional Theory of Self-Stabilization

自己安定化システムの合成に関する最近の研究を調べても、2000年代初頭から本質的な進展は見つからなかった。そこで、リトライストームのTLA+モデルを具体例に、パラメトリックなassume-guarantee契約とsmall gain定理を適用。しかし、メモリレスな入出力関係ではバックログを表現できず、2つのキュー間の結合とメモリを分けて考える必要があることが判明。線形安定性解析により、結合を無視したsmall gainの判定は誤りで、実際の系は不安定であることを示す。