An Approach for the Verification of Multi-agent Systems by Formally Guided Simulations

Multi-Agent Systems (MASs) can be used to model human and animal societies, for the purpose of analyzing their properties by computational means. We propose a verification technique that investigates such MASs by means of guided simulations. This is achieved by modeling the evolutions of an MAS as a transition system (implicitly), and the property to be verified as another transition system (explicitly). The former is derived (on-the-fly) from a formal specification of the MAS´s environment. The latter, which we call a simulation purpose, is used both to verify the property and to guide the simulation. In this way, only the states that are relevant for the property in question are actually simulated. Algorithmically, this corresponds to building a synchronous product of these two transitions systems on-the-fly and using it to operate a simulator. This paper presents an overall account of this approach, whose several parts were developed in a number of previous works. Our main objective here is to provide an overall account of the technique in a succinct manner, so that its most important and general features are highlighted. To clarify the theoretical discussions and show their practical importance, we develop concrete working examples along the text.