jrclogic / SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.
https://w4eg.de/malvin/illc/smcdelweb
GNU General Public License v2.0
39 stars 9 forks source link

succinct semantics based on mental programs #44

Open m4lvin opened 3 months ago

m4lvin commented 3 months ago

A DEL semantics based on mental programs (a version of PDL) is given in

The goal of this issue will be to include such a semantics as a module SMCDEL.Succinct.K.

An implementation of succinct DEL has already been created in https://github.com/maickelhartlief/SucExpModelCheckers as part of the BSc thesis https://fse.studenttheses.ub.rug.nl/23607/

An updated fork is at https://github.com/m4lvin/SucExpModelCheckers - in particular using Data.Set to speed things up.