Knowledge forgetting in propositional μ-calculus

The mu-calculus is one of the most important logics describing specifications of transition systems. It has been extensively explored for formal verification in model checking due to its exceptional balance between expressiveness and algorithmic properties. From the perspective of systems/knowledge evolving, one may want to discard some atoms (elements) that become irrelevant or unnecessary in a specification; one may also need to know what makes something true, or the minimal condition under which something holds. This paper aims to address these scenarios for mu-calculus in terms of knowledge forgetting. In particular, it proposes a notion of forgetting based on a generalized bisimulation and explores the semantic and logical properties of forgetting, including some reasoning complexity results. It also shows that forgetting can be employed to perform knowledge update.