論文の概要: SMT-Based Safety Verification of Data-Aware Processes under Ontologies
(Extended Version)
- arxiv url: http://arxiv.org/abs/2108.12330v1
- Date: Fri, 27 Aug 2021 15:04:11 GMT
- ステータス: 処理完了
- システム内更新日: 2021-08-30 14:16:47.575973
- Title: SMT-Based Safety Verification of Data-Aware Processes under Ontologies
(Extended Version)
- Title(参考訳): SMTによるオントロジーに基づくデータ認識プロセスの安全性検証(拡張版)
- Authors: Diego Calvanese and Alessandro Gianola and Andrea Mazzullo and Marco
Montali
- Abstract要約: 我々は、このスペクトルで最も調査されたモデルの1つ、すなわち単純なアーティファクトシステム(SAS)の変種を紹介する。
このDLは適切なモデル理論特性を享受し、後方到達性を適用可能なSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
- 参考スコア(独自算出の注目度): 71.12474112166767
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In the context of verification of data-aware processes (DAPs), a formal
approach based on satisfiability modulo theories (SMT) has been considered to
verify parameterised safety properties of so-called artifact-centric systems.
This approach requires a combination of model-theoretic notions and algorithmic
techniques based on backward reachability. We introduce here a variant of one
of the most investigated models in this spectrum, namely simple artifact
systems (SASs), where, instead of managing a database, we operate over a
description logic (DL) ontology expressed in (a slight extension of) RDFS. This
DL, enjoying suitable model-theoretic properties, allows us to define DL-based
SASs to which backward reachability can still be applied, leading to
decidability in PSPACE of the corresponding safety problems.
- Abstract(参考訳): データ認識プロセス(DAP)の検証の文脈では、いわゆるアーティファクト中心システムのパラメータ化安全性特性を検証するために、満足度変調理論(SMT)に基づく正式なアプローチが検討されている。
このアプローチには、モデル理論の概念と後方到達性に基づくアルゴリズム技術の組み合わせが必要である。
ここでは,データベースを管理する代わりに,RDFSで表現された記述論理(DL)オントロジーを運用する,このスペクトルで最も調査されたモデルの1つ,すなわち単純なアーティファクトシステム(SAS)を紹介した。
このDLは、適切なモデル理論特性を享受し、後方到達性がまだ適用可能なDLベースのSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
関連論文リスト
- From STPA to Safe Behavior Models [0.0]
結果クリティカルなシステム理論プロセス分析(STPA)に基づく安全臨界式の生成規則を提案する。
また、行動モデルにおける生活特性をカバーするために、AをDesired Control Actionsで拡張する。
結果のモデルは必ずしも完成していないが、安全と生きた特性をすでにカバーしている優れた基盤を提供する。
論文 参考訳(メタデータ) (2024-04-05T13:39:25Z) - Latent Semantic Consensus For Deterministic Geometric Model Fitting [109.44565542031384]
我々はLSC(Latent Semantic Consensus)と呼ばれる効果的な方法を提案する。
LSCは、モデルフィッティング問題をデータポイントとモデル仮説に基づく2つの潜在意味空間に定式化する。
LSCは、一般的な多構造モデルフィッティングのために、数ミリ秒以内で一貫した、信頼性の高いソリューションを提供することができる。
論文 参考訳(メタデータ) (2024-03-11T05:35:38Z) - Correct-by-Construction Control for Stochastic and Uncertain Dynamical
Models via Formal Abstractions [44.99833362998488]
我々は、様々なモデリングの前提の下でこの問題を解決するために使用できる抽象フレームワークを開発する。
我々は、与えられた仕様を満たすための保証とともに、iMDPの最適ポリシーを計算するために最先端の検証技術を使用します。
そして、このポリシーを構築によって、これらの保証が動的モデルに受け継がれるフィードバックコントローラに改良できることを示します。
論文 参考訳(メタデータ) (2023-11-16T11:03:54Z) - Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
本研究は,NFに基づく多次元条件(後)密度推定器の検証診断を容易にすることを提案する。
また、局所的な一貫性の結果に基づいた理論的保証も提供する。
この作業は、より良い特定モデルの設計を支援したり、新しいSBIアルゴリズムの開発を促進するのに役立つだろう。
論文 参考訳(メタデータ) (2022-11-17T15:48:06Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳(メタデータ) (2022-08-12T17:03:50Z) - Soundness of Data-Aware Processes with Arithmetic Conditions [8.914271888521652]
データペトリネット(DPN)は、単純さと表現性のバランスをとる能力によって、人気が高まっている。
データと制御フローの相互作用は、そのようなモデルの正しさ、特に音の良さ、決定的かつ困難さの確認を可能にする。
算術データ条件に富んだDPNの音質を評価するための枠組みを提供する。
論文 参考訳(メタデータ) (2022-03-28T14:46:10Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。