Cooperation of multiple autonomous robots and analysis of their swarm behawior

• Autorzy: Czejdo B. , Daszczuk W. B. , Grabski W. , Bhattacharya S.

Identyfikatory

DOI

10.24136/atest.2018.516

Warianty tytułu

PL

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

• Języki publikacji: EN

Abstrakty

EN

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.

PL

W artykule opisano kontynuację wcześniejszych badań dotyczących współpracy autonomicznych robotów wewnątrz budynku. Obejmują one obejmują sytuacje, w których zmiany środowiska i zmiana liczby robotów w roju mogą poprawić lub pogorszyć efektywność wykonywania zadań przypisanych do roju robotów. Zaprezentowaliśmy nowatorskie podejście z wykorzystaniem dzielenia zachowań robota na zachowania składowe. Poddiagramy opisujące kładowe podmarszruty pozwoliły nam modelować zaawansowane interakcje między autonomicznymi robotami w oparciu o ograniczoną liczbę kombinacji zachowań, unikając eksplozji kombinatorycznej przestrzeni osiągalności. Opisano systemy, dla których możemy zapewnić poprawność interakcji robotów i zaprezentowano techniki weryfikacji i analizy zachowań połączonych robotów. Diagramy podzielone na partycje pozwoliły nam modelować zaawansowane interakcje pomiędzy autonomicznymi robotami i wykrywać nieprawidłowości, takie jak zakleszczenia, brak terminacji itp. Przedstawiono techniki weryfikacji i analizy złożonych zachowań robotów za pomocą techniki weryfikacji modelowej. Opisany system weryfikacji, Dedan, jest wciąż rozwijany. W niedalekiej przyszłości planowana jest weryfikacja z czasem rzeczywistym i probabilistyczna.

Słowa kluczowe

EN

autonomous robots; behavior verification; model checking; integrated model of distributed systems; deadlock; termination

PL

robot autonomiczny; weryfikacja zachowań; weryfikacja modelowa; zintegrowany model systemów rozproszonych; zakleszczenie; terminacja

• Wydawca: Instytut Naukowo-Wydawniczy "SPATIUM". sp. z o.o.
• Czasopismo: Autobusy : technika, eksploatacja, systemy transportowe
• Rocznik: 2018
• Tom: R. 19, nr 12
• Strony: 872--879
• Opis fizyczny: Bibliogr. 46 poz., schem.

Twórcy

autor

Czejdo B.

• Department of Mathematics and Computer Science, Fayetteville State University, Fayetteville, NC 28301, USA

autor

Daszczuk W. B.

• Warsaw University of Technology, Institute of Computer Science, Nowowiejska Str. 15/19, 00-665 Warsaw, Poland

autor

Grabski W.

• Warsaw University of Technology, Institute of Computer Science, Nowowiejska Str. 15/19, 00-665 Warsaw, Poland

autor

Bhattacharya S.

• Department of Mathematics and Computer Science, Fayetteville State University, Fayetteville, NC 28301, USA

Bibliografia

• 1. Czejdo, B., Bhattacharya, S.: Programming Robots with State Diagrams. J. Comput. Sci. Coll. 24(5), pp. 19–26 (2009). https://dl.acm.org/citation.cfm?id=1516600
• 2. Dedan, http://staff.ii.pw.edu.pl/dedan/files/DedAn.zip.
• 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), http://www.iam.unibe.ch/tilpub/2008/lar08.pdf
• 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). http://www.cs.utah.edu/docs/techreports/2008/pdf/UUCS-08-004.pdf
• 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). https://pure.tue.nl/ws/files/3916267/889737443709527.pdf
• 12. Martens, M.: Establishing Properties of Interaction Systems, PhD Thesis, University of Mannheim (2009), http://ub-madoc.bib.uni-mannheim.de/2629/1/DrArbeitMyThesis.pdf
• 13. Sharma, N.K., Bhargava, B.: A Robust Distributed Termination Detection Algorithm, Report 87-726. Purdue University Press, West Lafayette, IN (1987). http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1626&context =cstech
• 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). http://www.iith.ac.in/~sathya_p/index_files/PDCS-Transtd.pdf
• 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), http://summit.sfu.ca/system/files/iritems1/8056/etd2938.pdf
• 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). http://ceur-ws.org/Vol-1269/paper69.pdf
• 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). https://www7.in.tum.de/~rybal/papers/MPI-I-2003-2-004.liveness-via-transition-invariants.pdf
• 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). http://www.tmrfindia.org/ijcsa/V4I11.pdf