The finite satisfiability problem for PCTL is undecidable

DOI10.1145/3661814.3662145MaRDI QIDQ6970256zbMATH OpenFDO

Authors Miroslav Chodil, Antonin Kučera

Publication date 18 June 2025

Full work available at URL https://doi.org/10.1145/3661814.3662145

zbMATH Keywords

PCTLprobabilistic temporal logicssatisfiability

Mathematics Subject Classification ID

Temporal logic (03B44) Probability and inductive logic (03B48) Undecidability and degrees of sets of sentences (03D35)

Cites work

• A logic for reasoning about time and reliability
• Bounded satisfiability for PCTL
• Boundedness problems for Minsky counter machines
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 765034 (Why is no real title available?)
• scientific article; zbMATH DE number 7280017 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Model checking of probabilistic and nondeterministic systems
• Model checking of recursive probabilistic systems
• Model Checking Probabilistic Pushdown Automata
• On the satisfiability of some simple probabilistic logics
• Reasoning with time and chance
• STACS 2005
• The satisfiability problem for a quantitative fragment of PCTL
• The satisfiability problem for unbounded fragments of probabilistic CTL

Cited in

(1)

• Probabilistic temporal reasoning using superposition semantics

This page was built for publication: The finite satisfiability problem for PCTL is undecidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6970256)