Kripke modelling of multiple robots with decentralized cooperation specified with temporal logic

Abstract

Kripke models are used to formalize decentralized cooperation of a group of robots, to propose temporal logic specification of the cooperation, and to verify the correctness of the specification by checking the models. The focus is on implementing this mathematical formalism under minimalist communication and under constrained motion of the robots. Kripke models consist of, firstly, a of possible worlds (system configurations), secondly, an accessibility relation in the (transitions between the worlds), and, thirdly, a labelling function (which logical statements are true in each world). This approach represents continuous dynamics and discrete decision making of the robots in a unified way. Desirable properties of cooperation can be precisely expressed using temporal logic statements defining safety, liveness, etc. Whether a group of robots, whose behaviour is formalized with Kripke models, possesses such properties is then verified using automated model checking tools. The scenarios considered include path planning of a group of three robots moving in an obstacle-free environment, without and with communication among group members. The results show that for each scenario the mathematical formalism of Kripke models expresses the group behaviour in a transparent and tractable way. Finally, desirable properties of the decentralized cooperation, specified with temporal logic, can be verified on the Kripke models by automatic model checking software. Hence, guaranteed performance of cooperating autonomous robots can be assured in a formal, precise, and clear way.