Reactive Control Meets Runtime Verification: A Case Study of Navigation
This work addresses safety and reliability in robotics navigation, but it is incremental as it applies existing runtime verification techniques to a specific case study.
The paper tackled the problem of controlling mobile robots by integrating runtime verification with reactive control, using formal specifications to ensure safety and mission compliance, and demonstrated the approach in a simulation.
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.