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.
翻译:分布式LLM智能体工作流不应被当作产生单一顺序日志来监控。在异步执行中,决策仅能依赖于因果上对执行该决策的执行线可见的事件:即某个日志中较早出现的事件可能仍未被局部知晓。我们扩展了ZipperGen智能体工作流框架,引入了因果过去时逻辑(CPL),这是一种用于条件语句和while循环中守卫条件的小型过去时态时序逻辑。除了标准的过去时态模态(如previous和since)外,守卫条件还可检查另一执行线的最新因果可见事件及其存储的选定变量。该公式是源级守卫条件:由所属执行线在线评估,并可在运行时影响控制流。我们提出了一种具有最新值视图的向量时钟监控器,并证明了局部计算的监控器值与当前事件处守卫条件的指称语义一致。由此,运行时验证成为协调语言本身的组成部分,而非基于执行日志的事后检查。