Model Checking Action-Based Temporal Epistemic Logic For Multi-Agent Systems

Researchers are paying more and more attention to model checking multi-agent system when analyzing the distributed system. The traditional temporal logic can model and check the temporal specification of a multi-agent system. But the model checking of the multi-agent system is working in the direction of verifying the more and more personate specification. With regard to the situation of some agents collaborate to enforce a system specification, the traditional temporal logic can’t handle. In addition, the modeling and verifying about knowledge of a multi-agent system, is also a very import scientific question.A kind of temporal and epistemic logic based on action we put forward can effectively describe the protocol and epistemic specification of the multi-agent system. This logic can be divided into temporal part and epistemic part: the temporal part consists of linear time and furcation time;the epistemic part is to enlarge the form of knowledge, adding the form of“everybody know” and “common knowledge”. How to check the formulas describing the case of some agents collaborate to enforce a system specification and the formulas of knowledge about an agent or some agents,may be the key technology when model checking action based temporal epistemic logic. We put forward a mixed transition system model called MTS.At the base of the MTS, we designed some model checking algorithms to check all kinds of ATL*K formulas.Our research contents can be summarized as follows:(1) According to the traditional Kripke structure of the multi-agent system,we put forward interpretation model IS and induced model M based on action. We also give out the describing language and syntax rules.(2) We put forward ATL*K logic and semantic interpretation system based on the model M. This logic mixes the linear time logic, alternating time logic and epistemic logic together. So it has greater ability than ATLK and CTL*K logics.(3) Using a method of post projection, we can map the action valuables into state valuables, and form a new kind of action state tuple, called AST. Based on AST,we put forward MTS as a mixed transition system model. So that the decision problem of model checking based on the model M, has changed to whether a MTS could satisfy an ATL*K formula. Depending on the MTS, we provide the theoretical proving and application process of the model checking about the ATL*K formulas, combining with the theory of fixpoint operation and local proposition.(4) Having applied our theory of model checking into the tool MCTK, we use it to check the ATL*K specification of the “Prisoners and Light Bulb” problem.