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

TL;DR

This paper presents a formal SMT-based approach for verifying safety in data-aware processes that utilize ontologies, extending simple artifact systems with description logic to ensure decidability.

Contribution

It introduces DL-based simple artifact systems, combining model-theoretic properties of ontologies with backward reachability for safety verification, achieving PSPACE decidability.

Findings

Decidability of safety verification in DL-based SASs

Extension of artifact systems with description logic

PSPACE complexity for safety problems

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.