论文标题
在线监视$ω$ - 未知马尔可夫链中的属性
Online Monitoring $ω$-Regular Properties in Unknown Markov Chains
论文作者
论文摘要
我们研究了$ω$的属性属性的运行时监视。我们考虑一个简单的设置，其中未知的有限国家马尔可夫链的运行$ \ MATHCAL M $是根据固定但任意$ω$的规格$φ$监视的。监视的目的是保持“不太可能”满足规范的中止运行，直到$ \ nathcal m $执行正确的运行。我们为重置操作设计控制器（假设$φ$具有正概率）满足以下属性W.P.1：重置的数量是有限的，并且在上次重置后由$ \ Mathcal M $执行的运行可满足$φ$。
We study runtime monitoring of $ω$-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 $ω$-regular specification $φ$. 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 $φ$ 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 $φ$.
