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
multirobot 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 blackboxes. 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: 
[SheshkalaniKhosraviMohammadi17]
A. N. Sheshkalani, R. Khosravi, and M. Mohammadi.
Verification of VisibilityBased Properties on Multiple Moving Robots.
Proceedings of the 18th Annual Conference on Towards Autonomous Robotic
Systems (TAROS'2017), Guildford, UK, LNCS vol. 10454, pages 5165.
Springer Verlag, July 2017.
Available online at: https://link.springer.com/chapter/10.1007/9783319641072_5 
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/casestudies 