Formal modelling and verification of multi-robot systems specified with temporal logic

Formal modelling and verification techniques give a high degree of confidence that the system performs as per the specifications. In this paper we present Kripke modelling approach to formalize multi-robot and multi-UAV systems. Temporal logic is used to specify the desirable system properties. The first scenario considered include path-planning of a group of three robots moving in an obstacle free environment. Linear Temporal Logic (LTL) formulae are used to precisely express the desirable properties of cooperation, safety, liveness etc. Whether the group of robots, whose behaviour is formalized by Kripke models, possesses such properties is then verified using \textsc{Spin} model checking tool. The second scenario is path-planning for a muti-UAV system cooperatively searching a given area in an unstructured environment with threats. Computation Tree Logic (CTL) is used to express the desirable behaviours of the UAVs. SMV languge is used to describe the Kripke model of this multi-UAV system and the specified CTL formulae are then verified against the Kripke model using \textsc{SMV} model checker.