Epistemic Model Checker

This is a model checker for verifying properties in epistemic models. The goal of the model checker is to check for Pluralistic Ignorace in complex scenarios and to probe its robustness. The motivation is based on the content of the paper [1].

Run the model checker by running run.py file using your favorite Python interpreter. This file takes two arguments, a model file and an epistemic logic formula:

python run.py model_file.em "(~p) \/ p"

Model file format:

{states}
{agents}
{agent}:({state}<={state}),...
...
{agent}:({state}<={state}),...
{state}:{proposition},...
...
{state}:{proposition},...

The models will be made transitive and reflexive upon parsing, so the user does not have to specify this. Here you can see an example model file:

s0,s1,s2
a,b
a:(s0<=s1),(s1<=s2)
b:(s2<=s0)
s1:q
s1:p
s2:p,r

This model contains three states, s0, s1 and s2 and two agents, a and b.

The formulas are written using the following operators:

• K = knowledge
• B = belief
• S = safe belief
• W = weakly safe belief
• T = strong belief
• I = ignorance
• D = doubt
• /\ = AND
• \/ = OR
• => = implication
• ~ = NOT
• (f1) ! (f2) = $[!\verb/f1/]\verb/f2/$

Some example formulas are shown below:

p /\ (~q)
I_a (D_b (p))
(K_a p) => (B_a p)
K_a ((B_b (~p)) ! (~(B_c (B_b (~p)))))

Please note that the parsing of parentheses can be tricky. If you encounter an error in the parse function, please try to add or remove some parentheses in the formula.

Future work

The following features would be nice to have:

• Better parsing of logic formulas
• Caching of results from intermediate steps
• Define formulas in files instead of in the command line

Bibliography

[1] Hansen, Jens Ulrik. "A logic-based approach to pluralistic ignorance." Proceedings of PhDs in Logic III. to appear (2012).