以知識邏輯驗算兩個分散式計算問題的訊息複雜度下限

Abstract

knowledge是一種modal logic，它是Halpern等人於1984年所提出，並且它提供一套統一的架構和工具方便吾人使用於不可解問題的證明，knowledge自此被當成分析的工具，廣泛地使用於分散式環境下不可解問題的證明。 本論文中，使用knowledge去驗算兩個分散式計算問題的訊息複雜度下限，驗算的問題是resynchronization problem以及infimum computation problem。Gerard Tel以組合數學方式證明任何可以解決這兩個問題的演算法都至少需要使用n-1個訊息，其中n是所有程序的總數。本論文中使用knowledge的架構驗算這兩個分散式計算問題的訊息複雜度下限，驗算結果顯示n-1的確都是這兩個問題的下限。本論文中的驗算再次顯示knowledge的確為一強大的分析工具。

Knowledge is a kind of modal logic. It was proposed by Halpern et al. in 1984, and provides a unified framework and a set of tools for formal proofs about impossibility results. Knowledge has been extensively used since then as an analytical tool to prove the impossibility result of the problem in distributed environments. In this thesis, we use knowledge to verify message complexity lower bounds of two distributed computing problems. The problems are the resynchronization problem and the infimum computation problem. Gerard Tel provided two combinatorial proofs for these problems and showed that any algorithm that solves one of these problems needs at least n-1 messages, where n is the number of processes. We use knowledge’s framework to verify message complexity lower bounds of the two problems. The result of our verification shows that n-1 is indeed a lower bound of each problem. The result attests the common belief in the field of distributed computing that knowledge is really a powerful analytical tool.