Verifying Epistemic Properties of Multi-agent Systems via Action-Based Temporal Logic

This paper provides a specifying and verifying framework of a multi-agent system, with the emphasis on their epistemic features. We use an epistemic transition system to specify the agents and an epistemic synchronous product to specify the multi-agent system.We verify the system by means of a special action-based temporal logic - ACTLW for Epistemic Reasoning (ACTLW stands for Action Computation Tree Logic with Unless Operator). Using temporal and epistemic operators we create the appropriate formulae to perform model checking for the system. We test our method by the example of security communication protocol called Dining Cryptographers.