論文の概要: Executable Interval Temporal Logic Specifications

• arxiv url: http://arxiv.org/abs/2105.03375v1
• Date: Fri, 7 May 2021 16:36:24 GMT
• ステータス: 処理完了
• システム内更新日: 2021-05-10 12:14:19.575039
• Title: Executable Interval Temporal Logic Specifications
• Title（参考訳）: 実行可能区間時間論理仕様
• Authors: Antonio Cau, Stefan Kuhn, James Hoey
• Abstract要約: ITLは、状態の空でないシーケンスとして表現される振る舞いの観点から、システムに関する推論を可能にする。 異なる抽象化レベルにおけるシステムの仕様化を可能にします。 実行可能なITL仕様の可逆性を調査します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this paper the reversibility of executable Interval Temporal Logic (ITL) specifications is investigated. ITL allows for the reasoning about systems in terms of behaviours which are represented as non-empty sequences of states. It allows for the specification of systems at different levels of abstraction. At a high level this specification is in terms of properties, for instance safety and liveness properties. At concrete level one can specify a system in terms of programming constructs. One can execute these concrete specification, i.e., test and simulate the behaviour of the system. In this paper we will formalise this notion of executability of ITL specifications. ITL also has a reflection operator which allows for the reasoning about reversed behaviours. We will investigate the reversibility of executable ITL specifications, i.e., how one can use this reflection operator to reverse the concrete behaviour of a particular system.
• Abstract（参考訳）: 本稿では,実行時時間論理(ITL)仕様の可逆性について検討する。 ITLは、状態の空でないシーケンスとして表される振る舞いの観点から、システムについての推論を可能にする。 異なる抽象化レベルにおけるシステムの仕様化を可能にします。 高いレベルでは、この仕様はプロパティ、例えば安全性と生存性の観点から定義されている。 具体的なレベルでは、プログラミング構成の観点からシステムを指定することができる。 これらの具体的な仕様、すなわちシステムの振る舞いをテストし、シミュレートすることができる。 本稿では,この ITL 仕様の実行可能性の概念を定式化する。 ITLはまた、逆動作の推論を可能にするリフレクション演算子も備えている。 我々は、実行可能なIPL仕様の可逆性、すなわち、このリフレクション演算子を用いて特定のシステムの具体的な振る舞いを反転させる方法について検討する。

関連論文リスト

• An Ontology-based Approach Towards Traceable Behavior Specifications in Automated Driving [0.0]
  本稿では,自動走行システム搭載車両の動作を特定する手法として,セマンティックノーム行動解析を提案する。 対象とする運用環境の特定行動を形式的に表現し、特定行動とステークホルダーのニーズの間のトレーサビリティを確立するために使用します。 評価の結果,行動仕様における仮定の明示的な文書化は,仕様の不備の特定と治療の両立を支えていることが明らかとなった。
  論文  参考訳（メタデータ） (2024-09-10T16:00:22Z)
• Complex Event Recognition with Symbolic Register Transducers: Extended Technical Report [51.86861492527722]
  本稿では,オートマトンに基づく複合イベント認識システムを提案する。 本システムは,記号とレジスタオートマトンを組み合わせたオートマトンモデルに基づいている。 我々は、イベントストリーム上のパターンを検出するために、SRTをCERでどのように使用できるかを示す。
  論文  参考訳（メタデータ） (2024-07-03T07:59:13Z)
• Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control [0.7580487359358722]
  時間論理は、反応系の合成と検証に広く使われている強力なツールである。 大規模言語モデルに関する最近の進歩は、そのような仕様を書くプロセスをよりアクセスしやすいものにする可能性がある。
  論文  参考訳（メタデータ） (2024-06-11T16:07:24Z)
• Retrieval-Augmented Mining of Temporal Logic Specifications from Data [0.46040036610482665]
  この研究は、観測された振る舞いからデータ駆動的な方法でSTL要求を学習するタスクに対処する。 本稿では,ベイズ最適化(BO)と情報検索(IR)技術を組み合わせて,STL式の構造とパラメータを同時に学習する新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-05-23T09:29:00Z)
• Defining and executing temporal constraints for evaluating engineering artifact compliance [56.08728135126139]
  プロセスコンプライアンスは、実際のエンジニアリング作業が記述されたエンジニアリングプロセスに可能な限り密接に従うことを保証することに焦点を当てます。 これらのプロセスの制約をチェックすることは、依然として大変な作業であり、多くの手作業を必要とし、プロセスの後半にエンジニアにフィードバックを提供する。 関連するエンジニアリングアーティファクト間の時間的制約を,アーティファクトの変更毎に段階的にチェックする,自動制約チェックアプローチを提案する。
  論文  参考訳（メタデータ） (2023-12-20T13:26:31Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Pointwise-in-Time Explanation for Linear Temporal Logic Rules [0.29008108937701327]
  ルールステータスアセスメント(RSA)という新しい枠組みを提案する。 RSAは、個々の時間ステップにおける軌道進行を記述するために、直感的なステータスを任意のルールに割り当てる。 我々は、RSAがポストホック診断として有用であることに気付き、ユーザーはルールの集合に関してエージェントの振る舞いを体系的に追跡できる。
  論文  参考訳（メタデータ） (2023-06-24T13:07:08Z)
• Measuring Rule-based LTLf Process Specifications: A Probabilistic Data-driven Approach [2.5407767658470726]
  宣言的プロセス仕様は、有限トレース上の線形時間論理に基づくルールによってプロセスの振舞いを定義します。 マイニングの文脈では、これらの仕様は情報システムによって記録された複数セットの実行から推論され、チェックされる。 本稿では,イベントログに対する仕様書の満足度を測定する手法を提案する。
  論文  参考訳（メタデータ） (2023-05-09T13:07:01Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• Analogous Process Structure Induction for Sub-event Sequence Prediction [111.10887596684276]
  本稿では,未確認プロセスのサブイベントシーケンス全体を予測するために,アナログプロセス構造誘導APSIフレームワークを提案する。 我々の実験と分析が示すように、APSIは目に見えないプロセスのための意味のあるサブイベントシーケンスの生成をサポートし、行方不明な事象を予測するのに役立ちます。
  論文  参考訳（メタデータ） (2020-10-16T17:35:40Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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