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
Preprint 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, interactive robustness, and multimodal structural-model reconstruction.

Sizhong Qin, Yi Gu, Yao Jiang et al. · 0 citations
Preprint 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, Xinkui 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

Software agents connect probabilistic model output to operations that change repositories, processes, networks, and graphical applications. We present Metis, a multi-provider runtime that converts provider streams into typed events before admitted calls reach external effects. Its execution path makes permission decisions, interference classes, terminal results, and lifecycle transitions explicit and inspectable. We evaluate these mechanisms on frozen source artifacts. Across 30 matched real-I/O pairs, four-class mediation reduced median elapsed time from 25.958 ms under forced serialization to 14.146 ms. The mean paired difference was -12.295 ms (95% bootstrap interval [-12.968, -11.694]), with mediation faster in all pairs. A ten-case fault matrix exposed duplicate-identifier and rollback limits. In a child-boundary ablation, the full gate-plus-registry condition blocked the declared unauthorized effect and hid all five escape tools. Removing both protections reversed both observations. A decision-only permission oracle matched all ten declared cases across five invocation routes. Five model conditions also completed a fixed Read-marker protocol in 3/3 trials each. These results support bounded claims about dispatch, permission routing, child authority, and provider-valid trace closure. They do not establish model competence, semantic safety, rollback, or superiority over another runtime.

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.

Wenhao Lan, Shan Li, Meiqi Wu et al. · 0 citations