Quantifying over coalitions in epistemic logic

ABSTRACT

Some natural epistemic properties which may arise in applications can only be expressed in standard epistemic logic by formulae which are exponentially long in the number of agents in the system. An example is the property "at least m agents know that at most n agents know φ". We present Epistemic Logic with Quantification over Coalitions (ELQC), where the standard common knowledge operator has been replaced allowing expressions of the form <φ> and [P]cφ where P is a coalition predicate, meaning that there is a coalition satisfying P which have common knowledge of φ and that all coalitions satisfying P have common knowledge of φ, respectively; and similarly for distributed knowledge and everybody-knows. While the language is no more expressive than standard epistemic logic, it is exponentially more succinct. We give a sound and complete axiomatisation for ELQC, and characterise the complexity of its model checking problem.

REFERENCES

• 1: T. Ågotnes, W. van der Hoek, and M. Wooldridge. Quantified coalition logic. In Proc. IJCAI-07, 2007.
• 2: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
• 3: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 4: Joseph Y. Halpern , Yoram Moses, A guide to completeness and complexity for modal logics of knowledge and belief, Artificial Intelligence, v.54 n.3, p.319-379, April 1992 [doi>10.1016/0004-3702(92)90049-4]
• 5: B. Kooi. Dynamic term-modal logic. In A Meeting of the Minds, pages 173--186, College Publications, 2007.
• 6: François Laroussinie , Nicolas Markey , Ph. Schnoebelen, Model Checking CTL+ and FCTL is Hard, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.318-331, April 02-06, 2001
• 7: Carsten Lutz, Complexity and succinctness of public announcement logic, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan [doi>10.1145/1160633.1160657]
• 8: John-Jules Ch Meyer , Wiebe Van Der Hoek, Epistemic Logic for AI and Computer Science, Cambridge University Press, New York, NY, 1995
• 9: C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
• 10: F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Jnl of Appl. Logic, 5:235--251, 2007.
• 11: H. van Ditmarsch, W. van der Hoek, and B. Kooi. Dynamic Epistemic Logic, volume 337 of Synthese Library. Springer-Verlag, 2007.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.4 Knowledge Representation Formalisms and Methods

General Terms:
Theory

Keywords:
complexity, epistemic logic, expressivity, model checking, succinctness