A symbolic model checker for Dynamic Epistemic Logic.
GPL-2.0 License
A symbolic model checker for Dynamic Epistemic Logic.
You can try SMCDEL online here: https://w4eg.de/malvin/illc/smcdelweb/
stack install
will build and install an executable smcdel
~/.local/bin
which should be in your PATH
variable.Create a text file MuddyShort.smcdel.txt
which describes the knowledge structure and the formulas you want to check for truth or validity:
-- Three Muddy Children in SMCDEL
VARS 1,2,3
LAW Top
OBS alice: 2,3
bob: 1,3
carol: 1,2
WHERE?
[ ! (1|2|3) ] alice knows whether 1
VALID?
[ ! (1|2|3) ]
[ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ]
[ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ]
(alice,bob,carol) comknow that (1 & 2 & 3)
Run smcdel MuddyShort.smcdel.txt
resulting in:
>> smcdel MuddyShort.smcdel.txt
SMCDEL 1.0 by Malvin Gattinger -- https://github.com/jrclogic/SMCDEL
At which states is ... true?
[]
[1]
Is ... valid on the given structure?
True
More example files are in the folder Examples.
To also build and install the web interface, run stack install --flag smcdel:web
Then you can run smcdel-web
and open http://localhost:3000.
The executables only provide model checking for S5 with public announcements. For K and to define more complex models and updates, SMCDEL should be used as a Haskell library. Please refer to the Haddock documentation for each module.
Examples can be found in the folders src/SMCDEL/Examples and bench.
Dependencies:
To get all visualisation functions working, graphviz, dot2tex and some LaTeX packages should be installed.
On Debian, please do sudo apt install graphviz dot2tex libtinfo5 texlive-latex-base poppler-utils preview-latex-style texlive-pstricks
.
SMCDEL uses different BDD packages.
Data.HasCacBDD which runs CacBDD from http://kailesu.net/CacBDD/.
This is the default choice used by the executables and the modules Symbolic.S5
and Symbolic.K
.
The pure Haskell library decision-diagrams
.
It is used by the module Symbolic.S5_DD
.
Optionally, Cudd (with some patches)
which uses the CUDD library.
To obtain the modules SMCDEL.Symbolic.S5_CUDD
, SMCDEL.Symbolic.S5_K
, SMCDEL.Symbolic.S5_Ki
you should compile with stack build --flag smcdel:with-cudd
.
Main reference for the theory behind the implementation, also containing benchmarks:
Additional publications: