A verification framework for agent knowledge

Abstract

One of the challenges for designing multi-agent systems is how to capture and reason about agent knowledge and knowledge evolution in a highly abstract and modular way. Hence it is very desirable to have a generic framework in which such systems can be conveniently specified and the properties verified under one umbrella. As a classical reasoning support, the model checking technique has proved to be applicable for systems of reasonable size. However current model checkers for epistemic logics suffer from the state explosion problem and their inability to handle infinite state problems. Prototype Verification System (PVS) is an environment for the development of formal specifications. It integrates a highly expressive specification language and a well supported theorem prover. In this paper, we demonstrate our attempt towards mechanizing epistemic logic reasoning by building a formal, sound and complete verification framework in PVS for reasoning about a spectrum of (dynamic) epistemic logics. © Springer-Verlag Berlin Heidelberg 2007.