On Modularity in Reactive Control Architectures, with an Application to Formal Verification

AbstractModularity is a central principle throughout the design process for cyber-physical systems. Modularity reduces complexity and increases reuse of behavior. In this article 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 generalizes some reactive control architectures that 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 [16] we define modules in decision structures and show how each decision structure possesses a canonical decomposition into its modules, which can be found in polynomial time. We establish intuitive connections between our proposed modularity and modularity in structured programming. In BTs, k-BTs, and DTs the modules we propose are in a one-to-one correspondence with their subtrees. We show we can naturally characterize each of the BTs, k-BTs, DTs, and TRs by properties of their module decomposition. This allows us to recognize which decision structures are equivalent to each of these architectures in quadratic time. Following McCabe [26], we define a complexity measure called essential complexity on decision structures, which measures the degree to which they can be decomposed into simpler modules. We characterize the k-BTs as the decision structures of unit-essential complexity. 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 completing a reconnaissance-based mission using 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 repeatedly modify modules while preserving its correctness, and this can be verified by considering only those modules that have been modified.