論文の概要: 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仕様の可逆性、すなわち、このリフレクション演算子を用いて特定のシステムの具体的な振る舞いを反転させる方法について検討する。
関連論文リスト
- 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) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - 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) - 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) - Mining Environment Assumptions for Cyber-Physical System Models [0.19336815376402716]
出力要求を満たす入力信号のサブセットをコンパクトに記述できることを示す。
教師付き学習手法を用いて,そのような環境仮定をマイニングするアルゴリズムを提案する。
本研究では、交通や医療など複数の分野の現実データに関する実験結果を示す。
論文 参考訳(メタデータ) (2020-05-18T03:05:21Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。