TY - GEN
T1 - Quantum probabilistic dyadic second-order logic
AU - Baltag, Alexandru
AU - Bergfeld, Jort M.
AU - Kishida, Kohei
AU - Sack, Joshua
AU - Smets, Sonja J.L.
AU - Zhong, Shengyang
N1 - Funding Information:
The research of J. Bergfeld, K. Kishida and J. Sack has been funded by VIDI grant 639.072.904 of the NWO. The research of S. Smets is funded by the VIDI grant 639.072.904 of the NWO and by the FP7/2007-2013/ERC Grant agreement no. 283963. The research of S. Zhong has been funded by China Scholarship Council.
PY - 2013/10/9
Y1 - 2013/10/9
N2 - We propose an expressive but decidable logic for reasoning about quantum systems. The logic is endowed with tensor operators to capture properties of composite systems, and with probabilistic predication formulas P ≥ r (s), saying that a quantum system in state s will yield the answer 'yes' (i.e. it will collapse to a state satisfying property P) with a probability at least r whenever a binary measurement of property P is performed. Besides first-order quantifiers ranging over quantum states, we have two second-order quantifiers, one ranging over quantum-testable properties, the other over quantum actions. We use this formalism to express the correctness of some quantum programs. We prove decidability, via translation into the first-order logic of real numbers.
AB - We propose an expressive but decidable logic for reasoning about quantum systems. The logic is endowed with tensor operators to capture properties of composite systems, and with probabilistic predication formulas P ≥ r (s), saying that a quantum system in state s will yield the answer 'yes' (i.e. it will collapse to a state satisfying property P) with a probability at least r whenever a binary measurement of property P is performed. Besides first-order quantifiers ranging over quantum states, we have two second-order quantifiers, one ranging over quantum-testable properties, the other over quantum actions. We use this formalism to express the correctness of some quantum programs. We prove decidability, via translation into the first-order logic of real numbers.
UR - http://www.scopus.com/inward/record.url?scp=84885002914&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84885002914&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39992-3-9
DO - 10.1007/978-3-642-39992-3-9
M3 - Conference contribution
AN - SCOPUS:84885002914
SN - 9783642399916
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 64
EP - 80
BT - Logic, Language, Information, and Computation - 20th International Workshop, WoLLIC 2013, Proceedings
PB - Springer
T2 - 20th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2013
Y2 - 20 August 2013 through 23 August 2013
ER -