Symbolic Model Checking Multi-Agent Systems

Automated verification of finite-state systems by means of model checking techniques is now a well-established area of research. The success of model checking has led to a recent growth of interest in the applications of the techniques to the fields of artificial intelligence, such as planning and Multi-Agent Systems (MAS). In MAS the emphasis is on the autonomy and rationality of the components or agents. In this area, modal logics representing concepts such as knowledge, belief, desire, intention, and the temporal evolution of these are used to specify mental states of the agents. Since these modalities are given interpretations that are different from the ones of the standard temporal operators, it is not straightforward to apply general model checking tools developed for standard LTL (or CTL) temporal logic to the specification of MAS.The aim of this dissertation is to do research on the representation of MAS specification and the model checking methods to the verification of MAS. We propose a novel Kripke model to represent and model agents' knowledge, belief, desire and intention. Based on this Kripke model, we developed some model checking techniques for the verification of MAS. The temporal epistemic logics used here are derived from the branching-time logic CTL* by incorporating these epistemic modalities representing agents' knowledge, belief, desire and intention. The temporal epistemic logics are of great expressive power in both temporal and epistemic dimensions. It is convenient for users to specify agents' mental states and the temporal evolution of these. Therefore, the research achievements of this dissertation extend and enrich state-of-the-art model checking techniques for MAS in both temporal and epistemic dimensions.