PULSE: An Executable Contract Language for Spatiotemporal Knowledge Graph Engineering

# 1 Introduction
Source: [https://arxiv.org/html/2608.02630](https://arxiv.org/html/2608.02630)
###### Abstract

Knowledge graph engineering often distributes accepted state, observations, constraints, processes, and hypothetical scenarios across artifacts whose combined execution contract remains external\. We present PULSE, an Object\-Process\-Methodology\-inspired language that localizes four operational roles and their write effects in one typed runtime\. Here, modes denote operational roles rather than modal or deontic logic\. The implemented contract fixes evidence non\-overwrite, branch isolation, grounded multi\-subject timers, guarded state change, and declaration\-ranked event ordering over time and space; an external runner still decides whether evidence becomes an authoritative move\. GeoSPARQL, SOSA, and SHACL remain generated views\. A core calculus gives an effect\-confinement lemma and six safety properties\. Lean 4 checks kernel analogues for positions, evidence, clocks, monitors, atomicity, and branch source retention; 88 tests, 3,534 bounded checks, and 32 Lean/Python runtime\-kernel cases bound the implementation claim to the checked cases\. First\-author implementations of a standards composition and a separate Sismic statechart reproduce the tested cold\-chain trace\. Across 37,440 generated temporal traces, PULSE matches a separate workflow and distinguishes ten single\-field mutants\. On the complete NOAA IBTrACSsince1980subset it agrees with GEOS and an event sweep on 1,476,290 transition\-zone pairs, including 4,800 sampled and 12,831 duration\-qualified events\. Project\-specific GeoSPARQL probes measure interface coverage\. Overall, the results support contract localization, safety arguments, and trace parity for the tested fragment; language superiority and usability remain outside the evaluation\.

Keywords:Knowledge graphs; executable contracts; spatiotemporal semantics; domain\-specific language; GeoSPARQL\.

Knowledge graphs \(KGs\) describe entities and relations, but operational models also record evidence, constrain states, react to time and location, and explore alternatives\. These concerns are commonly split across ontologies, observation and shape graphs, process models, spatial stores, and simulators\. Their semantics then depend on artifact boundaries: observations are not accepted updates, policies state obligations, scenarios must not mutate asserted state, and duration\-qualified departures are neither OWL axioms nor static SHACL violations\. Flattening them into ordinary triples obscures these distinctions\.

Object\-Process Methodology \(OPM\) integrates objects, processes, and states\[[10](https://arxiv.org/html/2608.02630#bib.bib10),[6](https://arxiv.org/html/2608.02630#bib.bib6)\]\. PULSE \(Process\-aware Unified Language for Semantic Evolution\) adopts that paradigm without claiming an ISO 19450 profile or full OPM implementation\. Executable OPM also predates this work\[[23](https://arxiv.org/html/2608.02630#bib.bib23),[16](https://arxiv.org/html/2608.02630#bib.bib16)\]\. PULSE instead contributes a narrower KG\-facing role/effect and deterministic spatiotemporal contract, with OWL/RDF serving as a generated view rather than the authoritative representation\.

An OWL–SHACL–workflow composition can reproduce a PULSE trace, as our baseline demonstrates\. We therefore evaluate contract localization: write partitions, scenario isolation, binding, and temporal order share one checked model/runtime boundary instead of residing in separately profiled adapters\. Observation acceptance remains at the runner\.

The contribution is established by \(1\) the language and Core calculus with an explicit write\-effect judgment and six safety results; \(2\) paper proof sketches and a Lean\-checked post\-parse subset covering kernel compilation, clocks, grounded monitors, and selected transition\-order fixtures; and \(3\) standards\-composition and Sismic baselines, mutation analysis, complete modern\-era trajectories, and external spatial engines\. Scale and persistence are secondary engineering evidence\.

## 2 Related Work and Positioning

OWL 2 provides open\-world axioms\[[17](https://arxiv.org/html/2608.02630#bib.bib17)\], SHACL validates RDF graphs\[[14](https://arxiv.org/html/2608.02630#bib.bib14)\], GeoSPARQL defines spatial RDF and query functions\[[2](https://arxiv.org/html/2608.02630#bib.bib2)\], and SOSA/SSN and OWL\-Time represent observations and temporal entities\[[8](https://arxiv.org/html/2608.02630#bib.bib8),[3](https://arxiv.org/html/2608.02630#bib.bib3)\]\. PULSE reuses these standards at projection boundaries; none prescribes its four modes and process runtime\.

Reactive semantic data also predates PULSE: RDFTL executes event\-condition\-action rules over RDF, C\-SPARQL handles continuous queries, ontology\-driven processes infer task executability, and ExeKG translates KG\-described pipelines to scripts\[[21](https://arxiv.org/html/2608.02630#bib.bib21),[1](https://arxiv.org/html/2608.02630#bib.bib1),[22](https://arxiv.org/html/2608.02630#bib.bib22),[24](https://arxiv.org/html/2608.02630#bib.bib24)\]\. The PULSE claim is therefore limited to a fixed operational role/effect partition and clock contract\.

PROV\-O contextualizes provenance\[[15](https://arxiv.org/html/2608.02630#bib.bib15)\], SHACL\-AF adds SPARQL and triple rules\[[13](https://arxiv.org/html/2608.02630#bib.bib13)\], and statecharts and Sismic provide mature event execution\[[9](https://arxiv.org/html/2608.02630#bib.bib9),[5](https://arxiv.org/html/2608.02630#bib.bib5)\]\. PULSE neither subsumes their reasoning nor introduces modal logic; it fixes a small write discipline and sample\-and\-hold clock across their usual artifact boundaries\.

OPM and its RDF exports cover object\-process\-state modeling\[[6](https://arxiv.org/html/2608.02630#bib.bib6),[10](https://arxiv.org/html/2608.02630#bib.bib10),[11](https://arxiv.org/html/2608.02630#bib.bib11)\]; its simulation and MAXIM’s OPCloud extension also make OPM models executable\[[23](https://arxiv.org/html/2608.02630#bib.bib23),[16](https://arxiv.org/html/2608.02630#bib.bib16)\]\. PULSE instead omits most OPM links, hierarchy, graphical\-textual equivalence, and general computation, selecting four KG roles, typed write effects, and a fixed spatiotemporal clock\.

The Parallel World Framework isolates what\-if KG versions through named graphs and copy\-on\-write\[[7](https://arxiv.org/html/2608.02630#bib.bib7)\]; PULSE makes the same non\-interference goal a typed effect rather than an agent/persistence protocol\. LinkML supplies schema\-first generators\[[18](https://arxiv.org/html/2608.02630#bib.bib18)\], while SysML v2 has broader systems scope\[[19](https://arxiv.org/html/2608.02630#bib.bib19)\]; neither prescribes this role/effect\-and\-clock contract\.

The resulting artifact is a research kernel with a handwritten parser; IDE support and authoring\-cost evaluation remain future work\.

Table 1:Where the selected contract resides; “external” denotes a supported composition\.We operationalize*localization*only as contract placement: its unit is the declaration or adapter that must change when an obligation changes\. The tested PULSE path edits one typed model consumed by its compiler/runtime, whereas the profiled baseline places equivalent obligations across RDF/SHACL, a statechart, and binding, ordering, and clone adapters\. Tables[1](https://arxiv.org/html/2608.02630#S2.T1)and[5](https://arxiv.org/html/2608.02630#S6.T5)record those sites\. This structural measure records placement; authoring time, maintenance cost, and defect rate require separate study\.

## 3 Language and Semantics

### 3\.1 Modes and Typed Representation

PULSE co\-locates content without assigning one truth status\. In this paper,*mode*denotes an operational role with a distinct write set, and*normative*denotes guarded constraint validation; neither term asserts a modal or deontic calculus\. Assertions form accepted state, observations are source\-qualified evidence, constraints are read\-only obligations, and scenarios are counterfactual branches\. This requirements\-derived partition is neither universal nor exhaustive: merging observations into assertions removes the authoritative\-state non\-overwrite boundary, merging constraints into assertions confuses violations with facts, and merging scenarios into assertions breaks isolation\. Listing[1](https://arxiv.org/html/2608.02630#LST1)exercises the selected roles with space and time\.

Recording evidence leaves transition choice to the runner API\. PULSE guarantees authoritative\-state non\-overwrite before acceptance, while broader evidence governance remains external\. Scenario semantics require source isolation rather than one copying algorithm: the prototype copies mutable state, while copy\-on\-write overlays are equivalent if observably isolated\.

1modelColdChainSTversion"0\.1"

2crsC="http://www\.opengis\.net/def/crs/OGC/1\.3/CRS84"

3regionZcrsC=polygon\[\[121\.49,31\.19\],\[121\.51,31\.19\],

4\[121\.51,31\.21\],\[121\.49,31\.21\],\[121\.49,31\.19\]\]

5entityShipment\{

6propertyposition:PointcrsC

7stateconditiononeof\[Safe,AtRisk\]

8\}

9instancebatch:Shipment\{

10position=point\(121\.50,31\.20\)condition=Safe\}

11observebatch\.position=point\(121\.512,31\.201\)\{

12at"2026\-07\-19T08:20:00Z"sourcegpsconfidence0\.98

13accuracy5m\}

14constraintContainment\{

15mustcoveredBy\(batch\.position,Z\)

16whileShipment\.condition==Safe\}

17processSustainedDeparture\(s:Shipment\)\{

18whenleaves\(s\.position,Z\)for10min

19changess\.condition:Safe\-\>AtRisk\}

20scenarioReroute\{

21assumebatch\.position==point\(121\.515,31\.205\)

22run20minaskcoveredBy\(batch\.position,Z\)

23askbatch\.condition\}

Listing 1:A compact PULSE spatiotemporal model\.The artifact contains this listing as an executable regression case\. With no explicit scenario start,t0t\_\{0\}is the latest observation timestamp \(or the Unix epoch if none exists\); assumptions execute att0t\_\{0\}in declaration order andrun 20 minadvances the isolated branch tot0\+20t\_\{0\}\+20minutes before the questions are answered\. The example emits the sampled departure, emits its qualified event at ten minutes, answersfalseandAtRisk, and leaves the source model unchanged\.

The immutable document isM=⟨n,v,R,E,I,O,C,P,S⟩M=\\langle n,v,R,E,I,O,C,P,S\\rangle\. Table[2](https://arxiv.org/html/2608.02630#S3.T2)records the principal implemented fields; optional values are explicit\. Parsing is followed by name, type, state\-domain, geometry, CRS, and reference validation before a runtime world can be created\.

Table 2:Principal records in the implemented typed representation\.
### 3\.2 Spatial and Temporal Execution

Execution uses configurationsX=⟨A,O,q,Q,t⟩X=\\langle A,O,q,Q,t\\rangle: asserted valuesAA, append\-only evidenceOO, finite object statesqq, a finite partial timer mapQQ, and event timett\. The compiler grounds a parameterized process once per compatible instance, in instance\-declaration order, assigning identifiers such asSustainedDeparture@batch\.QQis keyed by that ground identifier, so different subjects may hold concurrent monitors for one source process\. The declarationobserveperforms only𝗋𝖾𝖼𝗈𝗋𝖽​\(o\):⟨A,O,q,Q,t⟩↦⟨A,O\+o,q,Q,t⟩\\mathsf\{record\}\(o\):\\langle A,O,q,Q,t\\rangle\\mapsto\\langle A,O\\mathbin\{\+\}o,q,Q,t\\rangle\. Authoritative change is instead the runner action𝗆𝗈𝗏𝖾​\_​𝖺𝗍​\(i,p,t′\)\\mathsf\{move\\\_at\}\(i,p,t^\{\\prime\}\); it is an input command, not a model declaration\. The application owns the acceptance decision that may cause this command; the language guarantees only that recording evidence alone never triggers a process\.

Let𝗂𝗇c​\(g,r\)\\mathsf\{in\}\_\{c\}\(g,r\)be boundary\-inclusive Point/Polygon membership under CRScc\. Before a move,t′≥tt^\{\\prime\}\\geq t, references, and CRS equality are checked; failure has no effect\. For every accepted position after the first, includingtk−1=tkt\_\{k\-1\}=t\_\{k\}, letgk−1g\_\{k\-1\}be the immediately preceding accepted sample andgkg\_\{k\}the new one\. Sampled entry/exit is derived by

𝖾𝗇𝗍𝖾𝗋𝗌​\(i,r,tk\)=¬𝗂𝗇​\(gk−1,r\)∧𝗂𝗇​\(gk,r\),𝗅𝖾𝖺𝗏𝖾𝗌​\(i,r,tk\)=𝗂𝗇​\(gk−1,r\)∧¬𝗂𝗇​\(gk,r\)\.\\begin\{split\}\\mathsf\{enters\}\(i,r,t\_\{k\}\)&=\\neg\\mathsf\{in\}\(g\_\{k\-1\},r\)\\land\\mathsf\{in\}\(g\_\{k\},r\),\\\\ \\mathsf\{leaves\}\(i,r,t\_\{k\}\)&=\\mathsf\{in\}\(g\_\{k\-1\},r\)\\land\\neg\\mathsf\{in\}\(g\_\{k\},r\)\.\\end\{split\}The runner first emits timers due byt′t^\{\\prime\}, ordered by\(𝑑𝑒𝑎𝑑𝑙𝑖𝑛𝑒,𝑔𝑟𝑜𝑢𝑛𝑑𝑅𝑎𝑛𝑘\)\(\\mathit\{deadline\},\\mathit\{groundRank\}\); it then compares old/new membership, updatesAA, cancels inverse monitors, starts new monitors, and applies immediate rules in declaration order\. Ground rank is assigned by process then instance declaration, so alpha\-renaming is inert\. Later rules see earlier state mutations; a source\-state mismatch skips a rule\. Same\-time input moves follow input order and may therefore create crossings and cancel/start monitors, but no time elapses between them\. Positions are sample\-and\-hold: an outside\-to\-outside segment that intersects a polygon yields no sampled event\. A monitor⟨e,t0,δ⟩\\langle e,t\_\{0\},\\delta\\ranglecancelled beforet0\+δt\_\{0\}\+\\deltaemits nothing; otherwise its effective time ist0\+δt\_\{0\}\+\\deltaand its emission time is the first clock advance exposing the deadline\. Thus a due timer precedes a same\-time move\. A scenario may clone an activeXX, including its clock and pending monitors; the default CLI branch instead starts from the compiled base world withQ=∅Q=\\emptyset\. Both execute assumptions as moves only on the clone\.

These write sets induce four implementation invariants\.*P1*𝗋𝖾𝖼𝗈𝗋𝖽\\mathsf\{record\}cannot overwriteAA\.*P2*scenario effects cannot reach the source configuration\.*P3*validation plus guarded rules keepsqqwithin declared state domains\.*P4*fixed validated input, timer ordering, input order, and rule order yield one trace or an atomic error\. The next section states these properties over a core calculus\.

## 4 Core Calculus and Properties

The surface language is resolved and desugared to a finite kernel\. LetIIandSiS\_\{i\}be finite sets of instances and states, and letRRandKKbe declaration\-ordered sequences of regions and ground specification identifiers\. Each parameterized process is expanded over compatible instances to a uniquek∈Kk\\in Kwith rankρ​\(k\)\\rho\(k\)\. For each CRScc,GcG\_\{c\}is the domain of finite valid geometries incc\. The implemented fragment restricts authoritative moving values to points and regions to simple polygons\. The immutable environment is

Γ=⟨𝑐𝑟𝑠,𝑟𝑒𝑔𝑖𝑜𝑛,𝑠𝑡𝑎𝑡𝑒𝐷𝑜𝑚𝑎𝑖𝑛,𝑟𝑢𝑙𝑒𝑠,𝑠𝑝𝑒𝑐𝑠,𝑐𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡𝑠⟩\.\\Gamma=\\langle\\mathit\{crs\},\\mathit\{region\},\\mathit\{stateDomain\},\\mathit\{rules\},\\mathit\{specs\},\\mathit\{constraints\}\\rangle\.Rules and sustained\-event specifications are declaration\-ordered; ground identifiers are unique and durations are positive\. Following standard type\-safety structure, the relevant judgments areΓ⊢g:𝖦𝖾𝗈𝗆𝖾𝗍𝗋𝗒​\[c\]\\Gamma\\vdash g:\\mathsf\{Geometry\}\[c\],Γ⊢o:𝖮𝖻𝗌𝖾𝗋𝗏𝖺𝗍𝗂𝗈𝗇​\[i\]\\Gamma\\vdash o:\\mathsf\{Observation\}\[i\],Γ⊢a:𝖠𝖼𝗍𝗂𝗈𝗇\\Gamma\\vdash a:\\mathsf\{Action\}, andΓ⊢X​𝗈𝗄\\Gamma\\vdash X\\;\\mathsf\{ok\}\. A spatial predicate is well typed only when its point and polygon share one CRS\.

Core actions and outcomes are

a::=𝗋𝖾𝖼𝗈𝗋𝖽\(o\)∣𝗆𝗈𝗏𝖾\(i,g,t′\)∣𝖺𝖽𝗏𝖺𝗇𝖼𝖾\(t′\),u::=𝗈𝗄\(X′,T\)∣𝖾𝗋𝗋𝗈𝗋\(e,X\),\\begin\{split\}a&::=\\mathsf\{record\}\(o\)\\mid\\mathsf\{move\}\(i,g,t^\{\\prime\}\)\\mid\\mathsf\{advance\}\(t^\{\\prime\}\),\\\\ u&::=\\mathsf\{ok\}\(X^\{\\prime\},T\)\\mid\\mathsf\{error\}\(e,X\),\\end\{split\}whereTTis a finite ordered trace\. Well\-formedness requires resolved identifiers, declared CRSs,q​\(i\)∈Siq\(i\)\\in S\_\{i\}, typed offset\-aware observations, unique pending monitors, and offset\-aware time\. A pending monitor contains a ground identifier, event, subject, region, start, positive duration, and an optional guarded rule\.

The write\-effect judgmentΓ⊢a⊳W\\Gamma\\vdash a\\triangleright Wassigns𝗋𝖾𝖼𝗈𝗋𝖽↦\{O\}\\mathsf\{record\}\\mapsto\\\{O\\\},𝗆𝗈𝗏𝖾↦\{A,q,Q,t\}\\mathsf\{move\}\\mapsto\\\{A,q,Q,t\\\}, and𝖺𝖽𝗏𝖺𝗇𝖼𝖾↦\{q,Q,t\}\\mathsf\{advance\}\\mapsto\\\{q,Q,t\\\}; validation and questions haveW=∅W=\\emptyset\. A successful action leaves every configuration component outsideWWunchanged\. This is the limited sense in which PULSE is an effect discipline; the judgment is paper\-level bookkeeping, not a separately mechanized general effect system\.

Evaluation is a deterministic big\-step relationΓ⊢⟨X,a⟩⇓u\\Gamma\\vdash\\langle X,a\\rangle\\Downarrow u\. Observation recording has the single rule

Γ⊢o:𝖮𝖻𝗌𝖾𝗋𝗏𝖺𝗍𝗂𝗈𝗇Γ⊢⟨⟨A,O,q,Q,t⟩,𝗋𝖾𝖼𝗈𝗋𝖽​\(o\)⟩⇓𝗈𝗄​\(⟨A,O⋅o,q,Q,t⟩,ϵ\)\.\\frac\{\\Gamma\\vdash o:\\mathsf\{Observation\}\}\{\\Gamma\\vdash\\langle\\langle A,O,q,Q,t\\rangle,\\mathsf\{record\}\(o\)\\rangle\\Downarrow\\mathsf\{ok\}\(\\langle A,O\{\\cdot\}o,q,Q,t\\rangle,\\epsilon\)\}\.For time advance,𝖽𝗎𝖾​\(Q,t′\)\\mathsf\{due\}\(Q,t^\{\\prime\}\)selects deadlines no later thant′t^\{\\prime\}and sorts them by\(𝑑𝑒𝑎𝑑𝑙𝑖𝑛𝑒,ρ​\(k\)\)\(\\mathit\{deadline\},\\rho\(k\)\); unique ground keys make equal deadlines unambiguous without depending on spelling\.𝖾𝗆𝗂𝗍\\mathsf\{emit\}removes those monitors, emits their semantic deadline and current emission time, and applies an attached rule only when its source state still matches:

t′≥tD=𝖽𝗎𝖾​\(Q,t′\)𝖾𝗆𝗂𝗍​\(X,D,t′\)=⟨A,O,q′,Q′,T⟩Γ⊢⟨X,𝖺𝖽𝗏𝖺𝗇𝖼𝖾​\(t′\)⟩⇓𝗈𝗄​\(⟨A,O,q′,Q′,t′⟩,T\)\.\\frac\{t^\{\\prime\}\\geq t\\quad D=\\mathsf\{due\}\(Q,t^\{\\prime\}\)\\quad\\mathsf\{emit\}\(X,D,t^\{\\prime\}\)=\\langle A,O,q^\{\\prime\},Q^\{\\prime\},T\\rangle\}\{\\Gamma\\vdash\\langle X,\\mathsf\{advance\}\(t^\{\\prime\}\)\\rangle\\Downarrow\\mathsf\{ok\}\(\\langle A,O,q^\{\\prime\},Q^\{\\prime\},t^\{\\prime\}\\rangle,T\)\}\.
A move validates all premises before mutation, advances time, derives sampled crossings, commits the position, updates monitors, and applies immediate rules:

t′≥tΓ⊢g:𝖯𝗈𝗂𝗇𝗍​\[𝑐𝑟𝑠​\(i\)\]Γ⊢⟨X,𝖺𝖽𝗏𝖺𝗇𝖼𝖾​\(t′\)⟩⇓𝗈𝗄​\(X0,Td\)E=𝖼𝗋𝗈𝗌𝗌​\(A0,i,g\)A1=A0​\[i↦g\]Q1=𝖼𝖺𝗇𝖼𝖾𝗅𝖲𝗍𝖺𝗋𝗍​\(q0,Q0,E,t′\)q1=𝖺𝗉𝗉𝗅𝗒𝖱𝗎𝗅𝖾𝗌​\(q0,E\)X1=⟨A1,O0,q1,Q1,t′⟩Γ⊢⟨X,𝗆𝗈𝗏𝖾​\(i,g,t′\)⟩⇓𝗈𝗄​\(X1,Td⋅E\)\.\\frac\{\\begin\{gathered\}t^\{\\prime\}\\geq t\\quad\\Gamma\\vdash g:\\mathsf\{Point\}\[\\mathit\{crs\}\(i\)\]\\\\ \\Gamma\\vdash\\langle X,\\mathsf\{advance\}\(t^\{\\prime\}\)\\rangle\\Downarrow\\mathsf\{ok\}\(X\_\{0\},T\_\{d\}\)\\\\ E=\\mathsf\{cross\}\(A\_\{0\},i,g\)\\quad A\_\{1\}=A\_\{0\}\[i\\mapsto g\]\\quad Q\_\{1\}=\\mathsf\{cancelStart\}\(q\_\{0\},Q\_\{0\},E,t^\{\\prime\}\)\\\\ q\_\{1\}=\\mathsf\{applyRules\}\(q\_\{0\},E\)\\quad X\_\{1\}=\\langle A\_\{1\},O\_\{0\},q\_\{1\},Q\_\{1\},t^\{\\prime\}\\rangle\\end\{gathered\}\}\{\\begin\{gathered\}\\Gamma\\vdash\\langle X,\\mathsf\{move\}\(i,g,t^\{\\prime\}\)\\rangle\\\\\[\-2\.84526pt\] \\Downarrow\\mathsf\{ok\}\(X\_\{1\},T\_\{d\}\{\\cdot\}E\)\\end\{gathered\}\}\.The functional validator𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝖾​\(Γ,X,a\)\\mathsf\{validate\}\(\\Gamma,X,a\)checks the timestamp form, resolved identifier, time monotonicity, then type/CRS compatibility and returns the first error or𝗈𝗄\\mathsf\{ok\}; the single error rule returns𝖾𝗋𝗋𝗈𝗋​\(e,X\)\\mathsf\{error\}\(e,X\)\. Monitor creation requires the attached rule’s source\-state guard to hold inq0q\_\{0\}; emission rechecks the guard before applying its transition\. Scenarios evaluate a finite desugared action sequence over a fresh branch valueXs=𝖼𝗅𝗈𝗇𝖾​\(X\)X\_\{s\}=\\mathsf\{clone\}\(X\)\. The start ist0=max\(X\.t,𝗅𝖺𝗍𝖾𝗌𝗍\(O\),texplicit\)t\_\{0\}=\\max\(X\.t,\\mathsf\{latest\}\(O\),t\_\{\\mathrm\{explicit\}\}\)when an explicit start exists, omitting absent terms\. The clone first advances tot0t\_\{0\}, then applies assumptions there; a declared horizondddesugars to𝖺𝖽𝗏𝖺𝗇𝖼𝖾​\(t0\+d\)\\mathsf\{advance\}\(t\_\{0\}\+d\)\. The calculus treatsXsX\_\{s\}as a fresh value; the Python implementation’s no\-alias copy is checked separately\. Normative validation and scenario questions are read\-only judgmentsΓ⊢X⇓NV\\Gamma\\vdash X\\Downarrow\_\{N\}VandΓ⊢⟨Xs,q¯⟩⇓Qb¯\\Gamma\\vdash\\langle X\_\{s\},\\overline\{q\}\\rangle\\Downarrow\_\{Q\}\\overline\{b\}\.VVis the declaration\-ordered sequence of active constraints whose predicate is false \(a false optional state guard makes a constraint inactive\), whileb¯\\overline\{b\}answers questions in declaration order after assumptions and the horizon advance\. Both judgments leave their input configuration unchanged; the Python implementation executes them, but they are not core mutation actions or part of the current Lean\-checked subset\.

### 4\.1 Core Properties

Lemma 1 \(helper and effect confinement\)\.On well\-formed input,𝖼𝗋𝗈𝗌𝗌\\mathsf\{cross\}traversesRRin declaration order;𝖼𝖺𝗇𝖼𝖾𝗅𝖲𝗍𝖺𝗋𝗍\\mathsf\{cancelStart\}traverses that event sequence andKKin rank order, preserving ground\-key uniqueness and future deadlines;𝖽𝗎𝖾/𝖾𝗆𝗂𝗍\\mathsf\{due\}/\\mathsf\{emit\}use the total key\(𝑑𝑒𝑎𝑑𝑙𝑖𝑛𝑒,ρ​\(k\)\)\(\\mathit\{deadline\},\\rho\(k\)\); and𝖺𝗉𝗉𝗅𝗒𝖱𝗎𝗅𝖾𝗌\\mathsf\{applyRules\}preserves state domains\. Each helper has one finite result, and successful actions mutate only the components in their declaredWW\.

Theorem 1 \(preservation\)\.IfΓ⊢X​𝗈𝗄\\Gamma\\vdash X\\;\\mathsf\{ok\},Γ⊢a:𝖠𝖼𝗍𝗂𝗈𝗇\\Gamma\\vdash a:\\mathsf\{Action\}, andΓ⊢⟨X,a⟩⇓𝗈𝗄​\(X′,T\)\\Gamma\\vdash\\langle X,a\\rangle\\Downarrow\\mathsf\{ok\}\(X^\{\\prime\},T\), thenΓ⊢X′​𝗈𝗄\\Gamma\\vdash X^\{\\prime\}\\;\\mathsf\{ok\}\.*Proof\.*By cases onaa\. Record appends a typed observation\. Advance only removes well\-formed monitors and assigns declared rule targets\. Move validates identifier, time, and CRS before assigning a typed point; new monitors originate inΓ\\Gamma, cancellation only removes entries, and rules assign declared targets\. Unchanged components inherit their invariant\.

Theorem 2 \(determinism\)\.IfΓ⊢⟨X,a⟩⇓u1\\Gamma\\vdash\\langle X,a\\rangle\\Downarrow u\_\{1\}andΓ⊢⟨X,a⟩⇓u2\\Gamma\\vdash\\langle X,a\\rangle\\Downarrow u\_\{2\}, thenu1=u2u\_\{1\}=u\_\{2\}\.*Proof\.*Validation is functional\. In successful cases Lemma 1 fixes each intermediate result, and every order\-sensitive operation has an explicit order\. The error rule retainsXXand returns the unique validation error\.

Theorem 3 \(record confinement\)\.If recordingoomapsXXtoX′X^\{\\prime\}, thenX′\.A=X\.AX^\{\\prime\}\.A=X\.A,X′\.q=X\.qX^\{\\prime\}\.q=X\.q,X′\.Q=X\.QX^\{\\prime\}\.Q=X\.Q, andX′\.t=X\.tX^\{\\prime\}\.t=X\.t\. This is immediate from the recording rule\. Appended evidence can still affect later operations: for example,𝗅𝖺𝗍𝖾𝗌𝗍​\(O\)\\mathsf\{latest\}\(O\)selects a default scenario start\.

Theorem 4 \(extensional scenario isolation\)\.Scenario evaluation leaves every component of sourceXXunchanged because core steps consume and return only the fresh branch value\. Python heap\-alias absence is tested separately at the implementation level\.

Theorem 5 \(finite advance\)\.For finiteQQandt′≥tt^\{\\prime\}\\geq t,𝖺𝖽𝗏𝖺𝗇𝖼𝖾​\(t′\)\\mathsf\{advance\}\(t^\{\\prime\}\)terminates and emits at most\|Q\|\|Q\|sustained events\. The due set is finite; emission removes one distinct keyed monitor per iteration and starts none\.

Theorem 6 \(atomic failure\)\.If evaluation returns𝖾𝗋𝗋𝗈𝗋​\(e,Xe\)\\mathsf\{error\}\(e,X\_\{e\}\), thenXe=XX\_\{e\}=X\. This follows directly from validation before mutation and the error rule\.

Conditional projection adequacy\.Assume a GeoSPARQL processor uses the standard interpretation of CRS84 WKT Point/Polygon literals\. For the supported fragment, strictinsideagrees withsfWithin, and boundary\-inclusivecoveredByagrees withsfIntersects\. The latter mapping is fragment\-specific: it relies on a Point subject and Polygon region\. Section[6](https://arxiv.org/html/2608.02630#S6)tests the condition with an unmodified external engine\. Agreement checks this fragment; formal conformance requires the official test suite\.

## 5 Semantic Views and Prototype

The Python prototype contains an EBNF parser, immutable typed records, semantic compiler, dependency\-free Point/Polygon kernel, role\-aware runtime, temporal event queue, projection layer, and command\-line tools\. Table[3](https://arxiv.org/html/2608.02630#S5.T3)makes the responsibility split explicit\. Execution stays in the typed representation; the views are purpose\-specific and provide partial, role\-dependent fidelity\. Table[3](https://arxiv.org/html/2608.02630#S5.T3)is also a fidelity contract: asserted geometry and observations use selected vocabularies; processes and scenarios have JSON\-only outputs; runtime ordering, queues, and branch identity are not reconstructible\. The implementation supports forward generation only\.

Table 3:Construct coverage, projection fidelity, and responsibility boundary\.The optional projection validator executes generated SHACL with pySHACL and a GEOS adapter for the referenced GeoSPARQL functions\. It compares conformance and violations with internal validation\. This detects cross\-view drift; GeoSPARQL server behavior and conformance remain external\. A separate container pins Apache Jena GeoSPARQL 6\.1\.0\[[20](https://arxiv.org/html/2608.02630#bib.bib20)\]\. Its Java harness imports no PULSE geometry code, loads a projected Turtle graph, evaluates standardsfWithin,sfIntersects,sfDisjoint, andsfTouchesfunctions, and emits SPARQL Results JSON plus separately measured initialization, RDF\-load, and query\-materialization times\. Two separately enabled profile modules fill the GeoSPARQL 1\.1 Geometry surface and an H3 4\.4\.0 DGGS surface; they are measured both apart from and in combination with the unmodified Jena baseline\.

## 6 Evaluation

The evaluation follows the contribution hierarchy\. Its primary questions are whether the contract survives executable and reduced mechanized checks \(RQ1\), whether its spatial projections agree with external engines \(RQ2\), whether traces remain stable on complete modern\-era data \(RQ3\), and whether finite exhaustive temporal traces and single\-change mutants make the operational commitments observable in PULSE and a reference workflow \(RQ4\)\. Scale and persistent\-index checks assess component behavior \(RQ5–RQ6\)\. A durable PostGIS workload is reported only as a secondary feasibility stress test \(RQ7\); modeling ease and end\-to\-end database behavior lie outside its measurements\. Table[4](https://arxiv.org/html/2608.02630#S6.T4)summarizes these deliberately bounded claims\.

Table 4:Executed evidence and deliberately bounded claims\.### 6\.1 Core Contract and Policy Checks \(RQ1\)

The 88 tests exercise role, CRS, state, parser, projection, SHACL, timer, compiler, and multi\-subject contracts, including Listing[1](https://arxiv.org/html/2608.02630#LST1)\. A four\-position finite abstraction enumerates 340 move traces through depth four and exposes pending deadlines; all 3,534 determinism, preservation, finite\-advance, atomicity, and isolation checks pass within this bounded abstraction\.

A Lean 4\.30\.0 development\[[4](https://arxiv.org/html/2608.02630#bib.bib4)\], with nosorry, checks functional kernels for positions, evidence, clocks, monitors, atomicity, and scenarios\. Conditional compiler lemmas preserve guards, triggers, durations, deadlines, horizons, and actions; Lean and Python emit byte\-identical IR for Listing[1](https://arxiv.org/html/2608.02630#LST1)\.

Six namedCoredeclarations cover analogues of Theorems 1–6\. The integrated model checks both rule classes, due\-before\-crossing order, guarded updates, and atomic time/CRS failure, but neither object\-state preservation nor general surface compilation is a Lean theorem\. A 32\-case bridge agrees on final state, pending count, and ordered event fields; declaration order is checked by an alpha\-renaming regression and a two\-symbol Lean prefix\. Geometry, parsing, questions, and general Python refinement remain unmechanized\. Python tests also reject undeclared subjects atomically and clone live scenario state without aliases\.

Six policy\-sensitivity cases each replace one declared contract; every alternative changes state or event trace \(6/6\)\. RQ4 instead mutates one workflow switch at a time\. These results make the commitments observable; policy preference remains unevaluated\.

### 6\.2 External Spatial and Projection Agreement \(RQ2\)

A differential corpus compareswithin,onBoundary, andcoveredBywith GEOS across edges, vertices, concavity, ring orientation, near\-boundary points, thin polygons, large offsets, and four CRS84 translations/scales\. All 89 valid GEOS cases matched; 86 CRS84 cases feed the external\-engine comparison, and nine malformed geometry/CRS cases were rejected\. The adaptive exact\-orientation fallback avoids a fixed coordinate\-unit epsilon\. These are project\-level differential tests, distinct from the official GeoSPARQL suite\.

Generated RDF and SPARQL parse independently, and pySHACL and GEOS agree with internal constraints on four boundary and guard conditions\. Apache Jena then evaluated all 7,396 pairs of the 86 projected points and regions using four Simple Features predicates; every row matched PULSE, including 38 actual point\-on\-shell self\-pairs\. PostGIS returned the same rows without differences\. This triangulation also corrected the projection:ehCoveredBydoes not capture PULSE’s boundary\-inclusive Point/Polygon membership, whereassfIntersectsdoes for this fragment\.

### 6\.3 Secondary GeoSPARQL Profile Probes \(RQ2\)

As secondary interface coverage, a project manifest maps 55 GeoSPARQL 1\.1 Annex A identifiers\[[2](https://arxiv.org/html/2608.02630#bib.bib2)\]to 185 custom probes\. Native Jena passes 112/185; the isolated Geometry and H3 profiles pass 185/185\. A pinned source audit and per\-group purposes are preserved in the artifact\. These custom probes complement rather than execute the OGC abstract tests; conformance remains outside their scope\.

### 6\.4 Real Trajectories and Duration Semantics \(RQ3\)

The frozen NOAA IBTrACS v04r01since1980CSV\[[12](https://arxiv.org/html/2608.02630#bib.bib12)\]contains 307,382 rows \(143 MB\)\. Valid main\-track rows yield 4,775 tracks, 300,033 points, and 295,258 transitions across seven basins; 4,768 tracks have transitions\. A single\-zone replay matched GEOS on every transition, including 571 event\-bearing transitions from 501 tracks\.

Five\-zone replay compared every membership, crossing, and 6/12/24\-hour event with GEOS and an event sweep implemented separately by the first author\. All 1,476,290 pairs matched: 4,800 sampled events and 12,831 emissions from 14,400 monitor starts\. A dateline audit retained all tracks and found 420 normalized longitude jumps in 366 tracks across the Eastern, Southern, and Western Pacific\. After global latitude bands were closed at±180∘\\pm 180^\{\\circ\}, none of their membership changes was seam\-only; 108 changes remained at the deliberately bounded179\.999∘179\.999^\{\\circ\}E edge of the Western\-Pacific study zone\. Reported events therefore use sample\-and\-hold semantics; continuous\-segment and antimeridian\-crossing polygon interpretations remain outside this experiment\.

### 6\.5 End\-to\-End Execution and Composition \(RQ4\)

A 91\-point track exercised all four operational roles: 90 accepted moves produced three sampled events, one six\-hour event, oneSafe→\\rightarrowAtRiskchange, and two guarded violations\. Observation recording and a hypothetical move preserved asserted source state\. The 926 data and 6 shape triples parsed, and pySHACL and GEOS matched internal validation\. This single integration case assesses execution coherence; deployment behavior remains outside its scope\.

A cold\-chain trace was also implemented in PULSE, a workflow composed from GeoSPARQL, SOSA, OWL\-Time, and SHACL, and an OGC MF\-JSONStepworkflow\. All reproduced cancellation, a ten\-minute departure, and final stateAtRisk\. Because the composed paths share reference workflow machinery and adapters, we exclude source\-line and file counts from modeling\-effort and usability claims\.

We then retained the RDF/SHACL inputs but replaced the reference workflow with Sismic 1\.6\.11\[[5](https://arxiv.org/html/2608.02630#bib.bib5)\]\. The statechart, implemented separately by the first author, matched PULSE exactly on final state, all three crossings, cancellation, and the sustained event’s start, effective, and emission timestamps\. Table[5](https://arxiv.org/html/2608.02630#S6.T5)injects one fault at a time\. The six faults were selected to exercise distinct contract sites—identifier binding, effect domain, sample/clock order, scenario isolation, evidence/source role, and monitor start guard\. The unprofiled composition passes static graph validation and needs a complete outcome/source oracle; adding an RDF–statechart binding check, a state invariant, and adapter preconditions moves detection earlier\. All statecharts, workflows, and adapters were implemented by the first author\. The second author independently reviewed and validated every baseline implementation and reported comparison\. The review audits existing implementations; independent reimplementation remains future work\. The case localizes contract sites on one task, leaving authoring cost and generality open\.

Table 5:Detection stage for matched single\-site integration faults\. “Oracle” means comparison with the unchanged complete outcome/source state\.To test temporal obligations without assigning workflow\-code defects to SHACL, we generated every trace of lengths two through five over Boolean membership, increments of 1, 5, 10, or 11 minutes, initial statesSafeorMaintenance, and presence/absence of a same\-trigger immediate transition\. This Cartesian product contains4​∑n=252n​4n−1=37,4404\\sum\_\{n=2\}^\{5\}2^\{n\}4^\{n\-1\}=37\{,\}440traces\. For every trace the PULSE runtime and a reference workflow implemented in separate code by the first author agreed exactly on final state, instantaneous events, start, effective, and emission timestamps for sustained events, and ordering\.

The reference workflow exposes a declared nine\-switch experimental mutation model\. We changed each switch alone and used two directional substitutions for duration scale, producing ten operators: inverse cancellation; timer\-before\-move; start and deadline guards; deadline equality; shorter and longer duration; emission timestamp; transition\-on\-start; and pre\- versus post\-immediate monitor eligibility\. A runtime assertion rejects any operator that changes more than one field or any field without an operator\. All ten mutants were killed; depending on the operator, 1,680–11,024 generated traces distinguished it, and the report stores the first exact witness\. Workflow\-fault detection uses the outcome oracle and excludes RDF or SHACL results\. Exhaustiveness applies to the declared grid; the operator schema remains researcher\-defined\.

The baselines confirm that each composition computes the tested trace\. Their purpose is to identify where the obligations reside: PULSE validates names, types, CRS, operational roles, and runtime effects inside one boundary; the profiled statechart composition recovers all six protections only after binding, state\-invariant, adapter\-order, clone\-isolation, role, and start\-guard checks are added beside its RDF, SHACL, and statechart artifacts\. In this task, unprofiled composition finds 6/6 faults only at the complete outcome/source oracle; PULSE rejects two at compile time and prevents four at its runtime, record, or scenario boundary\. These results characterize contract location and maintenance surface; modeling effort, usability, and language\-level superiority require separate studies\.

### 6\.6 Secondary Engineering Checks \(RQ5–RQ7\)

Artifact\-only checks preserve counts through10510^\{5\}moves, retain 300,033 points and GiST indexes across PostgreSQL/PostGIS container replacement, and reproduce the IBTrACS sweep from stored memberships\. A 50,000\-object read/update/event workload also survives crash/restart; its open\-loop admission boundary is host\-specific\. These checks cover component persistence and host\-specific operation while bypassing parts of PULSE\.

## 7 Discussion and Limitations

Executable OPM, reactive RDF rules, ontology\-driven execution, and isolated KG scenarios predate PULSE; a standards/workflow composition reproduces the tested trace\. PULSE contributes placement, not new computational power: one typed runtime localizes evidence, obligations, hypothetical effects, and timer/state ordering, while acceptance remains external\.

The mutation and statechart executions use the same complete\-loop outcome as PULSE, with workflow faults assessed by the outcome oracle rather than SHACL\. Finite enumeration avoids trace cherry\-picking, while the nine switches and six contract\-site faults remain a researcher\-defined sample\. The first author implemented every executable path; the second author independently reviewed and validated the baseline implementations and reported comparisons\. Agreement plus this audit supports cross\-implementation consistency\. Independent reimplementation of the intended semantics remains future work\.

The four roles form an intentionally non\-exhaustive, requirements\-derived partition\. PULSE covers pre\-acceptance authoritative\-state non\-overwrite and branch isolation; acceptance policy and copy/overlay storage remain external\.

The result boundary is correspondingly narrow\. Geometry covers points and simple polygons under planar predicates and explicit CRS assumptions; holes, multipolygons, transformations, geodesics, uncertainty, continuous crossings, and antimeridian\-crossing polygons remain unsupported\. The custom GeoSPARQL probes measure interface coverage, while official OGC conformance remains untested\. H3 is approximate\. Single\-node PostGIS measurements cover component persistence and load, leaving end\-to\-end throughput, failover, and a portable SLA open\. IBTrACS is retrospective, the contract\-location case uses one track, and authoring\-cost claims await a user study\. Lean starts after parsing and abstracts geometry, floating\-point predicates, constraint validation, and scenario questions\. Its 32\-case bridge also omits specification name, start, and duration, providing case correspondence rather than general Python refinement\. Exhaustive mutation is bounded by its declared grid\.

Future work should independently reimplement the profiles, add interpolation, broaden Python–Lean refinement, test replicated deployments, and preregister a modeling study against composed standards and schema\-first baselines\.

## 8 Conclusion

PULSE contributes a typed executable contract for asserted state, evidence, obligations, counterfactuals, and clocked spatial processes\. Standards/Sismic baselines reproduce the tested protections through explicit cross\-artifact contracts\. On a finite grid, 37,440 exact matches and ten killed mutants expose temporal commitments\. The calculus, Lean subset, IBTrACS replay, and external spatial checks support safety and trace parity for the implemented fragment; persistence and load tests remain secondary component results\.

#### Artifact Availability\.

Grammar, source, tests, data, protocols, Lean files, and reports are in the[PULSE spatial artifact](https://github.com/deeplethe/pulse-spatial), commit798fb7e4e4ef4c04318f0790bae99bc191802e81\.

#### Author Contributions\.

Dongxu Yang conceived PULSE, designed the language and formal semantics, implemented the compiler and runtime, conducted the experiments, and drafted the manuscript\. Ziyi Liang independently reviewed and validated all baseline implementations and reported comparisons\. Both authors accept responsibility for the manuscript\.

#### Declaration of Generative AI Use\.

Generative AI tools were used for language editing, citation and formatting assistance, reviewer\-style critique, and test scaffolding\. Dongxu Yang independently originated the research problem and PULSE’s novel contribution; drafted the manuscript; designed the language, formal semantics, theorem statements, proofs, experimental protocol, and evaluation claims; designed and implemented the prototype, baselines, and experiments; interpreted the results; and verified the assisted material, citations, code, proofs, data, and reported results\. Both authors accept full responsibility for the content\.

## References

- \[1\]D\. F\. Barbieri, D\. Braga, S\. Ceri, E\. D\. Valle, and M\. Grossniklaus\.C\-SPARQL: SPARQL for continuous querying\.InProceedings of the 18th International Conference on World Wide Web, pages 1061–1062\. ACM, 2009\.
- \[2\]N\. J\. Car, T\. Homburg, M\. Perry, F\. Knibbe, S\. J\. D\. Cox, J\. Abhayaratna, M\. Bonduel, P\. J\. Cripps, and K\. Janowicz\.OGC GeoSPARQL – A Geographic Query Language for RDF Data\.OGC Standard 22\-047r1, OGC, 2024\.
- \[3\]S\. Cox and C\. Little\.Time Ontology in OWL\.Candidate recommendation draft, W3C, 2022\.
- \[4\]L\. de Moura and S\. Ullrich\.The lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28, volume 12699 ofLecture Notes in Computer Science, pages 625–635\. Springer, 2021\.
- \[5\]A\. Decan and T\. Mens\.Sismic—A Python Library for Statechart Execution and Testing\.SoftwareX, 12:100590, 2020\.
- \[6\]D\. Dori\.Object\-Process Methodology: A Holistic Systems Paradigm\.Springer, Berlin, Heidelberg, 2002\.
- \[7\]A\. Eibeck, A\. Chadzynski, M\. Q\. Lim, K\. Aditya, L\. Ong, A\. Devanand, G\. Karmakar, S\. Mosbach, R\. Lau, I\. A\. Karimi, E\. Y\. S\. Foo, and M\. Kraft\.A parallel world framework for scenario analysis in knowledge graphs\.Data\-Centric Engineering, 1:e6, 2020\.
- \[8\]A\. Haller, K\. Janowicz, S\. Cox, D\. L\. Phuoc, K\. Taylor, and M\. Lefrançois\.Semantic Sensor Network Ontology\.Recommendation, W3C, 2017\.
- \[9\]D\. Harel\.Statecharts: A visual formalism for complex systems\.Science of Computer Programming, 8\(3\):231–274, 1987\.
- \[10\]International Organization for Standardization\.ISO 19450:2024 Automation Systems and Integration – Object\-Process Methodology, 2024\.Standard ISO 19450:2024\.
- \[11\]S\. Jacobs, N\. Wengrowicz, and D\. Dori\.Exporting object\-process methodology system models to the semantic web\.In2014 IEEE International Conference on Systems, Man, and Cybernetics, pages 1014–1019\. IEEE, 2014\.
- \[12\]K\. R\. Knapp, M\. C\. Kruk, D\. H\. Levinson, H\. J\. Diamond, and C\. J\. Neumann\.The international best track archive for climate stewardship \(IBTrACS\): Unifying tropical cyclone best track data\.Bulletin of the American Meteorological Society, 91\(3\):363–376, 2010\.
- \[13\]H\. Knublauch, D\. Allemang, and S\. Steyskal\.SHACL Advanced Features\.Working group note, W3C, 2017\.
- \[14\]H\. Knublauch and D\. Kontokostas\.Shapes Constraint Language \(SHACL\)\.Recommendation, W3C, 2017\.
- \[15\]T\. Lebo, S\. Sahoo, and D\. McGuinness\.PROV\-O: The PROV Ontology\.Recommendation, W3C, 2013\.
- \[16\]N\. Levi\-Soskin, S\. Marwedel, A\. Jbara, and D\. Dori\.Enhancing conceptual models with computational capabilities: A methodical approach to executable integrative modeling\.Systems Engineering, 27\(4\):759–770, 2024\.
- \[17\]B\. Motik, P\. F\. Patel\-Schneider, and B\. Parsia\.OWL 2 Web Ontology Language: Structural Specification and Functional\-Style Syntax \(Second Edition\)\.Recommendation, W3C, 2012\.
- \[18\]S\. A\. T\. Moxon, H\. Solbrig, N\. L\. Harris, P\. Kalita, M\. A\. Miller, S\. Patil, K\. Schaper, et al\.LinkML: An open data modeling framework\.GigaScience, 15:giaf152, 2026\.
- \[19\]Object Management Group\.OMG Systems Modeling Language \(SysML\), Version 2\.0, Part 1: Language Specification\.Specification formal/2026\-03\-02, Object Management Group, 2026\.
- \[20\]T\. Osman and G\. Albiston\.GeoSPARQL\-Jena: Implementation and Benchmarking of a GeoSPARQL Graphstore\.InProceedings of the 23rd European Conference on Knowledge Management, pages 885–894, 2022\.
- \[21\]G\. Papamarkos, A\. Poulovassilis, and P\. T\. Wood\.RDFTL: An event\-condition\-action language for RDF\.InProceedings of the Third International Workshop on Web Dynamics, volume 703 ofCEUR Workshop Proceedings, pages 62–75, 2004\.
- \[22\]E\. Rietzke, C\. Maletzki, R\. Bergmann, and N\. Kuhn\.Execution of knowledge\-intensive processes by utilizing ontology\-based reasoning\.Journal on Data Semantics, 10\(1–2\):3–18, 2021\.
- \[23\]Y\. Yaroker, V\. Perelman, and D\. Dori\.An OPM conceptual model\-based executable simulation environment: Implementation and evaluation\.Systems Engineering, 16\(4\):381–390, 2013\.
- \[24\]Z\. Zheng, B\. Zhou, D\. Zhou, A\. Soylu, and E\. Kharlamov\.ExeKG: Executable knowledge graph system for user\-friendly data analytics\.InProceedings of the 31st ACM International Conference on Information and Knowledge Management, pages 5064–5068\. ACM, 2022\.