SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version)

• URL: http://arxiv.org/abs/2108.12330v1
• Date: Fri, 27 Aug 2021 15:04:11 GMT
• Title: SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version)
• Authors: Diego Calvanese and Alessandro Gianola and Andrea Mazzullo and Marco Montali
• Abstract summary: 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.
• Score: 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.

Related papers

• From STPA to Safe Behavior Models [0.0]
  We propose rules for generating safetycritical formulas based on the result-critical System-Theoretic Process Analysis (STPA) To also cover liveness properties in a behavior model, we extend A with Desired Control Actions. The resulting model is not necessarily complete but provides a good foundation that already covers safety and liveness properties.
  arXiv  Detail & Related papers  (2024-04-05T13:39:25Z)
• Latent Semantic Consensus For Deterministic Geometric Model Fitting [109.44565542031384]
  We propose an effective method called Latent Semantic Consensus (LSC) LSC formulates the model fitting problem into two latent semantic spaces based on data points and model hypotheses. LSC is able to provide consistent and reliable solutions within only a few milliseconds for general multi-structural model fitting.
  arXiv  Detail & Related papers  (2024-03-11T05:35:38Z)
• Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions [44.99833362998488]
  We develop an abstraction framework that can be used to solve this problem under various modeling assumptions. We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model.
  arXiv  Detail & Related papers  (2023-11-16T11:03:54Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  This work proposes easy to interpret validation diagnostics for multi-dimensional conditional (posterior) density estimators based on NF. It also offers theoretical guarantees based on results of local consistency. This work should help the design of better specified models or drive the development of novel SBI-algorithms.
  arXiv  Detail & Related papers  (2022-11-17T15:48:06Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  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.
  arXiv  Detail & Related papers  (2022-08-12T17:03:50Z)
• 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)
• 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.