Certified Execution Harness for Agentic AI: Safe and Least-Intrusive Petri-Net Supervisory Control Between Reasoning and Action

Chao Gu; Quanyan Zhu

cs.AIOct 22, 2026

Certified Execution Harness for Agentic AI: Safe and Least-Intrusive Petri-Net Supervisory Control Between Reasoning and Action

Authors: Chao Gu, Quanyan Zhu

Organizations: C. Gu is with the School of Electronics, Electrical Engineering and Computer Science, Queen’s University Belfast, Belfast, UK · Q. Zhu is with the Department of Electrical and Computer Engineering, New York University, Brooklyn, NY 11201, USA

Abstract

This paper studies the problem of safe tool execution for large language model (LLM) agents under prompt injection. Using Petri nets, we formalize the execution harness between the LLM and its tools as a supervisory control problem, in which marks represent capabilities, approvals and budgets. Since a transition fires only if the marks it needs are present, an injected request whose preconditions are unmet or already spent is refused regardless of its wording. Treating tool outcomes as uncontrollable, we enforce safety by the conventional maximally permissive supervisor, and this safety transfers to the running system under four assumptions. Moreover, to capture an agent that may propose again after a refusal, we introduce the notion of a replanning closed loop, in which each retry costs an inference call. We show that, in this loop, the conventional supervisor can be arbitrarily more intrusive than a stricter safe one. Furthermore, for a given proposer model, the maximally permissive least-intrusive supervisor is characterized as a value-threshold refinement of the conventional one. Under precise conditions, this refinement orders two concurrent actions by at most one monitor place. On an autonomous release agent, we find by synthesis that safe deployment requires a step that the supervisor can refuse after a rollout starts.

Figures & tables

Fig. 1: The execution harness between the untrusted LLM and its tools. The LLM proposes a tool call

u_{k}

, which is executed (green path) if and only if checks i)–iv) of the admission rule Eq. ( 1 ) pass. Otherwise, the LLM may propose again at the cost of an inference call. Admitted firings and uncontrollable firings (of transitions in

T_{u}

) update the marking

M_{k}

, i.e., the operational state. Assumption A4(a) in Section IV-D excludes the bypass (red dashed arrow), in which the untrusted LLM acts on the environment directly and skips the admission rule.

Fig. 2: One step of the execution harness. Green squares 1–7 number the steps of one proposal, and i)–iv) are the checks of Eq. ( 1 ). Step 6 executes the call and fires

t_{k}

, i.e., applies the update drawn in the kernel box, and step 7 returns the outcome to the kernel and to the context. In this and the later figures, black and white bars are controllable (

T_{c}

) and uncontrollable (

T_{u}

) transitions. In the supervisor box (step 5), the gray region is the closed-loop reachable set

R(S/\mathcal{N},M_{0})\subseteq\mathcal{Q}

. The context window holds the history

H_{k}

Panel of Figure 3 — Fig. 3: (a) $t_{\mathrm{exec}}$ consumes the mark that $t_{\mathrm{approve}}$ produced, so each approval authorizes one execution. (b) A self-loop (double-headed arc) only tests $p_{\mathrm{approved}}$ and returns the mark, so one approval authorizes any number of executions. In (a), $p_{\mathrm{approved}}$ is a monitor place, but in (b) it is not, since it does not limit the number of executions.

Fig. 4: Seven components of an agent harness and their relations. The execution harness holds only their AEPN counterparts, while the tools themselves and the stored text lie outside it.

Panel of Figure 5 — Fig. 5: The net of Example 1 , where all transitions are controllable.

Panel of Figure 6 — Fig. 6: A fork structure at $M_{\emptyset}$ , with the monitor place $p_{c}$ dashed (left), and its corresponding markings (right), where $M_{A}$ , $A\subseteq\{1,2\}$ , records which branches have fired. The refinement $S_{J_{\min}}$ removes the edge $t_{1}$ at $M_{\emptyset}$ , marked by a red cross, when Eq. ( 11 ) holds, e.g., if premature requests are likely enough at $M_{\{1\}}$ but not at $M_{\{2\}}$ . The monitor place $p_{c}$ implements this removal.

Fig. 7: The release net, where

p_{\mathrm{nf}}

(no freeze) and

p_{\mathrm{fr}}

(frozen) hold one mark between them, moved by

t_{\mathrm{incident}}

and

t_{\mathrm{thaw}}

. The firing of

t_{\mathrm{publish\_fr}}

marks

p_{\mathrm{bad}}

and thus reaches a marking in

\mathcal{B}

, while the recovery actuator

t_{\mathrm{abort}}

marks

p_{\mathrm{aborted}}

. The white bars are the transitions treated as uncontrollable in the least-intrusive analysis. Table I treats some of them as controllable.

Configuration	$\|\mathcal{Q}\|$	$\|K^{\star}\|$	$\|K^{\uparrow}\|$	Reach	Deployed?
one-phase, optimistic $T_{u}$	27	26	22	20	no
$+\ t_{\mathrm{abort}}$	28	27	25	20	no
$+\ t_{\mathrm{abort}}+t_{\mathrm{thaw}}$	30	28	28	28	yes
the same, honest $T_{u}$	30	26	24	20	no
two-phase, honest $T_{u}$	32	30	30	30	yes

