Modelling and Verification of Multi-Agent Systems via Sequential Emulation

A multi-agent system (MAS) is a collection of agents, often endowed with individual goals and a partial view of the whole system, that may be required to achieve complex goals by interacting with each other and with the environment. MASs are a convenient modelling paradigm for complex scenarios across many research fields: they may either be used to describe and reason about existing systems (such as colonies of insects, social networks, economic markets), or to design and assess the correctness of new ones (such as swarms of robots, smart transportation systems). MASs feature an unprecedented degree of complexity, making their specification and analysis an open problem. This complexity stems from several distinctive features, such as nondeterministic individual behaviour and interactions, asynchronous communication, and a lack of central control. Because of this, formal verification of MASs is particularly challenging. Some existing MAS specification formalisms and platforms lack support for formal verification altogether, and are limited to simulation-based analysis; others focus on specific sub-classes of MASs, or come with tailored verification platforms that might not keep up with the state of the art in formal verification. Meanwhile, formal verification research mainly targets low-level formalisms or traditional programming languages. However, these languages often lack constructs to naturally capture distinctive features of MASs, and thus may be not appropriate for describing them. To bridge this gap, we put forward a high-level specification language for MASs, where agents operate on (parts of) a decentralised data structure, called a virtual stigmergy, which allows to model the influence of local changes on the global behaviour by asynchronously diffusing the knowledge of the agents. This diffusion happens transparently: the user of the language simply defines one or more stigmergic variables and assigns values to them. As a consequence, stigmergies may capture the behaviour of several interesting classes of MASs in a compact and intuitive way. We also introduce a mechanised sequential emulation procedure that encodes a high-level system specification into a sequential imperative program. The execution traces of this program emulate the possible evolutions of the input system. Then, the question of whether a property of interest holds for the given system may be answered by performing a certain verification task on the generated program. This allows us to immediately exploit mature verification techniques developed for general-purpose languages, and to effortlessly integrate new techniques as soon as they become available. The procedure is language-agnostic, as it may generate programs in any imperative language with arrays and loops and it may be adapted to support different input formalisms. We show the feasibility of our approach by implementing a tool that applies this procedure to our original language. A thorough experimental evaluation shows that we can formally verify a selection of real-world systems using off-the-shelf program verification tools.