Total views : 192

Temporal Modelling and Verification of Multi-Robot Concurrent Activities

Affiliations

  • Department of Computer Science, Government College University, Lahore,, Pakistan
  • Department of Computer Science, Government College University, Lahore, Pakistan

Abstract


Objectives: In this work, we have introduced a method for formally verifying the concurrent activities of multiple robots. The objective is to formalize a framework for concurrent systems by using temporal logics. Methods/Statistical Analysis: The movement of the robots in given environment is modelled as a weighted transition system and the target is specified in Linear Temporal Logic (LTL) formulae over a set of propositions. Findings: The LTL formulas are characterized to handle the uncertainty or any abnormal activity during the process. The system is designed using SPIN model checker in which different LTL properties are verified. A theoretical description is supported by some experimental results, generated using the existing logics and techniques. Application/ Improvement: This work can be implemented for the surveillance task in pickup and delivery network.

Keywords

Formal Verification, Model Checking, Path Planning, Robotics

Full Text:

 |  (PDF views: 181)

References


  • Chiappini A, Cimatti A, Porzia C, Rotondo G, Sebastiani R, Traverso P, Villafiorita A. Formal specification and development of a safety-critical train management system. In International Conference on Computer Safety, Reliability, and Security Springer Berlin Heidelberg, Lecture Notes in Computer Science. 1999 Oct 14; 1698:410–9.
  • Wongpiromsarn T, Topcu U, Murray RM. Receding horizon control for temporal logic specifications. In Proceedings of the 13th Association for Computing Machinery (ACM) International Conference on Hybrid Systems: Computation And Control, USA; 2010 Apr. p. 101–10.
  • Rekleitis I, New AP, Rankin ES, Choset H. Efficient boustrophedon multi-robot coverage: an algorithmic approach. Annals of Mathematics and Artificial Intelligence. 2008 Apr; 52(2–4):109–42.
  • Tabuada P, Pappas GJ. Model checking LTL over controllable linear systems is decidable. In International Workshop on Hybrid Systems: Computation and Control Springer Berlin Heidelberg, Lecture Notes in Computer Science. 2003 Mar 14; 2623:498–513.
  • Bhatia A, Kavraki LE, Vardi MY. Sampling-based motion planning with temporal goals. In the Proceedings of Institute of Electrical and Electronics Engineers (IEEE) International Conference on Robotics and Automation (ICRA), Anchorage, Alaska, USA; 2010 May 3–7. p. 2689–96.
  • Kress-Gazit H, Fainekos GE, Pappas GJ. Temporal-logicbased reactive mission and motion planning. Institute of Electrical and Electronics Engineers (IEEE) transactions on robotics. 2009 Dec; 25(6):1370–81.
  • Calzolai F, Nicola DR, Loreti M, Tiezzi F. TAPAs: a tool for the analysis of process algebras. In Transactions on Petri Nets and Other Models of Concurrency I Springer Berlin Heidelberg, Lecture Notes in Computer Science. 2008; 5100:54–70.
  • Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: An open source tool for symbolic model checking. In International Conference on Computer Aided Verification Springer Berlin Heidelberg, Lecture Notes in Computer Science. 2002 Sep; 2404:359–64.
  • Holzmann GJ. The model checker SPIN. Institute of Electrical and Electronics Engineers (IEEE) Transactions on software engineering. 1997 May; 23(5):279–95.
  • Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods: practice and experience. Association for Computing Machinery (ACM) Computing Surveys (CSUR). 2009 Oct; 41(4):19.
  • Chen Y, Ding XC, Stefanescu A, Belta C. Formal approach to the deployment of distributed robotic teams. Institute of Electrical and Electronics Engineers (IEEE) Transactions on Robotics. 2012 Feb; 28(1):158–71.
  • Yarmohamadi M, Javadi HH, Erfani H. Improvement of robot path planning using particle swarm optimization in dynamic environments with mobile obstacles and target. Advanced Studies in Biology. 2011; 3(1):43–53.
  • Kim JH, Vadakkepat P. Multi-agent systems: a survey from the robot-soccer perspective. Intelligent Automation and Soft Computing. 2000 Jan; 6(1):3–17.
  • Frappier M, Fraikin B ,Chossart R , Fa RCY , Ouenzar M . Comparison of model checking tools for information systems. In 12th International Conference on Formal Engineering Methods (ICFEM), Lecture Notes in Computer Science, Springer. 2010 Nov; 6447:581–96.
  • Qasim A, Kazmi SA, Fakhir I. Executable semantics for the formal specification and verification of E-agents. Indian Journal of Science and Technology. 2015 Jul; 8(16):1–8.
  • Qasim A, Kazmi AR, Fakhir I. Formal specification and verification of real-time multi-agent system using timed arc Petri nets. Advances in Electrical and Computer Engineering. 2015 Jan; 15(3):73–8.
  • Navarro I, Matía F. A survey of collective movement of mobile robots. International Journal of Advanced Robotic Systems.2013 Jan; 10(73):1–9.
  • Clark CM, Rock SM, Latombe JC. Motion planning for multiple mobile robots using dynamic networks. In the Proceedings of Institute of Electrical and Electronics Engineers (IEEE) International Conference on Robotics and Automation (ICRA),USA. 2003 Sep; 3:4222–7.
  • Guo Y, Parker LE. A distributed and optimal motion planning approach for multiple mobile robots. In the Proceedings of Institute of Electrical and Electronics Engineers (IEEE) International Conference on Robotics and Automation (ICRA), USA. 2002 May; 3:2612–9 .
  • Vardi MY , Wolper P . An automata-theoretic approach to automatic program verification. In 1st Symposium in Logic in Computer Science (LICS). Institute of Electrical and Electronics Engineers (IEEE) Computer Society, Cambridge; 1986. p. 322–31.
  • Jiang K. Model checking C programs by translating C to promela [Master thesis]. Sweden, Institutionen för informationsteknologi, Uppsala Universitet; 2009. p. 1–81.

Refbacks

  • There are currently no refbacks.


Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.