Journal
INTERNATIONAL JOURNAL OF SYSTEMS SCIENCE
Volume 46, Issue 4, Pages 634-651Publisher
TAYLOR & FRANCIS LTD
DOI: 10.1080/00207721.2013.793890
Keywords
Kripke model; computational temporal logic; model checking; heterogeneous multi-agent system
Categories
Funding
- Systems Engineering for Autonomous Systems (SEAS) Defence Technology Centre
- UK Ministry of Defence
Ask authors/readers for more resources
The focus of the paper is how to model autonomous behaviours of heterogeneous multi-agent systems such that it can be verified that they will always operate within predefined mission requirements and constraints. This is done by using formal methods with an abstraction of the behaviours modelling and model checking for their verification. Three case studies are presented to verify the decision-making behaviours of heterogeneous multi-agent system using a convoy mission scenario. The multi-agent system in a case study has been extended by increasing the number of agents and function complexity gradually. For automatic verification, model checker for multi-agent systems (MCMAS) is adopted due to its novel capability to accommodate the multi-agent system and successfully verifies the targeting behaviours of the team-level autonomous systems. The verification results help retrospectively the design of decision-making algorithms improved by considering additional agents and behaviours during three steps of scenario modification. Consequently, the last scenario deals with the system composed of a ground control system, two unmanned aerial vehicles, and four unmanned ground vehicles with fault-tolerant and communication relay capabilities.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available