RDFdL: Integrating RDF with Differential Dynamic Logic

Yuyang Li; Lukas Kubelka; Julia Butte; Tobias Käfer

cs.AIAug 16, 2026

RDFdL: Integrating RDF with Differential Dynamic Logic

Authors: Yuyang Li, Lukas Kubelka, Julia Butte, Tobias Käfer

Organizations: Institute AIFB, Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany

Abstract

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.

Figures & tables

dL Formulas ( $\varphi,\psi$ )
Syntax	Meaning
$[\alpha]\varphi$	After all runs of $\alpha$ , $\varphi$ holds (safety)
$\langle\alpha\rangle\varphi$	Some run of $\alpha$ reaches a state where $\varphi$ holds (liveness)
$\varphi\wedge\psi$	Conjunction (and)
$\varphi\vee\psi$	Disjunction (or)
$\varphi\to\psi$	Implication

Table 1: Syntax of dL formulas and hybrid programs

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 2: Main Classes and Properties of our Ontology.

SHACL constraint	dL literal
sh:hasValue	$x=c$
sh:minInclusive	$x\geq c$
sh:maxInclusive	$x\leq c$
sh:minExclusive	$x>c$
sh:maxExclusive	$x<c$

Table 2: SHACL constraints and their dL correspondents.

Symbol	Meaning
$p$	URI of a numeric evolving variable, e.g. ex:T
$f,v$	SHACL constraint components and their literal values
$\theta_{f}$	Comparison operator mapped from $f$ (Table 2 )
$\mathsf{mode}_{d}$	Current mode of device $d$
$M_{d}$	Finite set of modes declared for device $d$
$\mathbf{f}$	ODE derivatives ( :derivative )

Table 3: Notation used in the SHACL

\rightarrow

dL mapping.

Figure 3: Yogurt and drum-boiler examples.

Use Case	States	Modes	State Transitions.	Correct Transitions.	dL Obligations.	Sound / Global Inv.
Oven	4	2	4	4	40	Yes/Yes
Empty Tank	5	2	4	4	36	Yes/Yes
Yogurt	14	8	18	18	350	Yes/Yes
Drumboiler	5	2	4	4	40	Yes/Yes

Table 4: Evaluation Results

Domain	Real-time State	Matched State
Oven	Oven: On, x=60	s12
Oven	Oven: Off, x=150	s11
Oven	Oven: On, x=190	s21
Oven	Oven: Off, x=200	s22
Yogurt	Heater: On, x=45; Homogenizer: Off, p=9	s112
Yogurt	Heater: Off, x=50; Homogenizer: Off, p=8	s122

Table 5: Valid real-time state mapping to correct SHACL shapes.

fromState	predicate	predLabel	toState
ex:s11	ex:Oven_OffMode_to_OnMode	"Change Off → On"	ex:s12
ex:s12	:next		ex:s21
ex:s21	ex:Oven_OnMode_to_OffMode	"Change On → Off"	ex:s22
ex:s22	:next		ex:s11

Listing 6 SPARQL query and extracted “happy-path” transitions (oven).

Explore similar work

Constructing Dynamic Master Logic Models as Knowledge Graphs for Complex System Diagnostics Using Retrieval-Augmented Large Language Models
Aug 12, 2026Saman Marandi, Yu-Shu Hu, Mohammad ModarresKG Construction Fault Diagnosis
Center for Risk and Reliability, University of Maryland, 0151F Glenn L. Martin Hall, Building 088, College Park, MD 20742, United States · DML Inc., Hsinchu, Taiwan
The Robot Data Factory
Sep 15, 2026Sami Haddadin, Ivan Laptev, Ian Reid +18Robotic Data Collection Robotics
Mohamed Bin Zayed University of Artificial Intelligence, Abu Dhabi, UAE
Beyond Explicit Edges: Robust Reasoning over Noisy and Sparse Knowledge Graphs
Mar 14, 2026Hang Gao, Dimitris N. MetaxasGraph Retrieval-Augmented Generation Graph-Based Retrieval
Department of Computer Science, Rutgers University, Piscataway, New Jersey, USA.

Aug 12, 2026J/K move · Enter open · S save

Constructing Dynamic Master Logic Models as Knowledge Graphs for Complex System Diagnostics Using Retrieval-Augmented Large Language Models

Saman Marandi, Yu-Shu Hu, Mohammad Modarres

Center for Risk and Reliability, University of Maryland, 0151F Glenn L. Martin Hall, Building 088, College Park, MD 20742, United States · DML Inc., Hsinchu, Taiwan

KG Construction Fault Diagnosis

Open paper AskPDF arXiv

Dynamic Master Logic (DML) provides a hierarchical framework for representing system behavior by linking functional objectives to underlying structural elements. However, DML construction typically relies on expert interpretation of technical documentation, limiting scalability for complex systems. This study presents a framework for automated construction of DML models from system descriptions and their representation as Knowledge Graphs (KG-DML), using Retrieval-Augmented Generation and Large Language Models as enabling tools. Building on prior work with small-scale systems, the framework extends automated KG-DML construction and evaluation to substantially larger and more complex systems. Model construction proceeds across the DML hierarchy using targeted retrieval while preserving functional dependencies and explicit logical relationships. The resulting KG-DML supports diagnostic reasoning, safety assessment, upward failure propagation, and downward dependency tracing. A multi-level validation methodology evaluates layer-specific precision and recall, logical gate consistency, and overall structural integrity. Application to the Low-Pressure Coolant Injection system of a decommissioned Boiling Water Reactor demonstrates consistent reconstruction across repeated runs. The results show that automated KG-DML construction can transform technical documentation into executable functional models for diagnostic and reliability analysis.

Abstract

Explore similar work

Constructing Dynamic Master Logic Models as Knowledge Graphs for Complex System Diagnostics Using Retrieval-Augmented Large Language Models

The Robot Data Factory

Beyond Explicit Edges: Robust Reasoning over Noisy and Sparse Knowledge Graphs