Symbolic Model Checking for Dynamic Epistemic Logic

摘要: Dynamic Epistemic Logic (DEL) can model complex information scenarios in a way that appeals to logicians. However, existing DEL implementations are ad-hoc, so we do not know how the framework really performs. For this purpose, want hook up with best available model-checking and SAT techniques computational logic. We by first providing bridge: new faithful representation of models as so-called knowledge structures allow for symbolic checking. Next, show now solve well-known benchmark problems epistemic much faster than methods. Finally, our method is just matter implementation, but it raises significant issues about logical update.