This paper studies the problem of model-checking of probabilistic automaton and probabilistic one-counter automata against probabilistic branching-time temporal logics (PCTL and PCTL$^*$). We show that it is undecidable for these problems. We first show, by reducing to emptiness problem of probabilistic automata, that the model-checking of probabilistic finite automata against branching-time temporal logics are undecidable. And then, for each probabilistic automata, by constructing a probabilistic one-counter automaton with the same behavior as questioned probabilistic automata the undecidability of model-checking problems against branching-time temporal logics are derived, herein.
翻译：本文研究了对概率自动图和概率单对子自动图进行模型检查以对抗概率分流时间逻辑( PCTL 和 PCTL$ $ $ ) 的概率自动图进行模型检查的问题。 我们发现,对于这些问题,这是不可测的。 我们首先通过将概率自动图的空洞问题降低到空洞程度,表明对分流时间时间逻辑的概率有限自动图进行模型检查是无法降解的。 然后,对于每一种概率自动图来说,通过构建一个概率单对子自动图,其行为与受质疑的概率自动图一样,可以产生模型检查问题对分流时间时间逻辑的不可降解性。
相关内容
微信扫码咨询专知VIP会员