D 2025

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

CHODIL, Miroslav a Antonín KUČERA

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

Vydání

Neuvedeno, 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"

Organizační jednotka

Fakulta informatiky

ISBN

978-3-95977-372-0

DOI

Klíčová slova anglicky

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

Štítky

Změněno: 19. 7. 2025 14:44, RNDr. Miroslav Chodil

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)