# Bayesian Verification under Model Uncertainty

## TL;DR

This paper introduces a Bayesian approach for runtime verification of systems with uncertain models, defining subjective satisfaction and providing stochastic error bounds, demonstrated through an example application.

## Contribution

It proposes the BV algorithm, a Bayesian method for verifying subjective satisfaction under model uncertainty, addressing challenges of limited data and undefined satisfaction criteria.

## Key findings

- BV algorithm offers stochastic bounds for verification errors
- Empirical results demonstrate effectiveness in example application
- Addresses model uncertainty in runtime verification

## Abstract

Machine learning enables systems to build and update domain models based on runtime observations. In this paper, we study statistical model checking and runtime verification for systems with this ability. Two challenges arise: (1) Models built from limited runtime data yield uncertainty to be dealt with. (2) There is no definition of satisfaction w.r.t. uncertain hypotheses. We propose such a definition of subjective satisfaction based on recently introduced satisfaction functions. We also propose the BV algorithm as a Bayesian solution to runtime verification of subjective satisfaction under model uncertainty. BV provides user-definable stochastic bounds for type I and II errors. We discuss empirical results from an example application to illustrate our ideas.