Variable Forgetting in Reasoning about Knowledge
This work addresses knowledge representation and reasoning challenges in multi-agent systems, offering a potentially more efficient framework for automated analysis and verification, though it appears incremental as it builds on existing logical and computational concepts.
The paper tackles the problem of knowledge reasoning in multi-agent systems by introducing a knowledge structure framework that uses variable forgetting and weakest sufficient conditions to define agents' knowledge and common knowledge, and shows that the framework can be more succinct than traditional Kripke structures. It demonstrates computational complexity results, with the general problem being PSPACE-hard but reducible to co-NP in some subcases, and applies the framework to scenarios like the muddy children puzzle and protocol verification.
In this paper, we investigate knowledge reasoning within a simple framework called knowledge structure. We use variable forgetting as a basic operation for one agent to reason about its own or other agents\ knowledge. In our framework, two notions namely agents\ observable variables and the weakest sufficient condition play important roles in knowledge reasoning. Given a background knowledge base and a set of observable variables for each agent, we show that the notion of an agent knowing a formula can be defined as a weakest sufficient condition of the formula under background knowledge base. Moreover, we show how to capture the notion of common knowledge by using a generalized notion of weakest sufficient condition. Also, we show that public announcement operator can be conveniently dealt with via our notion of knowledge structure. Further, we explore the computational complexity of the problem whether an epistemic formula is realized in a knowledge structure. In the general case, this problem is PSPACE-hard; however, for some interesting subcases, it can be reduced to co-NP. Finally, we discuss possible applications of our framework in some interesting domains such as the automated analysis of the well-known muddy children puzzle and the verification of the revised Needham-Schroeder protocol. We believe that there are many scenarios where the natural presentation of the available information about knowledge is under the form of a knowledge structure. What makes it valuable compared with the corresponding multi-agent S5 Kripke structure is that it can be much more succinct.