Model checking knowledge, strategies, and games in multi-agent systems
Alessio R. Lomuscio, Franco Raimondi · 2006
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.