Towards Symbolic Model Checking for Multi-Agent Systems via OBDD's

摘要

We present an algorithm for model checking temporal-epistemic properties of multi-agent systems, expressed in the formalism of interpreted systems. We first introduce a technique for the translation of interpreted systems into boolean formulae, and then present a model-checking algorithm based on this translation. The algorithm is based on ordered binary decision diagram's (OBDD's), as they offer a compact and efficient representation for boolean formulae.