Kripke modelling approaches of a multiple robots system with minimalist communication: A formal approach of choice

摘要

Real-time, critical systems such as avionics software and hardware chips, owe their reliability to formal modelling approaches from their design phase. Following this philosophy, an intuitive yet mathematically rigorous approach of Kripke modelling is used for representing a co-operative, decentralised mobile robot group. The robot group operates with minimalist communication and no a priori knowledge of the operating environment for achieving interception and coordinated time-over-target. This scenario is a prototype of a simple task envisaged for a group of unmanned aerial vehicles (UAVs). As such, the resulting behaviour of the UAVs must be designed and analysed, so that guaranteed performance is ensured if only to achieve flight certification. Hence, there is a need for a mathematically rigorous approach, or a formal modelling technique. Several such techniques are briefly reviewed and it is argued that Kripke modelling is the best suited one. Kripke models consist of, firstly, a set of possible worlds ( system configurations), secondly, an accessibility relation in the set ( 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 co-operation can be precisely expressed using temporal logic statements defining safety, liveness etc. Whether a group of robots, whose behaviour is formalised with Kripke models, possesses such properties is then verified using automated model checking tools. Rationale for this approach along with simulation and verification results are presented in the paper.