Formalised hybrid control scheme for a UAV group using Dubins set and model checking

A novel hybrid control scheme is proposed for a decentralised, autonomous UAV group. The system incorporates a formalised representation of the model in its entirety using Kripke Models of possible worlds. Using this approach, the system can be represented in a formalised, yet intuitive manner (as a directed graph) and can be subsequently subjected to analytical proof-checking. The vehicle model implements the classical Dubins result on curves of minimal length with a constraint on average curvature in its path planning techniques in order to optimise travel time, as well as travel distance. The Dubins path is obtained by using prescribed initial and terminal orientations between two waypoints - joined by circular arcs with a connecting tangent. Unlike previous studies, the Dubins´ model is applied on multiple vehicles, and their ability to co-ordinate feasible paths for the scenario is analysed. An algorithmic implementation of the aforementioned hybrid model is presented. Lastly, the control strategies presented are proof-checked using model checking techniques.