PROVING FINITE-STATE DISTRIBUTED PROGRAMS CORRECT.

Proving the correctness of a distributed program, analogous to proving the correctness of a sequential program, involves two parts: proof of partial correctness - the program computes its intended function - and proof of deadlock freedom - the program does not terminate abnormally. The author refers to these two aspects of the problem as 'verification' and 'synchronization analysis' respectively. The correctness problem is in general undecidable. Consequently, the author limits his attention to distributed programs that can be modeled (algebraically) as networks of Finite-State Processes (FSPs). Regarding the Synchronization Analysis Problem (SAP), he analyzes its complexity and provides an algorithm for its solution. The SAP is computationally difficult. The author identifies a significant subclass of programs for which it can be solved in linear time by divide-and-conquer. Regarding verification, he analyzes the complexity of testing various notions of equivalence of FSPs. The resulting algorithms enable one to check that a program meets its specification. The author illustrates his procedures for verification and synchronization analysis by application to network protocols.