| Paper title: |
A Formal Verification Model for Performance Analysis of Reinforcement Learning Algorithms Applied to Dynamic Networks |
| DOI: | https://doi.org/10.4316/JACSM.201701002 |
| Published in: | Issue 1, (Vol. 11) / 2017 |
| Publishing date: | 2017-04-13 |
| Pages: | 13-16 |
| Author(s): | KULKARNI Shrirang Ambaji, RAO Raghavendra G. |
| Abstract. | Routing data packets in a dynamic network is a difficult and important problem in computer networks. As the network is dynamic, it is subject to frequent topology changes and is subject to variable link costs due to congestion and bandwidth. Existing shortest path algorithms fail to converge to better solutions under dynamic network conditions. Reinforcement learning algorithms posses better adaptation techniques in dynamic environments. In this paper we apply model based Q-Routing technique for routing in dynamic network. To analyze the correctness of Q-Routing algorithms mathematically, we provide a proof and also implement a SPIN based verification model. We also perform simulation based analysis of Q-Routing for given metrics |
| Keywords: | Dynamic Networks, Reinforcement Learning, QRouting. SPIN Model Checking |
| References: | 1. W Stallings, “High-peed Networks and Internets, Performance and Quality of Service”, Pearson Education, Second Edition, 2002, pp. 409-415. 2. E Alpaydin, “Introduction to Machine Learning”, PHI, 2006 pp 11-12. 3. J.A Boyman, M.L Littman, “Packet Routing in Dynamically Changing Networks: A reinforcement Learning Approach”, In Advances in Neural Information Processing Systems, 1994, MIT Press, Cambridge M.A. 4. S Kumar, R Mikkulainen, “Dual Reinforcement Q-Routing: An On-line Adaptive Routing Algorithm”, In Proceedings of Artifical Neural Networks in Engineering 1997. 5. S Kumar, “Confidence based Dual Reinforcement Q-Routing: an On-line Adaptive Network Routing Algorithm”, A Technical Report Artifical Intelligence Laboratory, The University of Texas at Austin, Austin, AI98-267, May 1998. 6. C Baier and J-P Katoen, “Principles of Model Checking”, The MIT Press, Cambridge, 2007 7. Gerard J. Holzmann, “Spin Model Checker, The Primer and Reference Manual”, Addison Wesley, 2003. 8. G J. Holzmann, “The Model Checker SPIN”, IEEE Transactions on Software engineering, Vol. 23, No.5, May 1997. 9. L. Lamport, “The temporal logic of actions”, ACM Transactions on Programming Languages and Systems, vol. 16, no 3, pp. 872-923, May 1994. 10. R. Gerth, “A concise language reference for Promela”, http://www.spinroot.com/spin /Man/ Quick.html 11. N.A.S.A LARC, “What is formal methods?” http://shemesh.larc.nasa.gov/fm/fm-what.html. 12. Z Wang, J Crowcroft, “Analysis of Shortest-Path Routing Algorithms in a Dynamic Network Environment”, http://www.citeseer.ist. psu.edu/wang92analysis.html 13. F. Tekiner, Z. Ghassemlooy and T.R Srikanth, “Comparison of the Q-Routing and Shortest Path Routing Algorithms”, http://soe.unn.ac.uk/ocr/papers/2004/PGNET04 Firat/Tekiner.pdf 14.L Peshkin, V Savova, “Reinforcement Learning for Adaptive Routing”, http://people.csail.mit.edu/pesha/Public/route.pdf 15. R. d Renesse, A.H. Aghvami, “Formal Verification of Ad-Hoc Routing Protocols Using SPIN Model Checker”, http://www.sps.ele.tue.nl/members/m.j.bastiaans/spc/renesse.pdf |
| Back to the journal content | |
