On Probabilistic $\omega$-Pushdown Systems, and $\omega$-Probabilistic Computational Tree Logic

Abstract

In this paper, we define the notion of a {\em probabilistic $\omega$-pushdown automaton} and study its model-checking problem against $\omega$-probabilistic computational tree logic ($\omega$-PCTL) and its bounded version from a computational complexity perspective. Specifically, we obtain the following important new results: (1) We first discuss the expressiveness of the logics PCTL, PCTL$^*$, $\omega$-${\rm PCTL}$, and $\omega$-${\rm PCTL}^*$ and study how B\"uchi conditions of probabilistic $\omega$-pushdown systems influence $\omega$-PCTL formulas. We then investigate the model-checking problem for {\em stateless probabilistic $\omega$-pushdown system ($\omega$-pBPA)} against $\omega$-PCTL (as defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}). By constructing $\omega$-PCTL formulas that encode the {\em Post Correspondence Problem}, we show that this model-checking problem is generally undecidable. (2) We then study under which conditions there exists an algorithm for model-checking {\it stateless probabilistic $\omega$-pushdown systems} against $\omega$-PCTL-like logic. In particular, we show that the model-checking problem for {\it stateless probabilistic $\omega$-pushdown systems} against $\omega$-{\it bounded probabilistic computational tree logic} ($\omega$-bPCTL) is decidable and $\mathit{NP}$-hard. Currently, there is no known lower bound for this problem that is better than ours. (3) Finally, we investigate an upper bound for the model-checking problem for {\em stateless probabilistic $\omega$-pushdown systems} against $\omega$-bounded probabilistic computational tree logic ($\omega$-bPCTL). We propose a potential approach to solving it by establishing a conditional upper bound and analyze the challenges of this method.