A relativistic temporal algebra for efficient design of distributed systems

Adequate methods for checking the specification and design of distributed systems must allow for reasoning about asynchronous activities; efficient methods must perform the reasoning in polynomial time. This paper lays the groundwork for such an efficient deductive system by providing a very general temporal relation algebra that can be used by constraint propagation techniques to perform the required reasoning. Major choices exist when selecting an appropriate temporal model: discrete/dense, linear/nonlinear, and point/interval. James Allen and others have indicated the possible atomic relations between two intervals for the dense-linear-interval model, while Anger, Ladkin, and Rodriguez have shown those needed for a dense-branching-interval model. Rodriguez and Anger further developed a dense-relativistic-interval model based on Lamport'sprecede andcan affect arrows, determining a large number of atomic relations. This paper shows that those same atomic relations are exactly the correct ones for intervals in dense relativistic space-time if intervals are taken as pairs of points (E _s ,E _f ) in space-time such that it is possible to move fromE _s toE _f at less than the speed of light. The relations are defined and named consistently with the earlier work of Rodriguez and Anger, and the relationship between the two models is pursued. The relevance of the results to the verification of distributed specifications and algorithms is discussed.