RDFdL：将RDF与微分动态逻辑集成

# RDFdL：集成RDF与微分动态逻辑
来源：https://arxiv.org/html/2608.18165  
卡尔斯鲁厄理工学院（KIT）AIFB研究所，德国卡尔斯鲁厄  
Yuyang\.Li@kit\.edu  
https://orcid\.org/0009\-0001\-4924\-7720  

卡尔斯鲁厄理工学院（KIT）AIFB研究所，德国卡尔斯鲁厄  
lukas\.kubelka@kit\.edu  
https://orcid\.org/0009\-0008\-1828\-5207  

卡尔斯鲁厄理工学院（KIT）AIFB研究所，德国卡尔斯鲁厄  
julia\.butte@kit\.edu  
https://orcid\.org/0009\-0003\-5066\-8412  

卡尔斯鲁厄理工学院（KIT）AIFB研究所，德国卡尔斯鲁厄  
tobias\.kaefer@kit\.edu  
https://orcid\.org/0000\-0003\-0576\-7457\\  

\Copyright Yuyang Li and Tobias Käfer  
\ccsdesc[500]{Information systems Semantic web description languages}  
\ccsdesc[500]{Computing methodologies Knowledge representation and reasoning}  
\ccsdesc[300]{Theory of computation Logic and verification}  
\ccsdesc[300]{Software and its engineering Formal software verification}  
\Volume{1}  
\Issue{1}  
\Article{42}  
\Date{Submission}{Submission date}  
\Date{Acceptance}{Date of acceptance}  
\Date{Published}{Date of publishing}  
\Section{Area Editor}{TGDK section area editor}  

#### 摘要  
以RDF建模的知识图谱在描述静态知识方面功能强大，但它们无法捕获或推理物理系统的动态行为（例如由微分方程描述的系统），这对于AI驱动的网络物理系统而言是一个关键缺口。为解决此问题，我们提出了RDFdL框架，该框架将RDF与微分动态逻辑（dL）集成，以表示和推理静态知识与物理系统的连续动态。对于动态部分，我们在RDF和SHACL中语法化地表示微分方程和状态空间中的范围，并通过转换为dL提供语义。通过它们在一阶逻辑中的共同基础链接RDF和dL，实现了独特的集成：动态逻辑域中关于安全性和可达性属性的验证结果，可以作为SPARQL查询RDF数据的蕴含结果。我们使用Apache Jena实现本体驱动的RDF推理，使用dL定理证明器KeYmaera X实现该流水线，并概述了其在制造领域的适用性。  

#### 关键词  
RDF，微分动态逻辑，混合系统，知识图谱，形式化验证  

## 1 引言  
知识图谱被用作网络物理系统和工业系统的数据层。它们提供了全局可标识的资源、类型化的关系、图模式、溯源以及对诸如设备、传感器、控制器、产品、操作员、维护职责和流程配置等信息的查询机制。在制造环境中，此类信息通常通过数字孪生描述和资产模型来表示，而RDF是一种自然的表示语言，因为它支持跨组织和系统边界的开放图集成。  

这些图模型非常适合回答结构性问题：哪个设备属于哪个生产单元，哪个按钮控制哪个执行器，哪位技术员负责哪台机器，或者哪个产品由哪个单元处理。然而，关于网络物理系统的许多问题不仅仅是结构性的。它们还取决于物理过程如何随时间演变。加热设备根据微分方程改变温度；储罐液位根据流入和流出量变化；锅炉根据耦合的压力和水位动力学演变。从一个操作状态到另一个状态的转换是否可能、安全或被禁止，无法仅凭RDF三元组来决定。  

标准的RDF、RDFS、OWL、SHACL和SPARQL提供了图表示、模式验证和图查询，但它们本身并不能解决行为由常微分方程（ODE）支配的系统的可达性或安全性问题。图可能声明烤箱有`onMode`和`offMode`，但这并不能确定在特定温度下切换模式是否保持安全界限。  

