論文の概要: Automata for Hyperlanguages

• arxiv url: http://arxiv.org/abs/2002.09877v1
• Date: Sun, 23 Feb 2020 09:52:20 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-29 09:45:35.921453
• Title: Automata for Hyperlanguages
• Title（参考訳）: ハイパー言語のためのオートマトン
• Authors: Borzoo Bonakdarpour and Sarai Sheinvald
• Abstract要約: Hyperpropertiesは、従来のトレースプロパティを一連の実行トレースから一連の実行トレースへと持ち上げる。 単語集合上の言語であるemハイパーランゲージのためのハイパーオートマタを導入する。 非空さは一般には決定できないが、NFHのいくつかの断片に対して決定可能であることを示す。
• 参考スコア（独自算出の注目度）: 0.913755431537592
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Hyperproperties lift conventional trace properties from a set of execution traces to a set of sets of execution traces. Hyperproperties have been shown to be a powerful formalism for expressing and reasoning about information-flow security policies and important properties of cyber-physical systems such as sensitivity and robustness, as well as consistency conditions in distributed computing such as linearizability. Although there is an extensive body of work on automata-based representation of trace properties, we currently lack such characterization for hyperproperties. We introduce hyperautomata for em hyperlanguages, which are languages over sets of words. Essentially, hyperautomata allow running multiple quantified words over an automaton. We propose a specific type of hyperautomata called nondeterministic finite hyperautomata (NFH), which accept regular hyperlanguages. We demonstrate the ability of regular hyperlanguages to express hyperproperties for finite traces. We then explore the fundamental properties of NFH and show their closure under the Boolean operations. We show that while nonemptiness is undecidable in general, it is decidable for several fragments of NFH. We further show the decidability of the membership problem for finite sets and regular languages for NFH, as well as the containment problem for several fragments of NFH. Finally, we introduce learning algorithms based on Angluin's L-star algorithm for the fragments NFH in which the quantification is either strictly universal or strictly existential.
• Abstract（参考訳）: ハイパープロペラティは、実行トレースのセットから実行トレースのセットへの従来のトレースプロパティを持ち上げる。 ハイパープロペラティ(hyperproperties)は、情報フローセキュリティポリシーや、感度や堅牢性といったサイバー物理システムの重要な特性や、線形化可能性のような分散コンピューティングにおける一貫性条件を表現・推論するための強力な形式である。 トレース特性のオートマトンに基づく表現には幅広い研究があるが、現時点では超越性の特徴が欠如している。 単語集合上の言語であるemハイパーランゲージのためのハイパーオートマタを導入する。 本質的には、ハイパーオートマタはオートマトン上で複数の定量化された単語を実行できる。 非決定論的有限超オートマタ (NFH) と呼ばれる特定のタイプの超オートマタを提案する。 有限トレースに対して正規ハイパー言語がハイパープロパティを表現する能力を示す。 次にnfhの基本特性を調べ、ブール演算の下でそれらの閉包を示す。 非空さは一般には決定できないが、NFHのいくつかの断片に対して決定可能であることを示す。 さらに,NFH の有限集合および正規言語に対するメンバシップ問題の決定可能性,および NFH のいくつかの断片に対する包含問題を示す。 最後に、量子化が厳密な普遍的あるいは厳密な存在であるフラグメントNFHに対して、AngluinのL-starアルゴリズムに基づく学習アルゴリズムを導入する。

関連論文リスト

• IDEAL: Leveraging Infinite and Dynamic Characterizations of Large Language Models for Query-focused Summarization [59.06663981902496]
  クエリ中心の要約(QFS)は、特定の関心事に答え、より優れたユーザ制御とパーソナライゼーションを可能にする要約を作成することを目的としている。 本稿では,LLMを用いたQFSモデル,Longthy Document Summarization,およびクエリ-LLMアライメントの2つの重要な特徴について検討する。 これらのイノベーションは、QFS技術分野における幅広い応用とアクセシビリティの道を開いた。
  論文  参考訳（メタデータ） (2024-07-15T07:14:56Z)
