I am trying to program a model checker for dynamic epistemic logic, but I am not quite sure how to do it.
As far as I understand, model checking means to take a propositional formula and go through the model's states and check if the propositional formula holds.
But how should this be done? For instance, I want to check if the statement
$$ (M,w) \vDash (\color{red}{A} \land K_A \color{red}{A}) \land (\color{blue}{C}\land K_C \color{blue}{C}) $$
holds in the card example on the wikipedia page provided in the link above.
What would my approach be? I guess I should parse the statement and go through every single epistemic state $(M,w)$ in the epistemic model $M$ and check if it holds.
But what would I check against? Do there exist some algorithm to do this?