Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect
Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect
复制标题
量子逻辑的线性时间扩展及其动态方面的语义分析
DOI：
10.1145/3576926
复制
发表时间：
2023
影响因子：
0.5
通讯作者：
Tsubasa Takagi
中科院分区：
文献类型：
--
作者：
段野下 宙志;長谷川 寛;樋口 翔;松田 広志;川崎 卓郎;Stefanus Harjo;梅澤 修;Tsubasa Takagi
虽然已经提出了各种动态或时态逻辑来验证量子协议和系统，但这两种观点还没有得到足够全面的研究。我们提出了线性时间量子逻辑（LTQL），量子逻辑的线性时间扩展与量子蕴涵，并将其扩展到动态线性时间量子逻辑（DLTQL）。这种逻辑有时间算子来表达酉算子（量子门）和动态算子来表达投影（投影测量）。然后，我们证明了一些逻辑性质的关系，这两个转换表示的LTQL和DLTQL。将LTQL应用于量子协议验证的一个缺点是，这些逻辑不能表示线性时态逻辑中的未来算子。我们提出了一种方法来减轻这个缺点，通过使用从（D）LTQL的线性时序模态逻辑（LTML）和模拟的翻译。这种转换将（D）LTQL公式的可满足性问题简化为具有量子态经典语义的LTML公式的可满足性问题。
Although various dynamic or temporal logics have been proposed to verify quantum protocols and systems, these two viewpoints have not been studied comprehensively enough. We propose Linear Temporal Quantum Logic (LTQL), a linear temporal extension of quantum logic with a quantum implication, and extend it to Dynamic Linear Temporal Quantum Logic (DLTQL). This logic has temporal operators to express transitions by unitary operators (quantum gates) and dynamic ones to express those by projections (projective measurement). We then prove some logical properties of the relationship between these two transitions expressed by LTQL and DLTQL. A drawback in applying LTQL to the verification of quantum protocols is that these logics cannot express the future operator in linear temporal logic. We propose a way to mitigate this drawback by using a translation from (D)LTQL to Linear Temporal Modal Logic (LTML) and a simulation. This translation reduces the satisfiability problem of (D)LTQL formulas to that of LTML with the classical semantics over quantum states.
登录
查看更多内容
量子逻辑中的条件
影响因子：
1.5
作者：
Gary M. Hardegree
通讯作者：
Gary M. Hardegree
DOI：
10.1007/bf02120818
发表时间：
1972
期刊：
影响因子：
--
作者：
H. Dishkant
通讯作者：
H. Dishkant
正交模格中的蕴涵连接词
DOI：
10.1305/ndjfl/1093891789
发表时间：
1975
期刊：
Notre Dame J. Formal Log.
影响因子：
--
作者：
L. Herman;E. Marsden;R. Piziak
通讯作者：
R. Piziak
用于推理量子系统的时态逻辑
DOI：
10.1017/cbo9781139193313.011
发表时间：
2009
期刊：
影响因子：
--
作者：
P. Mateus;J. Ramos;A. Sernadas;C. Sernadas
通讯作者：
C. Sernadas
DOI：
10.1016/0097-3165(71)90040-9
发表时间：
1971
期刊：
J. Comb. Theory A
影响因子：
--
作者：
D. Foulis;C. H. Randall
通讯作者：
C. H. Randall