• Exploring State Space and Reasoning by Elimination in Tsetlin Machines [14.150011713654331]
  Tsetlin Machine(TM)は機械学習(ML)において大きな注目を集めている。 TMは、単語の埋め込みを構築し、節を使ってターゲット語を記述するために使われる。 これらの節の記述能力を高めるために,節の定式化におけるReasoning by Elimination(RbE)の概念を検討した。
  論文  参考訳（メタデータ） (2024-07-12T10:58:01Z)
• Non-Deterministic Planning for Hyperproperty Verification [4.726777092009553]
  提案手法は,ハイパープロパティの自動検証に強力な中間言語を提供することを示す。 本稿では,HyperLTL検証問題に対して,非決定論的マルチエージェント計画インスタンスを構築するアルゴリズムを提案する。 提案手法は,HyperLTLの大きな断片に対して,従来のFOND,あるいはPOND計画問題に対応していることを示す。
  論文  参考訳（メタデータ） (2024-05-22T09:57:49Z)
• Sparse Feature Circuits: Discovering and Editing Interpretable Causal Graphs in Language Models [55.19497659895122]
  本稿ではスパース特徴回路の発見と適用方法を紹介する。 これらは言語モデルの振る舞いを説明するための人間の解釈可能な特徴の因果関係の著作である。
  論文  参考訳（メタデータ） (2024-03-28T17:56:07Z)
• A General and Flexible Multi-concept Parsing Framework for Multilingual Semantic Matching [60.51839859852572]
  我々は,テキストを多言語セマンティックマッチングのためのマルチコンセプトに分解し,NERモデルに依存するモデルからモデルを解放することを提案する。 英語データセットのQQPとMRPC、中国語データセットのMedical-SMについて包括的な実験を行った。
  論文  参考訳（メタデータ） (2024-03-05T13:55:16Z)
• From Hypergraph Energy Functions to Hypergraph Neural Networks [94.88564151540459]
  パラメータ化されたハイパーグラフ正規化エネルギー関数の表現型族を示す。 次に、これらのエネルギーの最小化がノード埋め込みとして効果的に機能することを実証する。 提案した双レベルハイパーグラフ最適化と既存のGNNアーキテクチャを共通的に用いている。
  論文  参考訳（メタデータ） (2023-06-16T04:40:59Z)
• Non-Separable Multi-Dimensional Network Flows for Visual Computing [62.50191141358778]
  本研究では,非分離型多次元ネットワークフローに対する新しい定式化法を提案する。 フローは次元ごとに定義されるので、最大化フローは自動的に最適な特徴次元を選択する。 概念実証として,マルチオブジェクト追跡問題にフォーマリズムを適用し,ノイズに対するロバスト性の観点からMOT16ベンチマークのスカラー定式化よりも優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-15T13:21:44Z)
• On the Complexity of Rational Verification [5.230352342979224]
  合理的検証とは、同時マルチエージェントシステムの時間論理特性が保持する問題を指す。 合理的な検証の複雑さは仕様によって大幅に低減できることを示す。 平均支払ユーティリティ関数によって与えられるプレイヤーの目標を考慮した場合、合理的な検証のための改善された結果を提供する。
  論文  参考訳（メタデータ） (2022-07-06T12:56:22Z)
• Characterizing the Program Expressive Power of Existential Rule Languages [4.38078043834754]
  既存のルール言語は、in-mediated query answering (OMQA)で広く使われている。 プログラム表現力として知られるOMQAのドメイン知識を表現する表現力はまだ十分に理解されていない。 本稿では,いくつかの重要なルール言語のプログラム表現力について,新しい特徴を多数確立する。
  論文  参考訳（メタデータ） (2021-12-15T14:08:38Z)
• Improve Variational Autoencoder for Text Generationwith Discrete Latent Bottleneck [52.08901549360262]
  変分オートエンコーダ(VAE)は、エンドツーエンドの表現学習において必須のツールである。 VAEは強い自己回帰デコーダで潜伏変数を無視する傾向がある。 よりコンパクトな潜在空間において暗黙的な潜在特徴マッチングを強制する原理的アプローチを提案する。
  論文  参考訳（メタデータ） (2020-04-22T14:41:37Z)

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

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