Publication details
PCTL Satisfiability for Infinite Binary Trees
| Authors | |
|---|---|
| Year of publication | 2026 |
| Type | Paper in proceedings |
| Conference | Principles of Formal Quantitative Analysis : Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday |
| MU Faculty or unit | |
| Citation | |
| web | DOI |
| Doi | https://doi.org/10.1007/978-3-031-97439-7_9 |
| Keywords | Probabilistic temporal logic; PCTL |
| Description | We show that the problem of 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 F and G and operators, and even under the assumption that the PCTL formula on input is either unsatisfiable or it has a model with the aforementioned structure. |