On Probabilistic $\ddot{I}‰$-Pushdown Systems, and $\ddot{I}‰$-Probabilistic Computational Tree Logic

Abstract

In this paper, we define the notion of a {\em probabilistic $\ddot{I}‰$-pushdown automaton} and study its model-checking problem against $\ddot{I}‰$-probabilistic computational tree logic ($\ddot{I}‰$-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${}^{\ast }$, $\ddot{I}‰$-$\mathrm{PCTL}$, and $\ddot{I}‰$-${\mathrm{PCTL}}^{\ast }$ and study how Büchi conditions of probabilistic $\ddot{I}‰$-pushdown systems influence $\ddot{I}‰$-PCTL formulas. We then investigate the model-checking problem for {\em stateless probabilistic $\ddot{I}‰$-pushdown system ($\ddot{I}‰$-pBPA)} against $\ddot{I}‰$-PCTL (as defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}). By constructing $\ddot{I}‰$-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 $\ddot{I}‰$-pushdown systems} against $\ddot{I}‰$-PCTL-like logic. In particular, we show that the model-checking problem for {\it stateless probabilistic $\ddot{I}‰$-pushdown systems} against $\ddot{I}‰$-{\it bounded probabilistic computational tree logic} ($\ddot{I}‰$-bPCTL) is decidable and $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 $\ddot{I}‰$-pushdown systems} against $\ddot{I}‰$-bounded probabilistic computational tree logic ($\ddot{I}‰$-bPCTL). We propose a potential approach to solving it by establishing a conditional upper bound and analyze the challenges of this method.

[v19] Incorporating answers to anonymous readers' all comments; comments are welcome