Runtime Verification via Rational Monitor with Imperfect Information

TL;DR

This paper extends Runtime Verification to handle scenarios with imperfect information and rational monitors, enabling more reliable verification of autonomous systems operating in real-world environments.

Contribution

It introduces a novel approach to Runtime Verification that accounts for imperfect information and rational behavior of monitors, with practical implementation for robotic systems.

Findings

Successfully extended RV to imperfect information scenarios

Implemented a case study with robotic systems demonstrating effectiveness

Enhanced reliability of runtime verification in autonomous environments

Abstract

Trusting software systems, particularly autonomous ones, is challenging. To address this, formal verification techniques can ensure these systems behave as expected. Runtime Verification (RV) is a leading, lightweight method for verifying system behaviour during execution. However, traditional RV assumes perfect information, meaning the monitoring component perceives everything accurately. This assumption often fails, especially with autonomous systems operating in real-world environments where sensors might be faulty. Additionally, traditional RV considers the monitor to be passive, lacking the capability to interpret the system's information and thus unable to address incomplete data. In this work, we extend standard RV of Linear Temporal Logic properties to accommodate scenarios where the monitor has imperfect information and behaves rationally. We outline the necessary engineering steps to update the verification pipeline and demonstrate our implementation in a case study involving robotic systems.