論文の概要: 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仕様の可逆性、すなわち、このリフレクション演算子を用いて特定のシステムの具体的な振る舞いを反転させる方法について検討する。
関連論文リスト
- Zero-Shot Instruction Following in RL via Structured LTL Representations [50.41415009303967]
マルチタスク強化学習では、エージェントが訓練中に見えない新しいタスクをゼロショットで実行しなければならない。
この設定では、最近、時間的に拡張された構造化タスクを特定するための強力なフレームワークとして線形時間論理が採用されている。
既存のアプローチはジェネラリストの政策を訓練することに成功しているが、仕様に固有のリッチな論理的・時間的構造を効果的に捉えるのに苦労することが多い。
論文 参考訳（メタデータ） (2026-02-15T23:22:50Z) - Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
本研究では,大規模状態空間を持つ決定過程(MDP)における非マルコフ報酬の論理的仕様に関する新しい枠組みを提案する。
我々のアプローチは有限トレース(LTLfMT)上での線形時間論理モデュロ理論を利用する
本稿では,報酬マシンとHER(Hindsight Experience Replay)をベースとした一階述語論理仕様の翻訳手法を提案する。
論文 参考訳（メタデータ） (2026-02-05T22:11:28Z) - Counterexample Classification against Signal Temporal Logic Specifications [7.16622393795242]
Signal Temporal Logic (STL) は、ハイブリッドシステムの望ましい振る舞いを特定するための仕様言語として広く採用されている。
実際には、これらの反例は異なる原因から起こりうるので、異なるシステム欠陥に関係している。
パラメトリック信号時間論理(PSTL)を用いて各クラスを表す分類基準を提案する。
論文 参考訳（メタデータ） (2026-01-20T08:57:20Z) - LSRIF: Logic-Structured Reinforcement Learning for Instruction Following [56.517329105764475]
命令論理を明示的にモデル化するロジック構造化学習フレームワーク LSRIF を提案する。
実験の結果、LSRIFは命令追従と一般的な推論に大きな改善をもたらすことが示された。
論文 参考訳（メタデータ） (2026-01-10T05:11:38Z) - Fantastic Reasoning Behaviors and Where to Find Them: Unsupervised Discovery of the Reasoning Process [66.38541693477181]
本稿では, アクティベーション空間の方向として, 異なる推論挙動を符号化する, 推論ベクトルの発見のための教師なしフレームワークを提案する。
思考の連鎖トレースを文レベルの「ステップ」にセグメント化することで、リフレクションやバックトラックのような解釈可能な振る舞いに対応する歪んだ特徴を明らかにする。
本研究では,SAEデコーダ空間における信頼性関連ベクトルを同定し,応答信頼性を制御する能力を示す。
論文 参考訳（メタデータ） (2025-12-30T05:09:11Z) - Executing Discrete/Continuous Declarative Process Specifications via Complex Event Processing [2.314405422721801]
本稿では,ハイブリッド宣言モデルのリアルタイム実行と実行を可能にする,CEP(Complex Event Processing)ベースの実行アーキテクチャを提案する。
我々の3層アプローチは、STLにインスパイアされた述語を実行フローに統合し、システムがアクティブにアクティビティをトリガーし、連続的なセンサーの振る舞いに基づいてプロセス境界を強制することを可能にする。
論文 参考訳（メタデータ） (2025-12-05T11:57:52Z) - Zero-Shot Instruction Following in RL via Structured LTL Representations [54.08661695738909]
リニア時間論理(LTL)は、強化学習(RL)エージェントのための複雑で構造化されたタスクを特定するための魅力的なフレームワークである。
近年の研究では、命令を有限オートマトンとして解釈し、タスク進捗を監視する高レベルプログラムと見なすことができ、テスト時に任意の命令を実行することのできる1つのジェネラリストポリシーを学習できることが示されている。
本稿では,この欠点に対処する任意の命令に従うために,マルチタスクポリシーを学習するための新しいアプローチを提案する。
論文 参考訳（メタデータ） (2025-12-02T10:44:51Z) - Pretrained Embeddings as a Behavior Specification Mechanism [17.86560073144763]
仕様言語における第一級コンストラクトとして埋め込みを導入する。
埋め込みベースの仕様は、望ましい行動に向けてシステムを操るのに有効であることを示す。
論文 参考訳（メタデータ） (2025-03-03T19:41:22Z) - STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification [8.017203108408975]
STLCG++は,STL計算を時間ステップで並列化するマスキングに基づく手法である。
また,時間間隔境界による時間的有界性の異なるスムース化手法も導入する。
STLCG++のメリットを,3つのロボティクスユースケースを通じて実証し,JAXとPyTorchのオープンソースPythonライブラリを提供する。
論文 参考訳（メタデータ） (2025-01-08T00:06:43Z) - 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) - Describing Console I/O Behavior for Testing Student Submissions in Haskell [0.0]
単純なコンソールI/Oプログラムの動作を特定するための,小型で形式的な言語を提案する。
この設計は、学生が書いたインタラクティブHaskellプログラムをテストする具体的なアプリケーションケースによって進められている。
論文 参考訳（メタデータ） (2020-08-21T01:21:59Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。