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

• URL: http://arxiv.org/abs/2208.06377v2
• Date: Fri, 11 Aug 2023 15:54:43 GMT
• Title: Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)
• Authors: Silvio Ghilardi and Alessandro Gianola and Marco Montali and Andrey Rivkin
• Abstract summary: We introduce the general framework of relational action bases (RABs) RABs generalize existing models by lifting both restrictions. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
• Score: 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.

Related papers

• Testing Generalizability in Causal Inference [3.547529079746247]
  There is no formal procedure for statistically evaluating generalizability in machine learning algorithms. We propose a systematic and quantitative framework for evaluating model generalizability in causal inference settings. By basing simulations on real data, our method ensures more realistic evaluations, which is often missing in current work.
  arXiv  Detail & Related papers  (2024-11-05T11:44:00Z)
• Soundness of Data-Aware Processes with Arithmetic Conditions [8.914271888521652]
  Data Petri nets (DPNs) have gained increasing popularity thanks to their ability to balance simplicity with expressiveness. The interplay of data and control-flow makes checking the correctness of such models, specifically the well-known property of soundness, crucial and challenging. We provide a framework for assessing soundness of DPNs enriched with arithmetic data conditions.
  arXiv  Detail & Related papers  (2022-03-28T14:46:10Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  We introduce a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs) This DL, enjoying suitable model-theoretic properties, allows us to define SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.
  arXiv  Detail & Related papers  (2021-08-27T15:04:11Z)
• Learning Multimodal VAEs through Mutual Supervision [72.77685889312889]
  MEME combines information between modalities implicitly through mutual supervision. We demonstrate that MEME outperforms baselines on standard metrics across both partial and complete observation schemes.
  arXiv  Detail & Related papers  (2021-06-23T17:54:35Z)
• Lifted Model Checking for Relational MDPs [12.574454799055026]
  pCTL-REBEL is a lifted model checking approach for verifying pCTL properties on relational MDPs. We show that the pCTL model checking approach is decidable for relational MDPs even for possibly infinite domains.
  arXiv  Detail & Related papers  (2021-06-22T13:12:36Z)
• OR-Net: Pointwise Relational Inference for Data Completion under Partial Observation [51.083573770706636]
  This work uses relational inference to fill in the incomplete data. We propose Omni-Relational Network (OR-Net) to model the pointwise relativity in two aspects.
  arXiv  Detail & Related papers  (2021-05-02T06:05:54Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  We study the verification of parameterised multi-agent systems (MASs) In particular, we study whether unwanted states, characterised as a given state formula, are reachable in a given MAS.
  arXiv  Detail & Related papers  (2020-08-11T15:24:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.