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

TL;DR

This paper introduces probabilistic omegapushdown automata, explores their model-checking complexities against omegaPCTL, and establishes decidability and hardness results for specific cases.

Contribution

First definition and analysis of probabilistic omegapushdown automata, with complexity results for model-checking against omegaPCTL and omegabPCTL.

Findings

Model-checking omegapBPA against omegaPCTL is undecidable.

Model-checking omegapBPA against omegabPCTL is decidable.

The problem is NP-hard.

Abstract

In this paper, we define the notion of {\em probabilistic $\omega$-pushdown automaton} and study its model-checking problem against the logic of $\omega$-probabilistic computational tree logic ($\omega$-PCTL) and its bounded version from a computational complexity view. Specifically, we obtain the following equally important new results: (1) We define {\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, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $\omega$-pushdown systems ($\omega$-pBPA)} against $\omega$-PCTL is generally undecidable. Our approach is to construct $\omega$-PCTL formulas encoding the {\em Post Correspondence Problem}. (2) We then study in which case there exists an algorithm for model-checking {\it stateless probabilistic $\omega$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $\omega$-pushdown systems} against $\omega$-{\it bounded probabilistic computational tree logic} ($\omega$-bPCTL) is decidable, and further show that this problem is $\mathit{NP}$-hard.