SMCDEL

SMCDEL: A symbolic model checker for Dynamic Epistemic Logic (DEL) implemented in Haskell. At its core is a translation of epistemic and dynamic formulas to boolean formulas which are represented as Binary Decision Diagrams (BDDs). You can try SMCDEL online here: https://w4eg.de/malvin/illc/smcdelweb/