Reasoning about Multi-Agent systems using stochastic petri nets

Abstract

Multi-agent systems are composed by many independent agents where the task of some of themmay depend on the task of others. In this work we present a generic Stochastic Petri Netmodel for agents and illustrate the usage of a sound, complete and decidable logic systemto verify properties in multi-agent systems modelled as Stochastic Petri Nets: the DS3 logic. This logic takes advantage of the intuitive graphical interpretation of Petri Nets, allowing the user to model the behaviour of agents and their interactions by means of nets (i.e. seen Petri Nets as graphs). Our approach leads not only to a usual place-transition connection provided by Petri-nets underlying graphs modelling, such as the verification of properties and validation of agents, but also regards the verification of properties concerning their behaviour inside an environment.