Distributed event algebras (Q1191023)

Distributed event algebra or \(D\)-algebra is a general model for distributed computation is introduced. It generalizes Lynch's Event State Algebra. It consists of a set of nodes, a set of states and a set of partial operations from the global state space to itself. Each operation has a locality (the node performing the operation), and certain pairs of operations are said to be serial. That is, their order of execution is of importance. \(D\)-algebras come with two notions of mapping between \(D\)- algebras. One (interpretations) operates on the level of actions (mapping executions to executions). The other (possibility maps) operates on both the levels of actions and states (mapping each state of one system to a set of possible states of another). \(D\)-algebras allow hierarchical proof techniques. The proof of correctness consists 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.