Category Theory for Autonomous Robots: The Marathon 2 Use Case

TL;DR

This paper explores applying Category Theory to formalize models for autonomous robots, enabling better design, recovery, and trustworthiness, demonstrated through the Marathon 2 experiment.

Contribution

It introduces the use of Category Theory for modeling autonomous robots beyond design, including runtime recovery mechanisms, enhancing reliability and performance.

Findings

Formal models can be used at runtime for autonomous robots.

Category Theory provides a rigorous framework for robot modeling.

Application to Marathon 2 demonstrates practical benefits.

Abstract

Model-based systems engineering (MBSE) is a methodology that exploits system representation during the entire system life-cycle. The use of formal models has gained momentum in robotics engineering over the past few years. Models play a crucial role in robot design; they serve as the basis for achieving holistic properties, such as functional reliability or adaptive resilience, and facilitate the automated production of modules. We propose the use of formal conceptualizations beyond the engineering phase, providing accurate models that can be leveraged at runtime. This paper explores the use of Category Theory, a mathematical framework for describing abstractions, as a formal language to produce such robot models. To showcase its practical application, we present a concrete example based on the Marathon 2 experiment. Here, we illustrate the potential of formalizing systems -- including their recovery mechanisms -- which allows engineers to design more trustworthy autonomous robots. This, in turn, enhances their dependability and performance.