PaperlayerView exact revision on arXiv

Source-linked AI summary

Multi-Aspect Runtime Verification for Simulation-Based V&V of LLM-Enabled Autonomous Agents

Nikolaos Kekatos, Dimitrios Nikou, Anastasios Temperekidis, Alexios Lekidis, Nikolaos Kolokotronis, Panagiotis Katsaros, Stylianos Basagiannis

arXiv:2610.08928v1cs.CRcs.AIcs.LO

TL;DR

Defence staff agents face binding rules of engagement, classification and release policy, targeting law, and medical and humanitarian protections, motivating accountable monitoring at the individual-action interface. The framework decomposes policy clauses into spatial, temporal, and semantic monitors over a shared event stream and composes their verdicts with provenance to shield proposed actions. Full composition closed the evaluated attack suite, while each single aspect left at least 78% of attacks succeeding and the best pair left a third.

  • Problem

    Defence staff agents face binding rules of engagement, classification and release policy, targeting law, and medical and humanitarian protections, motivating accountable monitoring at the individual-action interface.

    Source: §1 · p. 2

  • Method

    The framework decomposes policy clauses into spatial, temporal, and semantic monitors over a shared event stream and composes their verdicts with provenance to shield proposed actions.

    Source: §2 · p. 5, §8 · p. 26

  • Results

    Full composition closed the evaluated attack suite, while each single aspect left at least 78% of attacks succeeding and the best pair left a third.

    Source: §5.1 · p. 18, §8 · p. 26

  • Takeaways & Limitations

    The evaluated obligations require combining aspects, and provenance makes refusals auditable against the policy clause behind them.

    Source: §6 · p. 24, §8 · p. 26

    The mission attacks were designed against the authors’ own properties, with no independent external-corpus replay, and the semantic aspect uses a fixed lexical cue matcher.

    Source: §6 · p. 24

Abstract

from arXiv · show

LLM-based agents are entering decision-support roles in defence staff work, where the obligations they must respect are already written down and binding, and where retraining is not available as a control because models arrive as procured components. What can be placed under engineering control is the interface between the agent and the systems it acts on. Those obligations are at once spatial, temporal and text-semantic, and a violation typically lives in the composition of a multi-step interaction, which is why per-event guardrails miss sequential tool-attack chains. We present a multi-aspect runtime-verification framework that decomposes a natural-language policy clause into a typed spatial/temporal/semantic triple over one canonical event stream, checks each aspect with its own monitoring specification, and fuses the verdicts through a four-valued algebra that carries provenance. The spatial aspect is interpreted over a weighted two-sorted location graph in which mission geometry and information-release topology are one object; we show that these spatial obligations are not in general subsumed by a first-order temporal specification. The past-time aspect runs on the unmodified MonPoly engine, which agrees with our reference monitor at every time point. Across two mission domains, casualty evacuation and contested sustainment, and one civil domain, composition under the precautionary blocking policy drives attack success to zero with no observed false positives and microsecond-scale per-event cost, while every single aspect and every pair leaves a substantial share of attacks succeeding. In a closed-loop experiment a policy-naive planner reaches a violating state in most unshielded missions and in none when shielded, and four refused episodes in five still recover to a compliant outcome.

1 Introduction

The paper addresses how to verify binding, multi-aspect obligations for tool-using LLM agents when retraining is unavailable and control lies at the agent–system interface. It combines aspect-specific monitors over a shared event stream with spatial modeling, provenance-bearing verdicts, and preventive enforcement.

Motivation

  • Procured models and binding obligations shift the controllable verification point to the interface between an agent and the systems it acts on.The obligations include rules of engagement, classification and release policy, targeting law, and protections for medical and humanitarian activity.Source: §1 · p. 2

Assurance problem

  • Violations often emerge only across multi-step interactions, so per-call guardrails cannot detect sequential tool-attack chains.The cited attack chains succeed against frontier models at rates above 90%.Source: §1 · p. 3

Approach

  • The framework decomposes policy clauses into spatial, temporal, and semantic aspects, checks each with a suitable monitor, and composes their verdicts into an auditable decision.The aspects operate over one canonical event stream.Source: §1 · p. 3

Spatial model

  • A weighted two-sorted location graph treats mission geometry and information-release topology as one spatial structure.A reachability query can determine both where an effect may land and where a record may travel.Source: §1 · pp. 3–4

Composition and enforcement

  • A provenance-bearing four-valued composition supports uncertain verdicts, while a shield evaluates proposed calls on a shadow world model and commits only permitted actions.This moves monitoring from reporting violations to preventing them.Source: §1 · pp. 3–4

