OntoSTL: Canonical Knowledge Graph Representation of Signal Temporal Logic Requirements
TL;DR
OntoSTL defines a bidirectional transformation between STL and OWL and applies equivalence-preserving canonicalization rules, including implication elimination, supported Negation Normal Form (NNF) conversion, Boolean simplification, associative flattening, and deterministic operand ordering.
Abstract
Formal verification of safety-critical cyber-physical systems uses languages such as Signal Temporal Logic (STL) to express time-sensitive properties over real-valued signals. However, large collections of formal requirements often contain recurring structural patterns that remain hidden in syntactically different formulas. Model-Driven Engineering supports requirement traceability, although existing methods provide limited means to identify and exploit these patterns within requirement sets. We address this limitation through OntoSTL, which first transforms STL formulas into Web Ontology Language (OWL) knowledge graphs then performs canonicalization on the formulas. The resulting representation supports querying with the SPARQL Protocol and RDF Query Language (SPARQL) and validation with the Shapes Constraint Language (SHACL). OntoSTL defines a bidirectional transformation between STL and OWL and applies equivalence-preserving canonicalization rules, including implication elimination, supported Negation Normal Form (NNF) conversion, Boolean simplification, associative flattening, and deterministic operand ordering. An analysis of 8,888 STL formulas identified 2,439 distinct structural topologies before canonicalization and 2,032 afterward, which indicates structural redundancy. The transformation algorithms terminate and preserve the information required to reconstruct formulas within the supported STL fragment. Empirical evaluation demonstrates round-trip structural preservation and an average processing time of 2.22 ms per formula.