Scholarlink

We show that the problem whether a given PCTL formula has an infinite binary tree model where all transition probabilities are equal to 1/2 is highly undecidable (i.e., beyond the arithmetical hierarchy). This result holds even for the PCTL fragment where the set of modal connectives is restricted to the \(\textbf{F}\) and \(\textbf{G}\) operators, and even under the assumption that the PCTL formula on input is either unsatisfiable or it has a model with the aforementioned structure.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

PCTL Satisfiability for Infinite Binary Trees

  • 章节

  • 发表日期：

    2026年

查看全文
  • Antonín Kučera

摘要

We show that the problem whether a given PCTL formula has an infinite binary tree model where all transition probabilities are equal to 1/2 is highly undecidable (i.e., beyond the arithmetical hierarchy). This result holds even for the PCTL fragment where the set of modal connectives is restricted to the \(\textbf{F}\) and \(\textbf{G}\) operators, and even under the assumption that the PCTL formula on input is either unsatisfiable or it has a model with the aforementioned structure.