Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic

要約

二分決定図 (BDD) は、モデル チェックにおける状態爆発の問題を軽減するために広く使用されています。
BDD のバリエーションとして、重要でない変数を省略するのではなく、偽である必要がある変数を省略するゼロ抑制決定図 (ZDD) があります。
ZDD を使用して、マルチエージェント システムにおける知識と情報のダイナミクスを推論するためのフレームワークである動的認識論理で使用されるクリプキ モデルを記号的にエンコードします。
文献からの 3 つのよく知られた例 (Muddy Children、Sum and Product パズル、Dining Cryptographers) について、さまざまな ZDD バリアントのメモリ使用量を比較します。
私たちの実装は、既存のモデル チェッカー SMCDEL と CUDD ライブラリに基づいています。
私たちの結果は、BDD を ZDD の適切なバージョンに置き換えることで、メモリ使用量を大幅に削減できることを示しています。
これは、ZDD がマルチエージェント システムのモデル チェックに有用なツールであることを示唆しています。

要約(オリジナル)

Binary decision diagrams (BDDs) are widely used to mitigate the state-explosion problem in model checking. A variation of BDDs are Zero-suppressed Decision Diagrams (ZDDs) which omit variables that must be false, instead of omitting variables that do not matter. We use ZDDs to symbolically encode Kripke models used in Dynamic Epistemic Logic, a framework to reason about knowledge and information dynamics in multi-agent systems. We compare the memory usage of different ZDD variants for three well-known examples from the literature: the Muddy Children, the Sum and Product puzzle and the Dining Cryptographers. Our implementation is based on the existing model checker SMCDEL and the CUDD library. Our results show that replacing BDDs with the right variant of ZDDs can significantly reduce memory usage. This suggests that ZDDs are a useful tool for model checking multi-agent systems.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google