Verification of Epistemic Properties in Probabilistic Multi-Agent Systems

摘要

Over the past decade Multi-Agent Systems (MAS) have emerged as a successful approach to develop distributed applications. In recent years proposals have been made to extend MAS models with probabilistic behavior. Languages to reason about such systems were presented in order to deal with uncertainty that can be encountered in practical application domains. While in recent works model checking techniques have been successfully applied for verifying knowledge in classical MAS, no methods for verifying knowledge in probabilistic MAS yet exist. This paper proposes such a model checking approach for probabilistic MAS. The approach comprises a compositional modeling process, a modal logic with operators for the specification of epistemic and temporal properties, the corresponding model checking procedure, and an outline of how these techniques can be implemented into existing model checking tools. The advantages of the chosen design include the possibility to analyze the MAS both from the global perspective as well as from the perspective of the agents, and the polynomial complexity of the model checking algorithm.