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

• Autoři: CHODIL Miroslav; KUČERA Antonín
• Rok publikování: 2025
• Druh: Článek ve sborníku
• Konference: 52nd International Colloquium on Automata, Languages, and Programming
• Fakulta / Pracoviště MU: Fakulta informatiky
• Doi: http://dx.doi.org/10.4230/LIPIcs.ICALP.2025.151
• Klíčová slova: pctl; probablistic computation tree logic; markov chains; modal and temporal logics; probabilistic verification
• Popis: 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.

Související projekty

• Efektivní analýza a optimalizace pravděpodobnostních systémů a her
• Modelování, analýza a verifikace (2025)