Model-Checking Branching-Time Properties of Stateless Probabilistic Pushdown Systems and Related Expansion

In this work, we first resolve a question in the probabilistic verification of infinite-state systems (specifically, the probabilistic pushdown systems). We show that model checking stateless probabilistic pushdown systems (pBPA) against probabilistic computational tree logic (PCTL) is generally undecidable. We define the quantum analogues of the probabilistic pushdown systems and Markov chains and investigate whether it is necessary to define a quantum analogue of probabilistic computational tree logic to describe the branching-time properties of the quantum Markov chain. We also study its model-checking problem and show that the model-checking of stateless quantum pushdown systems (qBPA) against probabilistic computational tree logic (PCTL) is generally undecidable, too. The immediate corollaries of the above results are summarized in the work.