The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable

CHODIL, Miroslav a Antonín KUČERA. The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable. Online. In 52nd International Colloquium on Automata, Languages, and Programming. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025, s. 2867-2886. ISBN 978-3-95977-372-0. Dostupné z: https://doi.org/10.4230/LIPIcs.ICALP.2025.151.

Základní údaje

Originální název

The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable

Autoři

CHODIL, Miroslav a Antonín KUČERA ORCID

Vydání

Dagstuhl, Germany, 52nd International Colloquium on Automata, Languages, and Programming, od s. 2867-2886, 20 s. 2025

Nakladatel

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

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

Forma vydání

elektronická verze "online"

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/25:00141636

Organizační jednotka

Fakulta informatiky

ISBN

978-3-95977-372-0

ISSN

DOI

https://doi.org/10.4230/LIPIcs.ICALP.2025.151

UT WoS

001740139600151

EID Scopus

2-s2.0-105009914753

Klíčová slova anglicky

pctl; probablistic computation tree logic; markov chains; modal and temporal logics; probabilistic verification

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts, the decidability of PCTL satisfiability and validity problems remained unresolved for 30 years. We show that both problems are highly undecidable, i.e., beyond the arithmetical hierarchy. Consequently, there is no sound and complete deductive system for PCTL.

---

Návaznosti

GA21-24711S, projekt VaV	Název: Efektivní analýza a optimalizace pravděpodobnostních systémů a her (Akronym: Efektivní analýza a optimalizace pravděpodobnostní) Investor: Grantová agentura ČR, Efektivní analýza a optimalizace pravděpodobnostních systémů a her
MUNI/A/1600/2024, interní kód MU	Název: Modelování, analýza a verifikace (2025) Investor: Masarykova univerzita, Modelování, analýza a verifikace (2025)