Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems

2014/05/19 by Lin, Deren, Lin, Tianrong
#F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Languages and Automata Theory (cs.FL) #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1405.4806

Abstract

In this communication, we resolve a longstanding open question in the probabilistic verification of infinite-state systems. We show that model checking \it stateless probabilistic pushdown systems (pBPA) against \it probabilistic computational tree logic (PCTL) is generally undecidable.

Related

• On Probabilistic ω-Pushdown Systems, and ω-Probabilistic Computational Tree Logic
• The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable
• Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata
• Robust Probabilistic Temporal Logics
• Bounded Satisfiability for PCTL