Verification of Multi-Agent Systems via SDD-Based Model Checking

Considerable progress has been achieved in the past ten years in the symbolic verification of Multi-Agent Systems (MAS). One of the most efficient techniques put forward is based on the use of ordered binary decision diagrams (OB-DDs) for representing the state space and computing the states at which specifications hold. Sentential Decision Diagrams (SDDs) have recently been put forward as an alternative symbolic representation for Boolean formulas in knowledge representation. In this abstract we report some preliminary results on the applicability of SDDs for the verification of MAS.