# Reactive Control Meets Runtime Verification: A Case Study of Navigation

## TL;DR

This paper integrates formal runtime verification with reactive control for mobile robots, enabling safety and mission compliance through layered architecture and formal specifications, demonstrated via simulation.

## Contribution

It introduces a layered control architecture embedding runtime monitors from formal specs into robot navigation, enhancing reactive control with verification techniques.

## Key findings

- Successful simulation of robot navigation with integrated runtime verification
- Formal specifications improve safety and mission adherence
- Non-intrusive, compositional approach to control architecture

## Abstract

This paper presents an application of specification based runtime verification techniques to control mobile robots in a reactive manner. In our case study, we develop a layered control architecture where runtime monitors constructed from formal specifications are embedded into the navigation stack. We use temporal logic and regular expressions to describe safety requirements and mission specifications, respectively. An immediate benefit of our approach is that it leverages simple requirements and objectives of traditional control applications to more complex specifications in a non-intrusive and compositional way. Finally, we demonstrate a simulation of robots controlled by the proposed architecture and we discuss further extensions of our approach.