Abstract In distributed network algorithms, network flooding is considered one of the simplest and most fundamental algorithms. This research specifies the basic synchronous memory-less network flooding algorithm where nodes on the network don’t have memory, for any fixed size of network, in Linear Temporal Logic. The specification can be customized to any single network topology or class of topologies. A specification of the termination problem is formulated and used to compare different topologies for earlier termination. This paper gives a worked example of one topology resulting in earlier termination than another, for which we perform a formal verification using the model checker NuSMV.

References

[1] Attiya H. and Welch J., Distributed Computing: Fundamentals, Simulations, and Advanced Topics, John Wiley and Sons, 2004.

[2] Cardelli L. and Gordon A., “Mobile Ambients,” Theoretical Computer Science, vol. 240, no. 1, pp. 177-213, 2000.

[3] Comer D. and Droms R., Computer Networks and Internets, Prentice-Hall, 2003.

[4] Dwork C., Peleg D., Pippenger N., and Upfal E., “Fault Tolerance in Networks of Bounded Degree,” Society for Industrial and Applied Mathematics, vol. 17, no. 5, pp. 975-988, 1988.

[5] Fiat A. and Saia J., “Censorship resistant peer-to- Peer Content Addressable Networks,” in Proceedings of the 30th Annual ACM-SIAM Symposium on Discrete Algorithm, USA, pp. 94- 103, 2002.

[6] Fiat A. and Saia J., “Censorship Resistant Peer- To-Peer Networks,” Theory of Computing, vol. 3, no. 1, pp.1-23, 2007.

[7] Gkantsidis C., Mihail M., and Saberi A., “Random Walks in Peer-To-Peer Networks: Algorithms and Evaluation,” Performance Evaluation, vol. 63, no. 3, pp. 241-263, 2006.

[8] Hillel K. and Shachnai H., “Partial Information Spreading with Application to Distributed Maximum Coverage,” in Proceedings of the 29th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, New York, pp. 161- 170, 2010.

[9] Hoare C., Communicating Sequential Processes, Prentice Hall, 1985.

[10] Hoory S., Linial N., and Wigderson A., “Expander Graphs and their Applications,” Bulletin of the AMS, vol. 43, no. 04, pp. 439-562, 2006.

[11] Hussak W., “The Serializability Problem for A Temporal Logic of Transaction Queries,” Journal of Applied Non-Classical Logics, vol. 18, no. 1, pp. 67-78, 2008.

[12] Khan S. and Waheed A., “Modeling and Formal Verification of IMPP,” The International Arab Journal of Information Technology, vol. 2, no. 3, pp. 192-198, 2005.

[13] King V., Saia J., Sanwalani V., and Vee E., “Towards Secure And Scalable Computation in Peer-To-Peer Networks,” in Proceedings of 47th Annual IEEE Symposium on Foundations of Computer Science, Berkeley, pp.87-98, 2006.

[14] Kutten S., Pandurangan G., Peleg D., Robinson P., and Trehan A., “On The Complexity of Universal Leader Election,” Journal of the ACM, vol. 62, no. 1, pp. 1-27, 2015.

[15] Kutten S., Pandurangan G., Peleg D., Robinson P., and Trehan A., “Sublinear Bounds for Randomized Leader Election,” Theoretical Computer Science, vol. 561, pp. 134-143, 2015.

[16] Law C. and Siu K., “Distributed Construction of Random Expander Networks,” in Proceedings of 20nd Annual Joint Conference of the IEEE 2 2 2 2 2 20 1 2 3 42 2 2 2 20 1 2 3 42 2 2 2 20 1 2 3 42 2 2 2 20 1 2 3 42 2 2 2 20 1 2 3 4 ( ) viMMMMM M M M M M M M M M M M M M M M M M M M M                                                1 1 2 2 111110 1 2 3 4222220 1 2 3 4 ( ) ( ) (( ) ( )) vvm i m i MMMMM MMMMM                   F 1vi 2vi 874 The International Arab Journal of Information Technology, Vol. 17, No. 6, November 2020 Computer and Communications Societies, San Francisco, pp. 2133-2143, 2003.

