概率自动机与概率单计数器自动机的分支时间性质模型检测
计算机科学中的逻辑
2023-07-19 v2 形式语言与自动机理论
逻辑
摘要
本文研究了概率自动机与概率单计数器自动机针对概率分支时间时序逻辑(PCTL与PCTL)的模型检测问题。我们证明这些问题是不可判定的。我们首先通过归约到概率自动机的空性问题，表明概率有限自动机针对分支时间时序逻辑的模型检测是不可判定的。进而，对于每个概率自动机，通过构造一个与所讨论概率自动机具有相同行为的概率单计数器自动机，由此得出针对分支时间时序逻辑的模型检测问题的不可判定性。
引用
@article{arxiv.1502.07549,
title = {Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata},
author = {T. Lin},
journal= {arXiv preprint arXiv:1502.07549},
year = {2023}
}
备注
This paper is no interesting today from the author's viewpoint, so withdrawn