Reasoning About Uncertainty in Fault-Tolerant Distributed Systems. Revision

摘要

A temporal logic is presented for reasoning about uncertainty in distributed systems that contain both probabilistic and nondeterministic transitions. Probabilistic transitions model randomness in the processes of the system and in the fault model. Nondeterministic transitions model lack of information about the true faulty behavior of the system and the progress of the computation. The naturalness of this approach is demonstrated by offering new analyses and solutions to some classic fault-tolerant distributed computing problems, namely the coordinated attack problem and authenticated Byzantine agreement problem. Keywords: Safety properties, Knowledge, Belief, Distributed systems, Nondeterministic systems, Probabilistic system, Liveness, Byzantine agreement, Coordinated attack. (jhd)