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

Diego Calvanese, Alessandro Gianola, Andrea Mazzullo, and Marco Montali

Proc. of the 34th Int. Workshop on Description Logics (DL 2021). Volume 2954 of CEUR Workshop Proceedings, http://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 2021)",
   volume = "2954",
   publisher = "CEUR-WS.org",
   series = "CEUR Workshop Proceedings, http://ceur-ws.org/",
}
pdf url