Evaluation

  • The evaluation tests when composition is required, temporal-monitor agreement, closed-loop mission effectiveness, and assurance failures under incomplete tool surfaces or forged evidence.The paper reuses established monitoring engines and adds the combined spatial model, composition, and preventive shield.Source: §1 · p. 4

2 Operational Scenario and Assurance Problem

The section frames a medical-evacuation agent whose individually admissible actions combine into a policy violation. The scenario motivates requirements for trace memory, heterogeneous evidence, pre-commit evaluation, and auditable refusals.

Operational scenario

  • The modeled evacuation agent supports a medical operations cell under rules for protective marking, cargo, casualty-record sharing, and urgent evacuation.The agents represent near-term roles rather than fielded systems, and the monitoring problem applies wherever multi-step tool use meets multi-aspect obligations.Source: §2 · p. 4

Assurance problem

  • A protected aircraft carrying materiel outside its medical function violates the obligation, and only combining narrative, marking history, and location reveals the violation at the crossing.The monitor refuses the crossing based on objective elements without determining intent or whether the conduct constitutes perfidy.Source: §2 · p. 5

Recurring violation pattern

  • The same trace-level structure appears in escaped casualty records, identifier-bearing summaries, and humanitarian convoys whose loads are later amended.In these cases, no single aspect suffices to detect the violation.Source: §2 · p. 5

Requirements

  • The requirements are trace memory, heterogeneous evidence, stopping a prohibited state before execution, and refusals that identify their obligation and evidence.These requirements address the limits of inspecting calls independently and the operator’s responsibility for accepting or overriding a recommendation.Source: §2 · p. 5

3 Multi-Aspect Runtime Assurance Framework

The framework decomposes policy clauses into spatial, temporal, and semantic monitors over one canonical event stream, then combines their verdicts with provenance. Its spatial model treats mission geometry and information-release topology as one weighted graph, while guarded composition supports pre-action enforcement.

3 Multi-Aspect Runtime Assurance Framework

  • The framework maps each natural-language clause to spatial, temporal, and semantic aspects over one event stream, then fuses their verdicts with provenance.The section presents the event schema, two-sorted graph, expressiveness limits, and composition algebra as its contributions.Source: §3 · p. 5

3.1 Canonical Event Model

  • Canonicalisation places all actions, tool calls, results, and observations on the same trace so aspect verdicts can be fused pointwise.A tool call’s simultaneous facts must remain at one timestamp; splitting them across time points would stretch bounded temporal windows.Source: §3.1 · pp. 5–6

3.2 Two-Sorted Spatial World Model

  • One weighted graph models physical distance and directed information-release paths, allowing reachability to check both standoff and whether records can reach disallowed domains.Physical edges are undirected and measured in kilometres; informational edges are directed and weighted by domain crossings. The informational distance is a quasi-pseudometric, not a metric.Source: §3.2 · pp. 6–7

3.3 Spatial Operators and Reachability Semantics

  • Restricted-path reachability distinguishes a genuinely accessible destination from one that is merely nearby or present in the topology.Masking can exclude a shorter physical path, while a disallowed enclave matters only if an opened channel makes it reachable.Source: §3.2 · p. 7, §3.3 · p. 8

3.4 Aspect-Specific Obligations

  • The obligations combine spatial reachability, casualty- and partner-specific authority and timing, and semantic typing and laundering checks.T1 authority for one casualty and partner does not discharge another’s obligation; T2 includes a golden-hour deadline, and semantic typing supplies the protected object the other aspects quantify over.Source: §3.4 · pp. 9–10

3.5 Expressiveness Limits and Motivation for Decomposition

  • Spatial containment is not uniformly expressible in first-order temporal logic over unbounded graphs, especially when runtime channel changes alter topology.A known bounded graph can be unrolled, but a fixed encoding must be regenerated when the traversable graph changes; the claim does not establish that exactly three aspects are necessary or that a sufficiently engineered single engine is impossible.Source: §3.5 · pp. 10–11

3.6 Guarded Four-Valued Composition and Provenance

  • Four-valued verdicts distinguish heuristic judgements through provenance, while guards arm clauses without creating refusals when their conditions are false.The design does not currently express liveness obligations; adding them would reintroduce trace-extension uncertainty and require separate truth and confidence statuses.Source: §3.6 · pp. 11–12

3.7 Model Independence, Applicability and Trust Assumptions

  • The assurance claim is bounded by the trusted interface: it excludes actions that bypass it, unobserved world-state changes, and unattributable obligation-discharging events.Enforcement completeness depends on the tool surface and evidence attribution, not only on the clause set.Source: §3.7 · p. 13

