Zero-suppression Decision Diagrams versus Binary Decision Diagrams on Dynamic Epistemic Logic Model Checking

Miedema, Daniel (2022) Zero-suppression Decision Diagrams versus Binary Decision Diagrams on Dynamic Epistemic Logic Model Checking. Master's Thesis / Essay, Artificial Intelligence.

Preview	Text mAI_2022_MiedemaD.pdf Download (3MB) | Preview
	Text toestemming.pdf Restricted to Registered users only Download (122kB)

Abstract

In this thesis we first give a theoretical analysis of translating Dynamic Epistemic Logic (DEL) to physical memory for model checking tasks, afterwards we give an analysis of Binary Decision Diagrams (BDDs) and the four Zero-suppressed Decision Diagram variants (ZDDs) and how they provide advantages for the memory and computation speed for model checking tasks. The analysis sets forth an alternative explanation for the relation between BDDs and ZDD variants by comparing their node elimination rules with more general inference rules (when considering boolean function contexts over a possibly countable infinite variables). This is then used to explain why and when ZDDs and BDDs need to keep track of a context in their traversal algorithms and leads to proposing a new naming convention for the ZDD variants. Furthermore we identify a common graph-pattern indicative of ZDD efficiency (named XOR-domain), which can be considered novel in the context of symbolic model checking. We conclude with an experimental comparison between BDD and ZDD compactness on multiple classical DEL problems. For this we extend the SMCDEL, a program and theoretical framework for symbolic DEL model checking using BDDs, with ZDD functionality. Our results show that the right ZDD elimination rule, instead of the BDD elimination rule, can significantly reduce the decision diagrams used for model checking classical DEL puzzles (ranging from 6% to 54% fewer nodes).

Item Type:	Thesis (Master's Thesis / Essay)
Supervisor name:	Verbrugge, L.C.
Degree programme:	Artificial Intelligence
Thesis type:	Master's Thesis / Essay
Language:	English
Date Deposited:	14 Jun 2022 10:14
Last Modified:	14 Jun 2022 10:14
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/27287

Actions (login required)

View Item