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

arXiv: https://arxiv.org/abs/2510.23487 · HTML: https://mlsanity.com/paper/2510.23487/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use.
- Builds on 4 of its 23 references that are in the map.
- First posted on arXiv 27 Oct 2025.

## Placed in

- LLM agents and tool use / [General LLM agent frameworks and benchmarks](https://mlsanity.com/agents/general-llm-agent-frameworks-and-benchmarks/)

## Builds on (most cited first, 4 of 4)

- [AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation](https://mlsanity.com/paper/2308.08155/) (2023)
- [Auto-GPT for Online Decision Making: Benchmarks and Additional Opinions](https://mlsanity.com/paper/2306.02224/) (2023)
- [Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents](https://mlsanity.com/paper/2402.00798/) (2024)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)

## Built on by (most cited first, 1 of 1)

- [Enforcing Benign Trajectories: A Behavioral Firewall for Structured-Workflow AI Agents](https://mlsanity.com/paper/2604.26274/) (2026)

## Abstract (arXiv)

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