OPERAS: A Framework for the Formal Modelling of Multi-Agent Systems and Its Application to Swarm-Based Systems

摘要

Swarm-based systems are a class of multi-agent systems (MAS) of particular interest because they exhibit emergent behaviour through self-organisation. They are biology-inspired but find themselves applicable to a wide range of domains, with some of them characterised as mission critical. It is therefore implied that the use of a formal framework and methods would facilitate modelling of a MAS in such a way that the final product is fully tested and safety properties are verified. One way to achieve this is by defining a new formalism to specify MAS, something which could precisely fit the purpose but requires significant period to formally prove the validation power of the method. The alternative is to use existing formal methods thus exploiting their legacy. In this paper, we follow the latter approach. We present OPERAS, an open framework that facilitates formal modelling of MAS through employing existing formal methods. We describe how a particular instance of this framework, namely OPERASxc, could integrate the most prominent characteristics of finite state machines and biological computation systems, such as X-machines and P Systems respectively. We demonstrate how the resulting method can be used to formally model a swarm system and discuss the flexibility and advantages of this approach.