Decidability of Propositionally Quantified Logics of Knowledge

Abstract. Logics of knowledge have important applications for reasoning about security protocols and multi-agent systems. We extend the semantics for the logic of necessity with local propositional quantification L( ,,1,...k) introduced in [4] to allow reasoning about knowledge in more general (non-hierarchical) systems. We show that these new semantics preserve the properties of knowledge in a multi-agent system, give a significant and useful increase in expressivity and most importantly, have a decidable satisfiability problem. The new semantics interpret propositional (local and non-local) quantification with respect to bisimulations, and the satisfiability problem is shown to be solvable via an embedding into the temporal logic, QCTL.

• Type: Conference
• Year: 2003
• Where: AUSAI
• Authors: Tim French
• Keywords: Artificial Intelligence, AUSAI 2003, Local Propositional Quantification, Multi-agent System, Satisfiability Problem