Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions

We put forward a specification language based on epistemic logic and a variant of the logic ATL interpreted on a three-valued semantics. We show that the model checking problem for multi-agent systems in this setting is tractable by giving a provably correct procedure which admits a PTime bound. We give a constructive technique for generating abstract approximations of concrete multiagent systems models and show that the truth values are preserved between abstract and concrete models. The talk will summarise the main results from A. Lomuscio and J. Michaliszyn. An abstraction technique for the verification of multi-agent systems against ATL specifications. In Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), pages 428–437. AAAI Press, 2014. A. Lomuscio and J. Michaliszyn. Verifying multi-agent systems by model checking three-valued abstractions. In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems (AAMAS15), pages 189–198, 2015.

Authors

• Jakub Michaliszyn

Keywords

No keywords are indexed for this paper.