Skip to content
Preprint

PULSE: An Executable Contract Language for Spatiotemporal Knowledge Graph Engineering

Jul 2026 · 0 citations · 24 references
Computer Science

TL;DR

This work presents 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.

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

View source

Similar papers

Preprint Jul 2026

TGMS: An Agent-Native Bi-Temporal Graph Management System

TGMS is a bi-temporal property graph management system that exposes thirteen verified temporal operators as agent tools that can answer belief-state questions such as ``as of transaction time $T$, what did the system believe?''

Xiaofei Zhang · 0 citations
Jul 2026

StructureClaw: Traceable LLM Agents and an Executable Benchmark for Structural Engineering Workflows

This work presents StructureClaw, an artifact-centered workbench in which LLM agents operate through governed engineering skills, typed tools, shared artifact state, and local analysis backends, together with StructureClaw-Bench, an executable benchmark of 150 controlled scenarios spanning standard workflows, interacti...

Sizhong Qin, Yi Gu, Yao Jiang et al. · 0 citations
Jul 2026

FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs

This work presents FAVA (Formal Authorization for Verified Agents), a permission-carrying authorization framework for agent execution that utilizes an LLM-guided Permission Intermediate Representation to translate ambiguous natural-language tasks into structured constraints.

Yifan Zhang, Xin-Kui Zhao, Sai-Da Liu et al. · 3 citations
Book Open access Aug 2026

IntentP4: Bridging P4 Temporal Specifications and Executable Network Tests

IntentP4 is presented, a formal-methods-aided pipeline that translates an operator's natural-language intent into a P4LTL specification and then into a replayable multi-packet test case, grounded throughout in compiler artifacts via a tool-queryable ProgramContext and gated by deterministic per-stage validators.

Ruonan Feng, Mingming Zhang, Yu Jiang et al. · 0 citations
Preprint Aug 2026

Metis: Typed Runtime Mediation for Tool-Using Software Agents

Metis, a multi-provider runtime that converts provider streams into typed events before admitted calls reach external effects is presented, a multi-provider runtime that converts provider streams into typed events before admitted calls reach external effects.

Jun'an Yu · 0 citations
Preprint Jul 2026

ContainmentBench: Trace-Based Evaluation of Post-Exposure Containment in Tool-Using LLM Agents

ContainmentBench, a sandboxed benchmark comprising a 504-scenario specification dataset, a shared rollout-trace schema, and stage-scoped metrics for endpoint violations, logged propagation, and explicitly authorized taint-exposed proposals that commit, is introduced.

Wen-Hao Lan, Shan Li, Meiqi Wu et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.