4 Simulation-Based V&V Methodology

The methodology places a canonical event stream and three aspect monitors between planner and executor, then composes their verdicts to enforce policy preventively. Its simulation design evaluates this arrangement across three domains while distinguishing the executed temporal engine from reference implementations.

4 Simulation-Based V&V Methodology

  • The framework combines a canonicaliser, three aspect monitors, a composer and a shield on the planner-to-executor path.The past-time monitor runs first only to arm the other two; spatial and temporal monitoring are then independent.Source: §4 · pp. 13–14, Figure 2 · p. 14
  • φS reduces spatial clauses to predicate-restricted shortest-path queries, φT checks past-time obligations, and φΣ combines marking lookup with narrative-content cues.The cue matcher is fixed and uncalibrated: a hit is presumptive, not a quantified-error verdict, and cannot alone produce definite refusal.Source: §4 · pp. 13–14
  • The shield blocks calls according to a configurable blocking set and commits an action only after shadow evaluation permits it.Under precautionary blocking, presumptive violations are refused; a refused call never mutates mission state.Source: §4 · p. 15

4.1 System Under Test and V&V Architecture

  • Simulation runs use canonical events and a world-model state, randomise obligation-relevant factors across 400 runs per domain, and measure violations, false refusals, cost and evidence.The same specification can run with a scripted or live planner; shadow-copy evaluation supplies a counterfactual before commitment.Source: §4.1 · pp. 15–16

4.2 Domain Instantiations and Implementation Status

  • The three instantiations cover MEDEVAC, contested logistics and civil GDPR; φT runs on unmodified MonPoly, while φS and φΣ are reference implementations.The logistics domain retains the framework and clause structures while adding domain vocabulary and mappings.Source: §4.2 · pp. 16–17

4.3 Research Questions and Evaluation Strategy

  • The evaluation asks whether composition prevents violations missed by partial monitoring, whether implementation is correct and efficient, whether shielded missions remain compliant, and whether enforcement can be bypassed.The first question also considers false refusals on benign traffic.Source: §4.3 · p. 17

5 Experimental Results

Across the evaluated mission settings, full multi-aspect composition prevents attacks that individual aspects and pairs miss. The experiments also test monitor agreement and cost, closed-loop mission outcomes, and whether the enforcement surface itself can be bypassed.

5.1 Multi-Aspect Effectiveness and Robustness

  • In both designed mission suites, full composition blocks all nine attacks without refusing a benign trace, while every proper subset leaves attacks succeeding.The two suites have nine attacks and nine benign traces each; their agreement reflects structurally matched attack families, not independent corroboration.Source: §5.1 · p. 17, Table 1 · p. 18
  • Each single aspect leaves at least 78% of attacks succeeding, the best pair leaves a third, and 33% of refusals draw evidence from multiple aspects.The M7 refusal jointly relies on the past-time obligation and semantic reading of the load manifest.Source: §5.1 · p. 18
  • At n = 400 per domain across seven families, full composition yields miss rate 0.0% [0, 1.8%] and false positives 0.0% [0, 2.0%].Every family separates cleanly, and the MEDEVAC and logistics generators agree to the sample.Source: §5.1 · p. 19

5.2 Monitor Validation and Runtime Cost

  • MonPoly fires at exactly the six MEDEVAC time points flagged by the reference monitor, while DejaVu misses only the golden-hour breach outside its untimed fragment.The contested-logistics suite reproduces the MonPoly clause-by-clause agreement; metric windows require a timed-capable engine.Source: §5.2 · p. 20
  • Full-composition monitoring averages 5.2 µs per MEDEVAC event and 5.3 µs per contested-logistics event; the civil suite averages 2.0 µs.Geometry or record-placement calls incur a predicate-restricted shortest-path computation; model inference and network time are excluded.Source: §5.2 · p. 21

5.3 Closed-Loop Agent Evaluation

  • The local language-model planner reaches the prohibited state in 6 of 12 injected unshielded episodes and in none of the shielded episodes.The sample is small and uses a 3B local model; refusals also impose utility costs on benign episodes.Source: Language-model planner under… · pp. 21–22
  • Across episodes, shielding reduced violations from 77.0% [72.6, 80.9] unshielded to 0.0% [0.0, 1.0] shielded, while delivery fell from 100% to 85.0% [81.2, 88.2].Of 308 episodes containing a refusal, 80.5% [75.7, 84.6] recovered to compliant delivery; 60 were abandoned because no compliant facility was reachable. Enforcement cost a median of two extra tool calls and one extra planning round.Source: Language-model planner under… · p. 22

