On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2022
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917378640576512 |
|---|---|
| author | Lin, Deren Lin, Tianrong |
| author_facet | Lin, Deren Lin, Tianrong |
| contents | In this paper, we define the notion of {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against the logic of $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity view. Specifically, we obtain the following equally important new results:
(1) We define {\em probabilistic $ω$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $ω$-pushdown systems ($ω$-pBPA)} against $ω$-PCTL is generally undecidable. Our approach is to construct $ω$-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 $ω$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable, and further show that this problem is $\mathit{NP}$-hard. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2209_10517 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic Lin, Deren Lin, Tianrong Logic in Computer Science Formal Languages and Automata Theory Quantum Physics 03B25, 03B45, 03B70 In this paper, we define the notion of {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against the logic of $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity view. Specifically, we obtain the following equally important new results: (1) We define {\em probabilistic $ω$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $ω$-pushdown systems ($ω$-pBPA)} against $ω$-PCTL is generally undecidable. Our approach is to construct $ω$-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 $ω$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable, and further show that this problem is $\mathit{NP}$-hard. |
| title | On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic |
| topic | Logic in Computer Science Formal Languages and Automata Theory Quantum Physics 03B25, 03B45, 03B70 |
| url | https://arxiv.org/abs/2209.10517 |