Formal analysis of control and termination of distributed computation in weaker spaces

Abstract

The control and termination detection of a distributed computation involving large-scale distributed database is difficult in the presence of concurrency, random network delays, and varying reliability of computing nodes. The formal modeling and analysis of controllability as well as termination detection of such systems are required to design reliable and dependable systems involving distributed computations and distributed datasets. The modeling and analysis of distributed computation can be performed by using combinatorial topology by forming simplexes, which imposes a set of relatively rigid geometric structures. This article proposes the modeling and analysis of observable and controllable distributed computation in weaker topological spaces. The proposed model enhances structural flexibility in metrized monotone spaces. The metrizability of the space and convergence property of the computation are analyzed. Axiomatic termination detection and fault mode analysis are formulated. A distributed algorithm is designed to observe and to determine varying control states of computation. The article includes a detailed comparative analysis of a set of models in the domain.

Keywords

• distributed computing
• termination detection
• monotone
• topology
• lattice
• stable predicate