論文の概要: Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs

• arxiv url: http://arxiv.org/abs/2206.13772v1
• Date: Tue, 28 Jun 2022 05:49:55 GMT
• ステータス: 処理完了
• システム内更新日: 2023-02-07 12:56:23.872232
• Title: Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• Title（参考訳）: 量子プログラムにおける抽象解釈、ホーア論理、不正確な論理
• Authors: Yuan Feng and Sanjiang Li
• Abstract要約: フーア論理(ホーアりょうり、英: Hoare logic)は、コンピュータプログラムの静的解析において強力な手法である。 完全な量子抽象解釈は、量子ホア論理と量子不正確な論理を誘導することを示す。
• 参考スコア（独自算出の注目度）: 6.2147758224415055
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. All of them have been successfully extended to the quantum setting, but largely developed in parallel. In this paper, we examine the relationship between these techniques in the context of verifying quantum while-programs, where the abstract domain and the set of assertions for quantum states are well-structured. In particular, we show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, both of which are sound and relatively complete. Unlike the logics proposed in the literature, the induced logic systems are in a forward manner, making them more useful in certain applications. Conversely, any sound and relatively complete quantum Hoare logic or quantum incorrectness logic induces a complete quantum abstract interpretation. As an application, we are able to show the non-existence of any sound and relatively complete quantum Hoare logic or incorrectness logic if tuples of local subspaces are taken as assertions.
• Abstract（参考訳）: 抽象解釈、フーア論理、および逆ホーア論理は、コンピュータプログラムの静的解析のための強力な技術である。 これらはすべて量子設定に拡張されたが、ほとんど並列に開発された。 本稿では,量子状態の抽象領域とアサーションの集合がよく構造化されている量子時効プログラムの検証におけるこれらの手法の関係について検討する。 特に、任意の完全量子抽象解釈は量子ホア論理と量子不正確な論理を誘導し、どちらも健全かつ相対的に完全であることを示す。 文献で提案された論理とは異なり、誘導論理系は前方向きであり、特定の応用においてより有用である。 逆に、健全で比較的完全な量子ホア論理や量子不正確な論理は完全な量子抽象解釈を引き起こす。 アプリケーションとして、局所部分空間のタプルがアサーションとして取り込まれている場合、音と相対的に完全な量子ホア論理や不正確な論理の非存在を示すことができる。

関連論文リスト

• BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
  ヒープ操作を伴う量子プログラミング言語Q While-hpのセマンティクスについて述べる。 我々は,意味を分離するための解釈を含む,BIスタイルの量子論理を開発する。 次に、この量子BIスタイルの論理をアサーション言語として採用し、ヒープ制御量子プログラムを推論する。
  論文  参考訳（メタデータ） (2024-09-16T10:34:45Z)
• Quantum algorithms: A survey of applications and end-to-end complexities [90.05272647148196]
  期待されている量子コンピュータの応用は、科学と産業にまたがる。 本稿では,量子アルゴリズムの応用分野について検討する。 私たちは、各領域における課題と機会を"エンドツーエンド"な方法で概説します。
  論文  参考訳（メタデータ） (2023-10-04T17:53:55Z)
• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  ボソニックモード超伝導回路におけるコヒーレント状態量子プロセストモグラフィ(csQPT)の使用を実証する。 符号化量子ビット上の変位とSNAP演算を用いて構築した論理量子ゲートを特徴付けることにより,本手法の結果を示す。
  論文  参考訳（メタデータ） (2023-03-02T18:08:08Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  量子変数を持つ一階述語論理は、量子プログラムの様々な性質を特定し、推論するためのアサーション言語として必要とされる。 本稿では,Birkhoff-von Neumann量子論理を量子変数上の普遍的および存在的量子化器を用いて一階拡張する。
  論文  参考訳（メタデータ） (2022-05-04T08:57:44Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。 本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。 アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
  論文  参考訳（メタデータ） (2021-10-04T12:20:23Z)
• The Logic of Quantum Programs [77.34726150561087]
  本稿では,量子プログラムにおける情報フローの論理計算について述べる。 特に、複素量子系における量子測定、ユニタリ進化、絡み合いを扱うことができる動的論理を導入する。
  論文  参考訳（メタデータ） (2021-09-14T16:08:37Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。 本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
  論文  参考訳（メタデータ） (2021-07-05T17:45:41Z)
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic [22.507329566323982]
  プリコンディションとポストコンディションは、量子状態を記述するBI式である。 量子ワンタイムパッドとシークレット共有のセキュリティを証明するロジックを実践する。
  論文  参考訳（メタデータ） (2021-01-30T22:24:36Z)
• Quantum Hoare logic with classical variables [3.1181601933418897]
  古典変数と量子変数の両方を含む簡単な時相言語に対して量子ホア論理を提案する。 古典量子状態とそれに対応するアサーションの新たな定義により、論理体系は非常に単純であり、古典的プログラムの伝統的なホア論理と類似している。
  論文  参考訳（メタデータ） (2020-08-15T23:56:18Z)
• Operational Resource Theory of Imaginarity [48.7576911714538]
  量子状態は、実際の要素しか持たなければ、生成や操作が容易であることを示す。 応用として、想像力は国家の差別にとって重要な役割を担っていることを示す。
  論文  参考訳（メタデータ） (2020-07-29T14:03:38Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。