K-文化的一切——从回归到 K-美妆，发送到您的邮箱订阅邮件

METAL MEDIA

RDFdL: Integrating RDF with Differential Dynamic Logic

arXiv:2608.181652026-08-20

把随时间变化的物理动态接入知识图谱后,一次查询就能同时问出系统能否安全到达某状态,以及该由哪位技术员负责

用RDF构建的知识图谱擅长描述设备、按钮、负责技术员这类静态信息,却无法表达温度等物理量随时间连续变化的规律。作者提出RDFdL框架,将RDF与用于验证连续动态和离散模式切换混合系统的形式化逻辑Differential Dynamic Logic(dL)连接起来,使静态元数据和已验证的动态行为可以在同一次图查询中一起被问到。团队在烤箱、酸奶生产线、工业鼓式锅炉和双水箱系统等多个案例上做了测试,证明经过验证的物理行为可以自然地作为图数据被查询。

METAL MEDIA 解读图

把随时间变化的物理动态接入知识图谱后,一次查询就能同时问出系统能否安全到达某状态,以及该由哪位技术员负责

  1. 01诸如'烤箱打开后温度能否安全到达某个范围'这类问题,单靠RDF或SPARQL无法回答,因为温度变化由微分方程描述,而RDF本身不具备表达连续变化含义的能力
  2. 02团队用RDF和SHACL表示由数值变量范围(如温度)与设备模式(开/关)组合而成的'状态区域',再将其自动翻译为dL公式;Apache Jena负责RDF推理,dL定理证明器KeYmaera X负责实际的形式化验证
  3. 03两个候选状态之间的转换不会被直接当作事实接受,而是被转化为dL证明义务交给KeYmaera X验证,只有证明成功的转换才会通过:next和:modeChange这两个谓词作为新的三元组被加回RDF图中,这样SPARQL的属性路径查询就能回答多步可达性问题
  4. 04团队在烤箱、含14次状态变化的酸奶生产线、工业鼓式锅炉、以及具有非线性耦合动态的双水箱系统上做了评估:线性或多项式动态的案例中,证明义务数量随状态和模式数量近似线性增长;而非线性水箱系统虽然需要更复杂的代数判定过程,所有证明义务依然全部成功完成
  5. 05SHACL被用来校验实时传感器读数属于哪个正确的符号化状态区域(例如把185度、关闭状态的读数匹配到对应的形状),而可达性与安全性的保证仍由dL证明负责,两者职责被清晰分开
这是 METAL MEDIA 制作的解读图，并非论文作者提供的原图。

他们做了什么

  1. 诸如'烤箱打开后温度能否安全到达某个范围'这类问题,单靠RDF或SPARQL无法回答,因为温度变化由微分方程描述,而RDF本身不具备表达连续变化含义的能力
  2. 团队用RDF和SHACL表示由数值变量范围(如温度)与设备模式(开/关)组合而成的'状态区域',再将其自动翻译为dL公式;Apache Jena负责RDF推理,dL定理证明器KeYmaera X负责实际的形式化验证
  3. 两个候选状态之间的转换不会被直接当作事实接受,而是被转化为dL证明义务交给KeYmaera X验证,只有证明成功的转换才会通过:next和:modeChange这两个谓词作为新的三元组被加回RDF图中,这样SPARQL的属性路径查询就能回答多步可达性问题
  4. 团队在烤箱、含14次状态变化的酸奶生产线、工业鼓式锅炉、以及具有非线性耦合动态的双水箱系统上做了评估:线性或多项式动态的案例中,证明义务数量随状态和模式数量近似线性增长;而非线性水箱系统虽然需要更复杂的代数判定过程,所有证明义务依然全部成功完成
  5. SHACL被用来校验实时传感器读数属于哪个正确的符号化状态区域(例如把185度、关闭状态的读数匹配到对应的形状),而可达性与安全性的保证仍由dL证明负责,两者职责被清晰分开