混合系统验证正是解决这种连续-离散行为问题的。微分动态逻辑（dL）为混合程序提供了规范和证明语言，其中离散控制动作和连续ODE演化可以组合成一个形式化模型\[17 (https://arxiv.org/html/2608.18165#bib.bib5), 7 (https://arxiv.org/html/2608.18165#bib.bib4)\]。在dL中，可以陈述并证明诸如“控制器的每次执行都保持温度界限”或“在给定的ODE和演化域下，存在从一个温度区域到另一个区域的连续演化”等属性。像KeYmaera X这样的定理证明器为此类证明提供演绎支持。  

然而，dL模型本身不是知识图谱。它们本身不提供RDF标识符、图模式验证、SPARQL路径查询、设备元数据链接、溯源、维护信息、产品描述，或与现有数字孪生数据的集成。因此，核心问题既不是用RDF推理替代混合系统定理证明器，也不是用dL模型替代RDF知识图谱，而是在两者之间建立一个可靠的桥梁：经过验证的连续和离散行为应能作为图数据被查询，同时图数据应提供符号状态区域、设备模式、元数据以及用于生成证明义务的候选转换。  

每当用户需要查询答案既依赖静态元数据又依赖经过形式化验证的动态行为的图查询时，这个桥梁就很有用。为弥合这一鸿沟，我们将微分动态逻辑（dL）与RDF集成。dL是一种用于混合系统的正式规范和验证语言，能够建模连续动态并证明系统属性\[17 (https://arxiv.org/html/2608.18165#bib.bib5)\]。在dL中，我们可以描述具有离散转换（如控制器决策或模式切换）的过程，以及由常微分方程（ODE）支配的物理过程的连续演化\[17 (https://arxiv.org/html/2608.18165#bib.bib5)\]。dL允许指定安全属性，如不变式、界限和避免不良状态，并形式化验证这些属性对于混合系统的所有可能行为都成立。像KeYmaera X这样的工具使用定理证明方法实现dL，从而能够验证混合程序的正确性属性\[7 (https://arxiv.org/html/2608.18165#bib.bib4)\]。例如，“如果系统开始时是安全的，它将永远不会违反安全条件。”这种演绎验证已成功应用于复杂的混合系统。它已被用于验证工业规模的网络物理系统，如铁路控制系统、空中交通防撞系统和自动驾驶控制器\[17 (https://arxiv.org/html/2608.18165#bib.bib5)\]。  

考虑一条生产线，其中烤箱加热产品。操作工程师问道：“沿着过程预期的加热路径，在哪个点发生第一次模式切换，哪个按钮触发它，以及哪位技术员负责该设备？”这个问题的前半部分是关于经过验证的动态行为——预期的转换是否能在烤箱的加热ODE下实现。后半部分是关于静态元数据——如按钮、设备和职责，这些自然存在于RDF图中。现有工具没有一个能在单个查询中回答问题的两半。  

因此，我们的贡献是弥合RDF与混合系统形式化验证之间的差距。我们提出了一种新方法：从基于RDF的网络物理过程知识模型开始，自动推导适合在dL中验证的形式化模型，并将dL推理结果集成到RDF推理和查询中。  

总而言之，我们的贡献如下：  
- **基于RDF的混合系统表示**：我们引入了在RDF中形式化表示混合系统的方法，在RDF中捕获连续动态（ODE）和基于SHACL的状态定义。  
- **dL公式生成与验证**：我们通过提供从RDF/SHACL混合系统表示到微分动态逻辑（dL）的转换，阐述了该表示的语义。  
- **RDFdL框架**：我们提供了RDFdL框架，使用Apache Jena进行推理和查询，使用KeYmaera X进行dL证明。  

本文其余部分组织如下：第3节 (https://arxiv.org/html/2608.18165#S3) 详细介绍动机示例和问题设置。第2节 (https://arxiv.org/html/2608.18165#S2) 回顾RDF、SHACL、SPARQL、混合系统和dL所需的背景知识。第5节 (https://arxiv.org/html/2608.18165#S5) 建立形式化保证，并讨论表达能力和复杂性。第4节 (https://arxiv.org/html/2608.18165#S4) 描述实现。第6节 (https://arxiv.org/html/2608.18165#S6) 报告评估。第7节 (https://arxiv.org/html/2608.18165#S7) 讨论相关工作，第9节 (https://arxiv.org/html/2608.18165#S9) 是结论。  

## 2 预备知识  
本节介绍本文其余部分所需的背景知识。我们首先回顾RDF、SHACL和SPARQL在RDFdL中的作用。然后介绍本文使用的混合系统和微分动态逻辑（dL）片段。最后，我们阐明具体的dL状态与RDFdL状态区域之间的区别，因为这一区别对我们的基于图的表示至关重要。  

### 2.1 RDF、SHACL和SPARQL  
我们简要介绍我们所应用的语义网技术：RDF、SHACL、SPARQL及其在我们方法中的作用。我们将混合系统的静态和动态信息表示为RDF数据，使用SHACL定义状态，并使用SPARQL查询数据，同时考虑来自dL的状态转换蕴含数据。  

**RDF（资源描述框架）**。RDF 111 https://www.w3.org/TR/rdf11-concepts/ 是W3C关于数据模型的推荐标准，它在有向标签图中编码二元谓词。RDF图定义为一组**三元组**，每个三元组形式为⟨subject, predicate, object⟩。在RDF中，对象可以是URI 222 http://www.ietf.org/rfc/rfc3986，根据https://prefix.cc/中的实践缩写为CURIE（见http://www.w3.org/TR/curie）。此外，空前缀：表示我们匿名化的词汇表“http://anonymous.example/rdfdl/vocabulary#”，而`ex:`表示“http://example.org/#”。全局资源标识符、空节点（文档范围内的资源标识符）或字面量（数据值）；主语可以是URI或空节点；谓词只能是URI。在本文中，我们使用Turtle语法333 https://www.w3.org/TR/turtle/ 编写RDF。在RDFdL中，RDF用于表示设备、变量、模式、符号状态区域、ODE记录、候选转换、已验证转换、证明工件和普通元数据。  

**SHACL（形状约束语言）**。SHACL 444 https://www.w3.org/TR/shacl/ 是W3C关于RDF数据约束语言的推荐标准。它允许定义**形状**，即可用于验证RDF图的条件。SHACL形状可以编码为RDF。在我们的工作中，我们使用SHACL来表达节点入/出边的基数约束以及边端点的值范围约束。我们使用SHACL编码我们定义的状态及其值范围。在RDFdL中，SHACL用于验证实时输入状态。它验证观测值和格式良好的RDF描述。它不定义ODE、连续演化或dL公式的语义。混合系统行为的语义由下面介绍的dL证明义务给出。  

例如，SHACL可以验证温度为185且模式为Off的观测值是否符合与高温关闭区域关联的形状。这种验证确定了观测值所属的符号区域。它并不证明系统可以安全地到达该区域。dL证明义务处理可达性和安全性。  

**SPARQL（SPARQL协议和查询语言）**。在SPARQL 555 https://www.w3.org/TR/sparql11-query/ RDF查询语言（W3C推荐标准）中，我们可以定义需要在RDF图上匹配的**基本图模式（BGP）**以提取特定信息。BGP由三元组模式组成，即每个位置都可能出现变量的三元组。可以对由此获得的结果应用FILTER。此外，SPARQL提供所谓的**属性路径**，可以使用它来查询任意属性序列。我们使用SPARQL来制定关于静态和动态部分的查询。属性路径对于制定序列状态上的可达性查询特别有用。在我们的方法中，我们还可以使用SPARQL来获取静态事实（设备类型、接线、模式记录）的基本图模式，并遍历物化的`:next`和`:modeChange`边，从而回答诸如“*找到从原料到成品的幸福路径*”之类的可达性查询，并在dL证明结果被物化后查询已验证的转换图。  

**SPARQL和Apache Jena中的蕴含**。SPARQL可以对RDF图匹配BGP以推导SPARQL查询结果。为了也能考虑通过对RDF图应用形式化推理得出的结果，实践中应用了多种选项：SPARQL蕴含W3C推荐标准666 https://www.w3.org/TR/sparql11-entailment/ 定义了如何将BGP匹配扩展到考虑诸如RDFS和OWL的蕴含规则。然而，属性路径的评估不是基于BGP匹配定义的；因此，推理结果在任意长度的属性路径中不可用\[10 (https://arxiv.org/html/2608.18165#bib.bib13)\]——而我们需要这样的属性路径来进行可达性查询。  

然而，Apache Jena中的推理是基于RETE引擎或表化Datalog引擎或两者的组合实现的，其方式是查询在原始数据和推断数据的组合上执行，这两个数据源被视为相同的\[21 (https://arxiv.org/html/2608.18165#bib.bib10)\]，因此属性路径查询确实可以在推断的三元组上进行评估。  

### 2.2 微分动态逻辑  
我们使用Platzer论文\[17 (https://arxiv.org/html/2608.18165#bib.bib5)\]中的微分动态逻辑（dL）。微分动态逻辑是一种用于规范和验证混合系统的逻辑，即其行为将离散转换与沿微分方程的连续演化相结合的系统。在dL中，系统行为由**混合程序**表示，此类程序的属性被陈述为逻辑公式。  

设\(\mathcal{V}\)为有限变量集。状态\(\nu\)是将值赋给\(\mathcal{V}\)中每个变量的赋值。对于本文使用的连续变量，其值为实数。我们用\(\nu(x)\)表示变量\(x\)在状态\(\nu\)下的值。本文使用的混合程序片段由以下语法生成：  
\(\alpha,\beta ::= x:=\theta \mid ?\phi \mid x_{1}'=\theta_{1},\ldots,x_{n}'=\theta_{n}\ \&\ Q \mid \alpha;\beta \mid \alpha\cup\beta \mid \alpha^{\ast}\)。  
这里，\(x:=\theta\)是离散赋值，?\phi\)是仅当\(\phi\)成立时才可继续的测试，\(x_{1}'=\theta_{1},\ldots,x_{n}'=\theta_{n}\ \&\ Q\)是在演化域\(Q\)内沿ODE系统的连续演化，\(\alpha;\beta\)是顺序组合，\(\alpha\cup\beta\)是非确定性选择，\(\alpha^{\ast}\)是