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 条

[1] Model checking quantified computation tree logic
Rensink, Arend
[J]. CONCUR 2006 - CONCURRENCY THEORY, PROCEEDINGS, 2006, 4137 : 110 - 125
[2] Model checking fuzzy computation tree logic
Pan, Haiyu
Li, Yongming
Cao, Yongzhi
Ma, Zhanyou
[J]. FUZZY SETS AND SYSTEMS, 2015, 262 : 60 - 77
[3] VECTORIZED MODEL CHECKING FOR COMPUTATION TREE LOGIC
HIRAISHI, H
MEKI, S
HAMAGUCHI, K
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 44 - 53
[4] Model Checking for the Full Hybrid Computation Tree Logic
Kernberger, Daniel
Lange, Martin
[J]. PROCEEDINGS 23RD INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING - TIME 2016, 2016, : 31 - 40
[5] Model checking computation tree logic over finite lattices
Pan, Haiyu
Li, Yongming
Cao, Yongzhi
Ma, Zhanyou
[J]. THEORETICAL COMPUTER SCIENCE, 2016, 612 : 45 - 62
[6] Computation tree logic model checking based on possibility measures
Li, Yongming
Li, Yali
Ma, Zhanyou
[J]. FUZZY SETS AND SYSTEMS, 2015, 262 : 44 - 59
[7] Polytime model checking for timed probabilistic computation tree logic
Beauquier, D
Slissenko, A
[J]. ACTA INFORMATICA, 1998, 35 (08) : 645 - 664
[8] Polytime model checking for timed probabilistic computation tree logic
Danièle Beauquier
Anatol Slissenko
[J]. Acta Informatica, 1998, 35 : 645 - 664
[9] Computation Tree Logic Formula Model Checking Using DNA Computing
Han, Ying-Jie
Wang, Jian-Wei
Huang, Chun
Zhou, Qing-Lei
[J]. JOURNAL OF NANOELECTRONICS AND OPTOELECTRONICS, 2020, 15 (05) : 620 - 629
[10] Generalized possibility computation tree logic with frequency and its model checking
He, Qing
Liu, Wuniu
Li, Yongming
[J]. INTERNATIONAL JOURNAL OF APPROXIMATE REASONING, 2024, 173

← 1 2 3 4 5 →