# On modularity in reactive control architectures, with an application to formal verification

arXiv: https://arxiv.org/abs/2008.12515 · HTML: https://mlsanity.com/paper/2008.12515/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Aug 2020.

## Built on by (most cited first, 11 of 11)

- [Behavior Trees in Robot Control Systems](https://mlsanity.com/paper/2203.13083/) (2022)
- [An expressiveness hierarchy of Behavior Trees and related architectures](https://mlsanity.com/paper/2104.07919/) (2021)
- [Designing Behavior Trees from Goal-Oriented LTLf Formulas](https://mlsanity.com/paper/2307.06399/) (2023)
- [A Unified Framework for Real-Time Failure Handling in Robotics Using Vision-Language Models, Reactive Planner and Behavior Trees](https://mlsanity.com/paper/2503.15202/) (2025)
- [Continuous-Time Behavior Trees as Discontinuous Dynamical Systems](https://mlsanity.com/paper/2109.01575/) (2021)
- [BVR Gym: A Reinforcement Learning Environment for Beyond-Visual-Range Air Combat](https://mlsanity.com/paper/2403.17533/) (2024)
- [A Unified Architecture for Dynamic Role Allocation and Collaborative Task Planning in Mixed Human-Robot Teams](https://mlsanity.com/paper/2301.08038/) (2023)
- [An Extended Convergence Result for Behaviour Tree Controllers](https://mlsanity.com/paper/2308.08994/) (2023)
- [Adaptable Recovery Behaviors in Robotics: A Behavior Trees and Motion Generators(BTMG) Approach for Failure Management](https://mlsanity.com/paper/2404.06129/) (2024)
- [Behavior Trees Enable Structured Programming of Language Model Agents](https://mlsanity.com/paper/2404.07439/) (2024)
- [Progress Constraints for Reinforcement Learning in Behavior Trees](https://mlsanity.com/paper/2602.06525/) (2026)

## Abstract (arXiv)

Modularity is a central principle throughout the design process for cyber-physical systems. Modularity reduces complexity and increases reuse of behavior. In this paper we pose and answer the following question: how can we identify independent `modules' within the structure of reactive control architectures? To this end, we propose a graph-structured control architecture we call a decision structure, and show how it generalises some reactive control architectures which are popular in Artificial Intelligence (AI) and robotics, specifically Teleo-Reactive programs (TRs), Decision Trees (DTs), Behavior Trees (BTs) and Generalised Behavior Trees (k-BTs). Inspired by the definition of a module in graph theory, we define modules in decision structures and show how each decision structure possesses a canonical decomposition into its modules. We can naturally characterise each of the BTs, k-BTs, DTs and TRs by properties of their module decomposition. This allows us to recognise which decision structures are equivalent to each of these architectures in quadratic time. Our proposed concept of modules extends to formal verification, under any verification scheme capable of verifying a decision structure. Namely, we prove that a modification to a module within a decision structure has no greater flow-on effects than a modification to an individual action within that structure. This enables verification on modules to be done locally and hierarchically, where structures can be verified and then repeatedly locally modified, with modules replaced by modules while preserving correctness. To illustrate the findings, we present an example of a solar-powered drone controlled by a decision structure. We use a Linear Temporal Logic-based verification scheme to verify the correctness of this structure, and then show how one can modify modules while preserving its correctness.