Hartlief, Maickel (2020) Making Model Checking Scalable: Implementing Succinct Kripke Models for Public Announcement Logic. Bachelor's Thesis, Artificial Intelligence.
|
Text
Maickel_Hartlief_Bachelor_Thesis.pdf Download (357kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (130kB) |
Abstract
Public Announcement Logic (PAL) is an extension of Propositional Logic including agents with knowledge about the world, and announcements that can be made to update the knowledge of these agents. Kripke Models for PAL can be extremely large, and model checkers slow. Aiming for a more efficient alternative, we consider a different representation: Succinct Kripke Models. This representation uses Mental Programs (based on Dynamic logic of propositional assignments) to describe the relations between worlds for agents, and a Boolean formula to denote the set of worlds, instead of listing all worlds and relations explicitly. Model checking is PSPACE-complete for both types of representations, but we still expect a difference in actual performance. To test this, we implemented the following in Haskell: a model checker for explicit Kripke models, a model checker for Succinct models, and an explicit and succinct model for the Muddy Children problem. The size of the succinct model is smaller than that of the explicit model, and this difference becomes larger for a higher number of children. The expectation is that the execution time for checking formulas will not be much larger. The results show that the succinct model checker is slower than the Kripke model checker, and that the difference grows for a higher number of children.
| 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: | 19 Nov 2020 09:57 |
| Last Modified: | 19 Nov 2020 09:57 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/23607 |
Actions (login required)
 |
View Item |