論文の概要: Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model
Checking Dynamic Epistemic Logic
- arxiv url: http://arxiv.org/abs/2307.05067v1
- Date: Tue, 11 Jul 2023 07:13:09 GMT
- ステータス: 処理完了
- システム内更新日: 2023-07-12 16:02:49.548907
- Title: Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model
Checking Dynamic Epistemic Logic
- Title(参考訳): 論理パズルにおける爆発的非対称性:動的エピステミック論理のシンボリックモデルにおけるZDDの利用
- Authors: Daniel Miedema (Bernoulli Institute, University of Groningen), Malvin
Gattinger (ILLC, University of Amsterdam)
- Abstract要約: 我々は、動的疫学論理で使用されるクリプキモデルを象徴的に符号化するためにZDDを使用する。
BDDを適切なZDDに置き換えることで、メモリ使用量を大幅に削減できることを示す。
これはZDDがマルチエージェントシステムのモデル検査に有用なツールであることを示唆している。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract(参考訳): バイナリ意思決定図(BDD)は、モデルチェックにおける状態展開の問題を軽減するために広く使われます。
BDDのバリエーションはゼロ抑圧決定図(ZDD)で、重要でない変数を省略するのではなく、偽でなければならない変数を省略する。
我々はZDDを用いて、マルチエージェントシステムにおける知識と情報力学を推論するフレームワークであるDynamic Epistemic Logicで使用されるKripkeモデルを象徴的に符号化する。
文献からよく知られた3つの例(Muddy Children, the Sum and Product puzzle, the Dining Cryptographers)に対して、異なるZDDのメモリ使用率を比較した。
本実装は,既存のモデルチェッカーSMCDELとCUDDライブラリをベースとしている。
その結果,BDDを適切なZDDに置き換えることで,メモリ使用量を大幅に削減できることがわかった。
これはZDDがマルチエージェントシステムのモデル検査に有用なツールであることを示唆している。
関連論文リスト
- MORBDD: Multiobjective Restricted Binary Decision Diagrams by Learning
to Sparsify [19.821484909092913]
まず、問題に対するすべての実行可能なソリューションを表すグラフを構築するバイナリ意思決定図(BDD)に注目します。
機械学習(ML)を用いて、制限されたBDDが多目的最適化にどのように適応できるかを検討する。
MorBDDは、非常に小さな制限されたBDDを、優れた近似品質で、幅制限の制限されたBDDよりも優れ、よく知られた進化的アルゴリズムNSGA-IIを作るのに非常に効果的です。
論文 参考訳(メタデータ) (2024-03-04T21:04:54Z) - Variants of Tagged Sentential Decision Diagrams [6.891570850234007]
最近提案されたブール関数の標準形式、すなわちタグ付き逐次決定図(TSDD)は、標準およびゼロ抑圧トリミングルールの両方を利用する。
本稿では,トリミング規則の順序を逆転することで,標準TSDD(STSDD)と呼ぶTSDDの変種について述べる。
次に、STSDDの正準性を証明し、TSDD上でのバイナリ演算のアルゴリズムを示す。
論文 参考訳(メタデータ) (2023-11-16T12:29:25Z) - Interpretability at Scale: Identifying Causal Mechanisms in Alpaca [62.65877150123775]
本研究では、Boundless DASを用いて、命令に従う間、大規模言語モデルにおける解釈可能な因果構造を効率的に探索する。
私たちの発見は、成長し、最も広くデプロイされている言語モデルの内部構造を忠実に理解するための第一歩です。
論文 参考訳(メタデータ) (2023-05-15T17:15:40Z) - Optimizing Binary Decision Diagrams with MaxSAT for classification [3.2894524838755608]
説明可能な人工知能への関心の高まりは、解釈可能な機械学習(ML)モデルの必要性を動機付けている。
近年、従来の手法の弱点を克服するために、そのようなモデルを計算するためのいくつかの正確な方法が提案されている。
本稿ではまず,最適なバイナリ決定図(BDD)を学習するためのSATモデルを提案する。
次に、符号化をMaxSATモデルに上げ、限られた深さで最適なBDDを学習します。
最後に、MaxSATモデルを介して見つけたBDDの互換性のあるサブツリーをマージする手法を導入することにより、フラグメンテーションの問題に取り組む。
論文 参考訳(メタデータ) (2022-03-21T23:17:37Z) - Belief Revision in Sentential Decision Diagrams [126.94029917018733]
本研究では,Dalリビジョンの構文的特徴化に基づくSDDの一般的なリビジョンアルゴリズムを開発する。
ランダムに生成した知識ベースを用いた予備実験は、SDDフォーマリズム内で直接リビジョンを行う利点を示している。
論文 参考訳(メタデータ) (2022-01-20T11:01:41Z) - Discrete Auto-regressive Variational Attention Models for Text Modeling [53.38382932162732]
変分オートエンコーダ(VAE)はテキストモデリングに広く応用されている。
情報不足と後部崩壊という2つの課題に悩まされている。
本稿では,自己回帰変動注意モデル(DAVAM)を提案する。
論文 参考訳(メタデータ) (2021-06-16T06:36:26Z) - Discriminative-Generative Dual Memory Video Anomaly Detection [81.09977516403411]
近年,ビデオ異常検出(VAD)には,トレーニングプロセス中に通常のデータに代えて,いくつかの異常を使おうと試みている。
本稿では,いくつかの異常を生かしてデータの不均衡を解決するために,識別生成型デュアルメモリ(dream)異常検出モデルを提案する。
論文 参考訳(メタデータ) (2021-04-29T15:49:01Z) - Coded Stochastic ADMM for Decentralized Consensus Optimization with Edge
Computing [113.52575069030192]
セキュリティ要件の高いアプリケーションを含むビッグデータは、モバイルデバイスやドローン、車両など、複数の異種デバイスに収集され、格納されることが多い。
通信コストとセキュリティ要件の制限のため、核融合センターにデータを集約するのではなく、分散的に情報を抽出することが最重要となる。
分散エッジノードを介してデータを局所的に処理するマルチエージェントシステムにおいて,モデルパラメータを学習する問題を考える。
分散学習モデルを開発するために,乗算器アルゴリズムの最小バッチ交互方向法(ADMM)のクラスについて検討した。
論文 参考訳(メタデータ) (2020-10-02T10:41:59Z) - Variable Shift SDD: A More Succinct Sentential Decision Diagram [10.91026094237478]
Sentential Decision Diagram (SDD) はブール関数の抽出可能な表現である。
可変シフトSDD(VS-SDD)という,より簡潔なSDD変種を提案する。
我々は,VS-SDDがSDDよりも大きくなることはなく,VS-SDDのサイズがSDDよりも指数関数的に小さいケースがあることを示した。
論文 参考訳(メタデータ) (2020-04-06T09:18:19Z) - Ordered Functional Decision Diagrams: A Functional Semantics For Binary
Decision Diagrams [0.0]
我々は、純粋に機能的な観点からバイナリ決定ダイアグラムを再検討する、$lambda$DDと呼ばれる新しいフレームワークを紹介します。
我々は、原則的に、このクラスのすべてのモデルを列挙し、最も表現力のあるモデルを分離する。
論文 参考訳(メタデータ) (2020-03-20T15:46:48Z) - Simple and Effective Prevention of Mode Collapse in Deep One-Class
Classification [93.2334223970488]
深部SVDDにおける超球崩壊を防止するための2つの正則化器を提案する。
第1の正則化器は、標準のクロスエントロピー損失によるランダムノイズの注入に基づいている。
第2の正規化器は、小さすぎるとミニバッチ分散をペナライズする。
論文 参考訳(メタデータ) (2020-01-24T03:44:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。