PULSE: An Executable Contract Language for Spatiotemporal Knowledge Graph Engineering

PULSE：一种用于时空知识图谱工程的可执行契约语言

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.

摘要： 知识图谱工程通常将已接受的状态、观测值、约束、流程和假设场景分散在不同的工件中，而这些工件组合后的执行契约往往处于外部。我们提出了 PULSE，这是一种受对象-过程-方法论（Object-Process-Methodology）启发的语言，它将四种操作角色及其写入效应本地化在一个类型化的运行时中。在此，模式（modes）指的是操作角色，而非模态逻辑或道义逻辑。

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.

该实现的契约固定了证据不可覆盖性、分支隔离、基于基础的多主体计时器、受保护的状态变更，以及时空上的声明排序事件顺序；外部运行器仍决定证据是否成为权威动作。GeoSPARQL、SOSA 和 SHACL 仍然作为生成的视图存在。核心演算提供了一个效应限制引理和六个安全属性。

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.

Lean 4 对位置、证据、时钟、监视器、原子性和分支源保留进行了内核模拟检查；88 个测试、3,534 个有界检查以及 32 个 Lean/Python 运行时内核案例将实现声明限制在已检查的案例范围内。第一作者对标准组合和独立的 Sismic 状态图的实现，重现了经过测试的冷链追踪记录。

Across 37,440 generated temporal traces, PULSE matches a separate workflow and distinguishes ten single-field mutants. On the complete NOAA IBTrACS since 1980 subset 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.

在 37,440 条生成的时序追踪中，PULSE 与独立工作流相匹配，并能区分十种单字段变体。在 1980 年以来的完整 NOAA IBTrACS 子集上，它与 GEOS 以及对 1,476,290 个过渡区对（包括 4,800 个采样事件和 12,831 个持续时间限定事件）的事件扫描结果一致。项目特定的 GeoSPARQL 探针用于测量接口覆盖率。总体而言，结果支持了所测试片段的契约本地化、安全论证和追踪一致性；语言的优越性和可用性未包含在本次评估范围内。