A Formal Verification Method of Obligation Policy in Multi-agent System

In Multi-Agent System, obligations are actions that agents are required to take or some states of affairs which should be maintained, formal modeling and verifying obligation policy which is high-level requirements specifications or communication protocol for constraining agent interaction can enhance the correctness of the system design. In this paper, we present a formal framework for modeling obligation policy, the framework is formalized using concepts of social commitments, it allows reasoning about change in the states of obligations and provides Kripke operational semantics which can help to convert framework of obligation policy to the input model of model checker MCMAS, at the same time ,the properties of framework depending on policy conflicts are represented with CTL, and the violations of properties is detected by using MCMAS which can provide the counterexample and trace it back to the errors in interaction policy. Finally, we present an implementation and report on experimental results of verifying obligation policy using MCMAS model checker.