SMT Safety Verification of Ontology-Based Processes
Authors: Diego Calvanese, Alessandro Gianola, Andrea Mazzullo, Marco Montali
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We prove that when the DL is expressed in (a slight extension of) RDFS, it enjoys suitable modeltheoretic 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. |
| Researcher Affiliation | Academia | Faculty of Engineering, Free University of Bozen-Bolzano, Italy, Computing Science Department, Ume a University, Sweden |
| Pseudocode | Yes | Algorithm 1: SMT-based backward reachability procedure |
| Open Source Code | No | The paper discusses the potential implementation in MCMT and extends existing work, but does not state that their specific code for this work is open-source or provide a link. |
| Open Datasets | No | The paper is theoretical and does not use or reference any datasets for training or evaluation. Therefore, there is no information about public availability of a dataset. |
| Dataset Splits | No | The paper is theoretical and does not describe empirical experiments with data splits. Therefore, there is no information about training/test/validation splits. |
| Hardware Specification | No | The paper is theoretical and does not describe empirical experiments, thus no hardware specifications are mentioned. |
| Software Dependencies | No | The paper mentions MCMT (Ghilardi and Ranise 2010) as a state-of-the-art model checker, but does not provide specific version numbers for MCMT or any other software dependencies. It only discusses extending MCMT. |
| Experiment Setup | No | The paper is theoretical and focuses on formal verification and complexity bounds, not empirical experimentation. As such, it does not provide details on experimental setup or hyperparameters. |