  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.