Figure 1: RDFdL architecture. The transition predicates :next and :modeChange are defined by Jena inference rules whose builtins invoke the KeYmaera X prover; verified transitions are therefore entailed triples, visible to SPARQL queries, including property paths alongside asserted data.
Figure 1: RDFdL architecture. The transition predicates :next and :modeChange are defined by Jena inference rules whose builtins invoke the KeYmaera X prover; verified transitions are therefore entailed triples, visible to SPARQL queries, including property paths alongside asserted data.
Table 1: Syntax of dL formulas and hybrid programs
dL Formulas (φ,ψ)
SyntaxMeaning
[α]​φAfter all runs of α, φ holds (safety)
⟨α⟩​φSome run of α reaches a state where φ holds (liveness)
φ∧ψConjunction (and)
φ∨ψDisjunction (or)
φ→ψImplication
φ↔ψBiimplication (equivalence)
Hybrid Programs (α,β)
SyntaxMeaning
α;βSequential: do α then β
α∪βChoice: execute either α or β
x:=tDiscrete assignment: set x to the value of t
{x′=t,y′=s&Q}Continuous evolution: x˙=t,y˙=s within domain Q
Figure 2: Main Classes and Properties of our Ontology.
Figure 2: Main Classes and Properties of our Ontology.
Table 2: SHACL constraints and their dL correspondents.
SHACL constraintdL literal
sh:hasValuex=c
sh:minInclusivex≥c
sh:maxInclusivex≤c
sh:minExclusivex>c
sh:maxExclusivex<c
Figure 3: Yogurt and drum-boiler examples.
Figure 3: Yogurt and drum-boiler examples.
Table 3: Notation used in the SHACL → dL mapping.
SymbolMeaning
pURI of a numeric evolving variable, e.g. ex:T
f,vSHACL constraint components and their literal values
θfComparison operator mapped from f (Table 2)
𝗆𝗈𝖽𝖾dCurrent mode of device d
MdFinite set of modes declared for device d
𝐟ODE derivatives (:derivative)
Q⁡(𝐱)Evolution-domain constraint
Figure 4: Oven and Tank Example
Figure 4: Oven and Tank Example
Table 4: Evaluation Results
Use CaseStatesModesState Transitions.Correct Transitions.dL Obligations.Sound / Global Inv.
Oven424440Yes/Yes
Empty Tank524436Yes/Yes
Yogurt1481818350Yes/Yes
Drumboiler524440Yes/Yes
Table 5: Valid real-time state mapping to correct SHACL shapes.
DomainReal-time StateMatched State
OvenOven: On, x=60s12
OvenOven: Off, x=150s11
OvenOven: On, x=190s21
OvenOven: Off, x=200s22
YogurtHeater: On, x=45; Homogenizer: Off, p=9s112
YogurtHeater: Off, x=50; Homogenizer: Off, p=8s122
YogurtHeater: On, x=60; Homogenizer: On, p=15s311
YogurtHeater: On, x=110; Homogenizer: Off, p=2s212
TankTank1: Off,h1=1.0 ; Tank2: Off,h2=0.1s0
TankTank1: On,h1=1.0 ; Tank2: On,h2=0.1s1
TankTank1: Off,h1=0.5 ; Tank2: Off,h2=0.5s2
TankTank1: On,h1=0.0 ; Tank2: On,h2=1.0s3
TankTank1: Off,h1=0.0 ; Tank2: Off,h2=1.0s4

为什么重要

在制造业数字孪生这类需要同时处理设备信息和物理规律的场景中,过去工程师必须用不同工具分别回答'谁负责这台设备'和'这次转换是否物理上安全'这两类问题。RDFdL展示了一种把两类问题合并进同一个SPARQL查询的方法,把经过形式化验证的物理行为当作普通图数据来对待。

本文术语

  • RDF · 用主语-谓语-宾语三元组表示事实的图数据模型
  • SHACL · 用于校验RDF数据是否符合特定形状约束的语言
  • SPARQL · 在RDF图中检索模式的查询语言
  • Differential Dynamic Logic(dL) · 用于对连续微分方程动态与离散模式切换混合的系统证明安全性和可达性的形式化逻辑
  • KeYmaera X · 用来完成dL证明义务的定理证明软件
  • entailment(蕴含推导) · 并非直接写明、而是通过推理得出的事实,被作为新三元组加入图中

论文原文摘要（英文）

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.

作者 · Yuyang Li, Lukas Kubelka, Julia Butte, Tobias K\"afer

在 arXiv 阅读

最新论文

全部论文 →

METAL MEDIA 最新报道

图片来源： Yuyang Li et al., arXiv:2608.18165, CC BY 4.0