Online Monitoring $\omega$-Regular Properties in Unknown Markov Chains

Abstract

We study runtime monitoring of $\omega$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $\mathcal{M}$ is monitored against a fixed but arbitrary $\omega$-regular specification $\phi$. The purpose of monitoring is to keep aborting runs that are "unlikely" to satisfy the specification until $\mathcal{M}$ executes a correct run. We design controllers for the reset action that (assuming that $\phi$ has positive probability) satisfy the following property w.p.1: the number of resets is finite, and the run executed by $\mathcal{M}$ after the last reset satisfies $\phi$.