[17] Lynch N. and Tuttle M., “Hierarchical Correctness Proofs for Distributed Algorithms,” in Proceedings of the 6th Annual ACM Symposium on Principles of Distributed computing, New York, pp. 137-151, 1987.

[18] Milner R., Communication and Concurrency International Series in Computer Science, Prentice Hall Englewood Cliffs, 1989.

[19] Milner R., Communicating and Mobile Systems: the Pi Calculus, Cambridge University Press, 1999.

[20] Pandurangan G., Raghavan P., and Upfal E., “Building Low-Diameter P2P Networks,” in Proceedings of the 42nd IEEE symposium on Foundations of Computer Science, USA, pp. 492-499, 2001.

[21] Pandurangan G., Robinson P., and Trehan A., “DEX: Self-Healing Expanders,” Distributed Computing, vol. 29, no. 3, pp. 163-185, 2016.

[22] Pandurangan G. and Trehan A., “Xheal: A Localized Self-Healing Algorithm Using Expanders,” Distributed Computing, vol. 27, no 1, pp. 39-54, 2014.

[23] Peleg D., “Distributed Computing,” SIAM Monographs on Discrete Mathematics and Applications, vol. 5, 2000.

[24] Pippenger N. and Lin G., “Fault-Tolerant Circuit- Switching Networks,” SIAM Journal on Discrete Mathematics, vol. 7, no. 1, pp. 108-118, 1994.

[25] Raynal M., Distributed Algorithms for Message- Passing Systems, Springer, 2013.

[26] Upfal E., “Tolerating a Linear Number of Faults in Networks of Bounded Degree,” Information and Computation, vol. 115, no. 2, pp. 312-320, 1994.

[27] Wan J., Yuan D., and Xu X., “A Review of Routing Protocols In Wireless Sensor Networks,” in Proceedings of 4th International Conference on Wireless Communications, Networking and Mobile Computing, Dalian, pp. 1-4, 2008. Ra’ed Bani Abdelrahman is an Assistant Professor of Software Engineering at Ajloun National University, Jordan. He has a Ph.D from Loughborough University, UK and his MSc. and BSc. from Yarmouk University, Jordan. His interest is in modelling safety and liveness properties of critical systems. His other interests are in the area of concurrent systems, network algorithms and protocols. Rafat Alshorman is an associate professor in the department of computer science at Yarmouk University/Jordan. He completed his Ph.D. at Loughborough University/UK and his undergraduate studies at Yarmouk University/Jordan. His research interests lie in the area of algorithms and mathematical models, ranging from theory to implementation, with a focus on checking the correctness conditions of concurrent and reactive systems. In recent years, he has focused on theoretical computer science such as Graph theory and Numerical analysis. Dr. Alshorman research interests are: 1. Mathematical methods in computer science, 2. Temporal logics, 3. Concurrent systems, 4. machine learning 5. Numerical analysis. Walter Hussak is an Honorary Fellow in the Department of Computer Science at Loughborough University, UK. Who has retired from lecturing but continues with research and project supervision. He has an MSc in Systems Design and a PhD in Mathematics. As such, he has broad interests in theoretical computer science and mathematics. Most of his work has been in the theory and applications of temporal logics, concurrent systems and graph theory. Amitabh Trehan is a Lecturer (i.e., Assistant Professor) of Computer Science at Loughborough University, UK. His research interests center around designing provably efficient algorithms and modelling and reasoning about multi-agent dynamic scenarios using tools such as graph theory and game theory. In particular, he has a large body of work on distributed algorithms - in static networks (e.g. Leader Election and flooding) and on dynamic scenarios, in particular, developing self- healing algorithms.