为分布式大模型代理工作流设计实时验证逻辑，让决策基于因果可见事件。
Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
- 引入因果过去逻辑（CPL），支持条件和循环中对其他代理因果可见事件的检查。
- 通过向量时钟监控机制，实现本地实时计算与全局语义一致的验证结果。
- 适用于需严格因果控制的多代理系统，如分布式AI工作流协同场景。
分布式大模型代理工作流不应被当作单一顺序日志进行监控。在异步执行中，一个决策只能依赖于对该生命线因果可见的事件：某些在某日志中更早出现的事件可能在本地仍不可知。我们扩展了ZipperGen代理工作流框架，引入因果过去逻辑（Causal Past Logic, CPL），一种用于条件与循环守卫的小型过去时间时态逻辑。除标准过去时间模态（如previous、since）外，守卫还可检查另一生命线最新的因果可见事件及存储在其中的选定变量。该公式为源码级守卫，由所属生命线在线评估，并可实时影响控制流。我们设计了基于向量时钟的最新值视图监控器，并证明局部计算的监控值与守卫在当前事件下的语义定义一致。因此，运行时验证成为协调语言本身的组成部分，而非对执行日志的事后检查。
原文摘要 · Abstract (English)
Distributed LLM agent workflows should not be monitored as if they produced a single sequential log. In an asynchronous execution, a decision can only depend on events that are causally visible to the lifeline that makes it: an event that appears earlier in some log may still be unknown locally. We extend the ZipperGen agent-workflow framework with Causal Past Logic (CPL), a small past-time temporal logic for guards in conditionals and while loops. In addition to standard past-time modalities such as previous and since, a guard can inspect the latest causally visible event of another lifeline and selected variables stored there. The formula is a source-level guard: it is evaluated online by the owner lifeline and can influence control flow at runtime. We give a vector-clock monitor with latest-value views and prove that the locally computed monitor value coincides with the denotational semantics of the guard at the current event. Thus runtime verification becomes part of the coordination language itself, rather than a post-hoc check over an execution log.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。