  In this paper, we first define the quantum analogues of the {\em
probabilistic pushdown systems} and {\em Markov chains}, and investigate the
question whether it is necessary to define a quantum analogue of {\em
probabilistic computational tree logic} to describe the probabilistic and
branching-time properties of the {\em quantum Markov chain} defined here. We
study its model-checking question and show that the model-checking of {\em
stateless quantum pushdown systems (qBPA)} against {\em probabilistic
computational tree logic (PCTL)} is generally undecidable.
  We next define the notion of {\em probabilistic $\omega$-pushdown automaton}
for the first time and study the model-checking question of {\em stateless
probabilistic $\omega$-pushdown system ($\omega$-pBPA)} against $\omega$-PCTL
(defined by Chatterjee et al. in \cite{CSH08}) and show that the model-checking
of {\em stateless probabilistic $\omega$-pushdown systems ($\omega$-pBPA)}
against $\omega$-PCTL is generally undecidable. Our approach is to construct
formulas of $\omega$-PCTL encoding the {\em Post Correspondence Problem}
indirectly.
  Thirdly, since the notion of {\em weak bisimulation relation} is such
important and interesting in {\em concurrency theory}, we study and analysis
soundness and completeness of {\em weak bisimulation} for {\em $\omega$
probabilistic computational tree logic ($\omega$-PCTL$^*$)} and show that it is
sound and complete. Our models are probabilistic labelled transition systems
induced by probabilistic $\omega$-pushdown automata defined in this paper.
