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.

翻译：本文研究智能体AI的标准控制器架构，通过轨迹语义与抽象推导其交互行为的自动机理论模型。我们将智能体实现建模为增强显式内存原语（有界缓冲区、调用栈或读写外部内存）的有限控制程序，以及一个在架构允许动作中进行选择的随机策略组件（例如大型语言模型）。不同于将具体智能体等同于确定性接受器，我们将智能体-环境闭环视为在有限交互轨迹上诱导出概率分布。给定从具体配置到有限抽象状态空间的抽象函数$\Abs$，我们得到适用于概率模型检测的概率轨迹语言与抽象概率转移模型$M_{\Abs}$。通过对内存访问与控制流施加显式且可审计的框架限制，我们证明：对于有界内存控制器，所得轨迹语言的支撑集是正则的；对于严格调用-返回控制器是上下文无关的；对于配备无界读写内存的控制器是递归可枚举的。这些对应关系使得现有有限状态系统与下推系统的验证方法得以复用，并精确界定了不可判定性障碍出现的条件。概率语义支持定量分析，例如：进入不安全抽象区域的概率是多少？在环境非确定性存在时如何界定该概率？