基于 SMT 的本体驱动数据感知过程安全验证（扩展版）
人工智能
2021-08-30 v1
摘要
在数据感知过程（DAPs）验证的背景下，一种基于可满足性模理论（SMT）的形式化方法已被用于验证所谓以构件为中心系统的参数化安全性质。该方法需要结合模型论概念与基于向后可达性的算法技术。本文引入该谱系中研究最广泛的模型之一——简单构件系统（SASs）的一个变体，其中我们不再管理数据库，而是在（RDFS 的轻微扩展上的）描述逻辑（DL）本体上进行操作。该描述逻辑具有合适的模型论性质，使我们能够定义基于 DL 的 SASs，向后可达性仍可应用于此，从而使得相应安全问题在 PSPACE 内可判定。
引用
@article{arxiv.2108.12330,
title = {SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version)},
author = {Diego Calvanese and Alessandro Gianola and Andrea Mazzullo and Marco Montali},
journal= {arXiv preprint arXiv:2108.12330},
year = {2021}
}