Making Model Checking Scalable: Implementing Succinct Kripke Models for Public Announcement Logic
Maickel Hartlief · 2020
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.