On distributed convergence
by
Norman R. Howes
Institute for Defense Analyses

In [1] the author introduced a more general temporal logic (TLB) for reasoning about the behavior of computer systems than the Temporal Logic of Actions (TLA) [2]. TLB allows us to prove whether computer system behaviors converge or cluster to particular states in state space. TLB is to TLA as calculus is to algebra in that it introduces the concept of a limit by topologizing state space and introducing appropriate behavioral operators to characterize convergent and clustering behaviors. In [1] behaviors are defined, as in TLA, as sequences of states, and computer systems are characterized by their set of possible behaviors. TLB eliminates some of the logical difficulties of TLA by being based on the axioms of Set Theory rather than the 19 proof rules introduced in [2]. In [1] it is shown that these 19 proof rules contain three rules that are equivalent to the Axiom of Infinity in Set Theory, and that Lamport's other proof rules are easily derived from the axioms of Set Theory.

Lamport [2] seems to indicate that TLA can be used to reason about distributed systems where concurrent processes execute in geographically distributed address spaces. We show that in general this is false. We also show that it is possible to extend TLB to include the distributed case, but to do this, behaviors must be defined as nets rather than sequences. Of primary interest is the observation that the naïve concept of distributed algorithms converging to particular states in a distributed state space is something different than the ordinary convergence of nets in a general topological space. There is a parallel between distributed convergence (and clustering) and the ordinary convergence (or clustering) of nets in product spaces that allows most of the theorems about the convergence of nets in product spaces to be translated into results about distributed behaviors. But in the case of clustering, distributed clustering appears to be much stronger than the ordinary clustering of nets in product spaces, showing that distributed convergence theory is something quite different from the ordinary theory of convergence of nets in product spaces. Distributed TLB (DTLB) is an application of distributed convergence that is important enough to justify this new concept. The author is not aware of any other applications of distributed convergence at the time, but wonders if it might be applicable to the modeling of other geographically distributed phenomena.

[1] N. Howes, The Temporal Logic of Behaviors, to appear.

[2] L. Lamport, The Temporal Logic of Actions, ACM Trans. on Programming Languages, vol. 16, no. 3, May 1994.

Date received: February 21, 2003