Using Temporal Subsumption for Developing Efficient Error-Detecting Distributed Algorithms

Distributed algorithms can use executable assertions derived from program verification to detect errors at run-time. However, a complete verification proof outline contains a large number of assertions, and embedding all of them into the program to be checked at run-time would make error-detection very inefficient. The technique of temporal subsumption examines the dependencies between the individual assertions along program execution paths. In contrast to classical subsumption, where all logical expressions to be examined are true simultaneously, an assertion need only be true when the corresponding statement in the distributed program has been executed. Thus, temporal subsumption based on the set of assertions derived from a verification proof and in combination with the set of all legal states in the system, allows for the removal of (partial) assertions along execution sequences. We assume a fault model of Byzantine (malicious) behavior, and therefore an individual process cannot c..