arXiv:2608.02630cs.AIcs.DB2026-08

PULSE让时空知识图谱的规则执行变得可编程且安全可控。

PULSE: An Executable Contract Language for Spatiotemporal Knowledge Graph Engineering

  • 用统一语言封装四种操作角色及其写入效果,实现运行时局部化控制
  • 在37,440条时间轨迹中与外部工作流一致,12,831个事件经时长验证
  • 适合需严格状态约束的时空系统建模,如气象追踪、供应链监控

知识图谱工程常将状态、观测、约束、流程和假设分散于多个文档,其联合执行逻辑难以显式表达。本文提出PULSE,一种受对象-过程方法论启发的语言,将四种操作角色及其写入效应统一于一个类型化的运行时环境中。其中“模式”表示操作角色,而非模态或道义逻辑。该语言实现证据不覆盖、分支隔离、多主体定时器、受控状态变更、按声明顺序排序事件等特性;外部运行器仍决定证据是否成为权威动作。GeoSPARQL、SOSA和SHACL仍作为生成视图存在。核心演算提供效应封闭引理及六项安全性质。使用Lean 4验证了位置、证据、时钟、监视器、原子性及分支源保留的内核等价性;通过88个测试、3,534次有限检查及32个Lean/Python运行时-内核案例,将实现范围限定在可验证范围内。第一作者实现了标准组合与独立的Sismic状态机,复现了测试中的冷链追踪路径。在37,440条生成的时间轨迹中,PULSE与另一工作流一致,并区分了十个单字段变异体。在1980年以来的完整NOAA IBTrACS子集上,其结果与GEOS及事件扫描在1,476,290个过渡区对中一致,涵盖4,800个采样事件与12,831个时长合格事件。项目特定的GeoSPARQL探针用于测量接口覆盖率。总体结果支持合约局部化、安全论证及测试片段的轨迹一致性;语言优越性与可用性不在评估范围内。

原文摘要 · Abstract (English)

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 IBTrACS since1980 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.

知识图谱时空建模形式化验证领域语言

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。