论文标题
关于反应性控制体系结构中的模块化，并应用正式验证
On modularity in reactive control architectures, with an application to formal verification
论文作者
论文摘要
在网络物理系统的整个设计过程中，模块化是一个中心原理。模块化会降低复杂性并增加行为的重复使用。在本文中，我们提出并回答以下问题：如何在反应性控制体系结构的结构中识别独立的“模块”？为此，我们提出了一种我们称为决策结构的图形结构构建体系结构，并展示了它如何概括一些在人工智能（AI）和机器人技术中流行的反应性控制体系结构，尤其是电信反应性程序（TRS），决策树（DTS），行为树（BTS），行为树（BTS）和广义行为树（$ k $ -bts）。受图理论中模块的定义的启发，我们定义了决策结构中的模块，并展示了每个决策结构如何在其模块中具有规范分解。我们可以自然地以其模块分解的属性来表征每个BTS，$ K $ -BTS，DTS和TRS。这使我们能够在二次时间内认识到哪些决策结构等于这些架构。在任何能够验证决策结构的验证方案下，我们提出的模块概念扩展到正式验证。也就是说，我们证明，对决策结构中模块的修改没有比修改该结构内的单个动作更大的流动效应。这使得可以在本地和层次上对模块进行验证，可以在该模块上进行验证，然后可以重复进行局部修改，然后由模块代替模块，同时保留正确性。为了说明发现，我们提供了一个由决策结构控制的太阳能无人机的示例。我们使用基于时间逻辑的线性验证方案来验证该结构的正确性，然后展示如何在保留其正确性的同时修改模块。
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.
