Towards Symbolic Factual Change in DEL

TL;DR

This paper extends symbolic model checking for Dynamic Epistemic Logic to include factual change, enabling more efficient verification of knowledge updates with a symbolic approach using BDDs.

Contribution

It introduces a symbolic method for DEL with factual change, using transformers and BDDs, applicable to S5 and general cases, improving model checking performance.

Findings

Provides a compact symbolic representation of action models.

Demonstrates the approach with Sally-Anne false belief task.

Expected to enhance model checking efficiency.

Abstract

We extend symbolic model checking for Dynamic Epistemic Logic (DEL) with factual change. Our transformers provide a compact representation of action models with pre- and postconditions, for both S5 and the general case. The method can be implemented using binary decision diagrams and we expect it to improve model checking performance. As an example we give a symbolic representation of the Sally-Anne false belief task.