Informace o publikaci
PCTL Satisfiability for Infinite Binary Trees
| Autoři | |
|---|---|
| Rok publikování | 2026 |
| Druh | Stať ve sborníku |
| Konference | Principles of Formal Quantitative Analysis : Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | DOI |
| Doi | https://doi.org/10.1007/978-3-031-97439-7_9 |
| Klíčová slova | Probabilistic temporal logic; PCTL |
| Popis | 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. |