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 $varphi$. 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 $varphi$ 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 $varphi$.
Download