Composable Verification Pipelines for Multi-Agent Systems
It provides a practical, composable verification tool for multi-agent systems, but the contribution is incremental.
The paper introduces a modular framework for transition and trajectory verification in multi-agent systems, implemented in Soda, that operationalizes action language semantics through executable verification pipelines. The framework enables modular specifications and reusable reasoning components with guaranteed pipeline termination.
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.