The general/finite PCTL satisfiability problem asks whether a given PCTL formula has a general/finite model. We show that the finite PCTL satisfiability problem is undecidable, and the general PCTL satisfiability problem is even highly undecidable (beyond the arithmetical hierarchy). Consequently, there are no sound deductive systems proving all generally/finitely valid PCTL formulae.

翻译：一般/有限PCTL可满足问题询问给定PCTL公式是否存在一般/有限模型。我们证明有限PCTL可满足问题不可判定，而一般PCTL可满足问题甚至高度不可判定（超越算术层级）。因此，不存在能够证明所有一般/有限有效PCTL公式的可靠演绎系统。