SMT Safety Verification of Ontology-Based Processes

Proc. of the 37th AAAI Conf. on Artificial Intelligence (AAAI 2023). 2023.

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. This approach requires a combination of model-theoretic notions and algorithmic techniques based on backward reachability. We introduce here Ontology-Based Processes, which are 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. We prove that when the DL is expressed in (a slight extension of ) RDFS, it enjoys suitable model-theoretic properties, and that by relying on such DL we can define Ontology-Based Processes to which backward reachability can still be applied. Relying on these results we are able to show that in this novel setting, verification of safety properties is decidable in PSPACE.

@inproceedings{AAAI-2023,
   title = "SMT Safety Verification of Ontology-Based Processes",
   year = "2023",
   author = "Diego Calvanese and Alessandro Gianola and Andrea Mazzullo
and Marco Montali",
   booktitle = "Proc. of the 37th AAAI Conf. on Artificial Intelligence
(AAAI 2023)",
   pages = "6271--6279",
   publisher = "AAAI Press",
   doi = "10.1609/aaai.v37i5.25772",
}