Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic
This work addresses memory efficiency in model checking for multi-agent systems, but it is incremental as it applies an existing method (ZDDs) to a specific domain.
The paper tackled the state-explosion problem in model checking for Dynamic Epistemic Logic by using Zero-suppressed Decision Diagrams (ZDDs) instead of Binary Decision Diagrams (BDDs), resulting in significantly reduced memory usage for multi-agent system examples like the Muddy Children puzzle.
Binary decision diagrams (BDDs) are widely used to mitigate the state-explosion problem in model checking. A variation of BDDs are Zero-suppressed Decision Diagrams (ZDDs) which omit variables that must be false, instead of omitting variables that do not matter. We use ZDDs to symbolically encode Kripke models used in Dynamic Epistemic Logic, a framework to reason about knowledge and information dynamics in multi-agent systems. We compare the memory usage of different ZDD variants for three well-known examples from the literature: the Muddy Children, the Sum and Product puzzle and the Dining Cryptographers. Our implementation is based on the existing model checker SMCDEL and the CUDD library. Our results show that replacing BDDs with the right variant of ZDDs can significantly reduce memory usage. This suggests that ZDDs are a useful tool for model checking multi-agent systems.