Temporal logics for reasoning about quantum systems
Temporal logics for reasoning about quantum systems
复制标题
用于推理量子系统的时态逻辑
DOI：
10.1017/cbo9781139193313.011
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
C. Sernadas
中科院分区：
文献类型：
--
作者：
P. Mateus;J. Ramos;A. Sernadas;C. Sernadas
由于量子系统在信息处理、安全、分布式系统和随机算法等应用方面的巨大潜力，量子系统的推理得到了突出的应用。这一事实吸引了关于量子态、程序和过程的形式推理的研究。另一方面，时间逻辑已被证明在经典分布式系统和安全协议的验证中是成功的。在本章中，我们扩展外生量子命题逻辑与时间模态，考虑线性和分支时间。我们为所提出的量子时间逻辑提供了一个弱完备的希尔伯特演算，并研究了它们的SAT和模型检验问题。
Reasoning about quantum systems has gained prominence due to a big potential in applications such as information processing, security, distributed systems and randomized algorithms. This fact has attracted research in formal reasoning about quantum states, programs and processes. On the other hand, temporal logics have proved to be successful in the verification of classical distributed systems and security protocols. In this chapter we extend Exogenous Quantum Propositional Logic with temporal modalities, considering both linear and branching time. We provide a weakly complete Hilbert calculi for the proposed quantum temporal logics and study their SAT and model-checking problems.