SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Preliminary Results)

Proc. of the 34th Int. Workshop on Description Logics (DL). Volume 2954 of CEUR Workshop Proceedings, https://ceur-ws.org/. 2021.

In the context of verification of data-aware processes, 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.

@inproceedings{DL-2021-verification,
   title = "SMT-Based Safety Verification of Data-Aware Processes under
Ontologies (Preliminary Results)",
   year = "2021",
   author = "Diego Calvanese and Alessandro Gianola and Andrea Mazzullo
and Marco Montali",
   booktitle = "Proc. of the 34th Int. Workshop on Description Logics (DL)",
   volume = "2954",
   publisher = "CEUR-WS.org",
   series = "CEUR Workshop Proceedings, https://ceur-ws.org/",
}