Model checking for decision making behaviour of heterogeneous multi-agent autonomous system

摘要

An autonomous system has been widely applied for various civil/military research
\nbecause of its versatile capability of understanding high-level intent and
\ndirection of a surrounding environment and targets of interest. However, as autonomous
\nsystems can be out of control to cause serious loss, injury, or death in
\nthe worst case, the verification of their functionalities has got increasing attention.
\nFor that reason, this study is focused on the verification of a heterogeneous
\nmulti-agent autonomous system. The thesis first presents an overview of formal
\nmethods, especially focuses on model checking for autonomous systems verification.
\nThen, six case studies are presented to verify the decision making behaviours
\nof multi-agent system using two basic scenarios: surveillance and convoy. The
\ninitial system considered in the surveillance mission consists of a ground control
\nsystem and a micro aerial vehicle. Their decision-making behaviours are
\nrepresented by means of Kripke model and computational tree logic is used to
\nspecify the properties of this system. For automatic verification, MCMAS (Model
\nChecker for Multi-Agent Systems) is adopted due to its novel capability to accommodate
\nthe multi-agent system. After that, the initial system is extended
\nto include a substitute micro aerial vehicle. These initial case studies are then
\nfurther extended based on SEAS DTC exemplar 2 dealing with behaviours of
\nconvoy protection. This case study includes now a ground control system, an
\nunmanned aerial vehicle, and an unmanned ground vehicle. The MCMAS successfully
\nverifies the targeting behaviours of the team-level unmanned systems.
\nReversely, these verification results help retrospectively improve the design of
\ndecision-making algorithms by considering additional agents and behaviours
\nduring four steps of scenario modification. Consequently, the last scenario deals
\nwith the system composed of a ground control system, two unmanned aerial
\nvehicles, and four unmanned ground vehicles with fault-tolerant and communications
\nrelay capabilities. In conclusion, this study demonstrates the feasibility
\nof model checking algorithms as a verification tool of a multi-agent system in
\nan initial design stage. Moreover, this research can be an important first step of
\nthe certification of multi-agent autonomous systems for the domains of robotics,
\naerospace and aeronautics.