Cooperation of multiple autonomous robots and analysis of their swarm behavior

Współpraca roju autonomicznych robotów i analiza ich zbiorowych zachowań

  • Bogdan Czejdo Department of Mathematics and Computer Science, Fayetteville State University, Fayetteville
  • Wiktor Daszczuk Warsaw University of Technology, Institute of Computer Science
  • Waldemar Grabski Warsaw University of Technology, Institute of Computer Science
  • Sambit Bhattacharya Department of Mathematics and Computer Science, Fayetteville State University, Fayetteville
Keywords: autonomous robots, behavior verification, model checking, Integrated Model of Distributed Systems, deadlock, termination


In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behavior. The sub-diagrams describing sub-routs allowed us to model advanced interactions between autonomous robots using limited number of state combinations avoiding combinatorial explosion of reachability. We identified the systems for which we can ensure the correctness of robots interactions. New techniques were presented to verify and analyze combined robots’ behavior. The partitioned diagrams allowed us to model advanced interactions between autonomous robots and detect irregularities such as deadlocks, lack of termination etc. The techniques were presented to verify and analyze combined robots’ behavior using model checking approach. The described system, Dedan verifier, is still under development. In the near future, timed and probabilistic verification are planned.


1. Czejdo, B., Bhattacharya, S.: Programming Robots with State Diagrams. J. Comput. Sci. Coll. 24(5), pp. 19–26 (2009).
2. Dedan,
3. Cho, J., Yoo, J., Cha, S.: NuEditor – A Tool Suite for Specification and Verification of NuSCR. In: SERA 2004: Software Engineering Research and Applications, Los Angeles, CA, 5-7 May 2004, LNCS Vol. 3647, pp. 19–28. Springer, Berlin Heidelberg (2006). DOI: 10.1007/11668855_2
4. Royer, J.: Formal specification and temporal proof techniques for mixed systems. In: Proceedings 15th International Parallel and Distributed Processing Symposium. IPDPS 2001, San Francisco, CA, 23-27 April 2001. pp. 1542–1551. IEEE Comput. Soc, New York, NY (2001). DOI: 10.1109/IPDPS.2001.925139
5. Mazuelo, C.L.: Automatic Model Checking of UML models, MSc Thesis, Universitat Berlin (2008),
6. Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification. Model-Checking Techniques and Tools. Springer-Verlag, Berlin Heidelberg (2001). ISBN: 978-3-662-04558-9
7. Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multithreaded C Programs, Report UUCS-08-004. University of Utah, Salt Lake City, UT (2008).
8. Attie, P.C.: Synthesis of large dynamic concurrent programs from dynamic specifications. Form. Methods Syst. Des. 47(131), pp. 1–54 (2016). DOI: 10.1007/s10703-016-0252-9
9. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge, MA (2008). ISBN: 9780262026499
10. Fahland, D., Favre, C., Koehler, J., Lohmann, N., Völzer, H., Wolf, K.: Analysis on demand: Instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70(5), pp. 448–466 (2011). DOI: 10.1016/j.datak.2011.01.004
11. Joosten, S.J.C., Julien, F.V., Schmaltz, J.: WickedXmas: Designing and Verifying on-chip Communication Fabrics. In: 3rd International Workshop on Design and Implementation of Formal Tools and Systems, DIFTS’14, Lausanne, Switzerland, 20 Oct. 2014. pp. 1–8. Technische Universiteit Eindhoven, The Netherlands (2014).
12. Martens, M.: Establishing Properties of Interaction Systems, PhD Thesis, University of Mannheim (2009),
13. Sharma, N.K., Bhargava, B.: A Robust Distributed Termination Detection Algorithm, Report 87-726. Purdue University Press, West Lafayette, IN (1987).
14. Guan, X., Li, Y., Xu, J., Wang, C., Wang, S.: A Literature Review of Deadlock Prevention Policy Based on Petri Nets for Automated Manufacturing Systems. Int. J. Digit. Content Technol. its Appl. 6(21), pp. 426–433 (2012). DOI: 10.4156/jdcta.vol6.issue21.48
15. Huang, S.-T.: Detecting termination of distributed computations by external agents. In: [1989] Proceedings. The 9th International Conference on Distributed Computing Systems, Newport Beach, CA, 5-9 June 1989. pp. 79–84. IEEE Comput. Soc. Press, New York, NY (1989). DOI: 10.1109/ICDCS.1989.37933
16. Mattern, F.: Global quiescence detection based on credit distribution and recovery. Inf. Process. Lett. 30(4), pp. 195–200 (1989). DOI: 10.1016/0020-0190(89)90212-3
17. Peri, S., Mittal, N.: On Termination Detection in an Asynchronous Distributed System. In: 17th ISCA International Conference on Parallel and Distributed Computing Systems (PDCS), San Francisco, CA, 15-17 Sept. 2004. pp. 209–215 (2004).
18. Zhou, J., Chen, X., Dai, H., Cao, J., Chen, D.: M-Guard: A New Distributed Deadlock Detection Algorithm Based on Mobile Agent Technology. In: 2nd international conference on Parallel and Distributed Processing and Applications ISPA’04, Hong Kong, China, 13-15 Dec. 2004. pp. 75–84. Springer-Verlag, Berlin Heidelberg (2004). DOI: 10.1007/978-3-540-30566-8_13
19. Dijkstra, E.W., Scholten, C.S.: Termination detection for diffusing computations. Inf. Process. Lett. 11(1), pp. 1–4 (1980). DOI: 10.1016/0020-0190(80)90021-6
20. Kumar, D.: A class of termination detection algorithms for distributed computations. In: Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India 16–18 Dec. 1985. pp. 73–100. Springer-Verlag, Berlin Heidelberg (1985). DOI: 10.1007/3-540-16042-6_4
21. Mattern, F.: Algorithms for distributed termination detection. Distrib. Comput. 2(3), pp. 161–175 (1987). DOI: 10.1007/BF01782776
22. Matocha, J., Camp, T.: A taxonomy of distributed termination detection algorithms. J. Syst. Softw. 43(3), pp. 207–221 (1998). DOI: 10.1016/S0164-1212(98)10034-1
23. Chalopin, J., Godard, E., Métivier, Y., Tel, G.: About the Termination Detection in the Asynchronous Message Passing Model. In: 33rd Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, 20-26 Jan. 2007. pp. 200–211. Springer, Berlin Heidelberg (2007). DOI: 10.1007/978-3-540-69507-3_16
24. Kshemkalyani, A.D., Mukesh, S.: Distributed Computing. Principles, Algorithms, and Systems. Cambridge University Press, Cambridge, UK (2008). ISBN: 978-0-521-87634-6
25. Ma, G.: Model checking support for CoreASM: model checking distributed abstract state machines using Spin, MSc Thesis, Simon Fraser University, Burnaby, Canada (2007),
26. Ray, I., Ray, I.: Detecting Termination of Active Database Rules Using Symbolic Model Checking. In: 5th East European Conference on Advances in Databases and Information Systems, ADBIS ’01, Vilnius, Lithuania, 25–28 Sept. 2001. pp. 266–279. Springer-Verlag, London, UK (2001). DOI: 10.1007/3-540-44803-9_21
27. Garanina, N.O., Bodin, E. V.: Distributed Termination Detection by Counting Agent. In: 23th International Workshop on Concurrency, Specification and Programming, CS&P, Chemnitz, Germany, 29 Sept. - 1 Oct. 2014. pp. 69–79. Humboldt University, Berlin, Germany (2014).
28. Podelski, A., Rybalchenko, A.: Software Model Checking of Liveness Properties via Transition Invariants, Research Report MPI–I–2003–2–00, Max Planck Institite fur Informatik, Dec. 2003. (2003).
29. Harel, D.: On visual formalisms. Commun. ACM. 31(5), pp. 514–530 (1988). DOI: 10.1145/42411.42414
30. Rumbaugh, J., Blaha, M., Premerlani, W., Eddy, F., Lorensen, W.: Object-Oriented Modeling and Design. Prentice Hall, New Jersey, NJ (1990). ISBN: 0-13-629841-9
31. Galamhos, C., Matas, J., Kittler, J.: Progressive probabilistic Hough transform for line detection. In: Proceedings. 1999 IEEE Computer Society Conference on Computer Vision and Pattern Recognition (Cat. No PR00149), Fort Collins, CO, 23–25 June 1999. pp. 554–560. IEEE Comput. Soc, New York, NY (1999). DOI: 10.1109/CVPR.1999.786993
32. Czejdo, B., Bhattacharya, S., Czejdo, J.: Use of Probabilistic State Diagrams for Robot Navigation in an Indoor Environment. In: Proceedings of the Annual International Conference on Advances in Distributed and Parallel Computing ADPC 2010, Singapore, 1-2 Nov. 2010. pp. A97–A102. Global Science and Technology Forum (2010). DOI: 10.5176/978-981-08-7656-2ATAI2010-63
33. Czejdo, B., Bhattacharya, S., Baszun, M.: Use of Multi-level State Diagrams for Robot Cooperation in an Indoor Environment. In: ICDIPC 2011: Digital Information Processing and Communications, Ostrava, Czech Republic, 7-9 July 2011, part II, CCIS vol. 189. pp. 411–425. Springer, Berlin Heidelberg (2011). DOI: 10.1007/978-3-642-22410-2_36
34. Peled, D.A.: Software Reliability Methods. Springer, Berlin Heidelberg (2001). ISBN: 978-1-4419-2876-4
35. Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), pp. 626–643 (1996). DOI: 10.1145/242223.242257
36. Clarke, E., McMillan, K., Campos, S., Hartonas-Garmhausen, V.: Symbolic model checking. In: Alur, R. and Henzinger, T.A. (eds.) 8th International Conference on Computer Aided Verification - CAV ’96, New Brunswick, NJ, 31 July – 3 Aug. 1996. pp. 419–422. Springer, Berlin Heidelberg (1996). DOI: 10.1007/3-540-61474-5_93
37. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), pp. 279–295 (1997). DOI: 10.1109/32.588521
38. Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), pp. 410–425 (2000). DOI: 10.1007/s100090050046
39. Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exp. 41(2), pp. 133–142 (2011). DOI: 10.1002/spe.1006
40. Daszczuk, W.B.: Communication and Resource Deadlock Analysis using IMDS Formalism and Model Checking. Comput. J. 60(5), pp. 729–750 (2017). DOI: 10.1093/comjnl/bxw099
41. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: 23rd International Conference, CAV 2011, Snowbird, UT, 14-20 July 2011. pp. 585–591. Springer, Berlin Heidelberg (2011). DOI: 10.1007/978-3-642-22110-1_47
42. Chrobot, S., Daszczuk, W.B.: Communication Dualism in Distributed Systems with Petri Net Interpretation. Theor. Appl. Informatics. 18(4), pp. 261–278 (2006). arXiv: 1710.07907
43. Daszczuk, W.B.: Deadlock and termination detection using IMDS formalism and model checking, ICS WUT Technical Report No.4/2007. Warsaw University of Technology, Warsaw, Poland (2007). DOI: 10.13140/RG.2.2.23294.48969
44. Jia, W., Zhou, W.: Distributed Network Systems. From Concepts to Implementations. Springer, New York (2005). DOI: 10.1007/b102545
45. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), pp. 183–235 (1994). DOI: 10.1016/0304-3975(94)90010-8
46. Daszczuk, W.B.: Real Time Model Checking Using Timed Concurrent State Machines. Int. J. Comput. Sci. Appl. 4(11), pp. 1–12 (2006).