TriCEGAR: A Trace-Driven Abstraction Mechanism for Agentic AI
Roham Koohestani, Ateş Görpelioğlu, Egor Klimov, Burcu Kulahcioglu Ozkan, Maliheh Izadi
TL;DR
TriCEGAR tackles the challenge of assuring agentic AI by automating state abstraction from execution traces and enabling online learning of an Agentic MDP (AMDP) for probabilistic model checking. It learns a predicate-tree abstraction from logs, constructs an AMDP over abstract states, and uses probabilistic model checking to compute bounds such as $P_{\max}$ and $P_{\min}$ for mission-critical properties, while also providing run-likelihood based anomaly detection. The approach combines three linked structures (predicate tree, trace prefix trie, and AMDP) to support live refinement via counterexamples, reducing reliance on manual state engineering. The prototype demonstrates end-to-end support for trace capture, abstraction, MDP induction, PMC, and anomaly signaling, and outlines a plan for probabilistic CEGAR refinements and dynamic property translation to broaden applicability in enterprise agent frameworks.
Abstract
Agentic AI systems act through tools and evolve their behavior over long, stochastic interaction traces. This setting complicates assurance, because behavior depends on nondeterministic environments and probabilistic model outputs. Prior work introduced runtime verification for agentic AI via Dynamic Probabilistic Assurance (DPA), learning an MDP online and model checking quantitative properties. A key limitation is that developers must manually define the state abstraction, which couples verification to application-specific heuristics and increases adoption friction. This paper proposes TriCEGAR, a trace-driven abstraction mechanism that automates state construction from execution logs and supports online construction of an agent behavioral MDP. TriCEGAR represents abstractions as predicate trees learned from traces and refined using counterexamples. We describe a framework-native implementation that (i) captures typed agent lifecycle events, (ii) builds abstractions from traces, (iii) constructs an MDP, and (iv) performs probabilistic model checking to compute bounds such as Pmax(success) and Pmin(failure). We also show how run likelihoods enable anomaly detection as a guardrailing signal.