PCTL Satisfiability for Infinite Binary Trees

KUČERA, Antonín. PCTL Satisfiability for Infinite Binary Trees. In Nathalie Bertrand, Clemens Dubslaff, Sascha Klüppelholz. Principles of Formal Quantitative Analysis : Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday. Berlin, Germany: Springer, 2026, s. 197-206. ISBN 978-3-031-97438-0. Dostupné z: https://doi.org/10.1007/978-3-031-97439-7_9.

Základní údaje

Originální název

PCTL Satisfiability for Infinite Binary Trees

Autoři

KUČERA, Antonín

Vydání

Berlin, Germany, Principles of Formal Quantitative Analysis : Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday, od s. 197-206, 10 s. 2026

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

DOI

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-97438-0

ISSN

DOI

https://doi.org/10.1007/978-3-031-97439-7_9

EID Scopus

2-s2.0-105016766010

Klíčová slova anglicky

Probabilistic temporal logic; PCTL

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.