发表机构
Ume University, Sweden（乌梅大学，瑞典）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究多智能体系统的验证问题，基于Tiles和Soda构建模块化框架，通过可执行验证管道操作动作语言语义，以类型化函数管道表示验证过程，含可执行规范层，有开源实现及示例说明。
AI 中文摘要
现有的关于动作和变化的推理方法为动态系统建模提供了富有表现力的语义，大多基于逻辑编程系统构建。我们基于瓦片（Tiles）引入了一个用于转换和轨迹验证的模块化框架，并在高效函数式编程语言Soda中实现。该框架通过可执行验证管道将动作语言语义操作化，管道将状态、动作、转换和规则作为组合函数组件处理。验证过程表示为类型化函数管道，实现模块化规范、可重用推理组件和具有保证管道终止的透明执行工作流程。框架包括一个可执行规范层，允许用户用YAML定义领域描述，将其操作化为底层验证模型和可执行管道结构。我们提供了开源实现，并通过涉及错误信息和情感推理的示例来说明该框架。
英文摘要
Existing approaches for reasoning about action and change provide expressive semantics for modeling dynamic systems, in most cases built on top of logic programming systems. We introduce a modular framework for transition and trajectory verification based on Tiles and implemented in Soda, which is an efficient functional programming language. The framework operationalizes action language semantics through executable verification pipelines that process states, actions, transitions, and rules as compositional functional components. Verification procedures are represented as typed functional pipelines, enabling modular specifications, reusable reasoning components, and transparent execution workflows with guaranteed pipeline termination. The framework includes an executable specification layer that allows users to define domain descriptions in YAML, which are operationalized into the underlying verification model and executable pipeline structure. We provide an open-source implementation and illustrate the framework through examples that involve misinformation and emotional reasoning.
