論文の概要: 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がマルチエージェントシステムのモデル検査に有用なツールであることを示唆している。

関連論文リスト

• Breaking Determinism: Fuzzy Modeling of Sequential Recommendation Using Discrete State Space Diffusion Model [66.91323540178739]
  シークエンシャルレコメンデーション(SR)は、ユーザーが過去の行動に基づいて興味を持つかもしれない項目を予測することを目的としている。 我々はSRを新しい情報理論の観点から再検討し、逐次モデリング手法がユーザの行動のランダム性と予測不可能性を適切に把握できないことを発見した。 ファジィ情報処理理論に触発された本論文では,制限を克服し,ユーザの関心事の進化をよりよく捉えるために,ファジィなインタラクションシーケンスの組を導入する。
  論文  参考訳（メタデータ） (2024-10-31T14:52:01Z)
• ZeroDDI: A Zero-Shot Drug-Drug Interaction Event Prediction Method with Semantic Enhanced Learning and Dual-Modal Uniform Alignment [11.290096354280111]
  以前は未観測/未確認のDDIEが登場しており、未確認のクラスがトレーニング段階でラベル付きインスタンスを持たない場合に、新しい分類タスクを呈している。 既存の計算手法はZS-DDIEには直接適用されないが、この方法には2つの主要な課題がある。 ZS-DDIEタスクのためのZeroDDIという新しい手法を提案する。これは重要な生物学的意味論を強調し、DDIE表現学習のための識別的分子サブ構造関連意味論を蒸留する。
  論文  参考訳（メタデータ） (2024-07-01T01:28:14Z)
• Long-Tailed Anomaly Detection with Learnable Class Names [64.79139468331807]
  性能評価のためのクラス不均衡とメトリクスのレベルが異なるデータセットをいくつか導入する。 次に、データセットのクラス名に頼ることなく、複数の長い尾を持つクラスから欠陥を検出する新しい手法LTADを提案する。 LTADは、ほとんどの形式のデータセットの不均衡に対して最先端の手法を大幅に上回っている。
  論文  参考訳（メタデータ） (2024-03-29T15:26:44Z)
• 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)
• Discriminative-Generative Dual Memory Video Anomaly Detection [81.09977516403411]
  近年,ビデオ異常検出(VAD)には,トレーニングプロセス中に通常のデータに代えて,いくつかの異常を使おうと試みている。 本稿では,いくつかの異常を生かしてデータの不均衡を解決するために,識別生成型デュアルメモリ(dream)異常検出モデルを提案する。
  論文  参考訳（メタデータ） (2021-04-29T15:49:01Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。