Source-linked AI summary
RDFdL: Integrating RDF with Differential Dynamic Logic
Yuyang Li, Lukas Kubelka, Julia Butte, Tobias Käfer
TL;DR
RDF knowledge graphs lack semantics for continuous physical dynamics, while differential dynamic logic lacks metadata integration. RDFdL connects them by translating RDF/SHACL hybrid-system descriptions into dL proof obligations, enabling SPARQL queries over verified transitions and complete verified paths.
Problem
RDF describes structural knowledge but lacks semantics for continuous dynamics, while dL cannot represent associated metadata needed for integrated cyber-physical-system queries.
Method
RDFdL represents hybrid systems with ODEs and SHACL-defined states, translates them into dL proof obligations, and materializes prover-verified transitions as RDF triples.
Results
RDFdL supports reachability-style queries that extract complete verified transition paths between two states.
Takeaways & Limitations
Verified dynamic behavior becomes queryable alongside RDF metadata through SPARQL, including complete “happy paths” between states.
Takeaways & Limitations
RDFdL is sound but incomplete because transitions may remain unmaterialized when proofs are inconclusive or resource bounds are exceeded.
Abstract
from arXiv · showhide
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.
1 Introduction
RDF knowledge graphs describe static cyber-physical-system information but cannot by themselves reason about ODE-governed behavior such as reachability and safety. RDFdL bridges RDF and differential dynamic logic so verified hybrid-system behavior becomes queryable graph data while RDF supplies models for verification.
- Motivation: RDF provides identifiable resources, typed relations, schemas, provenance, and queries for cyber-physical information including devices, sensors, controllers, products, operators, and configurations.In manufacturing, such information is often represented through digital-twin descriptions and asset models.
- Motivation: Standard RDF, RDFS, OWL, SHACL, and SPARQL cannot solve reachability or safety problems for systems governed by ordinary differential equations.Whether transitions are possible, safe, or forbidden depends on how physical processes evolve over time.
- Approach: Differential dynamic logic models discrete control actions together with continuous ODE evolution and supports specifying and proving hybrid-system properties such as safety bounds.The paper positions dL as the verification language rather than a replacement for RDF reasoning.
- Contributions: The bridge makes verified continuous and discrete behavior queryable as graph data while using graph-defined state regions, modes, metadata, and candidate transitions to generate proof obligations.The implementation combines Apache Jena for RDF reasoning and querying with KeYmaera X for dL verification.
- Contributions: RDFdL translates RDF and SHACL representations of hybrid systems, including ODEs and state definitions, into dL formulae for verification.The framework uses RDF for formal hybrid-system representation and SHACL for state definition.
2 Preliminaries
This section defines the RDF, SHACL, and SPARQL foundations of RDFdL and introduces the differential dynamic logic used to model hybrid-system behavior. It also distinguishes safety and reachability modalities and explains the practical challenge of verifying diamond-form reachability properties.
- RDF: RDF represents RDFdL knowledge as triples in labeled directed graphs, including devices, variables, modes, state regions, ODE records, transitions, proofs, and metadata.Triples contain a subject, predicate, and object; RDFdL uses Turtle syntax.
- SHACL: SHACL defines and validates RDF state descriptions through cardinality and value-range constraints, while leaving ODE, continuous-evolution, and dL semantics to proof obligations.It validates observations and well-formed RDF descriptions, such as a temperature-185 observation in an Off mode matching a high-temperature off-region.
- SPARQL: SPARQL queries static facts and dynamic information by matching basic graph patterns, applying filters and property paths, and traversing materialized transition edges for reachability queries.The approach uses SPARQL to query verified transition graphs after dL proof results have been materialized.
- Differential Dynamic Logic: Differential dynamic logic specifies and verifies hybrid systems whose behavior combines discrete transitions with continuous evolution along differential equations.Hybrid programs use constructs including continuous evolution with an evolution domain, sequential composition, nondeterministic choice, and finite repetition.
- Differential Dynamic Logic: The box modality [α]φ expresses safety over every execution, whereas the diamond modality ⟨α⟩φ expresses reachability through some execution between RDF state regions.RDFdL primarily targets reachability, but KeYmaera X strongly supports safety formulas and not direct diamond-form liveness verification, motivating a reformulation described later.
3 Motivating Example and Problem Setting
This section uses a production oven to define RDFdL’s problem setting: RDF captures metadata and candidate behavior, while dL verifies hybrid-system transitions and safety before verified results become queryable graph data. The example also distinguishes SHACL-based region identification from dL-based reachability and safety verification.
- Oven example: The oven has On and Off modes, continuous temperature T, heating and cooling dynamics, and safety bound T ≤200.Its metadata includes device, production, control, batch, and technician relationships represented as RDF graph data.
- Oven example: Four symbolic regions abstract temperature and mode: s11 and s12 cover T < 180, while s21 and s22 cover 180 ≤T ≤200.The regions form a finite abstraction, with T = 180 separating controller ranges and T = 200 marking safety.
- Verification requirements: The intended path s11→s12→s21→s22 is only candidate behavior until continuous reachability and guarded mode changes are verified.RDF graph presence alone does not establish that s12→s21 is reachable under the heating ODE or that mode changes satisfy modeled guards.
- Verification requirements: RDFdL generates dL proof obligations for candidate transitions and materializes a transition as an entailed triple only after the required verdict is discharged.Verified transitions can then be queried together with the original RDF metadata.
- General problem setting: SHACL validates runtime observations against region shapes, whereas dL proof obligations handle reachability and safety rather than merely identifying the current symbolic region.For example, an observation with mode Off and T = 185 can validate against s22 without proving that s22 is reachable.
- General problem setting: The general problem is to construct a verified RDF transition graph from regions, ODEs, guards, metadata, and candidate transitions, exposing only dL-justified dynamics to graph queries.RDF-only reasoning cannot prove ODE reachability or safety, while dL-only verification lacks graph-level metadata and SPARQL integration.
4 Approach
RDFdL models hybrid-system dynamics as RDF and SHACL data linked to device modes, then embeds dL verification within Jena inference. This makes prover-verified transitions entailed RDF triples that SPARQL queries can traverse alongside asserted data.
- Inputs: RDFdL ingests FMU simulation models and traces plus engineer-authored metadata, representing state regions and operating ranges as ordinary graph data.Tooling can construct state diagrams from FMU variable metadata and trace-derived operating ranges.
- Verification integration: Jena inference rules invoke KeYmaera X for state-pair proof obligations, deriving :next and :modeChange only when the required dL verdict is discharged.Proof verdicts are memoized per state pair, so each obligation is proved at most once per session.
- Data modeling: Its vocabulary links devices and modes to ODEs, state regions to SHACL numeric bounds, workflows to initial states, and variables to mathematical symbols.Variable symbols provide the formal alignment between RDF resources and identifiers in ODE, guard, and evolution-domain expressions.
- Dynamic representation: ODE-backed mode records define guards, evolution-domain invariants, and evolving variables, turning RDF triples into a hybrid-system model of discrete and continuous behavior.Triples select a discrete mode, while the attached ODE governs continuous evolution between state transitions.
- Querying verified behavior: Because entailed and asserted triples are evaluated uniformly, SPARQL property paths range over verified behavior, including paths combining :next and :modeChange.The predicates are subproperties of rdfdl:transition, allowing a single transition property path to traverse both verified edge types.
5 Extracting and Proving State Transitions
RDFdL extracts state predicates and transition obligations from RDF/SHACL, proves them with KeYmaera X, and materializes verified transition relations as RDF entailments. Its soundness results establish safety over verified paths, while inconclusive proofs and absent triples remain non-conclusive.
- Verification pipeline: The pipeline extracts dL specifications from RDF, proves them with KeYmaera X, and interprets verdicts through decision rules for transition predicates.SHACL NodeShapes encode numeric state-region bounds and classify runtime observations by validation.
- Transition proving: RDFdL tests reachability by refuting a safety-style box obligation over φ1 ∨φ2, with well-formedness ensuring that leaving φ1 enters φ2.Ill-formed candidates are rejected after automatic quantifier-elimination checks.
- State-predicate extraction: SHACL constraints translate into conjunctive dL state predicates; for oven region s11, φ11 = T < 180 ∧modeOven = Off.The mapping converts numeric constraints into atomic comparisons and mode constraints into mode literals.
- Transition predicates: A refuted obligation entails an :next transition, a valid obligation sets isNext false, and an inconclusive proof conservatively materializes no transition.The decision rules record inconclusive outcomes rather than treating them as evidence that the transition is impossible.
- Soundness and safety: Verified continuous and discrete edges are sound, and if every region entails a global invariant, every finite path preserves it; for the oven, all verified paths preserve T ≤200.The result follows from continuous-edge and discrete-edge soundness plus induction over path length.
- Limitations: RDFdL is sound but incomplete: an absent transition triple may indicate impossible behavior, inconclusive automation, or an exceeded resource bound.Entailed :next and :modeChange triples correspond to verified hybrid behavior, but absence does not establish behavioral absence.
6 Evaluation
The evaluation demonstrates RDFdL across four cyber–physical case studies, combining RDF state-transition reasoning with dL verification. All modeled obligations and safety invariants are handled successfully, while proof growth is approximately linear for polynomial dynamics and SHACL supports runtime state validation.
- Case studies: RDFdL models four representative processes: an oven thermostat, a two-tank nonlinear flow system, a yogurt line, and a linearized drum-boiler system.The cases span single-device, multi-device, nonlinear, and linearized dynamics.
- Logical correctness: Safety properties verified in dL become RDF entailments, while verified continuous or discrete edges compose into paths preserving global invariants.Formal lemmas establish soundness for every verified edge and invariant preservation for composed paths.
- Scalability: For the Oven, Drumboiler, and Yogurt process, proof obligations grow approximately linearly with the number of modes and states.The tank system remains successfully discharged despite two-dimensional nonlinear flows and decision procedures with doubly exponential complexity.
- Verification results: All four case studies automatically generate state transitions, discharge all dL obligations, and prove preservation of the global safety invariant.The workflow uses Jena for transition generation and KeYmaera X for dL obligations.
- Runtime validation: SHACL filters invalid real-time states before RDFdL performs state-transition and next-state reasoning, enabling continuous runtime validation and transition verification.Out-of-range readings and inconsistent mode combinations are immediately flagged as invalid.
7 Related Work
Prior work applies semantic-web technologies to represent industrial assets, control systems, and manufacturing processes, while formal verification addresses safety in cyber-physical systems with continuous dynamics. Existing ontology-based approaches mainly model system dynamics as discrete process steps, leaving continuous dynamics less integrated with semantic-web representations.
- Semantic-web AAS models: Asset Administration Shells provide standardized containers for digital-twin information about physical industrial assets in Industry 4.0 frameworks.Digital twins remain linked to their real industrial counterparts.
- Semantic-web technologies for manufacturing: RDF/OWL and SPARQL model heterogeneous engineering data and can automatically detect inconsistencies in interdisciplinary production-system models.SHACL is also identified as a semantic-web technology used in this modeling context.
- Formal verification of CPS: Differential dynamic logic specifies that safety properties remain true after control decisions and continuous evolutions under given initial conditions.This supports formal verification of cyber-physical systems combining control logic with continuous physical processes.
- Discrete dynamics and the Semantic Web: Existing ontology-based approaches to system dynamics primarily represent manufacturing and business processes as discrete steps.These approaches support requirements verification against concurrent procedural flows or process-ontology descriptions.
8 Discussion
RDFdL bridges RDF/SPARQL’s static metadata and dL’s verified continuous dynamics by materializing verified transitions as queryable RDF triples. It supports reachability queries that combine static links with complete verified transition paths.
- Why RDFdL?: RDFdL closes the gap between SPARQL’s RDF queries and dL’s continuous-dynamics reasoning by materializing every dL-verified transition as a queryable RDF triple.SPARQL lacks semantics for continuous dynamics, while pure dL lacks metadata and master data.
- Why RDFdL?: SPARQL can query reachability over the state space while following static RDF links from buttons to devices to technicians.This combines RDF metadata and SPARQL queries with proven dL lemmas for continuous behavior.
- Beyond the running example: RDFdL supports reachability-style queries that extract complete verified transition paths between two states.The oven case illustrates this capability in Appendix 12.
9 Conclusion
RDFdL integrates RDF knowledge graphs with Differential Dynamic Logic to represent hybrid systems, verify their dynamics, and expose verified transitions for SPARQL querying.
- Contributions: RDFdL represents hybrid systems in RDF using ordinary differential equations and SHACL-based state definitions.This representation captures continuous dynamics within an RDF-based knowledge-graph framework.
- Contributions: An automated pipeline extracts differential-logic proof obligations from RDF and verifies them with the KeYmaera X prover.The pipeline connects RDF data processing with formal verification in dL.
- Contributions: RDFdL exposes verified system transitions as RDF triples that can be queried by SPARQL engines.This makes verification results available within RDF query workflows.
Supplemental Material Statement
Supplemental codes, simulation models, implementation scripts, and ontology information are publicly provided to support reproducing the paper’s case studies and results.
- Supplemental codes and simulation models for all case studies are available in the RDFdL repository.The repository also includes the full RDFdL pipeline implementation and build scripts needed to reproduce the results.
- The RDFdL ontology information is listed at the project’s archived vocabulary URL.The statement provides the ontology location at https://purl.archive.org/rdfdl/vocab.
Appendix · 10 ODE
The oven example represents state variables and an ordinary differential equation (ODE) using RDF individuals or blank nodes. Device modes connect to the oven and may link to a blank node encoding the ODE, with details provided in Listing 4.
- Appendix: The oven example introduces RDF individuals or blank nodes to represent state variables and the ODE.This establishes the RDF representation used for the oven’s dynamic model.
- 10 ODE: ex:OvenOnMode and ex:OvenOffMode are examples of individuals representing oven modes.Both modes are explicitly identified in the example.
- 10 ODE: Each oven mode has an ex:hasDevice property connecting it to ex:Oven.The property links the modes to the oven resource.
- 10 ODE: The resource ex:Oven is described as a Heater device.The example identifies the oven’s device type as a heater.
- 10 ODE: The oven modes may use ex:hasODE to link to a blank node that encodes the oven’s ODE.The ODE is therefore represented separately and connected through an RDF property.
- Appendix: The RDF details of the oven’s state-variable and ODE representation appear in Listing 4.The passage directs readers to Listing 4 for the concrete RDF encoding.
11 State representation in SHACL · 12 More Application
The paper represents oven states in RDF using SHACL node shapes that constrain temperature, mode, and state structure. It then queries verified transitions to recover the oven’s nominal “happy path” from ex:s11 to ex:s22.
- 11 State representation in SHACL: The oven state representation uses SHACL node shapes for the oven and its enclosing state.The state shape targets ex:State and requires an ex:hasOven property linked to ex:s11OvenShape.
- 11 State representation in SHACL: The oven shape requires exactly one ex:x value and exactly one ex:mode value.The mode must have value ex:OffMode.
- 11 State representation in SHACL: The example instantiates ex:s11 as an ex:State with an ex:Oven and the ex:s11Shape.This links the concrete state to its oven and state-shape descriptions.
- 12 More Application: The SPARQL query extracts verified transitions on the oven’s “happy path” from ex:s11 to ex:s22.It follows :next and :ModeChange paths from the starting state to the ending state and orders results by source state.
- 12 More Application: Every extracted state transition matches the ideal workflow described in the oven use case.The paper reports that the query results align perfectly with the nominal process steps.
- 12 More Application: The extracted workflow contains ex:s11→ex:s12, ex:s12→ex:s21, and ex:s21→ex:s22 transitions.The listed predicates are an oven Off-to-On mode change, :next, and an On-to-Off mode change, followed by :next.