Quantum computation tree logic - Model checking and complete calculus

被引：16

作者：

Baltazar, P. ^{[1
,3
]}

Chadha, R. ^{[2
]}

Mateus, P. ^{[1
,3
]}

机构：

[1] Univ Tecn Lisboa, SQIG, Inst Telecommun, P-1049001 Lisbon, Portugal

[2] Univ Illinois, Dept Comp Sci, Urbana, IL 61821 USA

[3] Univ Tecn Lisboa, IST, P-1049001 Lisbon, Portugal

来源：

INTERNATIONAL JOURNAL OF QUANTUM INFORMATION | 2008年 / 6卷 / 02期

关键词：

quantum logic; verifying quantum systems; completeness;

D O I：

10.1142/S0219749908003530

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Logics for reasoning about quantum states and their evolution have been given in the literature. In this paper, we consider quantum computation tree logic ( QCTL), which adds temporal modalities to exogenous quantum propositional logic. We give a sound and complete axiomatization of QCTL and combine the standard CTL model- checking algorithm with the dEQPL model- checking algorithm to obtain a model- checking algorithm for QCTL. Finally, we illustrate the use of the logic by reasoning about the BB84 key distribution protocol.

引用

页码：219 / 236

页数：18

共 50 条

[21] Computation tree logic model checking based on multi-valued possibility measures
Li, Yongming
Lei, Lihui
Li, Sanjiang
[J]. INFORMATION SCIENCES, 2019, 485 : 87 - 113
[22] An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking
Wei Xiujuan
Li Yongming
[J]. CHINESE JOURNAL OF ELECTRONICS, 2019, 28 (02) : 309 - 315
[23] An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking
WEI Xiujuan
LI Yongming
[J]. Chinese Journal of Electronics, 2019, 28 (02) : 309 - 315
[24] Bounded Model Checking for Weighted Interpreted Systems and for Flat Weighted Epistemic Computation Tree Logic
Wozna-Szczesniak, Bozena
Szczesniak, Ireneusz
Zbrzezny, Agnieszka M.
Zbrzezny, Andrzej
[J]. PRIMA 2014: PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS, 2014, 8861 : 107 - 115
[25] Inconsistency-tolerant Hierarchical Probabilistic Computation Tree Logic and Its Application to Model Checking
Kamide, Norihiro
Yamamoto, Noriko
[J]. ICAART: PROCEEDINGS OF THE 13TH INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE - VOL 2, 2021, : 490 - 499
[26] Sound and Complete Tree-Sequent Calculus for Inquisitive Logic
Sano, Katsuhiko
[J]. LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, 2009, 5514 : 365 - 378
[27] A Modal Logic for pi-Calculus and Model Checking Algorithm
Chen, Taolue
Han, Tingting
Lu, Jian
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 123 : 19 - 33
[28] An AC complete model checking problem for intuitionistic logic
Mundhenk, Martin
Wei, Felix
[J]. COMPUTATIONAL COMPLEXITY, 2014, 23 (04) : 637 - 669
[29] Cache Timing Side-Channel Vulnerability Checking with Computation Tree Logic
Deng, Shuwen
Xiong, Wenjie
Szefer, Jakub
[J]. PROCEEDINGS OF THE 7TH INTERNATIONAL WORKSHOP ON HARDWARE AND ARCHITECTURAL SUPPORT FOR SECURITY AND PRIVACY (HASP '18), 2018,
[30] Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques
Wuniu LIU
Junmei WANG
Qing HE
Yongming LI
[J]. Chinese Journal of Electronics., 2024, 33 (06) - 1411

← 1 2 3 4 5 →