論文の概要: Model-Checking PCTL properties of Stateless Probabilistic Pushdown
Systems with Various Extensions
- arxiv url: http://arxiv.org/abs/2209.10517v7
- Date: Tue, 8 Aug 2023 00:42:01 GMT
- ステータス: 処理完了
- システム内更新日: 2023-08-27 05:32:15.944543
- Title: Model-Checking PCTL properties of Stateless Probabilistic Pushdown
Systems with Various Extensions
- Title(参考訳): 各種拡張を有する無定常確率型プッシュダウンシステムのモデルチェッキングPCTL特性
- Authors: Tianrong Lin
- Abstract要約: まず、無限状態系の確率的検証(具体的には、エム状態のない確率的プッシュダウンシステム)における開問題を解決する。
モデル検査は,pBPA (Stateless Probabilistic Pushdown System) とPCTL (Em Probabilistic Computing Tree logic) の併用が一般的ではないことを示す。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: In this paper, we first resolve an open question in the probabilistic
verification of infinite-state systems (specifically, the {\em stateless
probabilistic pushdown systems}). We show that model checking {\em stateless
probabilistic pushdown systems (pBPA)} against {\em probabilistic computational
tree logic (PCTL)} is generally undecidable. We define the quantum analogues of
the {\em probabilistic pushdown systems} and {\em Markov chains}, and further
investigate whether it is necessary to define a quantum analogue of {\em
probabilistic computational tree logic} to describe the branching-time
properties of the {\em quantum Markov chain} defined in this paper. We study
its model-checking question and show that the model-checking of {\em stateless
quantum pushdown systems (qBPA)} against {\em probabilistic computational tree
logic (PCTL)} is generally undecidable, with the immediate corollaries
summarized. We define the notion of {\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 et al. in \cite{CSH08}) and show that the
model-checking of {\em stateless probabilistic $\omega$-pushdown systems
($\omega$-pBPA)} against $\omega$-PCTL is generally undecidable, with immediate
consequences summarized. Our approach is to construct formulas of $\omega$-PCTL
encoding the {\em Post Correspondence Problem} indirectly.
- Abstract(参考訳): 本稿では、まず、無限状態系の確率的検証(具体的には、状態のない確率的プッシュダウン系)における開問題を解決する。
我々は、モデルチェック {\em stateless probabilistic pushdown system (pBPA) が一般には決定不可能であることを示す。
我々は「em確率的プッシュダウンシステム」と「emマルコフ連鎖」の量子アナログを定義し、本論文で定義された「em量子マルコフ連鎖」の分岐時間特性を記述するために「em確率的計算木論理」の量子アナログを定義する必要があるかどうかをさらに検討する。
モデルチェック問題について検討し,計算木論理 (PCTL) に対する状態のない量子プッシュダウンシステム (qBPA) のモデルチェックが概ね決定不可能であることを示す。
我々は「em確率的$\omega$-pushdown automaton」の概念を初めて定義し、"em stateless probabilistic $\omega$-pushdown system (\omega$-pbpa)} と$\omega$-pctl (chatterjee et al. in \cite{csh08}) とのモデルチェック問題を調べ、"em stateless probabilistic $\omega$-pushdown system (\omega$-pbpa)} と$\omega$-pctl のモデルチェックが一般に決定不能であることを示し、その結果を要約する。
我々のアプローチは間接的に$\omega$-PCTLを符号化する公式を構築することである。
関連論文リスト
- The Power of Unentangled Quantum Proofs with Non-negative Amplitudes [55.90795112399611]
非負の振幅を持つ非絡み合った量子証明のパワー、つまり $textQMA+(2)$ を表すクラスについて研究する。
特に,小集合拡張,ユニークなゲーム,PCP検証のためのグローバルプロトコルを設計する。
QMA(2) が $textQMA+(2)$ に等しいことを示す。
論文 参考訳(メタデータ) (2024-02-29T01:35:46Z) - Simulation of IBM's kicked Ising experiment with Projected Entangled
Pair Operator [71.10376783074766]
我々は最近,誤りを軽減した量子回路を用いてエミュレートされた127量子ビットキックド・イジングモデルの古典的シミュレーションを行った。
提案手法はハイゼンベルク図の射影的絡み合ったペア作用素(PEPO)に基づいている。
我々はクリフォード展開理論を開発し、正確な期待値を計算し、それらをアルゴリズムの評価に利用する。
論文 参考訳(メタデータ) (2023-08-06T10:24:23Z) - On sampling determinantal and Pfaffian point processes on a quantum
computer [49.1574468325115]
DPPは1970年代の量子光学のモデルとしてマッキによって導入された。
ほとんどのアプリケーションはDPPからのサンプリングを必要としており、その量子起源を考えると、古典的なコンピュータでDPPをサンプリングするのは古典的なものよりも簡単かどうか疑問に思うのが自然である。
バニラサンプリングは、各コスト$mathcalO(N3)$と$mathcalO(Nr2)$の2つのステップから構成される。
論文 参考訳(メタデータ) (2023-05-25T08:43:11Z) - A Quantum Algorithm Framework for Discrete Probability Distributions with Applications to Rényi Entropy Estimation [13.810917492304565]
離散確率分布の特性を推定するための統一量子アルゴリズムフレームワークを提案する。
我々のフレームワークは、$alpha$-R'enyi entropy $H_alpha(p)$を、少なくとも2/3$の確率で加算エラー$epsilon$内で推定する。
論文 参考訳(メタデータ) (2022-12-03T08:01:55Z) - Quantum Approximate Counting for Markov Chains and Application to
Collision Counting [0.0]
我々は,ブラザード,ホイヤー,タップ(ICALP 1998)によって開発された量子近似計数法を一般化し,マルコフ連鎖のマーク状態の数を推定する方法を示す。
これにより、Magniez、Nayak、Roland、Santhaによって確立された強力な"量子ウォークベースサーチ"フレームワークに基づいて、量子検索アルゴリズムから量子近似カウントアルゴリズムを構築することができる。
論文 参考訳(メタデータ) (2022-04-06T03:04:42Z) - Speeding up Learning Quantum States through Group Equivariant
Convolutional Quantum Ans\"atze [13.651587339535961]
我々はSU$(d)$対称性を持つ畳み込み量子回路の枠組みを開発する。
我々は、$nameSU(d)$と$S_n$ irrepbasesの同値性に関するHarrowの主張を証明する。
論文 参考訳(メタデータ) (2021-12-14T18:03:43Z) - Random quantum circuits transform local noise into global white noise [118.18170052022323]
低忠実度状態におけるノイズランダム量子回路の測定結果の分布について検討する。
十分に弱くユニタリな局所雑音に対して、一般的なノイズ回路インスタンスの出力分布$p_textnoisy$間の相関(線形クロスエントロピーベンチマークで測定)は指数関数的に減少する。
ノイズが不整合であれば、出力分布は、正確に同じ速度で均一分布の$p_textunif$に近づく。
論文 参考訳(メタデータ) (2021-11-29T19:26:28Z) - Sublinear quantum algorithms for estimating von Neumann entropy [18.30551855632791]
我々は、確率分布のシャノンエントロピーと混合量子状態のフォン・ノイマンエントロピーの乗法係数$gamma>1$における推定値を得る問題を研究する。
我々は古典的確率分布と混合量子状態の両方を扱える量子純粋クエリーアクセスモデルに取り組んでおり、文献の中では最も一般的な入力モデルである。
論文 参考訳(メタデータ) (2021-11-22T12:00:45Z) - Predictability as a quantum resource [0.0]
状態$rho$,$P$ of $rho$で作成されたシステムに対して、観測可能な$X$を参照して、$C$と等しいことを示す。
また、予測可能性に関するリソース理論を提案し、その自由量子状態と自由量子演算を同定する。
論文 参考訳(メタデータ) (2021-07-28T16:27:17Z) - Random quantum circuits anti-concentrate in log depth [118.18170052022323]
本研究では,典型的な回路インスタンスにおける測定結果の分布に要するゲート数について検討する。
我々の反集中の定義は、予測衝突確率が分布が均一である場合よりも大きい定数因子に過ぎないということである。
ゲートが1D環上で最寄りである場合と、ゲートが長距離である場合の両方において、$O(n log(n))ゲートも十分であることを示す。
論文 参考訳(メタデータ) (2020-11-24T18:44:57Z) - Quantum Algorithms for Simulating the Lattice Schwinger Model [63.18141027763459]
NISQとフォールトトレラントの両方の設定で格子シュウィンガーモデルをシミュレートするために、スケーラブルで明示的なデジタル量子アルゴリズムを提供する。
格子単位において、結合定数$x-1/2$と電場カットオフ$x-1/2Lambda$を持つ$N/2$物理サイト上のシュウィンガーモデルを求める。
NISQと耐故障性の両方でコストがかかるオブザーバブルを、単純なオブザーバブルとして推定し、平均ペア密度を推定する。
論文 参考訳(メタデータ) (2020-02-25T19:18:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。