Distributed event algebras

摘要

A general model, the Distributed Event Algebra or D-algebra, for distributed computation is developed, generalizing Lynch's Event State Algebras. Such models are essential to the construction of effective and convincing proofs of distributed algorithms. D-algebras are designed to allow hierarchical proof techniques. Two notions of mapping between D-algebras are defined. One operates on the level of uninterpreted actions, the other on the level of actions with interpretations as operators on states. A hierarchical proof of correctness using D-algebras consists of the construction of a series of D-algebras, from high level to low level, connected by a series of correctness preserving maps, and a proof of the correctness of the high level D-algebra. D-algebras also incorporate the notion of execution of a system as a partially ordered set of actions, thus reducing overspecification of executions. This results in the state history of a system under a particular execution being modeled as a directed graph, thus capturing all possible state sequences in a single structure.