論文の概要: Specification sketching for Linear Temporal Logic

• arxiv url: http://arxiv.org/abs/2206.06722v1
• Date: Tue, 14 Jun 2022 10:09:23 GMT
• ステータス: 処理完了
• システム内更新日: 2022-06-15 23:19:49.161033
• Title: Specification sketching for Linear Temporal Logic
• Title（参考訳）: 線形時相論理のための仕様スケッチ
• Authors: Simon Lutz, Daniel Neider and Rajarshi Roy
• Abstract要約: 線形時相論理(LTL)のための仕様スケッチという,形式仕様を書くための基本的新しいアプローチを提案する。 鍵となるアイデアは、エンジニアがスケッチと呼ばれる部分的な公式を提供することができることだ。 そこで本研究では,スケッチが完成するかどうかを複雑性クラスNPに分類し,SATベースのスケッチアルゴリズムを2つ提示する。
• 参考スコア（独自算出の注目度）: 3.3946853660795893
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: Virtually all verification and synthesis techniques assume that the formal specifications are readily available, functionally correct, and fully match the engineer's understanding of the given system. However, this assumption is often unrealistic in practice: formalizing system requirements is notoriously difficult, error-prone, and requires substantial training. To alleviate this severe hurdle, we propose a fundamentally novel approach to writing formal specifications, named specification sketching for Linear Temporal Logic (LTL). The key idea is that an engineer can provide a partial LTL formula, called an LTL sketch, where parts that are hard to formalize can be left out. Given a set of examples describing system behaviors that the specification should or should not allow, the task of a so-called sketching algorithm is then to complete a given sketch such that the resulting LTL formula is consistent with the examples. We show that deciding whether a sketch can be completed falls into the complexity class NP and present two SAT-based sketching algorithms. We also demonstrate that sketching is a practical approach to writing formal specifications using a prototype implementation.
• Abstract（参考訳）: 事実上すべての検証と合成技術は、正式な仕様が容易に利用可能であり、機能的に正しく、与えられたシステムに対するエンジニアの理解と完全に一致していると仮定する。 しかし、この仮定は実際は非現実的であり、システム要件の形式化は、非常に難しく、エラーを起こし、かなりの訓練を必要とする。 この厳しいハードルを緩和するために、線形時間論理(LTL)のための仕様スケッチと呼ばれる形式仕様を書くための根本的に新しいアプローチを提案する。 鍵となるアイデアは、エンジニアが ltl スケッチと呼ばれる部分的な ltl 式を提供することであり、そこでは形式化が難しい部分を外すことができる。 仕様が許すべきあるいは許すべきでないシステム動作を記述する一連の例が与えられたとき、いわゆるスケッチアルゴリズムのタスクは、得られたltl公式が例と一致するように、与えられたスケッチを完成させることである。 スケッチを完遂できるかどうかを決定することは、複雑性クラスnpに落とし込み、2つのsatベースのスケッチアルゴリズムを示す。 また,プロトタイプ実装を用いた形式仕様記述には,スケッチが実用的な手法であることを実証する。

関連論文リスト

• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications [59.01527054553122]
  リニア時間論理(LTL)は、強化学習(RL)における複雑で時間的に拡張されたタスクを特定する強力なフォーマリズムとして最近採用されている。 既存のアプローチはいくつかの欠点に悩まされており、それらは有限水平フラグメントにのみ適用でき、最適以下の解に制限され、安全制約を適切に扱えない。 本研究では,これらの問題に対処するための新しい学習手法を提案する。 提案手法は, 自動仕様のセマンティクスを明示的に表現したB"uchiaの構造を利用して, 所望の式を満たすための真理代入の順序を条件としたポリシーを学習する。
  論文  参考訳（メタデータ） (2024-10-06T21:30:38Z)
• It's All About Your Sketch: Democratising Sketch Control in Diffusion Models [114.73766136068357]
  本稿では,拡散モデルにおけるスケッチの可能性を明らかにするとともに,生成型AIにおける直接スケッチ制御の詐欺的可能性に対処する。 私たちはこのプロセスを民主化し、アマチュアのスケッチが正確なイメージを生成できるようにします。
  論文  参考訳（メタデータ） (2024-03-12T01:05:25Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
  論文  参考訳（メタデータ） (2023-10-26T14:13:15Z)
• I Know What You Draw: Learning Grasp Detection Conditioned on a Few Freehand Sketches [74.63313641583602]
  そこで本研究では,スケッチ画像に関連のある潜在的な把握構成を生成する手法を提案する。 私たちのモデルは、現実世界のアプリケーションで簡単に実装できるエンドツーエンドで訓練され、テストされています。
  論文  参考訳（メタデータ） (2022-05-09T04:23:36Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• From English to Signal Temporal Logic [7.6398837478968025]
  本稿では,サイバー物理システムのための公式な仕様言語であるSignal Temporal Logic (STL) に,自由英語文として与えられる非公式な要件を翻訳するためのツールおよびテクニックであるDeepSTLを提案する。 このような翻訳を考案する上での大きな課題は、公式な非公式な要件と公式な仕様の欠如である。 2番目のステップでは、最先端のトランスフォーマーベースのニューラル翻訳技術を用いて、英語からSTLへの正確な注意翻訳を訓練する。
  論文  参考訳（メタデータ） (2021-09-21T16:13:29Z)
• Learning-Augmented Sketches for Hessians [54.97773807211337]
  第二次手法の文脈でヘッセンの学習スケッチを設計する方法を紹介します。 学習したスケッチは,「学習されていない」スケッチと比較して,重要な問題に対する近似精度が向上することを示す。
  論文  参考訳（メタデータ） (2021-02-24T14:50:59Z)
• Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods [28.72161643908351]
  本稿では,STLCG(Signal Temporal Logic)公式の定量的意味を計算グラフを用いて計算する手法を提案する。 STLは、連続系とハイブリッド系の両方で生成される信号の空間的および時間的特性を指定できる、強力で表現力のある形式言語である。
  論文  参考訳（メタデータ） (2020-07-31T22:01:39Z)
• On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach [3.9461038686072847]
  計算木論理(CTL)における忘れ書きに基づくアプローチを導入する。 本研究では, 与えられたモデルの下で, 与えられたシグネチャ上で, 最強必要条件 (SNC) と最弱十分条件 (WSC) を計算できることを示す。 また, その理論的性質について考察し, 忘れることの概念が, 知識を忘れることの本質的な仮定を満足させることを示す。
  論文  参考訳（メタデータ） (2020-03-13T21:51:59Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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