論文の概要: Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)

• arxiv url: http://arxiv.org/abs/2208.06377v1
• Date: Fri, 12 Aug 2022 17:03:50 GMT
• ステータス: 処理完了
• システム内更新日: 2022-08-15 13:25:47.459850
• Title: Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)
• Title（参考訳）: リレーショナルアクションベース:形式化、効果的な安全性検証、不変量(拡張版)
• Authors: Silvio Ghilardi and Alessandro Gianola and Marco Montali and Andrey Rivkin
• Abstract要約: 我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。 RABは両方の制限を解除することで既存のモデルを一般化する。 データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
• 参考スコア（独自算出の注目度）: 67.99023219822564
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management, and Database Theory. To make these systems amenable to verification, the amount of information stored in each relational state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We introduce the general framework of relational action bases (RABs), which generalizes existing models by lifting both these restrictions: unbounded relational states can be evolved through actions that can quantify both existentially and universally over the data, and that can exploit numerical datatypes with arithmetic predicates. We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an off-the-shelf combination of existing verification modules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.
• Abstract（参考訳）: 状態のリレーショナル表現上で動作する動的システムのモデリングと検証は、ai、ビジネスプロセス管理、データベース理論においてますます研究されている。 これらのシステムを検証しやすいものにするには、各関係状態に格納された情報量が境界づけされるか、あるいは事前条件とアクションの効果に制限が課される必要がある。 これらの制約を解除することで既存のモデルを一般化する関係行動基盤(RAB)の一般的な枠組みを導入する。非有界な関係状態は、データ上で存在量と普遍性の両方を定量化し、算術的な述語で数値データ型を活用できるアクションによって進化することができる。 次に、SMTに基づく後方探索によるRABのパラメータ化安全性について検討し、その結果のメタプロパティを歌い、現状のMCMTモデルチェッカーの既存の検証モジュールの既製の組み合わせによってどのように実現できるかを示す。 データ対応ビジネスプロセスのベンチマークにおいて,このアプローチの有効性を示す。 最後に、この手続きを完全に正すために普遍不変量をどのように活用できるかを示す。

関連論文リスト

• Testing Generalizability in Causal Inference [3.547529079746247]
  機械学習アルゴリズムの一般化性を統計的に評価するための公式な手続きは存在しない。 本稿では,因果推論設定におけるモデル一般化可能性を評価するための体系的かつ定量的なフレームワークを提案する。 実データに基づくシミュレーションにより,本手法はより現実的な評価を確実にする。
  論文  参考訳（メタデータ） (2024-11-05T11:44:00Z)
• Soundness of Data-Aware Processes with Arithmetic Conditions [8.914271888521652]
  データペトリネット(DPN)は、単純さと表現性のバランスをとる能力によって、人気が高まっている。 データと制御フローの相互作用は、そのようなモデルの正しさ、特に音の良さ、決定的かつ困難さの確認を可能にする。 算術データ条件に富んだDPNの音質を評価するための枠組みを提供する。
  論文  参考訳（メタデータ） (2022-03-28T14:46:10Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  我々は、このスペクトルで最も調査されたモデルの1つ、すなわち単純なアーティファクトシステム(SAS)の変種を紹介する。 このDLは適切なモデル理論特性を享受し、後方到達性を適用可能なSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
  論文  参考訳（メタデータ） (2021-08-27T15:04:11Z)
• Learning Multimodal VAEs through Mutual Supervision [72.77685889312889]
  MEMEは、相互監督を通じて暗黙的にモダリティ間の情報を結合する。 我々は、MEMEが、部分的および完全観察スキームの双方で標準メトリクスのベースラインを上回ることを実証する。
  論文  参考訳（メタデータ） (2021-06-23T17:54:35Z)
• Lifted Model Checking for Relational MDPs [12.574454799055026]
  pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。 pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
  論文  参考訳（メタデータ） (2021-06-22T13:12:36Z)
• OR-Net: Pointwise Relational Inference for Data Completion under Partial Observation [51.083573770706636]
  この作業はリレーショナル推論を使って不完全なデータを埋めます。 本稿では,2つの点での相対性理論をモデル化するために,全関係ネットワーク (or-net) を提案する。
  論文  参考訳（メタデータ） (2021-05-02T06:05:54Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  パラメータ化マルチエージェントシステム(MAS)の検証について検討する。 特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
  論文  参考訳（メタデータ） (2020-08-11T15:24:05Z)

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

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