Kripke Modelling and Model Checking of a Multiple UAV System Monitoring Road Network
Gopinadh Sirigineedi, Antonios Tsourdos, Brian A. White, Rafał Żbikowski · 2010
This paper presents a veriflable multiple UAV system cooperatively monitoring a road network. The focus is on formal modelling and veriflcation which can guarantee correctness of reactive systems like multi-UAV systems. Kripke modelling is used to formally model the decentralized cooperative control strategy, and to verify correctness of the speciflcations. Desirable properties of the mission like liveness are expressed in Computation Tree Logic (CTL). Whether the group of autonomously operating UAVs, whose behaviour is formalized by Kripke model, possesses such properties is then verifled using automated model checking tool. Hence, guaranteed performance of cooperating UAVs can be assured in a formal and precise way.