論文の概要: On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach

• arxiv url: http://arxiv.org/abs/2003.06492v3
• Date: Fri, 3 Jul 2020 13:44:36 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-24 02:08:06.202310
• Title: On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach
• Title（参考訳）: 有界ctlにおける十分かつ必要条件について:忘れるアプローチ
• Authors: Renyan Feng, Erman Acar, Stefan Schlobach, Yisong Wang, Wanwei Liu
• Abstract要約: 計算木論理(CTL)における忘れ書きに基づくアプローチを導入する。 本研究では, 与えられたモデルの下で, 与えられたシグネチャ上で, 最強必要条件 (SNC) と最弱十分条件 (WSC) を計算できることを示す。 また, その理論的性質について考察し, 忘れることの概念が, 知識を忘れることの本質的な仮定を満足させることを示す。
• 参考スコア（独自算出の注目度）: 3.9461038686072847
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design points of view, some information content of such property might become irrelevant for the system due to various reasons, e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existing specifications over a given signature. Moreover, in such a scenario, two crucial notions are informative: the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a given property. To address such a scenario in a principled way, we introduce a forgetting-based approach in CTL and show that it can be used to compute SNC and WSC of a property under a given model and over a given signature. We study its theoretical properties and also show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting. Furthermore, we analyse the computational complexity of some basic reasoning tasks for the fragment CTL_AF in particular.
• Abstract（参考訳）: 計算木論理(ctl)は形式的検証における中心的な形式の一つである。 仕様言語として、手元にあるシステムが満たすであろう特性を表現するために使用される。 検証とシステム設計の観点からは、様々な理由により、そのような財産の情報内容がシステムに無関係になる場合があり、例えば、時間が経つにつれて時代遅れになる場合や、実際的な困難のために実現不可能になる場合がある。 そして、関連するシステム動作を変更したり、所定のシグネチャに対して既存の仕様に違反したりすることなく、そのような情報を減じる方法について問題が発生する。 さらに、そのようなシナリオでは、最強必要条件(SNC)と最弱十分条件(WSC)という2つの重要な概念が有益である。 このようなシナリオを原則的に解決するために、CTL に忘れ書きに基づくアプローチを導入し、与えられたモデルと与えられたシグネチャ上でのプロパティの SNC と WSC の計算に使用できることを示す。 我々は,その理論的性質を考察し,その概念が既存の知識の前提を満たすことを示す。 さらに,特にフラグメント ctl_af に対する基本的な推論タスクの計算複雑性を分析した。

関連論文リスト

• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  トークン化とは、アルファベット上の文字の文字列を語彙上のトークンの列に変換するプラクティスである。 本稿では,トークン化の基礎を形式的観点から説明する。
  論文  参考訳（メタデータ） (2024-07-16T11:12:28Z)
• Identifiable Causal Representation Learning: Unsupervised, Multi-View, and Multi-Environment [10.814585613336778]
  因果表現学習は、機械学習のコアとなる強みと因果性を組み合わせることを目的としている。 この論文は、CRLが直接の監督なしに何が可能であるかを調査し、理論的基礎に寄与する。
  論文  参考訳（メタデータ） (2024-06-19T09:14:40Z)
• Retrieval-Augmented Mining of Temporal Logic Specifications from Data [0.46040036610482665]
  この研究は、観測された振る舞いからデータ駆動的な方法でSTL要求を学習するタスクに対処する。 本稿では,ベイズ最適化(BO)と情報検索(IR)技術を組み合わせて,STL式の構造とパラメータを同時に学習する新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-05-23T09:29:00Z)
• Neuro-Symbolic Causal Reasoning Meets Signaling Game for Emergent Semantic Communications [71.63189900803623]
  創発的SCシステムフレームワークを提案し,創発的言語設計のためのシグナリングゲームと因果推論のためのニューロシンボリック(NeSy)人工知能(AI)アプローチで構成されている。 ESCシステムは、意味情報、信頼性、歪み、類似性の新たな指標を強化するように設計されている。
  論文  参考訳（メタデータ） (2022-10-21T15:33:37Z)
• On the Complexity of Rational Verification [5.230352342979224]
  合理的検証とは、同時マルチエージェントシステムの時間論理特性が保持する問題を指す。 合理的な検証の複雑さは仕様によって大幅に低減できることを示す。 平均支払ユーティリティ関数によって与えられるプレイヤーの目標を考慮した場合、合理的な検証のための改善された結果を提供する。
  論文  参考訳（メタデータ） (2022-07-06T12:56:22Z)
• Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
  このような問題に対する一般的なフレームワークとして,第2レベル代数モデルカウント (2AMC) を導入している。 KC(Knowledge Compilation)に基づく第1レベルのテクニックは、変数順序制約を課すことで、特定の2AMCインスタンスに適応している。 2AMC問題の論理構造を利用して、これらの制約の一部を省略し、負の効果を制限できることが示される。
  論文  参考訳（メタデータ） (2022-05-16T08:10:40Z)
• The Causal Neural Connection: Expressiveness, Learnability, and Inference [125.57815987218756]
  構造因果モデル (Structuor causal model, SCM) と呼ばれるオブジェクトは、調査中のシステムのランダムな変動のメカニズムと源の集合を表す。 本稿では, 因果的階層定理 (Thm. 1, Bareinboim et al., 2020) がまだニューラルモデルに対して成り立っていることを示す。 我々はニューラル因果モデル(NCM)と呼ばれる特殊なタイプのSCMを導入し、因果推論に必要な構造的制約をエンコードする新しいタイプの帰納バイアスを定式化する。
  論文  参考訳（メタデータ） (2021-07-02T01:55:18Z)
• Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming [8.677108656718824]
  イベント計算(英: Event Calculus、EC)は、常識推論を健全で論理的な基礎でモデル化する形式主義の一群である。 ECを用いた推論の機械化の試みは、高密度領域における連続的な変化の処理に困難に直面した。 我々は、ECシナリオが自然に、直接、s(CASP)にエンコードされる方法と、誘引的および誘引的推論タスクを実現する方法を示す。
  論文  参考訳（メタデータ） (2021-06-28T10:43:25Z)
• Structural Causal Models Are (Solvable by) Credal Networks [70.45873402967297]
  因果推論は、干潟網の更新のための標準的なアルゴリズムによって得ることができる。 この貢献は, 干潟ネットワークによる構造因果モデルを表現するための体系的なアプローチと見なされるべきである。 実験により, 実規模問題における因果推論には, クレーダルネットワークの近似アルゴリズムがすぐに利用できることがわかった。
  論文  参考訳（メタデータ） (2020-08-02T11:19:36Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
  論文  参考訳（メタデータ） (2020-06-05T10:56:52Z)
• CSNE: Conditional Signed Network Embedding [77.54225346953069]
  署名されたネットワークは、友人/フォアや信頼/不信のようなエンティティ間の正と負の関係を符号化する。 サイン予測のための既存の埋め込み手法は、一般に最適化関数におけるステータスやバランス理論の異なる概念を強制する。 条件付き符号付きネットワーク埋め込み(CSNE)を導入する。 我々の確率論的アプローチは、きめ細かな詳細とは別途、ネットワーク内の記号に関する構造情報をモデル化する。
  論文  参考訳（メタデータ） (2020-05-19T19:14:52Z)

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

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