Application of three-valued logic for distributed termination detection (Q1207442)

A three-valued logic method is used as a tool to design and proof the correctness of an algorithm for distributed termination detection. \textit{E. W. Dijkstra, W. H. J. Feigen} and \textit{A. J. M. von Gasteren} [NATO ASI Ser., Ser. F 14, 507-512 (1985; Zbl 0566.68025)] proposed an algorithm that was based on the assumption of zero delay in the communication channels, where a token and a two-color rule were used to detect termination. Similar to Dijkstra's algorithm we have developed an algorithm for distributed systems that does not rely on any clock synchronization scheme. Moreover, it uses a communication channel model that is non-FIFO with finite delay message transmission. This algorithm uses two auxiliary message types, called token and control messages, in addition to the regular messages that are used for computation. Auxiliary messages travel in a Hamiltonian path, however, regular messages travel in any arbitrary path between the sender and receiver of the message. For developing and proving the termination detection algorithm, multiple tokens and control messages are used together with a three-valued logic scheme with the values 0, 1/2 and 1 representing colors black, gray and white, respectively.