将知识图谱与微分动态逻辑结合,实现对物理系统的动态行为推理。
RDFdL: Integrating RDF with Differential Dynamic Logic

- 用RDF和SHACL语法表示微分方程与状态空间范围
- 通过映射到dL实现安全性和可达性验证
- 适合需要形式化验证的智能制造系统
以RDF建模的知识图谱擅长描述静态知识,但无法捕捉或推理物理系统的动态行为,例如由微分方程描述的系统,这对人工智能驱动的网络物理系统构成关键缺陷。为此,我们提出RDFdL框架,将RDF与微分动态逻辑(dL)结合,以同时表达和推理静态知识与物理系统的连续动态。针对动态部分,我们在RDF和SHACL中语法化表示微分方程与状态空间范围,并通过映射至dL提供语义。基于一阶逻辑的共同基础,实现了RDF与dL的唯一集成:动态逻辑领域的安全性与可达性验证结果可转化为对RDF数据的SPARQL查询蕴含关系。我们使用Apache Jena进行本体驱动的RDF推理,以及KeYmaera X(dL定理证明器)实现该流程,并在制造场景中展示其应用潜力。
原文摘要 · Abstract (English)
Knowledge graphs modeled in RDF are powerful for describing static knowledge, but they cannot capture or reason about the dynamic behavior of physical systems, e.g., systems described by differential equations, which is a critical gap for AI-driven cyber-physical systems. To solve this, we propose RDFdL, a framework that integrates RDF with Differential Dynamic Logic (dL) to represent and reason about both static knowledge and the continuous dynamics of physical systems. For the dynamic part, we syntactically represent differential equations and ranges in the state space in RDF and SHACL and provide semantics using a translation to dL. Linking RDF and dL through their shared foundation in first-order logic achieves a unique integration: verification results for safety and reachability properties in the dynamic logic domain become available as entailment to SPARQL queries over RDF data. We implement the pipeline using Apache Jena for ontology-driven RDF reasoning and KeYmaera X, the theorem prover for dL, and sketch its applicability in manufacturing.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。