Imperative Implementations of a Public Announcement Logic Model Checker

Soicher, Gabriel (2021) Imperative Implementations of a Public Announcement Logic Model Checker. Bachelor's Thesis, Artificial Intelligence.

Preview	Text g_soicher_bachelor_thesis_s3661806.pdf Download (949kB) | Preview
	Text toestemming.pdf Restricted to Registered users only Download (128kB)

Abstract

Contemporary model checkers for Public Announcement Logic (PAL) and Dynamic Epistemic Logic (DEL) are mostly written in Haskell, which is not usually seen as an easy to optimise language. Haskell is pure, lazy, and functional, and so this thesis investigates if there are any performance improvements to be had by writing an explicit model checker for PAL in an imperative language, and comparing that to both symbolic (SMCDEL, Gattinger(2019)) and explicit (DEMOS5, van Eijck (2014)) checkers written in Haskell. This research covers implementations in Python, Go, Java, and C++ - all of which involve parallelisation of model generation and of model solving, as well as some additional features compared to contemporary Haskell solutions. The main finding of this research is that parallelisation accounts for a large performance gain for larger models -- the implementation of which is made easier due to the use of imperative languages -- but that symbolic model checkers still outperform even these parallel explicit model checkers; explicit model checkers are still relevant, but only in those areas where a symbolic checker has not yet been developed.

Item Type:	Thesis (Bachelor's Thesis)
Supervisor name:	Gattinger, B.R.M.
Degree programme:	Artificial Intelligence
Thesis type:	Bachelor's Thesis
Language:	English
Date Deposited:	02 Aug 2021 09:30
Last Modified:	02 Aug 2021 14:03
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/25365

Actions (login required)

View Item