Local and Temporal Predicates in Distributed Systems

The definitions of the predicates Possibly ɸ and Definitely ɸ, where ɸ is a global predicate of a distributed computation, lead to the definitions of two predicate transformers P and D. We show that P plays the same role with respect to time as the predicate transformers K_i in knowledge theory play with respect to space. Pursuing this analogy, we prove that local predicates are exactly the fixed points of the K_i's while the stable predicates are the fixed points of P. In terms of the predicate transformers P and D, we define a new class of predicates that we call observer-independent predicates and for which the detection of Possibly ɸ and Definitely ɸ is quite easy. Finally, we establish a temporal counterpart to the knowledge change theorem of Chandy and Misra which formally proves that the global view of a distributed system provided by its various observations does not differ too much from its truth behavior.