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

arXiv: https://arxiv.org/abs/2108.12330 · HTML: https://mlsanity.com/paper/2108.12330/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 30 references that are in the map.
- First posted on arXiv 27 Aug 2021.

## Builds on (most cited first, 6 of 6)

- [The DL-Lite Family and Relations](https://mlsanity.com/paper/1401.3487/) (2014)
- [Description Logic Knowledge and Action Bases](https://mlsanity.com/paper/1402.0569/) (2014)
- [Petri Nets with Parameterised Data: Modelling and Verification (Extended Version)](https://mlsanity.com/paper/2006.06630/) (2020)
- [Verification of Hierarchical Artifact Systems](https://mlsanity.com/paper/1604.00967/) (2016)
- [Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)](https://mlsanity.com/paper/1906.07811/) (2019)
- [Formalizing Integration Patterns with Multimedia Data (Extended Version)](https://mlsanity.com/paper/2009.04589/) (2020)

## Abstract (arXiv)

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.