論文の概要: Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic

• arxiv url: http://arxiv.org/abs/2203.07982v1
• Date: Tue, 15 Mar 2022 15:14:25 GMT
• ステータス: 処理完了
• システム内更新日: 2022-03-16 20:50:12.770333
• Title: Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
• Title（参考訳）: 算術によるデータ認識動的システムの線形時間検証
• Authors: Paolo Felli, Marco Montali, Sarah Winkler
• Abstract要約: 我々は、忠実な有限状態抽象の存在を保証する「有限要約」という新しい意味的特性を導入する。 形式的手法やデータベース理論で研究されたいくつかの決定可能性条件は、この性質の具体的かつチェック可能な例と見なすことができる。 我々の結果は、以前のアプローチでは手の届かないシステムを分析することを可能にする。
• 参考スコア（独自算出の注目度）: 8.914271888521652
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Combined modeling and verification of dynamic systems and the data they operate on has gained momentum in AI and in several application domains. We investigate the expressive yet concise framework of data-aware dynamic systems (DDS), extending it with linear arithmetic, and provide the following contributions. First, we introduce a new, semantic property of "finite summary", which guarantees the existence of a faithful finite-state abstraction. We rely on this to show that checking whether a witness exists for a linear-time, finite-trace property is decidable for DDSs with finite summary. Second, we demonstrate that several decidability conditions studied in formal methods and database theory can be seen as concrete, checkable instances of this property. This also gives rise to new decidability results. Third, we show how the abstract, uniform property of finite summary leads to modularity results: a system enjoys finite summary if it can be partitioned appropriately into smaller systems that possess the property. Our results allow us to analyze systems that were out of reach in earlier approaches. Finally, we demonstrate the feasibility of our approach in a prototype implementation.
• Abstract（参考訳）: 動的システムのモデリングと検証とそれらが運用するデータの組み合わせは、AIやいくつかのアプリケーションドメインで勢いを増している。 本稿では,データ認識動的システム(dds)の表現的かつ簡潔なフレームワークについて検討し,線形算術を用いて拡張し,以下の貢献を与える。 まず,忠実な有限状態抽象の存在を保証する「有限要約」の新たな意味的性質を導入する。 これを頼りに、証人が線形時間有限トレース特性のために存在するかどうかを確認することは、有限要約を持つDSに対して決定可能であることを示す。 第二に、形式的手法やデータベース理論で研究されたいくつかの決定可能性条件が、この性質の具体的かつ検証可能な例であることを示す。 これはまた、新たな決定可能性結果をもたらす。 第三に、有限要約の抽象的一様性がモジュラリティの結果をもたらすことを示す: システムは、その性質を持つより小さなシステムに適切に分割できるならば、有限要約を楽しむ。 私たちの結果は、以前のアプローチでは手が届かなかったシステムを分析できます。 最後に,プロトタイプ実装におけるアプローチの実現可能性を示す。

関連論文リスト

• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Learning Latent Dynamics via Invariant Decomposition and (Spatio-)Temporal Transformers [0.6767885381740952]
  本研究では,高次元経験データから力学系を学習する手法を提案する。 我々は、システムの複数の異なるインスタンスからデータが利用できる設定に焦点を当てる。 我々は、単純な理論的分析と、合成および実世界のデータセットに関する広範な実験を通して行動を研究する。
  論文  参考訳（メタデータ） (2023-06-21T07:52:07Z)
• Schema-aware Reference as Prompt Improves Data-Efficient Knowledge Graph Construction [57.854498238624366]
  本稿では,データ効率のよい知識グラフ構築のためのRAP(Schema-Aware Reference As Prompt)の検索手法を提案する。 RAPは、人間の注釈付きおよび弱教師付きデータから受け継いだスキーマと知識を、各サンプルのプロンプトとして動的に活用することができる。
  論文  参考訳（メタデータ） (2022-10-19T16:40:28Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。 RABは両方の制限を解除することで既存のモデルを一般化する。 データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-08-12T17:03:50Z)
• Combining Machine Learning and Agent-Based Modeling to Study Biomedical Systems [0.0]
  エージェントベースモデリング(エージェントベースモデリング、ABM)は、構成体間の相互作用を通じて複雑なシステムをシミュレートするためのよく確立されたパラダイムである。 機械学習(ML)は、統計アルゴリズムがシステム行動の事前理論を課すことなく、自身のデータから'学習する'アプローチを指す。
  論文  参考訳（メタデータ） (2022-06-02T15:19:09Z)
• MACE: An Efficient Model-Agnostic Framework for Counterfactual Explanation [132.77005365032468]
  MACE(Model-Agnostic Counterfactual Explanation)の新たな枠組みを提案する。 MACE法では, 優れた反実例を見つけるための新しいRL法と, 近接性向上のための勾配のない降下法を提案する。 公開データセットの実験は、有効性、空間性、近接性を向上して検証する。
  論文  参考訳（メタデータ） (2022-05-31T04:57:06Z)
• Capturing Actionable Dynamics with Structured Latent Ordinary Differential Equations [68.62843292346813]
  本稿では,その潜在表現内でのシステム入力の変動をキャプチャする構造付き潜在ODEモデルを提案する。 静的変数仕様に基づいて,本モデルではシステムへの入力毎の変動要因を学習し,潜在空間におけるシステム入力の影響を分離する。
  論文  参考訳（メタデータ） (2022-02-25T20:00:56Z)
• Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression [11.729744197698718]
  安全クリティカルなシナリオにおける自律システムの活用には、不確実性の存在下での行動を検証する必要がある。 本研究では,非モデル化された力学と雑音測定を用いた離散時間力学システムの検証フレームワークを開発した。
  論文  参考訳（メタデータ） (2021-12-31T05:10:05Z)
• Learning on Abstract Domains: A New Approach for Verifiable Guarantee in Reinforcement Learning [9.428825075908131]
  有限抽象領域上でDRLシステムを学習するための抽象的アプローチを提案する。 入力状態が有限なニューラルネットワークを生成し、ホスティングDRLシステムが直接検証可能である。
  論文  参考訳（メタデータ） (2021-06-13T06:28:40Z)
• Active Learning for Nonlinear System Identification with Guarantees [102.43355665393067]
  状態遷移が既知の状態-作用対の特徴埋め込みに線形に依存する非線形力学系のクラスについて検討する。 そこで本稿では, トラジェクティブ・プランニング, トラジェクティブ・トラッキング, システムの再推定という3つのステップを繰り返すことで, この問題を解決するためのアクティブ・ラーニング・アプローチを提案する。 本手法は, 非線形力学系を標準線形回帰の統計速度と同様, パラメトリック速度で推定する。
  論文  参考訳（メタデータ） (2020-06-18T04:54:11Z)
• Data-Driven Verification under Signal Temporal Logic Constraints [0.0]
  力学が部分的に不明な不確実性のあるシステムを考える。 本研究の目的は,そのようなシステムの軌道による時間論理特性の満足度について研究することである。 本研究では, ベイズ推定手法を用いて, 信頼度と満足度を関連づける。
  論文  参考訳（メタデータ） (2020-05-08T08:32:30Z)

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

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