Are Agents Probabilistic Automata? A Trace-Based, Memory-Constrained Theory of Agentic AI

TL;DR

This paper develops an automata-theoretic framework for modeling agentic AI with explicit memory and stochastic policies, enabling probabilistic verification of their interaction behaviors and safety properties.

Contribution

It introduces a trace-based, probabilistic model of agent-environment interactions that captures memory constraints and stochastic policies, extending automata theory for AI verification.

Findings

Support for trace languages is regular with bounded memory.

Support is context-free with strict call-return control.

Support is recursively enumerable with unbounded memory.

Abstract

This paper studies standard controller architectures for agentic AI and derives automata-theoretic models of their interaction behavior via trace semantics and abstraction. We model an agent implementation as a finite control program augmented with explicit memory primitives (bounded buffers, a call stack, or read/write external memory) and a stochastic policy component (e.g., an LLM) that selects among architecturally permitted actions. Instead of equating the concrete agent with a deterministic acceptor, we treat the agent-environment closed loop as inducing a probability distribution over finite interaction traces. Given an abstraction function $\Abs$ from concrete configurations to a finite abstract state space, we obtain a probabilistic trace language and an abstract probabilistic transition model $M_{\Abs}$ suitable for probabilistic model checking. Imposing explicit, framework-auditable restrictions on memory access and control flow, we prove that the support of the resulting trace language is regular for bounded-memory controllers, context-free for strict call-return controllers, and recursively enumerable for controllers equipped with unbounded read/write memory. These correspondences allow the reuse of existing verification methods for finite-state and pushdown systems, and they delineate precisely when undecidability barriers arise. The probabilistic semantics leads to quantitative analyses such as: what is the probability of entering an unsafe abstract region, and how can we bound this probability in the presence of environment nondeterminism.