TABLE I: Synthesis on the release net. The column “Reach” counts the markings that the closed loop of

S_{K^{\uparrow}}

reaches from

M_{0}

, while “Deployed?” indicates whether one of them has

p_{\mathrm{live}}

marked.

Premature requests	$J_{S_{K^{\uparrow}}}-\bar{J}$	$J_{\min}-\bar{J}$	$\Delta J$	$S_{J_{\min}}$ removes
none	0	0	0	none
after tests, $h{=}0.9$	$75/17$	$20/17$	$55/17$	$t_{\mathrm{ci}}$
after tests, $h{=}0.98$	$415/17$	$20/17$	$395/17$	$t_{\mathrm{ci}}$
after either, $h{=}0.9$	$150/17$	$150/17$	0	none

TABLE II: Extra expected cost from

M_{0}

caused by premature requests, relative to the cost

\bar{J}

without them. Here,

\Delta J:=J_{S_{K^{\uparrow}}}-J_{\min}

. The entries are exact expected refusals and are the same for every

c_{a}

Panel of Figure 10 — Fig. 8: Sequencing the fork of the release net. The supervisor $S_{J_{\min}}$ refuses $t_{\mathrm{ci}}$ before the scan if and only if the solid curve lies above the dashed line, i.e., $h>h^{\ast}=43/60$ . The thick curve $J_{\min}-\bar{J}$ is the smaller of the two, and the shaded gap is $\Delta J$ in Eq. ( 12 ). Filled and open dots are the values of $J_{S_{K^{\uparrow}}}-\bar{J}$ and $J_{\min}-\bar{J}$ , respectively, in the “after tests” rows of Table II .

Fig. 9: Injection probability

q_{\mathrm{inj}}

swept from

0

0.5

on the release net under a scripted proposer, with

10^{4}

episodes per point. The left panel shows the fraction of episodes with an unauthorized deployment, i.e., a

t_{\mathrm{start}}

executed without an approval, injected or not. The right panel shows the fraction of episodes that complete the task. The classifier curves use the false-negative rates

f_{n}=0.10

and

f_{n}=0.30

Tool Access Control for LLM Agents

Tool access control for LLM agents limits which tools, resources, and actions agents may use, and under what conditions.

See all 221 papers

Tool Specifications Matter: Uncovering and Mitigating Safety Risks in AI Agents
Jul 31, 2026Minghui Pan, Jiayuxuan Yang, Yuanyuan Yuan +2LLM Guardrails Prompt Injection Attacks on AI Agents
Beijing University of Posts and Telecommunications · Beihang University · Tsinghua University
AgentBoundary: Counterfactual Evaluation of Safety in Tool-Using LLM Agents
Sep 27, 2026Tianzhuo Yang, Zirui Mi, Yantao Huang +4LLM Agent Evaluation LLM Agents
Peking University · Beijing Academy of Artificial Intelligence
Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement
Jun 22, 2026Pierre Dantas, Lucas Cordeiro, Ehsan Nowroozi +1LLM Agent Safety LLM Agent Reliability
The University of Manchester, Manchester, UK · The University of Greenwich, London, UK · Technology Innovation Institute, Abu Dhabi, UAE

Jul 31, 2026J/K move · Enter open · S save

Tool Specifications Matter: Uncovering and Mitigating Safety Risks in AI Agents

Minghui Pan, Jiayuxuan Yang, Yuanyuan Yuan, Yu Jiang+1

Beijing University of Posts and Telecommunications · Beihang University · Tsinghua University

LLM Guardrails Prompt Injection Attacks on AI Agents LLM Agent Safety

Open paper AskPDF arXiv

AI agents extend large language models (LLMs) with external tools, enabling them to perform complex tasks and translate model outputs into consequential real-world actions. Yet LLMs often become substantially less safe when deployed as agents, and the source of this degradation remains poorly understood. In this paper, we identify schema-formatted tool specifications as a primary source of agent safety degradation and show, through white-box representation analysis, that they weaken the model's internal refusal signals and contribute to unsafe tool execution. Building on this finding, we propose SafeKeep, an inference-time safeguard that decouples safety judgment from tool execution: it assesses requests using flattened textual tool specifications while retaining the original schema-formatted specifications for execution. Across two representative benchmarks and four LLMs, including both white-box and black-box models, SafeKeep increases the average refusal rate for harmful requests from 23.8% to 70.6% and reduces the average attack success rate under observation-level prompt injection from 25.6% to 2.5%. It also outperforms existing safeguards and preserves task-handling capability. We release the code and data at https://github.com/snowcatsmoking/SafeKeep .

Abstract

Tool Access Control for LLM Agents

Explore similar work

Tool Specifications Matter: Uncovering and Mitigating Safety Risks in AI Agents

AgentBoundary: Counterfactual Evaluation of Safety in Tool-Using LLM Agents

Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement