RDFdL: Integrating RDF with Differential Dynamic Logic
A framework lets you ask a single graph query that checks both 'is this physical transition safe' and 'who is the technician responsible for it'
RDF knowledge graphs are good at describing static facts like devices, buttons, and responsible technicians, but they cannot capture how physical quantities like temperature change continuously over time. The authors built RDFdL, which links RDF with Differential Dynamic Logic (dL), a formal language for verifying systems that mix continuous physics with discrete mode switches, so that both kinds of information can be queried together. They tested it on an oven, a yogurt production line, an industrial drum-boiler, and a coupled tank system, showing that verified physical behavior can be exposed as ordinary graph data.
METAL MEDIA explanatory visual
A framework lets you ask a single graph query that checks both 'is this physical transition safe' and 'who is the technician responsible for it'
- 01A question like 'can the oven's temperature safely reach a target range once it's switched on' cannot be answered by plain RDF or SPARQL, because temperature evolves according to a differential equation, and RDF has no built-in meaning for continuous change over time
- 02The team represents 'state regions'—combinations of a numeric variable range (like temperature) and a device mode (on/off)—in RDF and SHACL, then automatically translates them into dL formulas; Apache Jena handles RDF reasoning while the KeYmaera X theorem prover carries out the actual dL verification
- 03Candidate transitions between two state regions are not accepted as facts directly; instead they become dL proof obligations sent to KeYmaera X, and only the transitions that are successfully proven are added back into the RDF graph as new triples via predicates :next and :modeChange, which lets SPARQL's property-path queries answer multi-step reachability questions
- 04Evaluated on an oven, a yogurt production line with 14 state changes, an industrial drum-boiler, and a two-tank system with nonlinear coupled dynamics: for linear/polynomial cases, the number of proof obligations grew roughly linearly with the number of states and modes, and even the nonlinear tank system, despite requiring more complex algebraic decision procedures, had all its obligations successfully discharged
- 05SHACL is used to validate real-time sensor readings against the correct symbolic state region (e.g., matching a 185-degree, off-mode reading to its shape), while reachability and safety guarantees remain the job of dL proofs, keeping the two roles clearly separated
What they did
- A question like 'can the oven's temperature safely reach a target range once it's switched on' cannot be answered by plain RDF or SPARQL, because temperature evolves according to a differential equation, and RDF has no built-in meaning for continuous change over time
- The team represents 'state regions'—combinations of a numeric variable range (like temperature) and a device mode (on/off)—in RDF and SHACL, then automatically translates them into dL formulas; Apache Jena handles RDF reasoning while the KeYmaera X theorem prover carries out the actual dL verification
- Candidate transitions between two state regions are not accepted as facts directly; instead they become dL proof obligations sent to KeYmaera X, and only the transitions that are successfully proven are added back into the RDF graph as new triples via predicates :next and :modeChange, which lets SPARQL's property-path queries answer multi-step reachability questions
- Evaluated on an oven, a yogurt production line with 14 state changes, an industrial drum-boiler, and a two-tank system with nonlinear coupled dynamics: for linear/polynomial cases, the number of proof obligations grew roughly linearly with the number of states and modes, and even the nonlinear tank system, despite requiring more complex algebraic decision procedures, had all its obligations successfully discharged
- SHACL is used to validate real-time sensor readings against the correct symbolic state region (e.g., matching a 185-degree, off-mode reading to its shape), while reachability and safety guarantees remain the job of dL proofs, keeping the two roles clearly separated
| dL Formulas (φ,ψ) | |
|---|---|
| Syntax | Meaning |
| [α]φ | After all runs of α, φ holds (safety) |
| ⟨α⟩φ | Some run of α reaches a state where φ holds (liveness) |
| φ∧ψ | Conjunction (and) |
| φ∨ψ | Disjunction (or) |
| φ→ψ | Implication |
| φ↔ψ | Biimplication (equivalence) |
| Hybrid Programs (α,β) | |
| Syntax | Meaning |
| α;β | Sequential: do α then β |
| α∪β | Choice: execute either α or β |
| x:=t | Discrete assignment: set x to the value of t |
| {x′=t,y′=s&Q} | Continuous evolution: x˙=t,y˙=s within domain Q |
| SHACL constraint | dL literal |
|---|---|
| sh:hasValue | x=c |
| sh:minInclusive | x≥c |
| sh:maxInclusive | x≤c |
| sh:minExclusive | x>c |
| sh:maxExclusive | x<c |
| Symbol | Meaning |
|---|---|
| p | URI of a numeric evolving variable, e.g. ex:T |
| f,v | SHACL constraint components and their literal values |
| θf | Comparison operator mapped from f (Table 2) |
| 𝗆𝗈𝖽𝖾d | Current mode of device d |
| Md | Finite set of modes declared for device d |
| 𝐟 | ODE derivatives (:derivative) |
| Q(𝐱) | Evolution-domain constraint |
| 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 |
| 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 |
| Yogurt | Heater: On, x=60; Homogenizer: On, p=15 | s311 |
| Yogurt | Heater: On, x=110; Homogenizer: Off, p=2 | s212 |
| Tank | Tank1: Off,h1=1.0 ; Tank2: Off,h2=0.1 | s0 |
| Tank | Tank1: On,h1=1.0 ; Tank2: On,h2=0.1 | s1 |
| Tank | Tank1: Off,h1=0.5 ; Tank2: Off,h2=0.5 | s2 |
| Tank | Tank1: On,h1=0.0 ; Tank2: On,h2=1.0 | s3 |
| Tank | Tank1: Off,h1=0.0 ; Tank2: Off,h2=1.0 | s4 |
Why it matters
In cyber-physical settings like manufacturing digital twins, engineers previously needed separate tools to ask 'who is responsible for this device' versus 'is this physical transition actually safe,' forcing them to stitch together answers manually. RDFdL shows a way to merge both kinds of questions into a single SPARQL query, treating formally verified physical behavior as just another piece of graph data.
Terms in this paper
- RDF · A graph data model that represents facts as subject-predicate-object triples
- SHACL · A constraint language used to validate whether RDF data conforms to defined shapes
- SPARQL · The query language used to search patterns in RDF graphs
- Differential Dynamic Logic (dL) · A formal logic for specifying and proving safety/reachability properties of hybrid systems that combine continuous ODE-governed dynamics with discrete mode switches
- KeYmaera X · A theorem prover software that discharges dL proof obligations
- entailment · Facts that are logically derived rather than explicitly stated, added into the graph as new triples
Original 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.
Read on arXivLatest papers
- SWE-bench Science: Can Coding Agents Resolve Engineering Tasks in Science?AI coding agents were tested on fixing real scientific software, and even the best one failed more than half the time
- FlashPrefill V2: Block-Sparse Prefill Attention for Long-Context LLM ServingMaking sparse attention fast enough and accurate enough for real LLM serving, not just papers
- PolicyGuide: From Guarding One Action to Guiding the Whole Workflow for Policy-Compliant LLM AgentsMaking customer-service AI agents follow the whole procedure, not just avoid one bad action
- EXIMO: VLM Guided Exploration of VLA PoliciesTeaching a robot new chores without human teleoperation, by letting a chatty AI supervise it
- EnvHarness: Awakening Static Worlds for Agent LearningInstead of building new training worlds from scratch, this work adds a plug-in layer that reshapes existing ones around each agent's actual weaknesses
- Bounded Sovereignty and the Control Tax: Pricing AI Oversight When the Deployer Does Not Own the ModelCompanies that rent AI instead of owning it can only do half of AI safety oversight
- PersonalBench: Measuring the Authorship Gap in LLM PersonalizationAI can be prompted to write 'like someone,' but its own voice never fully disappears
- Automated Summarization of Financial News Using Large Language Models and Retrieval-Augmented Generation: An Early Empirical Study (Fall 2023)Testing AI summaries of stock news, the simple approach beat the trendy retrieval-based one
Latest from METAL MEDIA
Figures: Yuyang Li et al., arXiv:2608.18165, CC BY 4.0