未知马尔可夫链中的在线监测$omega$-正则属性
摘要：针对$omega$-regular属性，我们研究了运行时监控。我们考虑一个简单的设定，在这个设定中，一个未知有限状态马尔可夫链$\mathcal{M}$的运行被监控，以满足一个固定但任意的$omega$-regular规范$\varphi$。监控的目的是在$\mathcal{M}$执行正确运行之前，终止那些"不太可能"满足规范的运行。我们为复位动作设计了控制器(假设$\varphi$具有正概率)，满足以下性质概率为1：复位的次数是有限的，并且在最后一次复位之后由$\mathcal{M}$执行的运行满足$\varphi$。
作者：Javier Esparza, Stefan Kiefer, Jan Kretinsky and Maximilian Weininger
论文ID：2010.08347
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-07-21