Simple model checker for the Knowledge Based Logic KBL [1]. In KBL it is possible to reason about the knowledge of a group of users which are part of a social network. The reasoning machinery is based on the axiomatisation S5 of epistemic logic. Concretely, each user knowledge is modelled as a set of formulae, which we call the knowledge base of the user. Additionally, the logic includes special predicates to talk about relation between users and permissions related to the actions the users can execute in the social network.
[1] -> “Formalising Privacy Policies in Social Networks”. Raúl Pardo, Musard Balliu and Gerardo Schneider. In Journal of Logical and Algebraic Methods in Programming (JLAMP), 2016.