Verification of Visibility-Based Properties on Multiple Moving Robots

Organisation:	University of Tehran (IRAN)
Method:	LTL
Tools used:	CGAL CADP (Construction and Analysis of Distributed Processes)
Domain:	Robotics.
Period:	2017
Size:	4 polygons, 4 robots.
Description:	Mobile robots are able to sense, communicate, and interact with the physical world, and are able to collaboratively solve problems in a wide range of applications. Robot motion planning and computational geometry are closely related in the applications where the robots are constrained to move within a geometric domain. Traditionally, the correctness of robot motion planning algorithms within the context of computational geometry is investigated by manual proofs. However, when the motion planning algorithms' parameters are heuristically tuned to find the best solution, manually proving the algorithm with every change may be impractical. An alternative and more reliable approach to examine the correctness of the planning algorithms is formal verification, and more specifically, model checking. The proposed model checking method takes four inputs: (1) the environment, in the form of a simple polygon, (2) the algorithms controlling the motions of the robots, (3) the paths on which the robots are allowed to move, along with their initial positions, and (4) the requirement, expressed as a LTL formula. The method was automated using the CGAL (Computational Geometry Algorithms Library). The program automatically constructs the state space of the robot system during the movement of the robots. Precisely, the states and the transitions are constructed w.r.t. the decisions made by the robots during their movements (determined by the motion algorithms). The method was illustrated on a case study involving robot swarms algorithms, in which the robots use only local wireless connectivity information to achieve swarm aggregation. The state space generation process was executed during 360 minutes, and two LTL formulas were checked using CADP, expressing respectively that robots are infinitely often connected (connectivity) and the system eventually reaches a state in which the communication graph is connected and the environment is fully covered by the robots (coverage). CADP evaluated each formula in less than two seconds for the polygons considered, which shows the applicability of the proposed method.
Conclusions:	A method was proposed to construct a discrete state space for a multi-robot system and then verify the correctness properties by means of model checking techniques. The notion of state has been defined in such a way that each state can be uniquely labeled with the atomic propositions expressing connectivity and coverage. The method is generic, in the sense that it handles the navigation algorithms as black-boxes. The generated state space is used to verify temporal formulas constructed over the atomic propositions using CADP. An important benefit of this approach is to eliminate the need for analytical proof of correctness upon changes to the navigation algorithms.
Publications:	[Sheshkalani-Khosravi-Mohammadi-17] A. N. Sheshkalani, R. Khosravi, and M. Mohammadi. Verification of Visibility-Based Properties on Multiple Moving Robots. Proceedings of the 18th Annual Conference on Towards Autonomous Robotic Systems (TAROS'2017), Guildford, UK, LNCS vol. 10454, pages 51-65. Springer Verlag, July 2017. Available on-line at: https://link.springer.com/chapter/10.1007/978-3-319-64107-2_5 [Sheshkalani-Khosravi-18] Ali Narenji Sheshkalani and Ramtin Khosravi. Verification of Visibility-Based Properties on Multiple Moving Robots in an Environment with Obstacles. International Journal of Advanced Robotic Systems 15(4), pages 1-13, July 2018. Available on-line at: https://journals.sagepub.com/doi/abs/10.1177/1729881418786657 and from the CADP Web site in PDF or PostScript
Contact:	Ramtin Khosravi School of Electrical and Computer Engineering University of Tehran North Kargar st. Tehran Iran Tel: +98 (21) 88027756 Email: r.khosravi@ut.ac.ir
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page