Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)

要約

状態のリレーショナル表現上で動作する動的システムのモデリングと検証は、AI、ビジネス プロセス管理、データベース理論における問題としてますます研究されています。
これらのシステムを検証しやすくするには、各関係状態に保存される情報の量を制限するか、アクションの前提条件と効果に制限を課す必要があります。
リレーショナル アクション ベース (RAB) の一般的なフレームワークを導入します。これは、これらの制限の両方を解除することによって既存のモデルを一般化します。無制限のリレーショナル状態は、データ全体にわたって存在的および普遍的に定量化でき、算術演算を使用して数値データ型を利用できるアクションを通じて進化できます。
述語。
次に、(近似的な) SMT ベースの後方探索を介して RAB のパラメータ化された安全性を研究し、結果として得られる手順の重要なメタプロパティを選び出し、状態の既存の検証モジュールの既製の組み合わせによってどのように実現できるかを示します。
最先端の MCMT モデル チェッカー。
データを意識したビジネス プロセスのベンチマークでこのアプローチの有効性を実証します。
最後に、普遍的不変式を利用してこの手順を完全に正しくする方法を示します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google