We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.AI

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Artificial Intelligence

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

Authors: Oliver Biggar (1), Mohammad Zamani (2), Iman Shames (1) ((1) Australian National University, (2) Defence Science and Technology Group, Australia)
Abstract: 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.
Comments: Accepted to ACM Transactions on Cyber-Physical Systems. 26 pages, 9 figures. Version 3 changes: accepted version, minor changes
Subjects: Artificial Intelligence (cs.AI); Robotics (cs.RO)
Cite as: arXiv:2008.12515 [cs.AI]
  (or arXiv:2008.12515v3 [cs.AI] for this version)

Submission history

From: Oliver Biggar [view email]
[v1] Fri, 28 Aug 2020 07:25:38 GMT (88kb)
[v2] Tue, 4 May 2021 07:22:12 GMT (83kb)
[v3] Mon, 31 Jan 2022 02:19:04 GMT (85kb)

Link back to: arXiv, form interface, contact.