Model checking knowledge, strategies, and games in multi-agent systems

We present an OBDD-based methodology for verifying time, knowledge, and strategies in multi-agent systems specified by the formalism of interpreted systems. To this end, we investigate the interpretation of ATL and epistemic formulae in various classes of interpreted systems, we present model checking algorithms and their implementation, and report experimental results. General Terms Theory;Verification,Algorithms Keywords Model checking multi-agent systems; ATL

• Type: Conference
• Year: 2006
• Where: ATAL
• Authors: Alessio Lomuscio, Franco Raimondi
• Keywords: ATAL 2006, Intelligent Agents, Interpreted Systems, Model Checking, Multi-agent Systems