Searcharxiv⌕ Search

arXiv subjects

Deren Lin

Publications and source records attributed to Deren Lin.

3 recordsLinked to original sources
arXiv2025

Computational Complexity of Model-Checking Quantum Pushdown Systems

In this paper, we study the problem of model-checking quantum pushdown systems from a computational complexity point of view. We arrive at the following equally important, interesting new results: We first extend the notions of the {\it probabilistic pushdown systems} and {\it Markov chains} to their quantum counterparts, i.e., {\em quantum pushdown system (qPDS)} and {\em quantum Markov chains}, and prove a necessary and sufficient condition for a qPDS to be well formed, also presenting a method to extend the local transition function of a well-formed qPDS to a unitary local time evolution operator. Next, we investigate the question of whether it is necessary to define a quantum analogue of {\it probabilistic computational tree logic} to describe the probabilistic and branching-time properties of the {\it quantum Markov chain}. We study its model-checking question and show that model-checking of {\it stateless quantum pushdown systems (qBPA)} against {\it probabilistic computational tree logic (PCTL)} is generally undecidable, i.e., there exists no algorithm for model-checking {\it stateless quantum pushdown systems (qBPA)} against {\it probabilistic computational tree logic}. We then study in which case there exists an algorithm for model-checking {\it stateless quantum pushdown systems} and show that the problem of model-checking {\it stateless quantum pushdown systems (qBPA)} against {\it bounded probabilistic computational tree logic} (bPCTL) is decidable, and further show that this problem is in $\mathit{NP}$-hard. Our reduction is from the {\it bounded Post Correspondence Problem} for the first time, a well-known $\mathit{NP}$-complete problem.

cs.LO↗
arXiv2022

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

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.

cs.LO↗