5.4 Enforcement-Surface Robustness

  • Record creation, replication, and summary derivation bypassed spatial checking, while the agent could self-grant authority to discharge obligations.These findings bound assurance to covered tool paths and attributable obligation-discharging events; external-corpus replay and richer stateful baselines remain outside scope.Source: §5.4 · pp. 23–24

6 Discussion and Threats to Validity

The evaluated composition closes the attack suite where no proper subset does, and the temporal monitor agrees with MonPoly. The evidence is bounded by designed suites, limited external coverage, and a small single-model closed-loop test.

Discussion

  • The full composition closes the evaluated obligation suites where no proper subset does, while temporal monitoring agrees with MonPoly and per-event cost remains in the microsecond range.In closed loop, the shield keeps the planner out of violating states while most refused episodes recover to compliant outcomes.Source: §6 · p. 24

Deployment and applicability

  • Two enforcement defects—unmediated equivalent action paths and forged authority—show that sound deployment depends on complete mediation and trustworthy attribution of discharging authority.The paper states that the specification may be correct while deployment remains unsound if another tool reaches the same effect or the bound party can issue the discharging authority.Source: §6 · p. 24

Threats to validity

  • Designed suites sample seven anticipated attack families, so generated-suite robustness does not establish coverage of an unknown attack distribution.The designed suites are small, and the logistics traces are structural twins of the MEDEVAC traces; the two domains are not pooled.Source: §6 · p. 24
  • The evaluation lacks independent external-corpus replay, and its fixed lexical cue matcher can be defeated by paraphrases around the cues.The mission attacks were designed against the paper’s own properties, and comparison was with a reimplemented AgentSpec-style control rather than published Progent or GuardAgent implementations.Source: §6 · p. 24
  • The closed-loop test uses one small model and twelve episodes per condition, demonstrating operation on generated behavior rather than robustness across models.Golden-hour, standoff-distance, corridor-width, and freshness settings are configurable policy parameters, not validated doctrinal values.Source: §6 · p. 25

7 Related Work

Prior agent controls generally inspect individual calls or messages, while established runtime-verification engines target separate aspects or distribute monitoring across tiers. This work instead composes multiple aspects at one enforcement point and treats release topology as part of spatial monitoring.

Agent safety and guardrails

  • Per-event controls such as AgentSpec, Progent [25], GuardAgent [30], and LlamaGuard [12] inspect calls or messages in isolation, while the properties here concern multi-step traces.The STAC line [20] demonstrates the insufficiency of per-event controls; AgentDojo and SafeAgentBench [31] provide benchmarks.Source: §7 · p. 25

Runtime verification engines

  • Established engines cover stream monitoring, first-order past-time monitoring, or MFOTL, whereas this work contributes decomposition, a shared canonical stream, and a verdict-fusing algebra.MonPoly is used unmodified for the temporal aspect; the other mappings identify intended formalisms and capability boundaries.Source: §7 · p. 25

Spatial and spatio-temporal specification

  • Unlike prior spatial logics built around physical space, the location graph combines mission geometry with release topology weighted by domain crossings.This lets one monitor address obligations otherwise split between geofencing and data-loss prevention.Source: §7 · p. 25

Assurance and accountability

  • Clause-grounded, provenance-carrying verdicts support traceability obligations, and refusals naming the checked aspects and clause are auditable beyond a classifier score.The passage connects this to Article 12 of the EU AI Act and ISO/IEC 42001.Source: §7 · p. 26

Relation to our own work

  • This paper is single-agent and composes aspects; cross-agent aggregation, messaging fabric, and swarm properties belong to a separate companion submission.The two works share no scenario, property, measurement, or artefact.Source: §7 · p. 26

8 Conclusion

The paper concludes that full multi-aspect composition is the only tested configuration to close the evaluated attack suite, with closed-loop shielding reducing violations while many refusals still recover. It identifies external validation and richer guard semantics as future work.

8 Conclusion

  • Across the evaluated domains, no single aspect or pair closes the attack suite, while precautionary composition does so with no observed false positives and microsecond-scale overhead.Closed-loop violations fall from 77% to zero, and 80.5% of refused episodes recover to compliant delivery.Source: §8 · p. 26

Future work

  • Future evaluation should integrate external engines into the closed-loop harness, test optimized attackers, and generate scenarios from independently specified mission models.The current evaluation uses seven families of the authors’ own design.Source: §8 · p. 26
  • A formal open question is how to extend guarded composition beyond Boolean arming to uncertain and nested guards with formal guard provenance.The protected-status pattern suggests richer operators than the guarded maximum used here.Source: §8 · p. 27
Loading 2610.08928v1…