Mika Cohen

AAMAS Conference 2010 Conference Paper

Model checking detectability of attacks in multiagent systems

• Ioana Boureanu
• Mika Cohen
• Alessio Lomuscio

Information security is vital to many multiagent system applications. In this paper we formalise the notion of detectability of attacks in a MAS setting and analyse its applicability. We introduce a taxonomy of detectability specifications expressed in temporal-epistemic logic. We illustratethe practical relevance of attack detectability in a case studyapplied to a variant of Kerberos protocol. We model-checkattack detectability in automatically generated MAS modelsfor security protocols.

ECAI Conference 2010 Conference Paper

Non-elementary speed up for model checking synchronous perfect recall

• Mika Cohen
• Alessio Lomuscio

We consider the complexity of the model checking problem for the logic of knowledge and past time in synchronous systems with perfect recall. Previously established bounds are k-exponential in the size of the system for specifications with k nested knowledge modalities. We show that the upper bound for positive (respectively, negative) specifications is polynomial (respectively, exponential) in the size of the system irrespective of the nesting depth.

IJCAI Conference 2009 Conference Paper

• Mika Cohen
• Mads Dam
• Alessio Lomuscio
• Hongyang Qu

We introduce a symmetry reduction technique for model checking temporal-epistemic properties of multi-agent systems defined in the mainstream interpreted systems framework. The technique, based on counterpart semantics, aims to reduce the set of initial states that need to be considered in a model. We present theoretical results establishing that there are neither false positives nor false negatives in the reduced model. We evaluate the technique by presenting the results of an implementation tested against two well known applications of epistemic logic, the muddy children and the dining cryptographers. The experimental results obtained confirm that the reduction in model checking time can be dramatic, thereby allowing for the verification of hitherto intractable systems.

AAMAS Conference 2009 Conference Paper

Abstraction in Model Checking Multi-Agent Systems

• Mika Cohen
• Mads Dam
• Alessio Lomuscio

We present an abstraction technique for multi-agent systems preserving temporal-epistemic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain.